package coq

  1. Overview
  2. Docs
package coq
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module LibrarySource

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.

Sourceval 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
Sourcetype seg_sum

Segments of a library

Sourcetype seg_lib
Sourcetype seg_univ = Univ.ContextSet.t * bool
Sourcetype 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.

Sourcetype ('uid, 'doc) tasks = (('uid, 'doc) Stateid.request * bool) list
Sourcetype 'doc todo_proofs =
  1. | ProofsTodoNone
  2. | ProofsTodoSomeEmpty of Future.UUIDSet.t
  3. | ProofsTodoSome of Future.UUIDSet.t * (Future.UUID.t, 'doc) tasks
Sourceval save_library_to : 'document todo_proofs -> output_native_objects:bool -> Names.DirPath.t -> string -> unit
Sourceval save_library_raw : string -> seg_sum -> seg_lib -> seg_univ -> seg_proofs -> unit
Interrogate the status of libraries
Sourceval library_is_loaded : Names.DirPath.t -> bool
  • Tell if a library is loaded
Sourceval loaded_libraries : unit -> Names.DirPath.t list
  • Tell which libraries are loaded
Sourceval library_full_filename : Names.DirPath.t -> string
  • Return the full filename of a loaded library.
Sourceval overwrite_library_filenames : string -> unit
  • Overwrite the filename of all libraries (used when restoring a state)
Sourceval native_name_from_filename : string -> string

Native compiler.

Sourceval indirect_accessor : Global.indirect_accessor

Opaque accessors

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct