Jason Gross (Sep 08 2020 at 23:26): Jason Gross (Sep 08 2020 at 23:26):Between 8.10 and 8.11, Pfedit.build_by_tactic switched from correctly reporting Ltac errors to raising Not_found anomalies. Is this a known issue?
Jason Gross (Sep 08 2020 at 23:27):(I'll try to minimize an example to report as a bug.)
Emilio Jesús Gallego Arias (Sep 09 2020 at 13:30):If you do have a pointer to the code, or a backtrace with master [it should be much better] it would be very helpful
Emilio Jesús Gallego Arias (Sep 09 2020 at 13:30):that function is very very dubious tho
Emilio Jesús Gallego Arias (Sep 09 2020 at 13:30):it is very hard to use right, tho indeed that's likely unrelated to your problem at hand
Jason Gross (Sep 09 2020 at 14:08):The code is, e.g., https://github.com/mit-plv/rewriter/blob/258a24ba97af9a18b1e4f6cdb101e75c1092c4b6/src/Rewriter/Util/plugins/rewriter_build.ml.v813#L111 and if you want to see it for yourself, you can replace https://github.com/mit-plv/rewriter/blob/258a24ba97af9a18b1e4f6cdb101e75c1092c4b6/src/Rewriter/Rewriter/Examples.v#L11 with Make norules := Rewriter For () (extra idents (ex)). I'll try to make a small example
Emilio Jesús Gallego Arias (Sep 09 2020 at 14:14):@Jason Gross would be quick for you to get a backtrace
Emilio Jesús Gallego Arias (Sep 09 2020 at 14:14):indeed some rules related to how API works when accessing inductive that don't exist changed
Emilio Jesús Gallego Arias (Sep 09 2020 at 14:14):so the problem could be in the tactic
Jason Gross (Sep 09 2020 at 14:14):No, I'm not at a computer right now. When I'm at my computer in an hour or two, it'll be pretty quick
Emilio Jesús Gallego Arias (Sep 09 2020 at 14:15)::+1:
Jason Gross (Sep 09 2020 at 14:16):The issue might very well be that the error message from the tactic references an inductive that is defined earlier in the function, i.e., the inductive is no longer part of the environment when the error message is printed (assuming backtracking happens before error message printing)
Jason Gross (Sep 09 2020 at 17:40):@Emilio Jesús Gallego Arias Here's a backtrace from V8.11.1, I'll work on getting one from master shortly:
Error: Anomaly "Uncaught exception Not_found."
Please report at http://coq.inria.fr/bugs/.
frame @ file "toplevel/coqloop.ml", line 404, characters 6-31
frame @ file "toplevel/coqloop.ml", line 475, characters 14-38
frame @ file "lib/cErrors.ml", line 115, characters 2-34
frame @ file "lib/cErrors.ml", line 107, characters 4-69
frame @ file "clib/cList.ml", line 361, characters 10-13
frame @ file "plugins/ltac/tactic_debug.ml", line 429, characters 23-54
frame @ file "plugins/ltac/tactic_debug.ml", line 405, characters 21-55
frame @ file "plugins/ltac/tactic_debug.ml", line 387, characters 11-32
frame @ file "lib/pp.ml", line 253, characters 14-29
frame @ file "list.ml", line 82, characters 32-39
frame @ file "list.ml", line 82, characters 32-39
frame @ file "list.ml", line 82, characters 32-39
frame @ file "list.ml", line 82, characters 32-39
frame @ file "list.ml", line 82, characters 32-39
frame @ file "list.ml", line 82, characters 20-23
frame @ file "lib/pp.ml", line 272, characters 31-68
frame @ file "lib/pp.ml", line 253, characters 14-29
frame @ file "list.ml", line 82, characters 32-39
frame @ file "list.ml", line 82, characters 32-39
frame @ file "list.ml", line 82, characters 20-23
frame @ file "printing/printer.ml", line 107, characters 35-82
frame @ file "printing/proof_diffs.ml", line 255, characters 37-94
frame @ file "interp/constrextern.ml", line 826, characters 71-95
frame @ file "interp/constrextern.ml", line 281, characters 35-62
frame @ file "library/nametab.ml", line 550, characters 17-65
frame @ file "clib/hMap.ml", line 361, characters 12-28
raise @ file "clib/int.ml", line 39, characters 14-29
So, uh, in Coq master (cdfe69d6da6b32338ba74c9f599c74389089c9dd), Coq doesn't anomaly, it just dies. Things work fine with coqc, but if I pass the file in to coqtop, then, only when I've set Ltac Backtrace, I get
Fatal error: exception Not_found
Raised at file "clib/int.ml", line 39, characters 14-29
Called from file "clib/hMap.ml", line 365, characters 12-28
Called from file "library/nametab.ml", line 550, characters 17-64
Called from file "interp/constrextern.ml" (inlined), line 310, characters 35-62
Called from file "interp/constrextern.ml", line 936, characters 4-31
Called from file "interp/constrextern.ml", line 952, characters 71-95
Called from file "printing/proof_diffs.ml", line 253, characters 37-96
Called from file "printing/printer.ml" (inlined), line 84, characters 35-82
Called from file "plugins/ltac/tactic_debug.ml", line 387, characters 41-89
Called from file "list.ml", line 82, characters 20-23
Called from file "list.ml", line 82, characters 32-39
Called from file "list.ml", line 82, characters 32-39
Called from file "lib/pp.ml", line 249, characters 14-29
Called from file "lib/pp.ml" (inlined), line 268, characters 31-68
Called from file "plugins/ltac/tactic_debug.ml", line 380, characters 12-452
Called from file "list.ml", line 82, characters 20-23
Called from file "list.ml", line 82, characters 32-39
Called from file "list.ml", line 82, characters 32-39
Called from file "list.ml", line 82, characters 32-39
Called from file "list.ml", line 82, characters 32-39
Called from file "list.ml", line 82, characters 32-39
Called from file "lib/pp.ml", line 249, characters 14-29
Called from file "plugins/ltac/tactic_debug.ml", line 400, characters 11-32
Called from file "plugins/ltac/tactic_debug.ml", line 418, characters 21-55
Called from file "plugins/ltac/tactic_debug.ml", line 442, characters 23-54
Called from file "clib/cList.ml", line 361, characters 10-13
Called from file "lib/cErrors.ml", line 107, characters 4-69
Called from file "lib/cErrors.ml", line 121, characters 2-34
Called from file "toplevel/coqloop.ml", line 489, characters 14-38
Called from file "toplevel/coqloop.ml", line 501, characters 20-43
Called from file "toplevel/coqloop.ml", line 524, characters 27-45
Called from file "topbin/coqtop_bin.ml", line 16, characters 10-35
@Emilio Jesús Gallego Arias what do you make of this?
Jason Gross (Sep 09 2020 at 22:25):Oh, and it looks like I perhaps already have an issue for this: https://github.com/coq/coq/issues/12297
Emilio Jesús Gallego Arias (Sep 10 2020 at 15:51):Indeed that's the printer dying
Last updated: Apr 20 2024 at 03:40 UTC