search

mit-plv / kami

A Platform for High-Level Parametric Hardware Specification and its Modular Verification
https://plv.csail.mit.edu/kami/
MIT License
142 stars 24 forks source link

Make Command Fails Under Coq 8.8.1 #5

Closed llee454 closed 6 years ago

llee454 commented 6 years ago

Make fails with the following errors when run under Coq 8.8.1: $ make

make -f Makefile.coq.all make[1]: Entering directory '/home/larry/Projects/mit-kami' COQC Kami/ParametricWf.v File "./Kami/ParametricWf.v", line 281, characters 2-164: Error: Recursive definition of ValidRegsMetaModule is ill-formed. In environment type : Kind -> Type ValidRegsMetaModule : MetaModule -> Prop Recursive definition on "MetaModule" which should be a recursive inductive type. Recursive definition is: "fun mm : MetaModule => ValidRegsMetaRules (metaRegs mm) (metaRules mm) /\ ValidRegsMetaMeths (metaRegs mm) (metaMeths mm)".

Makefile.coq.all:656: recipe for target 'Kami/ParametricWf.vo' failed make[2]: [Kami/ParametricWf.vo] Error 1 Makefile.coq.all:317: recipe for target 'all' failed make[1]: [all] Error 2 make[1]: Leaving directory '/home/larry/Projects/mit-kami' Makefile:26: recipe for target 'coq' failed make: *** [coq] Error 2

vmurali commented 6 years ago

Larry, can you use https://github.com/sifive/Kami instead. That's where all the development is happening now.

joonwonc commented 6 years ago

If you're using Coq 8.8.x, you can use the coq-8.8 branch, which is up-to-date. We will soon merge the branch into master though.

llee454 commented 6 years ago

Thanks,

I was just taking a moment to compare the two developments, noticed that the master branch did not compile under the latest Coq version, and felt that I should post an issue for it.

joonwonc commented 6 years ago

Thanks for the report; just merged coq-8.8 into master.