You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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?
The text was updated successfully, but these errors were encountered:
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.
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:
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?
The text was updated successfully, but these errors were encountered: