Stream: Coq users

Topic: software foundations coq version?


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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 08 2021 at 20:27):

@Callan McGill seems your version is a bit outdated?

view this post on Zulip Emilio Jesús Gallego Arias (Feb 08 2021 at 20:27):

Try with SF 5.8

view this post on Zulip Callan McGill (Feb 08 2021 at 20:27):

ok, will do, thanks!

view this post on Zulip Emilio Jesús Gallego Arias (Feb 08 2021 at 20:27):

The online version can be of help too

view this post on Zulip Emilio Jesús Gallego Arias (Feb 08 2021 at 20:28):

https://jscoq.github.io/ext/sf/

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

view this post on Zulip Li-yao (Feb 08 2021 at 21:04):

It should build with both 8.12 and 8.13 so something else is going on...

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

view this post on Zulip Li-yao (Aug 01 2021 at 22:07):

I can confirm it compiles with 8.13.2 "Works on my machine" :)


Last updated: Jan 27 2023 at 01:03 UTC