platform
platform copied to clipboard
coq
"coqide -help" hangs when installed with the Coq platform, etc.
"coqide -help" hangs when installed with the Coq platform (1/22/22 version), whereas "coqide" by itself works. I suspect this is from incorrect handling of command line arguments when CoqIDE is installed--IIRC this option works in the development environment [which I can't try at the moment].
CoqIDE comes up with coqide -I _build_ci/rewriter/src/Rewriter/Util/plugins.
"coqide --version" doesn't hang, but doesn't give any output, either.
@ejgallego Any thoughts?
For comparison, "coqtop -help" shows the usual
$ coqtop -help
Usage: coqtop <options>
Coq options are:
-I dir look for ML files in dir
:
@jfehrle Are you talking about the Coq Platform Windows installer?
cc @MSoegtropIMC, should I transfer this issue to the Platform repo as well?
I've also observed similar issues. For example, in an environment where there is no GUI, coqide --help and coqide --version both fail. It seems that those commands should not touch the gtk machinery.
Using Ctrl-C and running coqide inside gdb may provide some more info on what's going on
I've also observed similar issues. For example, in an environment where there is no GUI,
coqide --helpandcoqide --versionboth fail. It seems that those commands should not touch the gtk machinery.
The latter is supposed to open a small window to display the version though.
@Zimmi48 updated the title in answer to your question. FWIW I've never tried to install a local build with dune.
@jfehrle My question was not local build or Coq Platform, it was Coq Platform Windows installer or Coq Platform scripts?
Scripts, I think. Can check this evening. It was -24 C here this morning (skiing Colorado this week).
[
coqide --version] is supposed to open a small window to display the version though.
Why does it do that instead of printing to stdout? If a shell script wants to check the version, it won't be able to get it from the window.
(Digressing: is there a way to print the installed version of the platform? Seems like that might be useful for reporting issues. Perhaps it could also report what options were chosen during installation.)
Why does it do that instead of printing to stdout? If a shell script wants to check the version, it won't be able to get it from the window.
Agreed this is not so nice, although in general the versions of coqide and coqtop are expected to be the same, so scripts can just use coqtop --version instead.
@Zimmi48 It has happened in the past that coqtop showed the version I was expecting, however due to a buggy install, coqide was pointing somewhere completely different. I will open a new issue about this since I think @jfehrle is correct.
I guess the main reason is that it is tricky to make a switch between console and windowed applications platform independent. As far as I remember the operating system's main function CoqIDE uses is defined in gtk-sourceview3 and implemented separately for every OS. So in order to support such a console / windowed switch one would have to reimplement these functions for all OSes or convince upstream gtk-sourceview to accept corresponding patches.
In my windows install of the Coq Platform 8.15 beta package pick, running coqide --help from the cygwin prompt, I get the following message. This seems consistent with the rest of this issue discussion.
$ coqide --help
(coqide.exe:8072): GdkPixbuf-WARNING **: Cannot open pixbuf loader module file '
C:\Coq\lib\gdk-pixbuf-2.0\2.10.0\loaders.cache': No such file or directory
This likely means that your installation is broken.
Try running the command
gdk-pixbuf-query-loaders > C:\Coq\lib\gdk-pixbuf-2.0\2.10.0\loaders.cache
to make things work again for the time being.
@andrew-appel : the pixbuf things has nothing to do with any issues CoqIDE might have. CoqIDE doesn't need fancy pixbuf loaders (say tiff, jpeg, ...) so it doesn't hurt that it can't load it. You will always get this error. I will see if I can fix it.