Add an --extra-config option to load additional configuration.

The loaded files are slimmed down version of the standard configuration
file. They only support the following sections and fields:

[main]
  loadpath=
  plugin=
[prover ...]
  option=
  driver=

It is also possible to define brand new [prover] sections.

For now, the only supported frontends are why3 and why3ide.

src/driver/autodetection.ml

@@ -160,7 +160,9 @@ let detect_exec main data com =
               command = c;
               driver  = Filename.concat (datadir main) data.prover_driver;
               editor = data.prover_editor;
-              interactive = match data.kind with ITP -> true | ATP -> false; }
+              interactive = (match data.kind with ITP -> true | ATP -> false);
+              extra_options = [];
+              extra_drivers = [] }
       end
     with Not_found ->
       begin

src/driver/whyconf.ml

@@ -59,6 +59,8 @@ type config_prover = {
   version : string;   (* "v2.95" *)
   editor  : string;
   interactive : bool;
+  extra_options : string list;
+  extra_drivers : string list;
 }
 
 type main = {
@@ -181,6 +183,8 @@ let load_prover dirname provers (id,section) =
       version = get_string ~default:"" section "version";
       editor  = get_string ~default:"" section "editor";
       interactive = get_bool ~default:false section "interactive";
+      extra_options = [];
+      extra_drivers = [];
     } provers
 
 let load_main dirname section =
@@ -248,6 +252,29 @@ let read_config conf_file =
     Format.bprintf b "%a" Exn_printer.exn_printer e;
     raise (ConfigFailure (fst filenamerc, Buffer.contents b))
 
+let merge_config config filename =
+  let dirname = Filename.dirname filename in
+  let rc = Rc.from_file filename in
+  let main = match get_section rc "main" with
+    | None -> config.main
+    | Some rc ->
+      let loadpath = (List.map (absolute_filename dirname)
+        (get_stringl ~default:[] rc "loadpath")) @ config.main.loadpath in
+      let plugins = (get_stringl ~default:[] rc "plugin") @ config.main.plugins in
+      { config.main with loadpath = loadpath; plugins = plugins } in
+  let provers = get_family rc "prover" in
+  let provers = List.fold_left
+    (fun provers (id, section) ->
+      match Mstr.find_option id provers with
+      | None -> load_prover dirname provers (id, section)
+      | Some c ->
+        let opt = (get_stringl ~default:[] section "option") @ c.extra_options in
+        let drv = (List.map (absolute_filename dirname)
+          (get_stringl ~default:[] section "driver")) @ c.extra_options in
+        Mstr.add id { c with extra_options = opt ; extra_drivers = drv } provers
+    ) config.provers provers in
+  { config with main = main; provers = provers }
+
 let save_config config =
   let filename = config.conf_file in
   Sysutil.backup_file filename;

src/driver/whyconf.mli

@@ -43,6 +43,9 @@ val read_config : string option -> config
     "$USERPROFILE/.why3.conf" under Windows) and, if not present, we return
     the built-in default_config with default configuration filename *)
 
+val merge_config : config -> string -> config
+(** [merge_config config filename] merge the content of [filename] into [config] *)
+
 val save_config : config -> unit
 (** [save_config config] save the configuration *)
 
@@ -89,10 +92,12 @@ type config_prover = {
   version : string;   (* "v2.95" *)
   editor  : string;   (* Dedicated editor *)
   interactive : bool; (* Interative theorem prover *)
+  extra_options : string list;
+  extra_drivers : string list;
 }
 
 val get_provers : config  -> config_prover Mstr.t
-(** [get_main config] get the prover family stored in the Rc file. The
+(** [get_provers config] get the prover family stored in the Rc file. The
     keys are the unique ids of the prover (argument of the family) *)
 
 val set_provers : config -> config_prover Mstr.t -> config

src/ide/gconfig.ml

@@ -164,6 +164,7 @@ let load_config config =
   }
 
 let save_config t =
+  (*
   let _save_prover _ pr acc =
     Mstr.add pr.Session.prover_id
       {
@@ -174,6 +175,7 @@ let save_config t =
         editor  = pr.Session.editor;
         interactive = pr.Session.interactive;
       } acc in
+  *)
   let config = t.config in
   let config = set_main config
     (set_limits (get_main config)
@@ -201,9 +203,10 @@ let save_config t =
 *)
   save_config config
 
-let read_config conf_file =
+let read_config conf_file extra_files =
   try
     let config = Whyconf.read_config conf_file in
+    let config = List.fold_left Whyconf.merge_config config extra_files in
     load_config config
   with e when not (Debug.test_flag Debug.stack_trace) ->
     eprintf "@.%a@." Exn_printer.exn_printer e;
@@ -215,9 +218,9 @@ let config,read_config =
     match !config with
       | None -> invalid_arg "configuration not yet loaded"
       | Some conf -> conf),
-  (fun conf_file ->
+  (fun conf_file extra_files ->
     eprintf "[Info] reading IDE config file...@?";
-    let c = read_config conf_file in
+    let c = read_config conf_file extra_files in
     eprintf " done.@.";
     config := Some c)
 
@@ -597,7 +600,7 @@ let run_auto_detection gconfig =
 
 (* let () = eprintf "[Info] end of configuration initialization@." *)
 
-let read_config conf_file = read_config conf_file; init ()
+let read_config conf_file extra_files = read_config conf_file extra_files; init ()
 
 (*
 Local Variables:

src/ide/gconfig.mli

@@ -41,7 +41,7 @@ type t =
       mutable config : Whyconf.config;
     }
 
-val read_config : string option -> unit
+val read_config : string option -> string list -> unit
 (** None use the default config *)
 
 val save_config : unit -> unit

src/ide/gmain.ml

@@ -38,6 +38,7 @@ let includes = ref []
 let file = ref None
 let opt_version = ref false
 let opt_config = ref None
+let opt_extra = ref []
 
 let spec = Arg.align [
   ("-L",
@@ -53,6 +54,8 @@ let spec = Arg.align [
       "<file> Read configuration from <file>";
   "--config", Arg.String (fun s -> opt_config := Some s),
       " same as -C";
+  "--extra-config", Arg.String (fun s -> opt_extra := !opt_extra @ [s]),
+      "<file> Read additional configuration from <file>";
 (*
   ("-f",
    Arg.String (fun s -> input_files := s :: !input_files),
@@ -84,7 +87,7 @@ let () =
     exit 0
   end
 
-let () = Gconfig.read_config !opt_config
+let () = Gconfig.read_config !opt_config !opt_extra
 
 let fname = match !file with
   | None ->

src/main.ml

@@ -90,6 +90,7 @@ let add_opt_meta meta =
   opt_metas := (meta_name,meta_arg)::!opt_metas
 
 let opt_config = ref None
+let opt_extra = ref []
 let opt_parser = ref None
 let opt_prover = ref None
 let opt_loadpath = ref []
@@ -135,6 +136,8 @@ let option_list = Arg.align [
       "<file> Read configuration from <file>";
   "--config", Arg.String (fun s -> opt_config := Some s),
       " same as -C";
+  "--extra-config", Arg.String (fun s -> opt_extra := !opt_extra @ [s]),
+      "<file> Read additional configuration from <file>";
   "-L", Arg.String (fun s -> opt_loadpath := s :: !opt_loadpath),
       "<dir> Add <dir> to the library search path";
   "--library", Arg.String (fun s -> opt_loadpath := s :: !opt_loadpath),
@@ -275,6 +278,7 @@ let () = try
   if !opt_list_provers then begin
     opt_list := true;
     let config = read_config !opt_config in
+    let config = List.fold_left merge_config config !opt_extra in
     let print fmt s prover = fprintf fmt "%s (%s)@\n" s prover.name in
     let print fmt m = Mstr.iter (print fmt) m in
     let provers = get_provers config in