search

ilyasergey / pnp

Lecture notes for a short course on proving/programming in Coq via SSReflect.
https://ilyasergey.net/pnp
BSD 2-Clause "Simplified" License
159 stars 16 forks source link

Fix warnings #16

Closed k4rtik closed 4 years ago

k4rtik commented 4 years ago

I am assuming this is the primary working version of HTT implementation, hence this PR. The one available at https://software.imdea.org/~aleks/htt/ seems old.

anton-trunov commented 4 years ago

Hi @k4rtik! There is also a Github repo -- https://github.com/imdea-software/htt, but I have no idea if it's compatible with the version in this book.

k4rtik commented 4 years ago

Thanks, @anton-trunov. Indeed, that's the same version as the link in the OP. I haven't compared the diffs, but from the commit history of this folder (https://github.com/ilyasergey/pnp/commits/master/htt) it seems like they started out about the same until the port to fcsl-pcm and removal of unused files. At least, this version in PnP seems better maintained.

ilyasergey commented 4 years ago

@anton-trunov I guess there is no HTT available as an opam package?

anton-trunov commented 4 years ago

@ilyasergey Indeed you are right, it's not on opam.

ilyasergey commented 4 years ago

Okay, on Coq 8.9.1, I have the following build error:

File "./htt/stsep.v", line 8, characters 8-13:
Error:
Syntax error: 'Equivalent' 'Keys' expected after 'Declare' (in [vernac:command]).

make[2]: *** [htt/stsep.vo] Error 1
make[1]: *** [all] Error 2
make: *** [default] Error 2
k4rtik commented 4 years ago

Ah, it looks like the new Declare Scope never made it to v8.9. See: https://github.com/coq/coq/issues/8925 I am on v8.10.2 where it is included and issues warnings when missing.

Please feel free to remove/comment Declare Scope lines if v8.9 needs to be supported.