From 52707ddc31693b3675371ed8042f6a99cbfc5e90 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 1 Oct 2020 17:32:23 +0200
Subject: [PATCH] [wp] added update and fixup modes
---
src/plugins/wp/GuiGoal.ml | 2 +-
src/plugins/wp/GuiNavigator.ml | 24 +++++++++---------
src/plugins/wp/ProverCoq.ml | 6 ++---
src/plugins/wp/ProverErgo.ml | 6 ++---
src/plugins/wp/ProverScript.ml | 2 +-
src/plugins/wp/ProverWhy3.ml | 46 ++++++++++++++++++++++------------
src/plugins/wp/VCS.ml | 26 +++++++++++--------
src/plugins/wp/VCS.mli | 18 +++++++------
src/plugins/wp/prover.ml | 2 +-
src/plugins/wp/register.ml | 4 +--
10 files changed, 79 insertions(+), 57 deletions(-)
diff --git a/src/plugins/wp/GuiGoal.ml b/src/plugins/wp/GuiGoal.ml
index 6444533328f..324803ba844 100644
--- a/src/plugins/wp/GuiGoal.ml
+++ b/src/plugins/wp/GuiGoal.ml
@@ -616,7 +616,7 @@ class pane (gprovers : GuiConfig.provers) =
VCS.pp_prover prv Wpo.pp_title wpo VCS.pp_result res
end
~success:(fun _ _ -> Wutil.later self#commit)
- ~pool (List.map (fun dp -> VCS.BatchMode , dp) provers)
+ ~pool (List.map (fun dp -> VCS.Batch , dp) provers)
method private fork proof fork =
Wutil.later
diff --git a/src/plugins/wp/GuiNavigator.ml b/src/plugins/wp/GuiNavigator.ml
index 48b88111f83..06cc23a28c4 100644
--- a/src/plugins/wp/GuiNavigator.ml
+++ b/src/plugins/wp/GuiNavigator.ml
@@ -251,7 +251,7 @@ class behavior
| VCS.Tactical ->
begin
match mode , ProverScript.get w with
- | (None | Some VCS.BatchMode) , `Script ->
+ | (None | Some VCS.Batch) , `Script ->
schedule (ProverScript.prove ~success w)
| _ ->
card#set `Goal ;
@@ -261,9 +261,9 @@ class behavior
| _ ->
let mode = match mode , prover with
| Some m , _ -> m
- | None , VCS.NativeCoq -> VCS.EditMode
- | None , VCS.NativeAltErgo -> VCS.FixMode
- | _ -> if VCS.is_auto prover then VCS.BatchMode else VCS.FixMode in
+ | None , VCS.NativeCoq -> VCS.Edit
+ | None , VCS.NativeAltErgo -> VCS.Fix
+ | _ -> if VCS.is_auto prover then VCS.Batch else VCS.Fix in
schedule (Prover.prove w ~mode ~result prover) ;
refresh w
end
@@ -325,17 +325,17 @@ class behavior
initializer
let open VCS in
begin
- popup_tip#add_item ~label:"Run Script" ~callback:(self#popup_run BatchMode) ;
- popup_tip#add_item ~label:"Edit Proof" ~callback:(self#popup_run EditMode) ;
+ popup_tip#add_item ~label:"Run Script" ~callback:(self#popup_run Batch) ;
+ popup_tip#add_item ~label:"Edit Proof" ~callback:(self#popup_run Edit) ;
popup_tip#add_item ~label:"Delete Script" ~callback:(self#popup_delete_script) ;
- popup_why3_auto#add_item ~label:"Run Prover" ~callback:(self#popup_run VCS.BatchMode) ;
- popup_why3_inter#add_item ~label:"Check Script" ~callback:(self#popup_run VCS.BatchMode) ;
- popup_why3_inter#add_item ~label:"Edit Script" ~callback:(self#popup_run VCS.EditMode) ;
- popup_why3_inter#add_item ~label:"Fixup Script" ~callback:(self#popup_run VCS.FixMode) ;
+ popup_why3_auto#add_item ~label:"Run Prover" ~callback:(self#popup_run VCS.Batch) ;
+ popup_why3_inter#add_item ~label:"Check Script" ~callback:(self#popup_run VCS.Batch) ;
+ popup_why3_inter#add_item ~label:"Edit Script" ~callback:(self#popup_run VCS.Edit) ;
+ popup_why3_inter#add_item ~label:"Fixup Script" ~callback:(self#popup_run VCS.FixUpdate) ;
self#add_popup_proofmodes popup_ergo
- [ "Run",BatchMode ; "Open Altgr-Ergo on Fail",EditMode ; "Open Altgr-Ergo",EditMode ] ;
+ [ "Run",Batch ; "Open Altgr-Ergo on Fail",Edit ; "Open Altgr-Ergo",Edit ] ;
self#add_popup_proofmodes popup_coq
- [ "Check Proof",BatchMode ; "Edit on Fail",EditMode ; "Edit Proof",EditMode ] ;
+ [ "Check Proof",Batch ; "Edit on Fail",Edit ; "Edit Proof",Edit ] ;
end
method private popup w p =
diff --git a/src/plugins/wp/ProverCoq.ml b/src/plugins/wp/ProverCoq.ml
index 1f3b14409a7..5bb7d9235d5 100644
--- a/src/plugins/wp/ProverCoq.ml
+++ b/src/plugins/wp/ProverCoq.ml
@@ -599,9 +599,9 @@ let prove_session ~mode w =
compile_headers w.cw_includes false w.cw_headers >>=
begin fun () ->
match mode with
- | BatchMode -> try_prove w
- | EditMode -> try_coqide w
- | FixMode ->
+ | Batch | Update -> try_prove w
+ | Edit -> try_coqide w
+ | Fix | FixUpdate ->
begin
try_prove w >>> function
| Task.Result true -> Task.return true
diff --git a/src/plugins/wp/ProverErgo.ml b/src/plugins/wp/ProverErgo.ml
index 0dc36e0245f..4813da2e3cd 100644
--- a/src/plugins/wp/ProverErgo.ml
+++ b/src/plugins/wp/ProverErgo.ml
@@ -455,11 +455,11 @@ let try_prove ~config ~pid ~gui ~file ~lines ~logout ~logerr =
let prove_file ~config ~pid ~mode ~file ~lines ~logout ~logerr =
let gui = match mode with
- | EditMode -> Lazy.force altergo_gui
- | BatchMode | FixMode -> false in
+ | Edit -> Lazy.force altergo_gui
+ | Batch | Update | Fix | FixUpdate -> false in
try_prove ~config ~pid ~gui ~file ~lines ~logout ~logerr >>= function
| { verdict=(VCS.Unknown|VCS.Timeout|VCS.Stepout) }
- when mode = FixMode && Lazy.force altergo_gui ->
+ when (mode = Fix || mode = FixUpdate) && Lazy.force altergo_gui ->
try_prove ~config ~pid ~gui:true ~file ~lines ~logout ~logerr
| r -> Task.return r
diff --git a/src/plugins/wp/ProverScript.ml b/src/plugins/wp/ProverScript.ml
index 50d39797232..2771afd2721 100644
--- a/src/plugins/wp/ProverScript.ml
+++ b/src/plugins/wp/ProverScript.ml
@@ -162,7 +162,7 @@ struct
| None -> ProofEngine.main env.tree
let prove env wpo ?config prover =
- Prover.prove wpo ?config ~mode:VCS.BatchMode
+ Prover.prove wpo ?config ~mode:VCS.Batch
~progress:env.progress prover
let backtracking env =
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index ec36e4a1235..f6fd227bee2 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -1276,22 +1276,25 @@ let scriptfile ~force ~ext wpo =
let dir = Wp_parameters.get_session_dir ~force "interactive" in
Format.sprintf "%s/%s%s" (dir :> string) wpo.Wpo.po_sid ext
+let updatescript ~script driver task =
+ let backup = script ^ ".bak" in
+ Sys.rename script backup ;
+ let old = open_in backup in
+ Command.pp_to_file script
+ (fun fmt ->
+ ignore @@ Why3.Driver.print_task_prepared ~old driver fmt task
+ );
+ close_in old ;
+ let d_old = Digest.file backup in
+ let d_new = Digest.file script in
+ if String.equal d_new d_old then Extlib.safe_remove backup
+
let editor ~script ~merge wpo pconf driver prover task =
Task.sync editor_mutex
begin fun () ->
Wp_parameters.feedback ~ontty:`Transient "Editing %S..." script ;
Cache.clear_result ~digest:(digest wpo driver) prover task ;
- if merge then
- begin
- let backup = script ^ ".bak" in
- Sys.rename script backup ;
- let old = open_in backup in
- Command.pp_to_file script
- (fun fmt ->
- ignore @@ Why3.Driver.print_task_prepared ~old driver fmt task
- );
- close_in old ;
- end ;
+ if merge then updatescript ~script driver task ;
let command = editor_command pconf in
let call = Why3.Call_provers.call_editor ~command script in
call_prover_task ~timeout:None ~steps:None pconf.prover call
@@ -1304,7 +1307,7 @@ let compile ~script ~timeout wpo pconf driver prover task =
let prepare ~mode wpo driver task =
let ext = Filename.extension (Why3.Driver.file_of_task driver "S" "T" task) in
- let force = mode <> VCS.BatchMode in
+ let force = mode <> VCS.Batch in
let script = scriptfile ~force wpo ~ext in
if Sys.file_exists script then Some (script, true) else
if force then
@@ -1324,16 +1327,27 @@ let interactive ~mode wpo pconf driver prover task =
| None -> Task.return VCS.unknown
| Some (script, merge) ->
match mode with
- | VCS.BatchMode ->
+ | VCS.Batch ->
compile ~script ~timeout wpo pconf driver prover task
- | VCS.EditMode ->
+ | VCS.Update ->
+ if merge then updatescript ~script driver task ;
+ compile ~script ~timeout wpo pconf driver prover task
+ | VCS.Edit ->
let open Task in
editor ~script ~merge wpo pconf driver prover task >>= fun _ ->
compile ~script ~timeout wpo pconf driver prover task
- | VCS.FixMode ->
+ | VCS.Fix ->
+ let open Task in
+ compile ~script ~timeout wpo pconf driver prover task >>= fun r ->
+ if VCS.is_valid r then return r else
+ editor ~script ~merge wpo pconf driver prover task >>= fun _ ->
+ compile ~script ~timeout wpo pconf driver prover task
+ | VCS.FixUpdate ->
let open Task in
+ if merge then updatescript ~script driver task ;
compile ~script ~timeout wpo pconf driver prover task >>= fun r ->
if VCS.is_valid r then return r else
+ let merge = false in
editor ~script ~merge wpo pconf driver prover task >>= fun _ ->
compile ~script ~timeout wpo pconf driver prover task
@@ -1345,7 +1359,7 @@ let is_trivial (t : Why3.Task.task) =
let goal = Why3.Task.task_goal_fmla t in
Why3.Term.t_equal goal Why3.Term.t_true
-let build_proof_task ?(mode=VCS.BatchMode) ?timeout ?steplimit ~prover wpo () =
+let build_proof_task ?(mode=VCS.Batch) ?timeout ?steplimit ~prover wpo () =
try
(* Always generate common task *)
let context = Wpo.get_context wpo in
diff --git a/src/plugins/wp/VCS.ml b/src/plugins/wp/VCS.ml
index 2b7862a000d..ffa0bccf1ca 100644
--- a/src/plugins/wp/VCS.ml
+++ b/src/plugins/wp/VCS.ml
@@ -34,9 +34,11 @@ type prover =
| Tactical (* Interactive Prover *)
type mode =
- | BatchMode (* Only check scripts *)
- | EditMode (* Edit then check scripts *)
- | FixMode (* Try check script, then edit script on non-success *)
+ | Batch (* Only check scripts *)
+ | Update (* Check and update scripts *)
+ | Edit (* Edit then check scripts *)
+ | Fix (* Try to check script, then edit script on non-success *)
+ | FixUpdate (* Update and fix *)
let parse_prover = function
| "" | "none" -> None
@@ -76,13 +78,15 @@ let parse_prover = function
let parse_mode m =
match String.lowercase_ascii m with
- | "fix" -> FixMode
- | "edit" -> EditMode
- | "batch" -> BatchMode
+ | "fix" -> Fix
+ | "edit" -> Edit
+ | "batch" -> Batch
+ | "update" -> Update
+ | "fixup" -> FixUpdate
| _ ->
Wp_parameters.error ~once:true
"Unrecognized mode %S (use 'batch' instead)" m ;
- BatchMode
+ Batch
let name_of_prover = function
| Why3 s -> Why3Provers.print_wp s
@@ -102,9 +106,11 @@ let title_of_prover = function
| Tactical -> "Script"
let title_of_mode = function
- | FixMode -> "Fix"
- | EditMode -> "Edit"
- | BatchMode -> "Batch"
+ | Fix -> "Fix"
+ | Edit -> "Edit"
+ | Batch -> "Batch"
+ | Update -> "Update"
+ | FixUpdate -> "Fix Update"
let sanitize_why3 s =
let buffer = Buffer.create 80 in
diff --git a/src/plugins/wp/VCS.mli b/src/plugins/wp/VCS.mli
index e43bb526177..270095ceaad 100644
--- a/src/plugins/wp/VCS.mli
+++ b/src/plugins/wp/VCS.mli
@@ -27,16 +27,18 @@
(** {2 Prover} *)
type prover =
- | Why3 of Why3Provers.t (* Prover via WHY *)
- | NativeAltErgo (* Direct Alt-Ergo *)
- | NativeCoq (* Direct Coq and Coqide *)
- | Qed (* Qed Solver *)
- | Tactical (* Interactive Prover *)
+ | Why3 of Why3Provers.t (** Prover via WHY *)
+ | NativeAltErgo (** Direct Alt-Ergo *)
+ | NativeCoq (** Direct Coq and Coqide *)
+ | Qed (** Qed Solver *)
+ | Tactical (** Interactive Prover *)
type mode =
- | BatchMode (* Only check scripts *)
- | EditMode (* Edit then check scripts *)
- | FixMode (* Try check script, then edit script on non-success *)
+ | Batch (** Only check scripts *)
+ | Update (** Check and update scripts *)
+ | Edit (** Edit then check scripts *)
+ | Fix (** Try check script, then edit script on non-success *)
+ | FixUpdate (** Update & Fix *)
module Pset : Set.S with type elt = prover
module Pmap : Map.S with type key = prover
diff --git a/src/plugins/wp/prover.ml b/src/plugins/wp/prover.ml
index 83b432ac6c2..45bd15f9cb4 100644
--- a/src/plugins/wp/prover.ml
+++ b/src/plugins/wp/prover.ml
@@ -59,7 +59,7 @@ let update ?result wpo prover res =
| None -> ()
| Some f -> f wpo prover res
-let run_prover wpo ?config ?(mode=BatchMode) ?progress ?result prover =
+let run_prover wpo ?config ?(mode=Batch) ?progress ?result prover =
signal ?progress wpo (VCS.name_of_prover prover) ;
dispatch ?config mode prover wpo >>>
fun status ->
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 74a692cf28f..c985100d700 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -615,7 +615,7 @@ let compute_provers ~mode ~script =
script.update <- true ;
prvs
| Some prover ->
- let pmode = if VCS.is_auto prover then VCS.BatchMode else mode in
+ let pmode = if VCS.is_auto prover then VCS.Batch else mode in
(pmode , prover) :: prvs
end (get_prover_names ()) []
@@ -720,7 +720,7 @@ let do_wp_proofs ?provers ?tip (goals : Wpo.t Bag.t) =
compute_provers ~mode ~script ;
compute_auto ~script ;
begin match provers with None -> () | Some prvs ->
- script.provers <- List.map (fun dp -> VCS.BatchMode , VCS.Why3 dp) prvs
+ script.provers <- List.map (fun dp -> VCS.Batch , VCS.Why3 dp) prvs
end ;
begin match tip with None -> () | Some tip ->
script.tactical <- tip ;
--
GitLab