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.3.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).

SEE ALSO

       The full documentation for sercomp is maintained as a Texinfo manual.  If the info and  sercomp  programs
       are properly installed at your site, the command

              info sercomp

       should give you access to the complete manual.

sercomp                                             June 2025                                         SERCOMP(1)