Stream: Coq users

Topic: Compiler error for Foundations of Separation Logic


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mukesh Tiwari (Jul 25 2020 at 01:46):

Thanks @Karl Palmskog .

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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: Jan 31 2023 at 12:01 UTC