fix reentrancy of tactic mode (fix #372)

Changelog.md

@@ -1,6 +1,6 @@
 # Changelog
 
-## [1.15.1] - XX-07-2022
+## [1.15.1] - 16-07-2022
 
 Requires Elpi 1.16.5 and Coq 8.16.
 
@@ -10,6 +10,7 @@ Requires Elpi 1.16.5 and Coq 8.16.
     refresh universes. This is useful to keep a link between
     a universe declaration and the declaration itself but still
     elaborate it
+  - Fix Coq-Elpi is reentrant when commands call tactics
 
 ## [1.15.0] - 13-07-2022
 

src/coq_elpi_builtins.ml

@@ -100,16 +100,20 @@ let pr_econstr_env options env sigma t =
       if options.hoas_holes = Some Heuristic then aux () expr else expr in
     Ppconstr.pr_constr_expr_n env sigma options.pplevel expr)
 
-let tactic_mode = ref false
+let tactic_mode = State.declare ~name:"coq-elpi:tactic-mode"
+  ~pp:(fun fmt x -> Format.fprintf fmt "%b" x)
+  ~init:(fun () -> false)
+  ~start:(fun x -> x)
+
 let on_global_state api thunk = (); (fun state ->
-  if !tactic_mode then
+  if State.get tactic_mode state then
     Coq_elpi_utils.err Pp.(strbrk ("API " ^ api ^ " cannot be used in tactics"));
   let state, result, gls = thunk state in
   Coq_elpi_HOAS.grab_global_env state, result, gls)
 
 (* This is for stuff that is not monotonic in the env, eg section closing *)
 let on_global_state_does_rewind_env api thunk = (); (fun state ->
-  if !tactic_mode then
+  if State.get tactic_mode state then
     Coq_elpi_utils.err Pp.(strbrk ("API " ^ api ^ " cannot be used in tactics"));
   let state, result, gls = thunk state in
   Coq_elpi_HOAS.grab_global_env_drop_univs state, result, gls)

src/coq_elpi_builtins.mli

@@ -24,6 +24,6 @@ type attribute_value =
 val attribute : (string * attribute_value) Conversion.t
 
 (* In tactic mode some APIs are disabled *)
-val tactic_mode : bool ref
+val tactic_mode : bool State.component
 
 val cache_tac_abbrev : qualified_name -> unit

src/coq_elpi_vernacular.ml

@@ -560,7 +560,7 @@ let run_static_check query =
   (* We turn a failure into a proper error in etc/coq-elpi_typechecker.elpi *)
   ignore (EC.static_check ~checker query)
 
-let run ~tactic_mode ~static_check program query =
+let run ~static_check program query =
   let t1 = Unix.gettimeofday () in
   let query =
     match query with
@@ -573,7 +573,6 @@ let run ~tactic_mode ~static_check program query =
   let leftovers = API.Setup.trace !trace_options in
   if leftovers <> [] then
     CErrors.user_err Pp.(str"Unknown trace options: " ++ prlist_with_sep spc str leftovers);
-  Coq_elpi_builtins.tactic_mode := tactic_mode;
   let exe = EC.optimize query in
   let t4 = Unix.gettimeofday () in
   let rc = API.Execute.once ~max_steps:!max_steps exe in
@@ -585,20 +584,20 @@ let run ~tactic_mode ~static_check program query =
   rc
 ;;
 
-let elpi_fails ~tactic_mode program_name =
+let elpi_fails program_name =
   let open Pp in
-  let kind = if tactic_mode then "tactic" else "command" in
+  let kind = "tactic/command" in
   let name = show_qualified_name program_name in
   CErrors.user_err (strbrk (String.concat " " [
     "The elpi"; kind; name ; "failed without giving a specific error message.";
     "Please report this inconvenience to the authors of the program."
   ]))
 
-let run_and_print ~tactic_mode ~print ~static_check program_name program_ast query_ast =
+let run_and_print ~print ~static_check program_name program_ast query_ast : unit =
   let open API.Data in let open Coq_elpi_utils in
-  match run ~tactic_mode ~static_check program_ast query_ast
+  match run ~static_check program_ast query_ast
   with
-  | API.Execute.Failure -> elpi_fails ~tactic_mode  program_name
+  | API.Execute.Failure -> elpi_fails program_name
   | API.Execute.NoMoreSteps ->
       CErrors.user_err Pp.(str "elpi run out of steps ("++int !max_steps++str")")
   | API.Execute.Success {
@@ -637,7 +636,7 @@ let run_in_program ?(program = current_program ()) (loc, query) =
   let elpi = ensure_initialized () in
   let program_ast, _ = get_and_compile program in
   let query_ast = `Ast (parse_goal ~elpi loc query) in
-  run_and_print ~tactic_mode:false ~print:true ~static_check:true program program_ast query_ast
+  run_and_print ~print:true ~static_check:true program program_ast query_ast
 ;;
 
 let typecheck_program ?(program = current_program ()) () =
@@ -691,8 +690,10 @@ let run_program loc name ~atts args =
       (Coq_elpi_arg_HOAS.in_elpi_cmd ~depth ~raw:raw_args Coq_elpi_HOAS.(mk_coq_context ~options:default_options state))
       state args in
     let state, q = atts2impl loc ~depth state atts (ET.mkApp mainc (EU.list_to_lp_list args) []) in
+    let state = API.State.set Coq_elpi_builtins.tactic_mode state false in
     state, (loc, q), gls in
-  run_and_print ~tactic_mode:false ~print:false ~static_check:false name program (`Fun query)
+
+  run_and_print ~print:false ~static_check:false name program (`Fun query)
 ;;
 
 let mk_trace_opts start stop preds =
@@ -746,7 +747,7 @@ let print name args =
       (EU.list_to_lp_list quotedP)
       [API.RawOpaqueData.of_string fname; EU.list_to_lp_list args] in
     state, (loc,q), [] in
-  run_and_print ~tactic_mode:false ~print:false ~static_check:false ["Elpi";"Print"] (compile ["Elpi";"Print"] [printer ()] []) (`Fun q)
+  run_and_print ~print:false ~static_check:false ["Elpi";"Print"] (compile ["Elpi";"Print"] [printer ()] []) (`Fun q)
 ;;
 
 open Tacticals
@@ -762,13 +763,14 @@ let run_tactic_common loc ?(static_check=false) program ~main ?(atts=[]) () =
       Coq_elpi_HOAS.goals2query sigma gls loc ~main
         ~in_elpi_tac_arg:Coq_elpi_arg_HOAS.in_elpi_tac ~depth state in
     let state, qatts = atts2impl loc ~depth state atts q in
+    let state = API.State.set Coq_elpi_builtins.tactic_mode state true in
     state, (loc, qatts), gls
     in
   let cprogram, _ = get_and_compile program in
-  match run ~tactic_mode:true ~static_check cprogram (`Fun query) with
+  match run ~static_check cprogram (`Fun query) with
   | API.Execute.Success solution -> Coq_elpi_HOAS.tclSOLUTION2EVD sigma solution
   | API.Execute.NoMoreSteps -> CErrors.user_err Pp.(str "elpi run out of steps")
-  | API.Execute.Failure -> elpi_fails ~tactic_mode:true program
+  | API.Execute.Failure -> elpi_fails program
   | exception (Coq_elpi_utils.LtacFail (level, msg)) -> tclFAILn level msg
 
 let run_tactic loc program ~atts _ist args =

tests/test_vernacular2.v

@@ -1,4 +1,4 @@
-From elpi Require Import test_vernacular1.
+From elpi Require Import elpi test_vernacular1.
 
 Elpi test.program1 "hello" x.
 Elpi test.program1 "hello" x y.
@@ -9,4 +9,42 @@ Elpi test.program1 "hello" x y.
 #[fwd_compat_attr] Elpi Export foo.
 #[fwd_compat_attr] Elpi Query lp:{{ true }}.
 #[fwd_compat_attr] Elpi foo.
-#[fwd_compat_attr] foo.
+#[fwd_compat_attr] foo.
+
+(* reentrance *)
+
+Elpi Command the_command.
+Elpi Accumulate lp:{{
+  pred mk-lem i:string.
+  mk-lem Name :- std.do! [
+    Lem = {{ (1 + 1 = 2)%nat }},
+    std.assert-ok! (coq.elaborate-skeleton Lem _ ELem) "failed",
+    std.assert-ok! (coq.typecheck {{ lp:Bo : lp:ELem }} _) "failed",
+    coq.ltac.collect-goals Bo [SealedGoal] [],
+    coq.ltac.open (coq.ltac.call "ltac1_that_calls_elpi" []) SealedGoal [],
+    % !tactic_mode should equal false here
+    coq.env.add-const Name Bo ELem @transparent! C_,
+  ].
+
+  main [str Name] :- std.do! [
+    mk-lem Name
+  ].
+}}.
+Elpi Typecheck.
+Elpi Export the_command.
+
+Elpi Tactic elpi_tac.
+Elpi Accumulate lp:{{
+  solve (goal _Ctx _ {{ (1 + 1 = lp:EX)%nat }} _ _) _ :- std.do! [
+    X = {{ 2%nat }},
+    std.assert-ok! (coq.elaborate-skeleton X _ EX) "failed",
+  ].
+  solve _ _ :- coq.ltac.fail _ "failed".
+}}.
+Elpi Typecheck.
+
+Ltac ltac1_that_calls_elpi :=
+  elpi elpi_tac;
+  reflexivity.
+
+the_command xx.