Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

Commit 861c6c77 authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

New incomplete why3shell.

Factor debug protocol functions.
Remade printing work for why3shell.
The Zipper was removed.
parent 7e478a08
......@@ -167,7 +167,7 @@ LIBGENERATED = src/util/config.ml \
LIB_UTIL = config bigInt util opt lists strings \
extmap extset exthtbl weakhtbl \
hashcons stdlib exn_printer pp json debug loc lexlib print_tree \
cmdline warning sysutil rc plugin bigInt number pqueue unix_scheduler
cmdline warning sysutil rc plugin bigInt number pqueue
LIB_CORE = ident ty term pattern decl theory \
task pretty dterm env trans printer model_parser
......@@ -835,7 +835,7 @@ install_local:: bin/why3session
# Why3 Shell
###############
SHELL_FILES = why3shell
SHELL_FILES = unix_scheduler why3shell
SHELLMODULES = $(addprefix src/why3shell/, $(SHELL_FILES))
......
......@@ -19,34 +19,15 @@ module Protocol_why3ide = struct
let print_request_debug r =
Debug.dprintf debug_proto "[request]";
Debug.dprintf debug_proto "%a" print_request r
let print_msg_debug m = match m with
| Proof_error (_ids, s) -> Debug.dprintf debug_proto "proof error %s" s
| Transf_error (_ids, s) -> Debug.dprintf debug_proto "transf error %s" s
| Strat_error (_ids, s) -> Debug.dprintf debug_proto "start error %s" s
| Replay_Info s -> Debug.dprintf debug_proto "replay info %s" s
| Query_Info (_ids, s) -> Debug.dprintf debug_proto "query info %s" s
| Query_Error (_ids, s) -> Debug.dprintf debug_proto "query error %s" s
| Help _s -> Debug.dprintf debug_proto "help"
| Information s -> Debug.dprintf debug_proto "info %s" s
| Task_Monitor _ -> Debug.dprintf debug_proto "task montor"
| Error s -> Debug.dprintf debug_proto "%s" s
Debug.dprintf debug_proto "%a@." print_request r
let print_msg_debug m =
Debug.dprintf debug_proto "[message]";
Debug.dprintf debug_proto "%a@." print_msg m
let print_notify_debug n =
Debug.dprintf debug_proto "[notification]";
match n with
| Node_change (_ni, _nf) -> Debug.dprintf debug_proto "node change"
| New_node (_ni, _pni, _nt, _nf) -> Debug.dprintf debug_proto "new node"
| Remove _ni -> Debug.dprintf debug_proto "remove"
| Initialized _gi -> Debug.dprintf debug_proto "initialized"
| Saved -> Debug.dprintf debug_proto "saved"
| Message msg ->
Debug.dprintf debug_proto "[message] ";
print_msg_debug msg
| Dead s -> Debug.dprintf debug_proto "dead :%s" s
| Proof_update (_ni, _pas) -> Debug.dprintf debug_proto "proof update"
| Task (_ni, _s) -> Debug.dprintf debug_proto "task"
Debug.dprintf debug_proto "%a@." print_notify n
let list_requests: ide_request list ref = ref []
......
......@@ -75,6 +75,7 @@ type request_type =
| Replay_req
| Exit_req
(* Debugging functions *)
let print_request fmt r =
match r with
| Command_req s -> fprintf fmt "command \"%s\"" s
......@@ -90,6 +91,32 @@ let print_request fmt r =
| Replay_req -> fprintf fmt "replay"
| Exit_req -> fprintf fmt "exit"
let print_msg fmt m =
match m with
| Proof_error (_ids, s) -> fprintf fmt "proof error %s" s
| Transf_error (_ids, s) -> fprintf fmt "transf error %s" s
| Strat_error (_ids, s) -> fprintf fmt "start error %s" s
| Replay_Info s -> fprintf fmt "replay info %s" s
| Query_Info (_ids, s) -> fprintf fmt "query info %s" s
| Query_Error (_ids, s) -> fprintf fmt "query error %s" s
| Help _s -> fprintf fmt "help"
| Information s -> fprintf fmt "info %s" s
| Task_Monitor _ -> fprintf fmt "task montor"
| Error s -> fprintf fmt "%s" s
let print_notify fmt n =
match n with
| Node_change (_ni, _nf) -> fprintf fmt "node change"
| New_node (_ni, _pni, _nt, _nf) -> fprintf fmt "new node"
| Remove _ni -> fprintf fmt "remove"
| Initialized _gi -> fprintf fmt "initialized"
| Saved -> fprintf fmt "saved"
| Message msg ->
print_msg fmt msg
| Dead s -> fprintf fmt "dead :%s" s
| Proof_update (_ni, _pas) -> fprintf fmt "proof update"
| Task (_ni, _s) -> fprintf fmt "task"
type ide_request = request_type * node_ID
open Session_itp
......@@ -525,20 +552,24 @@ exception Bad_prover_name of prover
| Replay_req -> replay_session (); resend_the_tree ()
| Command_req cmd ->
begin
match any_from_node_ID nid with
| APn pn_id ->
begin
match (interp config cont (Some pn_id) cmd) with
| Transform (s, _t, args) -> treat_request (Transform_req (s, args), nid)
| Query s -> P.notify (Message (Query_Info (nid, s)))
| Prove (p, limit) -> schedule_proof_attempt nid p limit
| Strategies st -> run_strategy_on_task nid st
| Help_message s -> P.notify (Message (Help s))
| QError s -> P.notify (Message (Query_Error (nid, s)))
| Other (s, _args) ->
if nid = 0 then
(* root_node is not in any_from_node_ID table *)
P.notify (Message (Information "Should be done on a proof node"))
else
match any_from_node_ID nid with
| APn pn_id ->
begin
match (interp config cont (Some pn_id) cmd) with
| Transform (s, _t, args) -> treat_request (Transform_req (s, args), nid)
| Query s -> P.notify (Message (Query_Info (nid, s)))
| Prove (p, limit) -> schedule_proof_attempt nid p limit
| Strategies st -> run_strategy_on_task nid st
| Help_message s -> P.notify (Message (Help s))
| QError s -> P.notify (Message (Query_Error (nid, s)))
| Other (s, _args) ->
P.notify (Message (Information ("Unknown command"^s)))
end
| _ ->
end
| _ ->
P.notify (Message (Information "Should be done on a proof node"))
(* TODO make it an error *)
end
......
......@@ -87,6 +87,8 @@ type request_type =
| Exit_req
val print_request: Format.formatter -> request_type -> unit
val print_msg: Format.formatter -> message_notification -> unit
val print_notify: Format.formatter -> notification -> unit
(* TODO: change to request_type * node_ID list ? *)
type ide_request = request_type * node_ID
......
......@@ -55,7 +55,7 @@ module Unix_scheduler = struct
while true do
if !print_prompt then begin
prompt_delay := !prompt_delay + 1;
if !prompt_delay = 2 then begin
if !prompt_delay = 1 then begin
Format.printf "%s@?" !prompt;
prompt_delay := 0;
print_prompt := false;
......
......@@ -15,4 +15,6 @@ module Unix_scheduler : sig
registered at the same time. Functions registered with higher
priority will be called first. *)
val main_loop: (string -> 'a) -> unit
end
(*
(* TODO *)
let proof_general = true
(*
module Unix_scheduler = struct
(* the private list of functions to call on idle, sorted higher
priority first. *)
let idle_handler = ref []
(* [insert_idle_handler p f] inserts [f] as a new function to call
on idle, with priority [p] *)
let insert_idle_handler p f =
let rec aux l =
match l with
| [] -> [p,f]
| (p1,_) as hd :: rem ->
if p > p1 then (p,f) :: l else hd :: aux rem
in
idle_handler := aux !idle_handler
(* the private list of functions to call on timeout, sorted on
earliest trigger time first. *)
let timeout_handler = ref []
(* [insert_timeout_handler ms t f] inserts [f] as a new function to call
on timeout, with time step of [ms] and first call time as [t] *)
let insert_timeout_handler ms t f =
let rec aux l =
match l with
| [] -> [ms,t,f]
| (_,t1,_) as hd :: rem ->
if t < t1 then (ms,t,f) :: l else hd :: aux rem
in
timeout_handler := aux !timeout_handler
(* public function to register a task to run on idle *)
let idle ~(prio:int) (f: unit -> bool) : unit =
insert_idle_handler prio f
(* public function to register a task to run on timeout *)
let timeout ~(ms:int) (f: unit -> bool) : unit =
assert (ms > 0);
let ms = float ms /. 1000.0 in
let time = Unix.gettimeofday () in
insert_timeout_handler ms (time +. ms) f
(* buffer for storing character read on stdin *)
let buf = Bytes.create 256
let prompt_delay = ref 0
let print_prompt = ref true
let prompt = ref "> "
(* [main_loop interp] starts the scheduler. On idle, standard input is
read. When a complete line is read from stdin, it is passed
as a string to the function [interp] *)
let main_loop interp =
try
while true do
if !print_prompt then begin
prompt_delay := !prompt_delay + 1;
if !prompt_delay = 2 then begin
Format.printf "%s@?" !prompt;
prompt_delay := 0;
print_prompt := false;
end
end;
(* attempt to run the first timeout handler *)
(let time = Unix.gettimeofday () in
match !timeout_handler with
| (ms,t,f) :: rem when t <= time ->
timeout_handler := rem;
let b = f () in
let time = Unix.gettimeofday () in
if b then insert_timeout_handler ms (ms +. time) f
| _ ->
(* time is not yet passed *)
(* attempt to run the first idle handler *)
match !idle_handler with
| (p,f) :: rem ->
idle_handler := rem;
let b = f () in
if b then insert_idle_handler p f
| [] ->
(* no idle handler *)
(* check stdin for a some delay *)
let delay =
match !timeout_handler with
| [] -> 0.125
(* 1/8 second by default *)
| (_,t,_) :: _ -> t -. time
(* or the time left until the next timeout otherwise *)
in
let a,_,_ = Unix.select [Unix.stdin] [] [] delay in
match a with
| [_] ->
let n = Unix.read Unix.stdin buf 0 256 in
interp (Bytes.sub_string buf 0 (n-1));
print_prompt := true
| [] -> () (* nothing read *)
| _ -> assert false);
done
with Exit -> ()
(* TODO
- detached theories
- obsolete
- update proof attempt
*)
open Why3
open Unix_scheduler
open Format
open Itp_server
(*************************)
(* Protocol of the shell *)
(*************************)
module Protocol_shell = struct
let debug_proto = Debug.register_flag "shell_proto"
~desc:"Print@ debugging@ messages@ about@ Why3Ide@ protocol@"
let print_request_debug r =
Debug.dprintf debug_proto "[request]";
Debug.dprintf debug_proto "%a" print_request r
let print_msg_debug m =
Debug.dprintf debug_proto "[message]";
Debug.dprintf debug_proto "%a@." print_msg m
let print_notify_debug n =
Debug.dprintf debug_proto "[notification]";
Debug.dprintf debug_proto "%a@." print_notify n
let list_requests: ide_request list ref = ref []
let get_requests () =
if List.length !list_requests > 0 then
Debug.dprintf debug_proto "get requests@.";
let l = List.rev !list_requests in
list_requests := [];
l
let send_request r =
print_request_debug (fst r);
Debug.dprintf debug_proto "@.";
list_requests := r :: !list_requests
let notification_list: notification list ref = ref []
let notify n =
print_notify_debug n;
Debug.dprintf debug_proto "@.";
notification_list := n :: !notification_list
let get_notified () =
if List.length !notification_list > 0 then
Debug.dprintf debug_proto "get notified@.";
let l = List.rev !notification_list in
notification_list := [];
l
end
*)
let get_notified = Protocol_shell.get_notified
let send_request = Protocol_shell.send_request
module Server = Itp_server.Make (Unix_scheduler) (Protocol_shell)
(************************)
(* parsing command line *)
(************************)
open Why3
open Unix_scheduler
open Session_user_interface
open Format
(* files of the current task *)
let files = Queue.create ()
......@@ -126,578 +80,263 @@ let usage_str = Format.sprintf
"Usage: %s [options] [ <file.xml> | <f1.why> <f2.mlw> ...]"
(Filename.basename Sys.argv.(0))
(* build command line *)
let config, base_config, env =
Why3.Whyconf.Args.initialize spec (fun f -> Queue.add f files) usage_str
let main : Whyconf.main = Whyconf.get_main config
(* all the provers detected, from the config file *)
let provers : Whyconf.config_prover Whyconf.Mprover.t =
Whyconf.get_provers config
(* builds the environment from the [loadpath] *)
(*let env : Env.env = Env.create_env (Whyconf.loadpath main)*)
(* -- declare provers -- *)
(* Return the prover corresponding to given name. name is of the form
| name
| name, version
| name, altern
| name, version, altern *)
let return_prover fmt name =
let fp = Whyconf.parse_filter_prover name in
(** all provers that have the name/version/altern name *)
let provers = Whyconf.filter_provers config fp in
if Whyconf.Mprover.is_empty provers then begin
fprintf fmt "Prover corresponding to %s has not been found@." name;
None
end else
Some (snd (Whyconf.Mprover.choose provers))
(* -- init controller -- *)
let cont =
Session_user_interface.cont_from_files spec usage_str env files provers
module C = Why3.Controller_itp.Make(Unix_Scheduler)
let () = C.set_max_tasks (Whyconf.running_provers_max main)
(* -- -- *)
let test_idle fmt _args =
Unix_Scheduler.idle
~prio:0
(fun () -> fprintf fmt "idle@."; false)
let test_timeout fmt _args =
Unix_Scheduler.timeout
~ms:1000
(let c = ref 10 in
fun () -> decr c;
if !c > 0 then
(fprintf fmt "%d@." !c; true)
else
(fprintf fmt "boom!@."; false))
let list_provers _fmt _args =
let l =
Whyconf.Hprover.fold
(fun p _ acc -> (Pp.sprintf "%a" Whyconf.print_prover p)::acc)
cont.Controller_itp.controller_provers
[]
in
let l = List.sort String.compare l in
printf "@[<hov 2>== Known provers ==@\n%a@]@."
(Pp.print_list Pp.newline Pp.string) l
let sort_pair (x,_) (y,_) = String.compare x y
let list_transforms _fmt _args =
let l =
List.rev_append (Trans.list_transforms ()) (Trans.list_transforms_l ())
in
let print_trans_desc fmt (x,r) =
fprintf fmt "@[<hov 2>%s@\n@[<hov>%a@]@]" x Pp.formatted r in
printf "@[<hov 2>== Known transformations ==@\n%a@]@\n@."
(Pp.print_list Pp.newline2 print_trans_desc)
(List.sort sort_pair l)
open Controller_itp
open Session_itp
(* _____________________________________________________________________ *)
(* -------------------- zipper ----------------------------------------- *)
type proof_hole =
Th of theory list * theory * theory list |
Pn of proofNodeID list * proofNodeID * proofNodeID list |
Tn of transID list * transID * transID list
type proof_zipper = { mutable cursor : proof_hole; ctxt : proof_hole Stack.t }
let ctxt = Stack.create ()
(* Parse files *)
let () = Whyconf.Args.parse spec (fun f -> Queue.add f files) usage_str;
if Queue.is_empty files then
Whyconf.Args.exit_with_usage spec usage_str
(*************************)
(* Notification Handling *)
(*************************)
let treat_message_notification fmt msg = match msg with
(* TODO: do something ! *)
| Proof_error (_id, s) -> fprintf fmt "%s@." s
| Transf_error (_id, s) -> fprintf fmt "%s@." s
| Strat_error (_id, s) -> fprintf fmt "%s@." s
| Replay_Info s -> fprintf fmt "%s@." s
| Query_Info (_id, s) -> fprintf fmt "%s@." s
| Query_Error (_id, s) -> fprintf fmt "%s@." s
| Help s -> fprintf fmt "%s@." s
| Information s -> fprintf fmt "%s@." s
| Task_Monitor (_t, _s, _r) -> () (* TODO do we want to print something for this? *)
| Error s ->
fprintf fmt "%s@." s
type shell_node_type =
| SRoot
| SFile
| STheory
| STransformation
| SGoal
| SProofAttempt
(* TODO will evolve *)
type node_info = { proved: bool }
type node = {
node_ID: node_ID;
node_parent: node_ID;
node_name: string;
mutable node_task: string option;
node_proof: Controller_itp.proof_attempt_status option;
node_trans_args: string list option;
node_type: shell_node_type;
mutable node_info: node_info;
mutable children_nodes: node_ID list
}
let root_node_ID = root_node
let max_ID = ref 1
let root_node = {
node_ID = root_node_ID;
node_parent = root_node_ID;
node_name = "root";
node_task = None;
node_proof = None;
node_trans_args = None;
node_type = SRoot;
node_info = {proved = false};
children_nodes = []
}
open Stdlib
open Format
let zipper =
let files =
get_files cont.Controller_itp.controller_session
in
let file = ref None in
Stdlib.Hstr.iter (fun _ f -> file := Some f) files;
let file = Opt.get !file in
match file.file_theories with
| th :: tail -> { cursor = (Th ([], th, tail)); ctxt }
| _ -> assert false
let zipper_init () =
let files =
get_files cont.Controller_itp.controller_session
in
let file = ref None in
Stdlib.Hstr.iter (fun _ f -> file := Some f) files;
let file = Opt.get !file in
match file.file_theories with
| th :: tail -> zipper.cursor <- (Th ([], th, tail));
while not (Stack.is_empty zipper.ctxt) do ignore (Stack.pop zipper.ctxt) done
| _ -> assert false
let zipper_down () =
match zipper.cursor with
| Th (_,th,_) ->
(match theory_goals th with
| pn::l ->
Stack.push zipper.cursor zipper.ctxt;
zipper.cursor <- Pn ([],pn,l);
true
| _ -> false)
| Pn (_,pn,_) ->
(match get_transformations cont.controller_session pn with
| tn::l ->
Stack.push zipper.cursor zipper.ctxt;
zipper.cursor <- Tn ([],tn,l);
true
| _ -> false)
| Tn (_,tn,_) ->
(match get_sub_tasks cont.controller_session tn with
| pn::l ->
Stack.push zipper.cursor zipper.ctxt;
zipper.cursor <- Pn ([],pn,l);
true
| _ -> false)
let zipper_up () =
if not (Stack.is_empty zipper.ctxt) then begin
zipper.cursor <- Stack.pop zipper.ctxt;
true
end else
false
let zipper_right () =
match zipper.cursor with
| Th (l,cs,hd::r) ->
zipper.cursor <- Th (cs::l,hd,r);
true
| Pn (l,cs,hd::r) ->
zipper.cursor <- Pn (cs::l,hd,r);
true
| Tn (l,cs,hd::r) ->
zipper.cursor <- Tn (cs::l,hd,r);
true
| _ -> false
module Hnode = Hint
let nodes : node Hnode.t = Hnode.create 17
let () = Hnode.add nodes root_node_ID root_node
(* Current node_ID *)
let cur_id = ref root_node_ID
let print_goal fmt n =
let node = Hnode.find nodes n in
match node.node_task with
| None -> fprintf fmt "No goal@."
| Some s -> fprintf fmt "Goal is: \n %s@." s
let convert_to_shell_type t =
match t with
| NRoot -> SRoot
| NFile -> SFile
| NTheory -> STheory
| NTransformation -> STransformation
| NGoal -> SGoal
| NProofAttempt _ -> SProofAttempt
let return_proof_info (t: node_type) =
match t with
| NProofAttempt (_pr, _obs) ->
Some Controller_itp.Scheduled
| _ -> None
let zipper_left () =
match zipper.cursor with
| Th (hd::l,cs,r) ->
zipper.cursor <- Th (l,hd,cs::r);
true
| Pn (hd::l,cs,r) ->
zipper.cursor <- Pn (l,hd,cs::r);
true
| Tn (hd::l,cs,r) ->
zipper.cursor <- Tn (l,hd,cs::r);
true
let add_new_node fmt (n: node_ID) (parent: node_ID) (t: node_type) (i: Itp_server.node_info) =
let new_node = {
node_ID = n;
node_parent = parent;
node_name = i.Itp_server.name;
node_task = None;
node_proof = return_proof_info t;