Stream: Coq devs & plugin devs

Topic: Debugging `Not_found` anomaly in Ltac2 `eval_cbn`

view this post on Zulip Janno (Jan 06 2021 at 13:07):

I switched a piece of Ltac2 from Std.eval_lazy to Std.eval_cbn and the tactic now raises a Not_found anomaly in 

Raised at file "kernel/environ.ml", line 162, characters 29-44
Called from file "engine/eConstr.ml" (inlined), line 723, characters 51-67
Called from file "pretyping/reductionops.ml", line 981, characters 13-29

(This is Coq 8.12.1). The corresponding code is the Rel branch of a match on a constr in whrec in whd_state_gen. How do I go about debugging this?

view this post on Zulip Janno (Jan 06 2021 at 13:08):

Oh, maybe I have unbound rels in my term. I guess lazy doesn't care about that?

view this post on Zulip Pierre-Marie Pédrot (Jan 06 2021 at 13:09):

lazy is probably more resilient than cbn indeed

view this post on Zulip Janno (Jan 06 2021 at 13:11):

Ugh, indeed.. unbound rels hidden in implicit arguments. I guess that settles it.

Last updated: Dec 07 2023 at 09:01 UTC