Commit 92ec2022 authored by MARCHE Claude's avatar MARCHE Claude

Replayer: capture case of missing proof script

parent 37da1e08
......@@ -90,16 +90,18 @@ https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990
== New Features to announce ==
* Coq realizations
* Coq tactic
* tool why3session, including commands latex, html, stats
* tool why3doc
* Support for several versions of the same prover, for prover upgrade
* Coq realizations. See manual Chapter xx
* Coq tactic. See manual Chapter xx
* tool why3session, including commands latex, html, stats. See manual Section xx
* tool why3doc. See manual Section xx
* Support for several versions of the same prover, for prover upgrade.
See manual Section xx
* Improved IDE:
- left scrollbar + selection of shown or hidden provers
- font enlargement
- left scrollbar, selection of shown or hidden provers, font enlargement
- integration of the support for prover upgrade
- support for selection of alternate editors
* Complete support for limiting provers' memory usage
* Improved support of Microsoft Windows OS
* what else ?
* see also the file CHANGES
......@@ -118,8 +120,8 @@ https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990
- add tag 0.72 to the git repository (do not forget to push it)
* put on the web page
- why3-0.72.tar.gz
- standard library online, using why3doc
- API doc, produced using ocamldoc, to http://why3.lri.fr/api/
- standard library online, using why3doc (make stdlibdoc)
- API doc, produced using ocamldoc (make apidoc), to http://why3.lri.fr/api/
Note: check that URL of API doc is correct in doc/api.tex line 9.
- update the main HTML page (sources are in why3-papers/www)
- add links to extra resources like
......
......@@ -289,7 +289,9 @@ let print_report (g,p,t,r) =
printf "no former result available, new result is: %a@." print_result new_res
| M.CallFailed msg ->
printf "internal failure '%a'@." Exn_printer.exn_printer msg;
| M.Prover_not_installed ->
| M.Edited_file_absent f ->
printf "proof script absent (%s)@." f
| M.Prover_not_installed ->
printf "not installed@."
......
......@@ -618,6 +618,7 @@ type report =
| Result of Call_provers.prover_result * Call_provers.prover_result
| CallFailed of exn
| Prover_not_installed
| Edited_file_absent of string
| No_former_result of Call_provers.prover_result
module Todo = struct
......@@ -649,6 +650,8 @@ end
let push_report report (g,p,t,r) =
report := (g.goal_name,p,t,r)::!report
exception NoFile of string
(** When no smoke *)
let check_external_proof eS eT todo a =
let g = a.proof_parent in
......@@ -666,36 +669,23 @@ let check_external_proof eS eT todo a =
*)
Todo._done todo (g,a.proof_prover,0,Prover_not_installed);
| Some(ap,npc,a) ->
(*
let ap = a.proof_prover in
match find_loadable_prover eS ap with
| None ->
dprintf debug "[sched] prover not found : %a@."
Whyconf.print_prover ap;
Todo._done todo (g,ap,0,Prover_not_installed)
(* set_proof_state ~notify ~obsolete:false a Undone *)
| Some (nap,npc) ->
let g = a.proof_parent in
try
if nap == ap then raise Not_found;
let np_a = PHprover.find g.goal_external_proofs nap in
if O.replace_prover np_a a then begin
(** The notification will be done by the new proof_attempt *)
O.remove np_a.proof_key;
raise Not_found end
with Not_found ->
(** replace [a] by a new_proof attempt if [a.proof_prover] was not
loadable *)
let a = if nap == ap then a
else
let a = copy_external_proof
~notify ~keygen:O.create ~prover:nap ~env_session:eS a in
O.init a.proof_key (Proof_attempt a);
a in
*)
let timelimit = adapt_timelimit a in
let memlimit = a.proof_memlimit in
let callback result =
let old =
match a.proof_edited_as with
| None -> None
| Some edited_as ->
let f = Filename.concat eS.session.session_dir edited_as in
if Sys.file_exists f then
begin
(* Format.eprintf "Info: proving using edited file %s@." f; *)
(Some (open_in f))
end
else
raise (NoFile f)
in
let timelimit = adapt_timelimit a in
let memlimit = a.proof_memlimit in
let callback result =
match result with
| Undone Scheduled | Undone Running | Undone Interrupted -> ()
| Undone (Unedited | JustEdited) -> assert false
......@@ -715,24 +705,18 @@ let check_external_proof eS eT todo a =
end;
set_proof_state ~notify ~obsolete:false ~archived:false
result a
in
let old =
match a.proof_edited_as with
| None -> None
| Some edited_as ->
let f = Filename.concat eS.session.session_dir edited_as in
(* Format.eprintf "Info: proving using edited file %s@." f; *)
(Some (open_in f))
in
let command =
String.concat " " (npc.prover_config.Whyconf.command ::
npc.prover_config.Whyconf.extra_options) in
schedule_proof_attempt eT
~timelimit ~memlimit
?old ~command
~driver:npc.prover_driver
~callback
(goal_task g)
in
let command =
String.concat " " (npc.prover_config.Whyconf.command ::
npc.prover_config.Whyconf.extra_options) in
schedule_proof_attempt eT
~timelimit ~memlimit
?old ~command
~driver:npc.prover_driver
~callback
(goal_task g)
with NoFile f ->
Todo._done todo (g,a.proof_prover,0,Edited_file_absent f);
end
let check_goal_and_children eS eT todo g =
......
......@@ -208,6 +208,7 @@ module Make(O: OBSERVER) : sig
(** Result(new_result,old_result) *)
| CallFailed of exn
| Prover_not_installed
| Edited_file_absent of string
| No_former_result of Call_provers.prover_result
val replay :
......@@ -264,6 +265,6 @@ end
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. bin/why3ide.byte"
compile-command: "unset LANG; make -C ../.. byte"
End:
*)
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment