Module Library

This module provides functions to load, open and save libraries. Libraries correspond to the subclass of modules that coincide with a file on disk (the ".vo" files). Libraries on the disk comes with checksums (obtained with the Digest module), which are checked at loading time to prevent inconsistencies between files written at various dates.

val require_library_from_dirpath : (Names.DirPath.t * string) list -> bool option -> unit
...

Require = load in the environment + open (if the optional boolean is not None); mark also for export if the boolean is Some true

Start the compilation of a library
type seg_sum

Segments of a library

type seg_lib
type seg_univ = Univ.ContextSet.t Future.computation array * Univ.ContextSet.t * bool
type seg_discharge = Opaqueproof.cooking_info list array
type seg_proofs = Constr.constr Future.computation array
val import_module : bool -> Libnames.qualid list -> unit

Open a module (or a library); if the boolean is true then it's also an export otherwise just a simple import

val save_library_to : ?⁠todo:(((Future.UUID.t, 'document) Stateid.request * bool) list * 'counters) -> output_native_objects:bool -> Names.DirPath.t -> string -> Opaqueproof.opaquetab -> unit

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 load_library_todo : string -> seg_sum * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs
val save_library_raw : string -> seg_sum -> seg_lib -> seg_univ -> seg_proofs -> unit
Interrogate the status of libraries
val library_is_loaded : Names.DirPath.t -> bool
  • Tell if a library is loaded or opened
val library_is_opened : Names.DirPath.t -> bool
val loaded_libraries : unit -> Names.DirPath.t list
  • Tell which libraries are loaded or imported
val opened_libraries : unit -> Names.DirPath.t list
val library_full_filename : Names.DirPath.t -> string
  • Return the full filename of a loaded library.
val overwrite_library_filenames : string -> unit
  • Overwrite the filename of all libraries (used when restoring a state)
exception LibUnmappedDir
Locate a library in the load paths
exception LibNotFound
type library_location =
| LibLoaded
| LibInPath
val locate_qualified_library : ?⁠root:Names.DirPath.t -> ?⁠warn:bool -> Libnames.qualid -> library_location * Names.DirPath.t * CUnix.physical_path

Locates a library by implicit name.

raises LibUnmappedDir

if the library is not in the path

raises LibNotFound

if there is no corresponding file in the path

val native_name_from_filename : string -> string
Native compiler.