package rocq-runtime
The Rocq Prover -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
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.
Type of libraries loaded in memory
Source
val intern_from_file :
CUnix.physical_path ->
(library_t, Exninfo.iexn) Result.t * Intern.Provenance.tSource
val require_library_syntax_from_dirpath :
intern:Intern.t ->
Names.DirPath.t Loc.located list ->
library_t listStart 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.
Source
val save_library_to :
'document todo_proofs ->
output_native_objects:bool ->
Names.DirPath.t ->
string ->
unitSave library to library_t format, that can be used later in require_library_syntax_from_dirpath
Interrogate the status of libraries
- Tell if a library is loaded
- Tell which libraries are loaded, in the order by which they were loaded.
Native compiler.
Opaque accessors