From c4852f5a0e14eb139e9fe1fe557302da3e1ac82b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Mon, 4 Dec 2023 14:29:02 +0100 Subject: [PATCH] Monad-thunk every nontrivial nontac_expr Fix #17 I am not fully sure that this is a compiler bug as the ~~~ocaml let l = List.map (fun f -> Proofview.tclIGNORE (thaw f)) l in ~~~ in the implementation of `dispatch` could also be blamed for not thunking properly (ie should be ~~~ocaml let l = List.map (fun f -> tclUNIT () >>= fun () -> tclIGNORE (thaw f)) l in ~~~ ) but it does seem hard or impossible to trigger a bug with non compiled ltac2. This change does cause some slowdown (bug_10107 goes from 0.04s to 0.06s, non compiled baseline being 0.25s) --- src/tac2compile.ml | 50 ++++++++++++------------- tests/Makefile.coq.local | 1 + tests/_CoqProject | 7 ++++ tests/compiler_bug_17.v | 21 +++++++++++ tests/src/META.compiler-bugs | 10 +++++ tests/src/compiler_bug_17.ml | 20 ++++++++++ tests/src/compiler_bug_17_plugin.mlpack | 1 + 7 files changed, 83 insertions(+), 27 deletions(-) create mode 100644 tests/Makefile.coq.local create mode 100644 tests/compiler_bug_17.v create mode 100644 tests/src/META.compiler-bugs create mode 100644 tests/src/compiler_bug_17.ml create mode 100644 tests/src/compiler_bug_17_plugin.mlpack diff --git a/src/tac2compile.ml b/src/tac2compile.ml index 0321695..c2bc6fc 100644 --- a/src/tac2compile.ml +++ b/src/tac2compile.ml @@ -747,8 +747,15 @@ let rec pp_nontac_expr = function (* produce a ocaml term of type valexpr tactic *) and pp_expr e = let { spilled_exprs = nonvals; head_expr = e; } = e in - if List.is_empty nonvals then pp_head_expr e - else surround (pp_binds Id.print pp_expr nonvals ++ pp_head_expr e) + let mainpp = + if List.is_empty nonvals then pp_head_expr e + else surround (pp_binds Id.print pp_expr nonvals ++ pp_head_expr e) + in + match e with + | Return _ | LetRec _ -> mainpp + | _ -> + (* monad-thunk nontrivial computations *) + surround (str "PV.tclUNIT () >>= fun () ->" ++ spc() ++ mainpp) and pp_head_expr = function | Return e -> surround (str "PV.tclUNIT" ++ spc() ++ pp_nontac_expr e) @@ -845,36 +852,25 @@ and pp_head_expr = function hv 0 (prlist pp_branch brs ++ str "end")) | CtorMut (i, es) -> - (* Not sure if we actually need to thunk this one but let's be safe. *) - hv 1 - (str "(PV.tclUNIT () >>= fun () ->" ++ spc() ++ - str "PV.tclUNIT" ++ spc() ++ + str "PV.tclUNIT" ++ spc() ++ + surround + (str "ValBlk" ++ spc() ++ surround - (str "ValBlk" ++ spc() ++ - surround - (int i ++ str "," ++ spc() ++ - hov 2 - (str "[|" ++ pp_val_list es ++ str "|]"))) ++ - str ")") + (int i ++ str "," ++ spc() ++ + hov 2 + (str "[|" ++ pp_val_list es ++ str "|]"))) | PrjMut (e, i) -> - (* Don't forget to delay the side effect with a thunk! *) - hv 1 - (str "(PV.tclUNIT () >>= fun () ->" ++ spc() ++ - str "PV.tclUNIT" ++ spc() ++ - surround - (str "Tac2ffi.Valexpr.field" ++ spc() ++ pp_nontac_expr e ++ spc() ++ int i) ++ - str ")") + str "PV.tclUNIT" ++ spc() ++ + surround + (str "Tac2ffi.Valexpr.field" ++ spc() ++ pp_nontac_expr e ++ spc() ++ int i) | Set (e1,i,e2) -> - (* Don't forget to delay the side effect with a thunk! *) - hv 1 - (str "(PV.tclUNIT () >>= fun () ->" ++ spc() ++ - h (str "let () = Tac2ffi.Valexpr.set_field" ++ spc() ++ - pp_nontac_expr e1 ++ spc() ++ int i ++ spc() ++ - pp_nontac_expr e2 ++ spc()) ++ - str "in" ++ spc() ++ - str "PV.tclUNIT (ValInt 0))") + h (str "let () = Tac2ffi.Valexpr.set_field" ++ spc() ++ + pp_nontac_expr e1 ++ spc() ++ int i ++ spc() ++ + pp_nontac_expr e2 ++ spc()) ++ + str "in" ++ spc() ++ + str "PV.tclUNIT (ValInt 0)" | Ext (ids, v) -> surround diff --git a/tests/Makefile.coq.local b/tests/Makefile.coq.local new file mode 100644 index 0000000..51cdd53 --- /dev/null +++ b/tests/Makefile.coq.local @@ -0,0 +1 @@ +CAMLPKGS:=-package coq-core.plugins.ltac2 diff --git a/tests/_CoqProject b/tests/_CoqProject index c0c2606..cf05b12 100644 --- a/tests/_CoqProject +++ b/tests/_CoqProject @@ -9,3 +9,10 @@ minibench.v compiler_bug_4.v compiler_bug_6.v compiler_bug_14.v +compiler_bug_17.v + +-I src + +src/META.compiler-bugs +src/compiler_bug_17.ml +src/compiler_bug_17_plugin.mlpack diff --git a/tests/compiler_bug_17.v b/tests/compiler_bug_17.v new file mode 100644 index 0000000..29a8367 --- /dev/null +++ b/tests/compiler_bug_17.v @@ -0,0 +1,21 @@ +From Ltac2 Require Import Ltac2 Printf. + +From Ltac2Compiler Require Import Ltac2Compiler. + +Declare ML Module "compiler-bugs.compiler_bug_17". + +Ltac2 @ external push : unit -> int := "compiler-bugs.compiler_bug_17" "push". +Ltac2 @ external pop : int -> unit := "compiler-bugs.compiler_bug_17" "pop". +Ltac2 @ external reset : unit -> unit := "compiler-bugs.compiler_bug_17" "reset". + +Ltac2 test2 () := + let outer := push () in + let inner := push () in + ltac1:(assert False) > + [pop inner; pop outer|let outer := push () in pop outer]. + +Ltac2 Compile test2. + +Goal True /\ True. + test2 (). +Abort. diff --git a/tests/src/META.compiler-bugs b/tests/src/META.compiler-bugs new file mode 100644 index 0000000..7b79016 --- /dev/null +++ b/tests/src/META.compiler-bugs @@ -0,0 +1,10 @@ +package "compiler_bug_17" ( + directory = "." + version = "dev" + requires = "coq-core.plugins.ltac2" + archive(byte) = "compiler_bug_17_plugin.cma" + archive(native) = "compiler_bug_17_plugin.cmxa" + plugin(byte) = "compiler_bug_17_plugin.cma" + plugin(native) = "compiler_bug_17_plugin.cmxs" +) +directory = "." diff --git a/tests/src/compiler_bug_17.ml b/tests/src/compiler_bug_17.ml new file mode 100644 index 0000000..6c35a91 --- /dev/null +++ b/tests/src/compiler_bug_17.ml @@ -0,0 +1,20 @@ +open Ltac2_plugin +open Tac2ffi +open Tac2expr +open Tac2externals + +let define s = define { mltac_plugin = "compiler-bugs.compiler_bug_17"; mltac_tactic = s } + +let state : int ref = Summary.ref ~name:"tac2compile_bug17" 0 +let push : unit -> int = fun () -> + state := 1 + !state; !state +let pop : int -> unit = fun i -> + if i == !state then + state := i - 1 + else + raise Not_found +let reset : unit -> unit = fun _ -> state := 0 + +let _ = define "push" (unit @-> ret int) push +let _ = define "pop" (int @-> ret unit) pop +let _ = define "reset" (unit @-> ret unit) reset diff --git a/tests/src/compiler_bug_17_plugin.mlpack b/tests/src/compiler_bug_17_plugin.mlpack new file mode 100644 index 0000000..319a0cf --- /dev/null +++ b/tests/src/compiler_bug_17_plugin.mlpack @@ -0,0 +1 @@ +Compiler_bug_17