Commit eb5705af authored by MARCHE Claude's avatar MARCHE Claude

whyconf file

parent e0d795c4
......@@ -32,6 +32,7 @@ datarootdir=@datarootdir@
exec_prefix=@exec_prefix@
BINDIR=$(DESTDIR)@bindir@
LIBDIR=$(DESTDIR)@libdir@
DATADIR=$(DESTDIR)@datarootdir@
EXE=@EXE@
STRIP=@STRIP@
......@@ -82,7 +83,7 @@ all: @OCAMLBEST@
# Why library
#############
LIBGENERATED = src/config.ml src/util/rc.ml \
LIBGENERATED = src/config.ml src/userconf/rc.ml \
src/parser/parser.mli src/parser/parser.ml src/parser/parser.output \
src/parser/lexer.ml src/driver/driver_lexer.ml \
src/driver/driver_parser.mli src/driver/driver_parser.ml \
......@@ -91,7 +92,7 @@ LIBGENERATED = src/config.ml src/util/rc.ml \
depend: $(LIBGENERATED)
LIBDIRS=core util parser transform driver printer
LIBDIRS=core util parser transform driver printer userconf
LIBCLEAN=$(addprefix src/, $(LIBDIRS))
LIBCLEAN:=$(addsuffix /*.cm[iox], $(LIBCLEAN)) \
$(addsuffix /*.annot, $(LIBCLEAN)) \
......@@ -104,14 +105,14 @@ clean::
include Version
doc/version.tex src/config.ml: Version version.sh config.status
BINDIR=$(BINDIR) LIBDIR=$(LIBDIR) COQVER=@COQVER@ ./version.sh
BINDIR=$(BINDIR) LIBDIR=$(LIBDIR) DATADIR=$(DATADIR) COQVER=@COQVER@ ./version.sh
CORE_CMO := ident.cmo ty.cmo term.cmo pattern.cmo decl.cmo theory.cmo\
task.cmo pretty.cmo trans.cmo env.cmo register.cmo
CORE_CMO := $(addprefix src/core/,$(CORE_CMO))
UTIL_CMO := pp.cmo loc.cmo prtree.cmo util.cmo hashcons.cmo \
sysutil.cmo hashweak.cmo rc.cmo
sysutil.cmo hashweak.cmo
UTIL_CMO := $(addprefix src/util/,$(UTIL_CMO))
PARSER_CMO := ptree.cmo parser.cmo lexer.cmo denv.cmo typing.cmo
......@@ -125,14 +126,17 @@ TRANSFORM_CMO := simplify_recursive_definition.cmo inlining.cmo\
TRANSFORM_CMO := $(addprefix src/transform/,$(TRANSFORM_CMO))
DRIVER_CMO := driver_ast.cmo call_provers.cmo dynlink_compat.cmo \
driver_parser.cmo driver_lexer.cmo driver.cmo whyrc.cmo
driver_parser.cmo driver_lexer.cmo driver.cmo
DRIVER_CMO := $(addprefix src/driver/,$(DRIVER_CMO))
PRINTER_CMO := print_real.cmo alt_ergo.cmo why3.cmo smt.cmo coq.cmo
PRINTER_CMO := $(addprefix src/printer/,$(PRINTER_CMO))
USERCONF_CMO := rc.cmo whyconf.cmo
USERCONF_CMO := $(addprefix src/userconf/,$(USERCONF_CMO))
LIBCMO = src/config.cmo $(UTIL_CMO) $(CORE_CMO) $(PARSER_CMO) $(DRIVER_CMO)\
$(TRANSFORM_CMO) $(PRINTER_CMO)
$(TRANSFORM_CMO) $(PRINTER_CMO) $(USERCONF_CMO)
LIBCMX = $(LIBCMO:.cmo=.cmx)
LIBINCLUDES = $(addprefix -I src/, $(LIBDIRS))
......
......@@ -2,16 +2,20 @@
open Why
let autodetection () =
Whyrc.add_driver_config "Alt-Ergo 0.9" "drivers/alt_ergo.drv" "alt-ergo";
Whyrc.add_driver_config "Z3 2.2" "drivers/z3.drv" "z3";
Whyrc.add_driver_config "CVC3 2.1" "drivers/cvc3.drv" "cvc3";
Whyrc.add_driver_config "Coq 8.3" "drivers/coq.drv" "coqc";
Whyrc.save ()
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 () =
try Whyrc.read_config_file ()
try Whyconf.read_config_file ()
with Not_found ->
Format.eprintf "No whyrc file found. Running autodetection of provers.@.";
Format.eprintf "No .why.conf file found. Running autodetection of provers.@.";
autodetection ()
......
/**************************************************************************/
/* */
/* Copyright (C) 2008 */
/* Dillon PARIENTE */
/* Copyright (C) 2008-2010 */
/* Dillon PARIENTE 2008 */
/* Claude MARCHE 2010 */
/* */
/* This software is free software; you can redistribute it and/or */
/* modify it under the terms of the GNU Library General Public */
......@@ -47,6 +48,7 @@ int main(int argc, char *argv[]) {
printf("%s: Error: when allocating %d bytes in memory\n", argv[0], (int) s);
return -1;
}
*p = '\0';
for (i = 2; i < argc; i++) {
strncat(p, argv[i], strlen(argv[i]));
if (i < argc - 1) strcat(p, " ");
......
open Format
let default_why3rc_file () =
let default_whyconf_file () =
let home = Rc.get_home_dir () in
let dir = Filename.concat home ".why" in
(* TODO: create dir if not exists *)
Filename.concat dir "why3rc"
Filename.concat home ".why.conf"
let known_provers : (string, string * Driver.driver option ref) Hashtbl.t =
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 rc file@."
"Warning: ignored field `%s' in section [prover] of conf file@."
field)
info;
Hashtbl.add known_provers !name (!driv,ref None)
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_why3rc_file()) () =
let read_config_file ?(name = default_whyconf_file()) () =
if !config_file <> "" then begin
eprintf "Whyrc.read_config_file: cannot load config file twice@.";
eprintf "Whyconf.read_config_file: cannot load config file twice@.";
exit 2;
end;
config_file := name;
......@@ -37,6 +64,7 @@ let read_config_file ?(name = default_why3rc_file()) () =
(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)
......@@ -44,36 +72,53 @@ let read_config_file ?(name = default_why3rc_file()) () =
let get_driver name env =
if !config_file = "" then begin
eprintf "Whyrc.get_driver: config file not loaded yet@.";
eprintf "Whyconf.get_driver: config file not loaded yet@.";
exit 2;
end;
let (file,driv) = Hashtbl.find known_provers name in
match !driv with
let pi = Hashtbl.find known_provers name in
match pi.driver with
| Some d -> d
| None ->
let d = Driver.load_driver file env in
driv := Some d;
let d = Driver.load_driver pi.driver_file env in
pi.driver <- Some d;
d
let add_driver_config id file cmd =
(* TODOL the command [cmd] should be inserted in the template [file]
(* 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 (file, ref None)
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 "Whyrc.save: config file not loaded yet@.";
eprintf "Whyconf.save: config file not loaded yet@.";
exit 2;
end;
let ch = open_out !config_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 (driv,_) ->
(fun name pi ->
fprintf fmt "[prover]@.";
fprintf fmt "name = \"%s\"@." name;
fprintf fmt "driver = \"%s\"@." driv;
fprintf fmt "invocation= \"%s\"@." pi.invocation;
fprintf fmt "driver = \"%s\"@." pi.driver_file;
fprintf fmt "@.")
known_provers;
close_out ch
......
......@@ -5,8 +5,8 @@
val read_config_file: ?name:string -> unit -> unit
(** reads the config file from file [name]. The
default rc file name is "$HOME/.why/why3rc" if HOME is set, or
"$USERPROFILE/.why/why3rc" if USERPROFILE is set, or "./.why/why3rc"
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
......@@ -16,11 +16,20 @@ 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
(** [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.
......
......@@ -15,6 +15,7 @@ echo "let version = \"$VERSION\"" >> $WHYVF
echo "let date = \""`date`"\"" >> $WHYVF
echo "let bindir = \"$BINDIR\"" >> $WHYVF
echo "let libdir = \"$LIBDIR/why\"" >> $WHYVF
echo "let datadir = \"$DATADIR/why\"" >> $WHYVF
# Doc
......
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