search

jwiegley / category-theory

An axiom-free formalization of category theory in Coq for personal study and practical work
BSD 3-Clause "New" or "Revised" License
745 stars 68 forks source link

not build for 8.12 #18

Closed HuStmpHrrr closed 3 years ago

HuStmpHrrr commented 4 years ago

the commit seems to indicate the library would work for 8.12 but it doesn't work for me:

File "./Theory/Isomorphism.v", line 89, characters 29-33:
Error:
 (in proof isomorphism_equiv_equivalence_obligation_2): Attempt to save an incomplete proof

Makefile.coq:715: recipe for target 'Theory/Isomorphism.vo' failed
make[2]: *** [Theory/Isomorphism.vo] Error 1
File "./Lib/MapDecide.v", line 333, characters 29-30:
Error:
Syntax error: [constr:operconstr level 200] expected after '[' (in [constr:operconstr]).
coqc -v
The Coq Proof Assistant, version 8.12.0 (September 2020)
compiled on Sep 1 2020 1:01:58 with OCaml 4.07.1

which Coq version works for you?

michaeljklein commented 4 years ago

I've been using:

coqc -v
The Coq Proof Assistant, version 8.10.2 (March 2020)
compiled on Mar 4 2020 13:46:04 with OCaml 4.07.1
jwiegley commented 3 years ago

It should now build for any version from 8.10 to 8.13.