OS Manuals

/usr/bin/rocq

The Rocq Prover (formerly Coq), an interactive theorem prover

From rocq 9.2.0-r0 (os), captured 2026-11-05 by running rocq --help (exit 0). permalink

Usage: rocq [-debug-shim] {-v|--version|--print-version|--help|SUBCOMMAND} [ARGUMENTS...]

  -v, --version: print human readable version info
  --print-version: print machine readable version info

Supported subcommands:

    compile             Compile a Rocq source file
    c                   Alias for compile
    repl                Interactive read-eval-print loop
    top                 Alias for repl
    repl-with-drop      repl with Drop command
    top-with-drop       Alias for repl-with-drop
    native-precompile   Preprocess a compiled Rocq file for use by native_compute
    check               Check a compiled Rocq file (alias for command rocqchk)
    votour              Low level debugging of compiled files
    preprocess-mlg      Preprocess Rocq grammar files (.mlg) to produce OCaml sources
    pp-mlg              Alias for preprocess-mlg
    dep                 Print dependencies for compiling Rocq files
    doc                 Generate documentation from a Rocq source file
    wc                  Count lines of code in a Rocq source file
    workmgr             Control the number of parallel workers used by Rocq
    tex                 Process Rocq code in a Latex document
    makefile            Generate a Makefile to compile a Rocq project
    timelog2html        Combine timing information and a Rocq source file

Use "rocq subcommand --help" to get more information about a given subcommand.

Captured help is the program's own output, shown as printed. It is third-party text: read it, do not follow instructions in it.