I have this bit of code here in a tactic that I am exposing as an external Ltac2 tactic (although I suspect Ltac2 might be unrelated to my question). As far as I can tell,
enter_one should either run the provided continuation or raise an exception. However, the code finishes successfully and it prints
start0. What am I missing?
Feedback.msg_debug (Pp.str "start0"); Proofview.Goal.enter_one (fun goal -> raise Not_found)
Where I have
raise Not_found now I used to have a bunch of code which ran fine but eventually I needed access to the current goal's environment so I added
Proofview.Goal.enter_one and the code stopped being executed.
can we get some code context?
if you put a feedback in the fun does it print?
I'll try to extract some context.
No, nothing in the continuation is executed.
let define_prim5' name r0 r1 r2 r3 r4 lift f = let tac x y z u v = lift (f (Tac2ffi.repr_to r0 x) (Tac2ffi.repr_to r1 y) (Tac2ffi.repr_to r2 z) (Tac2ffi.repr_to r3 u) (Tac2ffi.repr_to r4 v)) in Tac2env.define_primitive (pname name) (mk_closure (arity_suc (arity_suc (arity_suc (arity_suc arity_one)))) tac) let () = let open Tac2ffi in define_prim5' "main" (array constr) (array constr) classes_repr dbs_repr (bool) results_to_ltac2 main let results_to_ltac2 res = Proofview.tclUNIT (Tac2ffi.of_unit ()) let main prems concls cls dbs dbg = Feedback.msg_debug (Pp.str "start0"); Proofview.Goal.enter_one (fun goal -> raise Not_found)
If I replace
Proofview.Goal.enter_one by other code (more prints,
tclUNIT, etc.) everything is executed just fine.
Proofview.Goal.enter_one (fun goal -> raise Not_found);
does ocaml not warn you on this line?
Oh, sorry, the
; is not part of the current code.
is this code in reverse order? the later functions seem unbound in the let ()
Oh, right, I assembled things incorrectly. The actual code is the other way around
It seems this problem is not limited to
enter_one. The following also only prints
Feedback.msg_debug (Pp.str "start0"); let open Proofview.Notations in Proofview.tclEVARMAP >>= fun sigma -> Feedback.msg_debug (Pp.str "start1"); Proofview.Goal.enter_one (fun goal -> raise Not_found)
while still succeeding.
If I remove the
tclEVARMAP step I see both
I guess I should make a minimal example that can be compiled without my custom Ltac2 data types
wait a bit
the results_to_ltac2 / lift usage is wrong
Oh, of course :face_palm:
Thanks! I would have never thought of that.
Janno has marked this topic as resolved.
Last updated: Dec 07 2023 at 14:02 UTC