From f856d94ac12fd366f5a4834ab5b1629e3ab270b7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Claude=20March=C3=A9?= Date: Thu, 12 May 2011 17:55:43 +0200 Subject: [PATCH] reloading in IDE --- share/provers-detection-data.conf.in | 2 +- src/ide/gconfig.ml | 3 + src/ide/gconfig.mli | 1 + src/ide/newmain.ml | 87 ++++-- src/ide/replay.ml | 32 ++- src/ide/session.ml | 408 +++++++++++++-------------- src/ide/session.mli | 16 +- 7 files changed, 287 insertions(+), 262 deletions(-) diff --git a/share/provers-detection-data.conf.in b/share/provers-detection-data.conf.in index ffc394c68..9e2e99147 100644 --- a/share/provers-detection-data.conf.in +++ b/share/provers-detection-data.conf.in @@ -11,7 +11,7 @@ version_bad = "0.92" version_bad = "0.91" version_bad = "0.9" version_bad = "0.8" -command = "@LOCALBIN@why3-cpulimit %t %m -s %e %f" +command = "@LOCALBIN@why3-cpulimit %t %m -s %e -proof %f" driver = "drivers/alt_ergo_trunk.drv" [ATP alt-ergo] diff --git a/src/ide/gconfig.ml b/src/ide/gconfig.ml index 9453e6470..6776926c3 100644 --- a/src/ide/gconfig.ml +++ b/src/ide/gconfig.ml @@ -202,6 +202,7 @@ let iconname_prover = "wizard32" let iconname_transf = "configure32" let iconname_editor = "edit32" let iconname_replay = "refresh32" +let iconname_reload = "movefile32" let iconname_remove = "deletefile32" let iconname_cleaning = "trashb32" @@ -227,6 +228,7 @@ let image_prover = ref !image_default let image_transf = ref !image_default let image_editor = ref !image_default let image_replay = ref !image_default +let image_reload = ref !image_default let image_remove = ref !image_default let image_cleaning = ref !image_default @@ -253,6 +255,7 @@ let resize_images size = image_transf := image ~size iconname_transf; image_editor := image ~size iconname_editor; image_replay := image ~size iconname_replay; + image_reload := image ~size iconname_reload; image_remove := image ~size iconname_remove; image_cleaning := image ~size iconname_cleaning; () diff --git a/src/ide/gconfig.mli b/src/ide/gconfig.mli index f400cf4c9..5fc9c7b9b 100644 --- a/src/ide/gconfig.mli +++ b/src/ide/gconfig.mli @@ -72,6 +72,7 @@ val image_prover : GdkPixbuf.pixbuf ref val image_transf : GdkPixbuf.pixbuf ref val image_editor : GdkPixbuf.pixbuf ref val image_replay : GdkPixbuf.pixbuf ref +val image_reload : GdkPixbuf.pixbuf ref val image_remove : GdkPixbuf.pixbuf ref val image_cleaning : GdkPixbuf.pixbuf ref diff --git a/src/ide/newmain.ml b/src/ide/newmain.ml index 1d59ebd60..0b51cfa02 100644 --- a/src/ide/newmain.ml +++ b/src/ide/newmain.ml @@ -367,12 +367,15 @@ module M = Session.Make | Some r -> Some r#iter in let iter = goals_model#append ?parent () in + goals_model#set ~row:iter ~column:index_column (-1); goals_model#get_row_reference (goals_model#get_path iter) let remove row = let (_:bool) = goals_model#remove row#iter in () + let reset () = goals_model#clear () + let idle f = let (_ : GMain.Idle.id) = GMain.Idle.add f in () @@ -408,47 +411,57 @@ let set_proof_state ~obsolete a = let model_index = Hashtbl.create 17 -let get_any row = - try +let get_any row = + try let row = goals_model#get_iter row in let idx = goals_model#get ~row ~column:index_column in Hashtbl.find model_index idx with Not_found -> invalid_arg "Gmain.get_index" -let init = - let cpt = ref 0 in +let notify any = + match any with + | M.Goal g -> + set_row_status (M.goal_key g) (M.goal_proved g) + | M.Theory th -> + set_row_status (M.theory_key th) (M.verified th) + | M.File file -> + set_row_status file.M.file_key file.M.file_verified + | M.Proof_attempt a -> + set_proof_state ~obsolete:a.M.proof_obsolete a + | M.Transformation tr -> + set_row_status tr.M.transf_key tr.M.transf_proved + +let init = + let cpt = ref (-1) in fun row any -> - incr cpt; - Hashtbl.add model_index !cpt any; - goals_model#set ~row:row#iter ~column:index_column !cpt; - goals_model#set ~row:row#iter ~column:icon_column + let ind = goals_model#get ~row:row#iter ~column:index_column in + if ind < 0 then + begin + incr cpt; + Hashtbl.add model_index !cpt any; + goals_model#set ~row:row#iter ~column:index_column !cpt + end + else + begin + Hashtbl.replace model_index ind any; + end; + goals_model#set ~row:row#iter ~column:icon_column (match any with | M.Goal _ -> !image_file - | M.Theory _ + | M.Theory _ | M.File _ -> !image_directory | M.Proof_attempt _ -> !image_prover | M.Transformation _ -> !image_transf); - goals_model#set ~row:row#iter ~column:name_column + goals_model#set ~row:row#iter ~column:name_column (match any with | M.Goal g -> M.goal_expl g | M.Theory th -> M.theory_name th | M.File f -> Filename.basename f.M.file_name | M.Proof_attempt a -> let p = a.M.prover in p.Session.prover_name ^ " " ^ p.Session.prover_version - | M.Transformation tr -> Session.transformation_id tr.M.transf) + | M.Transformation tr -> Session.transformation_id tr.M.transf); + notify any -let notify any = - match any with - | M.Goal g -> - set_row_status (M.goal_key g) (M.goal_proved g) - | M.Theory th -> - set_row_status (M.theory_key th) (M.verified th) - | M.File file -> - set_row_status file.M.file_key file.M.file_verified - | M.Proof_attempt a -> - set_proof_state ~obsolete:false a - | M.Transformation tr -> - set_row_status tr.M.transf_key tr.M.transf_proved (********************) @@ -490,7 +503,7 @@ let () = let () = try eprintf "Opening session...@?"; - M.open_session ~env:gconfig.env ~provers:gconfig.provers + M.open_session ~env:gconfig.env ~provers:gconfig.provers ~init ~notify project_dir; M.maximum_running_proofs := gconfig.max_running_processes; eprintf " done@." @@ -567,7 +580,7 @@ let replay_obsolete_proofs () = List.iter (fun row -> let a = get_any row in - M.replay ~obsolete_only:true + M.replay ~obsolete_only:true ~context_unproved_goals_only:!context_unproved_goals_only a) goals_view#selection#get_selected_rows @@ -685,14 +698,14 @@ let exit_function () = match l with | [] -> () | f :: _ -> - eprintf "first element is a '%s' with %d sub-elements@." + eprintf "first element is a '%s' with %d sub-elements@." f.Xml.name (List.length f.Xml.elements); - + with e -> eprintf "test reloading failed with exception %s@." (Printexc.to_string e) end; let ret = Sys.command "xmllint --noout --dtdvalid share/why3session.dtd essai.xml" in - if ret = 0 then eprintf "DTD validation succeeded, good!@."; + if ret = 0 then eprintf "DTD validation succeeded, good!@."; *) M.save_session (); GMain.quit () @@ -911,7 +924,7 @@ let () = let () = b#set_image i#coerce in let (_ : GtkSignal.id) = b#connect#pressed ~callback:inline_selected_goals - in + in () @@ -1091,13 +1104,13 @@ let select_row p = match a with | M.Goal g -> let callback = function - | [t] -> + | [t] -> let task_text = Pp.string_of Pretty.print_task t in task_view#source_buffer#set_text task_text; task_view#scroll_to_mark `INSERT; scroll_to_source_goal g | _ -> assert false - in + in M.apply_transformation ~callback intro_transformation (M.get_task g) | M.Theory th -> @@ -1177,6 +1190,18 @@ let () = b#connect#pressed ~callback:replay_obsolete_proofs in () +let () = + let b = GButton.button ~packing:tools_box#add ~label:"Reload" () in + b#misc#set_tooltip_markup "Reloads the files"; + + let i = GMisc.image ~pixbuf:(!image_reload) () in + let () = b#set_image i#coerce in + let (_ : GtkSignal.id) = + b#connect#pressed ~callback:(fun () -> + current_file := ""; + M.reload_all gconfig.provers) + in () + (*************) (* removing *) (*************) diff --git a/src/ide/replay.ml b/src/ide/replay.ml index f3da57e13..c42af15f6 100644 --- a/src/ide/replay.ml +++ b/src/ide/replay.ml @@ -56,7 +56,7 @@ let loadpath = (Whyconf.loadpath (Whyconf.get_main config)) let env = Lexer.create_env loadpath -let provers = Whyconf.get_provers config +let provers = Whyconf.get_provers config let provers = Util.Mstr.fold (Session.get_prover_data env) provers Util.Mstr.empty @@ -71,13 +71,15 @@ module M = Session.Make (struct type key = int - let create ?parent () = + let create ?parent () = match parent with | None -> 0 | Some n -> n+1 let remove _row = () + let reset () = () + let idle f = match !idle_handler with | None -> idle_handler := Some f; @@ -115,16 +117,16 @@ let main_loop () = else (* attempt to run the idle handler *) match !idle_handler with - | None -> - begin - let ms = + | None -> + begin + let ms = match !timeout_handler with | None -> raise Exit | Some(ms,_) -> ms in usleep (ms -. time) end - | Some f -> + | Some f -> let b = f () in if b then () else begin @@ -136,8 +138,8 @@ open Format let model_index = Hashtbl.create 257 -let init = - let cpt = ref 0 in +let init = + let cpt = ref 0 in fun _row any -> incr cpt; Hashtbl.add model_index !cpt any; @@ -152,7 +154,7 @@ let init = in printf "Item '%s' loaded@." name -let string_of_result result = +let string_of_result result = match result with | Session.Undone -> "undone" | Session.Scheduled -> "scheduled" @@ -166,7 +168,7 @@ let string_of_result result = | Call_provers.Failure _ -> "failure" | Call_provers.HighFailure -> "high failure" -let print_result fmt res = +let print_result fmt res = let t = match res with | Session.Done { Call_provers.pr_time = time } -> Format.sprintf "(%.2f)" time @@ -186,8 +188,8 @@ let notify any = file.M.file_verified | M.Proof_attempt a -> let p = a.M.prover in - printf "Proof with '%s %s' gives %a@." - p.Session.prover_name p.Session.prover_version + printf "Proof with '%s %s' gives %a@." + p.Session.prover_name p.Session.prover_version print_result a.M.proof_state | M.Transformation tr -> printf "Transformation '%s' proved: %b@." @@ -220,12 +222,12 @@ let main () = try eprintf "Opening session...@?"; M.open_session ~env ~provers ~init ~notify project_dir; - M.maximum_running_proofs := + M.maximum_running_proofs := Whyconf.running_provers_max (Whyconf.get_main config); eprintf " done@."; let files = M.get_all_files () in - List.iter - (fun f -> + List.iter + (fun f -> eprintf "Replaying file '%s'@." f.M.file_name; M.replay ~obsolete_only:false ~context_unproved_goals_only:false (M.File f)) files; diff --git a/src/ide/session.ml b/src/ide/session.ml index fe10c8373..531a66a66 100644 --- a/src/ide/session.ml +++ b/src/ide/session.ml @@ -25,7 +25,7 @@ open Format (* provers *) (***************************) -type prover_data = +type prover_data = { prover_id : string; prover_name : string; prover_version : string; @@ -50,7 +50,7 @@ let get_prover_data env id pr acc = acc with e -> eprintf "Failed to load driver %s for prover %s (%a). prover disabled@." - pr.Whyconf.driver + pr.Whyconf.driver pr.Whyconf.name Exn_printer.exn_printer e ; @@ -64,7 +64,7 @@ type trans = | Trans_one of Task.task Trans.trans | Trans_list of Task.task Trans.tlist -type transformation_data = +type transformation_data = { transformation_name : string; transformation : trans; } @@ -82,7 +82,7 @@ let lookup_trans env name = let lookup_transformation env = let h = Hashtbl.create 13 in fun name -> - try + try Hashtbl.find h name with Not_found -> let t = {transformation_name = name; @@ -109,6 +109,7 @@ module type OBSERVER = sig type key val create: ?parent:key -> unit -> key val remove: key -> unit + val reset: unit -> unit val timeout: ms:int -> (unit -> bool) -> unit val idle: (unit -> bool) -> unit @@ -138,7 +139,7 @@ and goal = goal_expl : string option; parent : goal_parent; mutable task: Task.task option; - checksum : string; + mutable checksum : string; goal_key : O.key; mutable proved : bool; external_proofs: (string, proof_attempt) Hashtbl.t; @@ -181,25 +182,25 @@ let theory_key t = t.theory_key let verified t = t.verified let goals t = t.goals -let get_theory t = - match t.theory with - | None -> +let get_theory t = + match t.theory with + | None -> eprintf "Session: theory not yet reimported, this should not happen@."; assert false | Some t -> t let goal_name g = g.goal_name -let goal_expl g = - match g.goal_expl with +let goal_expl g = + match g.goal_expl with | None -> g.goal_name | Some s -> s let goal_key g = g.goal_key let goal_proved g = g.proved let transformations g = g.transformations -let get_task g = - match g.task with - | None -> +let get_task g = + match g.task with + | None -> begin match g.parent with | Parent_theory _th -> @@ -213,7 +214,7 @@ let get_task g = let all_files : file list ref = ref [] let get_all_files () = !all_files - + (************************) (* saving state on disk *) (************************) @@ -232,14 +233,14 @@ let save_result fmt r = let save_status fmt s = match s with | Undone | Scheduled | Running -> - fprintf fmt "@\n" - | InternalFailure msg -> - fprintf fmt "@\n" + fprintf fmt "@\n" + | InternalFailure msg -> + fprintf fmt "@\n" (Printexc.to_string msg) | Done r -> save_result fmt r let save_proof_attempt fmt _key a = - fprintf fmt "@\n@[" + fprintf fmt "@\n@[" a.prover.prover_id a.edited_as; save_status fmt a.proof_state; @@ -250,20 +251,20 @@ let opt lab fmt = function | Some s -> fprintf fmt "%s=\"%s\" " lab s let rec save_goal fmt g = - fprintf fmt "@\n@[" - g.goal_name (opt "expl") g.goal_expl g.proved; + fprintf fmt "@\n@[" + g.goal_name (opt "expl") g.goal_expl g.checksum g.proved; Hashtbl.iter (save_proof_attempt fmt) g.external_proofs; Hashtbl.iter (save_trans fmt) g.transformations; fprintf fmt "@]@\n" and save_trans fmt _ t = - fprintf fmt "@\n@[" + fprintf fmt "@\n@[" t.transf.transformation_name t.transf_proved; List.iter (save_goal fmt) t.subgoals; fprintf fmt "@]@\n" let save_theory fmt t = - fprintf fmt "@\n@[" + fprintf fmt "@\n@[" t.theory_name t.verified; List.iter (save_goal fmt) t.goals; fprintf fmt "@]@\n" @@ -272,7 +273,7 @@ let save_file fmt f = fprintf fmt "@\n@[" f.file_name f.file_verified; List.iter (save_theory fmt) f.theories; fprintf fmt "@]@\n" - + let save fname = let ch = open_out fname in let fmt = formatter_of_out_channel ch in @@ -348,7 +349,7 @@ let set_proof_state ~obsolete a res = (*************************) (* Scheduler *) -(*************************) +(*************************) (* timeout handler *) @@ -581,25 +582,24 @@ let raw_add_external_proof ~obsolete ~edit g p result = edited_as = edit; } in - Hashtbl.add g.external_proofs p.prover_name a; + Hashtbl.add g.external_proofs p.prover_id a; let any = Proof_attempt a in !init_fun key any; !notify_fun any; - (* !notify_fun (Goal g) ? *) a -(* [raw_add_goal parent name expl t] adds a goal to the given parent +(* [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 *) -let raw_add_goal parent name expl topt = +let raw_add_goal parent name expl sum topt = let parent_key = match parent with | Parent_theory mth -> mth.theory_key | Parent_transf mtr -> mtr.transf_key in let key = O.create ~parent:parent_key () in let sum = match topt with - | None -> "" + | None -> sum | Some t -> task_checksum t in let goal = { goal_name = name; @@ -664,7 +664,7 @@ let add_theory mfile name th = let id = (Task.task_goal t).Decl.pr_name in let name = id.Ident.id_string in let expl = get_explanation id (Task.task_goal_fmla t) in - let goal = raw_add_goal (Parent_theory mth) name expl (Some t) in + let goal = raw_add_goal (Parent_theory mth) name expl "" (Some t) in goal :: acc) [] tasks @@ -691,8 +691,8 @@ let project_dir = ref "" let read_file fn = let fn = Filename.concat !project_dir fn in - let env = match !current_env with - | None -> assert false | Some e -> e + let env = match !current_env with + | None -> assert false | Some e -> e in let theories = Env.read_file env fn in let theories = @@ -732,48 +732,38 @@ let file_exists fn = (* reload a file *) (**********************************) -let rec reimport_any_goal _parent gid _gname t goal __goal_obsolete = - let _info = get_explanation gid (Task.task_goal_fmla t) in +let reload_proof ~provers obsolete goal pid old_a = + try + let p = Util.Mstr.find pid provers in + let old_res = old_a.proof_state in + let obsolete = obsolete or old_a.proof_obsolete in + eprintf "proof_obsolete : %b@." obsolete; + let _a = + raw_add_external_proof ~obsolete ~edit:old_a.edited_as goal p old_res + in + ((* something TODO ?*)) + with Not_found -> + eprintf + "Warning: prover %s appears in database but is not installed.@." + pid + +let rec reload_any_goal ~provers parent gid gname sum t old_goal goal_obsolete = + let info = get_explanation gid (Task.task_goal_fmla t) in + let goal = raw_add_goal parent gname info sum (Some t) in goal.task <- Some t; + begin + match old_goal with + | None -> () + | Some g -> + Hashtbl.iter (reload_proof ~provers goal_obsolete goal) g.external_proofs; + Hashtbl.iter (reload_trans ~provers goal_obsolete goal) g.transformations + end; goal + + +and reload_trans ~provers:_ _goal_obsolete _goal _tr_id _tr = + () (* - let goal = raw_add_goal parent gname info t in - let proved = ref false in - let external_proofs = Db.external_proofs db_goal in - Db.Hprover.iter - (fun pid a -> - let pname = Db.prover_name pid in - try - let p = Util.Mstr.find pname gconfig.provers in - let s,t,o,edit = Db.status_and_time a in - if goal_obsolete && not o then Db.set_obsolete a; - let obsolete = goal_obsolete or o in - let s = match s with - | Db.Undone -> Call_provers.HighFailure - | Db.Done r -> - if r = Call_provers.Valid then - if not obsolete then proved := true; - r - in - let r = { Call_provers.pr_answer = s; - Call_provers.pr_output = ""; - Call_provers.pr_time = t; - } - in - let (_pa : Model.proof_attempt) = - Helpers.add_external_proof_row ~obsolete ~edit goal p a - (Gscheduler.Done r) - in - ((* something TODO ?*)) - with Not_found -> - eprintf - "Warning: prover %s appears in database but is not installed.@." - pname - ) - external_proofs; - let transformations = Db.transformations db_goal in - Db.Htransf.iter - (fun tr_id tr -> let trname = Db.transf_name tr_id in eprintf "Reimporting transformation %s for goal %s @." trname gname; let trans = trans_of_name trname in @@ -867,93 +857,83 @@ let rec reimport_any_goal _parent gid _gname t goal __goal_obsolete = *) -let reimport_root_goal mth tname goals t : goal = - (* re-imports database informations of a goal in theory mth (named tname) - goals is a table, indexed by names of DB goals formerly known to be - a in theory mth. returns true whenever the task t is known to be - proved *) +(* reloads the task [t] in theory mth (named tname) *) +let reload_root_goal ~provers mth tname old_goals t : goal = let id = (Task.task_goal t).Decl.pr_name in - let gname = id.Ident.id_string - in + let gname = id.Ident.id_string in let sum = task_checksum t in - let goal, goal_obsolete = - try - let dbg = Util.Mstr.find gname goals in - let db_sum = dbg.checksum in - let goal_obsolete = sum <> db_sum in - if goal_obsolete then - begin - eprintf "Goal %s.%s has changed@." tname gname; (* - Db.change_checksum dbg sum -*) - end; - dbg,goal_obsolete - with Not_found -> - assert false (* TODO *) -(* - let dbg = Db.add_goal mth.Model.theory_db gname sum in - dbg,false + let goal = raw_add_goal (Parent_theory mth) gname expl sum (Some t) in *) + let old_goal, goal_obsolete = + try + let old_goal = Util.Mstr.find gname old_goals in + let old_sum = old_goal.checksum in + (Some old_goal,sum <> old_sum) + with Not_found -> (None,false) in - reimport_any_goal (Parent_theory mth) id gname t goal goal_obsolete + if goal_obsolete then + eprintf "Goal %s.%s has changed@." tname gname; + reload_any_goal ~provers (Parent_theory mth) id gname sum t old_goal goal_obsolete -(* reloads a file *) +(* reloads a theory *) +let reload_theory ~provers mfile old_theories (_,tname,th) = + eprintf "[Reload] theory '%s'@."tname; + let tasks = List.rev (Task.split_theory th None None) in + let mth = raw_add_theory mfile (Some th) tname in + let old_goals = + try + let old_mth = Util.Mstr.find tname old_theories in + old_mth.goals + with Not_found -> [] + in + let goalsmap = List.fold_left + (fun goalsmap g -> Util.Mstr.add g.goal_name g goalsmap) + Util.Mstr.empty old_goals + in + let new_goals = List.fold_left + (fun acc t -> + let g = reload_root_goal ~provers mth tname goalsmap t in + g::acc) + [] tasks + in + mth.goals <- List.rev new_goals; + check_theory_proved mth; + mth -let reload_file mf = + +(* reloads a file *) +let reload_file ~provers mf = eprintf "[Reload] file '%s'@." mf.file_name; - try - let theories = read_file mf.file_name in - let old_theories = List.fold_left - (fun acc t -> Util.Mstr.add t.theory_name t acc) - Util.Mstr.empty - mf.theories - in - let mths = - List.fold_left - (fun acc (_,tname,th) -> - eprintf "[Reload] theory '%s'@."tname; - let mth = - try - let mth = Util.Mstr.find tname old_theories in - mth.theory <- Some th; - mth - with Not_found -> - raw_add_theory mf (Some th) tname - in - let goals = List.fold_left - (fun acc g -> Util.Mstr.add g.goal_name g acc) - Util.Mstr.empty mth.goals - in - let tasks = List.rev (Task.split_theory th None None) in - let goals = List.fold_left - (fun acc t -> - let g = reimport_root_goal mth tname goals t in - g::acc) - [] tasks - in - mth.goals <- List.rev goals; - (* TODO: what to do with remaining old theories? - for the moment they remain in the session - *) - check_theory_proved mth; - mth::acc - ) - [] theories - in - (* TODO: detecter d'eventuelles vieilles theories, qui seraient donc - dans [old_theories] mais pas dans [theories] - *) - mf.theories <- List.rev mths; - check_file_verified mf - with e -> - eprintf "@[Error while reading file@ '%s':@ %a@.@]" mf.file_name - Exn_printer.exn_printer e; - exit 1 - + let theories = + try + read_file mf.file_name + with e -> + eprintf "@[Error while reading file@ '%s':@ %a@.@]" mf.file_name + Exn_printer.exn_printer e; + (* TODO: do something clever than that! *) + exit 1 + in + let new_mf = raw_add_file mf.file_name in + let old_theories = List.fold_left + (fun acc t -> Util.Mstr.add t.theory_name t acc) + Util.Mstr.empty + mf.theories + in + let mths = List.fold_left + (fun acc th -> reload_theory ~provers new_mf old_theories th :: acc) + [] theories + in + new_mf.theories <- List.rev mths; + check_file_verified new_mf + (* reloads all files *) -let reload_all () = List.iter reload_file !all_files +let reload_all provers = + let files = !all_files in + all_files := []; + O.reset (); + List.iter (reload_file ~provers) files (****************************) (* session opening *) @@ -962,11 +942,11 @@ let reload_all () = List.iter reload_file !all_files let load_result r = match r.Xml.name with | "result" -> - let status = + let status = try List.assoc "status" r.Xml.attributes with Not_found -> assert false in - let answer = + let answer = match status with | "valid" -> Call_provers.Valid | "invalid" -> Call_provers.Invalid @@ -974,7 +954,7 @@ let load_result r = | "timeout" -> Call_provers.Timeout | "failure" -> Call_provers.Failure "" | "highfailure" -> Call_provers.Failure "" - | s -> + | s -> eprintf "Session.load_result: unexpected status '%s'@." s; assert false in @@ -986,40 +966,44 @@ let load_result r = Call_provers.pr_time = time; Call_provers.pr_output = ""; } - | s -> + | s -> eprintf "Session.load_result: unexpected element '%s'@." s; assert false - - -let rec load_goal ~env ~provers parent acc g = + + +let rec load_goal ~env ~provers parent acc g = match g.Xml.name with | "goal" -> - let gname = + let gname = try List.assoc "name" g.Xml.attributes with Not_found -> assert false in - let expl = + let expl = try Some (List.assoc "expl" g.Xml.attributes) with Not_found -> None in - let mg = raw_add_goal parent gname expl None in + let sum = + try List.assoc "sum" g.Xml.attributes + with Not_found -> "" + in + let mg = raw_add_goal parent gname expl sum None in List.iter (load_proof_or_transf ~env ~provers mg) g.Xml.elements; mg::acc - | s -> + | s -> eprintf "Session.load_goal: unexpected element '%s'@." s; assert false - + and load_proof_or_transf ~env ~provers mg a = match a.Xml.name with - | "proof" -> - let prover = + | "proof" -> + let prover = try List.assoc "prover" a.Xml.attributes with Not_found -> assert false in - let p = + let p = try - Util.Mstr.find prover provers + Util.Mstr.find prover provers with Not_found -> assert false (* TODO *) in let res = match a.Xml.elements with @@ -1027,73 +1011,73 @@ and load_proof_or_transf ~env ~provers mg a = | [] -> Undone | _ -> assert false in - let edit = + let edit = try List.assoc "edited" a.Xml.attributes with Not_found -> assert false in - let _pa = raw_add_external_proof ~obsolete:false + let _pa = raw_add_external_proof ~obsolete:false ~edit mg p res in (* already done by raw_add_external_proof Hashtbl.add mg.external_proofs prover pa *) () - | "transf" -> - let trname = + | "transf" -> + let trname = try List.assoc "name" a.Xml.attributes with Not_found -> assert false in - let tr = - try - lookup_transformation env trname + let tr = + try + lookup_transformation env trname with Not_found -> assert false (* TODO *) in - let _proved = + let _proved = try List.assoc "proved" a.Xml.attributes with Not_found -> assert false in let mtr = raw_add_transformation mg tr in mtr.subgoals <- - List.rev - (List.fold_left - (load_goal ~env ~provers (Parent_transf mtr)) + List.rev + (List.fold_left + (load_goal ~env ~provers (Parent_transf mtr)) [] a.Xml.elements); (* already done by raw_add_transformation Hashtbl.add mg.transformations trname mtr *) () - | s -> + | s -> eprintf "Session.load_proof_or_transf: unexpected element '%s'@." s; assert false let load_theory ~env ~provers mf acc th = match th.Xml.name with | "theory" -> - let thname = + let thname = try List.assoc "name" th.Xml.attributes with Not_found -> assert false in let mth = raw_add_theory mf None thname in - mth.goals <- - List.rev - (List.fold_left - (load_goal ~env ~provers (Parent_theory mth)) + mth.goals <- + List.rev + (List.fold_left + (load_goal ~env ~provers (Parent_theory mth)) [] th.Xml.elements); mth::acc - | s -> + | s -> eprintf "Session.load_theory: unexpected element '%s'@." s; assert false let load_file ~env ~provers f = match f.Xml.name with | "file" -> - let fn = + let fn = try List.assoc "name" f.Xml.attributes with Not_found -> assert false in let mf = raw_add_file fn in - mf.theories <- - List.rev + mf.theories <- + List.rev (List.fold_left (load_theory ~env ~provers mf) [] f.Xml.elements) - | s -> + | s -> eprintf "Session.load_file: unexpected element '%s'@." s; assert false @@ -1102,13 +1086,13 @@ let load_session ~env ~provers xml = match cont.Xml.name with | "why3session" -> List.iter (load_file ~env ~provers) cont.Xml.elements - | s -> + | s -> eprintf "Session.load_session: unexpected element '%s'@." s; assert false - + let db_filename = "why3session.xml" -let open_session ~env ~provers ~init ~notify dir = +let open_session ~env ~provers ~init ~notify dir = match !current_env with | None -> init_fun := init; notify_fun := notify; @@ -1116,20 +1100,20 @@ let open_session ~env ~provers ~init ~notify dir = begin try let xml = Xml.from_file (Filename.concat dir db_filename) in load_session ~env ~provers xml; - reload_all () - with - | Sys_error _ -> + reload_all provers + with + | Sys_error _ -> (* xml does not exist yet *) () | Xml.Parse_error s -> Format.eprintf "XML database corrupted, ignored (%s)@." s; () end - | _ -> + | _ -> eprintf "Session.open_session: session already opened@."; assert false -let save_session () = +let save_session () = match !current_env with | Some _ -> save (Filename.concat !project_dir db_filename) | None -> @@ -1191,24 +1175,24 @@ let rec prover_on_goal_or_children ~context_unproved_goals_only p g = let run_prover ~context_unproved_goals_only pr a = match a with - | Goal g -> + | Goal g -> prover_on_goal_or_children ~context_unproved_goals_only pr g - | Theory th -> - List.iter - (prover_on_goal_or_children ~context_unproved_goals_only pr) + | Theory th -> + List.iter + (prover_on_goal_or_children ~context_unproved_goals_only pr) th.goals - | File file -> + | File file -> List.iter (fun th -> - List.iter + List.iter (prover_on_goal_or_children ~context_unproved_goals_only pr) th.goals) file.theories | Proof_attempt a -> prover_on_goal_or_children ~context_unproved_goals_only pr a.proof_goal | Transformation tr -> - List.iter - (prover_on_goal_or_children ~context_unproved_goals_only pr) + List.iter + (prover_on_goal_or_children ~context_unproved_goals_only pr) tr.subgoals (**********************************) @@ -1228,9 +1212,9 @@ let rec replay_on_goal_or_children ~obsolete_only ~context_unproved_goals_only g then redo_external_proof g a) g.external_proofs; Hashtbl.iter - (fun _ t -> - List.iter - (replay_on_goal_or_children ~obsolete_only ~context_unproved_goals_only) + (fun _ t -> + List.iter + (replay_on_goal_or_children ~obsolete_only ~context_unproved_goals_only) t.subgoals) g.transformations @@ -1239,20 +1223,20 @@ let replay ~obsolete_only ~context_unproved_goals_only a = | Goal g -> replay_on_goal_or_children ~obsolete_only ~context_unproved_goals_only g | Theory th -> - List.iter + List.iter (replay_on_goal_or_children ~obsolete_only ~context_unproved_goals_only) th.goals | File file -> List.iter (fun th -> - List.iter + List.iter (replay_on_goal_or_children ~obsolete_only ~context_unproved_goals_only) th.goals) file.theories | Proof_attempt a -> replay_on_goal_or_children ~obsolete_only ~context_unproved_goals_only a.proof_goal | Transformation tr -> - List.iter + List.iter (replay_on_goal_or_children ~obsolete_only ~context_unproved_goals_only) tr.subgoals @@ -1306,7 +1290,7 @@ let transformation_on_goal g tr = in let goal = raw_add_goal (Parent_transf tr) - subgoal_name expl (Some subtask) + subgoal_name expl "" (Some subtask) in (goal :: acc, count+1) in @@ -1324,11 +1308,11 @@ let rec transform_goal_or_children ~context_unproved_goals_only tr g = Hashtbl.iter (fun _ t -> r := false; - List.iter + List.iter (transform_goal_or_children ~context_unproved_goals_only tr) - t.subgoals) + t.subgoals) g.transformations; - if !r then + if !r then schedule_delayed_action (fun () -> transformation_on_goal g tr) end diff --git a/src/ide/session.mli b/src/ide/session.mli index be453e374..fb290607b 100644 --- a/src/ide/session.mli +++ b/src/ide/session.mli @@ -69,6 +69,9 @@ module type OBSERVER = sig val remove: key -> unit (** removes a key *) + val reset: unit -> unit + (** deletes all keys *) + val timeout: ms:int -> (unit -> bool) -> unit (** a handler for functions that must be called after a given time elapsed, in milliseconds. When the given function returns @@ -149,18 +152,20 @@ module Make(O: OBSERVER) : sig env:Env.env -> provers:prover_data Util.Mstr.t -> init:(O.key -> any -> unit) -> - notify:(any -> unit) -> string -> unit + notify:(any -> unit) -> + string -> unit (** starts a new proof session, using directory given as argument this reloads the previous session database if any. Opening a session must be done prior to any other actions. And it cannot be done twice. + the [notify] function is a function that will be called at each + update of element of the state + the [init] function is a function that will be called at each creation of element of the state - the [notify] function is a function that will be called at each - update of element of the state *) val maximum_running_proofs : int ref @@ -216,6 +221,11 @@ module Make(O: OBSERVER) : sig if context_unproved_goals_only is set then reruns only proofs with result was 'valid' *) + val reload_all: prover_data Util.Mstr.t -> unit + (** reloads all the files + If for a given file, the parsing or typing fails, then + then old version is kept, but marked obsolete + *) (* TODO -- GitLab