Michael Soegtrop (Sep 07 2021 at 19:16): Michael Soegtrop (Sep 07 2021 at 19:16):In preparation of a 8.14 Coq Platform release I did a 8.14 dev build of Coq and CoqIDE. It works fine on Mac, but on Windows I get a "coqtop died badly". The interesting thing is that coqidetop doesn't seem to die - it doesn't exit before CoqIDE closes the pipe. Are there some quick options to debug this?
@Jim Fehrle : FYI.
Jim Fehrle (Sep 07 2021 at 19:24):I looked at it for a while. The best idea at the moment is to do a bisection, which failed for me because I couldn't build the necessary versions. See https://github.com/coq/coq/issues/14800.
Paolo Giarrusso (Sep 07 2021 at 19:36):(deleted)
Paolo Giarrusso (Sep 07 2021 at 19:39):nevermind, the one I had in mind is not in; https://github.com/coq/coq/pulls?q=is%3Apr+sort%3Aupdated-desc+is%3Amerged+xml+milestone%3A8.14%2Brc1 doesn't have anything obvious.
Guillaume Melquiond (Sep 07 2021 at 20:16):Hmm... I was about to publish the release candidate, but I guess there is no point in doing so, if we already know Coq does not build correctly on Windows.
Jim Fehrle (Sep 07 2021 at 21:13):I tried to do a bisection again. While building with coq platform pointing to git+https://github.com/coq/coq#v8.13 works, if I point to the equivalent revision number git+https://github.com/coq/coq#34da65afbe8fec419498f113548a7a58638cf404, the Windows build script doesn't produce a coqide executable even though the script output says it recompiled coqide. (Running coqtop shows the revision number as expected.)
Perhaps it's just a build script issue related to using a revision number. @Michael Soegtrop let me know if you want to do a debug session. Keep in mind I'm 9 hours behind European time.
Jim Fehrle (Sep 08 2021 at 01:32):I tried some more experiments and I'm baffled by the behavior:
None of these generate a coqide executable though the script appears to build it.
I'm out of ideas here.
Michael Soegtrop (Sep 08 2021 at 07:42):@Jim Fehrle : if you build in a new cygwin and you have coqtop (as you say in point 4), it obviously can't be that it didn't build it. I hope it is clear that if you build into a new cygwin, you actually have to start that cygwin via the cygwin.bat in the root folder of that cygwin.
How do you actually change the Coq version? Copy the opam file to the local patch repo and modify the reference there?
One more note: Coq Platform and opam are not build systems like make or dune, they are package management systems more like apt-get. This means that dependencies are not resolved at a file level but at a package level. If you e.g. change an opam file and rerun the Coq Platforms scripts, nothing will happen - you have to update the repos, uninstall and reinstall the package.
Michael Soegtrop (Sep 08 2021 at 07:49):I would say the best way to do a bisection on Windows is to use the platform scripts to setup a fresh cygwin and build only Coq and CoqIDE via opam (extent = i) and then in that cygwin clone the Coq repo and do a build with dune there - the cygwin setup by the Coq Platform scripts has everything required for that once Coq and CoqIDE have been built via opam. To be sure that you don't get the wrong Coq and CoqIDE, it would make sense to uninstall the Coq and CoqIDE opam packages, but keep all the dependencies that these packages installed.
Michael Soegtrop (Sep 08 2021 at 07:51):@Enrico Tassi : since coqidetop does not actually die (as I wrote it lives until CoqIDE closes the pipe to it), would it help if I provide a transcript of the communication between coqidetop and CoqIDE?
Michael Soegtrop (Sep 08 2021 at 08:00):@Jim Fehrle : btw, the still in development "multi-version" branch meanwhile has a 8.14 variant (currently just Coq and CoqIDE). It should be fairly equivalent to a 2021.02 patched up to 8.14, but it has a few advantages:
See (https://github.com/MSoegtropIMC/platform/tree/2021.09)
I will keep on eye on this thread in the evening today in case you want to do an online debug session.
Enrico Tassi (Sep 08 2021 at 08:16):@Michael Soegtrop post it here, if it rings a bell I'll tell you
Michael Soegtrop (Sep 08 2021 at 08:21):OK, I will flex my rusted WireShark muscles a bit ...
Michael Soegtrop (Sep 08 2021 at 08:22):@Guillaume Melquiond : yes, I guess we should wait a few days. This should be easy to fix.
Enrico Tassi (Sep 08 2021 at 08:22):btw, the installers we have signed are broken as well, I imagine. I usually can run coqide with wine, but this time I get:
gares@ollypat:/tmp/Coq/bin$ wine coqide.exe
Gtk-Message: Failed to load module "gail:atk-bridge"
Fatal error: exception Gtk.Error("GtkMain.init: initialization failed\nml_gtk_init: initialization failed")
this was the 32 bit one, let me also try the 64
Michael Soegtrop (Sep 08 2021 at 08:23):@Enrico Tassi : I was about to test them ... (on real Windows).
Enrico Tassi (Sep 08 2021 at 08:24):I get the same error on 64 bits, but of course it could be wine
Michael Soegtrop (Sep 08 2021 at 08:36):It works for me (both of them).
Enrico Tassi (Sep 08 2021 at 08:37):great!
Michael Soegtrop (Sep 08 2021 at 08:38):Didn't you have the issues with wine before?
The only thing I see is that the start menu icon fix @Jason Gross did doesn't seem to work, but sometimes Windows needs 10 minutes to display icons correctly. Also some Adwaita icons are still missing.
Michael Soegtrop (Sep 08 2021 at 13:38):@Jim Fehrle : I did compile your branch on Mac (where CoqIDE) comes up, but I don't know how to get into the debugger. The only difference I see is that Coq doesn't throw an error any more on Set Ltac Debug. I tried:
Set Ltac Debug.
Ltac test1:=
idtac "A";
exact I.
Goal True.
test1.
Btw.: I added a choosable variant for your debugger branch to (https://github.com/MSoegtropIMC/platform/tree/2021.09).
Jim Fehrle (Sep 08 2021 at 15:27):@Michael Soegtrop The debugger documentation is in https://github.com/coq/coq/pull/14864.
Michael Soegtrop (Sep 08 2021 at 15:29):Is there somewhere a compiled version online?
Michael Soegtrop (Sep 08 2021 at 15:37):OK, after looking at the PNGs, I got it working, thanks!
Michael Soegtrop (Sep 08 2021 at 15:38):Very cool :-)
Michael Soegtrop (Sep 08 2021 at 15:39):If you want to do a remote session on bisecting CoqIDE, I am available from now the next 2 hours or after 9:30 PM German time (should be noon your time).
Jim Fehrle (Sep 08 2021 at 16:49):How do we set up a session?
Jim Fehrle (Sep 08 2021 at 16:50):I can do a session now or anytime today.
Michael Soegtrop (Sep 08 2021 at 16:52):I send you a link via private Zulip message
Jim Fehrle (Sep 08 2021 at 16:58):I'm on the login screen for webex. Have you started the session?
Jim Fehrle (Sep 08 2021 at 19:50):./_build/install/default/bin/coqide.exe -coqlib "$(cygpath -aw .)"/_build/default
Michael Soegtrop (Sep 09 2021 at 09:10):@Emilio Jesús Gallego Arias : I had a debugging session with Jim on this topic yesterday - there is a preliminary indication that it makes a difference if CoqIDE and coqidetop are built with dune or make - in one test building 8.13.2 with dune didn't work either, but it might also be an issue with an unclean build - the assumption was that during a git bisection one does not need to clean the build folder and that dune can figure out what to compile. The question is: are the 8.14 and dev opam packages already using dune or are they still based on classic make? The just call make but this does not necessarily say something.
Btw.: the dune shims for calling CoqIDE don't work in the Cygwin MinGW cross environment, because dune passes cygwin absolute paths to CoqIDE, which MinGW apps don't understand - one either has to use relative paths or absolute Windows paths. We used the command line @Jim Fehrle posted just above to call CoqIDE after building with dune.
This suggests that a possible root cause for the suspected dune issue are wrong paths (cygwin rather than MinGW) compiled into Coq apps.
Enrico Tassi (Sep 09 2021 at 09:43):just to rule out one of the possible axes, does passing -async-proofs off to CoqIDE change anything? (when they are on, coqide starts coqidetop which in turn starts a worker, the latter step is skipped if they are off)
Karl Palmskog (Sep 09 2021 at 11:05):here is what the build clause looks like for the package coqide.8.14.dev:
build: [
[
"./configure"
"-configdir" "%{lib}%/coq/config"
"-prefix" prefix
"-mandir" man
"-docdir" doc
"-libdir" "%{lib}%/coq"
"-datadir" "%{share}%/coq"
"-native-compiler" "yes" {coq-native:installed} "no" {!coq-native:installed}
]
[ "dune" "build" "-p" name "-j" jobs ]
]
I was confused about the statement that the things worked on master, but not on 8.14, is that still the case?
Emilio Jesús Gallego Arias (Sep 09 2021 at 15:38):@Michael Soegtrop ?
Michael Soegtrop (Sep 09 2021 at 16:14):@Emilio Jesús Gallego Arias : Not sure where this statement comes from. What I know (or strongly suspect) is that it doesn't work in 8.13.2 if compiled with dune, but it does work in 8.13.2 if compiled with traditional make. And Jim said that it stopped working with "default make" with the commit which switched to dune. According to my tests it does not work in 8.14 latest and not in master either.
Emilio Jesús Gallego Arias (Sep 09 2021 at 16:40):Ah OK, I misunderstood the original issue, I thought it was working on master but not on 8.14 ; so that is a path problem then?
Michael Soegtrop (Sep 09 2021 at 16:59):Either a path problem or what @Enrico Tassi mentioned in the GIT issue, that in dune system dependent files are not used - which probably boils down to path issues.
Last updated: Dec 07 2023 at 06:38 UTC