Stream: Coq Platform devs & users

Topic: Failing compilation of VST in 8.12.1


view this post on Zulip Karl Palmskog (Nov 17 2020 at 07:12):

@Michael Soegtrop I just installed 8.12.1 and tried to reinstall coq-vst.2.6. However, I get the following error:

FAILURE: You need Coq 8.11.0 or-else 8.11.1 or-else 8.11.2 or-else 8.12+beta1 or-else 8.12.0 but you have this version: The Coq Proof Assistant, version 8.12.1 (November 2020) compiled on Nov 17 2020 6:42:48 with OCaml 4.10.1.  Stop.

So we either need to adjust Coq bounds for the package or patch it more.

view this post on Zulip Karl Palmskog (Nov 17 2020 at 08:17):

looks like one way to solve this would be to set IGNORECOQVERSION=1 as a parameter for the build declaration

view this post on Zulip Théo Zimmermann (Nov 17 2020 at 08:58):

Yes, for the Windows installer I had to do this for both the build step and the installation step.

view this post on Zulip Karl Palmskog (Nov 17 2020 at 09:00):

OK, let's just do this in the package then for now, and Michael can change it later if he prefers something else

view this post on Zulip Karl Palmskog (Nov 17 2020 at 15:18):

sigh, apparently the VST Makefile doesn't allow installing (silently fails) when passing IGNORECOQVERSION, since they don't pass this variable on to the script that calculates the files to install, which is a recursive make invocation. What a mess...

view this post on Zulip Théo Zimmermann (Nov 17 2020 at 16:13):

OMG then the Windows package for 8.12.1 is broken with respect to VST.

view this post on Zulip Théo Zimmermann (Nov 17 2020 at 16:14):

Well, I don't care enough to fix it. VST users will have to wait for the Coq Platform.

view this post on Zulip Karl Palmskog (Nov 17 2020 at 17:35):

hmm, I think I will try it out and see whether it's broken, but sounds plausible

view this post on Zulip Michael Soegtrop (Nov 29 2020 at 16:15):

Sorry, I just saw this. The VST make file is restricted to what has been tested. Assuming that 8.12.1 works, the solution is to updat ethe makefile. Planned next week.

view this post on Zulip Enrico Tassi (Nov 29 2020 at 16:17):

Théo Zimmermann said:

OMG then the Windows package for 8.12.1 is broken with respect to VST.

Did you manage to compile CoqIDE for 8.12.1?

view this post on Zulip Enrico Tassi (Nov 29 2020 at 16:18):

The problem I face seems to be cywin related, and not Coq related

view this post on Zulip Michael Soegtrop (Nov 29 2020 at 16:20):

I can work on a 8.12.1.beta1 platform release next week - shouldn't be difficult. The VST make file is generally very stiff regarding versions and insists to compile only combinations which are known to work.

view this post on Zulip Théo Zimmermann (Nov 30 2020 at 10:10):

Did you manage to compile CoqIDE for 8.12.1?

I would hope that there would already be an issue on the Coq repo if the Windows installer for 8.12.1 did not contain a working CoqIDE...

view this post on Zulip Michael Soegtrop (Dec 06 2020 at 17:34):

CoqIDE works fine for me with 8.12.1 - no issues. I just pushed a few updates to the Coq platform 8.12 branch (preparing the release).


Last updated: Jan 30 2023 at 11:03 UTC