diff --git a/src/command.ml b/src/command.ml
index 415fadee833000ea5be9c04e64a73db40adafd05..400a0447514d1252cc240a595150f9438f901382 100644
--- a/src/command.ml
+++ b/src/command.ml
@@ -359,6 +359,8 @@ let () = register ~name:"config" ~args:"[OPTIONS] PROVERS"
let velocity = ref false in
let default = ref false in
let detect = ref false in
+ let check = ref false in
+ let retval = ref 0 in
Arg.parse_argv argv
begin
Wenv.options () @
@@ -370,6 +372,8 @@ let () = register ~name:"config" ~args:"[OPTIONS] PROVERS"
"--reset", Arg.Set Wenv.reset, "configure from scratch";
"--default", Arg.Set default, "import local provers";
"--detect", Arg.Set detect, "detect and import local provers";
+ "--check", Arg.Set check,
+ "check that the proof certificates respect the configuration"
]
end
noargv
@@ -423,6 +427,22 @@ let () = register ~name:"config" ~args:"[OPTIONS] PROVERS"
let tactics = Wenv.tactics () in
(* --- Drivers ----- *)
let drivers = Wenv.drivers () in
+ (* --- Check ----- *)
+ if !check then
+ begin
+ let rec check_crc crc =
+ match crc.Crc.state with
+ | Stuck -> ()
+ | Prover (p, _) ->
+ if Prover.check_and_get_prover env ~patterns p = None then
+ retval := 1;
+ | Tactic { children; _ } -> List.iter check_crc children in
+ let check f =
+ let _, theories = Prove.load_proofs f in
+ Prove.M.(iter (fun _ -> iter (fun _ -> check_crc))) theories
+ in
+ Wenv.allfiles ~exts:[".mlw"] check "."
+ end ;
(* --- Printing -------------- *)
if !list then
begin
@@ -453,6 +473,7 @@ let () = register ~name:"config" ~args:"[OPTIONS] PROVERS"
Wenv.set_drivers drivers ;
end ;
Wenv.save () ;
+ exit (!retval)
end
(* -------------------------------------------------------------------------- *)
@@ -776,7 +797,7 @@ let () = register ~name:"install" ~args:"PKG PATH..."
src pkg ;
allsrc := false ;
Wenv.allfiles ~exts:[".mlw"] (install ~kind:"(source)") src ;
- let proofs = Filename.(concat (chop_extension src) "proof.json") in
+ let proofs = Prove.proofs_file src in
if Sys.file_exists proofs then
install ~kind:"(proof)" proofs ;
end in
diff --git a/src/docref.ml b/src/docref.ml
index 780c6d389f833dc7a6b078279e42de024533f727..4fb01e891c1420e6e3945b0cbbe1f29a12f6df31 100644
--- a/src/docref.ml
+++ b/src/docref.ml
@@ -214,16 +214,6 @@ let iter_theory cenv ~depend ~cloned thy =
(* --- Proofs --- *)
(* -------------------------------------------------------------------------- *)
-let jmap cc js =
- let m = ref Mstr.empty in
- Json.jiter (fun fd js -> m := Mstr.add fd (cc js) !m) js ; !m
-
-let load_proofs file =
- let js = if Sys.file_exists file then Json.of_file file else `Null in
- let profile = Calibration.of_json @@ Json.jfield "profile" js in
- let strategy = jmap (jmap Crc.of_json) @@ Json.jfield "proofs" js in
- profile , strategy
-
let zip_goals theory proofs =
let proofs = Mstr.find_def Mstr.empty (Session.thy_name theory) proofs in
List.fold_left
@@ -264,7 +254,6 @@ let parse ~wenv ~cenv ~henv file =
Log.error "invalid file name: %S" file ;
exit 2
end ;
- let dir = Filename.chop_extension file in
let lib = library_path file in
let path = String.concat "." lib in
let thys =
@@ -273,7 +262,7 @@ let parse ~wenv ~cenv ~henv file =
Log.error "%s" (Printexc.to_string exn) ;
exit 1
in
- let profile, proofs = load_proofs (Filename.concat dir "proof.json") in
+ let profile, proofs = Prove.load_proofs file in
let theories =
Mstr.mapi
(fun id (theory : Thy.theory) ->
diff --git a/src/hammer.ml b/src/hammer.ml
index eef873be12ce12dbb8ef2429a8180a06d25245e6..06cd099f399a33cb8c3c6d99437394a72ebd1a0b 100644
--- a/src/hammer.ml
+++ b/src/hammer.ml
@@ -176,26 +176,11 @@ let hammer henv =
(* --- Node Processing --- *)
(* -------------------------------------------------------------------------- *)
-let get_prover h pr =
- let prmatch pattern =
- try Prover.pmatch ~pattern pr with
- | Prover.InvalidPattern _ -> false in
- let prover = try Some (Prover.prover h.env pr) with Not_found -> None in
- if List.exists prmatch h.patterns
- then prover (* either the prover is available or we already complained *)
- else
- begin
- if prover = None then
- Log.warning "prover %a not found (why3)" Prover.pp_desc pr;
- Log.warning "prover %a not configured (project)" Prover.pp_desc pr;
- None
- end
-
let overhead t = max (t *. 2.0) 1.0
let replay h p t =
let client = if t > h.time *. 0.2 then h.client else None in
- match get_prover h p with
+ match Prover.check_and_get_prover h.env ~patterns:h.patterns p with
| None -> stuck
| Some p -> prove h.env ?client p (overhead t)
diff --git a/src/prove.ml b/src/prove.ml
index 3ff5daf707e70fa3e83b65e074c22cb991e1fd7b..3e338556e7604cc5de406d3d6877f9364e403ef8 100644
--- a/src/prove.ml
+++ b/src/prove.ml
@@ -62,14 +62,19 @@ let jproofs (prfs : proofs) : Json.t =
`Assoc (List.map (fun (g,r) -> g, Crc.to_json r) rs)
) prfs)
-let load_proofs file : profile * theories =
+let proofs_file file =
+ Filename.concat (Filename.chop_extension file) "proof.json"
+
+let load_proofs ?defaultprofile file : profile * theories =
+ let file = proofs_file file in
let js = if Sys.file_exists file then Json.of_file file else `Null in
- let default = Calibration.default () in
- let profile = Calibration.of_json ~default @@ Json.jfield "profile" js in
+ let profile =
+ Calibration.of_json ?default:defaultprofile @@ Json.jfield "profile" js in
let strategy = jmap (jmap Crc.of_json) @@ Json.jfield "proofs" js in
profile , strategy
let save_proofs ~mode dir file profile (prfs : proofs) =
+ let file = proofs_file file in
match mode with
| `Replay -> ()
| `Minimize | `Update | `Force ->
@@ -311,8 +316,8 @@ let process ~env ~mode ~session ~(log:results) ~axioms ~unsuccess file =
if Filename.is_relative file then dir else Filename.basename dir in
let theories, format = load_theories env file in
let session = Session.create ~session ~dir ~file ~format theories in
- let fp = Filename.concat dir "proof.json" in
- let profile, strategy = load_proofs fp in
+ let profile, strategy =
+ load_proofs ~defaultprofile:(Calibration.default ()) file in
let context = match log with `Context n -> n | _ -> (-1) in
let* proofs =
Fibers.all @@ List.map
@@ -320,7 +325,7 @@ let process ~env ~mode ~session ~(log:results) ~axioms ~unsuccess file =
(Session.theories session)
in
Session.save session ;
- save_proofs ~mode dir fp profile proofs ;
+ save_proofs ~mode dir file profile proofs ;
let henv =
if axioms then
Some (Axioms.init env)
diff --git a/src/prove.mli b/src/prove.mli
index dd4475452bccf26f3d0fa9960a4c308b1b684702..8458ccf8e2c9d138782dab86f7ab948e0d56e0db 100644
--- a/src/prove.mli
+++ b/src/prove.mli
@@ -21,6 +21,17 @@
(* --- Proof Manager --- *)
(* -------------------------------------------------------------------------- *)
+module M = Why3.Wstdlib.Mstr
+
+type profile = Calibration.profile
+type theories = Crc.crc M.t M.t
+
+val proofs_file : string -> string
+(** Returns the proofs file associated with the given mlw file *)
+
+val load_proofs : ?defaultprofile:profile -> string -> profile * theories
+(** Load the content of the proofs file associated with the given mlw file *)
+
type mode = [ `Force | `Update | `Minimize | `Replay ]
type log = [
`Default | `Modules | `Theories | `Goals | `Proofs | `Context of int
diff --git a/src/prover.ml b/src/prover.ml
index 78af5a1552a234adf72c4dd73d017be87850fc90..7c2d22471050ff4d53975969218358860967a520 100644
--- a/src/prover.ml
+++ b/src/prover.ml
@@ -162,3 +162,18 @@ let select env ~patterns =
| InvalidPattern s -> Log.warning "invalid prover pattern %s" s; None
| Not_found -> Log.warning "prover %s not found (why3)" pattern; None in
List.filter_map find patterns
+
+let check_and_get_prover env ~patterns pr =
+ let prmatch pattern =
+ try pmatch ~pattern pr with
+ | InvalidPattern _ -> false in
+ let prover = try Some (prover env pr) with Not_found -> None in
+ if List.exists prmatch patterns
+ then prover (* either the prover is available or we already complained *)
+ else
+ begin
+ if prover = None then
+ Log.warning "prover %a not found (why3)" pp_desc pr;
+ Log.warning "prover %a not configured (project)" pp_desc pr;
+ None
+ end
diff --git a/src/prover.mli b/src/prover.mli
index e9dd9987b4ac585d28ebf1e0eb13204fc1e6eeae..3e1332f53ea72c295b8e21642da1774893874662 100644
--- a/src/prover.mli
+++ b/src/prover.mli
@@ -99,3 +99,9 @@ val select : Wenv.env -> patterns:string list -> prover list
val default : Wenv.env -> prover list
(** Returns the set of available "default" provers *)
+
+val check_and_get_prover : Wenv.env -> patterns:string list -> prover_desc
+ -> prover option
+(** Returns the prover if available and selected by the [patterns]. Warn if
+ the prover is not found. We assume the [patterns] have been [select]ed so
+ we don't warn if an unavailable prover match the [patterns] *)
diff --git a/tests/command.t b/tests/command.t
index c9da4d10ef5652c2e625926db5e88a1946a16778..986f8b0a5ab3b5ba078f04e30f92a879c0b34d87 100644
--- a/tests/command.t
+++ b/tests/command.t
@@ -202,6 +202,7 @@
--reset configure from scratch
--default import local provers
--detect detect and import local provers
+ --check check that the proof certificates respect the configuration
-help Display this list of options
--help Display this list of options
diff --git a/tests/nonexisting_provers.t/run.t b/tests/nonexisting_provers.t/run.t
index ce09cf45d4f53ed3d77940babce0248991825c5f..dea1dbfc09af64c5b086492e8439d326ae51d923 100644
--- a/tests/nonexisting_provers.t/run.t
+++ b/tests/nonexisting_provers.t/run.t
@@ -41,3 +41,21 @@
Error: 1 unproved file
Emitted 5 warnings, 1 error
[1]
+
+ $ why3find config --check
+ Warning: prover foo not found (why3)
+ Warning: prover bar not found (why3)
+ Warning: prover non-existing@1.0 not found (why3)
+ Warning: prover non-existing@1.0 not configured (project)
+ Warning: prover alt-ergo@2.4.2 not configured (project)
+ Configuration:
+ - runner: 2 jobs, 1.0s
+ - tactics: split_vc (depth 4)
+ Summary:
+ Warning: prover foo not found (why3)
+ Warning: prover bar not found (why3)
+ Warning: prover non-existing@1.0 not found (why3)
+ Warning: prover non-existing@1.0 not configured (project)
+ Warning: prover alt-ergo@2.4.2 not configured (project)
+ Emitted 5 warnings
+ [1]