errors in config file and regeneration

parent e3f2f52f
......@@ -194,6 +194,7 @@ why.conf
/src/why3doc/*.annot
# /tests/
/tests/test-jcf/
/tests/test-claude/
# /examples/
......
......@@ -411,7 +411,7 @@ clean::
local_config: bin/why3config.@OCAMLBEST@
WHY3LIB=$(PWD) WHY3DATA=$(PWD)/share bin/why3config.@OCAMLBEST@ \
--autodetect-provers --conf_file .why.conf
--detect --conf_file .why.conf
install_no_local::
cp -f bin/why3config.@OCAMLBEST@ $(BINDIR)/why3config
......
......@@ -127,10 +127,10 @@ printer, as explained in the corresponding section.
If the user's configuration file is already present,
\texttt{why3config} will only reset unset variables to default value,
but will not try to detect provers.
The option \texttt{--autodetect-provers} should be used to force
The option \texttt{--detect-provers} should be used to force
\why\ to detect again the available
provers and to replace them in the configuration file. The option
\texttt{--autodetect-plugins} will do the same for plugins.
\texttt{--detect-plugins} will do the same for plugins.
\section{The \texttt{why3} command-line tool}
\label{sec:why3ref}
......
......@@ -181,7 +181,7 @@ autodetection of external provers. We have already seen how to do
it in the \why\ GUI. On the command line, this is done as follows
(here ``\texttt{>}'' is the prompt):
\begin{verbatim}
> why3config --autodetect-provers
> why3config --detect
\end{verbatim}
This prints some information messages on what detections are attempted. To know which
provers have been successfully detected, you can do as follows.
......
......@@ -61,10 +61,12 @@ let option_list = Arg.align [
($WHY_CONFIG), otherwise use the default one";
"--config", Arg.String (set_oref conf_file),
" same as -C";
"--autodetect-provers", Arg.Set autoprovers,
" autodetect the provers in the $PATH";
"--autodetect-plugins", Arg.Set autoplugins,
" autodetect the plugins in the default library directories";
"--detect-provers", Arg.Set autoprovers,
" detect the provers in $PATH";
"--detect-plugins", Arg.Set autoplugins,
" detect the plugins in default library directories";
"--detect", Arg.Unit (fun () -> autoprovers := true; autoplugins := true),
" detect both provers and plugins";
"--install-plugin", Arg.String add_plugin,
" install a plugin to the actual libdir";
"--dont-save", Arg.Clear save,
......@@ -112,7 +114,7 @@ let plugins_auto_detection config =
let main = Array.fold_left fold main files in
set_main config main
let () =
let main () =
(** Parse the command line *)
Arg.parse option_list anon_file usage_msg;
......@@ -142,12 +144,16 @@ let () =
(** Main *)
let config =
try read_config !conf_file
with Not_found ->
let conf_file = match !conf_file with
| None -> Sys.getenv "WHY_CONFIG"
| Some f -> f in
default_config conf_file in
try
read_config !conf_file
with
| Rc.CannotOpen (f, s)
| Whyconf.ConfigFailure (f, s) ->
autoprovers := true;
autoplugins := true;
eprintf "warning: cannot read config file %s (%s)@." f s;
default_config f
in
let main = get_main config in
(* let main = option_apply main (fun d -> {main with libdir = d})
!libdir in *)
......@@ -156,19 +162,29 @@ let () =
let main = try Queue.fold install_plugin main plugins with Exit -> exit 1 in
let config = set_main config main in
let conf_file = get_conf_file config in
let conf_file_doesnt_exist = not (Sys.file_exists conf_file) in
if conf_file_doesnt_exist then
printf "Config file %s doesn't exist, \
so autodetection of provers and plugins is automatically triggered@."
conf_file;
if not (Sys.file_exists conf_file) then begin
autoprovers := true;
autoplugins := true;
end;
let config =
if !autoprovers || conf_file_doesnt_exist
if !autoprovers
then Autodetection.run_auto_detection config
else config in
else config
in
let config =
if !autoplugins || conf_file_doesnt_exist
if !autoplugins
then plugins_auto_detection config
else config in
else config
in
if !save then begin
printf "Save config to %s@." conf_file;
save_config config end
save_config config
end
let () =
try
main ()
with e when not (Debug.test_flag Debug.stack_trace) ->
eprintf "%a@." Exn_printer.exn_printer e;
exit 1
......@@ -28,7 +28,9 @@ open Rc
If a configuration doesn't contain the actual magic number we don't use it.
*)
let magicnumber = 1
exception WrongMagicNumber
(* lib and shared dirs *)
......@@ -141,7 +143,7 @@ let default_main =
let set_main rc main =
let section = empty_section in
let section = set_int section "magicnumber" magicnumber in
let section = set_int section "magic" magicnumber in
let section = set_string ~default:default_main.private_libdir
section "libdir" main.private_libdir in
let section = set_string ~default:default_main.private_datadir
......@@ -185,8 +187,8 @@ let load_prover dirname provers (id,section) =
} provers
let load_main dirname section =
if get_int ~default:0 section "magicnumber" <> magicnumber
then raise WrongMagicNumber;
if get_int ~default:0 section "magic" <> magicnumber then
raise WrongMagicNumber;
{ private_libdir = get_string ~default:default_main.private_libdir
section "libdir";
private_datadir = get_string ~default:default_main.private_datadir
......@@ -210,15 +212,22 @@ let read_config_rc conf_file =
else raise Exit
end
in
filename,Rc.from_file filename
filename, Rc.from_file filename
exception ConfigFailure of string (* filename *) * string
let () = Exn_printer.register (fun fmt e -> match e with
| ConfigFailure (f, s) ->
Format.fprintf fmt "error in config file %s: %s" f s
| _ -> raise e)
let get_config (filename,rc) =
let dirname = Filename.dirname filename in
let rc, main =
match get_section rc "main" with
| None -> set_main rc default_main,default_main
| Some main ->
rc, load_main dirname main in
| None -> raise (ConfigFailure (filename, "no main section"))
| Some main -> rc, load_main dirname main
in
let provers = get_family rc "prover" in
let provers = List.fold_left (load_prover dirname) Mstr.empty provers in
{ conf_file = filename;
......@@ -227,26 +236,26 @@ let get_config (filename,rc) =
provers = provers;
}
let default_config conf_file = get_config (conf_file,Rc.empty)
let default_config conf_file =
get_config (conf_file, set_main Rc.empty default_main)
let read_config conf_file =
let filenamerc = try read_config_rc conf_file
with
| Exit -> (default_conf_file,Rc.empty) in
try get_config filenamerc
let filenamerc =
try
read_config_rc conf_file
with Exit ->
default_conf_file, set_main Rc.empty default_main
in
try
get_config filenamerc
with WrongMagicNumber ->
let (filename,_) = filenamerc in
let bak = filename^".bak" in
Format.eprintf
"Warning : your configuration file %s doesn't correspond to the \
current version of Why3. It is moved to %s. The default config is used.@."
filename bak;
Sys.rename filename bak;
default_config filename
let filename, _ = filenamerc in
raise (ConfigFailure (filename, "outdated config file; rerun why3config"))
let save_config config = to_file config.conf_file config.config
let save_config config =
let filename = config.conf_file in
if Sys.file_exists filename then Sys.rename filename (filename ^ ".bak");
to_file filename config.config
let get_main config = config.main
let get_provers config = config.provers
......
......@@ -31,15 +31,17 @@ type config
which are dealt by it ({!Whyconf.get_main}, {!Whyconf.set_main},
{!Whyconf.get_provers}, {!Whyconf.set_provers} *)
exception ConfigFailure of string (* filename *) * string
val read_config : string option -> config
(** [read_config conf_file] :
- If conf_file is given and the file doesn't exists Not_found is
- If conf_file is given and the file doesn't exist Rc.CannotOpen is
raised.
- If "$WHY_CONFIG" is given and the file doesn't exists Not_found is raised
- otherwise tries the following, Not_found is never raised :
"./why.conf"; "./.why.conf"; "$HOME/.why.conf";
"$USERPROFILE/.why.conf"; the built-in default_config with default
configuration filename*)
- If "$WHY3CONFIG" is given and the file doesn't exist Rc.CannotOpen
is raised
- otherwise we try reading "$HOME/.why.conf" (or
"$USERPROFILE/.why.conf" under Windows) and, if not present, we return
the built-in default_config with default configuration filename *)
val save_config : config -> unit
(** [save_config config] save the configuration *)
......
......@@ -135,9 +135,12 @@ let load_config config =
}
let read_config () =
try
let config = Whyconf.read_config None in
load_config config
with e when not (Debug.test_flag Debug.stack_trace) ->
eprintf "@.%a@." Exn_printer.exn_printer e;
exit 1
let save_config t =
let save_prover _ pr acc =
......@@ -168,7 +171,7 @@ let save_config t =
let config =
eprintf "reading IDE config file...@?";
let c= read_config () in
let c = read_config () in
eprintf " done.@.";
c
......
......@@ -214,11 +214,15 @@ let () =
if !opt_type_only then Debug.set_flag Typing.debug_type_only;
(** Configuration *)
let config = try read_config !opt_config with Not_found ->
option_iter (eprintf "Config file '%s' not found.@.") !opt_config;
option_iter
(eprintf "No config file found (required by '-P %s').@.") !opt_prover;
exit 1;
let config =
(* try *)
read_config !opt_config
(* with *)
(* | ConfigFailure (f, s) -> *)
(* option_iter (eprintf "Config file '%s' not found.@.") !opt_config; *)
(* option_iter *)
(* (eprintf "No config file found (required by '-P %s').@.") !opt_prover; *)
(* exit 1; *)
in
let main = get_main config in
......
......@@ -185,16 +185,19 @@ val check_exhaustive : section -> Util.Sstr.t -> unit
@raise UnknownField if it is not the case
*)
exception CannotOpen of string * string
exception SyntaxErrorFile of string * string
val from_channel : in_channel -> t
(** [from_channel cin] returns the Rc of the input channel [cin]
@raise Failure "lexing" in case of incorrect syntax
@raise SyntaxErrorFile in case of incorrect syntax
@raise ExtraParameters if a section header has more than one argument
*)
val from_file : string -> t
(** [from_file filename] returns the Rc of the file [filename]
@raise Not_found is [filename] does not exists
@raise Failure "lexing" in case of incorrect syntax
@raise CannotOpen is [filename] does not exist
@raise SyntaxErrorFile in case of incorrect syntax
@raise ExtraParameters if a section header has more than one argument
*)
......
......@@ -251,6 +251,9 @@ let push_record () =
current_rec := [];
current_list := []
exception SyntaxError of string
let syntax_error s = raise (SyntaxError s)
}
let space = [' ' '\t' '\r' '\n']+
......@@ -275,7 +278,7 @@ rule record = parse
| (ident as key) space* '=' space*
{ value key lexbuf }
| _ as c
{ failwith ("Rc: invalid keyval pair starting with " ^ String.make 1 c) }
{ syntax_error ("invalid keyval pair starting with " ^ String.make 1 c) }
and header keylist = parse
| (ident as key) space*
......@@ -285,9 +288,9 @@ and header keylist = parse
current_rec := List.rev keylist;
record lexbuf }
| eof
{ failwith "Rc: unterminated header" }
{ syntax_error "unterminated header" }
| _ as c
{ failwith ("Rc: invalid header starting with " ^ String.make 1 c) }
{ syntax_error ("invalid header starting with " ^ String.make 1 c) }
and value key = parse
| integer as i
......@@ -309,9 +312,9 @@ and value key = parse
{ push_field key (RCident (*kind_of_ident*) id);
record lexbuf }
| eof
{ failwith "Rc: unterminated keyval pair" }
{ syntax_error "unterminated keyval pair" }
| _ as c
{ failwith ("Rc: invalid value starting with " ^ String.make 1 c) }
{ syntax_error ("invalid value starting with " ^ String.make 1 c) }
and string_val key = parse
| '"'
......@@ -332,7 +335,7 @@ and string_val key = parse
Buffer.add_char buf c;
string_val key lexbuf }
| eof
{ failwith "Rc: unterminated string" }
{ syntax_error "unterminated string" }
{
......@@ -342,19 +345,25 @@ let from_channel cin =
record (from_channel cin);
make_t !current
exception CannotOpen of string * string
exception SyntaxErrorFile of string * string
let from_file f =
let c =
try open_in f
with Sys_error _ -> raise Not_found
(* TODO: can we catch only the "file not found" errors
and let other Sys_error's just come through? *)
(*
Format.eprintf "Cannot open file %s@." f;
exit 1
*)
try open_in f with Sys_error s -> raise (CannotOpen (f, s))
in
try let r = from_channel c in close_in c; r
with e -> close_in c; raise e
try
let r = from_channel c in close_in c; r
with
| SyntaxError s -> close_in c; raise (SyntaxErrorFile (f, s))
| e -> close_in c; raise e
let () = Exn_printer.register (fun fmt e -> match e with
| CannotOpen (_, s) ->
Format.fprintf fmt "system error: `%s'" s
| SyntaxErrorFile (f, s) ->
Format.fprintf fmt "syntax error in %s: %s" f s
| _ -> raise e)
let to_formatter fmt t =
let print_kv k fmt v = fprintf fmt "%s = %a" k print_rc_value v 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