Commit 01d6d03f authored by MARCHE Claude's avatar MARCHE Claude

Do not fail anymore when undetected provers are in the XML databas

parent 9971a6b6
......@@ -24,16 +24,8 @@ open Rc
open Whyconf
type prover_data = Session.prover_data
(*
{ prover_id : string;
prover_name : string;
prover_version : string;
command : string;
driver_name : string;
driver : Driver.driver;
mutable editor : string;
}
type prover_data = Session.prover_data
*)
type t =
......@@ -45,7 +37,9 @@ type t =
mutable mem_limit : int;
mutable verbose : int;
mutable max_running_processes : int;
(*
mutable provers : prover_data Util.Mstr.t;
*)
mutable default_editor : string;
mutable show_labels : bool;
mutable env : Env.env;
......@@ -109,9 +103,8 @@ let load_config config =
verbose = ide.ide_verbose;
max_running_processes = Whyconf.running_provers_max main;
(*
provers = Mstr.fold (get_prover_data env) provers [];
*)
provers = Mstr.empty;
*)
default_editor = ide.ide_default_editor;
show_labels = false;
config = config;
......@@ -127,7 +120,7 @@ let read_config () =
exit 1
let save_config t =
let save_prover _ pr acc =
let _save_prover _ pr acc =
Mstr.add pr.Session.prover_id
{
Whyconf.name = pr.Session.prover_name;
......@@ -149,8 +142,10 @@ let save_config t =
let ide = set_int ide "verbose" t.verbose in
let ide = set_string ide "default_editor" t.default_editor 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
let config =
......@@ -409,9 +404,11 @@ let preferences c =
let run_auto_detection gconfig =
let config = Autodetection.run_auto_detection gconfig.config in
gconfig.config <- config;
let provers = get_provers config in
let _provers = get_provers config in
(* TODO: store the result differently
gconfig.provers <- Mstr.fold (Session.get_prover_data gconfig.env) provers Mstr.empty
*)
()
let () = eprintf "end of configuration initialization@."
......
......@@ -19,16 +19,8 @@
open Why
type prover_data = Session.prover_data
(*
{ prover_id : string;
prover_name : string;
prover_version : string;
command : string;
driver_name : string;
driver : Driver.driver;
mutable editor : string;
}
type prover_data = Session.prover_data
*)
type t =
......@@ -40,7 +32,9 @@ type t =
mutable mem_limit : int;
mutable verbose : int;
mutable max_running_processes : int;
(*
mutable provers : prover_data Util.Mstr.t;
*)
mutable default_editor : string;
mutable show_labels : bool;
mutable env : Why.Env.env;
......
......@@ -149,11 +149,13 @@ let gconfig =
let c = Gconfig.config in
let loadpath = (Whyconf.loadpath (get_main ())) @ List.rev !includes in
c.env <- Lexer.create_env loadpath;
let provers = Whyconf.get_provers c.Gconfig.config in
c.provers <-
Util.Mstr.fold (Session.get_prover_data c.env) provers Util.Mstr.empty;
c
let provers =
let c = gconfig.Gconfig.config in
Util.Mstr.fold (Session.get_prover_data gconfig.Gconfig.env)
(Whyconf.get_provers c) Util.Mstr.empty
let () =
Whyconf.load_plugins (get_main ())
......@@ -424,7 +426,7 @@ end
module Model = struct
type proof_attempt =
{ prover : prover_data;
{ prover : Session.prover_data;
proof_goal : goal;
proof_row : GTree.row_reference;
proof_db : Db.proof_attempt;
......@@ -1140,7 +1142,7 @@ let rec reimport_any_goal parent gid gname t db_goal goal_obsolete =
(fun pid a ->
let pname = Db.prover_name pid in
try
let p = Util.Mstr.find pname gconfig.provers in
let p = Util.Mstr.find pname 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
......@@ -1888,7 +1890,7 @@ let () =
b#connect#pressed
~callback:(fun () -> prover_on_selected_goals p)
in ())
gconfig.provers
provers
in
add_refresh_provers add_item_provers;
add_item_provers ()
......
......@@ -111,9 +111,11 @@ let gconfig =
let c = Gconfig.config in
let loadpath = (Whyconf.loadpath (get_main ())) @ List.rev !includes in
c.env <- Lexer.create_env loadpath;
(*
let provers = Whyconf.get_provers c.Gconfig.config in
c.provers <-
Util.Mstr.fold (Session.get_prover_data c.env) provers Util.Mstr.empty;
*)
c
let () =
......@@ -480,8 +482,13 @@ let init =
| 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.Proof_attempt a ->
begin
match a.M.prover with
| M.Detected_prover p ->
p.Session.prover_name ^ " " ^ p.Session.prover_version
| M.Undetected_prover s -> s
end
| M.Transformation tr -> Session.transformation_id tr.M.transf);
notify any
......@@ -526,7 +533,9 @@ let () =
let () =
try
eprintf "Opening session...@?";
M.open_session ~env:gconfig.env ~provers:gconfig.provers
M.open_session ~env:gconfig.env
(* ~provers:gconfig.provers *)
~config:gconfig.Gconfig.config
~init ~notify project_dir;
M.maximum_running_proofs := gconfig.max_running_processes;
eprintf " done@."
......@@ -921,7 +930,7 @@ let () =
b#connect#pressed
~callback:(fun () -> prover_on_selected_goals p)
in ())
gconfig.provers
(M.get_provers ())
in
add_refresh_provers add_item_provers;
add_item_provers ()
......@@ -1145,7 +1154,7 @@ let reload () =
try
erase_color_loc source_view;
current_file := "";
M.reload_all gconfig.provers
M.reload_all ()
with
| e ->
let e = match e with
......
......@@ -149,13 +149,18 @@ let init =
incr cpt;
Hashtbl.add model_index !cpt any;
*)
let name =
let _name =
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.Proof_attempt a ->
begin
match a.M.prover with
| M.Detected_prover p ->
p.Session.prover_name ^ " " ^ p.Session.prover_version
| M.Undetected_prover s -> s
end
| M.Transformation tr -> Session.transformation_id tr.M.transf
in
(* eprintf "Item '%s' loaded@." name *)
......@@ -229,7 +234,7 @@ let project_dir =
let main () =
try
eprintf "Opening session...@?";
M.open_session ~env ~provers ~init ~notify project_dir;
M.open_session ~env ~config ~init ~notify project_dir;
M.maximum_running_proofs :=
Whyconf.running_provers_max (Whyconf.get_main config);
eprintf " done@.";
......
This diff is collapsed.
......@@ -34,11 +34,13 @@ type prover_data = private
}
(** record of necessary data for a given external prover *)
(* stays here until old IDE is deleted *)
val get_prover_data :
Env.env -> Util.Mstr.key -> Whyconf.config_prover ->
prover_data Util.Mstr.t -> prover_data Util.Mstr.t
(** loads all provers from the current configuration *)
(** {2 Transformation's data} *)
type transformation_data
......@@ -119,8 +121,12 @@ module Make(O: OBSERVER) : sig
val goal_expanded : goal -> bool
val set_goal_expanded : goal -> bool -> unit
type prover_option =
| Detected_prover of prover_data
| Undetected_prover of string
type proof_attempt = private
{ prover : prover_data;
{ prover : prover_option;
proof_goal : goal;
proof_key : O.key;
mutable proof_state : proof_attempt_status;
......@@ -165,7 +171,10 @@ module Make(O: OBSERVER) : sig
val open_session :
env:Env.env ->
(*
provers:prover_data Util.Mstr.t ->
*)
config:Whyconf.config ->
init:(O.key -> any -> unit) ->
notify:(any -> unit) ->
string -> unit
......@@ -183,6 +192,8 @@ module Make(O: OBSERVER) : sig
*)
val get_provers : unit -> prover_data Util.Mstr.t
val maximum_running_proofs : int ref
val save_session : unit -> unit
......@@ -236,7 +247,7 @@ module Make(O: OBSERVER) : sig
When finished, calls the callback with argument true if there is at least one difference, false otherwise
*)
val reload_all: prover_data Util.Mstr.t -> unit
val reload_all: unit -> unit
(** reloads all the files
If for one of the file, the parsing or typing fails, then
the complete old session state is kept, and an exception
......
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