diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/declaremods.ml | 4 | ||||
| -rw-r--r-- | library/declaremods.mli | 2 | ||||
| -rw-r--r-- | library/global.ml | 3 | ||||
| -rw-r--r-- | library/global.mli | 2 | ||||
| -rw-r--r-- | library/library.ml | 6 | ||||
| -rw-r--r-- | library/library.mli | 4 |
6 files changed, 12 insertions, 9 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml index 8699583cdf..5fd11e187a 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -928,10 +928,10 @@ let append_end_library_hook f = let old_f = !end_library_hook in end_library_hook := fun () -> old_f(); f () -let end_library ?except dir = +let end_library ?except ~output_native_objects dir = !end_library_hook(); let oname = Lib.end_compilation_checks dir in - let mp,cenv,ast = Global.export ?except dir in + let mp,cenv,ast = Global.export ?except ~output_native_objects dir in let prefix, lib_stack = Lib.end_compilation oname in assert (ModPath.equal mp (MPfile dir)); let substitute, keep, _ = Lib.classify_segment lib_stack in diff --git a/library/declaremods.mli b/library/declaremods.mli index 7aa4bc30ce..2b28ba908e 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -99,7 +99,7 @@ val get_library_native_symbols : library_name -> Nativecode.symbols val start_library : library_name -> unit val end_library : - ?except:Future.UUIDSet.t -> library_name -> + ?except:Future.UUIDSet.t -> output_native_objects:bool -> library_name -> Safe_typing.compiled_library * library_objects * Safe_typing.native_library (** append a function to be executed at end_library *) diff --git a/library/global.ml b/library/global.ml index 784a02449c..cf996ce644 100644 --- a/library/global.ml +++ b/library/global.ml @@ -143,7 +143,8 @@ let mind_of_delta_kn kn = (** Operations on libraries *) let start_library dir = globalize (Safe_typing.start_library dir) -let export ?except s = Safe_typing.export ?except (safe_env ()) s +let export ?except ~output_native_objects s = + Safe_typing.export ?except ~output_native_objects (safe_env ()) s let import c u d = globalize (Safe_typing.import c u d) diff --git a/library/global.mli b/library/global.mli index df18625a5f..4e2ad92717 100644 --- a/library/global.mli +++ b/library/global.mli @@ -108,7 +108,7 @@ val body_of_constant_body : Declarations.constant_body -> (Constr.constr * Univ. (** {6 Compiled libraries } *) val start_library : DirPath.t -> ModPath.t -val export : ?except:Future.UUIDSet.t -> DirPath.t -> +val export : ?except:Future.UUIDSet.t -> output_native_objects:bool -> DirPath.t -> ModPath.t * Safe_typing.compiled_library * Safe_typing.native_library val import : Safe_typing.compiled_library -> Univ.ContextSet.t -> Safe_typing.vodigest -> diff --git a/library/library.ml b/library/library.ml index 9b9bd07c93..37dadadb76 100644 --- a/library/library.ml +++ b/library/library.ml @@ -657,7 +657,7 @@ let error_recursively_dependent_library dir = (* Security weakness: file might have been changed on disk between writing the content and computing the checksum... *) -let save_library_to ?todo dir f otab = +let save_library_to ?todo ~output_native_objects dir f otab = let except = match todo with | None -> (* XXX *) @@ -668,7 +668,7 @@ let save_library_to ?todo dir f otab = assert(Filename.check_suffix f ".vio"); List.fold_left (fun e (r,_) -> Future.UUIDSet.add r.Stateid.uuid e) Future.UUIDSet.empty l in - let cenv, seg, ast = Declaremods.end_library ~except dir in + let cenv, seg, ast = Declaremods.end_library ~output_native_objects ~except dir in let opaque_table, univ_table, disch_table, f2t_map = Opaqueproof.dump otab in let tasks, utab, dtab = match todo with @@ -716,7 +716,7 @@ let save_library_to ?todo dir f otab = System.marshal_out_segment f' ch (opaque_table : seg_proofs); close_out ch; (* Writing native code files *) - if !Flags.output_native_objects then + if output_native_objects then let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in if not (Nativelib.compile_library dir ast fn) then user_err Pp.(str "Could not compile the library to native code.") diff --git a/library/library.mli b/library/library.mli index c016352808..a976be0184 100644 --- a/library/library.mli +++ b/library/library.mli @@ -38,9 +38,11 @@ type seg_proofs = Constr.constr Future.computation array an export otherwise just a simple import *) val import_module : bool -> qualid list -> unit -(** End the compilation of a library and save it to a ".vo" file *) +(** End the compilation of a library and save it to a ".vo" file. + [output_native_objects]: when producing vo objects, also compile the native-code version. *) val save_library_to : ?todo:(((Future.UUID.t,'document) Stateid.request * bool) list * 'counters) -> + output_native_objects:bool -> DirPath.t -> string -> Opaqueproof.opaquetab -> unit val load_library_todo : |