I compiled the Coq Platform from sources. How do I edit proofs?

Using Coq
1

So far I have always used the Windows installer for the Coq Platform. However, I am now in a situation where I need to update one of the provided packages to a newer version. As far as I could tell, this could not be done using the version from the Windows installer.

So I installed the Coq platform from sources for the first time using the provided script, so that I would have access to opam and could update my package.
After the installation I added the path to the coq binaries to the windows path as usual, but Emacs/Proof General do not work. When I try to start the Coq process I get told “Coq process exited!”. To test, I wanted to use the provided CoqIDE, but it crashes immediately when opening, saying that some .dlls are not found. Am I missing a step here?

2

I found some additional info. Emacs says that “Process coq exited abnormally with code 53”. Does anyone know what that means?

3

Does it say which DLLs are missing?

–
Ian

4

For coqide libcairo-2.dll and libfree-6.dll and libfontconfig-1.dll and libgdk-3-0.dll.

5

Hmm, those don’t seem like something a Windows system can be expected to have, without taking specific steps. If the build instructions say nothing specific about Windows, I’d try OPAM instead. OPAM has a “system dependencies” mechanism that may take care of this or at least make it obvious how to take care of it manually prior to the build.

–
Ian