Coq tactic: fixed compilation with outdated config file

parent 7a562df9
......@@ -830,12 +830,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 $<' &&) \
$(COQC) -byte -I lib/coq-tactic/ $< && \
WHY3NOCONFIG=42 $(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 $<' &&) \
$(COQC) -opt -I lib/coq-tactic/ $< && \
WHY3NOCONFIG=42 $(COQC) -opt -I lib/coq-tactic/ $< && \
touch src/coq-tactic/.why3-vo-opt
# depend and clean targets
......
......@@ -42,7 +42,15 @@ let debug =
try let _ = Sys.getenv "WHY3DEBUG" in true
with Not_found -> false
let config = Whyconf.read_config None
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)
let main = Whyconf.get_main config
let timelimit = timelimit main
......@@ -1114,7 +1122,8 @@ let why3tac ?(timelimit=timelimit) s gl =
if debug then Printexc.print_backtrace stderr; flush stderr;
error "Not a first order goal"
| Whyconf.ProverNotFound (_, s) ->
let pl = Mprover.fold (fun _ p l -> p.id :: l)
let pl =
Mprover.fold (fun _ p l -> if not p.interactive then p.id :: l else l)
(get_provers config) [] in
let msg = pr_str "No such prover `" ++ pr_str s ++ pr_str "'." ++
pr_spc () ++ pr_str "Available provers are:" ++ pr_fnl () ++
......
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