Module `Library`

val require_library_from_dirpath : lib_resolver:(Names.DirPath.t -> CUnix.physical_path) -> (Names.DirPath.t * string) list -> unit: ...
Require = load in the environment

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

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 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)

val native_name_from_filename : string -> string: Native compiler.

val indirect_accessor : Global.indirect_accessor: Opaque accessors