\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\In}{\kw{in}} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[4]{\kw{Ind}_{#4}[#1](#2:=#3)} \newcommand{\Indpstr}[5]{\kw{Ind}_{#4}[#1](#2:=#3)/{#5}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \newcommand{\length}{\textsf{length}} \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\List}{\textsf{list}} \newcommand{\lra}{\longrightarrow} \newcommand{\Match}{\kw{match}} \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} \newcommand{\ModImp}[3]{{\kw{Mod}}({#1}:{#2}:={#3})} \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} \newcommand{\mto}{.\;} \newcommand{\nat}{\textsf{nat}} \newcommand{\Nil}{\textsf{nil}} \newcommand{\nilhl}{\textsf{nil\_hl}} \newcommand{\nO}{\textsf{O}} \newcommand{\node}{\textsf{node}} \newcommand{\nS}{\textsf{S}} \newcommand{\odd}{\textsf{odd}} \newcommand{\oddS}{\textsf{odd}_\textsf{S}} \newcommand{\ovl}[1]{\overline{#1}} \newcommand{\Pair}{\textsf{pair}} \newcommand{\plus}{\mathsf{plus}} \newcommand{\SProp}{\textsf{SProp}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\Sort}{\mathcal{S}} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \newcommand{\trii}{\triangleright_\iota} \newcommand{\Type}{\textsf{Type}} \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WF}[2]{{\mathcal{W\!F}}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WFT}[2]{#1[] \vdash {\mathcal{W\!F}}(#2)} \newcommand{\WFTWOLINES}[2]{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} \newcommand{\with}{\kw{with}} \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} \newcommand{\zeroone}[1]{[{#1}]} \end{split}\]

The Rocq Prover commands

There are several Rocq commands:

• coqide: a graphical integrated development environment, described here. In addition, there are several other IDEs such as Proof General, vsCoq and Coqtail that are not included with the Coq installation.

• rocq: the main entry point for the Rocq prover

• rocqchk: the Rocq checker (validation of compiled libraries) (also available through rocq check)

Many of the parameters to start these tools are shared and are described below. Passing the -help option on the command line will print a summary of the available command line parameters. There are also man pages for each of these, but they are probably less current than -help or this document).

Interactive use (rocq repl)

The Rocq toplevel (or read-eval-print-loop) is run by the command rocq repl (equivalently, rocq top).

There is also a byte-code toplevel rocq repl-with-drop based on an OCaml toplevel. You can switch to the OCaml toplevel with the command Drop., and come back to the Rocq toplevel with the command #go;;.

Flag Coqtop Exit On Error

This flag, off by default, causes rocq top to exit with status code 1 if a command produces an error instead of recovering from it.

Batch compilation (rocq compile)

The rocq compile (equivalently, rocq c) command compiles a Rocq proof script file with a ".v" suffix to create a compiled file with a ".vo" suffix. (See Compiled files.) The last component of the filename must be a valid Rocq identifier as described in Lexical conventions; it should contain only letters, digits or underscores (_) with a ".v" suffix on the final component. For example /bar/foo/toto.v is valid, but /bar/foo/to-to.v is not.

We recommend specifying a logical path (which is also the module name) with the -R or the -Q options. Generally we recommend using utilities such as make (using rocq makefile to generate the Makefile) or dune to build Rocq projects. See Building a Rocq project with rocq makefile (details) and Building a Rocq project with Dune.

Example: Compiling and loading a single file

If foo.v is in Rocq's current directory, you can use rocq c foo.v to compile it and then Require foo. in your script. But this doesn't scale well for larger projects.

Generally it's better to define a new module: To compile foo.v as part of a module Mod1 that is rooted at . (i.e. the directory containing foo.v), run rocq c -Q . Mod1 foo.v.

To make the module available in CoqIDE, include the following line in the _CoqProject file (see Building a Rocq project with rocq makefile (details)) in the directory from which you start CoqIDE or give it as an argument to the coqide command. <PATH> is the pathname of the directory containing the module, which can be an absolute path or relative to Rocq's current directory. For now, you must close and reload a named script file for CoqIDE to pick up the change, or restart CoqIDE. The project file name is configurable in Edit / Preferences / Project.

-R <PATH> Mod1

Customization at launch time

Command parameters

There are 3 mechanisms for passing parameters to Rocq commands. In order of importance they are:

• command line options,

• environment variables and

• the coqrc start up script

coqrc start up script

When Rocq is launched, it can implicitly prepend a startup script to any document it reads, whether it is an interactive session or a file to compile. The startup script can come from a configuration directory or it can be specified on the command line.

Coq uses the first file found in this list as the startup script:

• $XDG_CONFIG_HOME/coqrc.<VERSION>

• $XDG_CONFIG_HOME/coqrc

• $HOME/.coqrc.<VERSION>

• $HOME/.coqrc

where $XDG_CONFIG_HOME is an environment variable. $HOME is the user's home directory. <VERSION> is the version of Rocq (as shown by rocq --version, for example).

-init-file file on the command line uses the specified file instead of a startup script from a configuration directory. -q prevents the use of a startup script.

Environment variables

$ROCQPATH can be used to specify the load path. It is a list of directories separated by : (; on Windows). Coq will also honor $XDG_DATA_HOME and $XDG_DATA_DIRS (see Section Logical paths and the load path).

Makefiles generated by rocq makefile call other Rocq commands. In this case, they look for the commands in directory specified by $COQBIN. If this variable is not set, they look for the commands in the executable path.

$ROCQ_COLORS can be used to specify the set of colors used by rocq repl to highlight its output. It uses the same syntax as the $LS_COLORS variable from GNU’s ls, that is, a colon-separated list of assignments of the form name=attr*; where name is the name of the corresponding highlight tag and each attr is an ANSI escape code. The list of highlight tags can be retrieved with the -list-tags command-line option of rocq repl.

The string uses ANSI escape codes to represent attributes. For example:

export ROCQ_COLORS=”diff.added=4;48;2;0;0;240:diff.removed=41”

sets the highlights for added text in diffs to underlined (the 4) with a background RGB color (0, 0, 240) and for removed text in diffs to a red background. Note that if you specify ROCQ_COLORS, the predefined attributes are ignored.

$OCAMLRUNPARAM, described here, can be used to specify certain runtime and memory usage parameters. In most cases, experimenting with these settings will likely not cause a significant performance difference and should be harmless.

If the variable is not set, Rocq uses the default values, except that space_overhead is set to 120 and minor_heap_size is set to 32Mwords (256MB with 64-bit executables or 128MB with 32-bit executables).

Specifies which components produce events when using the Profiling system. It is a comma separated list of component names.

If the variable is not set, all components produce events.

Component names are internally defined, but command which corresponds to the interpretation of one command is particularly notable.

Command line options

The following command-line options are recognized by the commands rocq compile and rocq repl, unless stated otherwise:

-I directory, -include directory

Add physical path directory to the OCaml loadpath, which is needed to load OCaml object code files (.cmo or .cmxs). Subdirectories are not included. See the command Declare ML Module.

Directories added with -I are searched after the current directory, in the order in which they were given on the command line

-Q directory dirpath

Makes the .vo files in a package available for loading with the Require command by adding new entries to the load path. The entries map the logical path dirpath to the physical path directory. Then Rocq recursively adds load path entries for subdirectories. For example, -Q . Lib may add the logical path Lib.SubDir.File, which maps to the file ./SubDir/File.vo.

Only subdirectories and files that follow the lexical conventions for idents are included. Subdirectories named CVS or _darcs are excluded. Some operating systems or file systems are more restrictive. For example, Linux’s ext4 file system limits filenames to 255 bytes. The default on NTFS (Windows) and HFS+ (MacOS X) file systems is to disallow two files in the same directory with names that differ only in their case.

Loading files from packages made available with -Q must include the logical name of the package in From clause of the Require command or provide a fully qualified name.

-R directory dirpath

Similar to -Q directory dirpath, but allows using Require with a partially qualified name (i.e. without a From clause).

-top dirpath

Set the logical module name to dirpath for the rocq repl interactive session. If no module name is specified, rocq repl will default to Top. rocq compile does not accept this option because the logical module name is inferred from the name of the input file and the corresponding -R / -Q options.

-exclude-dir directory

Exclude any subdirectory named directory while processing options such as -R and -Q. By default, only the conventional version control management directories named CVS and_darcs are excluded.

-nois, -noinit

Start from an empty state instead of loading the Init.Prelude module.

-init-file file

Load file as the resource file instead of loading the default resource file from the standard configuration directories.

-q

Do not to load the default resource file.

-l file, -load-vernac-source file

Load and execute the Rocq script from file.v.

-lv file, -load-vernac-source-verbose file

Load and execute the Rocq script from file.v. Write its contents to the standard output as it is executed.

-require qualid

Load Rocq compiled library qualid. This is equivalent to running Require qualid (note: the short form -r *qualid* is intentionally not provided to prevent the risk of collision with -R).

Note

Note that the relative order of this command-line option and its variants (-ri, -re, -rfrom, -refrom, -rifrom) and of the -set and -unset options matters since the various Require, Require Import, Require Export, Set and Unset commands will be executed in the order specified on the command-line.

-ri qualid, -require-import qualid

Load Rocq compiled library qualid and import it. This is equivalent to running Require Import qualid. See the note above regarding the order of command-line options.

-re qualid, -require-export qualid

Load Rocq compiled library qualid and transitively import it. This is equivalent to running Require Export qualid. See the note above regarding the order of command-line options.

-rfrom dirpath qualid, -require-from dirpath qualid

Load Rocq compiled library qualid. This is equivalent to running From dirpath Require qualid. See the note above regarding the order of command-line options.

-rifrom dirpath qualid, -require-import-from dirpath qualid

Load Rocq compiled library qualid and import it. This is equivalent to running From dirpath Require Import qualid. See the note above regarding the order of command-line options.

-refrom dirpath qualid, -require-export-from dirpath qualid

Load Rocq compiled library qualid and transitively import it. This is equivalent to running From dirpath Require Export qualid. See the note above regarding the order of command-line options.

-load-vernac-object qualid

Obsolete synonym of -require qualid.

-batch

Exit just after argument parsing. Available for rocq repl only.

-verbose

Output the content of the input file as it is compiled. This option is available for rocq compile only.

-native-compiler (yes|no|ondemand)

Enable the native_compute reduction machine and precompilation to .cmxs files for future use by native_compute. Setting yes enables native_compute; it also causes Rocq to precompile the native code for future use; all dependencies need to have been precompiled beforehand. Setting no disables native_compute which defaults back to vm_compute; no files are precompiled. Setting ondemand enables native_compute but disables precompilation; all missing dependencies will be recompiled every time native_compute is called.

Deprecated since version 8.14: This flag has been deprecated in favor of calling rocq native-precompile. The toolchain has been adapted to transparently rely on the latter, so if you use Building a Rocq project with rocq makefile (details) there is nothing to do. Otherwise you should substitute calls to rocq c -native-compiler yes to calls to rocq compile followed by rocq native-precompile on the resulting vo file.

Changed in version 8.13: The default value is set at configure time, -config can be used to retrieve it. All this can be summarized in the following table:

configure	rocq compile	native_compute	outcome	requirements
yes	yes (default)	native_compute	.cmxs	.cmxs of deps
yes	no	vm_compute	none	none
yes	ondemand	native_compute	none	none
no	yes, no, ondemand	vm_compute	none	none
ondemand	yes	native_compute	.cmxs	.cmxs of deps
ondemand	no	vm_compute	none	none
ondemand	ondemand (default)	native_compute	none	none

-native-output-dir dir

Set the directory in which to put the aforementioned .cmxs for native_compute. Defaults to .coq-native.

-output-directory dir, -output-dir dir

Sets the output directory for commands that write output to files, such as Program extraction commands, Redirect and Print Universes.

-vos

Indicate Rocq to skip the processing of opaque proofs (i.e., proofs ending with Qed or Admitted), output a .vos files instead of a .vo file, and to load .vos files instead of .vo files when interpreting Require commands.

-vok

Indicate Rocq to check a file completely, to load .vos files instead of .vo files when interpreting Require commands, and to output an empty .vok files upon success instead of writing a .vo file.

-w (all|none|w₁,…,wₙ)

Configure the display of warnings. This option expects all, none or a comma-separated list of warning names or categories (see Section Controlling display).

-color (on|off|auto)

Enable or disable color output. Default is auto, meaning color is shown only if the output channel supports ANSI escape sequences.

-diffs (on|off|removed)

Rocq repl only. Controls highlighting of differences between proof steps. on highlights added tokens, removed highlights both added and removed tokens. Requires that -color is enabled. (see Section Showing differences between proof steps).

-beautify

Pretty-print each command to file.beautified when compiling file.v, in order to get old-fashioned syntax/definitions/notations.

-emacs, -ide-slave

Start a special toplevel to communicate with a specific IDE.

-impredicative-set

Change the logical theory of Rocq by declaring the sort Set impredicative.

Warning

This is known to be inconsistent with some standard axioms of classical mathematics such as the functional axiom of choice or the principle of description.

-type-in-type

Collapse the universe hierarchy of Rocq.

Warning

This makes the logic inconsistent.

-mangle-names ident

Experimental. Do not depend on this option. Replace Rocq's auto-generated name scheme with names of the form ident0, ident1, etc. Within Rocq, the Mangle Names flag turns this behavior on, and the Mangle Names Prefix option sets the prefix to use. This feature is intended to be used as a linter for developments that want to be robust to changes in the auto-generated name scheme. The options are provided to facilitate tracking down problems.

-set string

Enable flags and set options. string should be setting_name=value, the value is interpreted according to the type of the option. For flags setting_name is equivalent to setting_name=true. For instance -set "Universe Polymorphism" will enable Universe Polymorphism. Note that the quotes are shell syntax, Rocq does not see them. See the note above regarding the order of command-line options.

-unset string

As -set but used to disable options and flags. string must be "setting_name". See the note above regarding the order of command-line options.

-compat version

same as -compat-from Stdlib Rocq<version> (or Rocq when version is 8.*)

-compat-from root library

Loads a file that sets a few options to maintain partial backward-compatibility with a previous version. This is equivalent to -require-import-from <root> <library> except that a non existing file only produces a warning (so that the option can be uniformly used on older versions that didn't offer the compat file yet). Note that the explanations above regarding the order of command-line options apply, and this could be relevant if you are resetting some of the compatibility options.

-dump-glob file

Dump references for global names in file file (to be used by rocq doc, see Documenting Rocq files with rocq doc). By default, if file.v is being compiled, file.glob is used.

-no-glob

Disable the dumping of references for global names.

-image file

Set the binary image to be used by rocq compile to be file instead of the standard one. Not of general use.

-bindir directory

Set the directory containing Rocq binaries to be used by rocq compile. It is equivalent to doing export COQBIN= directory before launching rocq compile.

-where

Print the location of Rocq’s standard library and exit.

-config

Print the locations of Rocq’s binaries, dependencies, and libraries, then exit.

-filteropts

Print the list of command line arguments that rocq repl has recognized as options and exit.

-v

Print Rocq’s version and exit.

-list-tags

Print the highlight tags known by Rocq as well as their currently associated color and exit.

-h, --help

Print a short usage and exit.

-time

Output timing information for each command to standard output.

-time-file file

Output timing information for each command to the given file.

-profile file

Output Profiling information to the given file.

Profiling

Use the rocq compile command line argument -profile or the environment variable PROFILE in rocq makefile, to generate profiling information in Google trace format <https://docs.google.com/document/d/1CvAClvFfyA5R-PhYUmn5OOQtYMH4h6I0nSsKchNAySU/edit>.

The output gives the duration and event counts for the execution of components of Rocq (for instance process for the whole file, command for each command, pretyping for elaboration).

Environment variable ROCQ_PROFILE_COMPONENTS can be used to filter which components produce events. This may be needed to reduce the size of the generated file.

The generated file can be visualized with <https://ui.perfetto.dev> (which can directly load the .gz compressed file produced by rocq makefile) or processed using any JSON-capable system.

Events are annotated with additional information in the args field (either on the beginning B or end E event):

• major and minor indicate how many major and minor words were allocated during the event.

• subtimes indicates how much time was spent in sub-components and how many times each subcomponent was profiled during the event (including subcomponents which do not appear in ROCQ_PROFILE_COMPONENTS).

• for the command event, cmd displays the precise location of the command and a compressed representation of it (like the -time header), and line is the start line of the command.

Compiled interfaces (produced using -vos)

Compiled interfaces help saving time while developing Rocq formalizations, by compiling the formal statements exported by a library independently of the proofs that it contains.

Warning

Compiled interfaces should only be used for development purposes. At the end of the day, one still needs to proof check all files by producing standard .vo files. (Technically, when using -vos, fewer universe constraints are collected.) Moreover, this feature is still experimental, it may be subject to change without prior notice.

Principle.

The compilation using rocq c -vos foo.v produces a file called foo.vos, which is similar to foo.vo except that all opaque proofs are skipped in the compilation process.

The compilation using rocq c -vok foo.v checks that the file foo.v correctly compiles, including all its opaque proofs. If the compilation succeeds, then the output is a file called foo.vok, with empty contents. This file is only a placeholder indicating that foo.v has been successfully compiled. (This placeholder is useful for build systems such as make.)

When compiling a file bar.v that depends on foo.v (for example via a Require Foo. command), if the compilation command is rocq c -vos bar.v or rocq c -vok bar.v, then the file foo.vos gets loaded (instead of foo.vo). A special case is if file foo.vos exists and has empty contents, and foo.vo exists, then foo.vo is loaded.

Appart from the aforementioned case where foo.vo can be loaded in place of foo.vos, in general the .vos and .vok files live totally independently from the .vo files.

Dependencies generated by ``rocq makefile``.

The files foo.vos and foo.vok both depend on foo.v.

Furthermore, if a file foo.v requires bar.v, then foo.vos and foo.vok also depend on bar.vos.

Note, however, that foo.vok does not depend on bar.vok. Hence, as detailed further, parallel compilation of proofs is possible.

In addition, rocq makefile generates for a file foo.v a target foo.required_vos which depends on the list of .vos files that foo.vos depends upon (excluding foo.vos itself). As explained next, the purpose of this target is to be able to request the minimal working state for editing interactively the file foo.v.

Warning

When writing a custom build system, be aware that rocq dep only produces dependencies related to .vos and .vok if the -vos command line flag is passed. This is to maintain compatibility with dune (see ocaml/dune#2642 on github).

Typical compilation of a set of file using a build system.

Assume a file foo.v that depends on two files f1.v and f2.v. The command make foo.required_vos will compile f1.v and f2.v using the option -vos to skip the proofs, producing f1.vos and f2.vos. At this point, one is ready to work interactively on the file foo.v, even though it was never needed to compile the proofs involved in the files f1.v and f2.v.

Assume a set of files f1.v ... fn.v with linear dependencies. The command make vos enables compiling the statements (i.e. excluding the proofs) in all the files. Next, make -j vok enables compiling all the proofs in parallel. Thus, calling make -j vok directly enables taking advantage of a maximal amount of parallelism during the compilation of the set of files.

Note that this comes at the cost of parsing and typechecking all definitions twice, once for the .vos file and once for the .vok file. However, if files contain nontrivial proofs, or if the files have many linear chains of dependencies, or if one has many cores available, compilation should be faster overall.

Need for Proof using

When a theorem is in a section, typechecking the statement of the theorem may be insufficient to deduce the type of the statement at the end of the section. For example, the proof of the theorem may make use of section variables or section hypotheses that are not mentioned in the statement of the theorem.

For this reason, proofs in sections should begin with Proof using instead of Proof. The using clause should give the names of the section variables that are required for the proof that are not involved in the typechecking of the statement. See Suggest Proof Using. (Note it's fine to use Proof using. instead of Proof. for proofs that are not in a section.)

When using -vos, proofs in sections with Proof using are skipped. Proofs in sections without Proof using are fully processed (much slower).

Interaction with standard compilation

When compiling a file foo.v using rocq compile in the standard way (i.e., without -vos nor -vok), an empty file foo.vos and an empty file foo.vok are created in addition to the regular output file foo.vo. If rocq compile is subsequently invoked on some other file bar.v using option -vos or -vok, and that bar.v requires foo.v, if Rocq finds an empty file foo.vos, then it will load foo.vo instead of foo.vos.

The purpose of this feature is to allow users to benefit from the -vos option even if they depend on libraries that were compiled in the traditional manner (i.e., never compiled using the -vos option).

Compiled libraries checker (rocqchk)

The rocqchk command takes a list of library paths as argument, described either by their logical name or by their physical filename, which must end in .vo. The corresponding compiled libraries (.vo files) are searched in the path, recursively processing the libraries they depend on. The content of all these libraries is then type checked. The effect of rocqchk is only to return with normal exit code in case of success, and with positive exit code if an error has been found. Error messages are not deemed to help the user understand what is wrong. In the current version, it does not modify the compiled libraries to mark them as successfully checked.

Note that non-logical information is not checked. By logical information, we mean the type and optional body associated with names. It excludes for instance anything related to the concrete syntax of objects (customized syntax rules, association between short and long names), implicit arguments, etc.

This tool can be used for several purposes. One is to check that a compiled library provided by a third-party has not been forged and that loading it cannot introduce inconsistencies 1. Another point is to get an even higher level of security. Since rocq repl can be extended with custom tactics, possibly ill-typed code, it cannot be guaranteed that the produced compiled libraries are correct. rocqchk is a standalone verifier, and thus it cannot be tainted by such malicious code.

Command-line options -Q, -R, -where and -impredicative-set are supported by rocqchk and have the same meaning as for rocq repl. As there is no notion of relative paths in object files -Q and -R have exactly the same meaning.

-norec module

Check module but do not check its dependencies.

-admit module

Do not check module and any of its dependencies, unless explicitly required.

-o

At exit, print a summary about the context. List the names of all assumptions and variables (constants without a body).

-silent

Do not write progress information to the standard output.

Environment variable $ROCQLIB can be set to override the location of the standard library.

The algorithm for deciding which modules are checked or admitted is the following: assuming that rocqchk is called with argument M, option -norec N, and -admit A. Let us write \(\overline{S}\) for the set of reflexive transitive dependencies of set \(S\). Then:

• Modules \(C = \overline{M} \backslash \overline{A} \cup M \cup N\) are loaded and type checked before being added to the context.

• And \(M \cup N \backslash C\) is the set of modules that are loaded and added to the context without type checking. Basic integrity checks (checksums) are nonetheless performed.

As a rule of thumb, -admit can be used to tell Rocq that some libraries have already been checked. So rocqchk A B can be split in rocqchk A && rocqchk B -admit A without type checking any definition twice. Of course, the latter is slightly slower since it makes more disk access. It is also less secure since an attacker might have replaced the compiled library A after it has been read by the first command, but before it has been read by the second command.

1

Ill-formed non-logical information might for instance bind Corelib.Init.Logic.True to short name False, so apparently False is inhabited, but using fully qualified names, Corelib.Init.Logic.False will always refer to the absurd proposition, what we guarantee is that there is no proof of this latter constant.