Use the "driver=" directives from extra configuration files.

src/bench/benchdb.ml

@@ -53,10 +53,10 @@ let rec goal whyconf env path dbgoal wgoal =
         Db.status_and_time proof_attempt in
       if obsolete then () else
       let prover_name = Db.prover_name prover_id in
-      let driver,command =
+      let driver, extra, command =
         try
           let p = Mstr.find prover_name (Whyconf.get_provers whyconf) in
-          p.Whyconf.driver ,p.Whyconf.command
+          p.Whyconf.driver, p.Whyconf.extra_drivers, p.Whyconf.command
         with
       (* TODO add exceptions pehaps inside rc.ml in fact*)
           | Not_found ->
@@ -84,7 +84,7 @@ let rec goal whyconf env path dbgoal wgoal =
       let call_prover : Call_provers.pre_prover_call =
         Driver.prove_task
           ~timelimit:(truncate (ceil (0.1 +. time *. 1.1)))
-          ~command (load_driver env driver) ?old wgoal in
+          ~command (load_driver env driver extra) ?old wgoal in
       BenchUtil.new_external_proof (call_prover,cb)
     with Exit -> ()
   in

src/bench/benchrc.ml

@@ -76,7 +76,7 @@ let read_tools absf wc map (name,section) =
   let provers = get_stringl ~default:[] section "prover" in
   let find_provers s =
     try let p = Mstr.find s (get_provers wc) in
-        s,p.driver ,p.command
+        s, p.driver, p.extra_drivers, p.command
     with
       (* TODO add exceptions pehaps inside rc.ml in fact*)
       | Not_found -> eprintf "Prover %s not found.@." s; exit 1 in
@@ -85,9 +85,9 @@ let read_tools absf wc map (name,section) =
     try
       let driver = get_string section "driver" in
       let command = get_string section "command" in
-      ("driver",absf driver,command) :: provers
+      ("driver", absf driver, [], command) :: provers
     with MissingField _ -> provers in
-  let load_driver (n,d,c) = n,Driver.load_driver env d,c in
+  let load_driver (n,d,e,c) = n, (Driver.load_driver env d e), c in
   let provers = List.map load_driver provers in
   let create_tool (n,driver,command) =
     { tval = {tool_name = name; prover_name = n; tool_db =

src/bench/whybench.ml

@@ -358,7 +358,7 @@ let () =
     in
     { B.tval   = {B.tool_name = "cmdline"; prover_name = s; tool_db = None};
       ttrans   = [Trans.identity,None];
-      tdriver  = load_driver env prover.driver;
+      tdriver  = load_driver env prover.driver prover.extra_drivers;
       tcommand = prover.command;
       tenv     = env;
       tuse     = [opt_theo,None];

src/driver/driver.ml

@@ -80,7 +80,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 ->
+let load_driver = let driver_tag = ref (-1) in fun env file extra_files ->
   let prelude   = ref [] in
   let regexps   = ref [] in
   let exitcodes = ref [] in
@@ -180,6 +180,7 @@ let load_driver = let driver_tag = ref (-1) in fun env file ->
     List.iter (add_local th) trl
   in
   List.iter add_theory f.f_rules;
+  List.iter (fun f -> List.iter add_theory (load_file f).f_rules) extra_files;
   incr driver_tag;
   {
     drv_env         = env;

src/driver/driver.mli

@@ -23,10 +23,11 @@
 
 type driver
 
-val load_driver : Env.env -> string -> driver
+val load_driver : Env.env -> string -> string list -> driver
 (** loads a driver from a file
     @param env TODO
     @param string driver file name
+    @param string list additional driver files containing only theories
 *)
 
 (** {2 use a driver} *)

src/ide/session.ml

@@ -38,7 +38,7 @@ type prover_data =
 
 let get_prover_data env id pr acc =
   try
-    let dr = Driver.load_driver env pr.Whyconf.driver in
+    let dr = Driver.load_driver env pr.Whyconf.driver pr.Whyconf.extra_drivers in
     Util.Mstr.add id
       { prover_id = id ;
         prover_name = pr.Whyconf.name;

src/main.ml

@@ -168,9 +168,9 @@ let option_list = Arg.align [
       "<meta_name>=<string> Add a string meta to every task";
   "--meta", Arg.String add_opt_meta,
       " same as -M";
-  "-D", Arg.String (fun s -> opt_driver := Some s),
+  "-D", Arg.String (fun s -> opt_driver := Some (s, [])),
       "<file> Specify a prover's driver (conflicts with -P)";
-  "--driver", Arg.String (fun s -> opt_driver := Some s),
+  "--driver", Arg.String (fun s -> opt_driver := Some (s, [])),
       " same as -D";
   "-o", Arg.String (fun s -> opt_output := Some s),
       "<dir> Print the selected goals to separate files in <dir>";
@@ -352,7 +352,7 @@ let () = try
             s (Whyconf.get_conf_file config); exit 1
       in
       opt_command := Some prover.command;
-      opt_driver := Some prover.driver
+      opt_driver := Some (prover.driver, prover.extra_drivers)
   | None ->
       ()
   end;
@@ -569,7 +569,7 @@ let do_input env drv = function
 let () =
   try
     let env = Env.create_env !opt_loadpath in
-    let drv = Util.option_map (load_driver env) !opt_driver in
+    let drv = Util.option_map (fun (f,ef) -> load_driver env f ef) !opt_driver in
     Queue.iter (do_input env drv) opt_queue;
     if !opt_token_count then
       Format.printf "Total: %d annot/%d programs, ratio = %.3f@."