Trouble Building in Coq 8.10-8.12.2
Closed this issue · 2 comments
I'm trying to build verdi-raft for a benchmark set I'm using, and I'm having some trouble.
My tool supports the released versions of Coq 8.10.0 - 8.12.2.
With Coq 8.10 and 8.11, I can install all the dependencies of verdi-raft through opam fine, but when I try to build verdi-raft itself, I get a failure of the lia tactic:
File "./raft/CommonTheorems.v", line 87, characters 11-15:
Error: Tactic failure: Cannot find witness.
If I revert a few commits back, omega is used instead of lia, which I figured might work better on older coq versions, but then I get errors that omega was never imported.
If instead I try to build with Coq 8.12.2, I find that opam won't install the dependencies:
(base) [5] sanchezstern@swarm033> opam install coq-verdi
Sorry, no solution found: there seems to be a problem with your request.
No solution found, exiting
This surprised me because there are commits in verdi-raft that claim to support up to Coq 8.14. But the StructTact and Cheerios dependencies both seem to list coq constraints:
"coq" {(>= "8.6.1" & < "8.12~") | (= "dev")`)
Which requires that the coq version be strictly less than 8.12, or be "dev". The opam file for StructTact on github appears to relax this constraint a bit, but the one indexed by opam in extra-dev still has the hard less than 12 constraint (as does the opam file for Cheerios in both places).
Basically, the gist of my question is, is there a recommended procedure for building verdi-raft now on non-dev coq?
Verdi Raft (and the libraries it depends on) is part of Coq's CI, and as such, the only version it is guaranteed to work with is the master branch of Coq. For every Coq version going back to Coq 8.7, there are commit SHAs here that work with that Coq version, but they can be difficult to find.
The repo version of Verdi Raft and its dependencies currently happens to work on Coq 8.12 to 8.15. However, the .opam files are not up to date with this. One way to get around this is to edit the repo opam files locally and set something like:
"coq" {>= "8.12"}
and then you do something like:
opam pin add <package-name>.opam -k path .
The "official" opam files may get updated later on during summer 2022, but I wouldn't count on an update all that soon.
If you want something that works with 8.11, you'll unfortunately have to dig into commit SHAs.
Okay, sounds like I can use a couple of sed scripts to get the whole thing building on 8.12, thanks!