Commit b7a50941 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Fix some build issues when theories/plugins are obsolete or not yet installed.

The empty string is now a recognized configuration filename. It means that
the default configuration with an empty loadpath should be loaded. It also
means it will not be saved.

This removes the need for a WHY3NOCONFIG environment variable and some
tricks based on the WHY3LOADPATH variable. This also removes the need for
a /dev/null file.
parent c14ce1d1
......@@ -829,12 +829,12 @@ src/coq-tactic/g_why3tac.ml: src/coq-tactic/g_why3tac.ml4
src/coq-tactic/.why3-vo-byte: lib/coq-tactic/Why3.v lib/coq-tactic/why3tac.cma
$(if $(QUIET),@echo 'Coqc $<' &&) \
WHY3NOCONFIG=42 $(COQC) -byte -I lib/coq-tactic/ $< && \
WHY3CONFIG="" $(COQC) -byte -I lib/coq-tactic/ $< && \
touch src/coq-tactic/.why3-vo-byte
src/coq-tactic/.why3-vo-opt: lib/coq-tactic/Why3.v lib/coq-tactic/why3tac.cmxs
$(if $(QUIET),@echo 'Coqc $<' &&) \
WHY3NOCONFIG=42 $(COQC) -opt -I lib/coq-tactic/ $< && \
WHY3CONFIG="" $(COQC) -opt -I lib/coq-tactic/ $< && \
touch src/coq-tactic/.why3-vo-opt
test-coq-tactic.byte: src/coq-tactic/.why3-vo-byte
......@@ -953,11 +953,11 @@ clean::
rm -f $(COQVO) $(COQVD) $(addsuffix .glob, $(COQLIBS_FILES))
update-coq: bin/why3 drivers/coq-realizations.aux
for f in $(COQLIBS_INT_ALL_FILES); do WHY3LOADPATH=theories bin/why3.@OCAMLBEST@ --realize -D drivers/coq-realize.drv -T int.$$f -o lib/coq/int/; done
for f in $(COQLIBS_REAL_FILES); do WHY3LOADPATH=theories bin/why3.@OCAMLBEST@ --realize -D drivers/coq-realize.drv -T real.$$f -o lib/coq/real/; done
for f in $(COQLIBS_NUMBER_FILES); do WHY3LOADPATH=theories bin/why3.@OCAMLBEST@ --realize -D drivers/coq-realize.drv -T number.$$f -o lib/coq/number/; done
for f in $(COQLIBS_SET_FILES); do WHY3LOADPATH=theories bin/why3.@OCAMLBEST@ --realize -D drivers/coq-realize.drv -T set.$$f -o lib/coq/set/; done
for f in $(COQLIBS_FP_FILES); do WHY3LOADPATH=theories bin/why3.@OCAMLBEST@ --realize -D drivers/coq-realize.drv -T floating_point.$$f -o lib/coq/floating_point/; done
for f in $(COQLIBS_INT_ALL_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/coq-realize.drv -T int.$$f -o lib/coq/int/; done
for f in $(COQLIBS_REAL_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/coq-realize.drv -T real.$$f -o lib/coq/real/; done
for f in $(COQLIBS_NUMBER_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/coq-realize.drv -T number.$$f -o lib/coq/number/; done
for f in $(COQLIBS_SET_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/coq-realize.drv -T set.$$f -o lib/coq/set/; done
for f in $(COQLIBS_FP_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/coq-realize.drv -T floating_point.$$f -o lib/coq/floating_point/; done
else
......@@ -1301,7 +1301,7 @@ STDMODFILES = $(addsuffix .mlw, $(addprefix modules/, $(STDMODS)))
stdlibdoc: $(STDLIBFILES) $(STDMODFILES) bin/why3doc.@OCAMLBEST@
mkdir -p doc/stdlibdoc
rm -f doc/stdlibdoc/style.css
WHY3LOADPATH=theories bin/why3doc.@OCAMLBEST@ -L modules \
WHY3CONFIG="" bin/why3doc.@OCAMLBEST@ -L theories -L modules \
-o doc/stdlibdoc --title "Why3 Standard Library" \
$(STDLIBFILES) $(STDMODFILES)
......
......@@ -43,9 +43,6 @@ let debug =
let config =
try
let _ = Sys.getenv "WHY3NOCONFIG" in
Whyconf.default_config ""
with Not_found -> try
Whyconf.read_config None
with Whyconf.ConfigFailure(file, msg) ->
error (file ^ ": " ^ msg)
......
......@@ -427,7 +427,7 @@ let run_auto_detection config =
config
let list_prover_ids () =
let config = default_config "/dev/null" in
let config = default_config "" in
let main = get_main config in
let l,_ = read_auto_detection_data main in
let s = List.fold_left (fun s p -> Sstr.add p.prover_id s) Sstr.empty l in
......
......@@ -210,17 +210,20 @@ type config = {
provers_upgrade_policy : prover_upgrade_policy Mprover.t;
}
let default_main =
let empty_main =
{
libdir = Config.libdir;
datadir = Config.datadir;
loadpath = default_loadpath;
loadpath = [];
timelimit = 5; (* 5 seconds *)
memlimit = 1000; (* 1 Mb *)
running_provers_max = 2; (* two provers run in parallel *)
plugins = [];
}
let default_main =
{ empty_main with loadpath = default_loadpath }
let set_main rc main =
let section = empty_section in
let section = set_int section "magic" magicnumber in
......@@ -453,7 +456,10 @@ let read_config_rc conf_file =
else raise Exit
end
in
filename, Rc.from_file filename
let rc =
if filename = "" then set_main Rc.empty empty_main
else Rc.from_file filename in
filename, rc
exception ConfigFailure of string (* filename *) * string
......@@ -631,8 +637,10 @@ let merge_config config filename =
let save_config config =
let filename = config.conf_file in
Sysutil.backup_file filename;
to_file filename config.config
if filename <> "" then begin
Sysutil.backup_file filename;
to_file filename config.config
end
let get_main config = config.main
let get_provers config = config.provers
......
......@@ -37,17 +37,23 @@ exception DuplicateShortcut of string
val read_config : string option -> config
(** [read_config conf_file] :
- If conf_file is given and the file doesn't exist Rc.CannotOpen is
raised.
- If "$WHY3CONFIG" is given and the file doesn't exist Rc.CannotOpen
is raised
- otherwise we try reading "$HOME/.why3.conf" (or
"$USERPROFILE/.why3.conf" under Windows) and, if not present, we return
the built-in default_config with default configuration filename *)
- If conf_file is given, then
- if it is an empty string, an empty config is loaded,
- if the file doesn't exist, Rc.CannotOpen is raised,
- otherwise the content of the file is parsed and returned.
- If conf_file is None and the WHY3CONFIG environment
variable exists, then the above steps are executed with
the content of the variable (possibly empty).
- If neither conf_file nor WHY3CONFIG are present, the file
"$HOME/.why3.conf" (or "$USERPROFILE/.why3.conf" under
Windows) is checked for existence:
- if present, the content is parsed and returned,
- otherwise, we return the built-in default_config with a
default configuration filename. *)
val merge_config : config -> string -> config
(** [merge_config config filename] merge the content of [filename]
into [config]( *)
into [config] *)
val save_config : config -> unit
(** [save_config config] save the configuration *)
......
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