From 5251da75285e1a53587c7ac2ed850e29003e93d8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 12 May 2023 17:17:54 +0200
Subject: [PATCH] [wp] script mode
---
src/plugins/wp/ProverScript.ml | 18 ++++++++++--------
src/plugins/wp/ProverScript.mli | 2 ++
src/plugins/wp/register.ml | 19 +++++++++++++++----
src/plugins/wp/wp_parameters.ml | 15 +++++++++++++++
src/plugins/wp/wp_parameters.mli | 1 +
5 files changed, 43 insertions(+), 12 deletions(-)
diff --git a/src/plugins/wp/ProverScript.ml b/src/plugins/wp/ProverScript.ml
index bb8daa671f0..e74b8f423fe 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 c93e5b7e867..e83c5e83dc8 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 306a38d81d3..4bfafe892e9 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 1d10e803ef8..4d6a6a21edc 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 7134a77ea95..53d15e5b023 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
--
GitLab