Stream: Coq Platform devs & users

Topic: Coq not available after installation


view this post on Zulip Jan Menz (Aug 23 2022 at 11:02):

Today I installed the coq platform on a new computer with Windows 11 using Coq-Platform-release-2022.04.1-version_8.15_2022.04-arch-x86_64_signed.exe. The installation seemd to work but I cannot access Coq in the usual ways. When I type coqc or coqtop in the command line interface it tells me the command is either misspelled or could not be found. When I try to compile a file using proof general emacs tells me

Searching for program: No such file or directory, coqtop

When I try to open a coq file using CoqIDE CoqIDE opens but the file I want to open does not. Additionally I get a separate window with the following error message:

(coqide.exe:15256): GdkPixbuf-WARNING **: Cannot open pixbuf loader module file 'C:\Coq-Platform~8.15~2022.04\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-Platform~8.15~2022.04\lib\gdk-pixbuf-2.0\2.10.0\loaders.cache
to make things work again for the time being.

So far I tried reinstalling the coq platform and adding coqc and coqtop to the PATH manually. Neither worked. Does anyone have an idea how to solve this isse?

view this post on Zulip Michael Soegtrop (Aug 23 2022 at 12:36):

@Jan Menz : the error message does not hurt - CoqIDE does not load JPEG files or the like, so it doesn't need the pixbuf loaders and so far I didn't bother to fix this.

CoqIDE should work without setting path out of the box, but if you want to use coqc or coqtop from the command line, you need to add it to the PATH manually.

What do you mean with the file you want to open does not open. Do you say that nothing happens of you use file open menu?

Please note that in CoqIDE you can't open or edit files whose name is not a valid Coq module name, e.g. contains hyphens or the like. The file name (without the .v) must be a valid identifier name.

view this post on Zulip Jan Menz (Aug 23 2022 at 12:57):

@Michael Soegtrop, thanks for the quick reply.

@Jan Menz : the error message does not hurt - CoqIDE does not load JPEG files or the like, so it doesn't need the pixbuf loaders and so far I didn't bother to fix this.

That is good to know.

What do you mean with the file you want to open does not open. Do you say that nothing happens of you use file open menu? Please note that in CoqIDE you can't open or edit files whose name is not a valid Coq module name, e.g. contains hyphens or the like. The file name (without the .v) must be a valid identifier name.

Yes, nothing happens. While I see no reason for the file not to work (it is called stdpppp.v) I just tried a different file and it works in CoqIDE. So the particular CoqIDE problem seems to be file specific. Let's ignore this problem for now. I usually don't use CoqIDE anyway and was just trying to use it because everything else did not work.
This still leaves me with the main problem.

CoqIDE should work without setting path out of the box, but if you want to use coqc or coqtop from the command line, you need to add it to the PATH manually.

Even after adding it to the path I cannot access coqc or coqtop from the command line and proof general does not seem to be able to find coqtop either. This is independent of which file I try to use.
Am I perhaps adding the wrong thing to the path? I added the path to the coqc.exe and coqtop.exe files (e.g. "C:\Coq-Platform~8.15~2022.04\bin\coqc.exe"). Is that correct?

view this post on Zulip Michael Soegtrop (Aug 23 2022 at 15:48):

@Jan Menz : depending in where you installed it, the path looks reasonable.

Are you sure you did set the PATH in a proper way? For using coqc in CMD it is sufficient to just set PATH. It doesn't make a lot of sense that WIndows doesn't find coqc when it is there and in PATH - it is likely that you are doing something wrong with setting the PATH.

If you want applications started e.g. from the start menu to see coqc, you need to set PATH in the system settings.

Try to download the smoke test kit from https://github.com/coq/platform/releases/tag/2022.04.1 and run the batch file. If your PATH is setup properly, this works.

view this post on Zulip Jan Menz (Aug 23 2022 at 16:00):

Are you sure you did set the PATH in a proper way? For using coqc in CMD it is sufficient to just set PATH. It doesn't make a lot of sense that WIndows doesn't find coqc when it is there and in PATH - it is likely that you are doing something wrong with setting the PATH.

Yes, it turned out that was the problem. I checked again and compared what I entered with other things in the PATH and it turned out the coq.exe should not have been included in the path. Thanks a lot for the help. Now proof general also works.

view this post on Zulip Michael Soegtrop (Aug 23 2022 at 17:27):

There have been some requests that the installer should set the PATh automatically, but I was against it because Coq is usually reinstalled every 6 months (new versions) and removing things from PATH can be messy. Also people might have different Coq versions installed in parallel (say specialized installers for certain lectures). Then setting up the 2nd lecture would destroy the setup of the first if the installer would set PATH.

But I guess what would help is if I would show instructions on how to set PATH properly in the installer (say a copy & paste command). Please feel free to create a ticket for this.

view this post on Zulip Michael Soegtrop (Aug 23 2022 at 17:28):

@Jan Menz : can you please point me to the file stdpppp.v which does not load in CoqIDE? I would like to double check this.

view this post on Zulip Jan Menz (Aug 23 2022 at 21:17):

Yes, instructions what to add to the PATH and perhaps more importantly the information that adding Coq to the PATH is necessary for proof general and the use in the command line would be very helpful. Ideally, it would both be part of the installation instructions on the website and in the installer itself. One compromise between making the installer do it automatically and having to do it manually might also be to have a checkbox in the installer allowing the user to choose if they want it added together with explanations of the pros and cons.

@Jan Menz : can you please point me to the file stdpppp.v which does not load in CoqIDE? I would like to double check this.

I found out in the meantime that this does not seem to be a problem with the file itself. When I copy it to a different location it can be opened normally.
When I try to open it a briefly get an error message in the bottom left corner of CoqIDE that I did not see the first time (the big other error was much more noticable). It says

Load failed: CoqProject_file.Parsing_Error("Unkown Option -install")

So I assume it is a problem with the CoqProject file in the same folder.

view this post on Zulip Michael Soegtrop (Aug 29 2022 at 13:01):

@Jan Menz : I guess it is more an issue that you installed the file in a folder containing a space or the like. Maybe some improvements can be done here.


Last updated: Jan 30 2023 at 11:03 UTC