Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit 90d38215 authored by Andrei Paskevich's avatar Andrei Paskevich

rewrite Whyconf, put an example of config in why.conf

parent d72aa5b9
(**************************************************************************)
(* *)
(* 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
let default_whyconf_file () =
let home = Rc.get_home_dir () in
Filename.concat home ".why.conf"
type prover_info =
{
invocation : string;
driver_file : string;
mutable driver : Driver.driver option;
}
let loadpath = ref []
let timelimit = ref 10
let get_loadpath () = !loadpath
let get_timelimit () = !timelimit
let known_provers : (string, prover_info) Hashtbl.t =
Hashtbl.create 7
let load_prover_info info =
let name = ref "" in
let driv = ref "" in
let invoc = ref "" in
List.iter
(function
| ("name",Rc.RCstring s) -> name := s
| ("invocation",Rc.RCstring s) -> invoc := s
| ("driver",Rc.RCstring s) -> driv := s
| (field,_) ->
eprintf
"Warning: ignored field `%s' in section [prover] of conf file@."
field)
info;
Hashtbl.add known_provers !name
{ invocation = !invoc; driver_file = !driv ; driver = None }
let load_main_settings args =
List.iter
(function
| ("timelimit", Rc.RCint n) -> timelimit := n
| ("loadpath", Rc.RCstring s) -> loadpath := s :: !loadpath
| (field,_) ->
eprintf
"Warning: ignored field `%s' in section [main] of conf file@."
field)
args
let config_file = ref ""
let read_config_file ?(name = default_whyconf_file()) () =
if !config_file <> "" then begin
eprintf "Whyconf.read_config_file: cannot load config file twice@.";
exit 2;
end;
config_file := name;
let rc = Rc.from_file name in
List.iter
(fun (key,args) ->
match key with
| "prover" -> load_prover_info args
| "main" -> load_main_settings args
| _ ->
eprintf
"Warning: ignored section [%s] in config file '%s'@." key name)
rc
let get_driver name env =
if !config_file = "" then begin
eprintf "Whyconf.get_driver: config file not loaded yet@.";
exit 2;
end;
let pi = Hashtbl.find known_provers name in
match pi.driver with
| Some d -> d
| None ->
let d = Driver.load_driver pi.driver_file env in
pi.driver <- Some d;
d
let add_driver_config id file cmd =
(* TODO
check that id does not exist yet
the command [cmd] should be inserted in the template [file]
and the result copied into ".why/<id>.drv"
corresponding values must be added into [known_provers]
*)
Hashtbl.add known_provers id
{ invocation = cmd; driver_file = file; driver = None; }
let set_loadpath s = loadpath := s
let add_loadpath s = loadpath := s :: !loadpath
let set_timelimit n = timelimit := n
let save () =
if !config_file = "" then begin
eprintf "Whyconf.save: config file not loaded yet@.";
exit 2;
end;
let ch = open_out !config_file in
open Util
(* Error handling *)
type error =
| SyntaxError
| UnknownSection of string
| UnknownField of string
| MissingSection of string
| MissingField of string
| DuplicateSection of string
| DuplicateField of string * Rc.rc_value * Rc.rc_value
| StringExpected of string * Rc.rc_value
| IdentExpected of string * Rc.rc_value
| IntExpected of string * Rc.rc_value
| DuplicateProver of string
exception Error of error
let error ?loc e = match loc with
| None -> raise (Error e)
| Some loc -> raise (Loc.Located (loc, Error e))
let print_rc_value fmt = function
| Rc.RCint i -> fprintf fmt "%d" i
| Rc.RCbool b -> fprintf fmt "%B" b
| Rc.RCfloat f -> fprintf fmt "%f" f
| Rc.RCstring s -> fprintf fmt "\"%s\"" s
| Rc.RCident s -> fprintf fmt "%s" s
let report fmt = function
| SyntaxError ->
fprintf fmt "syntax error"
| UnknownSection s ->
fprintf fmt "unknown section '%s'" s
| UnknownField s ->
fprintf fmt "unknown field '%s'" s
| MissingSection s ->
fprintf fmt "section '%s' is missing" s
| MissingField s ->
fprintf fmt "field '%s' is missing" s
| DuplicateSection s ->
fprintf fmt "section '%s' is already given" s
| DuplicateField (s,u,v) ->
fprintf fmt "cannot set field '%s' to %a, as it is already set to %a"
s print_rc_value v print_rc_value u
| StringExpected (s,v) ->
fprintf fmt "cannot set field '%s' to %a: a string is expected"
s print_rc_value v
| IdentExpected (s,v) ->
fprintf fmt "cannot set field '%s' to %a: an identifier is expected"
s print_rc_value v
| IntExpected (s,v) ->
fprintf fmt "cannot set field '%s' to %a: an integer is expected"
s print_rc_value v
| DuplicateProver s ->
fprintf fmt "prover %s is already listed" s
(* Configuration file *)
type config_prover = {
description : string; (* "Alt-Ergo v2.95 (special)" *)
command : string; (* "exec why-limit %t %m alt-ergo %f" *)
driver_file : string; (* "/usr/local/share/why/drivers/ergo-spec.drv" *)
}
type config = {
conf_file : string; (* "/home/innocent_user/.why.conf" *)
loadpath : string list; (* "/usr/local/share/why/theories" *)
timelimit : int option; (* default prover time limit in seconds *)
memlimit : int option; (* default prover memory limit in megabytes *)
provers : config_prover Mstr.t; (* indexed by short identifiers *)
}
let to_string key = function
| Rc.RCstring s -> s
| v -> error (StringExpected (key,v))
let to_ident key = function
| Rc.RCident s -> s
| v -> error (IdentExpected (key,v))
let to_int key = function
| Rc.RCint i -> i
| v -> error (IntExpected (key,v))
let set_string key r v = match !r with
| Some u -> error (DuplicateField (key,Rc.RCstring u,v))
| None -> r := Some (to_string key v)
let set_ident key r v = match !r with
| Some u -> error (DuplicateField (key,Rc.RCident u,v))
| None -> r := Some (to_ident key v)
let set_int key r v = match !r with
| Some u -> error (DuplicateField (key,Rc.RCint u,v))
| None -> r := Some (to_int key v)
let get_field f = function
| None -> error (MissingField f)
| Some v -> v
let load_prover provers al =
let nam = ref None in
let dsc = ref None in
let cmd = ref None in
let drv = ref None in
let load (key, value) = match key with
| "name" -> set_ident key nam value
| "description" -> set_string key dsc value
| "command" -> set_string key cmd value
| "driver" -> set_string key drv value
| _ -> error (UnknownField key)
in
List.iter load al;
let prover = {
description = get_field "description" !dsc;
command = get_field "command" !cmd;
driver_file = get_field "driver" !drv }
in
let n = get_field "name" !nam in
if Mstr.mem n provers then error (DuplicateProver n);
Mstr.add n prover provers
let load_main main al =
let lp = ref [] in
let tl = ref None in
let ml = ref None in
let load (key, value) = match key with
| "loadpath" -> lp := (to_string key value) :: !lp
| "timelimit" -> set_int key tl value
| "memlimit" -> set_int key ml value
| _ -> error (UnknownField key)
in
List.iter load al;
{ main with
loadpath = List.rev !lp;
timelimit = !tl;
memlimit = !ml;
provers = Mstr.empty }
let read_config ?conf_file () =
let filename = match conf_file with
| Some filename -> filename
| None -> begin try Sys.getenv "WHY_CONFIG" with Not_found ->
if Sys.file_exists "why.conf" then "why.conf" else
if Sys.file_exists ".why.conf" then ".why.conf" else
Filename.concat (Rc.get_home_dir ()) ".why.conf"
end
in
let rc = try Rc.from_file filename with
| Failure "lexing" -> error SyntaxError
in
let main = ref {
conf_file = filename;
loadpath = [];
timelimit = None;
memlimit = None;
provers = Mstr.empty }
in
let provers = ref Mstr.empty in
let have_main = ref false in
let load (key, al) = match key with
| "main" when !have_main -> error (DuplicateSection key)
| "main" -> main := load_main !main al
| "prover" -> provers := load_prover !provers al
| _ -> error (UnknownSection key)
in
List.iter load rc;
{ !main with provers = !provers }
let save_config config =
let ch = open_out config.conf_file in
let fmt = Format.formatter_of_out_channel ch in
fprintf fmt "[main]@.";
List.iter
(fun s ->
fprintf fmt "loadpath = \"%s\"@." s)
!loadpath;
fprintf fmt "timelimit = %d@." !timelimit;
fprintf fmt "@.";
Hashtbl.iter
(fun name pi ->
fprintf fmt "[prover]@.";
fprintf fmt "name = \"%s\"@." name;
fprintf fmt "invocation= \"%s\"@." pi.invocation;
fprintf fmt "driver = \"%s\"@." pi.driver_file;
fprintf fmt "@.")
known_provers;
fprintf fmt "[main]@\n";
List.iter (fprintf fmt "loadpath = \"%s\"@\n") config.loadpath;
Util.option_iter (fprintf fmt "timelimit = %d@\n") config.timelimit;
Util.option_iter (fprintf fmt "memlimit = %d@\n") config.memlimit;
fprintf fmt "@.";
let print_prover name prover =
fprintf fmt "[prover]@\n";
fprintf fmt "name = %s@\n" name;
fprintf fmt "description = \"%s\"@\n" prover.description;
fprintf fmt "command = \"%s\"@\n" prover.command;
fprintf fmt "driver = \"%s\"@\n@." prover.driver_file;
in
Mstr.iter print_prover config.provers;
close_out ch
let known_provers () =
Hashtbl.fold (fun key _ acc -> key::acc) known_provers []
(**************************************************************************)
(* *)
(* 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 Util
type config_prover = {
description : string; (* "Alt-Ergo v2.95 (special)" *)
command : string; (* "exec why-limit %t %m alt-ergo %f" *)
driver_file : string; (* "/usr/local/share/why/drivers/ergo-spec.drv" *)
}
type config = {
conf_file : string; (* "/home/innocent_user/.why.conf" *)
loadpath : string list; (* "/usr/local/share/why/theories" *)
timelimit : int option; (* default prover time limit in seconds *)
memlimit : int option; (* default prover memory limit in megabytes *)
provers : config_prover Mstr.t; (* indexed by short identifiers *)
}
(* if conf_file is not given, tries the following:
"$WHY_CONFIG"; "./why.conf"; "./.why.conf";
"$HOME/.why.conf"; "$USERPROFILE/.why.conf" *)
val read_config : ?conf_file:string -> unit -> config
val save_config : config -> unit
(** error reporting *)
type error
exception Error of error
val report : Format.formatter -> error -> unit
(** {2 access to user configuration and drivers} *)
val read_config_file: ?name:string -> unit -> unit
(** reads the config file from file [name]. The
default conf file name is "$HOME/.why.conf" if HOME is set, or
"$USERPROFILE/.why.conf" if USERPROFILE is set, or "./.why3.conf"
otherwise *)
val known_provers: unit -> string list
(** returns the list of known prover ids. *)
val get_driver: string -> Env.env -> Driver.driver
(** returns the driver associated to the given prover id
@raises Not_found if no driver of this name exist *)
val get_loadpath : unit -> string list
val get_timelimit : unit -> int
(** {2 configuration update} *)
val add_loadpath : string -> unit
val set_loadpath : string list -> unit
val set_timelimit : int -> unit
val add_driver_config: string -> string -> string -> unit
(** [add_driver_config id file cmd] adds in the current configuration
a new prover named [id], associated to a new driver description
file built from the template [file] and the command line [cmd].
This new setting is recorded in the user's rc file when [save] is called.
{!add_driver_config} *)
val save : unit -> unit
(** saves the current configuration into the same file as given in
[read_config_file] *)
open Format
open Why
open Whyconf
let autodetection () =
let alt_ergo = {
description = "Alt-Ergo";
command = "alt-ergo %s";
driver_file = "drivers/alt_ergo.drv" }
in
let z3 = {
description = "Z3";
command = "z3 -smt -in";
driver_file = "drivers/z3.drv" }
in
let cvc3 = {
description = "CVC3";
command = "cvc3 -lang smt";
driver_file = "drivers/cvc3.drv" }
in
let coq = {
description = "Coq";
command = "coqc %s";
driver_file = "drivers/coq.drv" }
in
let provers = Util.Mstr.empty in
let provers = Util.Mstr.add "alt-ergo" alt_ergo provers in
let provers = Util.Mstr.add "z3" z3 provers in
let provers = Util.Mstr.add "cvc3" cvc3 provers in
let provers = Util.Mstr.add "coq" coq provers in
let config = {
conf_file = "why.conf.test";
loadpath = ["theories"];
timelimit = Some 10;
memlimit = None;
provers = provers }
in
save_config config
(*
Whyconf.set_loadpath [Filename.concat Config.datadir "theories"];
Whyconf.set_driverpath (Filename.concat Config.datadir "drivers");
*)
Whyconf.add_driver_config "Alt-Ergo 0.9" "alt_ergo.drv" "alt-ergo";
Whyconf.add_driver_config "Z3 2.2" "z3.drv" "z3";
Whyconf.add_driver_config "CVC3 2.1" "cvc3.drv" "cvc3";
Whyconf.add_driver_config "Coq 8.3" "coq.drv" "coqc";
Whyconf.save ()
*)
let () =
let config =
try
Whyconf.read_config_file ()
Whyconf.read_config ()
with Not_found ->
eprintf "No .why.conf file found. Running autodetection of provers.@.";
eprintf "No config file found. Running autodetection of provers.@.";
autodetection ();
exit 0
let provers = Whyconf.known_provers ()
let provers = Util.Mstr.fold (fun name _ acc -> name :: acc) config.provers []
let () =
printf "Provers: ";
......
[main]
loadpath = "theories"
timelimit = 10
[prover]
name = alt-ergo
description = "Alt-Ergo"
command = "alt-ergo %s"
driver = "drivers/alt_ergo.drv"
[prover]
name = coq
description = "Coq"
command = "coqc %s"
driver = "drivers/coq.drv"
[prover]
name = cvc3
description = "CVC3"
command = "cvc3 -lang smt"
driver = "drivers/cvc3.drv"
[prover]
name = z3
description = "Z3"
command = "z3 -smt -in"
driver = "drivers/z3.drv"
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