Commit 171085d9 authored by MARCHE Claude's avatar MARCHE Claude

Merge branch 'master' into new_system

Conflicts:
	src/session/session.ml
	src/session/termcode.ml
	src/why3session/why3session_html.ml
parents cb8e5a38 5c6821f9
......@@ -51,6 +51,7 @@ why3.conf
/bench/programs/good/loops/
/bench/programs/good/po/
/bench/valid/list/
/bench/ce/*.out
# /bin/
/bin/why3.byte
......
#!/bin/sh
dir=`dirname $0`
case "$1" in
"-update-oracle")
updateoracle=true;;
"")
updateoracle=false;;
*)
echo "$0: Unknown option '$1'"
exit 2
esac
run_cvc4_15 () {
echo -n " $1... "
$dir/../bin/why3prove.opt -P "CVC4,1.5-prerelease" --get-ce $1 > $1.out
if cmp $1.oracle $1.out > /dev/null 2>&1 ; then
echo "ok"
else
if $updateoracle; then
echo "Updating oracle for $1"
mv $1.out $1.oracle
else
echo "FAILED!"
echo "diff is the following:"
diff $1.oracle $1.out
fi
fi
}
for f in $dir/ce/*.mlw; do
run_cvc4_15 $f
done
theory T
use import int.Int
goal g0 : forall x "model":int. ("model" x >= 42) -> ("model" x + 3 <= 50)
constant g : int
goal g1 : forall x "model":int. ("model" g >= x)
goal g2 : forall x1 "model" "model_trace:X" x2 "model" x3 "model" x4 "model" x5 "model" x6 "model" x7 "model" x8 "model".
("model" "model_trace: X1 + 1 = 2" x1 + 1 = 2) ->
("model" x2 + 1 = 2) ->
("model" x3 + 1 = 2) ->
("model" x4 + 1 = 2) ->
("model" x5 + 1 = 2) ->
("model" x6 + 1 = 2) ->
("model" x7 + 1 = 2) ->
("model" x8 + 1 = 2) ->
("model" x1 + x2 + x3 + x4 + x5 + x6 + x7 + x8 = 2)
end
bench/ce/logic.mlw T g0 : Invalid (0.00s)
Counter-example model:File bench/ce/logic.mlw:
Line 6:
x = {"type" : "Integer" ,
"val" : "48" }
bench/ce/logic.mlw T g1 : Invalid (0.00s)
Counter-example model:File bench/ce/logic.mlw:
Line 10:
x = {"type" : "Integer" ,
"val" : "0" }
bench/ce/logic.mlw T g2 : Invalid (0.00s)
Counter-example model:File bench/ce/logic.mlw:
Line 12:
X = {"type" : "Integer" , "val" : "1" }
x2 = {"type" : "Integer" ,
"val" : "1" }
x3 = {"type" : "Integer" ,
"val" : "1" }
x4 = {"type" : "Integer" ,
"val" : "1" }
x5 = {"type" : "Integer" ,
"val" : "1" }
x6 = {"type" : "Integer" ,
"val" : "1" }
x7 = {"type" : "Integer" ,
"val" : "1" }
x8 = {"type" : "Integer" ,
"val" : "1" }
......@@ -137,6 +137,16 @@ else
echo "Make bench succeeded. " >> $REPORT
fi
# run regression bench for counterexamples
bench/ce-bench &> $OUT
if test "$?" != "0" ; then
echo "Counterexample regression tests FAILED" >> $REPORT
cat $OUT >> $REPORT
SUBJECT="$SUBJECT (CE regression failed)"
else
echo "Counterexample regression tests succeeded. " >> $REPORT
fi
# replay proofs
examples/regtests.sh &> $OUT
......
This diff is collapsed.
......@@ -207,7 +207,7 @@ let get_prover s =
else
raise (Whyconf.ProverAmbiguity (wc,fp,provers))
in
let drv = Driver.load_driver env cp.driver cp.extra_drivers in
let drv = Whyconf.load_driver main env cp.driver cp.extra_drivers in
Hashtbl.add provers s (cp, drv);
cp, drv
......
......@@ -191,10 +191,6 @@ let read_auto_detection_data main =
| Not_found ->
Loc.errorm "provers-detection-data.conf not found at %s@." filename
(* dead code
let provers_found = ref 0
*)
let read_editors main =
let filename = Filename.concat (Whyconf.datadir main)
"provers-detection-data.conf" in
......@@ -403,7 +399,7 @@ let generate_auto_strategies config =
(add_strategy
(add_strategy (add_strategy config inline) split) auto1) auto2
let detect_exec env main data acc exec_name =
let detect_exec env data acc exec_name =
let s = ask_prover_version env exec_name data.version_switch in
match s with
| None -> acc
......@@ -482,9 +478,9 @@ let detect_exec env main data acc exec_name =
{prover = prover;
command = c;
command_steps = c_steps;
driver = Filename.concat (datadir main) data.prover_driver;
driver = data.prover_driver;
editor = data.prover_editor;
in_place = data.prover_in_place;
in_place = data.prover_in_place;
interactive = (match data.kind with ITP -> true | ATP -> false);
extra_options = [];
extra_drivers = [] } in
......@@ -512,8 +508,8 @@ let detect_exec env main data acc exec_name =
else (unknown_version env exec_name data.prover_id prover_config priority;
acc)
let detect_prover env main acc data =
List.fold_left (detect_exec env main data) acc data.execs
let detect_prover env acc data =
List.fold_left (detect_exec env data) acc data.execs
(** add the prover unknown *)
let detect_unknown env detected =
......@@ -541,7 +537,7 @@ let convert_shortcuts env =
let run_auto_detection config =
let main = get_main config in
let l,env = read_auto_detection_data main in
let detected = List.fold_left (detect_prover env main) Mprover.empty l in
let detected = List.fold_left (detect_prover env) Mprover.empty l in
let length_detected = Mprover.cardinal detected in
let detected = detect_unknown env detected in
let length_unsupported_version =
......@@ -595,7 +591,7 @@ let add_prover_binary config id path =
let l = List.filter (fun p -> p.prover_id = id) l in
if l = [] then Loc.errorm "Unknown prover id: %s" id;
let detected = List.fold_left
(fun acc data -> detect_exec env main data acc path) Mprover.empty l in
(fun acc data -> detect_exec env data acc path) Mprover.empty l in
let detected = detect_unknown env detected in
if Mprover.is_empty detected then
Loc.errorm "File %s does not correspond to the prover id %s" path id;
......
......@@ -67,7 +67,7 @@ exception UnknownProp of (string list * string list)
exception FSymExpected of lsymbol
exception PSymExpected of lsymbol
let load_driver = let driver_tag = ref (-1) in fun env file extra_files ->
let load_driver_absolute = let driver_tag = ref (-1) in fun env file extra_files ->
let prelude = ref [] in
let regexps = ref [] in
let exitcodes = ref [] in
......
......@@ -15,10 +15,10 @@
type driver
val load_driver : Env.env -> string -> string list -> driver
val load_driver_absolute : Env.env -> string -> string list -> driver
(** loads a driver from a file
@param env environment to interpret theories
@param string driver file name
@param string driver file name (absolute path name)
@param string list additional driver files containing only theories
*)
......
......@@ -17,16 +17,27 @@ exception InvalidAnswer of string
let is_connected () = !socket <> None
let client_connect socket_name =
let client_connect ~fail socket_name =
if !socket <> None then raise AlreadyConnected;
if Sys.os_type = "Win32" then begin
let name = "\\\\.\\pipe\\" ^ socket_name in
socket := Some (Unix.openfile name [Unix.O_RDWR] 0)
end else begin
let sock = Unix.socket Unix.PF_UNIX Unix.SOCK_STREAM 0 in
Unix.connect sock (Unix.ADDR_UNIX socket_name);
try
let sock =
if Sys.os_type = "Win32" then
let name = "\\\\.\\pipe\\" ^ socket_name in
Unix.openfile name [Unix.O_RDWR] 0
else
let sock = Unix.socket Unix.PF_UNIX Unix.SOCK_STREAM 0 in
Unix.connect sock (Unix.ADDR_UNIX socket_name);
sock
in
socket := Some sock
end
with
| Unix.Unix_error(err, func, arg) when fail ->
Format.eprintf "client_connect: connection failed: %s (%s,%s) (socket_name=%s)@." (Unix.error_message err) func arg socket_name;
exit 2
| e when fail ->
Format.eprintf "client_connect failed for some unexpected reason: %s@\nAborting.@."
(Printexc.to_string e);
exit 2
let client_disconnect () =
match !socket with
......@@ -86,7 +97,7 @@ let recv_buf : Buffer.t = Buffer.create 1024
let connect_external socket_name =
if is_connected () then raise AlreadyConnected;
Buffer.clear recv_buf;
client_connect socket_name
client_connect ~fail:true socket_name
let connect_internal () =
if is_connected () then raise AlreadyConnected;
......@@ -104,11 +115,11 @@ let connect_internal () =
Unix.chdir cwd;
(* sleep before connecting, or the server will not be ready yet *)
let rec try_connect n d =
if n <= 0 then client_connect socket_name else
try client_connect socket_name with _ ->
if n <= 0 then client_connect ~fail:true socket_name else
try client_connect ~fail:false socket_name with _ ->
ignore (Unix.select [] [] [] d);
try_connect (pred n) (d *. 4.0) in
try_connect 4 0.1; (* 0.1, 0.4, 1.6, 6.4 *)
try_connect 5 0.1; (* 0.1, 0.4, 1.6, 6.4, 25.6 *)
at_exit (fun () -> (* only if succesfully connected *)
(try client_disconnect () with NotConnected -> ());
ignore (Unix.waitpid [] pid))
......
......@@ -396,8 +396,6 @@ let set_policies rc policy =
in
set_family rc "uninstalled_prover" family
let absolute_filename = Sysutil.absolutize_filename
exception DuplicateShortcut of string
let add_prover_shortcuts acc prover shortcuts =
......@@ -408,7 +406,7 @@ let add_prover_shortcuts acc prover shortcuts =
) acc shortcuts
let load_prover dirname (provers,shortcuts) section =
let load_prover (provers,shortcuts) section =
try
let name = get_string section "name" in
let version = get_string ~default:"" section "version" in
......@@ -423,7 +421,7 @@ let load_prover dirname (provers,shortcuts) section =
{ prover = prover;
command = get_string section "command";
command_steps = get_stringo section "command_steps";
driver = absolute_filename dirname (get_string section "driver");
driver = get_string section "driver";
in_place = get_bool ~default:false section "in_place";
editor = get_string ~default:"" section "editor";
interactive = get_bool ~default:false section "interactive";
......@@ -524,7 +522,7 @@ let load_main dirname section =
raise WrongMagicNumber;
{ libdir = get_string ~default:default_main.libdir section "libdir";
datadir = get_string ~default:default_main.datadir section "datadir";
loadpath = List.map (absolute_filename dirname)
loadpath = List.map (Sysutil.absolutize_filename dirname)
(get_stringl ~default:[] section "loadpath");
timelimit = get_int ~default:default_main.timelimit section "timelimit";
memlimit = get_int ~default:default_main.memlimit section "memlimit";
......@@ -550,7 +548,7 @@ let read_config_rc conf_file =
exception ConfigFailure of string (* filename *) * string
let get_dirname filename =
Filename.dirname (absolute_filename (Sys.getcwd ()) filename)
Filename.dirname (Sysutil.absolutize_filename (Sys.getcwd ()) filename)
let get_config (filename,rc) =
let dirname = get_dirname filename in
......@@ -560,7 +558,7 @@ let get_config (filename,rc) =
| Some main -> rc, load_main dirname main
in
let provers = get_simple_family rc "prover" in
let provers,shortcuts = List.fold_left (load_prover dirname)
let provers,shortcuts = List.fold_left load_prover
(Mprover.empty,Mstr.empty) provers in
let fam_shortcuts = get_simple_family rc "shortcut" in
let shortcuts = List.fold_left load_shortcut shortcuts fam_shortcuts in
......@@ -682,7 +680,7 @@ let merge_config config filename =
let main = match get_section rc "main" with
| None -> config.main
| Some rc ->
let loadpath = (List.map (absolute_filename dirname)
let loadpath = (List.map (Sysutil.absolutize_filename dirname)
(get_stringl ~default:[] rc "loadpath")) @ config.main.loadpath in
let plugins =
(get_stringl ~default:[] rc "plugin") @ config.main.plugins in
......@@ -713,15 +711,14 @@ let merge_config config filename =
if not (filter_prover fp p) then c
else
let opt = get_stringl ~default:[] section "option" in
let drv = List.map (absolute_filename dirname)
(get_stringl ~default:[] section "driver") in
let drv = get_stringl ~default:[] section "driver" in
{ c with
extra_options = opt @ c.extra_options;
extra_drivers = drv @ c.extra_drivers })
provers
) config.provers prover_modifiers in
let provers,shortcuts =
List.fold_left (load_prover dirname)
List.fold_left load_prover
(provers,config.prover_shortcuts) (get_simple_family rc "prover") in
(* modify editors *)
let editor_modifiers = get_family rc "editor_modifiers" in
......@@ -911,3 +908,15 @@ module Args = struct
Arg.usage (align_options options) usage;
exit 1
end
(** Loading drivers with relative names *)
let absolute_driver_file main s =
if Sys.file_exists s || String.contains s '/' || String.contains s '.' then s
else Filename.concat main.datadir (Filename.concat "drivers" (s ^ ".drv"))
let load_driver main env file extras =
let file = absolute_driver_file main file in
Driver.load_driver_absolute env file extras
......@@ -258,3 +258,11 @@ module Args : sig
val exit_with_usage : (string * Arg.spec * string) list -> string -> 'a
end
(** Loading drivers with relative names *)
val load_driver : main -> Env.env -> string -> string list -> Driver.driver
(** wrapper for loading a driver from a file that may be relative to the datadir.
See [Driver.load_driver_absolute]
*)
......@@ -534,7 +534,7 @@ let get_selected_row_references () =
let row_expanded b iter _path =
session_needs_saving := true;
let expand_g g = goals_view#expand_row g.S.goal_key#path in
let expand_g g = goals_view#expand_row (S.goal_key g)#path in
let expand_tr _ tr = goals_view#expand_row tr.S.transf_key#path in
let expand_m _ m = goals_view#expand_row m.S.metas_key#path in
match get_any_from_iter iter with
......@@ -545,8 +545,8 @@ let row_expanded b iter _path =
| S.Goal g ->
S.set_goal_expanded g b;
if b then begin
Session.PHstr.iter expand_tr g.S.goal_transformations;
Session.Mmetas_args.iter expand_m g.S.goal_metas
Session.PHstr.iter expand_tr (S.goal_transformations g);
Session.Mmetas_args.iter expand_m (S.goal_metas g)
end
| S.Transf tr ->
S.set_transf_expanded tr b;
......@@ -739,7 +739,7 @@ let notify any =
session_needs_saving := true;
let row,expanded =
match any with
| S.Goal g -> g.S.goal_key, g.S.goal_expanded
| S.Goal g -> (S.goal_key g), (S.goal_expanded g)
| S.Theory t -> t.S.theory_key, t.S.theory_expanded
| S.File f -> f.S.file_key, f.S.file_expanded
| S.Proof_attempt a -> a.S.proof_key,false
......@@ -750,7 +750,7 @@ let notify any =
(* name is set by notify since upgrade policy may update the prover name *)
goals_model#set ~row:row#iter ~column:name_column
(match any with
| S.Goal g -> S.goal_expl g
| S.Goal g -> S.goal_user_name g
| S.Theory th -> th.S.theory_name.Ident.id_string
| S.File f -> Filename.basename f.S.file_name
| S.Proof_attempt a ->
......@@ -770,7 +770,7 @@ let notify any =
goals_view#collapse_row row#path;
match any with
| S.Goal g ->
set_row_status row g.S.goal_verified
set_row_status row (S.goal_verified g)
| S.Theory th ->
set_row_status row th.S.theory_verified
| S.File file ->
......@@ -1408,8 +1408,8 @@ let (_ : GMenu.image_menu_item) =
~label:"Expand all" ~callback:(fun () -> goals_view#expand_all ()) ()
let rec collapse_verified = function
| S.Goal g when Opt.inhabited g.S.goal_verified ->
let row = g.S.goal_key in
| S.Goal g when Opt.inhabited (S.goal_verified g) ->
let row = S.goal_key g in
goals_view#collapse_row row#path
| S.Theory th when Opt.inhabited th.S.theory_verified ->
let row = th.S.theory_key in
......
This diff is collapsed.
......@@ -37,12 +37,6 @@ type proof_attempt_status =
| Done of Call_provers.prover_result (** external proof done *)
| InternalFailure of exn (** external proof aborted by internal error *)
type expl
(** An explanation gives hint about how the goal has been produced.
Allow to reattach proof_attempt to goal when the source file has been
modified.
*)
type task_option
(** The task can be removed and later reconstructible *)
......@@ -75,10 +69,12 @@ type idpos = {
information the user want. It is generated by the keygen argument
of the functions of this module *)
type 'a goal = private
type 'a goal
(*
= private
{ mutable goal_key : 'a;
goal_name : Ident.ident; (** ident of the task *)
goal_expl : expl;
mutable goal_expl : string option;
goal_parent : 'a goal_parent;
mutable goal_checksum : Termcode.checksum option; (** checksum of the task *)
mutable goal_shape : Termcode.shape; (** shape of the task *)
......@@ -89,6 +85,7 @@ type 'a goal = private
goal_transformations : 'a transf PHstr.t;
mutable goal_metas : 'a metas Mmetas_args.t;
}
*)
and 'a proof_attempt = private
{ proof_key : 'a;
......@@ -164,6 +161,14 @@ and 'a session = private
session_dir : string;
}
val goal_key : 'a goal -> 'a
val goal_name : 'a goal -> Ident.ident
val goal_verified : 'a goal -> float option
val goal_external_proofs : 'a goal -> 'a proof_attempt PHprover.t
val goal_transformations : 'a goal -> 'a transf PHstr.t
val goal_metas : 'a goal -> 'a metas Mmetas_args.t
val goal_expanded : 'a goal -> bool
val print_session : Format.formatter -> 'a session -> unit
(** Print a session with a pstree format (cf Tree module) *)
......@@ -313,8 +318,8 @@ val goal_task : 'key goal -> Task.task
val goal_task_option : 'key goal -> Task.task option
(** Return the task of a goal. *)
val goal_expl : 'key goal -> string
(** Return the explication of a goal *)
val goal_user_name : 'key goal -> string
(** Return a user-friendly name for a goal, derived from its name, its number in a sequence of sub-goals, and/or its explanation *)
val proof_verified : 'key proof_attempt -> float option
(** Return [Some t] if the proof is not obsolete and the result is
......
......@@ -329,7 +329,7 @@ let find_prover eS a =
let g = a.proof_parent in
begin
try
let _ = PHprover.find g.goal_external_proofs new_p in
let _ = PHprover.find (goal_external_proofs g) new_p in
(* yes, then we do nothing *)
None
with Not_found ->
......@@ -349,7 +349,7 @@ let find_prover eS a =
let g = a.proof_parent in
begin
try
let _ = PHprover.find g.goal_external_proofs new_p in
let _ = PHprover.find (goal_external_proofs g) new_p in
(* yes, then we do nothing *)
None
with Not_found ->
......@@ -533,7 +533,7 @@ let run_external_proof eS eT ?(cntexample=false) ?callback a =
let prover_on_goal eS eT ?callback ?(cntexample=false) ~limit p g =
let a =
try
let a = PHprover.find g.goal_external_proofs p in
let a = PHprover.find (goal_external_proofs g) p in
set_timelimit (limit.Call_provers.limit_time) a;
set_memlimit (limit.Call_provers.limit_mem) a;
a
......@@ -609,7 +609,7 @@ type report =
| No_former_result of Call_provers.prover_result
let push_report report (g,p,limits,r) =
(g.goal_name,p,limits,r)::report
(goal_name g,p,limits,r)::report
let check_external_proof ~use_steps eS eT todo a =
let callback a ap limits old s =
......@@ -635,9 +635,9 @@ let check_external_proof ~use_steps eS eT todo a =
let rec goal_iter_proof_attempt_with_release ~release f g =
let iter g = goal_iter_proof_attempt_with_release ~release f g in
PHprover.iter (fun _ a -> f a) g.goal_external_proofs;
PHstr.iter (fun _ t -> List.iter iter t.transf_goals) g.goal_transformations;
Mmetas_args.iter (fun _ t -> iter t.metas_goal) g.goal_metas;
PHprover.iter (fun _ a -> f a) (goal_external_proofs g);
PHstr.iter (fun _ t -> List.iter iter t.transf_goals) (goal_transformations g);
Mmetas_args.iter (fun _ t -> iter t.metas_goal) (goal_metas g);
if release then release_task g
let check_all ?(release=false) ~use_steps ?filter eS eT ~callback =
......@@ -733,7 +733,7 @@ let rec play_on_goal_and_children eS eT ~limit todo l g =
| None, Done { Call_provers.pr_answer = Call_provers.Valid } ->
Call_provers.limit_max limit pa.proof_limit, true
| _ -> acc)
g.goal_external_proofs (limit, false) in
(goal_external_proofs g) (limit, false) in
let callback _key status =
if not (running status) then Todo._done todo () in
if auto_proved then begin
......@@ -832,7 +832,7 @@ let edit_proof_v3 ~cntexample eS sched ~default_editor callback a =
in
let file = update_edit_external_proof ~cntexample eS a in
Debug.dprintf debug "[Editing] goal %s with command '%s' on file %s@."
a.proof_parent.goal_name.Ident.id_string editor file;
(goal_name a.proof_parent).Ident.id_string editor file;
schedule_edition sched editor file (fun res -> callback a res)
let edit_proof ~cntexample eS sched ~default_editor a =
......@@ -893,7 +893,7 @@ let proof_removable a =
let rec clean = function
| Goal g when Opt.inhabited g.goal_verified ->
| Goal g when Opt.inhabited (goal_verified g) ->
iter_goal
(fun a -> if proof_removable a then remove_proof_attempt a)
(fun t ->
......
......@@ -40,7 +40,7 @@ let convert_unknown_prover ~keygen env_session =
let pks = Mprover.find_def [] pr.proof_prover unknown_provers in
List.iter (fun pk ->
(* If such a prover already exists we add nothing *)
if not (PHprover.mem pr.proof_parent.goal_external_proofs pk) then
if not (PHprover.mem (goal_external_proofs pr.proof_parent) pk) then
ignore (copy_external_proof ~keygen ~prover:pk pr)
) pks;
) env_session.session
......@@ -64,12 +64,12 @@ let transform_proof_attempt ?notify ~keygen env_session tr_name =
remove_external_proof ?notify pr;
let tr =
try
PHstr.find g.goal_transformations tr_name
PHstr.find (goal_transformations g) tr_name
with Not_found ->
add_registered_transformation ~keygen env_session tr_name g
in
let add_pa sg =
if not (PHprover.mem sg.goal_external_proofs pr.proof_prover) then
if not (PHprover.mem (goal_external_proofs sg) pr.proof_prover) then
ignore (copy_external_proof ~keygen ~goal:sg
~attempt_status:Interrupted pr)
in
......
This diff is collapsed.
......@@ -14,7 +14,7 @@
val arg_extra_expl_prefix : string * Arg.spec * string
val goal_expl_task:
root:bool -> Task.task -> Ident.ident * string option * Task.task
root:bool -> Task.task -> Ident.ident * string * Task.task
val search_labels :
(Ident.Slab.t -> 'a list) -> Term.term -> 'a list
......@@ -26,7 +26,9 @@ val search_labels :
(** Shapes *)
(*
val reset_dict : unit -> unit
*)
val current_shape_version : int
......@@ -40,7 +42,7 @@ val print_shape: Format.formatter -> shape -> unit
(* val t_shape_buf : ?version:int -> Term.term -> shape *)
(** returns the shape of a given term *)
val t_shape_task: ?version:int -> Task.task -> shape
val t_shape_task: ?version:int -> expl:string -> Task.task -> shape
(** returns the shape of a given task *)
(** Checksums *)
......
......@@ -15,7 +15,6 @@ open Stdlib
open Whyconf
open Theory
open Task
open Driver
let usage_msg = sprintf
"Usage: %s [options] [[file|-] [-T <theory> [-G <goal>]...]...]..."
......@@ -155,11 +154,7 @@ let option_list = [
let config, _, env =
Whyconf.Args.initialize option_list add_opt_file usage_msg
let driver_file s =
if Sys.file_exists s || String.contains s '/' || String.contains s '.' then s
else Filename.concat Config.datadir (Filename.concat "drivers" (s ^ ".drv"))
let opt_driver = ref (match List.rev_map driver_file !opt_driver with
let opt_driver = ref (match !opt_driver with
| f::ef -> Some (f, ef)
| [] -> None)
......@@ -391,7 +386,7 @@ let do_input env drv = function
let () =
try
let load (f,ef) = load_driver env f ef in
let load (f,ef) = load_driver (Whyconf.get_main config) env f ef in
let drv = Opt.map load !opt_driver in
Queue.iter (do_input env drv) opt_queue
with e when not (Debug.test_flag Debug.stack_trace) ->
......
......@@ -73,17 +73,13 @@ let opt_output =
exit 1
| Some d -> d
let driver_file s =
if Sys.file_exists s || String.contains s '/' || String.contains s '.' then s
else Filename.concat Config.datadir (Filename.concat "drivers" (s ^ ".drv"))
let opt_driver =
try match List.rev_map driver_file !opt_driver with
try match !opt_driver with
| [] ->
eprintf "Realization driver (-D) is required.@.";
exit 1