Fix "Interrupt computations" on Windows #16142

jfehrle · 2022-06-06T00:26:24Z

Windows doesn't support signals, so another mechanism was used to support "Interrupt computations" in CoqIDE. On Windows, every process that shares a console (i.e. coqide and all the coqidetop's and worker processes) receives the interrupt. This PR creates an empty file in a temp directory to signal which coqtopide should pay attention to the interrupt. The others will ignore it.

For all major releases back to 8.5pl3, interrupt stops working in a buffer after it's been reset. The original code in coqide_WIN32.c.in dating from 2011 called FreeConsole(), which detaches coqide from the console. Then when you subsequently reset the CoqIDE buffer, creating a new process, the new coqidetop doesn't inherit the console, so it can't be interrupted.

Also, contrary to the documentation, the SetConsoleCtrlHandler appears to affect more than the calling process. Removing that means that coqide will send the signal to itself, so I added code to ignore the signal in that case.

I suspect the bug dates to the original code rather than being a regression. It's possible this worked in 2011 and that the behavior of these Windows calls has changed. I'm on Windows 10.

While I've tested this a lot, it would be nice to get someone with a fresh perspective to try it on Windows in case I missed something.

Fixes: #13550

jfehrle · 2022-06-06T01:34:10Z

The dune file and the setup for the additional OS specific file seem pretty wordy. I'm open to suggestions on how to improve them. Rudi had some suggestions in #16139.

ide/coqide/dune

ide/coqide/shared_X11.c.in

ide/coqide/shared_QUARTZ.c.in

Alizter · 2022-06-07T13:03:41Z

ide/coqide/coq.ml

-    try !interrupter (CoqTop.unixpid coqtop.handle.proc)
+    try
+      let pid = CoqTop.unixpid coqtop.handle.proc in
+      if Sys.os_type = "Win32" then begin


There is also a "Cygwin" value for this. Which windows setup does the issue occur on?

https://v2.ocaml.org/api/Sys.html

The documentation you linked to says

"Cygwin" (for MS-Windows, OCaml compiled with Cygwin).

We don't support CoqIDE on Cygwin. Compiling CoqIDE with Cygwin libraries gives an unusable binary.

jfehrle · 2022-06-07T20:58:06Z

Updated.

@MSoegtropIMC, would you be willing to test this? I don't know of any other developer who has Windows available.

jfehrle · 2022-06-07T21:13:30Z

@andrew-appel Your description of the behavior in #13550 is somewhat different from what I found. Please let me know if my description doesn't match the behavior you see.

If it doesn't match, what version of Windows do you use? Did you see the issue with the 32-bit binaries and/or 64-bit binaries? I'm using Windows 10 with 64-bit binaries.

ide/coqide/coq.ml

ppedrot · 2022-06-08T05:38:25Z

ide/coqide/shared_WIN32.c.in

@@ -0,0 +1,16 @@
+#define _WIN32_WINNT 0x0501  /* Cf below, we restrict to  */
+
+#include <caml/mlvalues.h>


We already have a C stub file per OS, is there a solid reason to add a new one? I think it's not very good practice from the OCaml world to have a lot of C stubs lying around (especially given that they're preprocessed).

I didn't want to add the second one. win32_cvtpid is used both in CoqIDE and in coqidetop. In the dune file, coqide_WIN32.ml.in is part of library coqide_gui. When I included win32_cvtpid in coqide_WIN32.c.in and included the library in the idetop executable as @rgrinberg suggested, I got very strange behavior in CoqIDE (delay of a second or so for each character entered). I'm guessing that all the files in the library were not merely linked, but in fact loaded. So their let () = ... expressions were executed rather than just the ones that were referenced, e.g. as in coqide_main.ml, which is bad.

If there's a way to link specific modules without loading everything in the library, I'm all for it. I didn't understand Rudi's suggestion here well enough to try it.

I figured out a way to avoid the need for shared_WIN32.c.in and its friends. Now there's os_specific.ml which has the references to C code (usable in both coqide and coqidetop) and gui_specific.ml, containing items that depend on GTK and the GUI. Tedious to sort these out. If you're OK with this, I'll squash before the merge.

I spoke too soon. It appears that Glib.Io.channel_of_descr_socket in GTK is Windows-only. Whatever library contains that can't be linked into coqtopide, while win32_cvtpid must be linked into both coqide and coqtopide. It appears they need to be two separate libraries. Let's go with the first commit. I'll remove the second one momentarily.

Alizter · 2022-09-05T09:24:15Z

While I've tested this a lot, it would be nice to get someone with a fresh perspective to try it on Windows in case I missed something.

This is something I believe most of the dev team is lacking unfortunately.

I've had a visual look through your changes and they seem sound to me. If you have been able to get interrupt working on Windows again, then I trust it has been done properly.

@MSoegtropIMC How do you test the Windows installations for Coq platform, especially CoqIDE. Would you be able to lend a hand testing this?

MSoegtropIMC · 2022-09-05T10:51:59Z

@Alizter : I download the installer from CI, install it to some test folder and go through some test files from the smoke test kit in CoqIDE. I don't do fancy testing of CoqIDE - I would consider this to be part of Coq testing (not Coq Platform). In Coq Platform testing I concentrate on correct installation.

I am fairly busy with Coq Platform (and other things), but if there is no one else with a Windows machine, I could give it a try.

Alizter · 2022-09-05T12:16:24Z

Thanks @MSoegtropIMC, whenever you have some spare time, if you could give this PR a test that would be most welcome.

jfehrle · 2022-09-05T19:08:56Z

if there is no one else with a Windows machine, I could give it a try.

Hmm, if a lack of hardware is the main problem for potential testers, that seems like a readily solvable problem. I suppose it's also possible to install Windows in a virtual machine, but that may require more work to set up/maintain. There's also a question of how often we need to test on Windows (and perhaps whether the other Coq IDEs have much need to test on Windows). I hope to make more improvements to CoqIDE fairly soon, though most of them shouldn't have OS-specific code (as does this one).

I think the harder part may be finding someone willing to test things from time to time.

MSoegtropIMC · 2022-09-06T07:09:20Z

For installation in a VM you need a WIndows license and 16GB RAM.

Since I switched to Mac (and VSCoq for that matter - except when I need your Ltac debugger, which is frequent wnough) I am only doing essential testing for CoqIDE on Windows - which is not sufficient to guarantee the quality we want.

I will ask the Windows users I know if they can take some responsibility in testing Coq / CoqIDE / Coq Platform on Windows.

jfehrle · 2022-10-06T15:55:10Z

Let's not delay this any more waiting for a tester. While it would be good to have a second tester for Windows specific changes, the relevant functionality is almost completely broken on Windows, so there is little risk it will be worse than before. I have no specific reason to expect this PR may not work for others.

@ppedrot If you have no further review comments, would you merge? Thanks.

MSoegtropIMC · 2022-10-07T07:48:12Z

How about I take the patch into the 2022.09 beta release (I likely build the installers today and they should be signed on Monday)? There is anyway already a patch in for CoqIDE for the Mac preferences dialog crash.

MSoegtropIMC · 2022-10-07T07:49:56Z

And I will send a reminder to the Windows users I had in mind ...

MSoegtropIMC · 2022-10-07T12:45:33Z

I added this as opam level patch to the Coq Platform beta.

…16142

jfehrle · 2022-10-07T15:38:49Z

@MSoegtropIMC Sounds good, thanks.

jfehrle · 2022-10-07T16:40:42Z

Is this correct? The patch copied the code from the PR rather than depending on it, so if I change the code here, it won't affect the platform?

MSoegtropIMC · 2022-10-07T17:02:33Z

@jfehrle : yes, a Coq Platform release is carved in stone. Since you asked this to be merged I guessed that this is appropriate.

jfehrle · 2022-10-07T17:05:59Z

Great! I was thinking about when you did the debugger preview and my subsequent tweaking of the PR meant you had to update the platform a bit, too.

MSoegtropIMC · 2022-10-07T17:49:08Z

This was a dev pick - the coqide package in it linked to a branch.

Zimmi48 · 2022-10-10T10:44:55Z

@MSoegtropIMC I'm surprised to discover that this patch is included in the upcoming 8.16 beta Platform release. If that's the case, doesn't it mean that the patch should eventually be in 8.16.1 instead of 8.17? (cc @ppedrot)

ppedrot · 2022-10-10T11:05:41Z

We can indeed backport this, it looks like an important bugfix.

ppedrot

Seems a bit contrived to me, but if it works...

ppedrot · 2022-10-13T13:18:03Z

@coqbot merge now

ejgallego · 2022-10-14T14:38:23Z

ide/coqide/dune

 (foreign_stubs
  (language c)
  (names coqide_os_stubs))
- (libraries coqide-server.protocol coqide-server.core lablgtk3-sourceview3))
+ (optional)


I think this optional wasn't meant to be added back

Not the first time I see some old stuff being added back. Be careful with how you resolve merge conflicts @jfehrle 😉

See #16672.

I am careful, but also fallible.

We could avoid some rebasing and resulting merge errors by reducing the long wait between writing the code and its merge (about 4 months for this fairly small PR). That's long enough to forget many details. It took me a couple hours over two days to remember how to build and retest the code on Windows. (The weirdest detail being that I can't push from the cygwin/Windows command line because I couldn't figure out how to set up the security token in Windows--as it was last time. I can only push from the WSL command line.)

jfehrle added kind: fix This fixes a bug or incorrect documentation. part: CoqIDE Issues and PRs related to CoqIDE or other IDE features of coq. labels Jun 6, 2022

jfehrle added this to the 8.17+rc1 milestone Jun 6, 2022

jfehrle requested review from a team as code owners June 6, 2022 00:26

jfehrle force-pushed the fix_win_interrupt2 branch 2 times, most recently from 86d2b93 to 011fbdf Compare June 6, 2022 01:31

jfehrle force-pushed the fix_win_interrupt2 branch from 011fbdf to a2b5c42 Compare June 6, 2022 02:46

Alizter reviewed Jun 7, 2022

View reviewed changes

jfehrle force-pushed the fix_win_interrupt2 branch from a2b5c42 to d60e0da Compare June 7, 2022 20:51

ppedrot reviewed Jun 8, 2022

View reviewed changes

jfehrle force-pushed the fix_win_interrupt2 branch 2 times, most recently from 4fa8ec1 to 45ecf17 Compare June 10, 2022 20:55

SkySkimmer requested a review from a team August 30, 2022 11:44

github-actions bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Sep 20, 2022

Fix interrupt on Windows

5b06aa0

jfehrle force-pushed the fix_win_interrupt2 branch from 45ecf17 to 5b06aa0 Compare October 6, 2022 05:53

coqbot-app bot removed the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Oct 6, 2022

MSoegtropIMC added a commit to MSoegtropIMC/platform that referenced this pull request Oct 7, 2022

Pick 8.16~2022.09~beta1: included CoqIDE patch from rocq-prover/rocq#…

74f1aa9

…16142

Alizter requested a review from ppedrot October 7, 2022 17:03

ppedrot self-assigned this Oct 10, 2022

ppedrot modified the milestones: 8.17+rc1, 8.16.1 Oct 10, 2022

ppedrot approved these changes Oct 13, 2022

View reviewed changes

coqbot-app bot merged commit 18145d8 into rocq-prover:master Oct 13, 2022

ppedrot added a commit to ppedrot/coq that referenced this pull request Oct 14, 2022

Backport PR rocq-prover#16142: Fix "Interrupt computations" on Windows

825e175

ejgallego reviewed Oct 14, 2022

View reviewed changes

jfehrle mentioned this pull request Oct 14, 2022

Remove unwanted "(optional)" #16672

Merged

andrew-appel mentioned this pull request Oct 16, 2022

CoqIDE interrupt doesn't work on Windows #13550

Open

ppedrot added a commit to ppedrot/coq that referenced this pull request Oct 21, 2022

Backport PR rocq-prover#16142: Fix "Interrupt computations" on Windows

8542800

ppedrot added a commit to ppedrot/coq that referenced this pull request Oct 26, 2022

Backport PR rocq-prover#16142: Fix "Interrupt computations" on Windows

b2f0abc

jfehrle mentioned this pull request Nov 16, 2022

Document windows-specific limitation of Interrupt in CoqIDE #16824

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Fix "Interrupt computations" on Windows #16142

Fix "Interrupt computations" on Windows #16142

jfehrle commented Jun 6, 2022 •

edited

Loading

jfehrle commented Jun 6, 2022 •

edited

Loading

Alizter Jun 7, 2022

jfehrle Jun 7, 2022 •

edited

Loading

jfehrle commented Jun 7, 2022

jfehrle commented Jun 7, 2022 •

edited

Loading

ppedrot Jun 8, 2022

jfehrle Jun 8, 2022 •

edited

Loading

jfehrle Jun 10, 2022

jfehrle Jun 10, 2022 •

edited

Loading

Alizter commented Sep 5, 2022

MSoegtropIMC commented Sep 5, 2022

Alizter commented Sep 5, 2022

jfehrle commented Sep 5, 2022

MSoegtropIMC commented Sep 6, 2022

jfehrle commented Oct 6, 2022

MSoegtropIMC commented Oct 7, 2022

MSoegtropIMC commented Oct 7, 2022

MSoegtropIMC commented Oct 7, 2022

jfehrle commented Oct 7, 2022

jfehrle commented Oct 7, 2022

MSoegtropIMC commented Oct 7, 2022

jfehrle commented Oct 7, 2022

MSoegtropIMC commented Oct 7, 2022

Zimmi48 commented Oct 10, 2022

ppedrot commented Oct 10, 2022

ppedrot left a comment

ppedrot commented Oct 13, 2022

ejgallego Oct 14, 2022

Zimmi48 Oct 14, 2022

jfehrle Oct 14, 2022

		@@ -0,0 +1,16 @@
		#define _WIN32_WINNT 0x0501 /* Cf below, we restrict to */

		#include <caml/mlvalues.h>

Fix "Interrupt computations" on Windows #16142

Fix "Interrupt computations" on Windows #16142

Conversation

jfehrle commented Jun 6, 2022 • edited Loading

jfehrle commented Jun 6, 2022 • edited Loading

Alizter Jun 7, 2022

Choose a reason for hiding this comment

jfehrle Jun 7, 2022 • edited Loading

Choose a reason for hiding this comment

jfehrle commented Jun 7, 2022

jfehrle commented Jun 7, 2022 • edited Loading

ppedrot Jun 8, 2022

Choose a reason for hiding this comment

jfehrle Jun 8, 2022 • edited Loading

Choose a reason for hiding this comment

jfehrle Jun 10, 2022

Choose a reason for hiding this comment

jfehrle Jun 10, 2022 • edited Loading

Choose a reason for hiding this comment

Alizter commented Sep 5, 2022

MSoegtropIMC commented Sep 5, 2022

Alizter commented Sep 5, 2022

jfehrle commented Sep 5, 2022

MSoegtropIMC commented Sep 6, 2022

jfehrle commented Oct 6, 2022

MSoegtropIMC commented Oct 7, 2022

MSoegtropIMC commented Oct 7, 2022

MSoegtropIMC commented Oct 7, 2022

jfehrle commented Oct 7, 2022

jfehrle commented Oct 7, 2022

MSoegtropIMC commented Oct 7, 2022

jfehrle commented Oct 7, 2022

MSoegtropIMC commented Oct 7, 2022

Zimmi48 commented Oct 10, 2022

ppedrot commented Oct 10, 2022

ppedrot left a comment

Choose a reason for hiding this comment

ppedrot commented Oct 13, 2022

ejgallego Oct 14, 2022

Choose a reason for hiding this comment

Zimmi48 Oct 14, 2022

Choose a reason for hiding this comment

jfehrle Oct 14, 2022

Choose a reason for hiding this comment

jfehrle commented Jun 6, 2022 •

edited

Loading

jfehrle commented Jun 6, 2022 •

edited

Loading

jfehrle Jun 7, 2022 •

edited

Loading

jfehrle commented Jun 7, 2022 •

edited

Loading

jfehrle Jun 8, 2022 •

edited

Loading

jfehrle Jun 10, 2022 •

edited

Loading