Commit 406f058e authored by Guillaume Melquiond's avatar Guillaume Melquiond

Keep track of "ITP" provers and avoid running such provers on unedited proofs.

When the user wants to write a Coq proof, she needs to run Coq on the goal,
wait five seconds for it to fail (it will fail, otherwise there is no point
in running Coq on this goal: another prover would have succeeded already),
and finally edit it. This is a waste of time. So goals run with an
interactive prover are now marked as unknown until their file is edited.

Interactive provers could have been detected by a nonempty "editor" string,
but there are interactive provers that don't have dedicated editors, and
there might be automated provers with dedicated user interfaces. So a new
field was added to prover descriptions.

TODO: actually run the editor when there is only one selected goal,
rather than keeping the current three-click method of editing proofs.
parent 841b97b2
......@@ -159,7 +159,8 @@ let detect_exec main data com =
version = ver;
command = c;
driver = Filename.concat (datadir main) data.prover_driver;
editor = data.prover_editor}
editor = data.prover_editor;
interactive = match data.kind with ITP -> true | ATP -> false; }
end
with Not_found ->
begin
......
......@@ -17,7 +17,7 @@
(* *)
(**************************************************************************)
(** Call provers and parse there outputs *)
(** Call provers and parse their outputs *)
type prover_answer =
| Valid
......
......@@ -54,6 +54,7 @@ type config_prover = {
driver : string; (* "/usr/local/share/why/drivers/ergo-spec.drv" *)
version : string; (* "v2.95" *)
editor : string;
interactive : bool;
}
type main = {
......@@ -159,6 +160,7 @@ let set_prover id prover family =
let section = set_string section "driver" prover.driver in
let section = set_string section "version" prover.version in
let section = set_string section "editor" prover.editor in
let section = set_bool section "interactive" prover.interactive in
(id,section)::family
let set_provers rc provers =
......@@ -174,6 +176,7 @@ let load_prover dirname provers (id,section) =
driver = absolute_filename dirname (get_string section "driver");
version = get_string ~default:"" section "version";
editor = get_string ~default:"" section "editor";
interactive = get_bool ~default:false section "interactive";
} provers
let load_main dirname section =
......
......@@ -87,7 +87,8 @@ type config_prover = {
command : string; (* "exec why-limit %t %m alt-ergo %f" *)
driver : string; (* "/usr/local/share/why/drivers/ergo-spec.drv" *)
version : string; (* "v2.95" *)
editor : string; (* Interative theorem prover *)
editor : string; (* Dedicated editor *)
interactive : bool; (* Interative theorem prover *)
}
val get_provers : config -> config_prover Mstr.t
......
......@@ -172,6 +172,7 @@ let save_config t =
driver = pr.Session.driver_name;
version = pr.Session.prover_version;
editor = pr.Session.editor;
interactive = pr.Session.interactive;
} acc in
let config = t.config in
let config = set_main config
......
......@@ -333,6 +333,7 @@ let clear model = model#clear ()
let image_of_result ~obsolete result =
match result with
| Session.Undone -> !image_undone
| Session.Unedited -> !image_unknown
| Session.Scheduled -> !image_scheduled
| Session.Running -> !image_running
| Session.Interrupted -> assert false
......@@ -400,6 +401,7 @@ let set_proof_state ~obsolete a =
let t = match res with
| Session.Done { Call_provers.pr_time = time } ->
Format.sprintf "%.2f" time
| Session.Unedited -> "not yet edited"
| _ -> ""
in
let t = if obsolete then t ^ " (obsolete)" else t in
......@@ -1533,8 +1535,9 @@ let select_row r =
let o =
match a.M.proof_state with
| Session.Undone -> "proof not yet scheduled for running"
| Session.Unedited -> "proof not yet edited"
| Session.Done r -> r.Call_provers.pr_output
| Session.Scheduled-> "proof scheduled by not running yet"
| Session.Scheduled-> "proof scheduled but not running yet"
| Session.Running -> "prover currently running"
| Session.Interrupted -> assert false
| Session.InternalFailure e ->
......
......@@ -33,6 +33,7 @@ type prover_data =
driver_name : string;
driver : Driver.driver;
mutable editor : string;
interactive : bool;
}
let get_prover_data env id pr acc =
......@@ -46,6 +47,7 @@ let get_prover_data env id pr acc =
driver_name = pr.Whyconf.driver;
driver = dr;
editor = pr.Whyconf.editor;
interactive = pr.Whyconf.interactive;
}
acc
with e ->
......@@ -100,7 +102,7 @@ type proof_attempt_status =
| Running (** external proof attempt is in progress *)
| Done of Call_provers.prover_result (** external proof done *)
| InternalFailure of exn (** external proof aborted by internal error *)
| Unedited (** interactive prover yet no proof script *)
(***************************)
(* main functor *)
......@@ -201,6 +203,9 @@ let verified t = t.verified
let goals t = t.goals
let theory_expanded t = t.theory_expanded
let running a = match a.proof_state with
| Scheduled | Running | Interrupted -> true
| Undone | Done _ | InternalFailure _ | Unedited -> false
let get_theory t =
match t.theory with
......@@ -283,6 +288,8 @@ let save_status fmt s =
match s with
| Undone | Scheduled | Running | Interrupted ->
fprintf fmt "<undone/>@\n"
| Unedited ->
fprintf fmt "<unedited/>@\n"
| InternalFailure msg ->
fprintf fmt "<internalfailure reason=\"%s\"/>@\n"
(Printexc.to_string msg)
......@@ -1333,6 +1340,7 @@ let load_result r =
Call_provers.pr_output = "";
}
| "undone" -> Undone
| "unedited" -> Unedited
| s ->
eprintf "[Warning] Session.load_result: unexpected element '%s'@." s;
Undone
......@@ -1517,16 +1525,15 @@ let save_session () =
let redo_external_proof ~timelimit g a =
(* check that the state is not Scheduled or Running *)
let previous_result,previous_obs = a.proof_state,a.proof_obsolete in
let running = match previous_result with
| Scheduled | Running | Interrupted -> true
| Done _ | Undone | InternalFailure _ -> false
in
if running then ()
if running a then ()
(* info_window `ERROR "Proof already in progress" *)
else
match a.prover with
| Undetected_prover _ -> ()
| Detected_prover p ->
if a.edited_as = "" && p.interactive then
set_proof_state ~obsolete:false a Unedited
else begin
let callback result =
match result with
| Interrupted ->
......@@ -1546,6 +1553,7 @@ let redo_external_proof ~timelimit g a =
?old ~command:p.command ~driver:p.driver
~callback
(get_task g)
end
let rec prover_on_goal ~timelimit p g =
let id = p.prover_id in
......@@ -1696,11 +1704,7 @@ let same_result r1 r2 =
let check_external_proof g a =
(* check that the state is not Scheduled or Running *)
let running = match a.proof_state with
| Scheduled | Running | Interrupted -> true
| Done _ | Undone | InternalFailure _ -> false
in
if running then ()
if running a then ()
else
begin
incr proofs_to_do;
......@@ -1714,7 +1718,7 @@ let check_external_proof g a =
let callback result =
match result with
| Scheduled | Running | Interrupted -> ()
| Undone -> assert false
| Undone | Unedited -> assert false
| InternalFailure msg ->
push_report g p_name (CallFailed msg);
incr proofs_done;
......@@ -1889,11 +1893,7 @@ let ft_of_pa a =
let edit_proof ~default_editor ~project_dir a =
(* check that the state is not Scheduled or Running *)
let running = match a.proof_state with
| Scheduled | Running | Interrupted -> true
| Undone | Done _ | InternalFailure _ -> false
in
if running then ()
if running a then ()
(*
info_window `ERROR "Edition already in progress"
*)
......@@ -1925,6 +1925,7 @@ let edit_proof ~default_editor ~project_dir a =
let file = name ^ "_" ^ (string_of_int !i) ^ ext in
let file = Sysutil.relativize_filename project_dir file in
a.edited_as <- file;
if a.proof_state = Unedited then a.proof_state <- Undone;
file
| f -> f
in
......
......@@ -31,6 +31,7 @@ type prover_data = private
driver_name : string;
driver : Driver.driver;
mutable editor : string;
interactive : bool;
}
(** record of necessary data for a given external prover *)
......@@ -61,6 +62,7 @@ type proof_attempt_status = private
| Running (** external proof attempt is in progress *)
| Done of Call_provers.prover_result (** external proof done *)
| InternalFailure of exn (** external proof aborted by internal error *)
| Unedited (** interactive prover yet no proof script *)
(** {2 Observers signature} *)
......
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