Mukesh Tiwari (Jul 25 2020 at 01:26): Mukesh Tiwari (Jul 25 2020 at 01:26):Hi everyone, I am trying to compile the downloaded file [1], but I am getting error:
File "./SepSimpl.v", line 1664, characters 2-19:
Error: Tactic failure: Instantiation fails for:
(boxer hwand_hpure_l :: boxer ___ :: >>).
make[2]: *** [SLFDirect.vo] Error 1
make[1]: *** [all] Error 2
make: *** [build] Error 2
slf coqtop -v
The Coq Proof Assistant, version 8.11.2 (July 2020)
compiled on Jul 25 2020 1:04:04 with OCaml 4.09.1
Any idea how to resolve this?
[1] https://chargueraud.org/teach/verif/slf.tar.gz
Karl Palmskog (Jul 25 2020 at 01:36):unfortunately, the tarball (md5: 3df376c63060a32033a04c698900f079) is only compatible with Coq 8.9 and presumably Coq 8.8. Ping @Arthur Charguéraud that compilation fails on Coq 8.10.2, Coq 8.11.2 and Coq 8.12.
Karl Palmskog (Jul 25 2020 at 01:37):so @Mukesh Tiwari you can either wait for a fix or use (an opam switch with) Coq 8.9.
Mukesh Tiwari (Jul 25 2020 at 01:46):Thanks @Karl Palmskog .
Arthur Charguéraud (Jul 25 2020 at 13:23):I thought that I had uploaded the version that compiles with all versions in the range 8.8 - 8.12. Let me double check right away.
Arthur Charguéraud (Jul 25 2020 at 13:33):I've just uploaded a new version of the archive that, I've just tested on my laptop, compiles well with 8.9, 8.11, and 8.12. (Warning show up, but they can be safely ignored). Please try it out and let me know if you encounter any issue.
Karl Palmskog (Jul 25 2020 at 13:55):works for me on 8.10.2, 8.11.2 and 8.12. (for tarball with md5 cf28710bc68b24cb80725aee106c2efe)
Mukesh Tiwari (Jul 26 2020 at 02:43):@Arthur Charguéraud Thanks for uploading the new version. It's working with Coq-8.11.2.
Last updated: Oct 13 2024 at 01:02 UTC