Commit eb751c1b authored by MARCHE Claude's avatar MARCHE Claude

allow relative pathnames for drivers stored in the Why3 config file

If drivers in why3.conf are simple names like "alt_ergo", then the driver file
is search as <datadir>/drivers/alt_ergo.drv

This behavior is now the same as when a driver is given with option -D on the
command line for why3prove, why3replay or why3extract

Reminder: the datadir is either given as
1) the environment variable WHY3DATA
2) the field "datadir" of the [main] section of the
   why3 config file if exists
3) or by default the compile-time datadir
parent 3e625c03
......@@ -42,7 +42,7 @@ let provers =
Whyconf.Mprover.fold
(fun _ p acc ->
try
let d = Driver.load_driver env p.Whyconf.driver [] in
let d = Whyconf.load_driver main env p.Whyconf.driver [] in
(p,d)::acc
with e ->
let p = p.Whyconf.prover in
......
......@@ -85,7 +85,7 @@ let env : Env.env = Env.create_env (Whyconf.loadpath main)
(* loading the Alt-Ergo driver *)
let alt_ergo_driver : Driver.driver =
try
Driver.load_driver env alt_ergo.Whyconf.driver []
Whyconf.load_driver main env alt_ergo.Whyconf.driver []
with e ->
eprintf "Failed to load driver for alt-ergo: %a@."
Exn_printer.exn_printer e;
......
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
*)
......
......@@ -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
......@@ -259,3 +259,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]
*)
......@@ -1903,10 +1903,11 @@ let load_prover eS prover =
let r = match r with
| None -> None
| Some pr ->
let dr = Driver.load_driver eS.env
pr.Whyconf.driver pr.Whyconf.extra_drivers in
Some { prover_config = pr;
prover_driver = dr}
let dr = Whyconf.load_driver (Whyconf.get_main eS.whyconf)
eS.env
pr.Whyconf.driver pr.Whyconf.extra_drivers in
Some { prover_config = pr;
prover_driver = dr}
in
PHprover.add eS.loaded_provers prover r;
r
......
......@@ -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>]...]...]..."
......@@ -151,11 +150,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)
......@@ -385,7 +380,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
| f::ef ->
Driver.load_driver env f ef
Whyconf.load_driver (Whyconf.get_main config) env f ef
with e when not (Debug.test_flag Debug.stack_trace) ->
eprintf "%a@." Exn_printer.exn_printer e;
exit 1
......
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