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

How to build? #13

Closed HuStmpHrrr closed 5 years ago

HuStmpHrrr commented 5 years ago

Sorry to ask a stupid question but I just can't build from master branch. I am wonder how am I supposed to build? I am using Coq 8.8.1 and equations, but it keeps fail to build with follow messages:

NOT IN _CoqProject: Instance/LambdaOld.v
NOT IN _CoqProject: Instance/Lambda/Lec1.v
NOT IN _CoqProject: Instance/Lambda/Connect.v
NOT IN _CoqProject: Instance/Lambda/Nominal.v
NOT IN _CoqProject: Instance/Lambda/Lemmas.v
NOT IN _CoqProject: Instance/Lambda/Definitions.v
NOT IN _CoqProject: Instance/Lambda/Lec3.v
NOT IN _CoqProject: Instance/Lambda/Lec2.v
make -j -f Makefile.coq  # TIMECMD=time
make[1]: Entering directory '/home/hu/projects/category-theory'
make[2]: *** No rule to make target 'Instance/Lambda/Definitions.vo', needed by 'Instance/Lambda.vo'.  Stop.
COQC Lib/Datatypes.v
make[2]: *** Waiting for unfinished jobs....
File "./Lib/Datatypes.v", line 212, characters 0-4:
Error:
Illegal application: 
The term "list_equivalence_obligation_1" of type
 "∀ (A : Type) (H : Setoid A), Reflexive list_equiv"
cannot be applied to the terms
 "A" : "Type"
 "H" : "Setoid A"
The 1st term has type "Type@{Category.Lib.Datatypes.1007}"
which should be coercible to "Type@{Category.Lib.Datatypes.1020}".

Makefile.coq:656: recipe for target 'Lib/Datatypes.vo' failed
make[2]: *** [Lib/Datatypes.vo] Error 1
Makefile.coq:317: recipe for target 'all' failed
make[1]: *** [all] Error 2
make[1]: Leaving directory '/home/hu/projects/category-theory'
Makefile:2: recipe for target 'all' failed
make: *** [all] Error 2

Even if I added those missing files to _CoqProject, it still fails to build, not to mention the universe inconsistency. How should I proceed?

Also, it seems Lambda depends on Metalib, which is not stated as dependency in README. Can I just skip Lambda entirely?

jwiegley commented 5 years ago

Hello! This library has never worked with 8.8.1, due to a bug that I reported which was fixed in 8.8.2. Please let me know if the problem persists after upgrading.