Commit c3aa905c authored by MARCHE Claude's avatar MARCHE Claude

always save sessions using the current shape version

parent 3b45464e
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<why3session shape_version="5">
<prover id="3" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="Coq" version="8.7.1" timelimit="6" steplimit="0" memlimit="1000"/>
......
......@@ -223,18 +223,18 @@ let print_session fmt c =
find a corresponding new theory resp. old goal are kept, with
tasks associated to them *)
let reload_files (c : controller) ~use_shapes =
let reload_files (c : controller) ~shape_version =
let old_ses = c.controller_session in
c.controller_env <- Env.create_env (Env.get_loadpath c.controller_env);
Whyconf.Hprover.reset c.controller_provers;
load_drivers c;
c.controller_session <- empty_session ~from:old_ses (get_dir old_ses);
merge_files ~use_shapes c.controller_env c.controller_session old_ses
merge_files ~shape_version c.controller_env c.controller_session old_ses
exception Errors_list of exn list
let reload_files (c: controller) ~use_shapes =
let errors, b1, b2 = reload_files c ~use_shapes in
let reload_files (c: controller) ~shape_version =
let errors, b1, b2 = reload_files c ~shape_version in
match errors with
| [] -> b1, b2
| _ -> raise (Errors_list errors)
......
......@@ -110,8 +110,17 @@ val print_session : Format.formatter -> controller -> unit
exception Errors_list of exn list
val reload_files : controller -> use_shapes:bool -> bool * bool
(** reload the files of the given session:
val reload_files : controller -> shape_version:int option -> bool * bool
(** [reload_files] returns a pair [(o,d)]: [o] true means there are
obsolete goals, [d] means there are missed objects (goals,
transformations, theories or files) that are now detached in the
session returned.
If parsing or typing errors occurs, a list of errors is raised
inside exception Errors_list.
The detailed process of reloading the files of the given session is
as follows.
- each file is parsed again and theories/goals extracted from it. If
some syntax error or parsing error occurs, then the corresponding
......@@ -155,13 +164,7 @@ val reload_files : controller -> use_shapes:bool -> bool * bool
it, neither to its subgoals.
[reload_files] It returns a pair (o, d): o true means there are
obsolete goals, d means there are missed objects (goals, transformations,
theories or files) that are now detached in the session returned.
If parsing or typing errors occurs, a list of errors is raised inside
exception Errors_list.
*)
*)
val add_file : controller -> ?format:Env.fformat -> string -> unit
(** [add_fil cont ?fmt fname] parses the source file
......
......@@ -595,10 +595,10 @@ end
(* Reload_files that is used even if the controller is not correct. It can
be incorrect and end up in a correct state. *)
let reload_files cont ~use_shapes =
let reload_files cont ~shape_version =
capture_parse_or_type_errors
(fun c ->
try let (_,_) = reload_files ~use_shapes c in [] with
try let (_,_) = reload_files ~shape_version c in [] with
| Errors_list le -> le) cont
let add_file cont ?format fname =
......@@ -971,7 +971,7 @@ end
let init_server ?(send_source=true) config env f =
Debug.dprintf debug "loading session %s@." f;
let ses,use_shapes = Session_itp.load_session f in
let ses,shape_version = Session_itp.load_session f in
Debug.dprintf debug "creating controller@.";
let c = create_controller config env ses in
let shortcuts =
......@@ -1011,7 +1011,7 @@ end
};
Debug.dprintf debug "reloading source files@.";
let d = get_server_data () in
let x = reload_files d.cont ~use_shapes in
let x = reload_files d.cont ~shape_version in
reset_and_send_the_whole_tree ();
(* After initial sending, we don't check anymore that there is a need to
focus on a specific node. *)
......@@ -1273,7 +1273,9 @@ end
let _old_focus = !focused_node in
unfocus ();
clear_tables ();
let l = reload_files d.cont ~use_shapes:true in
let l = reload_files d.cont
~shape_version:(Some Termcode.current_shape_version)
in
reset_and_send_the_whole_tree ();
match l with
| [] ->
......
This diff is collapsed.
......@@ -169,8 +169,9 @@ val read_file :
signaled with exceptions. *)
val merge_files :
use_shapes:bool -> Env.env -> session -> session -> exn list * bool * bool
(** [merge_files ~use_shapes env ses old_ses] merges the file sections
shape_version:int option ->
Env.env -> session -> session -> exn list * bool * bool
(** [merge_files ~use_shape_version env ses old_ses] merges the file sections
of session [s] with file sections of the same name in old session
[old_ses]. Recursively, for each theory whose name is identical to
old theories, it is attempted to associate the old goals,
......@@ -221,11 +222,11 @@ val mark_obsolete: session -> proofAttemptID -> unit
val save_session : session -> unit
(** [save_session s] Save the session [s] *)
val load_session : string -> session * bool
val load_session : string -> session * int option
(** [load_session dir] load a session in directory [dir]; all the
tasks are initialised to None
The returned boolean is set when there was shapes read from disk.
The second result is the shape version read from disk, if any
raises [SessionFileError msg] if the database file cannot be read
correctly.
......
......@@ -384,12 +384,12 @@ let () =
Whyconf.Args.exit_with_usage option_list usage_msg;
try
Debug.dprintf debug "Opening session '%s'...@?" dir;
let ses,use_shapes = S.load_session dir in
let ses,shape_version = S.load_session dir in
let cont = Controller_itp.create_controller config env ses in
(* update the session *)
let found_obs, found_detached =
try
Controller_itp.reload_files cont ~use_shapes
Controller_itp.reload_files cont ~shape_version
with
| Controller_itp.Errors_list l ->
List.iter (fun e -> Format.eprintf "%a@." Exn_printer.exn_printer e) l;
......
......@@ -78,7 +78,7 @@ let read_session fname =
S.load_session project_dir
let read_update_session ~allow_obsolete env config fname =
let session,use_shapes = read_session fname in
let session,shape_version = read_session fname in
(*
let ctxt = S.mk_update_context
~allow_obsolete_goals:allow_obsolete
......@@ -90,7 +90,7 @@ let read_update_session ~allow_obsolete env config fname =
let cont = Controller_itp.create_controller config env session in
let found_obs, some_merge_miss =
try
Controller_itp.reload_files cont ~use_shapes
Controller_itp.reload_files cont ~shape_version
with
| Controller_itp.Errors_list l ->
List.iter (fun e -> Format.eprintf "%a@." Exn_printer.exn_printer e) l;
......
......@@ -44,7 +44,10 @@ val common_options : spec_list
val read_env_spec : unit -> Env.env * Whyconf.config * bool
(** read_simple_spec also *)
val read_session : string -> Session_itp.session * bool
val read_session : string -> Session_itp.session * int option
(** [read_session s] reads the session file [s] and returns a pair
[(ses,shape_version)] where [ses] is the session structure (without
any tasks) and [shape_version] indicates the shapes version, if any *)
val read_update_session :
allow_obsolete:bool -> Env.env ->
......
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