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?
Try with SF 5.8
ok, will do, thanks!
The online version can be of help too
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?
It should build with both 8.12 and 8.13 so something else is going on...
@Li-yao the file says:
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.
I can confirm it compiles with 8.13.2 "Works on my machine" :)
Last updated: Jan 27 2023 at 01:03 UTC