diff --git a/src/ide/gmain.ml b/src/ide/gmain.ml index ee9ec61c5e085086ce98373cb0ddc35e38b8e920..1c8abe9953fde3e1086fe95249511d38939f21d0 100644 --- a/src/ide/gmain.ml +++ b/src/ide/gmain.ml @@ -432,11 +432,11 @@ let clear model = model#clear () let image_of_result ~obsolete result = match result with - | Session.Undone Session.Interrupted -> !image_undone - | Session.Undone Session.Unedited - | Session.Undone Session.JustEdited -> !image_unknown - | Session.Undone Session.Scheduled -> !image_scheduled - | Session.Undone Session.Running -> !image_running + | Session.Interrupted -> !image_undone + | Session.Unedited -> !image_editor + | Session.JustEdited -> !image_unknown + | Session.Scheduled -> !image_scheduled + | Session.Running -> !image_running | Session.InternalFailure _ -> !image_failure | Session.Done r -> match r.Call_provers.pr_answer with | Call_provers.Valid -> @@ -486,11 +486,11 @@ let set_proof_state a = Format.sprintf "%.2f [%d.0]" time a.S.proof_timelimit else Format.sprintf "%.2f" time - | S.Undone S.Unedited -> "(not yet edited)" - | S.Undone S.JustEdited -> "(edited)" + | S.Unedited -> "(not yet edited)" + | S.JustEdited -> "(edited)" | S.InternalFailure _ -> "(internal failure)" - | S.Undone S.Interrupted -> "(interrupted)" - | S.Undone (S.Scheduled | S.Running) -> + | S.Interrupted -> "(interrupted)" + | S.Scheduled | S.Running -> Format.sprintf "[limit=%d sec., %d M]" a.S.proof_timelimit a.S.proof_memlimit in @@ -576,17 +576,16 @@ let update_task_view a = | S.Proof_attempt a -> let o = match a.S.proof_state with - | S.Undone S.Interrupted -> - "proof not yet scheduled for running" - | S.Undone S.Unedited -> "Interactive proof, not yet edited. Edit with \"Edit\" button" - | S.Undone S.JustEdited -> "Edited interactive proof. Run it with \"Replay\" button" + | S.Interrupted -> "proof not yet scheduled for running" + | S.Unedited -> "Interactive proof, not yet edited. Edit with \"Edit\" button" + | S.JustEdited -> "Edited interactive proof. Run it with \"Replay\" button" | S.Done ({Call_provers.pr_answer = Call_provers.HighFailure} as r) -> let b = Buffer.create 37 in bprintf b "%a" Call_provers.print_prover_result r; Buffer.contents b | S.Done r -> r.Call_provers.pr_output - | S.Undone S.Scheduled-> "proof scheduled but not running yet" - | S.Undone S.Running -> "prover currently running" + | S.Scheduled-> "proof scheduled but not running yet" + | S.Running -> "prover currently running" | S.InternalFailure e -> let b = Buffer.create 37 in bprintf b "%a" Exn_printer.exn_printer e; @@ -955,10 +954,10 @@ let bisect_proof_attempt pa = let set_timelimit res = timelimit := 1 + (int_of_float (floor res.Call_provers.pr_time)) in let rec callback lp pa c = function - | S.Undone (S.Running | S.Scheduled) -> () - | S.Undone S.Interrupted -> + | S.Running | S.Scheduled -> () + | S.Interrupted -> dprintf debug "Bisecting interrupted.@." - | S.Undone (S.Unedited | S.JustEdited) -> assert false + | S.Unedited | S.JustEdited -> assert false | S.InternalFailure exn -> (** Perhaps the test can be considered false in this case? *) dprintf debug "Bisecting interrupted by an error %a.@." @@ -1005,10 +1004,10 @@ let bisect_proof_attempt pa = update the proof attempt *) let first_callback pa = function (** this pa can be different than the first pa *) - | S.Undone (S.Running | S.Scheduled) -> () - | S.Undone S.Interrupted -> + | S.Running | S.Scheduled -> () + | S.Interrupted -> dprintf debug "Bisecting interrupted.@." - | S.Undone (S.Unedited | S.JustEdited) -> assert false + | S.Unedited | S.JustEdited -> assert false | S.InternalFailure exn -> dprintf debug "proof of the initial task interrupted by an error %a.@." Exn_printer.exn_printer exn diff --git a/src/session/session.ml b/src/session/session.ml index 9ced44e0e1c3bcf76e88f9f60965a85149ea2859..63f1a683bac23f625646a089f300384c394a9723 100644 --- a/src/session/session.ml +++ b/src/session/session.ml @@ -41,15 +41,12 @@ let debug = Debug.register_info_flag "session" module PHstr = Util.Hstr -type undone_proof = +type proof_attempt_status = + | Unedited (** editor not yet run for interactive proof *) + | JustEdited (** edited but not run yet *) + | Interrupted (** external proof has never completed *) | Scheduled (** external proof attempt is scheduled *) - | Interrupted | Running (** external proof attempt is in progress *) - | Unedited - | JustEdited - -type proof_attempt_status = - | Undone of undone_proof | Done of Call_provers.prover_result (** external proof done *) | InternalFailure of exn (** external proof aborted by internal error *) @@ -491,9 +488,9 @@ let save_result fmt r = let save_status fmt s = match s with - | Undone Unedited -> + | Unedited -> fprintf fmt "@\n" - | Undone _ -> + | Scheduled | Running | Interrupted | JustEdited -> fprintf fmt "@\n" | InternalFailure msg -> fprintf fmt "@\n" @@ -1025,11 +1022,11 @@ let load_result r = Call_provers.pr_output = ""; Call_provers.pr_status = Unix.WEXITED 0 } - | "undone" -> Undone Interrupted - | "unedited" -> Undone Unedited + | "undone" -> Interrupted + | "unedited" -> Unedited | s -> eprintf "[Warning] Session.load_result: unexpected element '%s'@." s; - Undone Interrupted + Interrupted let load_option attr g = try Some (List.assoc attr g.Xml.attributes) @@ -1091,7 +1088,7 @@ and load_proof_or_transf ~old_provers mg a = in let res = match a.Xml.elements with | [r] -> load_result r - | [] -> Undone Interrupted + | [] -> Interrupted | _ -> eprintf "[Error] Too many result elements@."; raise (LoadError (a,"too many result elements")) @@ -1753,10 +1750,9 @@ let update_edit_external_proof env_session a = let file = Sysutil.uniquify file in let file = Sysutil.relativize_filename session_dir file in set_edited_as (Some file) a; - if a.proof_state = Undone Unedited + if a.proof_state = Unedited then set_proof_state ~notify ~obsolete:a.proof_obsolete - ~archived:a.proof_archived - (Undone Interrupted) a; + ~archived:a.proof_archived Interrupted a; file | Some f -> f in @@ -1781,7 +1777,12 @@ let update_edit_external_proof env_session a = file let print_attempt_status fmt = function - | Undone _ -> pp_print_string fmt "Undone" + | Scheduled | Running -> + pp_print_string fmt "Running" + | JustEdited | Interrupted -> + pp_print_string fmt "Not yet run" + | Unedited -> + pp_print_string fmt "Not yet edited" | Done pr -> Call_provers.print_prover_result fmt pr | InternalFailure _ -> pp_print_string fmt "Failure" diff --git a/src/session/session.mli b/src/session/session.mli index 8ba94845d198254368fb0080f3bd93b29257533d..9e0a618b724c0ff28aa487573041f4f2f506c3a5 100644 --- a/src/session/session.mli +++ b/src/session/session.mli @@ -35,18 +35,13 @@ module PHprover : Util.PrivateHashtbl with type key = Whyconf.prover (** {2 Proof attempts} *) -(** State of proof without result *) -type undone_proof = - | Scheduled (** external proof attempt is scheduled *) - | Interrupted (** external proof has been interrupted or - has never been scheduled*) - | Running (** external proof attempt is in progress *) - | Unedited (** unedited but editable *) - | JustEdited (** edited but not run yet *) - (** State of a proof *) type proof_attempt_status = - | Undone of undone_proof + | Unedited (** editor not yet run for interactive proof *) + | JustEdited (** edited but not run yet *) + | Interrupted (** external proof has never completed *) + | Scheduled (** external proof attempt is scheduled *) + | 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 *) diff --git a/src/session/session_scheduler.ml b/src/session/session_scheduler.ml index 25f70ff20354302f33ef0715ab6173ca662b435c..6e376f732703317290b67fcb9d4970e737d8a2ee 100644 --- a/src/session/session_scheduler.ml +++ b/src/session/session_scheduler.ml @@ -87,9 +87,9 @@ let goals t = t.theory_goals let theory_expanded t = t.theory_expanded *) -let running a = match a.proof_state with - | Undone (Scheduled | Running) -> true - | Undone (Unedited | JustEdited | Interrupted) +let running = function + | Scheduled | Running -> true + | Unedited | JustEdited | Interrupted | Done _ | InternalFailure _ -> false (*************************) @@ -170,7 +170,7 @@ let timeout_handler t = if List.length l < t.maximum_running_proofs then begin try let (callback,pre_call) = Queue.pop t.proof_attempts_queue in - callback (Undone Running); + callback Running; dprintf debug "[Sched] proof attempts started@."; let call = pre_call () in (Check_prover(callback,call))::l @@ -271,7 +271,7 @@ let cancel_scheduled_proofs t = match Queue.pop t.actions_queue with | Action_proof_attempt(_timelimit,_memlimit,_old,_inplace,_command, _driver,callback,_goal) -> - callback (Undone Interrupted) + callback Interrupted | Action_delayed _ as a-> Queue.push a new_queue done @@ -280,7 +280,7 @@ let cancel_scheduled_proofs t = try while true do let (callback,_) = Queue.pop t.proof_attempts_queue in - callback (Undone Interrupted) + callback Interrupted done with | Queue.Empty -> @@ -292,7 +292,7 @@ let schedule_proof_attempt ~timelimit ~memlimit ?old ~inplace dprintf debug "[Sched] Scheduling a new proof attempt (goal : %a)@." (fun fmt g -> Format.pp_print_string fmt (Task.task_goal g).Decl.pr_name.Ident.id_string) goal; - callback (Undone Scheduled); + callback Scheduled; Queue.push (Action_proof_attempt(timelimit,memlimit,old,inplace,command,driver, callback,goal)) @@ -305,7 +305,7 @@ let schedule_edition t command filename callback = Call_provers.call_on_file ~command ~regexps:[] ~timeregexps:[] ~exitcodes:[(0,Call_provers.Unknown "")] filename in - callback (Undone Running); + callback Running; t.running_proofs <- (Check_prover(callback, precall ())) :: t.running_proofs; run_timeout_handler t @@ -413,7 +413,7 @@ let adapt_timelimit a = let run_external_proof eS eT ?callback a = (* check that the state is not Scheduled or Running *) (* Perhaps this test, a.proof_archived, should be done somewhere else *) - if a.proof_archived || running a then () + if a.proof_archived || running a.proof_state then () else match find_prover eS a with | None -> @@ -457,7 +457,7 @@ let run_external_proof eS eT ?callback a = npc.prover_config.Whyconf.interactive then begin set_proof_state ~notify ~obsolete:false ~archived:false - (Undone Unedited) a; + Unedited a; Util.apply_option2 () callback a a.proof_state end else @@ -467,7 +467,7 @@ let run_external_proof eS eT ?callback a = let memlimit = a.proof_memlimit in let callback result = begin match result with - | Undone Interrupted -> + | Interrupted -> set_proof_state ~notify ~obsolete:previous_obs ~archived:false previous_result a | _ -> @@ -510,7 +510,7 @@ let prover_on_goal eS eT ?callback ~timelimit ~memlimit p g = with Not_found -> let ep = add_external_proof ~keygen:O.create ~obsolete:false ~archived:false ~timelimit ~memlimit - ~edit:None g p (Undone Interrupted) in + ~edit:None g p Interrupted in O.init ep.proof_key (Proof_attempt ep); ep in @@ -558,7 +558,7 @@ let run_prover eS eT ~context_unproved_goals_only ~timelimit ~memlimit pr a = let proof_successful_or_just_edited a = match a.proof_state with | Done { Call_provers.pr_answer = Call_provers.Valid } - | Undone JustEdited -> true + | JustEdited -> true | _ -> false let rec replay_on_goal_or_children eS eT @@ -674,7 +674,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 a.proof_archived || running a then () + if a.proof_archived || running a.proof_state then () else begin Todo.todo todo; @@ -704,8 +704,8 @@ let check_external_proof eS eT todo a = let memlimit = a.proof_memlimit in let callback result = match result with - | Undone Scheduled | Undone Running | Undone Interrupted -> () - | Undone (Unedited | JustEdited) -> assert false + | Scheduled | Running -> () + | Unedited | Interrupted | JustEdited -> assert false | InternalFailure msg -> Todo._done todo (g,ap,timelimit,(CallFailed msg)); set_proof_state ~notify ~obsolete:false ~archived:false @@ -758,12 +758,7 @@ let check_all eS eT ~callback = let rec play_on_goal_and_children eS eT ~timelimit ~memlimit todo l g = let callback _key status = - match status with - | Undone Running | Undone Scheduled -> () - | _ -> - Todo._done todo (); - (* eprintf "todo decreased to %d@." todo.Todo.todo *) - in + if not (running status) then Todo._done todo () in List.iter (fun p -> Todo.todo todo; @@ -868,7 +863,7 @@ let rec transform eS sched ~context_unproved_goals_only ?callback tr a = let edit_proof eS sched ~default_editor a = (* check that the state is not Scheduled or Running *) - if a.proof_archived || running a then () + if a.proof_archived || running a.proof_state then () (* info_window `ERROR "Edition already in progress" *) @@ -910,7 +905,7 @@ let edit_proof eS sched ~default_editor a = match res with | Done {Call_provers.pr_answer = Call_provers.Unknown ""} -> set_proof_state ~notify ~obsolete:true ~archived:false - (Undone JustEdited) a + JustEdited a | _ -> set_proof_state ~notify ~obsolete:false ~archived:false res a diff --git a/src/session/session_tools.ml b/src/session/session_tools.ml index a25f46e4e9d0471b8709160d3f05b49609fe1b8e..e08f4127fc77ce24908cd7acc8ec0943d0d38910 100644 --- a/src/session/session_tools.ml +++ b/src/session/session_tools.ml @@ -80,7 +80,7 @@ let transform_proof_attempt ?notify ~keygen env_session tr_name = let add_pa sg = if not (PHprover.mem sg.goal_external_proofs pr.proof_prover) then ignore (copy_external_proof ~keygen ~goal:sg - ~attempt_status:(Undone Interrupted) pr) + ~attempt_status:Interrupted pr) in List.iter add_pa tr.transf_goals in let proofs = all_proof_attempts env_session.session in diff --git a/src/why3session/why3session_html.ml b/src/why3session/why3session_html.ml index d98d78a83b69f132f8633d3df3d0c45af6f25cd1..23e46054e11139c502492d92e0195298f2f690b3 100644 --- a/src/why3session/why3session_html.ml +++ b/src/why3session/why3session_html.ml @@ -154,10 +154,13 @@ let print_results fmt provers proofs = | Call_provers.HighFailure -> fprintf fmt "FF8000\">High Failure" end - | S.Undone _ -> fprintf fmt "E0E0E0\">Undone" | S.InternalFailure _ -> fprintf fmt "E0E0E0\">Internal Failure" + | S.Interrupted -> fprintf fmt "E0E0E0\">Not yet run" + | S.Unedited -> fprintf fmt "E0E0E0\">Not yet edited" + | S.Scheduled | S.Running + | S.JustEdited -> assert false end; - if pr.S.proof_obsolete then fprintf fmt "(obsolete)" + if pr.S.proof_obsolete then fprintf fmt " (obsolete)" with Not_found -> fprintf fmt "E0E0E0\">---" end; fprintf fmt "") provers @@ -264,10 +267,12 @@ struct let print_prover = Whyconf.print_prover let print_proof_status fmt = function - | Undone _ -> fprintf fmt "Undone" - | Done pr -> fprintf fmt "Done : %a" Call_provers.print_prover_result pr + | Interrupted -> fprintf fmt "Not yet run" + | Unedited -> fprintf fmt "Not yet edited" + | JustEdited | Scheduled | Running -> assert false + | Done pr -> fprintf fmt "Done: %a" Call_provers.print_prover_result pr | InternalFailure exn -> - fprintf fmt "Failure : %a"Exn_printer.exn_printer exn + fprintf fmt "Failure: %a"Exn_printer.exn_printer exn let print_proof_attempt fmt pa = fprintf fmt "
  • %a : %a
  • " @@ -334,11 +339,13 @@ struct let print_prover = Whyconf.print_prover let print_proof_status fmt = function - | Undone _ -> fprintf fmt "Undone" - | Done pr -> fprintf fmt "Done : %a" + | Interrupted -> fprintf fmt "Not yet run" + | Unedited -> fprintf fmt "Not yet edited" + | JustEdited | Scheduled | Running -> assert false + | Done pr -> fprintf fmt "Done: %a" Call_provers.print_prover_result pr | InternalFailure exn -> - fprintf fmt "Failure : %a" + fprintf fmt "Failure: %a" Exn_printer.exn_printer exn let cmd_regexp = Str.regexp "%\\(.\\)" diff --git a/src/why3session/why3session_latex.ml b/src/why3session/why3session_latex.ml index 265c82c8f87d354fd6b05c4c706089d08f7edd2b..354ed8bc480cdb132e19b3ca3472149c233ba55e 100644 --- a/src/why3session/why3session_latex.ml +++ b/src/why3session/why3session_latex.ml @@ -145,7 +145,10 @@ let print_result_prov proofs prov fmt= end | Session.InternalFailure _ -> fprintf fmt "& Internal Failure" - | Session.Undone _ -> fprintf fmt "& Undone" + | Session.Interrupted -> fprintf fmt "& Not yet run" + | Session.Unedited -> fprintf fmt "& Not yet edited" + | Session.Scheduled | Session.Running + | Session.JustEdited -> assert false with Not_found -> fprintf fmt "& \\noresult") prov; fprintf fmt "\\\\ @."