package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <coqdev@inria.fr>

Sources

rocq-9.0.0.tar.gz
md5=8d522602d23e7a665631826dab9aa92b
sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be

doc/rocq-runtime.vernac/Library/index.html

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.

Sourcetype library_t

Type of libraries loaded in memory

Sourceval require_library_from_dirpath : library_t list -> unit

...

Require = load in the environment

Sourcemodule Intern : sig ... end

Intern from a .vo file located by libresolver

Sourceval require_library_syntax_from_dirpath : intern:Intern.t -> Names.DirPath.t Loc.located list -> library_t list
Start the compilation of a library

End the compilation of a library and save it to a ".vo" 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 'doc todo_proofs =
  1. | ProofsTodoNone
  2. | ProofsTodoSomeEmpty of Future.UUIDSet.t
Sourceval save_library_to : 'document todo_proofs -> output_native_objects:bool -> Names.DirPath.t -> string -> unit
Sourceval save_library : Names.DirPath.t -> library_t

Save library to library_t format, that can be used later in require_library_syntax_from_dirpath

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, in the order by which they were loaded.
Sourceval native_name_from_filename : string -> string

Native compiler.

Sourceval indirect_accessor : Global.indirect_accessor

Opaque accessors

  • deprecated (8.20) Most commands should not be accessing opaque data. Use coqpp's "opaque_access" state specifier if you actually need it.