diff --git a/ROADMAP b/ROADMAP index 6556d87d96fd07ed1383172404544a5422686386..6caed06c4eafa4c1e4b2074d004217229b2c0f7b 100644 --- a/ROADMAP +++ b/ROADMAP @@ -98,8 +98,8 @@ https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990 * Improved IDE: - left scrollbar + selection of shown or hidden provers - font enlargement - - integration of support for prover upgrade - - !!TODO!! support for selection of alternate editors + - integration of the support for prover upgrade + - support for selection of alternate editors * what else ? * see also the file CHANGES @@ -136,14 +136,6 @@ https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990 == TODOs == -* (TOUS) Faire marcher la selection de l'editeur associé a un prouveur -dans l'IDE -** probleme: le choix n'est pas pris en compte, pas enregistré -** question subsidaire: remise en cause du systeme de Whyconf inutilement - compliqué et tres difficile a maintenir. - La raison initiale "permettre a l'IDE de stocker sa config dans - le meme fichier .conf" ne me semble pas justifier une telle complication - * DONE Document the Coq plugin and tactic ** DONE option timelimit ** DONE renommer "coq-plugin" en "coq-tactic" diff --git a/src/ide/gconfig.ml b/src/ide/gconfig.ml index d93dd284469876c040c591803dbb9ff1b7c167f4..5f8410bb0977298e5849d3714b90b476384ebc7d 100644 --- a/src/ide/gconfig.ml +++ b/src/ide/gconfig.ml @@ -41,10 +41,7 @@ type t = mutable window_height : int; mutable tree_width : int; mutable task_height : int; - mutable time_limit : int; - mutable mem_limit : int; mutable verbose : int; - mutable max_running_processes : int; mutable default_editor : string; mutable intro_premises : bool; mutable show_labels : bool; @@ -182,7 +179,7 @@ let load_altern alterns (_,section) = Mprover.add unknown known alterns let load_config config original_config = - let main = get_main config in + (* let main = get_main config in *) let ide = match get_section config "ide" with | None -> default_ide | Some s -> load_ide s @@ -198,8 +195,6 @@ let load_config config original_config = window_width = ide.ide_window_width; tree_width = ide.ide_tree_width; task_height = ide.ide_task_height; - time_limit = Whyconf.timelimit main; - mem_limit = Whyconf.memlimit main; verbose = ide.ide_verbose; intro_premises= ide.ide_intro_premises ; show_labels = ide.ide_show_labels ; @@ -209,7 +204,6 @@ let load_config config original_config = premise_color = ide.ide_premise_color; goal_color = ide.ide_goal_color; error_color = ide.ide_error_color; - max_running_processes = Whyconf.running_provers_max main; default_editor = ide.ide_default_editor; config = config; original_config = original_config; @@ -238,14 +232,28 @@ let load_config config original_config = *) +let debug_save_config n c = + let coq = { prover_name = "Coq" ; prover_version = "8.3pl3"; + prover_altern = "" } in + let p = Mprover.find coq (get_provers c) in + let time = Whyconf.timelimit (Whyconf.get_main c) in + Format.eprintf "[debug] save_config %d: timelimit=%d ; editor for Coq=%s@." + n time p.editor + let save_config t = + eprintf "[Info] saving IDE config file@."; + (* taking original config, without the extra_config *) let config = t.original_config in - let config = set_main config - (set_limits (get_main config) - t.time_limit t.mem_limit t.max_running_processes) - in - (* let _,alterns = Mprover.fold save_altern t.altern_provers (0,[]) in *) - (* let config = set_family config "alternative_prover" alterns in *) + (* copy possibly modified settings to original config *) + let new_main = Whyconf.get_main t.config in + let time = Whyconf.timelimit new_main in + let mem = Whyconf.memlimit new_main in + let nb = Whyconf.running_provers_max new_main in + let config = set_main config (set_limits (get_main config) time mem nb) in + (* copy also provers section since it may have changed (the editor + can be set via the preferences dialog) *) + let config = set_provers config (get_provers t.config) in + (* copy also the possibly changed policies *) let config = set_policies config (get_policies t.config) in let ide = empty_section in let ide = set_int ide "window_height" t.window_height in @@ -262,17 +270,9 @@ let save_config t = let ide = set_string ide "goal_color" t.goal_color in let ide = set_string ide "error_color" t.error_color in let ide = set_string ide "default_editor" t.default_editor in - (* let ide = set_string ~default:"ask" ide "replace_prover" *) - (* (match t.replace_prover with *) - (* | CRP_Ask -> "ask" *) - (* | CRP_Not_Obsolete -> "never not obsolete") in *) let ide = set_stringl ide "hidden_prover" t.hidden_provers in let config = set_section config "ide" ide in -(* TODO: store newly detected provers ! - let config = set_provers config - (Mstr.fold save_prover t.provers Mstr.empty) in -*) - save_config config + Whyconf.save_config config let read_config conf_file extra_files = try @@ -494,17 +494,21 @@ let general_settings c (notebook:GPack.notebook) = in *) (* timelimit ? *) + let main = Whyconf.get_main c.config in + let timelimit = ref (Whyconf.timelimit main) in + let memlimit = ref (Whyconf.memlimit main) in let hb = GPack.hbox ~homogeneous:false ~packing:page#pack () in let _ = GMisc.label ~text:"Time limit: " ~packing:(hb#pack ~expand:false) () in let timelimit_spin = GEdit.spin_button ~digits:0 ~packing:hb#add () in timelimit_spin#adjustment#set_bounds ~lower:2. ~upper:300. ~step_incr:1. (); - timelimit_spin#adjustment#set_value (float_of_int c.time_limit); + timelimit_spin#adjustment#set_value (float_of_int !timelimit); let (_ : GtkSignal.id) = timelimit_spin#connect#value_changed ~callback: - (fun () -> c.time_limit <- timelimit_spin#value_as_int) + (fun () -> timelimit := timelimit_spin#value_as_int) in (* nb of processes ? *) + let nb_processes = ref (Whyconf.running_provers_max main) in let hb = GPack.hbox ~homogeneous:false ~packing:page#pack () in let _ = GMisc.label ~text:"Nb of processes: " ~packing:(hb#pack ~expand:false) () in @@ -512,10 +516,10 @@ let general_settings c (notebook:GPack.notebook) = nb_processes_spin#adjustment#set_bounds ~lower:1. ~upper:16. ~step_incr:1. (); nb_processes_spin#adjustment#set_value - (float_of_int c.max_running_processes); + (float_of_int !nb_processes); let (_ : GtkSignal.id) = nb_processes_spin#connect#value_changed ~callback: - (fun () -> c.max_running_processes <- nb_processes_spin#value_as_int) + (fun () -> nb_processes := nb_processes_spin#value_as_int) in let display_options_frame = GBin.frame ~label:"Display options" @@ -611,8 +615,7 @@ let general_settings c (notebook:GPack.notebook) = let _fillbox = GPack.vbox ~packing:(page#pack ~expand:true) () in - () - + timelimit, memlimit, nb_processes (* Page "Provers" *) @@ -742,8 +745,8 @@ let editors_page c (notebook:GPack.notebook) = | "default" -> "" | s -> s in - Format.eprintf "prover %a : selected editor '%s'@." - print_prover p data; + (* Format.eprintf "prover %a : selected editor '%s'@." *) + (* print_prover p data; *) let provers = Whyconf.get_provers c.config in c.config <- Whyconf.set_provers c.config @@ -764,7 +767,7 @@ let preferences (c : t) = let vbox = dialog#vbox in let notebook = GPack.notebook ~packing:vbox#add () in (** page "general settings" **) - general_settings c notebook; + let t,m,n = general_settings c notebook in (*** page "editors" **) editors_page c notebook; (** page "Provers" **) @@ -788,7 +791,13 @@ let preferences (c : t) = (** bottom button **) dialog#add_button "Close" `CLOSE ; let ( _ : GWindow.Buttons.about) = dialog#run () in - eprintf "saving IDE config file@."; + (* let config = set_main config *) + (* (set_limits (get_main config) *) + (* t.time_limit t.mem_limit t.max_running_processes) *) + (* in *) + + c.config <- Whyconf.set_main c.config + (Whyconf.set_limits (Whyconf.get_main c.config) !t !m !n); save_config (); dialog#destroy () diff --git a/src/ide/gconfig.mli b/src/ide/gconfig.mli index c8c2a8243cb17a2b73d3867a399d79948853f7bc..e64cea46d058e2f7c4e2306c3970e964399a371f 100644 --- a/src/ide/gconfig.mli +++ b/src/ide/gconfig.mli @@ -21,20 +21,12 @@ open Why3 open Whyconf -(** Todo do something generic perhaps*) -(* type conf_replace_prover = *) -(* | CRP_Ask *) -(* | CRP_Not_Obsolete *) - type t = { mutable window_width : int; mutable window_height : int; mutable tree_width : int; mutable task_height : int; - mutable time_limit : int; - mutable mem_limit : int; mutable verbose : int; - mutable max_running_processes : int; mutable default_editor : string; mutable intro_premises : bool; mutable show_labels : bool; diff --git a/src/ide/gmain.ml b/src/ide/gmain.ml index ecc10f84e3cb39334ab8f4e979f134b021b8825f..4d3ba08f18c6239330d35717afced1fdb28f7328 100644 --- a/src/ide/gmain.ml +++ b/src/ide/gmain.ml @@ -414,7 +414,7 @@ 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.Unedited | Session.Undone Session.JustEdited -> !image_unknown | Session.Undone Session.Scheduled -> !image_scheduled | Session.Undone Session.Running -> !image_running @@ -536,7 +536,7 @@ let update_task_view a = | S.Goal g -> if (Gconfig.config ()).intro_premises then let trans = - Trans.lookup_transform intro_transformation (env_session()).S.env + Trans.lookup_transform intro_transformation (env_session()).S.env in display_task (Trans.apply trans (S.goal_task g)) else @@ -587,7 +587,7 @@ module M = Session_scheduler.Make session_needs_saving := true; let (_:bool) = goals_model#remove row#iter in () - let reset () = + let reset () = session_needs_saving := true; goals_model#clear () @@ -765,7 +765,9 @@ let sched = M.update_session ~allow_obsolete:true session gconfig.env gconfig.Gconfig.config in - let sched = M.init gconfig.max_running_processes in + let sched = M.init (Whyconf.running_provers_max + (Whyconf.get_main gconfig.config)) + in dprintf debug "@]@\n[Info] Opening session: done@."; session_needs_saving := false; current_env_session := Some env; @@ -804,6 +806,7 @@ let () = (*****************************************************) let prover_on_selected_goals pr = + let timelimit = Whyconf.timelimit (Whyconf.get_main gconfig.config) in List.iter (fun row -> try @@ -811,7 +814,7 @@ let prover_on_selected_goals pr = M.run_prover (env_session()) sched ~context_unproved_goals_only:!context_unproved_goals_only - ~timelimit:gconfig.time_limit + ~timelimit pr a with e -> eprintf "@[Exception raised while running a prover:@ %a@.@]" @@ -938,18 +941,20 @@ let (_ : GMenu.image_menu_item) = begin match !current_env_session with | None -> () - | Some _e -> - (* Can't do that since field .whyconf is not mutable *) - (* e.Session.whyconf <- gconfig.config *) - () + | Some e -> + Session.update_env_session_config e gconfig.config; + Session.unload_provers e end; !refresh_provers (); +(* Mprover.iter (fun p pi -> Format.eprintf "editor for %a : %s@." Whyconf.print_prover p pi.editor) (Whyconf.get_provers gconfig.config); - M.set_maximum_running_proofs gconfig.max_running_processes sched) +*) + let nb = Whyconf.running_provers_max (Whyconf.get_main gconfig.config) in + M.set_maximum_running_proofs nb sched) () let add_refresh_provers f _msg = @@ -975,7 +980,6 @@ let save_session () = let exit_function ?(destroy=false) () = - eprintf "[Info] saving IDE config file@."; save_config (); if not !session_needs_saving then GMain.quit () else match (Gconfig.config ()).saving_policy with @@ -1023,7 +1027,7 @@ let enlarge_font () = () let reduce_font () = - decr font_size; + decr font_size; change_font (); (* GConfig.save () @@ -1511,8 +1515,18 @@ let edit_selected_row r = | S.File _file -> () | S.Proof_attempt a -> - M.edit_proof - (env_session()) sched ~default_editor:gconfig.default_editor a + let e = env_session () in +(* + let coq = { prover_name = "Coq" ; prover_version = "8.3pl3"; + prover_altern = "" } in + let c = e.Session.whyconf in + let p = Mprover.find coq (get_provers c) in + let time = Whyconf.timelimit (Whyconf.get_main c) in + Format.eprintf + "[debug] save_config %d: timelimit=%d ; editor for Coq=%s@." + 0 time p.editor; +*) + M.edit_proof e sched ~default_editor:gconfig.default_editor a | S.Transf _ -> () let edit_current_proof () = @@ -1695,7 +1709,7 @@ let () = (***************) - + (* to be run when a row in the tree view is selected *) let select_row r = let ind = goals_model#get ~row:r#iter ~column:index_column in diff --git a/src/session/session.ml b/src/session/session.ml index d454cff6cd6a7abbaf171e05e7056d76165e0979..15986b5fb06c09aec195d57a6819ea3aab46fdb5 100644 --- a/src/session/session.ml +++ b/src/session/session.ml @@ -119,10 +119,11 @@ type loaded_provers = loaded_prover option PHprover.t type 'a env_session = { env : Env.env; - whyconf : Whyconf.config; + mutable whyconf : Whyconf.config; loaded_provers : loaded_provers; session : 'a session} +let update_env_session_config e c = e.whyconf <- c (*************************) (** Iterators *) @@ -1138,6 +1139,8 @@ let load_prover eS prover = PHprover.add eS.loaded_provers prover r; r +let unload_provers eS = PHprover.clear eS.loaded_provers + let () = Exn_printer.register (fun fmt exn -> match exn with diff --git a/src/session/session.mli b/src/session/session.mli index 12edfabbbb3ff3fceae506b9009fb5cd0f57cad1..391d52f505fafad807f4d0d58bc661011fe12725 100644 --- a/src/session/session.mli +++ b/src/session/session.mli @@ -173,13 +173,20 @@ type loaded_provers = loaded_prover option PHprover.t type 'a env_session = private { env : Env.env; - whyconf : Whyconf.config; + mutable whyconf : Whyconf.config; loaded_provers : loaded_provers; session : 'a session} +val update_env_session_config : 'a env_session -> Whyconf.config -> unit +(** updates the configuration *) + val load_prover : 'a env_session -> Whyconf.prover -> loaded_prover option (** load a prover *) +val unload_provers : 'a env_session -> unit +(** forces unloading of all provers, + to force reading again the configuration *) + (** {2 Update session} *) type 'key keygen = ?parent:'key -> unit -> 'key