coq

coq copied to clipboard

Description of the problem

Finished failing transaction in 18.917 secs (18.809u,0.108s) (failure) Fatal error: exception Not_found Raised at Int.Map.find in file "clib/int.ml", line 39, characters 14-29 Called from HMap.Make.find in file "clib/hMap.ml", line 365, characters 12-28 Called from Nametab.shortest_qualid_of_global in file "library/nametab.ml", line 552, characters 17-64 Called from Constrextern.default_extern_reference in file "interp/constrextern.ml", line 327, characters 6-51 Called from Constrextern.extern_reference in file "interp/constrextern.ml" (inlined), line 335, characters 35-62 Called from Constrextern.extern_ref in file "interp/constrextern.ml", line 972, characters 4-31 Called from Constrextern.extern in file "interp/constrextern.ml", line 999, characters 71-95 Called from Proof_diffs.pr_leconstr_env in file "printing/proof_diffs.ml", line 272, characters 37-96 Called from Printer.pr_lconstr_under_binders_env in file "printing/printer.ml" (inlined), line 86, characters 35-82 Called from Ltac_plugin__Tactic_debug.explain_ltac_call_trace.pr_call.(fun) in file "plugins/ltac/tactic_debug.ml", line 825, characters 41-89 Called from Stdlib__list.map in file "list.ml", line 92, characters 20-23 Called from Pp.prlist_sep_lastsep in file "lib/pp.ml", line 249, characters 14-29 Called from Pp.prlist_with_sep in file "lib/pp.ml" (inlined), line 268, characters 31-68 Called from Ltac_plugin__Tactic_debug.explain_ltac_call_trace.pr_call in file "plugins/ltac/tactic_debug.ml", line 823, characters 12-200 Called from Stdlib__list.map in file "list.ml", line 92, characters 20-23 Called from Stdlib__list.map in file "list.ml", line 92, characters 32-39 Called from Stdlib__list.map in file "list.ml", line 92, characters 32-39 Called from Stdlib__list.map in file "list.ml", line 92, characters 32-39 Called from Stdlib__list.map in file "list.ml", line 92, characters 32-39 Called from Stdlib__list.map in file "list.ml", line 92, characters 32-39 Called from Stdlib__list.map in file "list.ml", line 92, characters 32-39 Called from Stdlib__list.map in file "list.ml", line 92, characters 32-39 Called from Stdlib__list.map in file "list.ml", line 92, characters 32-39 Called from Stdlib__list.map in file "list.ml", line 92, characters 32-39 Called from Stdlib__list.map in file "list.ml", line 92, characters 32-39 Called from Pp.prlist_sep_lastsep in file "lib/pp.ml", line 249, characters 14-29 Called from Ltac_plugin__Tactic_debug.explain_ltac_call_trace in file "plugins/ltac/tactic_debug.ml", line 838, characters 11-32 Called from Ltac_plugin__Tactic_debug.extract_ltac_trace in file "plugins/ltac/tactic_debug.ml", line 856, characters 21-55 Called from Ltac_plugin__Tactic_debug.get_ltac_trace in file "plugins/ltac/tactic_debug.ml", line 880, characters 23-54 Called from CList.map_filter_loop in file "clib/cList.ml", line 366, characters 10-13 Called from CList.map_filter in file "clib/cList.ml", line 380, characters 6-28 Called from CErrors.print_gen in file "lib/cErrors.ml", line 107, characters 4-69 Called from CErrors.iprint in file "lib/cErrors.ml", line 121, characters 2-34 Called from Coqloop.read_and_execute in file "toplevel/coqloop.ml", line 476, characters 14-38 Called from Coqloop.vernac_loop in file "toplevel/coqloop.ml", line 488, characters 20-43 Called from Coqloop.loop in file "toplevel/coqloop.ml", line 513, characters 27-45 Called from Dune__exe__Coqtop_bin in file "topbin/coqtop_bin.ml", line 16, characters 10-35

Generated by

"coqtop" -bt '-w' '+implicit-core-hint-db,+implicits-in-term,+non-reversible-notation,+deprecated-intros-until-0,+deprecated-focus,+unused-intro-pattern,+deprecated-hint-constr,+fragile-hint-constr,+variable-collision,+unexpected-implicit-declaration,+omega-is-deprecated,+deprecated-instantiate-syntax,+non-recursive,+deprecated-hint-rewrite-without-locality,+deprecated-hint-without-locality,+deprecated-instance-without-locality,+undeclared-scope,+deprecated-typeclasses-transparency-without-locality,unsupported-attributes' -w -notation-overridden,-unusable-identifier -w -notation-overridden,-undeclared-scope  "-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" -I src/Rewriter/Util/plugins  -R src/Rewriter Rewriter < src/Rewriter/Rewriter/Examples/PerfTesting/Plus0Tree.v 2>&1 | sed 's|file "\([^"]*\)"\([^,]*\), line \([0-9]*\)|[file "\1"\2, line \3](https://github.com/coq/coq/blob/V8.15.0/\1#L\3)|g'

after make src/Rewriter/Rewriter/Examples/PerfTesting/Plus0Tree.vo on https://github.com/JasonGross/rewriter/tree/zzz-bug-not-found

Sorry, I don't have an easy way to minimize this, but hopefully the backtrace is enough to harden coqtop against crashing here. I'm guessing the issue is that my failing tactic added something to the global environment, this was rolled back, and then the exception printing failed

Note that coqc fails with a regular error message

Coq Version

8.15.0

Here's a small example:

$ cat foo.v

Ltac foo x y := idtac; fail 1.
Ltac bar x f := idtac; f foo x I.
Ltac baz x := let H := fresh in
              simple refine (let H : True := _ in _);
              [ abstract exact I
              | let v := (eval cbv in H) in
                let F := ltac:(fun _ => let v' := v in constr:(fun _ => ltac:(idtac v'; fail 1))) in
                let f := ltac:(fun f x y => idtac v; f x) in
                f F () () ].
Set Ltac Backtrace.
Goal True.
  baz I.

$ coqc -q foo.v
Unnamed_thm_subproof
Unnamed_thm_subproof
File "./foo.v", line 12, characters 2-8:
Error:
In nested Ltac calls to "baz", "f" (bound to fun f x y => idtac v; f x),
"f" (bound to fun _ => let v' := v in
                       constr:((fun _ => _))) and
"(fun _ => _)" (with x:=I, v':=Unnamed_thm_subproof, v:=Unnamed_thm_subproof,
H:=H), last term evaluation failed.
Tactic failure (level 1).

$ coqtop -q < foo.v
Welcome to Coq 8.15.0
Skipping rcfile loading.

Coq < foo is defined

Coq < bar is defined

Coq < Coq < Coq < Coq < Coq < Coq < Coq < baz is defined

Coq <
Coq < 1 goal

  ============================
  True

Unnamed_thm < Unnamed_thm_subproof
Unnamed_thm_subproof
Fatal error: exception Not_found