From 3b4b50789e74e7d596199e4b18349a810ae18696 Mon Sep 17 00:00:00 2001 From: letouzey Date: Sat, 6 Oct 2012 11:45:34 +0000 Subject: Turn mltop.ml4 into a regular ocaml file The IFDEF's in mltop.ml4 were there to support platforms with a native ocaml compiler but no dynlink.cmxa, a situation that should be pretty rare in the Coq community nowadays (playing with coqtop on ARM, anyone ?). So we now refuse to build a native coqtop unless dynlink.cmxa exists (cf ./configure), and we explain how to create a dummy one if necessary (cf dev/dynlink.ml). This way, we can clean-up mltop.ml, and remove ugly special rules in Makefile and myocamlbuild NB: I checked that this shouldn't have any impact on Coq's debian packages on exotic architectures (arm, mips, ...), since apparently on these architectures no ocamlopt at all are shipped, and coq packages are already byte-only git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15879 85f007b7-540e-0410-9357-904b9bb8a0f7 --- .gitignore | 3 - Makefile.build | 21 ---- _tags | 2 - configure | 67 ++++++----- dev/dynlink.ml | 51 ++++++++ myocamlbuild.ml | 20 ---- toplevel/mltop.ml | 335 ++++++++++++++++++++++++++++++++++++++++++++++++++++ toplevel/mltop.ml4 | 337 ----------------------------------------------------- 8 files changed, 423 insertions(+), 413 deletions(-) create mode 100644 dev/dynlink.ml create mode 100644 toplevel/mltop.ml delete mode 100644 toplevel/mltop.ml4 diff --git a/.gitignore b/.gitignore index c3669497f8..2b497f9a91 100644 --- a/.gitignore +++ b/.gitignore @@ -136,15 +136,12 @@ tactics/eqdecide.ml tactics/extratactics.ml tactics/extraargs.ml tools/coq_tex.ml -toplevel/mltop.ml toplevel/whelp.ml ide/coqide_main.ml ide/coqide_main_opt.ml # other auto-generated files -toplevel/mltop.optml -toplevel/mltop.byteml kernel/byterun/coq_jumptbl.h kernel/copcodes.ml scripts/tolink.ml diff --git a/Makefile.build b/Makefile.build index f2fabf918e..6efdf95a4a 100644 --- a/Makefile.build +++ b/Makefile.build @@ -742,27 +742,6 @@ grammar/grammar.cma: | grammar/grammar.mllib.d $(SHOW)'OCAMLC -a $@' $(HIDE)$(OCAMLC) $(BYTEFLAGS) $^ -linkall -a -o $@ -# toplevel/mltop.ml4 (ifdef Byte) - -## NB: mltop.ml correspond to the byte version (and hence need no special rules) -## while the opt version is in mltop.optml. Since mltop.optml uses mltop.ml.d -## as dependency file, be sure to import the same modules in the different sections -## of the ml4 - -MLTOP:=toplevel/mltop - -$(MLTOP).cmx: $(MLTOP).optml | $(MLTOP).ml.d $(MLTOP).ml4.d - $(SHOW)'OCAMLOPT $<' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -c -impl $< -o $@ - -$(MLTOP).ml: $(MLTOP).ml4 config/Makefile # no camlp4deps here - $(SHOW)'CAMLP4O $<' - $(HIDE)$(CAMLP4O) $(PR_O) $(CAMLP4USE) -DByte -DHasDynlink -impl $< -o $@ - -$(MLTOP).optml: $(MLTOP).ml4 config/Makefile # no camlp4deps here - $(SHOW)'CAMLP4O $<' - $(HIDE)$(CAMLP4O) $(PR_O) $(CAMLP4USE) $(NATDYNLINKDEF) -impl $< -o $@ - ide/coqide_main.ml: ide/coqide_main.ml4 $(SHOW)'CAMLP4O $<' $(HIDE)$(CAMLP4O) $(PR_O) $(CAMLP4USE) -impl $< -o $@ diff --git a/_tags b/_tags index 3097447c32..b50dbfed21 100644 --- a/_tags +++ b/_tags @@ -28,8 +28,6 @@ ## tags for camlp4 files -"toplevel/mltop.ml4": is_mltop - "toplevel/whelp.ml4": use_grammar "parsing/g_constr.ml4": use_compat5 diff --git a/configure b/configure index f4b5b7e2ff..1795156f15 100755 --- a/configure +++ b/configure @@ -465,36 +465,6 @@ if [ "$coq_debug_flag" = "-g" ]; then esac fi -# Native dynlink -if [ "$natdynlink" = "yes" -a -f "$CAMLLIB"/dynlink.cmxa ]; then - HASNATDYNLINK=true -else - HASNATDYNLINK=false -fi - -case $HASNATDYNLINK,$ARCH,`uname -r`,$CAMLVERSION in - true,Darwin,9.*,3.11.*) # ocaml 3.11.0 dynlink on MacOS 10.5 is buggy - NATDYNLINKFLAG=os5fixme;; - #Possibly a problem on 10.6.0/10.6.1/10.6.2 - #May just be a 32 vs 64 problem for all 10.6.* - true,Darwin,10.0.*,3.11.*) # Possibly a problem on 10.6.0 - NATDYNLINKFLAG=os5fixme;; - true,Darwin,10.1.*,3.11.*) # Possibly a problem on 10.6.1 - NATDYNLINKFLAG=os5fixme;; - true,Darwin,10.2.*,3.11.*) # Possibly a problem on 10.6.2 - NATDYNLINKFLAG=os5fixme;; - true,Darwin,10.*,3.11.*) - if [ `getconf LONG_BIT` = "32" ]; then - # Still a problem for x86_32 - NATDYNLINKFLAG=os5fixme - else - # Not a problem for x86_64 - NATDYNLINKFLAG=$HASNATDYNLINK - fi;; - *) - NATDYNLINKFLAG=$HASNATDYNLINK;; -esac - # Camlp4 / Camlp5 configuration # Assume that camlp(4|5) binaries are at the same place as ocaml ones @@ -572,6 +542,13 @@ if [ "$best_compiler" = "opt" ] ; then best_compiler=byte echo "Cannot find native-code $CAMLP4," echo "only the bytecode version of Coq will be available." + elif [ ! -f "$CAMLLIB"/dynlink.cmxa ]; then + best_compiler=byte + echo "Cannot find native-code dynlink library," + echo "only the bytecode version of Coq will be available." + echo "For building a native-code Coq, you may try to first" + echo "compile and install a dummy dynlink.cmxa (see dev/dynlink.ml)" + echo "and then run ./configure -natdynlink no" else if [ "$CAMLOPTVERSION" != "$CAMLVERSION" ] ; then echo "Native and bytecode compilers do not have the same version!" @@ -584,6 +561,36 @@ if [ "$best_compiler" = "opt" ] ; then fi fi +# Native dynlink +if [ "$natdynlink" = "yes" -a -f "$CAMLLIB"/dynlink.cmxa ]; then + HASNATDYNLINK=true +else + HASNATDYNLINK=false +fi + +case $HASNATDYNLINK,$ARCH,`uname -r`,$CAMLVERSION in + true,Darwin,9.*,3.11.*) # ocaml 3.11.0 dynlink on MacOS 10.5 is buggy + NATDYNLINKFLAG=os5fixme;; + #Possibly a problem on 10.6.0/10.6.1/10.6.2 + #May just be a 32 vs 64 problem for all 10.6.* + true,Darwin,10.0.*,3.11.*) # Possibly a problem on 10.6.0 + NATDYNLINKFLAG=os5fixme;; + true,Darwin,10.1.*,3.11.*) # Possibly a problem on 10.6.1 + NATDYNLINKFLAG=os5fixme;; + true,Darwin,10.2.*,3.11.*) # Possibly a problem on 10.6.2 + NATDYNLINKFLAG=os5fixme;; + true,Darwin,10.*,3.11.*) + if [ `getconf LONG_BIT` = "32" ]; then + # Still a problem for x86_32 + NATDYNLINKFLAG=os5fixme + else + # Not a problem for x86_64 + NATDYNLINKFLAG=$HASNATDYNLINK + fi;; + *) + NATDYNLINKFLAG=$HASNATDYNLINK;; +esac + # OS dependent libraries OSDEPLIBS="-cclib -lunix" diff --git a/dev/dynlink.ml b/dev/dynlink.ml new file mode 100644 index 0000000000..810e0ffcae --- /dev/null +++ b/dev/dynlink.ml @@ -0,0 +1,51 @@ + +(** Some architectures may have a native ocaml compiler but no native + dynlink.cmxa (e.g. ARM). If you still want to build a native coqtop + there, you'll need this dummy implementation of Dynlink. + Compile it and install with: + + ocamlopt -a -o dynlink.cmxa dynlink.ml + sudo cp -i dynlink.cmxa `ocamlopt -where` + + Then build coq this way: ./configure -natdynlink no && make world +*) + +let is_native = true (* This file will only be given to the native compiler *) + +type linking_error = +| Undefined_global of string +| Unavailable_primitive of string +| Uninitialized_global of string + +type error = +| Not_a_bytecode_file of string +| Inconsistent_import of string +| Unavailable_unit of string +| Unsafe_file +| Linking_error of string * linking_error +| Corrupted_interface of string +| File_not_found of string +| Cannot_open_dll of string +| Inconsistent_implementation of string + +exception Error of error + +let error_message = function + | Not_a_bytecode_file s -> "Native dynamic link not supported (module "^s^")" + | _ -> "Native dynamic link not supported" + +let loadfile : string -> unit = fun s -> raise (Error (Not_a_bytecode_file s)) +let loadfile_private = loadfile + +let adapt_filename s = s + +let init () = () +let allow_only : string list -> unit = fun _ -> () +let prohibit : string list -> unit = fun _ -> () +let default_available_units : unit -> unit = fun _ -> () +let allow_unsafe_modules : bool -> unit = fun _ -> () +let add_interfaces : string list -> string list -> unit = fun _ _ -> () +let add_available_units : (string * Digest.t) list -> unit = fun _ -> () +let clear_available_units : unit -> unit = fun _ -> () +let digest_interface : string -> string list -> Digest.t = + fun _ _ -> failwith "digest_interface" diff --git a/myocamlbuild.ml b/myocamlbuild.ml index 0ed2053509..793522f847 100644 --- a/myocamlbuild.ml +++ b/myocamlbuild.ml @@ -299,26 +299,6 @@ let extra_rules () = begin mlp_cmo "tools/compat5b"; end; -(** Special case of toplevel/mltop.ml4: - - mltop.ml will be the old mltop.optml and be used to obtain mltop.cmx - - we add a special mltop.ml4 --> mltop.cmo rule, before all the others -*) - flag ["is_mltop"; "p4option"] flag_dynlink; - -(*TODO: this is rather ugly for a simple file, we should try to - benefit more from predefined rules *) - let mltop = "toplevel/mltop" in - let ml4 = mltop^".ml4" and mlo = mltop^".cmo" and - ml = mltop^".ml" and mld = mltop^".ml.depends" - in - rule "mltop_byte" ~deps:[ml4;mld] ~prod:mlo ~insert:`top - (fun env build -> - Ocaml_compiler.prepare_compile build ml; - Cmd (S [!Options.ocamlc; A"-c"; A"-pp"; - Quote (S [camlp4o; T(tags_of_pathname ml4 ++ "p4mod"); - A"-DByte";A"-DHasDynlink";camlp4compat;A"-impl"]); - camlp4incl; incl ml4; A"-impl"; P ml4])); - (** All caml files are compiled with +camlp4/5 and ide files need +lablgtk2 *) diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml new file mode 100644 index 0000000000..2ca3a4cd7a --- /dev/null +++ b/toplevel/mltop.ml @@ -0,0 +1,335 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* canonical_path_name path') in + coq_mlpath_copy := path :: List.filter filter !coq_mlpath_copy + +(* If there is a toplevel under Coq *) +type toplevel = { + load_obj : string -> unit; + use_file : string -> unit; + add_dir : string -> unit; + ml_loop : unit -> unit } + +(* Determines the behaviour of Coq with respect to ML files (compiled + or not) *) +type kind_load = + | WithTop of toplevel + | WithoutTop + +(* Must be always initialized *) +let load = ref WithoutTop + +(* Are we in a native version of Coq? *) +let is_native = Dynlink.is_native + +(* Sets and initializes a toplevel (if any) *) +let set_top toplevel = load := WithTop toplevel + +(* Removes the toplevel (if any) *) +let remove ()= load := WithoutTop + +(* Tests if an Ocaml toplevel runs under Coq *) +let is_ocaml_top () = + match !load with + | WithTop _ -> true + |_ -> false + +(* Tests if we can load ML files *) +let has_dynlink = Coq_config.has_natdynlink || not is_native + +(* Runs the toplevel loop of Ocaml *) +let ocaml_toploop () = + match !load with + | WithTop t -> Printexc.catch t.ml_loop () + | _ -> () + +(* Dynamic loading of .cmo/.cma *) +let dir_ml_load s = + match !load with + | WithTop t -> + (try t.load_obj s + with + | (UserError _ | Failure _ | Anomaly _ | Not_found as u) -> raise u + | _ -> errorlabstrm "Mltop.load_object" (str"Cannot link ml-object " ++ + str s ++ str" to Coq code.")) + | WithoutTop -> + let warn = Flags.is_verbose() in + let _,gname = find_file_in_path ~warn !coq_mlpath_copy s in + try + Dynlink.loadfile gname; + with Dynlink.Error a -> + errorlabstrm "Mltop.load_object" (str (Dynlink.error_message a)) + +(* Dynamic interpretation of .ml *) +let dir_ml_use s = + match !load with + | WithTop t -> t.use_file s + | _ -> msg_warning (str "Cannot access the ML compiler") + +(* Adds a path to the ML paths *) +let add_ml_dir s = + match !load with + | WithTop t -> t.add_dir s; keep_copy_mlpath s + | WithoutTop when has_dynlink -> keep_copy_mlpath s + | _ -> () + +(* For Rec Add ML Path *) +let add_rec_ml_dir unix_path = + List.iter (fun (lp,_) -> add_ml_dir lp) (all_subdirs ~unix_path) + +(* Adding files to Coq and ML loadpath *) + +let add_path ~unix_path:dir ~coq_root:coq_dirpath = + if exists_dir dir then + begin + add_ml_dir dir; + Library.add_load_path true (dir,coq_dirpath) + end + else + msg_warning (str ("Cannot open " ^ dir)) + +let convert_string d = + try Names.id_of_string d + with _ -> + if_warn msg_warning (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)")); + raise Exit + +let add_rec_path ~unix_path ~coq_root = + if exists_dir unix_path then + let dirs = all_subdirs ~unix_path in + let prefix = Names.repr_dirpath coq_root in + let convert_dirs (lp, cp) = + try + let path = List.map convert_string (List.rev cp) @ prefix in + Some (lp, Names.make_dirpath path) + with Exit -> None + in + let dirs = List.map_filter convert_dirs dirs in + List.iter (fun lpe -> add_ml_dir (fst lpe)) dirs; + add_ml_dir unix_path; + List.iter (Library.add_load_path false) dirs; + Library.add_load_path true (unix_path, coq_root) + else + msg_warning (str ("Cannot open " ^ unix_path)) + +(* convertit un nom quelconque en nom de fichier ou de module *) +let mod_of_name name = + let base = + if Filename.check_suffix name ".cmo" then + Filename.chop_suffix name ".cmo" + else + name + in + String.capitalize base + +let get_ml_object_suffix name = + if Filename.check_suffix name ".cmo" then + Some ".cmo" + else if Filename.check_suffix name ".cma" then + Some ".cma" + else if Filename.check_suffix name ".cmxs" then + Some ".cmxs" + else + None + +let file_of_name name = + let name = String.uncapitalize name in + let suffix = get_ml_object_suffix name in + let fail s = + errorlabstrm "Mltop.load_object" + (str"File not found on loadpath : " ++ str s) in + if is_native then + let name = match suffix with + | Some ((".cmo"|".cma") as suffix) -> + (Filename.chop_suffix name suffix) ^ ".cmxs" + | Some ".cmxs" -> name + | _ -> name ^ ".cmxs" + in + if is_in_path !coq_mlpath_copy name then name else fail name + else + let (full, base) = match suffix with + | Some ".cmo" | Some ".cma" -> true, name + | Some ".cmxs" -> false, Filename.chop_suffix name ".cmxs" + | _ -> false, name + in + if full then + if is_in_path !coq_mlpath_copy base then base else fail base + else + let name = base ^ ".cmo" in + if is_in_path !coq_mlpath_copy name then name else + let name = base ^ ".cma" in + if is_in_path !coq_mlpath_copy name then name else + fail (base ^ ".cm[oa]") + +(** 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. *) + +(* [known_loaded_module] contains the names of the loaded ML modules + * (linked or loaded with load_object). It is used not to load a + * module twice. It is NOT the list of ML modules Coq knows. *) + +let known_loaded_modules = ref Stringset.empty + +let add_known_module mname = + let mname = String.capitalize mname in + known_loaded_modules := Stringset.add mname !known_loaded_modules + +let module_is_known mname = + Stringset.mem (String.capitalize mname) !known_loaded_modules + +(** A plugin is just an ML module with an initialization function. *) + +let known_loaded_plugins = ref Stringmap.empty + +let add_known_plugin init name = + let name = String.capitalize name in + add_known_module name; + known_loaded_plugins := Stringmap.add name init !known_loaded_plugins + +let init_known_plugins () = + Stringmap.iter (fun _ f -> f()) !known_loaded_plugins + +(** ml object = ml module or plugin *) + +let init_ml_object mname = + try Stringmap.find mname !known_loaded_plugins () + with Not_found -> () + +let load_ml_object mname fname= + dir_ml_load fname; + add_known_module mname; + init_ml_object mname + +(* Summary of declared ML Modules *) + +(* List and not Stringset because order is important: most recent first. *) + +let loaded_modules = ref [] +let get_loaded_modules () = List.rev !loaded_modules +let add_loaded_module md = loaded_modules := md :: !loaded_modules +let reset_loaded_modules () = loaded_modules := [] + +let if_verbose_load verb f name fname = + if not verb then f name fname + else + let info = "[Loading ML file "^fname^" ..." in + try + f name fname; + msg_info (str (info^" done]")); + with e -> + msg_info (str (info^" failed]")); + raise e + +(** Load a module for the first time (i.e. dynlink it) + or simulate its reload (i.e. doing nothing except maybe + an initialization function). *) + +let cache_ml_object verb reinit name = + begin + if module_is_known name then + (if reinit then init_ml_object name) + else if not has_dynlink then + error ("Dynamic link not supported (module "^name^")") + else + if_verbose_load (verb && is_verbose ()) + load_ml_object name (file_of_name name) + end; + add_loaded_module name + +let unfreeze_ml_modules x = + reset_loaded_modules (); + List.iter (cache_ml_object false false) x + +let _ = + Summary.declare_summary "ML-MODULES" + { Summary.freeze_function = get_loaded_modules; + Summary.unfreeze_function = unfreeze_ml_modules; + Summary.init_function = reset_loaded_modules } + +(* Liboject entries of declared ML Modules *) + +type ml_module_object = { + mlocal : Vernacexpr.locality_flag; + mnames : string list +} + +let cache_ml_objects (_,{mnames=mnames}) = + List.iter (cache_ml_object true true) mnames + +let classify_ml_objects ({mlocal=mlocal} as o) = + if mlocal then Dispose else Substitute o + +let inMLModule : ml_module_object -> obj = + declare_object + {(default_object "ML-MODULE") with + load_function = (fun _ -> cache_ml_objects); + cache_function = cache_ml_objects; + subst_function = (fun (_,o) -> o); + classify_function = classify_ml_objects } + +let declare_ml_modules local l = + let l = List.map mod_of_name l in + Lib.add_anonymous_leaf (inMLModule {mlocal=local; mnames=l}) + +let print_ml_path () = + let l = !coq_mlpath_copy in + str"ML Load Path:" ++ fnl () ++ str" " ++ + hv 0 (prlist_with_sep fnl str l) + +(* Printing of loaded ML modules *) + +let print_ml_modules () = + let l = get_loaded_modules () in + str"Loaded ML Modules: " ++ pr_vertical_list str l diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 deleted file mode 100644 index 09dd2a67f0..0000000000 --- a/toplevel/mltop.ml4 +++ /dev/null @@ -1,337 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* canonical_path_name path') in - coq_mlpath_copy := path :: List.filter filter !coq_mlpath_copy - -(* If there is a toplevel under Coq *) -type toplevel = { - load_obj : string -> unit; - use_file : string -> unit; - add_dir : string -> unit; - ml_loop : unit -> unit } - -(* Determines the behaviour of Coq with respect to ML files (compiled - or not) *) -type kind_load = - | WithTop of toplevel - | WithoutTop - -(* Must be always initialized *) -let load = ref WithoutTop - -(* Are we in a native version of Coq? *) -let is_native = IFDEF Byte THEN false ELSE true END - -(* Sets and initializes a toplevel (if any) *) -let set_top toplevel = load := WithTop toplevel - -(* Removes the toplevel (if any) *) -let remove ()= load := WithoutTop - -(* Tests if an Ocaml toplevel runs under Coq *) -let is_ocaml_top () = - match !load with - | WithTop _ -> true - |_ -> false - -(* Tests if we can load ML files *) -let has_dynlink = IFDEF HasDynlink THEN true ELSE false END - -(* Runs the toplevel loop of Ocaml *) -let ocaml_toploop () = - match !load with - | WithTop t -> Printexc.catch t.ml_loop () - | _ -> () - -(* Dynamic loading of .cmo/.cma *) -let dir_ml_load s = - match !load with - | WithTop t -> - (try t.load_obj s - with - | (UserError _ | Failure _ | Anomaly _ | Not_found as u) -> raise u - | _ -> errorlabstrm "Mltop.load_object" (str"Cannot link ml-object " ++ - str s ++ str" to Coq code.")) -(* TO DO: .cma loading without toplevel *) - | WithoutTop -> - IFDEF HasDynlink THEN - (* WARNING - * if this code section starts to use a module not used elsewhere - * in this file, the Makefile dependency logic needs to be updated. - *) - let warn = Flags.is_verbose() in - let _,gname = find_file_in_path ~warn !coq_mlpath_copy s in - try - Dynlink.loadfile gname; - with | Dynlink.Error a -> - errorlabstrm "Mltop.load_object" (str (Dynlink.error_message a)) - ELSE - errorlabstrm "Mltop.no_load_object" - (str"Loading of ML object file forbidden in a native Coq.") - END - -(* Dynamic interpretation of .ml *) -let dir_ml_use s = - match !load with - | WithTop t -> t.use_file s - | _ -> msg_warning (str "Cannot access the ML compiler") - -(* Adds a path to the ML paths *) -let add_ml_dir s = - match !load with - | WithTop t -> t.add_dir s; keep_copy_mlpath s - | WithoutTop when has_dynlink -> keep_copy_mlpath s - | _ -> () - -(* For Rec Add ML Path *) -let add_rec_ml_dir unix_path = - List.iter (fun (lp,_) -> add_ml_dir lp) (all_subdirs ~unix_path) - -(* Adding files to Coq and ML loadpath *) - -let add_path ~unix_path:dir ~coq_root:coq_dirpath = - if exists_dir dir then - begin - add_ml_dir dir; - Library.add_load_path true (dir,coq_dirpath) - end - else - msg_warning (str ("Cannot open " ^ dir)) - -let convert_string d = - try Names.id_of_string d - with _ -> - if_warn msg_warning (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)")); - raise Exit - -let add_rec_path ~unix_path ~coq_root = - if exists_dir unix_path then - let dirs = all_subdirs ~unix_path in - let prefix = Names.repr_dirpath coq_root in - let convert_dirs (lp, cp) = - try - let path = List.map convert_string (List.rev cp) @ prefix in - Some (lp, Names.make_dirpath path) - with Exit -> None - in - let dirs = List.map_filter convert_dirs dirs in - List.iter (fun lpe -> add_ml_dir (fst lpe)) dirs; - add_ml_dir unix_path; - List.iter (Library.add_load_path false) dirs; - Library.add_load_path true (unix_path, coq_root) - else - msg_warning (str ("Cannot open " ^ unix_path)) - -(* convertit un nom quelconque en nom de fichier ou de module *) -let mod_of_name name = - let base = - if Filename.check_suffix name ".cmo" then - Filename.chop_suffix name ".cmo" - else - name - in - String.capitalize base - -let get_ml_object_suffix name = - if Filename.check_suffix name ".cmo" then - Some ".cmo" - else if Filename.check_suffix name ".cma" then - Some ".cma" - else if Filename.check_suffix name ".cmxs" then - Some ".cmxs" - else - None - -let file_of_name name = - let name = String.uncapitalize name in - let suffix = get_ml_object_suffix name in - let fail s = - errorlabstrm "Mltop.load_object" - (str"File not found on loadpath : " ++ str s) in - if is_native then - let name = match suffix with - | Some ((".cmo"|".cma") as suffix) -> - (Filename.chop_suffix name suffix) ^ ".cmxs" - | Some ".cmxs" -> name - | _ -> name ^ ".cmxs" - in - if is_in_path !coq_mlpath_copy name then name else fail name - else - let (full, base) = match suffix with - | Some ".cmo" | Some ".cma" -> true, name - | Some ".cmxs" -> false, Filename.chop_suffix name ".cmxs" - | _ -> false, name - in - if full then - if is_in_path !coq_mlpath_copy base then base else fail base - else - let name = base ^ ".cmo" in - if is_in_path !coq_mlpath_copy name then name else - let name = base ^ ".cma" in - if is_in_path !coq_mlpath_copy name then name else - fail (base ^ ".cm[oa]") - -(** 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. *) - -(* [known_loaded_module] contains the names of the loaded ML modules - * (linked or loaded with load_object). It is used not to load a - * module twice. It is NOT the list of ML modules Coq knows. *) - -let known_loaded_modules = ref Stringset.empty - -let add_known_module mname = - let mname = String.capitalize mname in - known_loaded_modules := Stringset.add mname !known_loaded_modules - -let module_is_known mname = - Stringset.mem (String.capitalize mname) !known_loaded_modules - -(** A plugin is just an ML module with an initialization function. *) - -let known_loaded_plugins = ref Stringmap.empty - -let add_known_plugin init name = - let name = String.capitalize name in - add_known_module name; - known_loaded_plugins := Stringmap.add name init !known_loaded_plugins - -let init_known_plugins () = - Stringmap.iter (fun _ f -> f()) !known_loaded_plugins - -(** ml object = ml module or plugin *) - -let init_ml_object mname = - try Stringmap.find mname !known_loaded_plugins () - with Not_found -> () - -let load_ml_object mname fname= - dir_ml_load fname; - add_known_module mname; - init_ml_object mname - -(* Summary of declared ML Modules *) - -(* List and not Stringset because order is important: most recent first. *) - -let loaded_modules = ref [] -let get_loaded_modules () = List.rev !loaded_modules -let add_loaded_module md = loaded_modules := md :: !loaded_modules -let reset_loaded_modules () = loaded_modules := [] - -let if_verbose_load verb f name fname = - if not verb then f name fname - else - let info = "[Loading ML file "^fname^" ..." in - try - f name fname; - msg_info (str (info^" done]")); - with e -> - msg_info (str (info^" failed]")); - raise e - -(** Load a module for the first time (i.e. dynlink it) - or simulate its reload (i.e. doing nothing except maybe - an initialization function). *) - -let cache_ml_object verb reinit name = - begin - if module_is_known name then - (if reinit then init_ml_object name) - else if not has_dynlink then - error ("Dynamic link not supported (module "^name^")") - else - if_verbose_load (verb && is_verbose ()) - load_ml_object name (file_of_name name) - end; - add_loaded_module name - -let unfreeze_ml_modules x = - reset_loaded_modules (); - List.iter (cache_ml_object false false) x - -let _ = - Summary.declare_summary "ML-MODULES" - { Summary.freeze_function = get_loaded_modules; - Summary.unfreeze_function = unfreeze_ml_modules; - Summary.init_function = reset_loaded_modules } - -(* Liboject entries of declared ML Modules *) - -type ml_module_object = { - mlocal : Vernacexpr.locality_flag; - mnames : string list -} - -let cache_ml_objects (_,{mnames=mnames}) = - List.iter (cache_ml_object true true) mnames - -let classify_ml_objects ({mlocal=mlocal} as o) = - if mlocal then Dispose else Substitute o - -let inMLModule : ml_module_object -> obj = - declare_object - {(default_object "ML-MODULE") with - load_function = (fun _ -> cache_ml_objects); - cache_function = cache_ml_objects; - subst_function = (fun (_,o) -> o); - classify_function = classify_ml_objects } - -let declare_ml_modules local l = - let l = List.map mod_of_name l in - Lib.add_anonymous_leaf (inMLModule {mlocal=local; mnames=l}) - -let print_ml_path () = - let l = !coq_mlpath_copy in - str"ML Load Path:" ++ fnl () ++ str" " ++ - hv 0 (prlist_with_sep fnl str l) - -(* Printing of loaded ML modules *) - -let print_ml_modules () = - let l = get_loaded_modules () in - str"Loaded ML Modules: " ++ pr_vertical_list str l -- cgit v1.2.3