SERTOP(1)

📦 version 8.20.0+0.20.0, in debian trixie, ubuntu questing

👑 NAME 👑

okay bestie, welcome to <strong>sertop</strong></strong> — the SerAPI Coq Toplevel, and yes it's serving main character energy in your terminal 💅

🌈 SYNOPSIS 🌈

sertop [OPTION]???

(yeah, those three question marks are literally in there, she's mysterious like that ✨)

🦋 DESCRIPTION 🦋

Experimental Coq Toplevel with Serialization Support — that's the whole vibe. It's a Coq toplevel, it's experimental, and it serializes stuff. Slay. 🎀

💖 USAGE 💖

So here's how you actually talk to her, bestie. To build a Coq document, you 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. (Not me being obsessed with how it just splits them like that 😭)

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

(Exec 5)

Other queries are also possible; some examples, fr fr:

(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 — iykyk 🌸

✨ OPTIONS ✨

  • --async=COQTOP — Enable async support using Coq binary COQTOP (experimental). 👀 experimental, bestie, tread lightly
  • --async-workers=VAL (absent=3) — Maximum number of async workers. Three little worker bees by default 🐝
  • --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). Not me revoking SProp privileges 💀
  • --error-recovery — Enable Coq's error recovery inside tactics and commands. She heals 💅
  • --exn_on_opaque — [debug option] raise an exception on non-serializeble terms. (yes, "serializeble" is spelled exactly like that, we don't fix her typos, she's iconic 🙈)
  • -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). She literally does nothing and we respect her for it 🫶
  • --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). indices MATTER periodt ✨
  • --length — Emit a byte-length header before output. (deprecated). ⚠️ deprecated, bestie, the old ways are fading
  • --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. You're on your own, main character 🫡
  • --omit_att — [debug option] omit attribute nodes.
  • --omit_env — [debug option] turn enviroments into abstract objects. (again: "enviroments", verbatim, no notes 💀)
  • --omit_loc — [debug option] shorten location printing.
  • --print0 — End responses with a \0 char. Null byte girlie 🌸
  • --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. Recursive queen 👑
  • --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). 😭 not the 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. go read it bestie, it's giving ✨informed✨

and that's the whole page, no cap 💜 this was sertop from June 2025, mwah, bye!! 🎀✨💅

📦 where this page comes from