Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

Commit 38ac7eb5 authored by Sylvain Dailler's avatar Sylvain Dailler

Added initialization of controller.

Controller is now dummy until the first open request is given.
parent 9b299112
......@@ -59,7 +59,7 @@ type proof_state = {
pn_state : bool Hpn.t;
}
let init_proof_state _ses =
let init_proof_state () =
{th_state = Hid.create 7;
tn_state = Htn.create 42;
pn_state = Hpn.create 42}
......@@ -71,13 +71,16 @@ type controller =
controller_provers : (Whyconf.config_prover * Driver.driver) Whyconf.Hprover.t;
}
let create_controller env s = {
controller_session = s;
proof_state = init_proof_state s;
let create_controller env = {
controller_session = Session_itp.dummy_session;
proof_state = init_proof_state ();
controller_env = env;
controller_provers = Whyconf.Hprover.create 7;
}
let init_controller s c =
c.controller_session <- s
let tn_proved c tid = Htn.find_def c.proof_state.tn_state false tid
let pn_proved c pid = Hpn.find_def c.proof_state.pn_state false pid
let th_proved c th =
......
......@@ -78,7 +78,8 @@ type controller = private
controller_provers : (Whyconf.config_prover * Driver.driver) Whyconf.Hprover.t;
}
val create_controller : Env.env -> Session_itp.session -> controller
val create_controller: Env.env -> controller
val init_controller: Session_itp.session -> controller -> unit
(** Used to find if a proof/trans node or theory is proved or not *)
val tn_proved: controller -> Session_itp.transID -> bool
......
......@@ -47,6 +47,7 @@ type notification =
| Initialized of global_information
| Saved
| Message of message_notification
| Dead of string
type request_type =
| Command_req of string
......@@ -102,11 +103,11 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
"Usage: %s [options] [<file.why>|<project directory>]..."
(Filename.basename Sys.argv.(0))
(* Files are passed with request Open *)
let config, _base_config, env =
let c, b, e =
Whyconf.Args.initialize spec (fun f -> Queue.add f files) usage_str
Whyconf.Args.initialize [] (fun _ -> ()) ""
in
if Queue.is_empty files then Whyconf.Args.exit_with_usage spec usage_str;
c, b, e
let get_config () = config
......@@ -130,37 +131,26 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
strategies = strategies_list
}
(*
let get_global_information c =
{
provers = get_prover_list ();
transformations = get_transformation_list c;
strategies = get_strategies_list c;
(* Controller is not initialized: we cannot process any request *)
let init_controller = ref false
hidden_provers = config.????
provers : prover list;
transformations : transformation list;
strategies : strategy list;
hidden_provers : string list;
session_time_limit : int;
session_mem_limit : int;
session_nb_processes : int;
session_cntexample : bool;
main_dir : string
}
*)
(* Create_controller creates a dummy controller *)
let cont =
init_controller := false;
create_controller env
(* ------------ init controller ------------ *)
(* TODO: find a way to init cont only when requested (Open file request is send) *)
let cont =
(* Init cont is called only when an Open is requested *)
let init_cont f =
Queue.add f files;
try
(let cont =
Session_user_interface.cont_from_files spec usage_str env files provers in
P.notify (Initialized infos);
cont)
(Session_user_interface.cont_from_files cont spec usage_str env files provers;
init_controller := true;
P.notify (Initialized infos))
with e ->
Format.eprintf "%a@." Exn_printer.exn_printer e;
P.notify (Dead (Pp.string_of Exn_printer.exn_printer e));
exit 1
(* ----------------------------------- ------------------------------------- *)
......@@ -515,7 +505,11 @@ exception Bad_prover_name of prover
P.notify (Message (Information "Should be done on a proof node"))
(* TODO make it an error *)
end
| Open_req _file_name -> assert false (* Unsupported *)
| Open_req file_name ->
if !init_controller then
Controller_itp.add_file cont file_name
else
init_cont file_name
| Exit_req -> exit 0 (* TODO *)
......
......@@ -53,6 +53,8 @@ type notification =
(* the session was saved on disk *)
| Message of message_notification
(* an informative message, can be an error message *)
| Dead of string
(* server exited *)
type request_type =
| Command_req of string
......
......@@ -94,6 +94,20 @@ type session = {
session_prover_ids : int Hprover.t;
}
let dummy_session =
{
proofAttempt_table = Hint.create 23;
next_proofAttemptID = 0;
proofNode_table = Hint.create 23;
next_proofNodeID = 0;
trans_table = Hint.create 23;
next_transID = 0;
session_dir = "";
session_files = Hstr.create 23;
session_shape_version = 0;
session_prover_ids = Hprover.create 23
}
let theory_parent s th =
Hstr.find s.session_files th.theory_parent_name
......
......@@ -16,6 +16,7 @@ unique identifiers of type [proofNodeId]
type session
val dummy_session: session
type proofNodeID
val print_proofNodeID : Format.formatter -> proofNodeID -> unit
......
open Format
open Session_itp
open Controller_itp
(* TODO: raise exceptions instead of using explicit eprintf/exit *)
let cont_from_files spec usage_str env files provers =
let cont_from_files cont spec usage_str env files provers =
if Queue.is_empty files then Whyconf.Args.exit_with_usage spec usage_str;
let fname = Queue.peek files in
(* extract project directory, and create it if needed *)
......@@ -35,25 +34,23 @@ let cont_from_files spec usage_str env files provers =
let ses,use_shapes = load_session dir in
eprintf "using shapes: %a@." pp_print_bool use_shapes;
(* create the controller *)
let c = Controller_itp.create_controller env ses in
Controller_itp.init_controller ses cont;
(* update the session *)
Controller_itp.reload_files c env ~use_shapes;
Controller_itp.reload_files cont env ~use_shapes;
(* add files to controller *)
Queue.iter (fun fname -> Controller_itp.add_file c fname) files;
Queue.iter (fun fname -> Controller_itp.add_file cont fname) files;
(* load provers drivers *)
Whyconf.Mprover.iter
(fun _ p ->
try
let d = Driver.load_driver env p.Whyconf.driver [] in
Whyconf.Hprover.add c.Controller_itp.controller_provers p.Whyconf.prover (p,d)
Whyconf.Hprover.add cont.Controller_itp.controller_provers p.Whyconf.prover (p,d)
with e ->
let p = p.Whyconf.prover in
eprintf "Failed to load driver for %s %s: %a@."
p.Whyconf.prover_name p.Whyconf.prover_version
Exn_printer.exn_printer e)
provers;
(* return the controller *)
c
provers
(**********************************)
(* list unproven goal and related *)
......
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