Skip to content

GitLab

why3
why3
Commit 176be2d1 authored by Francois Bobot's avatar Francois Bobot
Browse files
Options

Final Rc, WhyConf API libdir datadir are in .why.conf

parent 83dc345b
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 446 additions and 360 deletions
Makefile.in
View file @ 176be2d1
......@@ -120,7 +120,7 @@ LIB_CORE = ident ty term pattern decl theory task pretty env printer trans
LIB_PARSER = ptree denv typing parser lexer
LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \
whyconf
whyconf autodetection
LIB_TRANSFORM = simplify_recursive_definition simplify_formula \
inlining split_conjunction split_goal \
......
share/provers-detection-data.conf
View file @ 176be2d1
......@@ -3,18 +3,18 @@ name = "Alt-Ergo"
exec = "alt-ergo"
exec = "ergo"
version_switch = "-version"
version_regexp = ".*Ergo \\([^ ]*\\)"
version_regexp = ".*Ergo \\([^ \n]*\\)"
version_ok = "0.92"
version_old = "0.8"
version_old = "0.9"
command = "why3-cpulimit %t %m %e %f"
driver = "drivers/alt_ergo.drv"
[ATP cvc3]
[ATP cvc3]
name = "CVC3"
exec = "cvc3"
version_switch = "-version"
version_regexp = "This is CVC3 version \\([^ ]+\\)"
version_regexp = "This is CVC3 version \\([^ \n]+\\)"
version_ok = "2.2"
version_old = "2.1"
command = "why3-cpulimit 0 %m %e -timeout %t -lang smt %f 2>&1"
......@@ -30,7 +30,7 @@ driver = "drivers/tptp.drv"
name = "Gappa"
exec = "gappa"
version_switch = "--version"
version_regexp = "Gappa \\([^ ]*\\)"
version_regexp = "Gappa \\([^ \n]*\\)"
version_ok = "0.13.0"
version_old = "0.11.2"
version_old = "0.12.0"
......@@ -47,7 +47,7 @@ exec = "simplify"
exec = "Simplify-1.5.4"
exec = "Simplify-1.5.5"
version_switch = "-version"
version_regexp = "Simplify version \\([^ ,]+\\)"
version_regexp = "Simplify version \\([^ \n,]+\\)"
version_ok = "1.5.4"
version_ok = "1.5.5"
command = "why3-cpulimit %t %m %e %f 2>&1"
......@@ -56,8 +56,8 @@ driver = "drivers/simplify.drv"
[ATP spass]
name = "Spass"
exec = "SPASS"
version_switch = "-version (TODO)"
version_regexp = "SPASS version \\([^ ,]+\\) (TODO)"
version_switch = " || true"
version_regexp = "SPASS V \\([^ \n\t]+\\)"
command = "why3-cpulimit 0 %m %e -TPTP -PGiven=0 -PProblem=0 -DocProof -TimeLimit=%t %f 2>&1"
driver = "drivers/tptp.drv"
......@@ -66,7 +66,7 @@ name = "Z3"
exec = "z3"
exec = "z3-2.2"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \r]+\\)"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
version_ok = "2.2"
version_old = "2.1"
version_old = "1.3"
......@@ -77,7 +77,7 @@ driver = "drivers/z3.drv"
name = "Coq"
exec = "coqc"
version_switch = "-v"
version_regexp = "The Coq Proof Assistant, version \\([^ ]+\\)"
version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
version_ok = "8.0"
version_ok = "8.1"
version_ok = "8.2"
......
src/driver/autodetection.ml 0 → 100644
View file @ 176be2d1
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* 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 Util
open Whyconf
open Rc
(* auto-detection of provers *)
type prover_kind = ATP | ITP
type prover_autodetection_data =
{ kind : prover_kind;
prover_id : string;
prover_name : string;
execs : string list;
version_switch : string;
version_regexp : string;
versions_ok : string list;
versions_old : string list;
prover_command : string;
prover_driver : string;
prover_editor : string;
}
let prover_keys =
let add acc k = Sstr.add k acc in
List.fold_left add Sstr.empty
["name";"exec";"version_switch";"version_regexp";
"version_ok";"version_old";"command";
"editor";"driver"]
let load_prover kind (id,section) =
check_exhaustive section prover_keys;
{ kind = kind;
prover_id = id;
prover_name = get_string section "name";
execs = get_stringl section "exec";
version_switch = get_string section ~default:"" "version_switch";
version_regexp = get_string section ~default:"" "version_regexp";
versions_ok = get_stringl section ~default:[] "version_ok";
versions_old = get_stringl section ~default:[] "version_old";
prover_command = get_string section "command";
prover_driver = get_string section "driver";
prover_editor = get_string section ~default:"" "editor";
}
let load rc =
let atps = get_family rc "ATP" in
let atps = List.map (load_prover ATP) atps in
let itps = get_family rc "ITP" in
let tps = List.fold_left (cons (load_prover ITP)) atps itps in
tps
let read_auto_detection_data main =
let filename = Filename.concat main.datadir "provers-detection-data.conf" in
try
let rc = Rc.from_file filename in
load rc
with
| Failure "lexing" ->
eprintf "Syntax error in provers-detection-data.conf@.";
exit 2
| Not_found ->
eprintf "provers-detection-data.conf not found at %s@." filename;
exit 2
let provers_found = ref 0
let prover_tips_info = ref false
let make_command exec com =
let cmd_regexp = Str.regexp "%\\(.\\)" in
let replace s = match Str.matched_group 1 s with
| "e" -> exec
| c -> "%"^c
in
Str.global_substitute cmd_regexp replace com
let detect_prover main acc data =
List.fold_left
(fun acc com ->
let out = Filename.temp_file "out" "" in
let cmd = sprintf "%s %s" com data.version_switch in
let c = sprintf "(%s) > %s" cmd out in
let ret = Sys.command c in
if ret <> 0 then
begin
eprintf "command '%s' failed@." cmd;
acc
end
else
let s =
try
let ch = open_in out in
Sysutil.channel_contents ch
(* let s = ref (input_line ch) in *)
(* while !s = "" do s := input_line ch done; *)
(* close_in ch; *)
(* Sys.remove out; *)
(* !s *)
with Not_found | End_of_file -> ""
in
let re = Str.regexp data.version_regexp in
try
ignore (Str.search_forward re s 0);
let nam = data.prover_name in
let ver = Str.matched_group 1 s in
if List.mem ver data.versions_ok then
eprintf "Found prover %s version %s, OK.@." nam ver
else
begin
prover_tips_info := true;
if List.mem ver data.versions_old then
eprintf "Warning: prover %s version %s is quite old, please \
consider upgrading to a newer version.@."
nam ver
else
eprintf "Warning: prover %s version %s is not known to be \
supported, use it at your own risk!@." nam ver
end;
incr provers_found;
let c = make_command com data.prover_command in
Mstr.add data.prover_id
{name = data.prover_name;
version = ver;
command = c;
driver = Filename.concat main.libdir data.prover_driver;
editor = data.prover_editor} acc
with Not_found ->
begin
prover_tips_info := true;
eprintf "Warning: found prover %s but name/version not \
recognized by regexp `%s'@."
data.prover_name data.version_regexp;
eprintf "Answer was `%s'@." s;
acc
end)
acc
data.execs
let run_auto_detection config =
let main = get_main config in
let l = read_auto_detection_data main in
let detect = List.fold_left (detect_prover main) Mstr.empty l in
let length = Mstr.fold (fun _ _ i -> i+1) detect 0 in
eprintf "%d provers detected.@." length;
set_provers config detect
src/driver/autodetection.mli 0 → 100644
View file @ 176be2d1
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* 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. *)
(* *)
(**************************************************************************)
(** Replace the provers by autodetected one *)
val run_auto_detection : Whyconf.config -> Whyconf.config
src/driver/whyconf.ml
View file @ 176be2d1
This diff is collapsed.
src/driver/whyconf.mli
View file @ 176be2d1
......@@ -21,8 +21,6 @@
open Util
val sharedir : string (* For image, ... *)
type config_prover = {
name : string; (* "Alt-Ergo v2.95 (special)" *)
command : string; (* "exec why-limit %t %m alt-ergo %f" *)
......@@ -32,7 +30,9 @@ type config_prover = {
}
type main = {
loadpath : string list; (* "/usr/local/share/why/theories" *)
libdir : string; (* "/usr/local/lib/why/" *)
datadir : string; (* "/usr/local/share/why/" *)
loadpath : string list; (* "/usr/local/lib/why/theories" *)
timelimit : int; (* default prover time limit in seconds
(0 unlimited) *)
memlimit : int;
......@@ -41,16 +41,14 @@ type main = {
(* max number of running prover processes *)
}
type config = {
conf_file : string; (* "/home/innocent_user/.why.conf" *)
config : Rc.t;
}
val default_config : config
type config
(** if conf_file is not given, tries the following:
"$WHY_CONFIG"; "./why.conf"; "./.why.conf";
"$HOME/.why.conf"; "$USERPROFILE/.why.conf" *)
(** - If conf_file is given and the file doesn't exists Not_found is
raised.
- If "$WHY_CONFIG" is given and the file doesn't exists Not_found is raised
- otherwise tries the following:
"./why.conf"; "./.why.conf"; "$HOME/.why.conf";
"$USERPROFILE/.why.conf"; the built-in default_config *)
val read_config : string option -> config
val save_config : config -> unit
......@@ -61,6 +59,9 @@ val get_provers : config -> config_prover Mstr.t
val set_main : config -> main -> config
val set_provers : config -> config_prover Mstr.t -> config
val get_section : config -> string -> Rc.section option
val get_family : config -> string -> Rc.family
val set_section : config -> string -> Rc.section -> config
val set_family : config -> string -> Rc.family -> config
(** Replace the provers by autodetected one *)
val run_auto_detection : unit -> config_prover Mstr.t
src/ide/gconfig.ml
View file @ 176be2d1
......@@ -2,8 +2,9 @@
open Format
open Why
open Util
open Whyconf
open Rc
open Whyconf
type prover_data =
{ prover_id : string;
......@@ -46,7 +47,7 @@ let default_ide =
ide_tree_width = 512;
ide_task_height = 384;
ide_verbose = 0;
ide_default_editor = "";
ide_default_editor = ""; (*TODO : editor? *)
}
let load_ide section =
......@@ -83,7 +84,7 @@ let get_prover_data env id pr acc =
let load_config config =
let main = get_main config in
let ide = match get_section config.Whyconf.config "ide" with
let ide = match get_section config "ide" with
| None -> default_ide
| Some s -> load_ide s in
let provers = get_provers config in
......@@ -131,12 +132,20 @@ let save_config t =
let ide = set_int ide "task_height" t.task_height in
let ide = set_int ide "verbose" t.verbose in
let ide = set_string ide "default_editor" t.default_editor in
let rc = set_section config.Whyconf.config "ide" ide in
let config = {config with Whyconf.config = rc} in
let config = set_section config "ide" ide in
let config = set_provers config
(List.fold_left save_prover Mstr.empty t.provers) in
save_config config
let config =
eprintf "reading IDE config file@.";
read_config ()
let save_config () = save_config config
let get_main () = (get_main config.config)
(*
boomy icons
......@@ -144,7 +153,8 @@ let save_config t =
*)
let image ?size f =
let n = Filename.concat Whyconf.datadir (Filename.concat "images" (f^".png"))
let main = get_main () in
let n = Filename.concat main.datadir (Filename.concat "images" (f^".png"))
in
match size with
| None ->
......@@ -294,8 +304,10 @@ let preferences c =
let hb = GPack.hbox ~homogeneous:false ~packing:page1#add () in
let _ = GMisc.label ~text:"Nb of processes" ~packing:hb#add () 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. ();
nb_processes_spin#adjustment#set_value (float_of_int c.max_running_processes);
nb_processes_spin#adjustment#set_bounds
~lower:1. ~upper:16. ~step_incr:1. ();
nb_processes_spin#adjustment#set_value
(float_of_int c.max_running_processes);
let (_ : GtkSignal.id) =
nb_processes_spin#connect#value_changed ~callback:
(fun () -> c.max_running_processes <- nb_processes_spin#value_as_int)
......@@ -303,16 +315,19 @@ let preferences c =
(** page 2 **)
let label2 = GMisc.label ~text:"Provers" () in
let _page2 = GMisc.label ~text:"This page should display detected provers"
~packing:(fun w -> ignore(notebook#append_page ~tab_label:label2#coerce w)) ()
~packing:(fun w -> ignore(notebook#append_page
~tab_label:label2#coerce w)) ()
in
dialog#add_button "Close" `CLOSE ;
let ( _ : GWindow.Buttons.about) = dialog#run () in
eprintf "saving IDE config file@.";
save_config c;
save_config ();
dialog#destroy ()
let run_auto_detection gconfig =
let provers = run_auto_detection () in
let config = Autodetection.run_auto_detection gconfig.config in
gconfig.config <- config;
let provers = get_provers config in
gconfig.provers <- Mstr.fold (get_prover_data gconfig.env) provers [];
(*
......
src/ide/gconfig.mli
View file @ 176be2d1
......@@ -26,9 +26,11 @@ type t =
mutable config : Whyconf.config;
}
val read_config : unit -> t
val save_config : unit -> unit
val save_config : t -> unit
val config : t
val get_main : unit -> Whyconf.main
(***************)
(* boomy icons *)
......
src/ide/gmain.ml
View file @ 176be2d1
......@@ -54,7 +54,8 @@ let fname = match !file with
f
let lang =
let load_path = Filename.concat Whyconf.datadir "lang" in
let main = get_main () in
let load_path = Filename.concat main.datadir "lang" in
let languages_manager =
GSourceView2.source_language_manager ~default:true
in
......@@ -79,11 +80,7 @@ let source_text =
(* loading WhyIDE configuration *)
(********************************)
let gconfig =
eprintf "reading IDE config file@.";
read_config ()
let gconfig = Gconfig.config
(***********************)
(* Parsing input file *)
......@@ -133,7 +130,8 @@ let z3 = find_prover "Z3"
(*
let () =
printf "previously known goals:@\n";
List.iter (fun s -> printf "%s@\n" (Db.goal_task_checksum s)) (Db.root_goals ());
List.iter (fun s -> printf "%s@\n" (Db.goal_task_checksum s))
(Db.root_goals ());
printf "@."
*)
......@@ -204,7 +202,8 @@ module Model = struct
let time_column = cols#add Gobject.Data.string
let visible_column = cols#add Gobject.Data.boolean
(*
let bg_column = cols#add (Gobject.Data.unsafe_boxed (Gobject.Type.from_name "GdkColor"))
let bg_column = cols#add (Gobject.Data.unsafe_boxed
(Gobject.Type.from_name "GdkColor"))
*)
let name_renderer = GTree.cell_renderer_text [`XALIGN 0.]
......@@ -265,7 +264,7 @@ end
let exit_function () =
eprintf "saving IDE config file@.";
save_config gconfig;
save_config ();
GMain.quit ()
let w = GWindow.window
......@@ -310,7 +309,8 @@ let (_ : GtkSignal.id) =
(fun {Gtk.width=w;Gtk.height=_h} ->
gconfig.tree_width <- w)
let goals_model,filter_model,goals_view = Model.create ~packing:scrollview#add ()
let goals_model,filter_model,goals_view =
Model.create ~packing:scrollview#add ()
module Helpers = struct
......@@ -430,7 +430,8 @@ let rec prover_on_goal p g =
let name = p.prover_name in
let prover_row = goals_model#append ~parent:row () in
goals_model#set ~row:prover_row ~column:Model.icon_column !image_prover;
goals_model#set ~row:prover_row ~column:Model.name_column (name ^ " " ^ p.prover_version);
goals_model#set ~row:prover_row ~column:Model.name_column
(name ^ " " ^ p.prover_version);
goals_model#set ~row:prover_row ~column:Model.visible_column true;
goals_view#expand_row (goals_model#get_path row);
let a = { Model.prover = p;
......@@ -499,9 +500,12 @@ let split_unproved_goals () =
let callback subgoals =
if List.length subgoals >= 2 then
let split_row = goals_model#append ~parent:row () in
goals_model#set ~row:split_row ~column:Model.visible_column true;
goals_model#set ~row:split_row ~column:Model.name_column "split";
goals_model#set ~row:split_row ~column:Model.icon_column !image_transf;
goals_model#set ~row:split_row ~column:Model.visible_column
true;
goals_model#set ~row:split_row ~column:Model.name_column
"split";
goals_model#set ~row:split_row ~column:Model.icon_column
!image_transf;
let tr =
{ Model.parent_goal = g;
(*
......@@ -544,7 +548,8 @@ let split_unproved_goals () =
goals_view#expand_row (goals_model#get_path row)
in
Scheduler.apply_transformation ~callback split_transformation g.Model.task
Scheduler.apply_transformation ~callback
split_transformation g.Model.task
)
th.Model.goals
)
......
src/main.ml
View file @ 176be2d1
......@@ -288,8 +288,7 @@ let () =
option_iter (eprintf "Config file '%s' not found.@.") !opt_config;
option_iter
(eprintf "No config file found (required by '-P %s').@.") !opt_prover;
if !opt_config <> None || !opt_prover <> None then exit 1;
default_config
exit 1;
in
let main = get_main config in
......
src/util/rc.mli
View file @ 176be2d1
......@@ -17,23 +17,32 @@
(* *)
(**************************************************************************)
(** Parse rc files *)
exception Bad_value_type of string * string * string
(** key * expected * found *)
exception Key_not_found of string
(** key *)
exception Multiple_value of string
(** key *)
exception Yet_defined_key of string
(** key *)
exception Multiple_section of string
exception Section_b_family of string
exception Family_two_many_args of string
exception Not_exhaustive of string
exception Yet_defined_section of string
(** key *)
(* Exception *)
type rc_value =
| RCint of int
| RCbool of bool
| RCfloat of float
| RCstring of string
| RCident of string
(* exception SyntaxError *)
exception ExtraParameters of string
exception MissingParameters of string
(* exception UnknownSection of string *)
exception UnknownField of string
(* exception MissingSection of string *)
exception MissingField of string
exception DuplicateSection of string
exception DuplicateField of string * rc_value * rc_value
exception StringExpected of string * rc_value
exception IdentExpected of string * rc_value
exception IntExpected of string * rc_value
exception BoolExpected of string * rc_value
exception DuplicateProver of string
(* RC API *)
type t
type section
type family = (string * section) list
......
src/util/rc.mll
View file @ 176be2d1
......@@ -20,6 +20,7 @@
{
open Lexing
open Format
open Util
let get_home_dir () =
......@@ -29,18 +30,7 @@
try Sys.getenv "USERPROFILE"
with Not_found -> ""
exception Bad_value_type of string * string * string
(** key * expected * found *)
exception Key_not_found of string
(** key *)
exception Multiple_value of string
(** key *)
exception Multiple_section of string
exception Section_b_family of string
exception Family_two_many_args of string
exception Not_exhaustive of string
exception Yet_defined_section of string
exception Yet_defined_key of string
type rc_value =
| RCint of int
......@@ -49,6 +39,70 @@ type rc_value =
| RCstring of string
| RCident of string
(* Error handling *)
(* exception SyntaxError *)
exception ExtraParameters of string
exception MissingParameters of string
(* exception UnknownSection of string *)
exception UnknownField of string
(* exception MissingSection of string *)
exception MissingField of string
exception DuplicateSection of string
exception DuplicateField of string * rc_value * rc_value
exception StringExpected of string * rc_value
exception IdentExpected of string * rc_value
exception IntExpected of string * rc_value
exception BoolExpected of string * rc_value
exception DuplicateProver of string
let error ?loc e = match loc with
| None -> raise e
| Some loc -> raise (Loc.Located (loc, e))
(* conf files *)
let print_rc_value fmt = function
| RCint i -> fprintf fmt "%d" i
| RCbool b -> fprintf fmt "%B" b
| RCfloat f -> fprintf fmt "%f" f
| RCstring s -> fprintf fmt "%S" s (* "%s" %S ? *)
| RCident s -> fprintf fmt "%s" s
let () = Exn_printer.register (fun fmt e -> match e with
(* | SyntaxError -> *)
(* fprintf fmt "syntax error" *)
| ExtraParameters