Assertion failed in `force_nontac_expr`
Closed this issue · 1 comments
Janno commented
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.
SkySkimmer commented
The backtrace may be weird but the assert failure line is pretty clear.
Basically the todo at
coq-ltac2-compiler/src/tac2compile.ml
Line 543 in 886c17f
force_nontac_expr
works on all ltac2 syntactic values (ie possible values of ltac2 definitions).Will handle next week.