Anomaly "Uncaught exception Not_found." when trying to use Ltac2

[afdw]

On this file:

From Ltac2 Require Import Ltac2.

Goal True /\ True.
  split; exact I.
Qed.

I get the following error:

Anomaly "Uncaught exception Not_found." Please report at http://coq.inria.fr/bugs/.
Raised at HMap.Make.find in file "clib/hMap.ml", line 361, characters 31-46 Called from Ltac2_plugin__Tac2env.interp_notation in file "plugins/ltac2/tac2env.ml" (inlined), line 126, characters 25-54
Called from Ltac2_plugin__Tac2intern.expand_notation in file "plugins/ltac2/tac2intern.ml", line 1093, characters 8-34
Called from Ltac2_plugin__Tac2intern.intern_rec in file "plugins/ltac2/tac2intern.ml", line 1228, characters 10-36
Called from Ltac2_plugin__Tac2intern.intern_rec in file "plugins/ltac2/tac2intern.ml", line 1236, characters 17-39
Called from Ltac2_plugin__Tac2intern.intern in file "plugins/ltac2/tac2intern.ml", line 1554, characters 15-36
Called from Ltac2_plugin__Tac2entries.ltac2_interp in file "plugins/ltac2/tac2entries.ml", line 1233, characters 15-40
Called from ComTactic.solve in file "vernac/comTactic.ml" (inlined), line 58, characters 10-22
Called from Ltac2_plugin__Tac2entries.call in file "plugins/ltac2/tac2entries.ml", line 1242, characters 2-71
Called from Vernactypes.vtmodifyproof.(fun) in file "vernac/vernactypes.ml", line 185, characters 32-47
Called from Vernactypes.typed_vernac.(fun) in file "vernac/vernactypes.ml", line 170, characters 65-71
Called from Vernactypes.run.(fun) in file "vernac/vernactypes.ml", line 164, characters 15-32
Called from Vernactypes.combine_runners.(fun) in file "vernac/vernactypes.ml", line 126, characters 16-23
Called from Vernactypes.OpaqueAccess.runner.(fun) in file "vernac/vernactypes.ml", line 114, characters 30-34
Called from Vernactypes.combine_runners.(fun) in file "vernac/vernactypes.ml", line 125, characters 14-100
Called from Vernactypes.combine_runners.(fun) in file "vernac/vernactypes.ml", line 126, characters 16-23
Called from Vernactypes.Proof.runner.(fun) in file "vernac/vernactypes.ml", line 72, characters 19-22
Called from Vernactypes.combine_runners.(fun) in file "vernac/vernactypes.ml", line 125, characters 14-100
Called from Vernactypes.Prog.runner.(fun) in file "vernac/vernactypes.ml", line 27, characters 30-34
Called from Vernactypes.combine_runners.(fun) in file "vernac/vernactypes.ml", line 124, characters 12-173
Called from Vernactypes.combine_runners.(fun) in file "vernac/vernactypes.ml", line 124, characters 12-173
Called from Vernactypes.run in file "vernac/vernactypes.ml", line 163, characters 14-96
Called from Vernacinterp.interp_expr in file "vernac/vernacinterp.ml", line 120, characters 60-157
Called from Vernacinterp.interp_control.(fun) in file "vernac/vernacinterp.ml", line 153, characters 24-126
Called from Flags.with_modified_ref in file "lib/flags.ml", line 17, characters 14-17 Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Vernacinterp.interp_gen in file "vernac/vernacinterp.ml", line 197, characters 16-41 Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Dm__ExecutionManager.interp_ast in file "dm/executionManager.ml", line 156, characters 13-46

Coq version: https://github.com/coq/coq/commit/ed9fe8e2351ff59f662c3950c1cb07813db312bd. Language server version: https://github.com/coq-community/vscoq/commit/d37fd297e509ee41e07bbad07a4e497cbb77d485.

[SkySkimmer]

Cannot reproduce in proof general, may be a vscoq issue cc @rtetley

[rtetley]

Also not reproducible on coqide, probably something to do with interp phase in the language server ? @gares

[gares]

The Not_found comes from a table living in the synterp state. But that table has, as keys, kernel names that look like data that only makes sense in the interp phase. I know they are used as sort of UUIDs, but Ltac2 crafts them at synterp time they may be bogus. Maybe @SkySkimmer know better why Ltac notations are keyd on kernel names.

[SkySkimmer]

(* in tac2env *)
let ltac_notations = Summary.ref KNmap.empty ~stage:Summary.Stage.Synterp ~name:"ltac2-notations"

should be stage Interp (this map should be only the interp side of ltac2 notations)

[SkySkimmer]

Could you try with https://github.com/coq/coq/pull/19096 ?

[rtetley]

On it!

[rtetley]

Yup ! That fixes it !

[afdw]

Thanks!