Module Library
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_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 indirect_accessor : Global.indirect_accessor
Opaque accessors