Stream: Coq devs & plugin devs

Topic: Coq.Init.Datatypes.nat does not appear in env


view this post on Zulip Arpan Agrawal (May 27 2024 at 18:37):

Hi,

I'm porting a plugin from Coq 8.13 to 8.14, and I get this error when I run one of the tests (I've included the backtrace):

File "./coq/Preprocess.v", line 35, characters 2-29:
Error:
Anomaly
"Inductive Coq.Init.Datatypes.nat does not appear in the environment."
Please report at http://coq.inria.fr/bugs/.
Raised at Exninfo.iraise in file "clib/exninfo.ml", line 79, characters 4-11
Called from Environ.lookup_mind in file "kernel/environ.ml" (inlined), line 252, characters 6-30
Called from Inductive.expand_case in file "kernel/inductive.ml", line 430, characters 15-54
Called from Hofs.map_term_env_rec in file "src/coq-plugin-lib/src/coq/logicutils/hofs/hofs.ml", line 144, characters 21-42
Called from Hofs.map_term_env_rec in file "src/coq-plugin-lib/src/coq/logicutils/hofs/hofs.ml", line 145, characters 21-86
Called from Hofs.map_term_env_rec in file "src/coq-plugin-lib/src/coq/logicutils/hofs/hofs.ml", line 145, characters 21-86
Called from Hofs.map_term in file "src/coq-plugin-lib/src/coq/logicutils/hofs/hofs.ml", line 196, characters 4-122
Called from Debruijn.unshift_by in file "src/coq-plugin-lib/src/coq/logicutils/hofs/debruijn.ml", line 55, characters 2-23
Called from CList.fold_left_i.it_list_f in file "clib/cList.ml", line 560, characters 32-41
Called from Desugar.desugar_match.build_premise in file "src/automation/desugar.ml", line 301, characters 14-72
Called from Stdlib__Array.map2 in file "array.ml", line 122, characters 23-60
Called from Desugar.desugar_match in file "src/automation/desugar.ml", line 302, characters 7-73
Called from Desugar.desugar_constr.aux.(fun) in file "src/automation/desugar.ml", line 336, characters 13-60
Called from Hofs.map_term_env_rec in file "src/coq-plugin-lib/src/coq/logicutils/hofs/hofs.ml", line 157, characters 22-44
Called from Hofs.map_term_env_rec in file "src/coq-plugin-lib/src/coq/logicutils/hofs/hofs.ml", line 149, characters 21-86
Called from Hofs.map_term_env_rec in file "src/coq-plugin-lib/src/coq/logicutils/hofs/hofs.ml", line 149, characters 21-86
Called from Hofs.map_term_env_rec in file "src/coq-plugin-lib/src/coq/logicutils/hofs/hofs.ml", line 149, characters 21-86
Called from Desugar.desugar_constr in file "src/automation/desugar.ml", line 345, characters 20-40
Called from Transform.transform_constant in file "src/coq-plugin-lib/src/coq/logicutils/transformation/transform.ml", line 54, characters 21-45
Called from Fixtranslation.do_desugar_constant in file "src/fixtranslation.mlg", line 34, characters 4-132

Can someone tell me what the issue might be?
Thanks!

The code is here if that's helpful: https://github.com/agrarpan/fix-to-elim/tree/coq-8.14

view this post on Zulip Gaëtan Gilbert (May 27 2024 at 20:01):

you use empty_env here https://github.com/agrarpan/coq-plugin-lib/blob/f2e8f9104d6a6a58254c584251d92cfffcdc93df/src/coq/logicutils/hofs/hofs.ml#L199 and other places
you should never do that, always thread the correct env instead
also never use Evd.empty, if you know you don't have evars or local universes use Evd.from_env

view this post on Zulip Arpan Agrawal (May 27 2024 at 20:34):

Thanks! I will make those changes. Do you know why this wasn't an issue until 8.13?

view this post on Zulip Gaëtan Gilbert (May 27 2024 at 20:40):

is 8.13 the one with the case representation change? ie expand_case

view this post on Zulip Arpan Agrawal (May 27 2024 at 20:41):

Yes, 8.14 is where the case representation changed


Last updated: Oct 13 2024 at 01:02 UTC