Commit 08b81e74 authored by François Bobot's avatar François Bobot

Add the property archived to proof_attempt.

If a proof_attempt is archived, it is not replayed nor set obsolete.
parent abb66e65
......@@ -396,7 +396,8 @@ let set_row_status row b =
else
goals_model#set ~row:row#iter ~column:status_column !image_unknown
let set_proof_state ~obsolete a =
let set_proof_state a =
let obsolete = a.S.proof_obsolete in
let row = a.S.proof_key in
let res = a.S.proof_state in
goals_model#set ~row:row#iter ~column:status_column
......@@ -414,6 +415,8 @@ let set_proof_state ~obsolete a =
Format.sprintf "[limit=%d.0]" a.S.proof_timelimit
in
let t = if obsolete then t ^ " (obsolete)" else t in
(* TODO find a better way to signal arhived row *)
let t = if a.S.proof_archived then t ^ " (archived)" else t in
goals_model#set ~row:row#iter ~column:time_column t
let model_index = Hashtbl.create 17
......@@ -512,7 +515,7 @@ let notify any =
| S.File file ->
set_row_status row file.S.file_verified
| S.Proof_attempt a ->
set_proof_state ~obsolete:a.S.proof_obsolete a
set_proof_state a
| S.Transf tr ->
set_row_status row tr.S.transf_verified
......@@ -710,6 +713,16 @@ let cancel_proofs () =
M.cancel a)
(get_selected_row_references ())
(*****************************************)
(* method: Set or unset the archive flag *)
(*****************************************)
let set_archive_proofs b () =
List.iter
(fun r ->
let a = get_any_from_row_reference r in
S.iter_proof_attempt (fun a -> M.set_archive a b) a)
(get_selected_row_references ())
(*****************************************************)
(* method: split selected goals *)
......@@ -1394,14 +1407,30 @@ let () =
~label:"Mark as obsolete"
~callback:cancel_proofs
() : GMenu.image_menu_item) in
let add_item_archived () =
ignore (tools_factory#add_image_item
~label:"Mark as archive"
~callback:(set_archive_proofs true)
() : GMenu.image_menu_item) in
let add_item_unarchived () =
ignore (tools_factory#add_image_item
~label:"Remove from archive"
~callback:(set_archive_proofs false)
() : GMenu.image_menu_item) in
add_refresh_provers add_separator "add sep in tools menu";
add_refresh_provers add_item_edit "add edit in tools menu";
add_refresh_provers add_item_replay "add replay in tools menu";
add_refresh_provers add_item_cancel "add cancel in tools menu";
add_refresh_provers add_item_archived "add archive in tools menu";
add_refresh_provers add_item_unarchived "add unarchive in tools menu";
add_separator ();
add_item_edit ();
add_item_replay ();
add_item_cancel ()
add_item_cancel ();
add_item_archived ();
add_item_unarchived ()
let () =
let b = GButton.button ~packing:tools_box#add ~label:"Edit" () in
......
......@@ -66,6 +66,7 @@ and 'a proof_attempt =
mutable proof_state : proof_attempt_status;
mutable proof_timelimit : int;
mutable proof_obsolete : bool;
mutable proof_archived : bool;
mutable proof_edited_as : string option;
}
......@@ -321,9 +322,10 @@ let opt lab fmt = function
let save_proof_attempt provers fmt _key a =
fprintf fmt
"@\n@[<v 1><proof@ prover=\"%i\"@ timelimit=\"%d\"@ %a\
obsolete=\"%b\">"
obsolete=\"%b\"@ archived=\"%b\">"
(Mprover.find a.proof_prover provers) a.proof_timelimit
(opt "edited") a.proof_edited_as a.proof_obsolete;
(opt "edited") a.proof_edited_as a.proof_obsolete
a.proof_archived;
save_status fmt a.proof_state;
fprintf fmt "@]@\n</proof>"
......@@ -510,13 +512,15 @@ type 'a keygen = ?parent:'a -> unit -> 'a
let add_external_proof
?(notify=notify)
~(keygen:'a keygen) ~obsolete ~timelimit ~edit (g:'a goal) p result =
~(keygen:'a keygen) ~obsolete
~archived ~timelimit ~edit (g:'a goal) p result =
assert (edit <> Some "");
let key = keygen ~parent:g.goal_key () in
let a = { proof_prover = p;
proof_parent = g;
proof_key = key;
proof_obsolete = obsolete;
proof_archived = archived;
proof_state = result;
proof_timelimit = timelimit;
proof_edited_as = edit;
......@@ -532,9 +536,10 @@ let remove_external_proof ?(notify=notify) a =
check_goal_proved notify g
let set_proof_state ?(notify=notify) ~obsolete res a =
let set_proof_state ?(notify=notify) ~obsolete ~archived res a =
a.proof_state <- res;
a.proof_obsolete <- obsolete;
a.proof_archived <- archived;
notify (Proof_attempt a);
check_goal_proved notify a.proof_parent
......@@ -542,6 +547,13 @@ let set_edited_as edited_as a = a.proof_edited_as <- edited_as
let set_timelimit timelimit a = a.proof_timelimit <- timelimit
let set_obsolete ?(notify=notify) a =
a.proof_obsolete <- true;
notify (Proof_attempt a);
check_goal_proved notify a.proof_parent
let set_archive a b = a.proof_archived <- b
(* [raw_add_goal parent name expl sum t] adds a goal to the given parent
DOES NOT record the new goal in its parent, thus this should not be exported
*)
......@@ -766,6 +778,7 @@ and load_proof_or_transf ~old_provers mg a =
let edit = load_option "edited" a in
let edit = match edit with None | Some "" -> None | _ -> edit in
let obsolete = bool_attribute "obsolete" a true in
let archived = bool_attribute "archived" a false in
let timelimit = int_attribute "timelimit" a (-1) in
if timelimit < 0 then begin
eprintf "[Error] incorrector unspecified timelimit '%i'@."
......@@ -774,7 +787,8 @@ and load_proof_or_transf ~old_provers mg a =
timelimit))
end;
let (_ : 'a proof_attempt) =
add_external_proof ~keygen ~obsolete ~timelimit ~edit mg p res
add_external_proof ~keygen ~archived ~obsolete
~timelimit ~edit mg p res
in
()
| "transf" ->
......@@ -1105,12 +1119,13 @@ let ft_of_pa a =
But since it will be perhaps removed...
*)
let copy_external_proof
?notify ~keygen ?obsolete ?timelimit ?edit
?notify ~keygen ?obsolete ?archived ?timelimit ?edit
?goal ?prover ?attempt_status ?env_session ?session a =
let session = match env_session with
| Some eS -> Some eS.session
| _ -> session in
let obsolete = default_option a.proof_obsolete obsolete in
let archived = default_option a.proof_archived archived in
let timelimit = default_option a.proof_timelimit timelimit in
let pas = default_option a.proof_state attempt_status in
let ngoal = default_option a.proof_parent goal in
......@@ -1158,7 +1173,7 @@ let copy_external_proof
Some (dst_file)
in
add_external_proof ?notify ~keygen
~obsolete ~timelimit ~edit ngoal nprover pas
~obsolete ~archived ~timelimit ~edit ngoal nprover pas
exception UnloadableProver of Whyconf.prover
......@@ -1180,6 +1195,7 @@ let update_edit_external_proof env_session a =
set_edited_as (Some file) a;
if a.proof_state = Undone Unedited
then set_proof_state ~notify ~obsolete:a.proof_obsolete
~archived:a.proof_archived
(Undone Interrupted) a;
file
| Some f -> f
......@@ -1210,11 +1226,12 @@ let print_attempt_status fmt = function
| InternalFailure _ -> pp_print_string fmt "Failure"
let print_external_proof fmt p =
fprintf fmt "%a - %a (%i)%s%s"
fprintf fmt "%a - %a (%i)%s%s%s"
Whyconf.print_prover p.proof_prover
print_attempt_status p.proof_state
p.proof_timelimit
(if p.proof_obsolete then " obsolete" else "")
(if p.proof_archived then " archived" else "")
(if p.proof_edited_as <> None then " edited" else "")
(***********************************************************)
......@@ -1540,6 +1557,7 @@ let merge_proof ~keygen obsolete to_goal _ from_proof =
ignore
(add_external_proof ~keygen
~obsolete:(obsolete || from_proof.proof_obsolete)
~archived:from_proof.proof_archived
~timelimit:from_proof.proof_timelimit
~edit:from_proof.proof_edited_as
to_goal
......@@ -1566,7 +1584,8 @@ and merge_trans ~keygen env to_goal _ from_transf =
from_transf_name to_goal goals in
List.iter2 (fun (_,_,_,_,_,from_goal,obsolete) to_goal ->
match from_goal with
| Some from_goal -> merge_any_goal ~keygen env obsolete from_goal to_goal
| Some from_goal -> merge_any_goal ~keygen env obsolete
from_goal to_goal
| None -> ()) goals transf.transf_goals
exception OutdatedSession
......
......@@ -83,6 +83,7 @@ and 'a proof_attempt = private
mutable proof_state : proof_attempt_status;
mutable proof_timelimit : int;
mutable proof_obsolete : bool;
mutable proof_archived : bool;
mutable proof_edited_as : string option;
}
......@@ -255,6 +256,7 @@ val add_external_proof :
?notify:'key notify ->
keygen:'key keygen ->
obsolete:bool ->
archived:bool ->
timelimit:int ->
edit:string option ->
'key goal ->
......@@ -267,9 +269,14 @@ val remove_external_proof : ?notify:'key notify -> 'key proof_attempt -> unit
val set_proof_state :
?notify:'key notify ->
obsolete:bool ->
archived:bool ->
proof_attempt_status ->
'key proof_attempt -> unit
val set_obsolete : ?notify:'key notify -> 'key proof_attempt -> unit
val set_archive : 'key proof_attempt -> bool -> unit
val set_edited_as : string option -> 'key proof_attempt -> unit
val update_edit_external_proof :
......@@ -284,6 +291,7 @@ val copy_external_proof :
?notify:'key notify ->
keygen:'key keygen ->
?obsolete:bool ->
?archived:bool ->
?timelimit:int ->
?edit:string option ->
?goal:'key goal ->
......
......@@ -335,14 +335,14 @@ let rec find_loadable_prover eS prover =
let redo_external_proof eS eT ?timelimit a =
let timelimit = match timelimit with
| None -> Whyconf.timelimit (Whyconf.get_main eS.whyconf)
| Some t -> t in
(* check that the state is not Scheduled or Running *)
let previous_result,previous_obs = a.proof_state,a.proof_obsolete in
if running a then ()
(* info_window `ERROR "Proof already in progress" *)
if a.proof_archived || running a then ()
else
let timelimit = match timelimit with
| None -> Whyconf.timelimit (Whyconf.get_main eS.whyconf)
| Some t -> t in
(* check that the state is not Scheduled or Running *)
let previous_result,previous_obs = a.proof_state,a.proof_obsolete in
(* info_window `ERROR "Proof already in progress" *)
let ap = a.proof_prover in
match find_loadable_prover eS a.proof_prover with
| None -> Debug.dprintf debug
......@@ -369,15 +369,17 @@ loaded@."
a in
if a.proof_edited_as = None &&
npc.prover_config.Whyconf.interactive then
set_proof_state ~notify ~obsolete:false (Undone Unedited) a
set_proof_state ~notify ~obsolete:false ~archived:false
(Undone Unedited) a
else begin
let callback result =
match result with
| Undone Interrupted ->
set_proof_state ~notify
~obsolete:previous_obs previous_result a
~obsolete:previous_obs ~archived:false previous_result a
| _ ->
set_proof_state ~notify ~obsolete:false result a;
set_proof_state ~notify ~obsolete:false
~archived:false result a;
in
let old =
match a.proof_edited_as with
......@@ -401,7 +403,8 @@ let rec prover_on_goal eS eT ~timelimit p g =
let a =
try PHprover.find g.goal_external_proofs p
with Not_found ->
let ep = add_external_proof ~keygen:O.create ~obsolete:false ~timelimit
let ep = add_external_proof ~keygen:O.create ~obsolete:false
~archived:false ~timelimit
~edit:None g p (Undone Interrupted) in
O.init ep.proof_key (Proof_attempt ep);
ep
......@@ -508,10 +511,16 @@ let replay eS eT ~obsolete_only ~context_unproved_goals_only a =
(* method: mark proofs as obsolete *)
(***********************************)
let cancel_proof a = set_proof_state ~notify ~obsolete:true a.proof_state a
let cancel_proof a =
if not a.proof_archived then
set_obsolete ~notify a
let cancel = iter_proof_attempt cancel_proof
(** Set or unset archive *)
let set_archive a b = set_archive a b; notify (Proof_attempt a)
(*********************************)
(* method: check existing proofs *)
(*********************************)
......@@ -557,7 +566,7 @@ let check_external_proof eS eT todo a =
dprintf debug "[Sched] Check external proof : %a@."
(fun fmt g -> pp_print_string fmt g.goal_name.Ident.id_string) g;
(* check that the state is not Scheduled or Running *)
if running a then ()
if a.proof_archived || running a then ()
else
begin
Todo.todo todo;
......@@ -592,7 +601,8 @@ let check_external_proof eS eT todo a =
| Undone Unedited -> assert false
| InternalFailure msg ->
Todo._done todo (g,ap,(CallFailed msg));
set_proof_state ~notify ~obsolete:false result a
set_proof_state ~notify ~obsolete:false ~archived:false
result a
| Done new_res ->
begin
match a.proof_state with
......@@ -601,7 +611,8 @@ let check_external_proof eS eT todo a =
| _ ->
Todo._done todo (g,ap,No_former_result new_res)
end;
set_proof_state ~notify ~obsolete:false result a
set_proof_state ~notify ~obsolete:false ~archived:false
result a
in
let old =
match a.proof_edited_as with
......@@ -698,7 +709,7 @@ let rec transform eS sched ~context_unproved_goals_only tr a =
let edit_proof eS sched ~default_editor a =
(* check that the state is not Scheduled or Running *)
if running a then ()
if a.proof_archived || running a then ()
(*
info_window `ERROR "Edition already in progress"
*)
......@@ -730,9 +741,11 @@ let edit_proof eS sched ~default_editor a =
let callback res =
match res with
| Done _ ->
set_proof_state ~notify ~obsolete:true old_res a
set_proof_state ~notify ~obsolete:true ~archived:false
old_res a
| _ ->
set_proof_state ~notify ~obsolete:false res a
set_proof_state ~notify ~obsolete:false ~archived:false
res a
in
let editor =
match npc.prover_config.Whyconf.editor with
......
......@@ -154,6 +154,8 @@ module Make(O: OBSERVER) : sig
val remove_transformation : O.key transf -> unit
val set_archive : O.key proof_attempt -> bool -> unit
val clean : O.key any -> unit
(** [clean a] removes failed attempts below [a] where
there at least one successful attempt or transformation *)
......
......@@ -51,14 +51,7 @@ let convert_unknown_prover ?(remove_converted=false) ~keygen env_session =
(** If such a prover already exists we add nothing *)
if not (PHprover.mem pr.proof_parent.goal_external_proofs pk) then
converted := true;
ignore (add_external_proof
~keygen
~obsolete:pr.proof_obsolete
~timelimit:pr.proof_timelimit
~edit:pr.proof_edited_as
pr.proof_parent
pk
pr.proof_state)
ignore (copy_external_proof ~keygen ~prover:pk pr)
) pks;
(** pks = [] (!converted = false) also for the one which are known *)
if remove_converted && !converted then Session.remove_external_proof pr
......@@ -88,9 +81,8 @@ let transform_proof_attempt ?notify ~keygen env_session tr_name =
add_registered_transformation ~keygen env_session tr_name g in
let add_pa sg =
if not (PHprover.mem sg.goal_external_proofs pr.proof_prover) then
ignore (add_external_proof ~keygen ~obsolete:pr.proof_obsolete
~timelimit:pr.proof_timelimit ~edit:pr.proof_edited_as
sg pr.proof_prover (Undone Interrupted)) in
ignore (copy_external_proof ~keygen ~goal:sg
~attempt_status:(Undone Interrupted) pr) in
List.iter add_pa tr.transf_goals in
let proofs = all_proof_attempts env_session.session in
List.iter replace proofs
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