NAME

sercomp - manual page for sercomp

DESCRIPTION

NAME

: sercomp - sercomp Coq Compiler

SYNOPSIS

: sercomp [OPTION]??? FILE

DESCRIPTION

: Experimental Coq compiler with serialization and deserialization support.

USAGE

: To serialize `fs/fun.v` with logical path `Funs`:
: sercomp -Q fs,Funs --input=vernac --mode=sexp fs/fun.v > fs/fun.sexp
: To deserialize and check `fs/fun.sexp` with logical path `Funs`:
: sercomp -Q fs,Funs --input=sexp --mode=check fs/fun.sexp
: To generate `fs/fun.vo` from `fs/fun.sexp` with logical path `Funs`:
: sercomp -Q fs,Funs --input=sexp --mode=vo fs/fun.sexp
: See the documentation on the project's webpage for more information.

ARGUMENTS

: FILE (required)
: Input file.

OPTIONS

--async=COQTOP

: Enable async support using Coq binary COQTOP (experimental).

--async-workers=VAL (absent=3)

: Maximum number of async workers.

--coqlib=COQPATH (absent=/usr/lib/x86_64-linux-gnu/ocaml/5.2.0/coq)

: Load Coq.Init.Prelude from COQPATH; plugins/ and theories/ should live there.

--debug

: Enable debug mode for Coq.

--disallow-sprop

: Forbid using the proof irrelevant SProp sort (allowed by default)

--error-recovery

: Enable Coq's error recovery inside tactics and commands.

--exn_on_opaque

: [debug option] raise an exception on non-serializeble terms

-I DIR, --ml-include-path=DIR

: Include DIR in default loadpath, for locating ML files

--impredicative-set

: Enable Coq -impredicative-set option (disabled by default)

--indices-matter

: Levels of indices (and nonuniform parameters) contribute to the level of inductives (disabled by default)

--input=VAL (absent=vernac)

: either vernac: Coq vernacular or sexp: serialized Coq vernacular

--mode=VAL (absent=parse)

: one of parse: parse the file and remain silent (except for Coq output), stats: output stats on the input file, print: output using the Coq pretty printer, sexp: output serialized version of the input file, check: check proofs in the file and remain silent (except for Coq output), vo: check proofs and output .vo version of the input file or kenv: check proofs and output the final kernel enviroment

--omit_att

: [debug option] omit attribute nodes

--omit_env

: [debug option] turn enviroments into abstract objects

--omit_loc

: [debug option] shorten location printing

--printer=VAL (absent=sertop)

: one of sertop, a custom printer (UTF-8 with emacs-compatible quoting), human, sexplib's human-format printer (recommended for debug sessions) or mach, sexplib's machine-format printer

-Q DIR,LP, --load-path=DIR,LP

: Bind a logical loadpath LP to a directory DIR

--quick

: Skip checking opaque proofs (very experimental).

-R DIR,LP, --rec-load-path=DIR,LP

: Bind a logical loadpath LP to a directory DIR and implicitly open its namespace.

COMMON OPTIONS

--help[=FMT] (default=auto)

: Show this help in format FMT. The value FMT must be one of auto, pager, groff or plain. With auto, the format is pager or plain whenever the TERM env var is dumb or undefined.

--version

: Show version information.

EXIT STATUS

: sercomp exits with:

0: on success.

: 123 on indiscriminate errors reported on standard error.
: 124 on command line parsing errors.
: 125 on unexpected internal errors (bugs).

NAME

DESCRIPTION

SEE ALSO