Callan McGill (Feb 08 2021 at 20:26): Callan McGill (Feb 08 2021 at 20:26):Does anyone know which version of coq I should be using with software foundations. When I try to compile using the makefile with both 8.13.0 and 8.12.2 I get the error:
File "./Tactics.v", line 1154, characters 38-39:
Error:
The term "5" has type "nat" while it is expected to have type "string".
@Callan McGill seems your version is a bit outdated?
Emilio Jesús Gallego Arias (Feb 08 2021 at 20:27):Try with SF 5.8
Callan McGill (Feb 08 2021 at 20:27):ok, will do, thanks!
Emilio Jesús Gallego Arias (Feb 08 2021 at 20:27):The online version can be of help too
Emilio Jesús Gallego Arias (Feb 08 2021 at 20:28):https://jscoq.github.io/ext/sf/
Callan McGill (Feb 08 2021 at 20:30):I get exactly the same error with version 5.8 and coq 8.13.0, what is the exact combination you are meant to use so that it can compile?
Li-yao (Feb 08 2021 at 21:04):It should build with both 8.12 and 8.13 so something else is going on...
Bas Spitters (Jul 30 2021 at 11:35):@Li-yao the file says:
https://github.com/DeepSpec/sfdev/blob/master/INSTRUCTORS
coq 8.12.2
Could you confirm it works with a recent version too.
I would also recommend providing install instructions using coq platform. That should simplify installing QC on windows for example...
I'm trying to get things to compile, will report back here, if succesful.
Li-yao (Aug 01 2021 at 22:07):I can confirm it compiles with 8.13.2 "Works on my machine" :)
Last updated: Oct 03 2023 at 02:34 UTC