I just fixed a typo in one of my tactics that made the tactic fail under
repeat despite otherwise working fine. Here's a minimal example. I would love to understand what is going on here. The typo was that the handler for
throw) was outside of
once instead of inside. (I assume the resulting behaviour is as intended.. I just don't understand it.)
From Ltac2 Require Import Ltac2 Control. Ltac2 what (_ : unit) := once (fun _ => plus (fun _ => ())) throw. (* Control.throw is not given to `plus` directly but to `once` instead *) Goal True. what (). (* works fine *) repeat (what ()). (* Error: Failed to progress. *)
I think once is useless here because it's applied to a value.
Sorry, forget about it, I can't read.
plus (fun _ => ()) has a single success returning a function of type
(exn -> unit) -> unit. So your
what is equivalent to
plus (fun _ => ()) throw. Your call to
repeat (what ()) is effectively equivalent to
try (progress what) (perhaps more accurately,
plus (fun _ => once (progress what); repeat (what ())) (fun _ => ()) which in this case is equivalent to
plus (fun _ => progress what) (fun _ => ())) because
repeat stops when the tactic fails to make progress. However,
throw is not caught by
zero for a failure that is caught by
try), so the "Failed to progress" exception is the exception which causes backtracking into
what and thus the exception passed to
plus, this is the error message you see at top level.
I guess this is a very belated explanation @Janno , but I only saw this now, and am reading Coq users to delay working on finishing editing my dissertation. Incidentally @Pierre-Marie Pédrot , is there a chance we can get backtraces in Ltac2 similar to the OCaml backtraces we get in Coq on
Last updated: Jan 29 2023 at 01:02 UTC