Stream: MetaCoq

Topic: Strange Error when Compile PCUICWcbvEval.v

view this post on Zulip Ember Edison (Aug 28 2021 at 06:56):

coqc PCUICWcbvEval.v

File "./PCUICWcbvEval.v", line 528, characters 4-34:
Error: The reference x was not found in the current environment.

view this post on Zulip Paolo Giarrusso (Aug 28 2021 at 07:04):

Which Metacoq version against which dependency versions? For instance, the head of the 8.13 branch needs a specific version of Equations — and the changes might include the x mentioned in your error?

https://github.com/MetaCoq/metacoq/pull/571
https://github.com/MetaCoq/metacoq/commit/b4cab3eb299154d527a6996ef31d27265ce67590#diff-8d2f69eedbc169ff70ee8cfd51c27396df70bfe65549b9ce51f88548a4dcfae1

view this post on Zulip Ember Edison (Aug 28 2021 at 07:13):

Paolo Giarrusso said:

Which Metacoq version against which dependency versions? For instance, the head of the 8.13 branch needs a specific version of Equations — and the changes might include the x mentioned in your error?

coq-8.13 branch, compiling from sources

view this post on Zulip Paolo Giarrusso (Aug 28 2021 at 07:41):

Then coq-metacoq-pcuic.opam says you need coq-equations version 1.3~beta2+8.13.

Last updated: May 31 2023 at 09:01 UTC