NAME

       sertop - manual page for sertop

DESCRIPTION

       NAME

              sertop - SerAPI Coq Toplevel

       SYNOPSIS

              sertop [OPTION]???

       DESCRIPTION

              Experimental Coq Toplevel with Serialization Support

       USAGE

              To build a Coq document, use the `Add` command:

              (Add () "Lemma addn0 n : n + 0. Proof. now induction n. Qed.")

              SerAPI will parse and split the document into "logical" sentences.

              Then, you can ask Coq to check the proof with `Exec`:

              (Exec 5)

              Other queries are also possible; some examples:

              (Query ((sid 4)) Ast)

              Will print the AST at sentence 4.

              (Query ((sid 3)) Goals)

              Will print the goals at sentence 3.

              See the documentation on the project's webpage for more information

       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.

       --deep-edits

              Enable Coq's deep document edits option.

       --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

       --implicit

              No-op (used to allow loading unqualified stdlib libraries, which is now the default).

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

       --length

              Emit a byte-length header before output. (deprecated).

       --no_init

              Omits the creation of a new document; this means the user will have to call `(NewDoc ...)`  before
              Coq can be used and set there the proper loadpath, requires, ...

       --no_prelude

              Omits requiring any module on start, thus `Prelude`, ltac, etc...  won't be available

       --omit_att

              [debug option] omit attribute nodes

       --omit_env

              [debug option] turn enviroments into abstract objects

       --omit_loc

              [debug option] shorten location printing

       --print0

              End responses with a \0 char.

       --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

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

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

       --topfile=TOPFILE

              Set the toplevel name as though compiling TOPFILE

       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

              sertop 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 sertop is maintained as a Texinfo manual.  If the info and sertop programs are
       properly installed at your site, the command

              info sertop

       should give you access to the complete manual.

sertop                                            February 2025                                        SERTOP(1)