Karl Palmskog (Nov 17 2020 at 07:12): 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.
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
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.
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
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...
Théo Zimmermann (Nov 17 2020 at 16:13):OMG then the Windows package for 8.12.1 is broken with respect to VST.
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.
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
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.
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?
Enrico Tassi (Nov 29 2020 at 16:18):The problem I face seems to be cywin related, and not Coq related
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.
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...
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: Apr 18 2024 at 04:02 UTC