Nous avons procédé ce jeudi matin 08 avril 2021 à une MAJ de sécurité urgente. Nous sommes passé de la version 13.9.3 à la version 13.9.5 les releases notes correspondantes sont ici:
https://about.gitlab.com/releases/2021/03/17/security-release-gitlab-13-9-4-released/
https://about.gitlab.com/releases/2021/03/31/security-release-gitlab-13-10-1-released/

Commit f6e83a16 authored by MARCHE Claude's avatar MARCHE Claude

Why3shell: load a file + print a goal

parent ee32c786
......@@ -33,6 +33,12 @@ type controller =
controller_provers : (Whyconf.config_prover * Driver.driver) Whyconf.Hprover.t;
}
let create_controller s = {
controller_session = s;
controller_provers = Whyconf.Hprover.create 7;
}
module type Scheduler = sig
val timeout: ms:int -> (unit -> bool) -> unit
......@@ -163,7 +169,7 @@ let timeout_handler () =
build_prover_call c id pr timelimit callback
with e when not (Debug.test_flag Debug.stack_trace) ->
Format.eprintf
"@[Exception raise in Controller_itp.build_prover_call:@ %a@.@]"
"@[Exception raised in Controller_itp.build_prover_call:@ %a@.@]"
Exn_printer.exn_printer e;
callback (InternalFailure e)
done;
......
......@@ -49,12 +49,14 @@ module type Scheduler = sig
end
type controller =
type controller = private
{ controller_session : Session_itp.session;
(* controller_env : Env.env; *)
controller_provers : (Whyconf.config_prover * Driver.driver) Whyconf.Hprover.t;
}
val create_controller : Session_itp.session -> controller
module Make(S : Scheduler) : sig
val schedule_proof_attempt :
......
......@@ -127,15 +127,21 @@ let provers : Whyconf.config_prover Whyconf.Mprover.t =
(* builds the environment from the [loadpath] *)
let env : Env.env = Env.create_env (Whyconf.loadpath main)
let ses =
module C = Why3.Controller_itp.Make(Unix_scheduler)
let cont =
if Queue.is_empty files then Why3.Whyconf.Args.exit_with_usage spec usage_str;
let fname = Queue.pop files in
ref (Why3.Session_itp.load_session fname)
let cont = Controller_itp.{
controller_session = !ses;
controller_provers = Whyconf.Hprover.create 7;
}
let ses =
if Filename.check_suffix fname ".xml" then
Session_itp.load_session fname
else
let ses = Session_itp.empty_session () in
C.add_file_to_session env ses fname;
ses
in
Controller_itp.create_controller ses
(* loading the drivers *)
let () =
......@@ -162,9 +168,6 @@ let alt_ergo =
end else
snd (Whyconf.Mprover.choose provers)
module C = Why3.Controller_itp.Make(Unix_scheduler)
let test_idle fmt _args =
Unix_scheduler.idle
~prio:0
......@@ -204,12 +207,12 @@ let list_transforms _fmt _args =
(List.sort sort_pair l)
let dump_session_raw fmt _args =
fprintf fmt "%a@." Session_itp.print_session !ses
fprintf fmt "%a@." Session_itp.print_session cont.Controller_itp.controller_session
let test_schedule_proof_attempt fmt _args =
(* temporary : get the first goal *)
let id =
match Session_itp.get_theories !ses with
match Session_itp.get_theories cont.Controller_itp.controller_session with
| (_n, (_thn, x::_)::_)::_ -> x
| _ -> assert false
in
......@@ -227,6 +230,18 @@ let test_schedule_proof_attempt fmt _args =
cont id alt_ergo.Whyconf.prover
~limit ~callback
let task_driver = Driver.load_driver env "drivers/why3_itp.drv" []
let test_print_goal fmt _args =
(* temporary : get the first goal *)
let id =
match Session_itp.get_theories cont.Controller_itp.controller_session with
| (_n, (_thn, x::_)::_)::_ -> x
| _ -> assert false
in
let task = Session_itp.get_task cont.Controller_itp.controller_session id in
Driver.print_task ~cntexample:false task_driver fmt task
let commands =
[
"list-provers", "list available provers", list_provers;
......@@ -235,7 +250,8 @@ let commands =
"i", "run a simple test of Unix_scheduler.idle", test_idle;
"a", "run a simple test of Unix_scheduler.timeout", test_timeout;
"p", "print the session in raw form", dump_session_raw;
"t", "test schedule_proof_attempt on the first goal", test_schedule_proof_attempt;
"t", "test schedule_proof_attempt with alt-ergo on the first goal", test_schedule_proof_attempt;
"g", "prints the first goal", test_print_goal;
]
let commands_table = Stdlib.Hstr.create 17
......
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