Commit da5b5d18 authored by François Bobot's avatar François Bobot

Why3session : a new why3 program

It's goal is to allow to view and modify sessions.

Currently three sub-commands :
info : can give the provers used, pretty-print in ascii a session,
     can give the corresponding directory
mod : allow to set obsolete, or modify the archive state of proof attempt
    which corresponds to selected provers
copy : copy a proof attempt by modifing its prover
parent 08b81e74
......@@ -671,6 +671,60 @@ install_no_local::
install_local: bin/why3replayer
###############
# Session
###############
SESSION_FILES = why3session_lib why3session_mod why3session_copy \
why3session_info why3session
SESSIONMODULES = $(addprefix src/why3session/, $(SESSION_FILES))
SESSIONML = $(addsuffix .ml, $(SESSIONMODULES))
SESSIONMLI = $(addsuffix .mli, $(SESSIONMODULES))
SESSIONCMO = $(addsuffix .cmo, $(SESSIONMODULES))
SESSIONCMX = $(addsuffix .cmx, $(SESSIONMODULES))
$(SESSIONCMO) $(SESSIONCMX): INCLUDES += -I src/why3session
# build targets
byte: bin/why3session.byte
opt: bin/why3session.opt
bin/why3session.opt: src/why3.cmxa $(PGMCMX) $(SESSIONCMX)
$(if $(QUIET), @echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
$(STRIP) $@
bin/why3session.byte: src/why3.cma $(PGMCMO) $(SESSIONCMO)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
bin/why3session: bin/why3session.@OCAMLBEST@
ln -sf why3session.@OCAMLBEST@ $@
# depend and clean targets
include .depend.session
.depend.session:
$(OCAMLDEP) -slash -I src -I src/why3session $(SESSIONML) $(SESSIONMLI) > $@
depend: .depend.session
clean::
rm -f src/ide/*.cm[iox] src/ide/*.o
rm -f src/ide/*.annot src/ide/*~
rm -f bin/why3session.byte bin/why3session.opt bin/why3session
rm -f .depend.session
install_no_local::
cp -f bin/why3session.@OCAMLBEST@ $(BINDIR)/why3session$(EXE)
install_local: bin/why3session
###############
# Stats
###############
......
......@@ -337,7 +337,6 @@ let is_prover_known whyconf prover =
Mprover.mem prover (get_provers whyconf)
exception ProverNotFound of config * string
exception ProverAmbiguity of config * string * prover list
let prover_by_id whyconf id =
let potentials =
......@@ -345,7 +344,7 @@ let prover_by_id whyconf id =
match Mprover.keys potentials with
| [] -> raise (ProverNotFound(whyconf,id))
| [_] -> snd (Mprover.choose potentials)
| l -> raise (ProverAmbiguity(whyconf,id,l))
| _ -> assert false (** by the verification done by set_provers *)
let () = Exn_printer.register
(fun fmt exn ->
......@@ -353,10 +352,6 @@ let () = Exn_printer.register
| ProverNotFound (config,s) ->
fprintf fmt "Prover '%s' not found in %s@."
s (get_conf_file config)
| ProverAmbiguity (config,s,l) ->
fprintf fmt "More than one provers corresponds to '%s' in %s:@.%a@."
s (get_conf_file config)
(Pp.print_list Pp.newline print_prover) l
| e -> raise e
)
......
......@@ -121,9 +121,10 @@ val is_prover_known : config -> prover -> bool
(** test if a prover is detected *)
exception ProverNotFound of config * string
exception ProverAmbiguity of config * string * prover list
val prover_by_id : config -> string -> config_prover
(** return the configuration of the prover if found, otherwise return
ProverNotFound *)
(** {2 For accesing other parts of the configuration } *)
......
......@@ -276,26 +276,9 @@ let model_index = Hashtbl.create 257
*)
let project_dir =
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
failwith "file does not exist"
try
Session.get_project_dir fname
with Not_found -> failwith "file does not exist"
let goal_statistics (goals,n,m) g =
if g.S.goal_verified then (goals,n+1,m+1) else (g::goals,n,m+1)
......
......@@ -113,7 +113,6 @@ let opt_list_metas = ref false
let opt_token_count = ref false
let opt_parse_only = ref false
let opt_type_only = ref false
let opt_debug_all = ref false
let opt_version = ref false
let option_list = Arg.align [
......
......@@ -211,7 +211,11 @@ module PTreeT = struct
then g.goal_name.Ident.id_string^"*"
else g.goal_name.Ident.id_string
| Proof_attempt pr ->
Pp.string_of_wnl Whyconf.print_prover pr.proof_prover
Pp.sprintf_wnl "%a%s%s%s"
Whyconf.print_prover pr.proof_prover
(if pr.proof_obsolete || pr.proof_archived then " " else "")
(if pr.proof_obsolete then "O" else "")
(if pr.proof_archived then "A" else "")
| Transf tr -> tr.transf_name in
let l = ref [] in
iter (fun a -> l := (Any a)::!l) t;
......@@ -552,7 +556,7 @@ let set_obsolete ?(notify=notify) a =
notify (Proof_attempt a);
check_goal_proved notify a.proof_parent
let set_archive a b = a.proof_archived <- b
let set_archived a b = a.proof_archived <- b
(* [raw_add_goal parent name expl sum t] adds a goal to the given parent
DOES NOT record the new goal in its parent, thus this should not be exported
......@@ -1650,23 +1654,22 @@ let update_session ~keygen ~allow_obsolete old_session env whyconf =
new_env_session, obsolete
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
if not (Sys.file_exists fname) then raise Not_found;
let d =
if Sys.is_directory fname then fname
else if Filename.basename fname = db_filename then begin
dprintf debug "Info: found db file '%s'@." fname;
Filename.dirname fname
end
else begin
eprintf "Info: found regular file '%s'@." fname;
let d =
else
begin
dprintf debug "Info: found regular file '%s'@." fname;
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
with Invalid_argument _ -> fname^".w3s"
end
in
dprintf debug "Info: using '%s' as directory for the project@." d;
d
let key_any = function
| File p -> p.file_key
......
......@@ -275,7 +275,7 @@ val set_proof_state :
val set_obsolete : ?notify:'key notify -> 'key proof_attempt -> unit
val set_archive : 'key proof_attempt -> bool -> unit
val set_archived : 'key proof_attempt -> bool -> unit
val set_edited_as : string option -> 'key proof_attempt -> unit
......
......@@ -519,7 +519,7 @@ let cancel = iter_proof_attempt cancel_proof
(** Set or unset archive *)
let set_archive a b = set_archive a b; notify (Proof_attempt a)
let set_archive a b = set_archived a b; notify (Proof_attempt a)
(*********************************)
(* method: check existing proofs *)
......
(**************************************************************************)
(* *)
(* 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. *)
(* *)
(**************************************************************************)
open Format
open Why3
open Why3session_lib
let cmds =
[|
Why3session_mod.cmd;
Why3session_copy.cmd;
Why3session_info.cmd;
|]
let usage = "why3session cmd [opts]:"
let print_usage () =
eprintf "%s@.@.command:@.@[<hov>%a@]@."
usage (Pp.print_iter1 Array.iter Pp.newline
(fun fmt e -> fprintf fmt "%s @[<hov>%s@]"
e.cmd_name e.cmd_desc)) cmds;
exit 1
let () =
if Array.length Sys.argv < 2 then print_usage ();
let cmd_name = Sys.argv.(1) in
match cmd_name with "-h" | "--help" -> print_usage ()
| "-v" | "--version" -> print_version ()
| _ -> ();
let module M = struct exception Found of cmd end in
let cmd =
try
Array.iter (fun e ->
if e.cmd_name = cmd_name
then raise (M.Found e)) cmds;
eprintf "command %s unknown@." cmd_name;
print_usage ()
with M.Found cmd -> cmd
in
incr Arg.current;
let cmd_usage = sprintf "why3session %s [opts]:" cmd_name in
Arg.parse (Arg.align cmd.cmd_spec) anon_fun cmd_usage;
cmd.cmd_run ()
(**************************************************************************)
(* *)
(* 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. *)
(* *)
(**************************************************************************)
open Why3
open Why3session_lib
open Whyconf
open Session
open Format
type filter_prover =
| Prover of Whyconf.prover
| ProverId of string
(**
TODO add_transformation,...
**)
let opt_to_prover = ref None
(** Currently doesn't share the configuration of ide *)
type replace = Interactive | Always | Not_valid | Never
let opt_replace = ref Not_valid
let set_replace s () = opt_replace := s
let spec =
("--to-prover",
Arg.String (fun s -> opt_to_prover := Some (read_opt_prover s)),
" the proof is copied to this new prover")::
("--interactive",
Arg.Unit (set_replace Interactive), " ask before replacing proof_attempt")::
("-i",
Arg.Unit (set_replace Interactive), " same as --interactive")::
("--force", Arg.Unit (set_replace Always),
" force the replacement of proof_attempt")::
("-f", Arg.Unit (set_replace Always), " same as --force")::
("--conservative", Arg.Unit (set_replace Not_valid),
" never replace proof which are not obsolete and valid (default)")::
("-c", Arg.Unit (set_replace Not_valid), " same as --conservative")::
("--never", Arg.Unit (set_replace Never),
" never replace a proof")::
("-n", Arg.Unit (set_replace Never), " same as --never")::
(filter_spec @ env_spec)
let rec interactive to_remove =
eprintf "Do you want to replace the external proof %a (y/n)@."
print_external_proof to_remove;
let answer = read_line () in
match answer with
| "y" -> true
| "n" -> false
| _ -> interactive to_remove
let keygen ?parent:_ _ = ()
let run_one env config filters fname =
let pk = match !opt_to_prover with
| None ->
eprintf "You should specify one prover with --to_prover";
exit 1
| Some fpr ->
try prover_of_filter_prover config fpr
with ProverNotFound (_,id) ->
eprintf
"The prover %s is not found in the configuration file %s@."
id (get_conf_file config);
exit 1 in
let env_session,_ =
read_update_session ~allow_obsolete:false env config fname in
let s = Stack.create () in
session_iter_proof_attempt_by_filter filters
(fun pr -> Stack.push pr s) env_session.session;
Stack.iter (fun pr ->
(** If such a prover already exists on the goal *)
let exists =
(PHprover.mem pr.proof_parent.goal_external_proofs pk) in
let replace = not exists || match !opt_replace with
| Always -> true | Never -> false
| Interactive ->
interactive
(PHprover.find pr.proof_parent.goal_external_proofs pk)
| Not_valid ->
let rm = (PHprover.find pr.proof_parent.goal_external_proofs pk) in
not (proof_verified rm) in
if replace then
ignore (copy_external_proof ~keygen ~prover:pk ~env_session pr)
) s;
save_session env_session.session
let run () =
let env,config,should_exit1 = read_env_spec () in
let filters,should_exit2 = read_filter_spec config in
if should_exit1 || should_exit2 then exit 1;
iter_files (run_one env config filters)
let cmd =
{ cmd_spec = spec;
cmd_desc = "copy proof based on a filter. \
No filter means all the possibilities.";
cmd_name = "copy";
cmd_run = run;
}
(**************************************************************************)
(* *)
(* 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. *)
(* *)
(**************************************************************************)
open Why3
open Why3session_lib
open Whyconf
open Format
module S = Session
let opt_print_provers = ref false
let opt_tree_print = ref false
let opt_project_dir = ref false
let spec =
("--provers", Arg.Set opt_print_provers,
" the prover used in the session are listed" ) ::
("--tree", Arg.Set opt_tree_print,
" the session is pretty printed in an ascii tree format" ) ::
("--dir", Arg.Set opt_project_dir,
" print the directory of the session" ) ::
simple_spec
let run_one fname =
let project_dir = Session.get_project_dir fname in
if !opt_project_dir then printf "%s@." project_dir;
let session = Session.read_session project_dir in
if !opt_print_provers then
printf "%a@."
(Pp.print_iter1 Sprover.iter Pp.newline print_prover)
(S.get_used_provers session);
if !opt_tree_print then
printf "%a@." S.print_session session
let run () =
let should_exit1 = read_simple_spec () in
if should_exit1 then exit 1;
iter_files run_one
let cmd =
{ cmd_spec = spec;
cmd_desc = "print informations about session";
cmd_name = "info";
cmd_run = run;
}
(**************************************************************************)
(* *)
(* 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. *)
(* *)
(**************************************************************************)
open Why3
module S = Session
module C = Whyconf
type spec_list = (Arg.key * Arg.spec * Arg.doc) list
type cmd =
{
cmd_spec : spec_list;
cmd_desc : string;
cmd_name : string;
cmd_run : unit -> unit;
}
let files = Queue.create ()
let iter_files f = Queue.iter f files
let anon_fun (f:string) = Queue.add f files
let opt_version = ref false
let print_version () =
Format.printf "Why3 session, version %s (build date: %s)@."
Config.version Config.builddate
let simple_spec = [
("-v", Arg.Set opt_version, " print version information") ;
Debug.Opt.desc_debug_list;
Debug.Opt.desc_debug_all;
Debug.Opt.desc_debug;
]
let read_simple_spec () =
if !opt_version then begin
print_version (); exit 0
end;
Debug.Opt.set_flags_selected ();
Debug.Opt.option_list ()
let includes = ref []
let opt_config = ref None
let opt_loadpath = ref []
let env_spec = [
"-C", Arg.String (fun s -> opt_config := Some s),
"<file> Read configuration from <file>";
"--config", Arg.String (fun s -> opt_config := Some s),
" same as -C";
"-L", Arg.String (fun s -> opt_loadpath := s :: !opt_loadpath),
"<dir> Add <dir> to the library search path";
"--library", Arg.String (fun s -> opt_loadpath := s :: !opt_loadpath),
" same as -L";
]@simple_spec
let read_env_spec () =
(** Configuration *)
let config = Whyconf.read_config !opt_config in
let main = Whyconf.get_main config in
Whyconf.load_plugins main;
let loadpath = (Whyconf.loadpath (Whyconf.get_main config))
@ List.rev !includes in
let env = Env.create_env loadpath in
env,config,read_simple_spec ()
let read_update_session ~allow_obsolete env config fname =
let project_dir = Session.get_project_dir fname in
let session = Session.read_session project_dir in
Session.update_session ~keygen:(fun ?parent:_ _ -> ())
~allow_obsolete session env config
(** filter *)
type filter_prover =
| Prover of Whyconf.prover
| ProverId of string
let filter_prover = Stack.create ()
let read_opt_prover s =
let sl = Util.split_string_rev s ',' in
(* reverse order *)
let prover =
match sl with
| [altern;version;name] ->
Prover {C.prover_name = name; prover_version = version;
prover_altern = altern}
| [version;name] ->
Prover {C.prover_name = name; prover_version = version;
prover_altern = ""}
| [id] -> ProverId id
| _ -> raise (Arg.Bad "--filter-prover [name,version[,alternative]|id]")
in prover
let add_filter_prover s = Stack.push (read_opt_prover s) filter_prover
let filter_spec =
["--filter-prover", Arg.String add_filter_prover,
" [name,version[,alternative]|id] \
the proof containing this prover will be transformed"]
type filters = C.Sprover.t (* if empty : every provers *)
(* * ... *)
let prover_of_filter_prover whyconf = function
| Prover p -> p
| ProverId id -> (C.prover_by_id whyconf id).C.prover
let read_filter_spec whyconf : filters * bool =
let should_exit = ref false in
let s = ref C.Sprover.empty in
let iter p =
try
s := C.Sprover.add (prover_of_filter_prover whyconf p) !s
with C.ProverNotFound (_,id) ->
Format.eprintf
"The prover %s is not found in the configuration file %s@."
id (Whyconf.get_conf_file whyconf);
should_exit := true in
Stack.iter iter filter_prover;
!s,!should_exit
let session_iter_proof_attempt_by_filter provers f session =
let iter a = if C.Sprover.mem a.S.proof_prover provers then f a in
if C.Sprover.is_empty provers
(** if no prover is filtered then they are all taken *)
then S.session_iter_proof_attempt f session
else S.session_iter_proof_attempt iter session
(**************************************************************************)
(* *)
(* 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. *)
(* *)
(**************************************************************************)
open Why3
open Whyconf
type spec_list = (Arg.key *