diff options
| -rw-r--r-- | toplevel/coqtop.ml | 16 | ||||
| -rw-r--r-- | toplevel/mltop.ml4 | 54 | ||||
| -rw-r--r-- | toplevel/mltop.mli | 5 |
3 files changed, 39 insertions, 36 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index fa8fca66f..dd92ccfc2 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -79,20 +79,6 @@ let set_include d p = let set_rec_include d p = let p = dirpath_of_string p in check_coq_overwriting p; push_rec_include(d,p) -let load_initial_plugins () = - (** Order matters ! For instance ground_plugin needs cc_plugin *) - let initial_plugins = - [ "extraction_plugin"; - "jprover_plugin"; - "cc_plugin"; - "ground_plugin"; - "dp_plugin"; - "recdef_plugin"; - (*"subtac_plugin";*) - "xml_plugin"; - ] in - if Mltop.has_dynlink then Mltop.declare_ml_modules initial_plugins - let load_vernacular_list = ref ([] : (string * bool) list) let add_load_vernacular verb s = load_vernacular_list := ((make_suffix s ".v"),verb) :: !load_vernacular_list @@ -354,7 +340,7 @@ let init is_ide = if (not !batch_mode|| !compile_list=[]) && Global.env_is_empty() then Option.iter Declaremods.start_library !toplevel_name; init_library_roots (); - load_initial_plugins (); + Mltop.load_initial_plugins (); load_vernac_obj (); require (); load_rcfile(); diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index 611567af9..dcdc46e8e 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -215,21 +215,37 @@ let file_of_name name = if is_in_path !coq_mlpath_copy name then name else fail (base ^ ".cm[oa]") -(* TODO: supprimer ce hack, si possible *) -(* Initialisation of ML modules that need the state (ex: tactics like - * natural, omega ...) - * Each module may add some inits (function of type unit -> unit). - * These inits are executed right after the initial state loading if the - * module is statically linked, or after the loading if it is required. *) - -let init_list = ref ([] : (unit -> unit) list) - -let add_init_with_state init_fun = - init_list := init_fun :: !init_list - -let init_with_state () = - List.iter (fun f -> f()) (List.rev !init_list); init_list := [] - +(** Is the ML code of the standard library placed into loadable plugins + or statically compiled into coqtop ? For the moment this choice is + made according to the presence of native dynlink : even if bytecode + coqtop could always load plugins, we prefer to have uniformity between + bytecode and native versions. *) + +let stdlib_use_plugins = Coq_config.has_natdynlink + +(** List of plugins we want to dynamically load at launch-time. + Order matters, for instance ground_plugin needs cc_plugins. *) + +let initial_plugins = + [ "Extraction_plugin"; "Jprover_plugin"; "Cc_plugin"; + "Ground_plugin"; "Dp_plugin"; "Recdef_plugin"; (*"subtac_plugin";*) + "Xml_plugin"; ] + +(** Other plugins of the standard library. We need their list + to avoid trying to load them if they have been statically compiled + into coqtop. Otherwise, they will be loaded automatically when + doing the corresponding Require. *) + +let other_stdlib_plugins = + [ "Omega_plugin"; "Romega_plugin"; "Micromega_plugin"; "Quote_plugin"; + "Ring_plugin"; "Newring_plugin"; "Field_plugin"; "Fourier_plugin"; + "Rtauto_plugin" ] + +let initially_known_modules = + if stdlib_use_plugins then Stringset.empty + else + let all_plugins = initial_plugins @ other_stdlib_plugins in + List.fold_right Stringset.add all_plugins Stringset.empty (* [known_loaded_module] contains the names of the loaded ML modules * (linked or loaded with load_object). It is used not to load a @@ -237,7 +253,7 @@ let init_with_state () = type ml_module_object = { mnames : string list } -let known_loaded_modules = ref Stringset.empty +let known_loaded_modules = ref initially_known_modules let add_known_module mname = known_loaded_modules := Stringset.add mname !known_loaded_modules @@ -246,7 +262,6 @@ let module_is_known mname = Stringset.mem mname !known_loaded_modules let load_object mname fname= dir_ml_load fname; - init_with_state(); add_known_module mname (* Summary of declared ML Modules *) @@ -317,7 +332,10 @@ let (inMLModule,outMLModule) = let declare_ml_modules l = Lib.add_anonymous_leaf (inMLModule {mnames=l}) - + +let load_initial_plugins () = + if stdlib_use_plugins then declare_ml_modules initial_plugins + let print_ml_path () = let l = !coq_mlpath_copy in ppnl (str"ML Load Path:" ++ fnl () ++ str" " ++ diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli index 15fdbe4c5..af638241c 100644 --- a/toplevel/mltop.mli +++ b/toplevel/mltop.mli @@ -48,9 +48,6 @@ val add_rec_ml_dir : string -> unit val add_path : unix_path:string -> coq_root:Names.dir_path -> unit val add_rec_path : unix_path:string -> coq_root:Names.dir_path -> unit -val add_init_with_state : (unit -> unit) -> unit -val init_with_state : unit -> unit - (* List of modules linked to the toplevel *) val add_known_module : string -> unit val module_is_known : string -> bool @@ -67,6 +64,8 @@ val inMLModule : ml_module_object -> Libobject.obj val outMLModule : Libobject.obj -> ml_module_object val declare_ml_modules : string list -> unit +val load_initial_plugins : unit -> unit + val print_ml_path : unit -> unit val print_ml_modules : unit -> unit |