Stream: Coq devs & plugin devs

Topic: ✔ Proofview.Goal.enter_one not triggering

Janno (Feb 23 2022 at 10:26):

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)

Janno (Feb 23 2022 at 10:29):

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.

Gaëtan Gilbert (Feb 23 2022 at 10:31):

can we get some code context?

Gaëtan Gilbert (Feb 23 2022 at 10:32):

if you put a feedback in the fun does it print?

Janno (Feb 23 2022 at 10:32):

I'll try to extract some context.

Janno (Feb 23 2022 at 10:32):

No, nothing in the continuation is executed.

Janno (Feb 23 2022 at 10:34):

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)

Janno (Feb 23 2022 at 10:35):

If I replace Proofview.Goal.enter_one by other code (more prints, tclUNIT, etc.) everything is executed just fine.

Gaëtan Gilbert (Feb 23 2022 at 10:35):

Proofview.Goal.enter_one (fun goal -> raise Not_found);

does ocaml not warn you on this line?

Janno (Feb 23 2022 at 10:36):

No

Gaëtan Gilbert (Feb 23 2022 at 10:36):

(warning 10)

Janno (Feb 23 2022 at 10:36):

Oh, sorry, the ; is not part of the current code.

Gaëtan Gilbert (Feb 23 2022 at 10:37):

is this code in reverse order? the later functions seem unbound in the let ()

Janno (Feb 23 2022 at 10:38):

Oh, right, I assembled things incorrectly. The actual code is the other way around

Janno (Feb 23 2022 at 10:38):

It seems this problem is not limited to enter_one. The following also only prints start0:

  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.

Janno (Feb 23 2022 at 10:39):

If I remove the tclEVARMAP step I see both start0 and start1.

Janno (Feb 23 2022 at 10:42):

I guess I should make a minimal example that can be compiled without my custom Ltac2 data types

Gaëtan Gilbert (Feb 23 2022 at 10:43):

wait a bit

Gaëtan Gilbert (Feb 23 2022 at 10:44):

the results_to_ltac2 / lift usage is wrong

Janno (Feb 23 2022 at 10:44):

Oh, of course :face_palm:

Janno (Feb 23 2022 at 10:46):

Thanks! I would have never thought of that.

Notification Bot (Feb 23 2022 at 10:47):

Janno has marked this topic as resolved.

Last updated: Sep 09 2024 at 05:02 UTC