Janno (Dec 18 2020 at 12:13): Janno (Dec 18 2020 at 12:13):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 plus (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.
Pierre-Marie Pédrot (Dec 18 2020 at 12:17):Sorry, forget about it, I can't read.
Jason Gross (Jan 01 2021 at 13:36):The tactic 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 try(you want 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 throw. Since throw escapes try and plus, this is the error message you see at top level.
Jason Gross (Jan 01 2021 at 13:37):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 -debug?
Last updated: Oct 13 2024 at 01:02 UTC