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

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.

so @Mukesh Tiwari you can either wait for a fix or use (an opam switch with) Coq 8.9.

Thanks @Karl Palmskog .

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.

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.

works for me on 8.10.2, 8.11.2 and 8.12. (for tarball with md5 `cf28710bc68b24cb80725aee106c2efe`

)

@Arthur Charguéraud Thanks for uploading the new version. It's working with Coq-8.11.2.

Last updated: Jun 25 2024 at 14:01 UTC