Commit 191603cf authored by MARCHE Claude's avatar MARCHE Claude

Merge branch 'master' into claude

Conflicts:
	drivers/cvc4_bare.drv
parents aa611eed 6fe88dfc
/examples/in_progress/ export-ignore
/misc/ export-ignore
/ROADMAP export-ignore
/DEVELOPER.readme export-ignore
/opam/ export-ignore
.gitignore export-ignore
......@@ -132,6 +132,9 @@ why3.conf
# /share/
/share/emacs/semantic.cache
/share/Makefile.config
/share/drivers
/share/modules
/share/theories
# /src/
/src/config.sh
......
......@@ -118,6 +118,11 @@ CLEANDIRS =
CLEANLIBS =
GENERATED =
install_local::
ln -s ../drivers share/drivers
ln -s ../modules share/modules
ln -s ../theories share/theories
##############
# Why3 library
##############
......@@ -1744,23 +1749,15 @@ wc:
#########
NAME = why3-@VERSION@
DISTRIB_DIR = distrib/$(NAME)
DISTRIB_TAR = $(DISTRIB_DIR).tar.gz
# TODO?
# share/zsh ?
# symbolic links in share/ ?
# see .gitattributes for the list of files that are not distributed
EXTRA_DIST = configure doc/manual.pdf
NODIST = examples/in_progress/ misc/ ROADMAP DEVELOPER.readme opam/
dist: $(EXTRA_DIST)
rm -rf $(DISTRIB_TAR) $(DISTRIB_DIR)
mkdir -p $(DISTRIB_DIR)
for d in `git ls-tree -d -r --name-only HEAD`; do mkdir $(DISTRIB_DIR)/$$d; done
for f in `git ls-tree -r --name-only HEAD` $(EXTRA_DIST); do cp $$f $(DISTRIB_DIR)/$$f; done
rm `find $(DISTRIB_DIR) -name .gitignore`
cd $(DISTRIB_DIR); rm -rf $(NODIST)
rm -rf distrib/$(NAME)/ distrib/$(NAME).tar.gz
mkdir -p distrib/
git archive --format tar --prefix $(NAME)/ HEAD | tar x -C distrib/
for f in $(EXTRA_DIST); do cp $$f distrib/$(NAME)/$$f; done
cd distrib; tar cf $(NAME).tar $(NAME); gzip -f --best $(NAME).tar
......
......@@ -13,8 +13,10 @@ timeout "Steps limit reached"
outofmemory "Fatal error: out of memory"
outofmemory "Fatal error: exception Stack_overflow"
fail "typing error:\\(.*\\)$" "Failure : File generation error : \\1"
time "Valid (%s) (%S)"
time "Valid (%s) (%S steps)"
time "Valid (%s)"
time "Valid (%s)"
steps "Valid (\\([0-9]+.?[0-9]*\\)) (\\([0-9]+.?[0-9]*\\))" 2
steps "Valid (\\([0-9]+.?[0-9]*\\)) (\\([0-9]+.?[0-9]*\\) steps)" 2
time "why3cpulimit time : %s s"
(* À discuter *)
......
......@@ -32,14 +32,8 @@ transformation "encoding_smt"
outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
timeout "interrupted by timeout"
steps "smt::SmtEngine::resourceUnitsUsed, \\([0-9]+.?[0-9]*\\)" 1
(* regexp for steps should match things like
smt::SmtEngine::resourceUnitsUsed, 1041
but not in the same line as the "valid" answer
*)
(** Extra theories supported by CVC4 *)
......
This diff is collapsed.
../drivers
\ No newline at end of file
../modules/
\ No newline at end of file
......@@ -86,19 +86,32 @@ version_old = "0.8"
command = "%l/why3-cpulimit %t %m -s %e %f"
driver = "drivers/alt_ergo_0.92.drv"
# CVC4 version 1.4 and 1.5-prerelease
# CVC4 version 1.5-prerelease
[ATP cvc4]
name = "CVC4"
exec = "cvc4"
exec = "cvc4-1.5-prerelease"
exec = "cvc4-1.4"
version_switch = "--version"
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
version_ok = "1.5-prerelease"
driver = "drivers/cvc4.drv"
# --random-seed=42 is not needed as soon as --random-freq=0.0 by default
# to try: --inst-when=full-last-call
command = "%l/why3-cpulimit %T %m -s %e --stats --tlimit-per=%t000 --rlimit=%S --lang=smt2 %f"
# CVC4 version 1.4
[ATP cvc4]
name = "CVC4"
exec = "cvc4"
exec = "cvc4-1.4"
version_switch = "--version"
version_regexp = "This is CVC4 version \\([^ \n\r]+\\)"
version_ok = "1.4"
driver = "drivers/cvc4_14.drv"
# --random-seed=42 is not needed as soon as --random-freq=0.0 by default
# to try: --inst-when=full-last-call
# to try: --inst-when=full-last-call
# --rlimit=%S : cvc4 1.4 DOES NOT accept -1 as argument
# cvc4 .14 does not print steps used in --stats anyway
command = "%l/why3-cpulimit %T %m -s %e --tlimit-per=%t000 --lang=smt2 %f"
# CVC4 version 1.0 to 1.3
......
../theories
\ No newline at end of file
......@@ -11,19 +11,27 @@
open Format
let debug = Debug.register_info_flag "call_prover"
~desc:"Print@ debugging@ messages@ about@ prover@ calls@ \
and@ keep@ temporary@ files."
(** time regexp "%h:%m:%s" *)
type timeunit =
| Hour
| Min
| Sec
| Msec
| Step
type timeregexp = {
re : Str.regexp;
group : timeunit array; (* i-th corresponds to the group i+1 *)
}
type stepsregexp = {
steps_re : Str.regexp;
steps_group_num : int; (* the number of matched group which corresponds to the number of steps *)
}
let timeregexp s =
let cmd_regexp = Str.regexp "%\\(.\\)" in
let nb = ref 0 in
......@@ -35,7 +43,6 @@ let timeregexp s =
| "m" -> add_unit Min
| "s" -> add_unit Sec
| "i" -> add_unit Msec
| "S" -> add_unit Step
| _ -> failwith "unknown format specifier, use %%h, %%m, %%s, %%i, %%S"
in
let s = Str.global_substitute cmd_regexp replace s in
......@@ -49,17 +56,29 @@ let rec grep_time out = function
begin try
ignore (Str.search_forward re.re out 0);
let t = ref 0. in
let s = ref (-1) in
Array.iteri (fun i u ->
let v = Str.matched_group (succ i) out in
match u with
| Hour -> t := !t +. float_of_string v *. 3600.
| Min -> t := !t +. float_of_string v *. 60.
| Sec -> t := !t +. float_of_string v
| Msec -> t := !t +. float_of_string v /. 1000.
| Step -> s := int_of_string v ) re.group;
Some( !t, !s )
with _ -> grep_time out l end
| Msec -> t := !t +. float_of_string v /. 1000. ) re.group;
Some( !t )
with _ -> grep_time out l
end
let stepsregexp s_re s_group_num =
{steps_re = (Str.regexp s_re); steps_group_num = s_group_num}
let rec grep_steps out = function
| [] -> None
| re :: l ->
begin try
ignore (Str.search_forward re.steps_re out 0);
let v = Str.matched_group (re.steps_group_num) out in
Some(int_of_string v)
with _ -> grep_steps out l
end
(** *)
......@@ -83,6 +102,7 @@ type prover_result = {
type prover_result_parser = {
prp_regexps : (Str.regexp * prover_answer) list;
prp_timeregexps : timeregexp list;
prp_stepsregexp : stepsregexp list;
prp_exitcodes : (int * prover_answer) list;
}
......@@ -122,11 +142,6 @@ let rec grep out l = match l with
| HighFailure -> assert false
with Not_found -> grep out l end
let debug = Debug.register_info_flag "call_prover"
~desc:"Print@ debugging@ messages@ about@ prover@ calls@ \
and@ keep@ temporary@ files."
type post_prover_call = unit -> prover_result
type prover_call = {
......@@ -152,8 +167,8 @@ let parse_prover_run res_parser time out ret on_timelimit timelimit =
with Not_found -> grep out res_parser.prp_regexps)
in
Debug.dprintf debug "Call_provers: prover output:@\n%s@." out;
let time,steps = Opt.get_def (time,-1) (grep_time out res_parser.prp_timeregexps) in
(* TODO: separate grep for time and for steps into different regexps *)
let time = Opt.get_def (time) (grep_time out res_parser.prp_timeregexps) in
let steps = Opt.get_def (-1) (grep_steps out res_parser.prp_stepsregexp) in
let ans = match ans with
| Unknown _ | HighFailure when on_timelimit && timelimit > 0
&& time >= (0.9 *. float timelimit) -> Timeout
......@@ -169,6 +184,7 @@ let parse_prover_run res_parser time out ret on_timelimit timelimit =
let actualcommand command timelimit memlimit stepslimit file =
let arglist = Cmdline.cmdline_split command in
let use_stdin = ref true in
(* FIXME: use_stdin is never modified below ?? *)
let on_timelimit = ref false in
let cmd_regexp = Str.regexp "%\\(.\\)" in
let replace s = match Str.matched_group 1 s with
......@@ -184,8 +200,9 @@ let actualcommand command timelimit memlimit stepslimit file =
| "l" -> Config.libdir
| "d" -> Config.datadir
| "S" -> string_of_int stepslimit
| _ -> failwith "unknown specifier, use %%, %f, %t, %T, %U, %m, %l, or %d"
| _ -> failwith "unknown specifier, use %%, %f, %t, %T, %U, %m, %l, %d or %S"
in
(* FIXME: are we sure that tuples are evaluated from left to right ? *)
List.map (Str.global_substitute cmd_regexp replace) arglist,
!use_stdin, !on_timelimit
......
......@@ -57,13 +57,21 @@ val debug : Debug.flag
type timeregexp
(** The type of precompiled regular expressions for time parsing *)
type stepsregexp
(** The type of precompiled regular expressions for parsing of steps *)
val timeregexp : string -> timeregexp
(** Converts a regular expression with special markers '%h','%m',
'%s','%i' (for milliseconds) into a value of type [timeregexp] *)
val stepsregexp : string -> int -> stepsregexp
(** stepsregexp s n creates a regular expression for matching number of steps.
s is regular expression, n is a group number with steps information *)
type prover_result_parser = {
prp_regexps : (Str.regexp * prover_answer) list;
prp_timeregexps : timeregexp list;
prp_stepsregexp : stepsregexp list;
prp_exitcodes : (int * prover_answer) list;
}
......
......@@ -75,6 +75,7 @@ let load_driver = let driver_tag = ref (-1) in fun env file extra_files ->
let printer = ref None in
let transform = ref [] in
let timeregexps = ref [] in
let stepsregexps = ref [] in
let blacklist = Queue.create () in
let set_or_raise loc r v error = match !r with
......@@ -91,6 +92,7 @@ let load_driver = let driver_tag = ref (-1) in fun env file extra_files ->
| RegexpUnknown (s,t) -> add_to_list regexps (Str.regexp s, Unknown t)
| RegexpFailure (s,t) -> add_to_list regexps (Str.regexp s, Failure t)
| TimeRegexp r -> add_to_list timeregexps (Call_provers.timeregexp r)
| StepRegexp (r,ns) -> add_to_list stepsregexps (Call_provers.stepsregexp r ns)
| ExitCodeValid s -> add_to_list exitcodes (s, Valid)
| ExitCodeInvalid s -> add_to_list exitcodes (s, Invalid)
| ExitCodeTimeout s -> add_to_list exitcodes (s, Timeout)
......@@ -197,6 +199,7 @@ let load_driver = let driver_tag = ref (-1) in fun env file extra_files ->
{
prp_regexps = List.rev !regexps;
prp_timeregexps = List.rev !timeregexps;
prp_stepsregexp = List.rev !stepsregexps;
prp_exitcodes = List.rev !exitcodes;
};
drv_tag = !driver_tag;
......
......@@ -60,6 +60,7 @@ type global =
| RegexpUnknown of string * string
| RegexpFailure of string * string
| TimeRegexp of string
| StepRegexp of string * int
| ExitCodeValid of int
| ExitCodeInvalid of int
| ExitCodeTimeout of int
......
......@@ -31,6 +31,7 @@
"meta", META;
"prelude", PRELUDE;
"printer", PRINTER;
"steps", STEPS;
"valid", VALID;
"invalid", INVALID;
"timeout", TIMEOUT;
......
......@@ -23,7 +23,7 @@
%token <string> OPERATOR
%token <string> INPUT (* never reaches the parser *)
%token THEORY END SYNTAX REMOVE META PRELUDE PRINTER
%token VALID INVALID TIMEOUT OUTOFMEMORY UNKNOWN FAIL TIME
%token VALID INVALID TIMEOUT OUTOFMEMORY UNKNOWN FAIL TIME STEPS
%token UNDERSCORE LEFTPAR RIGHTPAR DOT QUOTE EOF
%token BLACKLIST
%token MODULE EXCEPTION VAL CONVERTER
......@@ -56,6 +56,7 @@ global:
| TIMEOUT STRING { RegexpTimeout $2 }
| OUTOFMEMORY STRING { RegexpOutOfMemory $2 }
| TIME STRING { TimeRegexp $2 }
| STEPS STRING INTEGER { StepRegexp ($2, $3) }
| UNKNOWN STRING STRING { RegexpUnknown ($2, $3) }
| FAIL STRING STRING { RegexpFailure ($2, $3) }
| VALID INTEGER { ExitCodeValid $2 }
......@@ -106,20 +107,21 @@ qualid_:
| ident DOT qualid_ { ($1 :: $3) }
ident:
| IDENT { $1 }
| SYNTAX { "syntax" }
| REMOVE { "remove" }
| PRELUDE { "prelude" }
| BLACKLIST { "blacklist" }
| PRINTER { "printer" }
| VALID { "valid" }
| INVALID { "invalid" }
| TIMEOUT { "timeout" }
| UNKNOWN { "unknown" }
| FAIL { "fail" }
| FILENAME { "filename" }
| TRANSFORM { "transformation" }
| PLUGIN { "plugin" }
| IDENT { $1 }
| SYNTAX { "syntax" }
| REMOVE { "remove" }
| PRELUDE { "prelude" }
| BLACKLIST { "blacklist" }
| PRINTER { "printer" }
| STEPS { "steps" }
| VALID { "valid" }
| INVALID { "invalid" }
| TIMEOUT { "timeout" }
| UNKNOWN { "unknown" }
| FAIL { "fail" }
| FILENAME { "filename" }
| TRANSFORM { "transformation" }
| PLUGIN { "plugin" }
ident_rich:
| ident { $1 }
......
......@@ -333,14 +333,24 @@ let source_page,source_tab =
(fun w -> ignore(notebook#append_page ~tab_label:label#coerce w)) ()
let task_page,task_tab =
let label = GMisc.label ~text:"Task/Prover Output" () in
let label = GMisc.label ~text:"Task" () in
1, GPack.vbox ~homogeneous:false ~packing:
(fun w -> ignore(notebook#append_page ~tab_label:label#coerce w)) ()
let right_hb = GPack.hbox ~packing:(source_tab#pack ~expand:false) ()
let edited_page,edited_tab =
let label = GMisc.label ~text:"Edited proof" () in
2, GPack.vbox ~homogeneous:false ~packing:
(fun w -> ignore(notebook#append_page ~tab_label:label#coerce w)) ()
let output_page,output_tab =
let label = GMisc.label ~text:"Prover Output" () in
3, GPack.vbox ~homogeneous:false ~packing:
(fun w -> ignore(notebook#append_page ~tab_label:label#coerce w)) ()
let _ = GPack.hbox ~packing:(source_tab#pack ~expand:false) ()
(******************)
(* goal text view *)
(* views *)
(******************)
let scrolled_task_view =
......@@ -355,8 +365,33 @@ let task_view =
~packing:scrolled_task_view#add
()
let scrolled_edited_view =
GBin.scrolled_window
~hpolicy: `AUTOMATIC ~vpolicy: `AUTOMATIC
~shadow_type:`ETCHED_OUT ~packing:edited_tab#add ()
let edited_view =
GSourceView2.source_view
~editable:false
~show_line_numbers:true
~packing:scrolled_edited_view#add
()
let scrolled_output_view =
GBin.scrolled_window
~hpolicy: `AUTOMATIC ~vpolicy: `AUTOMATIC
~shadow_type:`ETCHED_OUT ~packing:output_tab#add ()
let output_view =
GSourceView2.source_view
~editable:false
~show_line_numbers:true
~packing:scrolled_output_view#add
()
let modifiable_sans_font_views = ref [goals_view#misc]
let modifiable_mono_font_views = ref [task_view#misc]
let modifiable_mono_font_views =
ref [task_view#misc;edited_view#misc;output_view#misc]
let () = task_view#source_buffer#set_language why_lang
let () = task_view#set_highlight_current_line true
......@@ -504,20 +539,39 @@ let split_transformation = "split_goal_wp"
let inline_transformation = "inline_goal"
let intro_transformation = "introduce_premises"
let update_task_view a =
let text =
match a with
| S.Goal g ->
if (Gconfig.config ()).intro_premises then
let trans =
Trans.lookup_transform intro_transformation (env_session()).S.env
in
task_text (try Trans.apply trans (S.goal_task g) with
e -> eprintf "@.%a@." Exn_printer.exn_printer e; raise e)
else
task_text (S.goal_task g)
let goal_task_text g =
if (Gconfig.config ()).intro_premises then
let trans =
Trans.lookup_transform intro_transformation (env_session()).S.env
in
task_text (try Trans.apply trans (S.goal_task g) with
e -> eprintf "@.%a@." Exn_printer.exn_printer e; raise e)
else
task_text (S.goal_task g)
let update_tabs a =
let task_text =
match a with
| S.Goal g -> goal_task_text g
| S.Proof_attempt a -> goal_task_text a.S.proof_parent
| S.Theory th -> "Theory " ^ th.S.theory_name.Ident.id_string
| S.File file -> "File " ^ file.S.file_name
| S.Transf tr -> "transformation \"" ^ tr.S.transf_name ^ "\""
| S.Metas _ -> "metas"
in
let edited_text =
match a with
| S.Proof_attempt a ->
begin
let env = env_session () in
match S.get_edited_as_abs env.S.session a with
| None -> ""
| Some f -> source_text f
end
| _ -> ""
in
let output_text =
match a with
| S.Proof_attempt a ->
begin
match a.S.proof_state with
......@@ -533,18 +587,9 @@ let update_task_view a =
Buffer.contents b
| S.Done r ->
let out = r.Call_provers.pr_output in
let out = if out = "" then
"Output not available. Rerun it with \"Replay\" button"
else out
in
begin
let env = env_session () in
match S.get_edited_as_abs env.S.session a with
| None -> out
| Some f -> (source_text f) ^
"\n----------------------------------------------\n\n"
^ out
end
if out = "" then
"Output not available. Rerun it with \"Replay\" button"
else out
| S.Scheduled-> "proof scheduled but not running yet"
| S.Running -> "prover currently running"
| S.InternalFailure e ->
......@@ -552,20 +597,22 @@ let update_task_view a =
bprintf b "%a" Exn_printer.exn_printer e;
Buffer.contents b
end
| S.Transf tr ->
"transformation \"" ^ tr.S.transf_name ^ "\""
| S.Metas m ->
let print_meta_args =
Pp.hov 2 (Pp.print_list Pp.space Pretty.print_meta_arg) in
let print =
Pp.print_iter2 Mstr.iter Pp.newline2 Pp.newline Pp.string
(Pp.indent 2
(Pp.print_iter1 S.Smeta_args.iter Pp.newline print_meta_args))
in
(Pp.string_of (Pp.hov 2 print) m.S.metas_added)
| S.Metas m ->
let print_meta_args =
Pp.hov 2 (Pp.print_list Pp.space Pretty.print_meta_arg) in
let print =
Pp.print_iter2 Mstr.iter Pp.newline2 Pp.newline Pp.string
(Pp.indent 2
(Pp.print_iter1 S.Smeta_args.iter Pp.newline print_meta_args))
in
(Pp.string_of (Pp.hov 2 print) m.S.metas_added)
| _ -> ""
in
task_view#source_buffer#set_text text;
task_view#scroll_to_mark `INSERT
task_view#source_buffer#set_text task_text;
task_view#scroll_to_mark `INSERT;
edited_view#source_buffer#set_text edited_text;
edited_view#scroll_to_mark `INSERT;
output_view#source_buffer#set_text output_text
......@@ -641,7 +688,7 @@ let notify any =
begin
match !current_selected_row with
| Some r when r == ind ->
update_task_view any
update_tabs any
| _ -> ()
end;
if expanded then goals_view#expand_to_path row#path else
......@@ -2259,19 +2306,19 @@ let select_row r =
let ind = goals_model#get ~row:r#iter ~column:index_column in
current_selected_row := Some ind;
let a = get_any_from_row_reference r in
update_task_view a;
update_tabs a;
match a with
| S.Goal g ->
scroll_to_source_goal g
| S.Theory th ->
scroll_to_theory th;
notebook#goto_page source_page (* go to "source" tab *)
(* notebook#goto_page source_page (* go to "source" tab *)*)
| S.File file ->
scroll_to_file (Filename.concat project_dir file.S.file_name);
notebook#goto_page source_page (* go to "source" tab *)
(* notebook#goto_page source_page (\* go to "source" tab *\) *)
| S.Proof_attempt a ->
scroll_to_source_goal a.S.proof_parent;
notebook#goto_page task_page (* go to "prover output" tab *)
(* notebook#goto_page output_page (\* go to "prover output" tab *\) *)
| S.Transf tr ->
scroll_to_source_goal tr.S.transf_parent
| S.Metas m ->
......
......@@ -292,7 +292,8 @@ let schedule_edition t command filename callback =
let res_parser =
{ Call_provers.prp_exitcodes = [(0,Call_provers.Unknown "")];
Call_provers.prp_regexps = [];
Call_provers.prp_timeregexps = []
Call_provers.prp_timeregexps = [];
Call_provers.prp_stepsregexp = [];
} in
let precall =
Call_provers.call_on_file ~command ~res_parser ~redirect:false filename in
......@@ -461,13 +462,13 @@ let run_external_proof_v3 eS eT a callback =
end else begin
let previous_result = a.proof_state in
let timelimit, memlimit = adapt_limits a in
let stepslimit, timelimit =
let stepslimit =
match a with
| { proof_state =
Done { Call_provers.pr_answer = Call_provers.Valid;
Call_provers.pr_steps = s };
proof_obsolete = false } when s >= 0 -> s, 0
| _ -> -1, timelimit
proof_obsolete = false } when s >= 0 -> s
| _ -> -1
in
let inplace = npc.prover_config.Whyconf.in_place in
let command = Whyconf.get_complete_command npc.prover_config in
......
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