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.

type library_t

Type of libraries loaded in memory

val require_library_from_dirpath : library_t list -> unit

...

Require = load in the environment

val require_library_syntax_from_dirpath : lib_resolver:( Names.DirPath.t -> CUnix.physical_path ) -> Names.DirPath.t list -> library_t list
Start the compilation of a library
type seg_sum

Segments of a library

type seg_lib
type seg_univ = Univ.ContextSet.t * bool
type seg_proofs = Opaques.opaque_disk

End the compilation of a library and save it to a ".vo" file, a ".vio" file, or a ".vos" file, depending on the todo_proofs argument. output_native_objects: when producing vo objects, also compile the native-code version.

type ('uid, 'doc) tasks = (( 'uid, 'doc ) Stateid.request * bool) list
type 'doc todo_proofs =
| ProofsTodoNone
| ProofsTodoSomeEmpty of Future.UUIDSet.t
| ProofsTodoSome of Future.UUIDSet.t * ( Future.UUID.t, 'doc ) tasks
val save_library_to : 'document todo_proofs -> output_native_objects:bool -> Names.DirPath.t -> string -> unit
val load_library_todo : CUnix.physical_path -> seg_sum * seg_lib * seg_univ * ( Opaqueproof.opaque_handle option, 'doc ) 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
val loaded_libraries : unit -> Names.DirPath.t list
  • Tell which libraries are loaded
val native_name_from_filename : string -> string

Native compiler.

val indirect_accessor : Global.indirect_accessor

Opaque accessors