Merge branch 'realization'

Makefile.in

@@ -106,8 +106,7 @@ plugins: plugins.@OCAMLBEST@
 LIBGENERATED = src/util/rc.ml src/parser/lexer.ml \
 	       src/parser/parser.mli src/parser/parser.ml \
 	       src/driver/driver_parser.mli src/driver/driver_parser.ml \
-	       src/driver/driver_lexer.ml src/coq_config.ml \
-               src/session/xml.ml
+	       src/driver/driver_lexer.ml src/session/xml.ml
 
 LIB_UTIL = stdlib exn_printer pp debug loc print_tree print_number \
 	   cmdline hashweak hashcons util sysutil rc plugin
@@ -136,7 +135,7 @@ LIB_PRINTER = alt_ergo why3printer smtv1 smtv2 coq pvs simplify gappa \
 
 LIB_SESSION = xml termcode session session_tools session_scheduler
 
-LIBMODULES = src/config src/coq_config \
+LIBMODULES = src/config \
 	      $(addprefix src/util/, $(LIB_UTIL)) \
 	      $(addprefix src/core/, $(LIB_CORE)) \
 	      $(addprefix src/parser/, $(LIB_PARSER)) \
@@ -942,16 +941,15 @@ COQVO = $(addsuffix .vo, $(COQLIBS_FILES))
 %.vo: %.v
 	$(COQC) -R lib/coq Why3 $<
 
-src/coq_config.ml:
-	echo "let realized_theories = [" > $@
-	for f in $(COQLIBS_INT_FILES); do echo '  ["int"; "'"$$f"'"];'; done >> $@
-	for f in $(COQLIBS_REAL_FILES); do echo '  ["real"; "'"$$f"'"];'; done >> $@
+drivers/coq-realizations.aux:
+	echo "(* generated automatically at compilation time *)" > $@
+	for f in $(COQLIBS_INT_FILES); do echo 'theory int.'"$$f"' meta "realized" "int.'"$$f"'", "" end'; done >> $@
+	for f in $(COQLIBS_REAL_FILES); do echo 'theory real.'"$$f"' meta "realized" "real.'"$$f"'", "" end'; done >> $@
 ifeq (@enable_coq_fp_libs@,yes)
-	for f in $(COQLIBS_FP_FILES); do echo '  ["floating_point"; "'"$$f"'"];'; done >> $@
+	for f in $(COQLIBS_FP_FILES); do echo 'theory floating_point.'"$$f"' meta "realized" "floating_point.'"$$f"'", "" end'; done >> $@
 endif
-	echo "]" >> $@
 
-all: $(COQVO)
+opt byte: $(COQVO)
 
 install_no_local::
 	mkdir -p $(LIBDIR)/why3/coq
@@ -963,8 +961,9 @@ ifeq (@enable_coq_fp_libs@,yes)
 	mkdir -p $(LIBDIR)/why3/coq/floating_point
 	cp $(addsuffix .vo, $(COQLIBS_FP)) $(LIBDIR)/why3/coq/floating_point/
 endif
+	cp drivers/coq-realizations.aux $(DATADIR)/why3/drivers/
 
-install_local: $(COQVO)
+install_local: $(COQVO) drivers/coq-realizations.aux
 
 ifneq "$(MAKECMDGOALS)" "clean"
 include .depend.coq-libs
@@ -981,11 +980,16 @@ clean::
 
 else
 
-src/coq_config.ml:
-	echo "let realized_theories = []" > $@
+drivers/coq-realizations.aux:
+	echo "(* generated automatically at compilation time *)" > $@
 
 endif
 
+opt byte: drivers/coq-realizations.aux
+
+clean::
+	rm -f drivers/coq-realizations.aux
+
 #######
 # tools
 #######

drivers/coq-common.gen

@@ -285,3 +285,6 @@ theory real.Trigonometry
   remove prop Sin_pi2
 
 end
+
+(* this file has an extension .aux rather than .gen since it should not be distributed *)
+import "coq-realizations.aux"

examples/use_api.ml

@@ -103,7 +103,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
+    Driver.load_driver env alt_ergo.Whyconf.driver []
   with e ->
     eprintf "Failed to load driver for alt-ergo: %a@."
       Exn_printer.exn_printer e;

src/bench/benchdb.ml

@@ -53,10 +53,11 @@ 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 = Whyconf.prover_by_id whyconf prover_name in
-          p.Whyconf.driver ,p.Whyconf.command
+          p.Whyconf.driver, p.Whyconf.extra_drivers,
+          String.concat " " (p.Whyconf.command :: p.Whyconf.extra_options)
         with
       (* TODO add exceptions pehaps inside rc.ml in fact*)
           | Not_found ->
@@ -84,7 +85,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,8 @@ let read_tools absf wc map (name,section) =
   let provers = get_stringl ~default:[] section "prover" in
   let find_provers s =
     try let p = prover_by_id wc s in
-        s,p.driver ,p.command
+        s, p.driver, p.extra_drivers,
+        String.concat " " (p.command :: p.extra_options)
     with
       (* TODO add exceptions pehaps inside rc.ml in fact*)
       | Not_found -> eprintf "Prover %s not found.@." s; exit 1 in
@@ -85,9 +86,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 = {Bench.tool_name = name; prover_name = n; tool_db =

src/bench/whybench.ml

@@ -337,7 +337,7 @@ let () =
     let prover = prover_by_id config s 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/coq-plugin/whytac.ml

@@ -894,7 +894,7 @@ let whytac s gl =
   try
     tr_goal gl;
     let cp, drv = get_prover s in
-    let command = cp.command in
+    let command = String.concat " " (cp.command :: cp.extra_options) in
     if debug then Format.printf "@[%a@]@\n---@." Pretty.print_task !task;
     if debug then Format.printf "@[%a@]@\n---@." (Driver.print_task drv) !task;
     let res = Driver.prove_task ~command ~timelimit drv !task () () in

src/core/printer.ml

@@ -171,6 +171,7 @@ exception KnownLogicSyntax of lsymbol
 let meta_syntax_type  = register_meta "syntax_type" [MTtysymbol; MTstring]
 let meta_syntax_logic = register_meta "syntax_logic" [MTlsymbol; MTstring]
 let meta_remove_prop  = register_meta "remove_prop" [MTprsymbol]
+let meta_realized     = register_meta "realized" [MTstring; MTstring]
 
 let syntax_type ts s =
   check_syntax s (List.length ts.ts_args);

src/core/printer.mli

@@ -48,6 +48,7 @@ val print_prelude_for_theory : theory -> prelude_map pp
 val meta_syntax_type : meta
 val meta_syntax_logic : meta
 val meta_remove_prop : meta
+val meta_realized : meta
 
 val syntax_type : tysymbol -> string -> tdecl
 val syntax_logic : lsymbol -> string -> tdecl

src/driver/autodetection.ml

@@ -163,7 +163,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/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
@@ -181,6 +181,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/driver/whyconf.ml

@@ -102,6 +102,8 @@ type config_prover = {
   driver  : string;
   editor  : string;
   interactive : bool;
+  extra_options : string list;
+  extra_drivers : string list;
 }
 
 type main = {
@@ -237,6 +239,8 @@ let load_prover dirname provers (id,section) =
       driver  = absolute_filename dirname (get_string section "driver");
       editor  = get_string ~default:"" section "editor";
       interactive = get_bool ~default:false section "interactive";
+      extra_options = [];
+      extra_drivers = [];
     } provers
 
 let load_main dirname section =
@@ -306,6 +310,30 @@ 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) ->
+      try
+        let key,c = Mprover.choose (Mprover.filter (fun _ p -> p.id = id) provers) in
+        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
+        Mprover.add key { c with extra_options = opt ; extra_drivers = drv } provers
+      with
+        Not_found -> load_prover dirname provers (id, section)
+    ) 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 *)
 
@@ -107,10 +110,12 @@ type config_prover = {
   driver  : string;   (* "/usr/local/share/why/drivers/ergo-spec.drv" *)
   editor  : string;   (* Dedicated editor *)
   interactive : bool; (* Interative theorem prover *)
+  extra_options : string list;
+  extra_drivers : string list;
 }
 
 val get_provers : config  -> config_prover Mprover.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 Mprover.t -> config

src/ide/gconfig.ml

@@ -55,6 +55,7 @@ type t =
       (** colors *)
       mutable env : Env.env;
       mutable config : Whyconf.config;
+      original_config : Whyconf.config;
       mutable altern_provers : altern_provers;
       mutable replace_prover : conf_replace_prover;
     }
@@ -169,7 +170,7 @@ let load_altern alterns (_,section) =
         } in
   Mprover.add unknown known alterns
 
-let load_config config =
+let load_config config original_config =
   let main = get_main config in
   let ide  = match get_section config "ide" with
     | None -> default_ide
@@ -199,6 +200,7 @@ let load_config config =
     max_running_processes = Whyconf.running_provers_max main;
     default_editor = ide.ide_default_editor;
     config         = config;
+    original_config = original_config;
     env            = env;
     altern_provers = alterns;
     replace_prover = ide.ide_replace_prover;
@@ -219,7 +221,7 @@ let save_altern unknown known (id,family) =
   (id+1,(sprintf "alt%i" id,alt)::family)
 
 let save_config t =
-  let config = t.config in
+  let config = t.original_config in
   let config = set_main config
     (set_limits (get_main config)
        t.time_limit t.mem_limit t.max_running_processes)
@@ -252,10 +254,11 @@ 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
-    load_config config
+    let merged_config = List.fold_left Whyconf.merge_config config extra_files in
+    load_config merged_config config
   with e when not (Debug.test_flag Debug.stack_trace) ->
     eprintf "@.%a@." Exn_printer.exn_printer e;
     exit 1
@@ -266,9 +269,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)
 
@@ -774,7 +777,7 @@ let replace_prover c to_be_removed to_be_copied =
   dialog#destroy ();
   res
 
-  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

@@ -45,11 +45,12 @@ type t =
       mutable error_color : string;
       mutable env : Why3.Env.env;
       mutable config : Whyconf.config;
+      original_config : Whyconf.config;
       mutable altern_provers : prover option Mprover.t;
       mutable replace_prover : conf_replace_prover;
     }
 
-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

@@ -43,6 +43,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",
@@ -58,6 +59,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),
@@ -92,7 +95,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/ide/replay.ml

@@ -51,10 +51,25 @@ let set_opt_smoke = function
   | "deep" ->  opt_smoke := SD_Deep
   | _ -> assert false
 
+let opt_config = ref None
+let opt_extra = ref []
+
 let spec = Arg.align [
-  ("-I",
+  ("-L",
    Arg.String (fun s -> includes := s :: !includes),
    "<s> add s to loadpath") ;
+  ("--library",
+   Arg.String (fun s -> includes := s :: !includes),
+   " same as -L") ;
+  ("-I",
+   Arg.String (fun s -> includes := s :: !includes),
+   " same as -L (obsolete)") ;
+  ("-C", Arg.String (fun s -> opt_config := Some s),
+   "<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>") ;
   ("-force",
    Arg.Set opt_force,
    " enforce saving of session even if replay failed") ;
@@ -122,7 +137,8 @@ let fname = match !file with
   | Some f ->
       f
 
-let config = Whyconf.read_config None
+let config = Whyconf.read_config !opt_config
+let config = List.fold_left Whyconf.merge_config config !opt_extra
 
 let loadpath = (Whyconf.loadpath (Whyconf.get_main config))
   @ List.rev !includes

src/main.ml

@@ -87,6 +87,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 []
@@ -130,6 +131,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),
@@ -160,9 +163,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>";
@@ -256,6 +259,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 prover pc = fprintf fmt "%s (%a)@\n"
       pc.id print_prover prover in
     let print fmt m = Mprover.iter (print fmt) m in
@@ -319,9 +323,9 @@ let () = try
   if !opt_memlimit  = None then opt_memlimit  := Some (Whyconf.memlimit main);
   begin match !opt_prover with
   | Some s ->
-    let prover = Whyconf.prover_by_id config s in
-    opt_command := Some prover.command;
-    opt_driver := Some prover.driver
+      let prover = Whyconf.prover_by_id config s in
+      opt_command := Some (String.concat " " (prover.command :: prover.extra_options));
+      opt_driver := Some (prover.driver, prover.extra_drivers)
   | None ->
       ()
   end;
@@ -534,7 +538,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@."

src/printer/coq.ml

@@ -32,10 +32,12 @@ let black_list =
   [ "at"; "cofix"; "exists2"; "fix"; "IF"; "left"; "mod"; "Prop";
     "return"; "right"; "Set"; "Type"; "using"; "where"; ]
 
-let iprinter =
+let fresh_printer () =
   let isanitize = sanitizer char_to_alpha char_to_alnumus in
   create_ident_printer black_list ~sanitizer:isanitize
 
+let iprinter = fresh_printer ()
+
 let forget_all () = forget_all iprinter
 
 let tv_set = ref Sid.empty
@@ -102,7 +104,7 @@ let print_pr fmt pr =
 
 type info = {
   info_syn : syntax_map;
-  symbol_printers : (Theory.theory * ident_printer) Mid.t;
+  symbol_printers : (string * ident_printer) Mid.t;
   realization : bool;
 }
 
@@ -111,12 +113,10 @@ let print_path = print_list (constant_string ".") string
 let print_id fmt id = string fmt (id_unique iprinter id)
 
 let print_id_real info fmt id =
-        try let th,ipr = Mid.find id info.symbol_printers in
-        fprintf fmt "%a.%s.%s"
-          print_path th.Theory.th_path
-          th.Theory.th_name.id_string
-          (id_unique ipr id)
-        with Not_found -> print_id fmt id
+  try
+    let path,ipr = Mid.find id info.symbol_printers in
+    fprintf fmt "%s.%s" path (id_unique ipr id)
+  with Not_found -> print_id fmt id
 
 let print_ls_real info fmt ls = print_id_real info fmt ls.ls_name
 let print_ts_real info fmt ts = print_id_real info fmt ts.ts_name
@@ -679,53 +679,45 @@ let print_decl ~old info fmt d = match d.d_node with
 let print_decls ~old info fmt dl =
   fprintf fmt "@[<hov>%a@\n@]" (print_list nothing (print_decl ~old info)) dl
 
-let init_printer th =
-  let isanitize = sanitizer char_to_alpha char_to_alnumus in
-  let pr = create_ident_printer black_list ~sanitizer:isanitize in
-  Sid.iter (fun id -> ignore (id_unique pr id)) th.Theory.th_local;
-  pr
-
-(* TODO: add a driver meta and make lookup for realized theories a bit
-   more efficient *)
-let realized_theories = Coq_config.realized_theories
-
-let print_task _env pr thpr realize ?old fmt task =
+let print_task env pr thpr realize ?old fmt task =
   forget_all ();
   print_prelude fmt pr;
   print_th_prelude task fmt thpr;
-  let symbol_printers,decls =
-      let used = Task.used_theories task in
-      let used = Mid.filter (fun _ th -> List.mem (th.Theory.th_path@[th.Theory.th_name.id_string]) realized_theories) used in
-      (* 2 cases: goal is clone T with [] or goal is a real goal *)
-      let used = match task with
-        | None -> assert false
-        | Some { Task.task_decl = { Theory.td_node = Theory.Clone (th,_) }} ->
-            Sid.iter
-              (fun id -> ignore (id_unique iprinter id))
-              th.Theory.th_local;
-            Mid.remove th.Theory.th_name used
-        | _ -> used
-      in
-      (*
-      (* output the Require commands *)
-      List.iter
-        (fprintf fmt "Add Rec LoadPath \"%s\".@\n")
-        (Env.get_loadpath env);
-      *)
-      Mid.iter
-        (fun id th -> fprintf fmt "Require %a.%s.@\n"
-          print_path th.Theory.th_path id.id_string)
-        used;
-      let symbols = Task.used_symbols used in
-      (* build the printers for each theories *)
-      let printers = Mid.map init_printer used in
-      let decls = Task.local_decls task symbols in
-      let symbols =
-        Mid.map (fun th -> (th,Mid.find th.Theory.th_name printers))
-          symbols
-      in
-      symbols, decls
-  in
+  (* find theories that are both used and realized from metas *)
+  let realized_theories =
+    Task.on_meta meta_realized (fun mid args ->
+      match args with
+      | [Theory.MAstr s1; Theory.MAstr s2] ->
+        (* TODO: do not split string; in fact, do not even use a string argument *)
+        let f,id = let l = split_string_rev s1 '.' in List.rev (List.tl l),List.hd l in
+        let th = Env.find_theory env f id in
+        Mid.add th.Theory.th_name (th, if s2 = "" then s1 else s2) mid
+      | _ -> assert false
+    ) Mid.empty task in
+  (* 2 cases: goal is clone T with [] or goal is a real goal *)
+  let realized_theories =
+    match task with
+    | None -> assert false
+    | Some { Task.task_decl = { Theory.td_node = Theory.Clone (th,_) }} ->
+      Sid.iter (fun id -> ignore (id_unique iprinter id)) th.Theory.th_local;
+      Mid.remove th.Theory.th_name realized_theories
+    | _ -> realized_theories in
+  let realized_theories' =
+    Mid.map (fun (th,s) -> fprintf fmt "Require %s.@\n" s; th) realized_theories in
+  let realized_symbols = Task.used_symbols realized_theories' in
+  let local_decls = Task.local_decls task realized_symbols in
+  (* associate a special printer to each symbol in a realized theory *)
+  let symbol_printers =
+    let printers =
+      Mid.map (fun th ->
+        let pr = fresh_printer () in
+        Sid.iter (fun id -> ignore (id_unique pr id)) th.Theory.th_local;
+        pr
+      ) realized_theories' in
+    Mid.map (fun th ->
+      (snd (Mid.find th.Theory.th_name realized_theories),
+       Mid.find th.Theory.th_name printers)
+    ) realized_symbols in
   let info = {
     info_syn = get_syntax_map task;
     symbol_printers = symbol_printers;
@@ -736,7 +728,7 @@ let print_task _env pr thpr realize ?old fmt task =
     | None -> None
     | Some ch -> Some(ref NoWhere,ch)
   in
-  print_decls ~old info fmt decls
+  print_decls ~old info fmt local_decls
 
 let print_task_full env pr thpr ?old fmt task =
   print_task env pr thpr false ?old fmt task

src/printer/pvs.ml

@@ -781,7 +781,7 @@ let init_printer th =
 
 (* TODO: add a driver meta and make lookup for realized theories a bit
    more efficient *)
-let realized_theories = Coq_config.realized_theories
+let realized_theories = []
 
 let print_task _env pr thpr realize ?old fmt task =
   forget_all ();

src/session/session.ml

@@ -1109,7 +1109,7 @@ let load_prover eS prover =
     let r = match r with
       | None -> None
       | Some pr ->
-        let dr = Driver.load_driver eS.env pr.Whyconf.driver in
+        let dr = Driver.load_driver eS.env pr.Whyconf.driver pr.Whyconf.extra_drivers in
         Some { prover_config = pr;
                prover_driver = dr}
     in

src/session/session_scheduler.ml

@@ -397,7 +397,7 @@ loaded@."
           set_timelimit timelimit a;
           schedule_proof_attempt
             ~timelimit ~memlimit:0
-            ?old ~command:npc.prover_config.Whyconf.command
+            ?old ~command:(String.concat " " (npc.prover_config.Whyconf.command :: npc.prover_config.Whyconf.extra_options))
             ~driver:npc.prover_driver
             ~callback
             eT
@@ -629,7 +629,7 @@ let check_external_proof eS eT todo a =
           in
           schedule_proof_attempt eT
             ~timelimit:a.proof_timelimit ~memlimit:0
-            ?old ~command:npc.prover_config.Whyconf.command
+            ?old ~command:(String.concat " " (npc.prover_config.Whyconf.command :: npc.prover_config.Whyconf.extra_options))
             ~driver:npc.prover_driver
             ~callback
             (goal_task g)
@@ -755,7 +755,7 @@ let edit_proof eS sched ~default_editor a =
           let editor =
             match npc.prover_config.Whyconf.editor with
               | "" -> default_editor
-              | s -> s
+              | s -> String.concat " " (s :: npc.prover_config.Whyconf.extra_options)
           in
           (*