package coq-core

You can search for identifiers within the package.

in-package search v0.2.0

The Coq Proof Assistant -- Core Binaries and Tools

Install

Dune Dependency

coq.inria.fr Readme Edit opam file Versions (9)

Authors

T

The Coq development team, INRIA, CNRS, and contributors

Maintainers

T

The Coq development team <coqdev@inria.fr>

Sources

coq-8.19.0.tar.gz

md5=64b49dbc3205477bd7517642c0b9cbb6

sha512=02fb5b4fb575af79e092492cbec6dc0d15a1d74a07f827f657a72d4e6066532630e5a6d15be4acdb73314bd40b9a321f9ea0584e0ccfe51fd3a56353bd30db9b

doc/coq-core.vernac/Library/index.html

Module `Library`Source

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.

Sourcetype library_t

Type of libraries loaded in memory

Sourceval require_library_from_dirpath : library_t list -> unit

...

Require = load in the environment

Source

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

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 =

| ProofsTodoNone
| ProofsTodoSomeEmpty of Future.UUIDSet.t
| ProofsTodoSome of Future.UUIDSet.t * (Future.UUID.t, 'doc) tasks

Source

val save_library_to : 
  'document todo_proofs ->
  output_native_objects:bool ->
  Names.DirPath.t ->
  string ->
  unit

Source

val load_library_todo : 
  CUnix.physical_path ->
  seg_sum
  * seg_lib
  * seg_univ
  * (Opaqueproof.opaque_handle option, 'doc) tasks
  * seg_proofs

Source

val 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 native_name_from_filename : string -> string

Native compiler.

Sourceval indirect_accessor : Global.indirect_accessor

Opaque accessors

On This Page

Start the compilation of a library
Interrogate the status of libraries

package coq-core

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.vernac/Library/index.html

Module LibrarySource

Start the compilation of a library

Interrogate the status of libraries

Module `Library`Source