Commit 49c19a38 authored by François Bobot's avatar François Bobot

new session

Split session in two :
Session : an API for managing session without running provers
Session_scheduler : an API for running provers asynchronously

All the global states have been removed.

A session must be first read, which give a session without task.
Afterward it must be updated to the current state of the files with
some environnement and configuration.

printer and iterator are provided for session.

Session_tools : some useful functions on session.

Smoke detector : not anymore integrated to session. Just add the
      transformation "smoke_detector_top" or "smoke_detector_deep" to
      all the valid proof attempt.

prover_id are not yet removed but all is in place in session for that.
parent af8d1edf
......@@ -111,7 +111,8 @@ plugins: plugins.@OCAMLBEST@
LIBGENERATED = src/util/rc.ml src/parser/lexer.ml \
src/parser/parser.mli src/parser/parser.ml \
src/driver/driver_parser.mli src/driver/driver_parser.ml \
src/driver/driver_lexer.ml src/coq_config.ml
src/driver/driver_lexer.ml src/coq_config.ml \
src/session/xml.ml
LIB_UTIL = stdlib exn_printer pp debug loc print_tree print_number \
cmdline hashweak hashcons util sysutil rc plugin
......@@ -138,15 +139,18 @@ LIB_TRANSFORM = simplify_recursive_definition simplify_formula \
LIB_PRINTER = alt_ergo why3printer smtv1 smtv2 coq simplify gappa \
cvc3 yices
LIB_SESSION = xml termcode session session_tools session_scheduler
LIBMODULES = src/config src/coq_config \
$(addprefix src/util/, $(LIB_UTIL)) \
$(addprefix src/core/, $(LIB_CORE)) \
$(addprefix src/parser/, $(LIB_PARSER)) \
$(addprefix src/driver/, $(LIB_DRIVER)) \
$(addprefix src/transform/, $(LIB_TRANSFORM)) \
$(addprefix src/printer/, $(LIB_PRINTER))
$(addprefix src/printer/, $(LIB_PRINTER)) \
$(addprefix src/session/, $(LIB_SESSION))
LIBDIRS = util core parser driver transform printer
LIBDIRS = util core parser driver transform printer session
LIBINCLUDES = $(addprefix -I src/, $(LIBDIRS))
ifeq (@enable_hypothesis_selection@,yes)
......@@ -542,7 +546,7 @@ install_local: bin/why3config
ifeq (@enable_ide@,yes)
IDE_FILES = xml termcode session gconfig gmain
IDE_FILES = gconfig gmain
IDEMODULES = $(addprefix src/ide/, $(IDE_FILES))
......@@ -578,7 +582,7 @@ bin/why3ide: bin/why3ide.@OCAMLBEST@
include .depend.ide
.depend.ide: src/ide/xml.ml
.depend.ide:
$(OCAMLDEP) -slash -I src -I src/ide $(IDEML) $(IDEMLI) > $@
depend: .depend.ide
......@@ -602,7 +606,7 @@ endif
# Replayer
###############
REPLAYER_FILES = xml termcode session replay
REPLAYER_FILES = replay
REPLAYERMODULES = $(addprefix src/ide/, $(REPLAYER_FILES))
......@@ -634,13 +638,12 @@ bin/why3replayer: bin/why3replayer.@OCAMLBEST@
include .depend.replayer
.depend.replayer: src/ide/xml.ml
.depend.replayer:
$(OCAMLDEP) -slash -I src -I src/ide $(REPLAYERML) $(REPLAYERMLI) > $@
depend: .depend.replayer
clean::
rm -f src/ide/xml.ml
rm -f src/ide/*.cm[iox] src/ide/*.o
rm -f src/ide/*.annot src/ide/*~
rm -f bin/why3replayer.byte bin/why3replayer.opt bin/why3replayer
......@@ -655,7 +658,7 @@ install_local: bin/why3replayer
# Stats
###############
STATS_FILES = xml termcode session session_ro stats
STATS_FILES = stats
STATSMODULES = $(addprefix src/ide/, $(STATS_FILES))
......@@ -687,7 +690,7 @@ bin/why3stats: bin/why3stats.@OCAMLBEST@
include .depend.stats
.depend.stats: src/ide/xml.ml
.depend.stats:
$(OCAMLDEP) -slash -I src -I src/ide $(STATSML) $(STATSMLI) > $@
depend: .depend.stats
......@@ -705,7 +708,7 @@ install_local: bin/why3stats
# Html
###############
HTML_FILES = xml termcode session session_ro html_session
HTML_FILES = html_session
HTMLMODULES = $(addprefix src/ide/, $(HTML_FILES))
......@@ -737,7 +740,7 @@ bin/why3html: bin/why3html.@OCAMLBEST@
include .depend.html
.depend.html: src/ide/xml.ml
.depend.html:
$(OCAMLDEP) -slash -I src -I src/ide $(HTMLML) $(HTMLMLI) > $@
depend: .depend.html
......@@ -1120,8 +1123,8 @@ test-api: src/why3.cma
ocaml -I src/ $(INCLUDES) $(EXTCMA) src/why3.cma examples/use_api.ml \
|| (printf "Test of Why API calls failed. Please fix it"; exit 2)
test-shape: src/why3.cma src/ide/termcode.cmo
ocaml -I src/ -I src/ide/ $(INCLUDES) $(EXTCMA) $? examples/test_shape.ml
test-shape: src/why3.cma
ocaml -I src/ $(INCLUDES) $(EXTCMA) $? examples/test_shape.ml
bts12244: src/why3.cma
ocaml -I src/ $(INCLUDES) $(EXTCMA) src/why3.cma examples/bts12244.ml
......@@ -1179,7 +1182,7 @@ MODULESTODOC = util/util util/hashweak \
core/ident core/ty core/term core/decl core/theory \
core/env core/task \
driver/whyconf driver/driver \
ide/session
session/session session/session_tools session/session_scheduler
# transform/introduction \
# ide/db
......
......@@ -282,6 +282,24 @@ let lookup_transform_l s =
let list_transforms () = Hashtbl.fold (fun k _ acc -> k::acc) transforms []
let list_transforms_l () = Hashtbl.fold (fun k _ acc -> k::acc) transforms_l []
(** fast transform *)
type gentrans =
| Trans_one of Task.task trans
| Trans_list of Task.task tlist
let lookup_trans env name =
try
let t = lookup_transform name env in
Trans_one t
with UnknownTrans _ ->
let t = lookup_transform_l name env in
Trans_list t
let apply_transform tr_name env task =
match lookup_trans env tr_name with
| Trans_one t -> [apply t task]
| Trans_list t -> apply t task
(** Flag-dependent transformations *)
exception UnknownFlagTrans of meta * string * string list
......
......@@ -127,3 +127,5 @@ val list_transforms_l : unit -> string list
val named : string -> 'a trans -> 'a trans
(** give transformation a name without registering *)
val apply_transform : string -> Env.env -> task -> task list
(** apply a registered 1-to-1 or a 1-to-n function directly *)
......@@ -99,7 +99,8 @@ let load_ide section =
ide_verbose =
get_int section ~default:default_ide.ide_verbose "verbose";
ide_intro_premises =
get_bool section ~default:default_ide.ide_intro_premises "intro_premises";
get_bool section ~default:default_ide.ide_intro_premises
"intro_premises";
ide_show_labels =
get_bool section ~default:default_ide.ide_show_labels "print_labels";
ide_show_locs =
......@@ -164,16 +165,6 @@ let load_config config =
}
let save_config t =
let _save_prover _ pr acc =
Mstr.add pr.Session.prover_id
{
Whyconf.name = pr.Session.prover_name;
command = pr.Session.command;
driver = pr.Session.driver_name;
version = pr.Session.prover_version;
editor = pr.Session.editor;
interactive = pr.Session.interactive;
} acc in
let config = t.config in
let config = set_main config
(set_limits (get_main config)
......@@ -269,7 +260,8 @@ let iconname_reload = "movefile32"
let iconname_remove = "deletefile32"
let iconname_cleaning = "trashb32"
let image_default = ref (GdkPixbuf.create ~width:1 ~height:1 ()) (** dumb pixbuf *)
let image_default = ref (GdkPixbuf.create ~width:1 ~height:1 ())
(** dumb pixbuf *)
let image_undone = ref !image_default
let image_scheduled = ref !image_default
let image_running = ref !image_default
......@@ -438,7 +430,8 @@ let preferences c =
*)
(* timelimit ? *)
let hb = GPack.hbox ~homogeneous:false ~packing:page1#add () in
let _ = GMisc.label ~text:"Time limit: " ~packing:(hb#pack ~expand:false) () in
let _ = GMisc.label ~text:"Time limit: "
~packing:(hb#pack ~expand:false) () in
let timelimit_spin = GEdit.spin_button ~digits:0 ~packing:hb#add () in
timelimit_spin#adjustment#set_bounds ~lower:2. ~upper:300. ~step_incr:1. ();
timelimit_spin#adjustment#set_value (float_of_int c.time_limit);
......@@ -448,7 +441,8 @@ let preferences c =
in
(* nb of processes ? *)
let hb = GPack.hbox ~homogeneous:false ~packing:page1#add () in
let _ = GMisc.label ~text:"Nb of processes: " ~packing:(hb#pack ~expand:false) () in
let _ = GMisc.label ~text:"Nb of processes: "
~packing:(hb#pack ~expand:false) () in
let nb_processes_spin = GEdit.spin_button ~digits:0 ~packing:hb#add () in
nb_processes_spin#adjustment#set_bounds
~lower:1. ~upper:16. ~step_incr:1. ();
......
This diff is collapsed.
......@@ -20,7 +20,6 @@
open Format
open Why3
let includes = ref []
let files = Queue.create ()
let opt_version = ref false
let output_dir = ref ""
......@@ -49,9 +48,6 @@ let set_opt_pp_in,set_opt_pp_cmd,set_opt_pp_out =
(fun s -> opt_pp := (!suf,(!cmd,s))::!opt_pp)
let spec = Arg.align [
("-I",
Arg.String (fun s -> includes := s :: !includes),
"<s> Add s to loadpath") ;
("-v",
Arg.Set opt_version,
" Print version information") ;
......@@ -112,13 +108,6 @@ let () =
(* List.iter (fun (in_,(cmd,out)) -> *)
(* printf "in : %s, cmd : %s, out : %s@." in_ cmd out) !opt_pp *)
let allow_obsolete = !allow_obsolete
let includes = List.rev !includes
open Session_ro
let env = read_config ~includes !opt_config
let () =
Debug.Opt.set_flags_selected ();
if Debug.Opt.option_list () then exit 0
......@@ -136,17 +125,20 @@ let output_dir =
let edited_dst = Filename.concat output_dir "edited"
let whyconf = Whyconf.read_config !opt_config
open Session
open Util
type context =
(string ->
(formatter -> Session_ro.session -> unit) -> Session_ro.session
(formatter -> notask session -> unit) -> notask session
-> unit, formatter, unit) format
let run_file (context : context) print_session f =
let session_path = get_project_dir f in
let basename = Filename.basename session_path in
let session = read_project_dir ~allow_obsolete ~env session_path in
let session = read_session session_path in
let cout = if output_dir = "-" then stdout else
open_out (Filename.concat output_dir (basename^".html")) in
let fmt = formatter_of_out_channel cout in
......@@ -163,44 +155,45 @@ struct
let print_prover fmt pd = fprintf fmt "%s" pd.prover_name
let print_proof_status fmt = function
| Undone -> fprintf fmt "Undone"
| Undone _ -> fprintf fmt "Undone"
| Done pr -> fprintf fmt "Done : %a" Call_provers.print_prover_result pr
| InternalFailure exn ->
fprintf fmt "Failure : %a"Exn_printer.exn_printer exn
let print_proof_attempt fmt pa =
fprintf fmt "<li>%a : %a</li>"
print_prover pa.prover
print_prover pa.proof_prover
print_proof_status pa.proof_state
let rec print_transf fmt tr =
fprintf fmt "<li>%s : <ul>%a</ul></li>"
tr.transf_name
(Pp.print_list Pp.newline print_goal) tr.subgoals
(Pp.print_list Pp.newline print_goal) tr.transf_goals
and print_goal fmt g =
fprintf fmt "<li>%s : <ul>%a%a</ul></li>"
g.goal_name
(Pp.print_iter2 Mstr.iter Pp.newline Pp.nothing
g.goal_name.Ident.id_string
(Pp.print_iter2 PHprover.iter Pp.newline Pp.nothing
Pp.nothing print_proof_attempt)
g.external_proofs
(Pp.print_iter2 Mstr.iter Pp.newline Pp.nothing
g.goal_external_proofs
(Pp.print_iter2 PHstr.iter Pp.newline Pp.nothing
Pp.nothing print_transf)
g.transformations
g.goal_transformations
let print_theory fmt th =
fprintf fmt "<li>%s : <ul>%a</ul></li>"
th.theory_name
(Pp.print_list Pp.newline print_goal) th.goals
th.theory_name.Ident.id_string
(Pp.print_list Pp.newline print_goal) th.theory_goals
let print_file fmt f =
fprintf fmt "<li>%s : <ul>%a</ul></li>"
f.file_name
(Pp.print_list Pp.newline print_theory) f.theories
(Pp.print_list Pp.newline print_theory) f.file_theories
let print_session _name fmt s =
fprintf fmt "<ul>%a</ul>"
(Pp.print_list Pp.newline print_file) s.files
(Pp.print_iter2 PHstr.iter Pp.newline Pp.nothing Pp.nothing
print_file) s.session_files
let context : context = "<!DOCTYPE html
......@@ -232,7 +225,7 @@ struct
let print_prover fmt pd = fprintf fmt "%s" pd.prover_name
let print_proof_status fmt = function
| Undone -> fprintf fmt "<span class='notverified'>Undone</span>"
| Undone _ -> fprintf fmt "<span class='notverified'>Undone</span>"
| Done pr -> fprintf fmt "<span class='verified'>Done : %a</span>"
Call_provers.print_prover_result pr
| InternalFailure exn ->
......@@ -274,17 +267,17 @@ struct
base_dst
let print_proof_attempt fmt pa =
match pa.edited_as with
match pa.proof_edited_as with
| None ->
fprintf fmt "@[<hov><li rel='prover' ><a href='#'>%a : %a</a></li>@]"
print_prover pa.prover
print_prover pa.proof_prover
print_proof_status pa.proof_state
| Some f ->
let output = find_pp f in
fprintf fmt "@[<hov><li rel='prover' ><a href='#' \
onclick=\"showedited('%s'); return false;\">%a : %a</a></li>@]"
output
print_prover pa.prover
print_prover pa.proof_prover
print_proof_status pa.proof_state
let rec print_transf fmt tr =
......@@ -293,28 +286,28 @@ onclick=\"showedited('%s'); return false;\">%a : %a</a></li>@]"
<span %a>%s</span></a>@,<ul>%a</ul></li>@]"
print_verified tr.transf_verified
tr.transf_name
(Pp.print_list Pp.newline print_goal) tr.subgoals
(Pp.print_list Pp.newline print_goal) tr.transf_goals
and print_goal fmt g =
fprintf fmt
"@[<hov><li rel='goal'><a href='#'>\
<span %a>%s</a></a>@,<ul>%a%a</ul></li>@]"
print_verified g.goal_verified
g.goal_name
(Pp.print_iter2 Mstr.iter Pp.newline Pp.nothing
g.goal_name.Ident.id_string
(Pp.print_iter2 PHprover.iter Pp.newline Pp.nothing
Pp.nothing print_proof_attempt)
g.external_proofs
(Pp.print_iter2 Mstr.iter Pp.newline Pp.nothing
g.goal_external_proofs
(Pp.print_iter2 PHstr.iter Pp.newline Pp.nothing
Pp.nothing print_transf)
g.transformations
g.goal_transformations
let print_theory fmt th =
fprintf fmt
"@[<hov><li rel='theory'><a href='#'>\
<span %a>%s</span></a>@,<ul>%a</ul></li>@]"
print_verified th.theory_verified
th.theory_name
(Pp.print_list Pp.newline print_goal) th.goals
th.theory_name.Ident.id_string
(Pp.print_list Pp.newline print_goal) th.theory_goals
let print_file fmt f =
fprintf fmt
......@@ -322,12 +315,13 @@ onclick=\"showedited('%s'); return false;\">%a : %a</a></li>@]"
<span %a>%s</span></a>@,<ul>%a</ul></li>@]"
print_verified f.file_verified
f.file_name
(Pp.print_list Pp.newline print_theory) f.theories
(Pp.print_list Pp.newline print_theory) f.file_theories
let print_session_aux name fmt s =
fprintf fmt "@[<hov><ul><a href='#'>%s</a>@,%a</ul>@]"
name
(Pp.print_list Pp.newline print_file) s.files
(Pp.print_iter2 PHstr.iter Pp.newline Pp.nothing Pp.nothing print_file)
s.session_files
let print_session name fmt s =
......@@ -404,7 +398,7 @@ $(function () {
if not (Sys.file_exists edited_dst) then Unix.mkdir edited_dst 0o755;
Queue.iter (run_file context print_session) files;
if !opt_context then
let data_dir = Whyconf.datadir (Whyconf.get_main env.config) in
let data_dir = Whyconf.datadir (Whyconf.get_main whyconf) in
(** copy images *)
let img_dir_src = Filename.concat data_dir "images" in
let img_dir_dst = Filename.concat output_dir "images" in
......
This diff is collapsed.
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
(** This module is a wrapper around Session which is simpler when you
only want to read a session *)
open Why3
open Util
type session =
{ files : file list;
provers : prover_data Mstr.t}
and file =
{ file_name : string;
theories : theory list;
file_verified : bool}
and theory =
{ theory_name : string;
theory : Theory.theory;
goals : goal list;
theory_verified : bool}
and goal =
{ goal_name : string;
goal_expl : string;
goal_verified : bool;
transformations : transf Mstr.t;
external_proofs : proof_attempt Mstr.t}
and transf =
{ transf_name : string;
transf_verified : bool;
subgoals : goal list}
and prover_data =
{ prover_name : string;
prover_version : string;
(** will be added again when session records it *)
(* prover_interactive : bool; *)
}
and proof_attempt_status =
| Undone
| Done of Call_provers.prover_result (** external proof done *)
| InternalFailure of exn (** external proof aborted by internal error *)
and proof_attempt =
{ prover : prover_data;
proof_state : proof_attempt_status;
timelimit : int;
proof_obsolete : bool;
edited_as : string option;
}
(** a proof attempt for a given goal *)
type env =
{ env : Env.env;
config : Whyconf.config}
let read_config ?(includes=[]) conf_path_opt =
let config = Whyconf.read_config conf_path_opt in
let loadpath = (Whyconf.loadpath (Whyconf.get_main config)) @ includes in
let env = Env.create_env loadpath in
{env = env; config = config}
let get_provers env =
let provers = Whyconf.get_provers env.config in
let get_prover_data pr =
{ prover_name = pr.Whyconf.name;
prover_version = pr.Whyconf.version;
(* prover_interactive = pr.Whyconf.interactive; *)
}
in
Mstr.map get_prover_data provers
module Observer_dumb : Session.OBSERVER =
struct
type key = unit
let create ?parent:_ () = ()
let remove _ = ()
let reset () = ()
let idle _ = ()
let timeout ~ms:_ _ = ()
let notify_timer_state _ _ _ = ()
end
module Read_project (O : Session.OBSERVER)
(P : sig val project_dir : string end) =
struct
module M = Session.Make(Observer_dumb)
let old_provers = ref Mstr.empty
let get_prover_by_id pid =
try Mstr.find pid !old_provers
with Not_found -> assert false (** the provers must be an old_provers *)
let read_prover_option po =
get_prover_by_id (match po with
| M.Detected_prover pd -> pd.Session.prover_id
| M.Undetected_prover s -> s)
let read_attempt_status = function
| Session.Undone | Session.Scheduled | Session.Interrupted
| Session.Running | Session.Unedited -> Undone
| Session.Done pr -> Done pr
| Session.InternalFailure exn -> InternalFailure exn
let read_edited_as prover ea =
match prover, ea with
| (_, "") | (M.Detected_prover {Session.interactive = false},_) -> None
| _ -> Some (Filename.concat P.project_dir ea)
let rec read_trans key transf acc =
Mstr.add key
{ transf_name = Session.transformation_id transf.M.transf;
transf_verified = transf.M.transf_proved;
subgoals = List.map read_goal transf.M.subgoals;
} acc
and read_proof key pa acc =
Mstr.add key
{ prover = read_prover_option pa.M.prover;
proof_state = read_attempt_status pa.M.proof_state;
timelimit = pa.M.timelimit;
proof_obsolete = pa.M.proof_obsolete;
edited_as = read_edited_as pa.M.prover pa.M.edited_as;
} acc
and read_goal g =
let transformations = M.transformations g in
let transformations = Hashtbl.fold read_trans transformations Mstr.empty in
let external_proofs = M.external_proofs g in
let external_proofs = Hashtbl.fold read_proof external_proofs Mstr.empty in
{ goal_name = M.goal_name g;
goal_expl = M.goal_expl g;
goal_verified = M.goal_proved g;
transformations = transformations;
external_proofs = external_proofs}
let read_theory th =
{ theory_name = M.theory_name th;
theory = M.get_theory th;
goals = List.map read_goal (M.goals th);
theory_verified = M.verified th}
let read_file file =
{ file_name = file.M.file_name;
theories = List.map read_theory file.M.theories;
file_verified = file.M.file_verified}
let read_project_dir ~allow_obsolete ~env =
let init _ _ = () in
let notify _ = () in
let _found_obs = M.open_session ~allow_obsolete
~env:env.env ~config:env.config ~init ~notify P.project_dir
in
let prover_data (name,version) =
{ prover_name = name; prover_version = version} in
let op = Mstr.map prover_data (M.get_old_provers ()) in
old_provers := op;
{files = List.map read_file (M.get_all_files ());
provers = op}
end
let read_project_dir ~allow_obsolete ~env project_dir =
let module Rp = Read_project(Observer_dumb)
(struct let project_dir = project_dir end)in
Rp.read_project_dir ~allow_obsolete ~env
open Format
let get_project_dir fname =
if Sys.file_exists fname then begin
if Sys.is_directory fname then begin
eprintf "Info: found directory '%s' for the project@." fname;
fname
end
else begin
eprintf "Info: found regular file '%s'@." fname;
let d =
try Filename.chop_extension fname
with Invalid_argument _ -> fname
in
eprintf "Info: using '%s' as directory for the project@." d;
d
end
end
else
raise Not_found
......@@ -16,7 +16,8 @@
open Format
open Why3
open Util
open Session_ro
open Session
let includes = ref []
let files = Queue.create ()
......@@ -62,8 +63,6 @@ let () =
let allow_obsolete = !allow_obsolete
let env = read_config ~includes:!includes !opt_config