diff --git a/src/plugins/wp/ProverScript.ml b/src/plugins/wp/ProverScript.ml
index bb8daa671f0645d85cf2c71bc14e4fe343a3db62..e74b8f423fefe24fb4791be868260b2aad27c7a6 100644
--- a/src/plugins/wp/ProverScript.ml
+++ b/src/plugins/wp/ProverScript.ml
@@ -504,7 +504,7 @@ let rec process env node =
let task
~valid ~failed ~provers
- ~depth ~width ~backtrack ~auto
+ ~depth ~width ~backtrack ~auto ~scratch
~start ~progress ~result ~success wpo =
begin fun () ->
Wp_parameters.debug ~dkey:dkey_pp_allgoals "%a" Wpo.pp_goal_flow wpo ;
@@ -513,8 +513,10 @@ let task
then
( success wpo (Some VCS.Qed) ; Task.return ())
else
- let json = ProofSession.load wpo in
- let script = Priority.sort (ProofScript.decode json) in
+ let script =
+ if scratch then [] else
+ Priority.sort @@ ProofScript.decode @@ ProofSession.load wpo
+ in
let tree = ProofEngine.proof ~main:wpo in
let env = Env.make tree
~valid ~failed ~provers
@@ -529,7 +531,7 @@ let task
(* -------------------------------------------------------------------------- *)
type 'a process =
- ?valid:bool -> ?failed:bool -> ?provers:VCS.prover list ->
+ ?valid:bool -> ?failed:bool -> ?scratch:bool -> ?provers:VCS.prover list ->
?depth:int -> ?width:int -> ?backtrack:int ->
?auto:Strategy.heuristic list ->
?start:(Wpo.t -> unit) ->
@@ -543,23 +545,23 @@ let skip2 _ _ = ()
let skip3 _ _ _ = ()
let prove
- ?(valid = true) ?(failed = true) ?(provers = [])
+ ?(valid = true) ?(failed = true) ?(scratch = false) ?(provers = [])
?(depth = 0) ?(width = 0) ?(backtrack = 0) ?(auto = [])
?(start = skip1) ?(progress = skip2) ?(result = skip3) ?(success = skip2)
wpo =
Task.todo (task
~valid ~failed ~provers
- ~depth ~width ~backtrack ~auto
+ ~depth ~width ~backtrack ~auto ~scratch
~start ~progress ~result ~success wpo)
let spawn
- ?(valid = true) ?(failed = true) ?(provers = [])
+ ?(valid = true) ?(failed = true) ?(scratch = false) ?(provers = [])
?(depth = 0) ?(width = 0) ?(backtrack = 0) ?(auto = [])
?(start = skip1) ?(progress = skip2) ?(result = skip3) ?(success = skip2)
wpo =
schedule (task
~valid ~failed ~provers
- ~depth ~width ~backtrack ~auto
+ ~depth ~width ~backtrack ~auto ~scratch
~start ~progress ~result ~success wpo)
let search
diff --git a/src/plugins/wp/ProverScript.mli b/src/plugins/wp/ProverScript.mli
index c93e5b7e867c916f14c2abf980e88665cd3d84c6..e83c5e83dc87cc7f9c84d22137fa35a7fef2661e 100644
--- a/src/plugins/wp/ProverScript.mli
+++ b/src/plugins/wp/ProverScript.mli
@@ -24,6 +24,7 @@ open VCS
(** - [valid]: Play provers with valid result (default: true)
- [failed]: Play provers with invalid result (default: true)
+ - [scratch]: Discard existing script (default: false)
- [provers]: Additional list of provers to {i try} when stuck
- [depth]: Strategy search depth (default: 0)
- [width]: Strategy search width (default: 0)
@@ -33,6 +34,7 @@ open VCS
type 'a process =
?valid:bool ->
?failed:bool ->
+ ?scratch:bool ->
?provers:prover list ->
?depth:int ->
?width:int ->
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 306a38d81d30d28187dbcdc22107a678eccf196c..4bfafe892e9d8cbee8969a13f22501366314f0e8 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -482,8 +482,9 @@ let do_list_scheduled_result () =
type script = {
mutable tactical : bool ;
+ mutable scratch : bool ;
mutable update : bool ;
- mutable on_stdout : bool ;
+ mutable stdout : bool ;
mutable depth : int ;
mutable width : int ;
mutable backtrack : int ;
@@ -509,6 +510,7 @@ let spawn_wp_proofs ~script goals =
then
ProverScript.spawn
~failed:false
+ ~scratch:script.scratch
~auto:script.auto
~depth:script.depth
~width:script.width
@@ -566,7 +568,8 @@ let dump_strategies =
)))
let default_script_mode () = {
- tactical = false ; update=false ; on_stdout = false ; provers = [] ;
+ provers = [] ;
+ tactical = false ; update = false ; scratch = false ; stdout = false ;
depth=0 ; width = 0 ; auto=[] ; backtrack = 0 ;
}
@@ -649,7 +652,7 @@ let do_collect_session goals =
removed = !removed ; }
let do_update_session script session =
- let stdout = script.on_stdout in
+ let stdout = script.stdout in
List.iter
begin fun (g, _, s) ->
(* we always mark existing scripts *)
@@ -733,8 +736,16 @@ let do_wp_proofs ?provers ?tip (goals : Wpo.t Bag.t) =
script.tactical <- tip ;
script.update <- tip ;
end ;
+ begin match Wp_parameters.ScriptMode.get () with
+ | "default" -> ()
+ | "batch" -> script.update <- false
+ | "update" -> script.update <- true
+ | "init" -> script.scratch <- true
+ | "dry" -> script.scratch <- true ; script.update <- false
+ | opt -> Wp_parameters.error "Invalid -wp-script '%s' option" opt
+ end ;
begin
- script.on_stdout <- Wp_parameters.ScriptOnStdout.get ();
+ script.stdout <- Wp_parameters.ScriptOnStdout.get ();
end ;
let spawned = script.tactical || script.provers <> [] in
begin
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index 1d10e803ef806dcbd9307cbec4301e58a6800e45..4d6a6a21edca5670384cf485a789534e6ee63ba8 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -715,6 +715,21 @@ module Interactive = String
"
end)
+let () = Parameter_customize.set_group wp_prover
+module ScriptMode = String
+ (struct
+ let option_name = "-wp-script"
+ let arg_name = "mode"
+ let default = "default"
+ let help =
+ "WP mode for managing scripts and proof strategies:\n\
+ - 'batch': replay from existing scripts (default for script prover)\n\
+ - 'update': replay and update scripts (default for tip prover)\n\
+ - 'init': replay from scratch and save scripts\n\
+ - 'dry': replay from scratch, no script update\n\
+ "
+ end)
+
let () = Parameter_customize.set_group wp_prover
module StrategyEngine = True
(struct
diff --git a/src/plugins/wp/wp_parameters.mli b/src/plugins/wp/wp_parameters.mli
index 7134a77ea956179861b103ea52cbef3359ceb6c1..53d15e5b02311f7fd22328e247729ded1359ba4b 100644
--- a/src/plugins/wp/wp_parameters.mli
+++ b/src/plugins/wp/wp_parameters.mli
@@ -121,6 +121,7 @@ module DryFinalizeScripts: Parameter_sig.Bool
module Provers: Parameter_sig.String_list
module Interactive: Parameter_sig.String
module StrategyEngine: Parameter_sig.Bool
+module ScriptMode: Parameter_sig.String
module DefaultStrategies: Parameter_sig.String_list
module RunAllProvers: Parameter_sig.Bool
module Cache: Parameter_sig.String