Lasse Blaauwbroek (Feb 04 2021 at 16:53): Lasse Blaauwbroek (Feb 04 2021 at 16:53):I have installed Coq platform through the binary installer on Windows, and everything works fine. However, if I build Coq platform myself and generate an installer, I'm having some problems with CoqIDE. Everything works fine including proving things, until one tries to open a file with Ctrl+O. Then the ide freezes for a few seconds and then crashes. I've been unable to retrieve any logs anywhere. For the generation of the installer, I'm following the instructions of the readme, choosing the 'Coq+CoqIDE only' installation option. Does anyone know what could cause this?
Guillaume Melquiond (Feb 04 2021 at 17:00):I am pretty sure I have already heard about this issue. So, there might be some open report about it with some information.
Lasse Blaauwbroek (Feb 04 2021 at 17:04):Ah that is good to know. I have not found a relevant issue on Coq platform's repo though. My guess is that some system library of GTK is missing, but I have little knowledge of Windows and GTK.
Enrico Tassi (Feb 04 2021 at 17:09):The issue would be in Coq's tracker
Enrico Tassi (Feb 04 2021 at 17:10):Are you testing v8.13 or master?
Lasse Blaauwbroek (Feb 04 2021 at 17:11):I'm on 8.12.2 at the moment
Lasse Blaauwbroek (Feb 04 2021 at 17:11):Is there reason to believe 8.13 will be better?
Enrico Tassi (Feb 04 2021 at 17:12):No, I just don't know how the binary installers for 8.12 were generated
Enrico Tassi (Feb 04 2021 at 17:12):The ones from 8.13 are generated by the platform CI
Enrico Tassi (Feb 04 2021 at 17:14):Are you downloading them from Coq's releases, of from the CI of the platform.
Lasse Blaauwbroek (Feb 04 2021 at 17:14):Ah, okay. The release notes of 8.12.2 do mention coq platform, although there is no explicit mention that the binaries are generated from coq platform
Lasse Blaauwbroek (Feb 04 2021 at 17:15):I'm using the one from Coq's releases.
Lasse Blaauwbroek (Feb 04 2021 at 17:18):Curiously, if I run coqide on the commandline of Cygwin, everything works correctly.
Enrico Tassi (Feb 04 2021 at 17:25):Are you saying that the same binary works if started from a cygwin shell but not if "double clicked" on?
Lasse Blaauwbroek (Feb 04 2021 at 17:27):It works from the Cygwin shell (in which case the binary is the one in the opam switch), but not whatever gets packaged into the installer and then installed into C:\Coq\bin\coqide.exe.
Enrico Tassi (Feb 04 2021 at 17:28):Ah ok, maybe it's the icons business. CC @Michael Soegtrop
Enrico Tassi (Feb 04 2021 at 17:30):Can you type C:\Coq\bin\coqide.exe from cmd.exe so that we see if it spits an error message when it crashes?
Lasse Blaauwbroek (Feb 04 2021 at 17:33):Yes I tried that, noting gets outputted. Tried it both in powershell and command prompt. The only thing I can find is a coqide.exe.dmp file that gets generated in <user>/AppData/Local/CrashDumps. But I have no idea how to view these files, they are binary.
Enrico Tassi (Feb 04 2021 at 17:34):and there is no "stderr.txt" or similar (it used to write that at some point)
Lasse Blaauwbroek (Feb 04 2021 at 17:36):Not that I can find. I tried redirecting the output to a file using > test.txt but it is empty.
Enrico Tassi (Feb 04 2021 at 17:37):hum, maybe you could try to use strace (from cygwin) to run the broken coqide and see if there is something interesting in the log http://www.cygwin.com/cygwin-ug-net/strace.html
Lasse Blaauwbroek (Feb 04 2021 at 17:40):Ah I didn't know I could run binaries outside of Cygwin inside of it. That does indeed work. I'm running strace now, but it is really slow.
Lasse Blaauwbroek (Feb 04 2021 at 17:43):After loading the several plugins like ground_plugin.cmxs, Coqide is loaded. Then I press Ctrl+O, and 4 threads are created, and C:\Window\System32\WindowsCodecs.dll is loaded. Now about 15 threads are slowly exiting with statuscode 0x0 (taking multiple minutes)
Lasse Blaauwbroek (Feb 04 2021 at 17:58):The end of the trace that error out looks like this (it has still not crashed it is just hanging):
--- Process 1248 loaded C:\Windows\System32\cryptbase.dll at 00007ffd879a0000
--- Process 7488 loaded C:\Coq\lib\coq\plugins\ltac\ltac_plugin.cmxs at 00000000652c0000
--- Process 7488 loaded C:\Coq\lib\coq\plugins\syntax\string_notation_plugin.cmxs at 000000006eec0000
--- Process 7488 loaded C:\Coq\lib\coq\plugins\ltac\tauto_plugin.cmxs at 0000000068500000
--- Process 7488 loaded C:\Coq\lib\coq\plugins\cc\cc_plugin.cmxs at 0000000068d80000
--- Process 7488 loaded C:\Coq\lib\coq\plugins\firstorder\ground_plugin.cmxs at 0000000067ac0000
--- Process 7488 loaded C:\Coq\lib\coq\plugins\syntax\numeral_notation_plugin.cmxs at 00000000642c0000
----------------- Me pressing Ctrl+O -----------------------------
--- Process 1248 thread 11736 created
--- Process 1248 thread 8800 created
--- Process 1248 thread 11620 created
--- Process 1248 loaded C:\Windows\System32\WindowsCodecs.dll at 00007ffd837a0000
--- Process 1248 thread 11296 created
--- Process 1248 thread 8800 exited with status 0x0
--- Process 1248 thread 11296 exited with status 0x0
--- Process 1248 thread 11620 exited with status 0x0
--- Process 12844 thread 1988 exited with status 0x0
--- Process 12844 thread 10380 exited with status 0x0
--- Process 12844 thread 6564 exited with status 0x0
--- Process 7488 thread 6460 exited with status 0x0
--- Process 7488 thread 11164 exited with status 0x0
--- Process 7488 thread 8440 exited with status 0x0
--- Process 1248 thread 12596 exited with status 0x0
--- Process 1248 thread 3324 exited with status 0x0
--- Process 1248 thread 4384 exited with status 0x0
--- Process 1248 thread 13132 exited with status 0x0
--- Process 1248 thread 13156 exited with status 0x0
--- Process 1248 thread 5176 created
--- Process 1248 thread 6192 created
--- Process 12844 thread 4516 created
--- Process 1248 thread 5176 exited with status 0x0
--- Process 1248 thread 6192 exited with status 0x0
--- Process 12844 thread 4516 exited with status 0x0
--- Process 1248 thread 5164 created
--- Process 1248 thread 6980 created
--- Process 12844 thread 1256 created
--- Process 1248 thread 6980 exited with status 0x0
--- Process 12844 thread 1256 exited with status 0x0
--- Process 1248 thread 5164 exited with status 0x0
I see no i/o syscall. I don't know that strace, maybe you have to thinker with the options...
Théo Zimmermann (Feb 04 2021 at 18:02):I confirm that the 8.12.2 Windows binaries were generated (by Michael) with the platform scripts.
Enrico Tassi (Feb 04 2021 at 18:02):or wait for Michael to show up, he surely know better.
Enrico Tassi (Feb 04 2021 at 18:02):Is there any difference in the files shipped by these installer and the ones you are getting in C:\Coq\ ?
Lasse Blaauwbroek (Feb 04 2021 at 18:06):I tried enabling all settings I could find, but it does not seem to make a difference. Unless someone knows something else to try, let's wait for Michael. In case anyone knows how to read these things, attached is a CrashDump file. coqide.exe.2844.dmp
Michael Soegtrop (Feb 04 2021 at 18:15):I guess you are missing the compiled GTK resource files.
You should build an installer using the Coq platform scripts - they can build an installer from an opam switch.
Michael Soegtrop (Feb 04 2021 at 18:16):Essentially you are missing what this opam file does in Coq Platform:
(https://github.com/coq/platform/tree/v8.13/opam/packages/dep-glib-compiled-schemas/dep-glib-compiled-schemas.1.0)
Lasse Blaauwbroek (Feb 04 2021 at 18:17):That is exactly what I've done, but it doesn't work. That is, the executable in opam does work, but when I create an installer and install into C:\Coq, it is having problems.
Michael Soegtrop (Feb 04 2021 at 18:17):Well then the installer is missing these files.
How do you create the installer?
Lasse Blaauwbroek (Feb 04 2021 at 18:18):Note that CoqIDE does run, it only crashes when trying to open a file through the file explorer
Michael Soegtrop (Feb 04 2021 at 18:18):Yes - it crashes as soon as it needs a GTK default dialog box.
Michael Soegtrop (Feb 04 2021 at 18:18):This is what is in the "compiled schemas" file.
Lasse Blaauwbroek (Feb 04 2021 at 18:19):I just ran windows/create_installer_windoows.sh
Lasse Blaauwbroek (Feb 04 2021 at 18:19):Note that I did not do a full install, but only the Coq+CoqIDE option. Could that option be missing something?
Michael Soegtrop (Feb 04 2021 at 18:19):This puts the file in cygwin.
When you create an installer it needs to be copied to the install destination folder.
Michael Soegtrop (Feb 04 2021 at 18:19):As I said, the Coq Platform installer creation scripts should tale care of this.
Michael Soegtrop (Feb 04 2021 at 18:20):Could that option be missing something?
Possibly. The installer creator has dependency management.
Lasse Blaauwbroek (Feb 04 2021 at 18:21):Maybe I'm misunderstanding, but the Windows Readme says that I should run windows/create_installer_windows.sh to create an installer. I'm following the readme literally.
Michael Soegtrop (Feb 04 2021 at 18:21):But I darkly remember that because this is a hack opam file which creates files outside of .opam, opam doesn't know about the dependency, so the dependencies are explicitly hacked into the auto generated file lists.
Michael Soegtrop (Feb 04 2021 at 18:22):This happens here:
(https://github.com/coq/platform/blob/v8.13/windows/create_installer_windows.sh#L378)
Michael Soegtrop (Feb 04 2021 at 18:23):OK, then it is a bug. It should work.
Michael Soegtrop (Feb 04 2021 at 18:23):Points to check are:
files_dep-glib-compiled-schemas Michael Soegtrop (Feb 04 2021 at 18:25):dependencies_hidden.nshcontain a dependency chain between CoqIDE and the dep-glib-compiled-schemas package Lasse Blaauwbroek (Feb 04 2021 at 18:25):Where should I be looking for those files?
Michael Soegtrop (Feb 04 2021 at 18:26):So what you are doing is:
Michael Soegtrop (Feb 04 2021 at 18:27):After you did run the installer creation script, you should have a folder windows_installer. They are in there.
Lasse Blaauwbroek (Feb 04 2021 at 18:30):Sorry, I'm a bit slow, having to transfer files via USB to my Linux machine
$ cat dependencies_hidden.nsh | grep glib
${CheckHiddenSectionDependency} ${Sec_conf_gtksourceview3} ${Sec_dep_glib_compiled_schemas} 'conf_gtksourceview3' 'dep_glib_compiled_schemas'
${CheckHiddenSectionDependency} ${Sec_dep_glib_compiled_schemas} ${Sec_conf_gtk3} 'dep_glib_compiled_schemas' 'conf_gtk3'
$ cat files_dep-glib-compiled-schemas.nsh
# File list for dep-glib-compiled-schemas matching . excluding (\.byte\.exe|\.cm[aiox]|\.cmxa|\.o)$
That looks like it could be a problem
Michael Soegtrop (Feb 04 2021 at 18:32):Yes, this is what is in opam, e.g. dep-glib-compiled-schemas depends on conf-gtk3
Lasse Blaauwbroek (Feb 04 2021 at 18:32):This is coming from coq-platform/windows-installer
Michael Soegtrop (Feb 04 2021 at 18:33):Yes, the file should be in there.
Also you need to check if the dependency file has a path from Sec_dep_glib_compiled_schemas to CoqIDE
Michael Soegtrop (Feb 04 2021 at 18:33):So the question is why the command add_single_file "/usr/${COQ_ARCH}-w64-mingw32/sys-root/mingw/" "share/glib-2.0/schemas/gschemas.compiled" "files_dep-glib-compiled-schemas" is no trun.
Lasse Blaauwbroek (Feb 04 2021 at 18:34):I did have an overlapping problem in a previous install, documented here: https://github.com/coq/platform/issues/66
Michael Soegtrop (Feb 04 2021 at 18:34):The windows installer creator gets the package dependecy information from opam.
Lasse Blaauwbroek (Feb 04 2021 at 18:35):But after that I installed cygwin completely from scratch and I didn't seem to have that problem anymore
Michael Soegtrop (Feb 04 2021 at 18:37):You mean the cygwin you used to git clone the Coq Platform repo? Possibly you had changed the default settings.
Michael Soegtrop (Feb 04 2021 at 18:37):If you use GIT for Windows to clone, it might not work - it is better to use the zip then.
Michael Soegtrop (Feb 04 2021 at 18:37):But pack to the topic:
Michael Soegtrop (Feb 04 2021 at 18:38):Can you debug why the line
add_single_file "/usr/${COQ_ARCH}-w64-mingw32/sys-root/mingw/" "share/glib-2.0/schemas/gschemas.compiled" "files_dep-glib-compiled-schemas"
in the script is not run? It is top level and it should add the missing file to the dependency file.
Lasse Blaauwbroek (Feb 04 2021 at 18:38):I think I found why the line was not run. It does not seem to be in there. Note that I'm using the 8.12 branch
Michael Soegtrop (Feb 04 2021 at 18:39):Ah OK, that explains it. This is not updated recently. If you need it, I can update it.
Lasse Blaauwbroek (Feb 04 2021 at 18:39):That would be great
Michael Soegtrop (Feb 04 2021 at 18:39):There should be quite a few more fixes.
Lasse Blaauwbroek (Feb 04 2021 at 18:40):Were doing some tests with Tactician with students, so I need a windows installer
Michael Soegtrop (Feb 04 2021 at 18:40):But essentially I think you can use the 8.13 branch and just exchange the package list and switch name file.
Lasse Blaauwbroek (Feb 04 2021 at 18:41):Ah, okay, I'll do that then. I can downgrade the Coq version in Opam from 8.13 to 8.12 without problems?
Michael Soegtrop (Feb 04 2021 at 18:42):I mean get a Copy of the 8.13 branch and then replace the package list and switch name files with the ones from the 8.12 branch.
Michael Soegtrop (Feb 04 2021 at 18:42):That is: coq_platform_packages.sh and coq_platform_switch_name.sh.
Lasse Blaauwbroek (Feb 04 2021 at 18:43):Ah, oke I'll give that a try
Michael Soegtrop (Feb 04 2021 at 18:43):You might have to merge the packages file - the logic for selecting packages changed, but it should be easy to merge.
Lasse Blaauwbroek (Feb 04 2021 at 18:43):Okay, I'll give it a try tomorrow. Thanks for your help, and the others :-)
Michael Soegtrop (Feb 04 2021 at 18:44):Anyway, I will update the 8.12 branch tomorrow.
Théo Zimmermann (Feb 04 2021 at 18:44):I'm thinking we would really gain by having only one branch with the scripts. It would avoid these problems. The concern you raised against this last time was that most of the code is actually the opam patch repo, but maybe it should be a separate repo then, to keep things tidy...
Michael Soegtrop (Feb 04 2021 at 18:44):You are welcome!
Michael Soegtrop (Feb 04 2021 at 18:44):Ah yes: Lasse: you also need to replace the opam patch repo with the one from the 8.12 branch.
Lasse Blaauwbroek (Feb 04 2021 at 18:45):Ah, oke, that all sounds complicated. If you are updating the 8.12 branch tomorrow anyway, then I'll just wait for that I think :-)
Michael Soegtrop (Feb 04 2021 at 18:45):@Theo: actually there has been little change recently. Master and 8.13 are identical regarding the scripts, but have some slight intended differences in the opam repo setup.
Michael Soegtrop (Feb 04 2021 at 18:46):@Lasse : yes this would be good if you could test it!
Lasse Blaauwbroek (Feb 04 2021 at 18:46):Sure, will do. Send me a message when it's ready
Michael Soegtrop (Feb 04 2021 at 18:47):I will.
Michael Soegtrop (Feb 04 2021 at 18:49):@Théo Zimmermann : for master and v8.13 I cherry pick the changes which is a bit of work, but not that much. About 1 hour in total last month. For 8.12 I would just copy the scripts from 8.13 and merge it as one commit. This is a few minutes of work. And this should become rarer, so I still don' think it is worthwhile to do something special, especially since the master branch is different.
Théo Zimmermann (Feb 04 2021 at 18:49):Sure, that's your call.
Michael Soegtrop (Feb 04 2021 at 18:51):Of cause one could factor out the master branch difference - the only difference is that it drags in the dev repo instead of the released repo.
Michael Soegtrop (Feb 04 2021 at 18:58):Théo Zimmermann said:
I confirm that the 8.12.2 Windows binaries were generated (by Michael) with the platform scripts.
I don't think this is the case. 8.12.2 should still have been generated with the legacy Windows installer scripts. This is easy to see. The new installer has a longer list of packages without hierarchy. The old installer had a bit of package hierarchy. Also the new installer uses the synopsis from opam as package name and generally has opam package names.
Théo Zimmermann (Feb 04 2021 at 19:12):The release note says:
New: a 64-bit Windows Coq platform installer is now available. A 32-bit Windows installer should eventually become available.
Given that I'm the one who wrote that, I'm pretty sure of what this means.
Michael Soegtrop (Feb 04 2021 at 20:01):I will double check. But then this installer does work?
Lasse Blaauwbroek (Feb 04 2021 at 20:02):For me the provided 8.12.2 installer works
Michael Soegtrop (Feb 05 2021 at 08:41):@Lasse : did you use a tag or v8.12 latest? Actually the installer build script in v8.12 latest is identical to v8.13 latest. But it lacks a few fixes for recent cygwin errors and also the script to generate a smoke test kit.
Lasse Blaauwbroek (Feb 05 2021 at 08:42):I cloned v8.12.2.0
Michael Soegtrop (Feb 05 2021 at 08:43):I see. Can you please try v8.12 latest?
Michael Soegtrop (Feb 05 2021 at 08:44):I will merge over the Cygwin fixes and the smoke test kit.
Michael Soegtrop (Feb 05 2021 at 08:44):But unless you run in the intermittent cygwin 64 bug, it should work fine as is.
Lasse Blaauwbroek (Feb 05 2021 at 08:46):Oke will do. You might want to update the README_Windows.md file on the v8.12 branch, because that instructs people to clone v8.12.2.0
Michael Soegtrop (Feb 05 2021 at 08:48):Yes, expect a new tag v8.12.2.1 some time soon. I was not aware that 8.12.2.0 had a sever issue on Windows (I am personally more Mac centric since a while ;-).
Lasse Blaauwbroek (Feb 05 2021 at 10:25):I can confirm that the v8.12 branch works properly. Hopefully, it also works properly after I've made my modifications to Opam :-)
Michael Soegtrop (Feb 05 2021 at 10:32):The installer packaging scripts are obviously only tested with the packages which are there, but they use opam in a very direct and generic way. The only thing which is known not to work are opam packages which write outside of .opam, but I think I am the only one creating such packages (to fix cygwin issues without yet another meta build system). Also the opam dependencies need to be correct. They are not always. Some opam packages simply assume that stuff is there.
Michael Soegtrop (Feb 05 2021 at 10:33):So you are creating a dedicated installer for some machine learning capable Coq?
Lasse Blaauwbroek (Feb 05 2021 at 10:33):I already tested it before, and it works (just modulo the CoqIDE problem). I was even able to upgrade OCaml to 4.08 without problems.
Lasse Blaauwbroek (Feb 05 2021 at 10:33):Indeed
Lasse Blaauwbroek (Feb 05 2021 at 10:34):The only problem I have is that my auxiliary executables that are generated by my package do not seem to be packaged. But I can work around that for now.
Michael Soegtrop (Feb 05 2021 at 13:31):The only problem I have is that my auxiliary executables that are generated by my package do not seem to be packaged. But I can work around that for now.
If you create an opam package for these files and they end up in the .opam switch folder and if you use opam to install these files, the installer scripts should automatically pick them up. But it is critical that the files end up under .opam (otherwise the opam package will anyway not work except on Windows where sandboxing is off).
If this does not work it is a bug and I will fix it. In case, please point me to the modified branch of Coq Platform.
Michael Soegtrop (Feb 06 2021 at 10:53):@Lasse : does the installer creation including your additional components work now? I wanted to make a release and would prefer if at least one custom installer project would work.
Lasse Blaauwbroek (Feb 06 2021 at 11:19):Yes it works indeed. Due to one of my packages doing some pathological things (overwriting the standard library), I had to modify one line of the installer: https://github.com/coq/platform/blob/ac5063122fb8a01d35fd9e2d77b8734e3a22d942/windows/create_installer_windows.sh#L252 I had to add sed 's/(modified since)//g' to the pipeline.
Michael Soegtrop (Feb 06 2021 at 13:26):I see. Did you think about putting the modified standard library somewhere else and somehow point Coq to it? Coq 8.13 has a new mechanism - a config file which it reads from the same path as the binary path which allows to set environment variables. One could then supply e.g. a batch file to switch between the two versions.
Lasse Blaauwbroek (Feb 06 2021 at 14:15):Installing a separate standard library is not a sustainable solution, because you cannot switch on the fly between stdlibs. All packages depend on the stdlib, and if you just perform a bait-n-switch, those packages will fail at runtime because the hashes of the files they depend on are wrong.
Long-term, the solution to this is to split the standard library from the main coq package. There are already two pull-requests to do this, but there seems to be a shortage of manpower to work on dune/opam related issues for Coq. Until the split is realized I think this is the best solution available.
Last updated: Oct 12 2024 at 12:01 UTC