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.
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.
(deleted)
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.
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.
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.
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.
@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.
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.
@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?
@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.
@Michael Soegtrop post it here, if it rings a bell I'll tell you
OK, I will flex my rusted WireShark muscles a bit ...
@Guillaume Melquiond : yes, I guess we should wait a few days. This should be easy to fix.
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
@Enrico Tassi : I was about to test them ... (on real Windows).
I get the same error on 64 bits, but of course it could be wine
It works for me (both of them).
great!
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.
@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).
@Michael Soegtrop The debugger documentation is in https://github.com/coq/coq/pull/14864.
Is there somewhere a compiled version online?
OK, after looking at the PNGs, I got it working, thanks!
Very cool :-)
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).
How do we set up a session?
I can do a session now or anytime today.
I send you a link via private Zulip message
I'm on the login screen for webex. Have you started the session?
./_build/install/default/bin/coqide.exe -coqlib "$(cygpath -aw .)"/_build/default
@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.
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)
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?
@Michael Soegtrop ?
@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.
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?
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: May 28 2023 at 13:30 UTC