SkySkimmer/coq-ltac2-compiler

Assertion failed in `force_nontac_expr`

Closed this issue · 1 comments

I am still trying to make progress on compiling our automation and managed to minimize another failure:

From Ltac2Compiler Require Import Ltac2Compiler.
Ltac2 Compile apply_cancelx_instance.
Ltac2 beta_iota :=
  let x := { rBeta := true; rMatch := true; rFix := true; rCofix := true; rZeta := false; rDelta := false; rConst := [] } in x.
Ltac2 test () := Std.eval_lazy beta_iota.
Set Debug "backtrace".
Ltac2 Compile test.

The failure disappears when using

Ltac2 beta_iota :=
  { rBeta := true; rMatch := true; rFix := true; rCofix := true; rZeta := false; rDelta := false; rConst := [] }.

Unfortunately the backtrace is just pure confusion:

Error: Anomaly "File "src/tac2compile.ml", line 624, characters 2-8: Assertion failed."
Please report at http://coq.inria.fr/bugs/.
Raised at Unicode.next_utf8 in file "clib/unicode.ml", line 162, characters 16-34
Called from Unicode.ident_refutation.aux in file "clib/unicode.ml", line 267, characters 26-39
Called from Unicode.ident_refutation in file "clib/unicode.ml", line 271, characters 16-21
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" (inlined), line 212, characters 16-41
Called from Vernacinterp.interp.(fun) in file "vernac/vernacinterp.ml", line 226, characters 54-111
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from NewProfile.profile in file "lib/newProfile.ml" (inlined), line 151, characters 32-36
Called from Vernacinterp.interp in file "vernac/vernacinterp.ml" (inlined), line 226, characters 15-115
Called from Vernacinterp.interp in file "vernac/vernacinterp.ml", line 226, characters 15-115
Called from Stm.Reach.known_state.reach.(fun) in file "stm/stm.ml", line 2185, characters 16-43
Called from Stm.State.define in file "stm/stm.ml", line 965, characters 6-10
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Stm.Reach.known_state.reach in file "stm/stm.ml", line 2327, characters 4-105
Called from Stm.observe in file "stm/stm.ml", line 2424, characters 4-60
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Vernac.interp_vernac in file "toplevel/vernac.ml", line 79, characters 29-50
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Vernac.process_expr in file "toplevel/vernac.ml", line 153, characters 6-46

Raised at Exninfo.iraise in file "clib/exninfo.ml" (inlined), line 79, characters 4-11
Called from Vernac.process_expr in file "toplevel/vernac.ml", line 164, characters 4-34
Called from Util.try_finally in file "lib/util.ml" (inlined), line 140, characters 16-19
Called from Vernac.process_expr in file "toplevel/vernac.ml" (inlined), line 168, characters 2-166
Called from Vernac.process_expr in file "toplevel/vernac.ml", line 168, characters 2-166
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Util.try_finally in file "lib/util.ml" (inlined), line 144, characters 6-32
Called from Vernac.process_expr in file "toplevel/vernac.ml", line 168, characters 2-166
Called from Coqloop.process_toplevel_command in file "toplevel/coqloop.ml", line 433, characters 17-62

I am working on a slightly adapted fork of the main branch to make it work in 8.18 so the line numbers could be a little off.

The backtrace may be weird but the assert failure line is pretty clear.
Basically the todo at

(* XXX detect when a let can be nontac_expr *)
needs to be done so that the compiler force_nontac_expr works on all ltac2 syntactic values (ie possible values of ltac2 definitions).
Will handle next week.