SERCOMP(1)

👑 SERCOMP — the manual page, but make it cute

okay bestie, sit down, hydrate, because we're about to talk about sercomp, aka sercomp Coq Compiler — the experimental Coq compiler with serialization AND deserialization support. it's giving "compiler but it also keeps receipts" and honestly? iconic. ✨

---

🌸 SYNOPSIS 🌸

sercomp [OPTION]??? FILE

yeah that's the whole vibe. options, a mystery ???, and a file. periodt.

---

💖 DESCRIPTION 💖

sercomp is an experimental Coq compiler with serialization and deserialization support. that's it, that's the whole personality. it takes your Coq vernacular, and it can turn it into a serialized form, and it can turn that serialized form back into something real. no cap. 💅

---

✨ USAGE ✨

okay so here are the canonical little rituals, and you're gonna want to copy these exactly, bestie.

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. (yes, the webpage. go look. iykyk.)

---

🎀 ARGUMENTS 🎀

• FILE (required) — the input file. mandatory. you cannot skip it, she's the main character. 👑

---

💅 OPTIONS 💅

• --async=COQTOP — turn on async support using the Coq binary COQTOP. (experimental!) 🔥
• --async-workers=VAL (absent=3) — max number of async workers. defaults to 3, so 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. the "turn the lights on" option. 🔍
• --disallow-sprop — forbid using the proof irrelevant SProp sort. (it's allowed by default, so this is you being strict.)
• --error-recovery — enable Coq's error recovery inside tactics and commands. she gets back up. 💪
• --exn_on_opaque — [debug option] raise an exception on non-serializeble terms. (yes, "serializeble". that's the original spelling. we keep the facts, bestie.) 😭
• -I DIR, --ml-include-path=DIR — include DIR in the default loadpath, for locating ML files. 📁
• --impredicative-set — enable the 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. pick your fighter. 🥊
• --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
  • 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)
  • 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). living dangerously, we love that for you.
• -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. the "who even am i" button. ⭐

---

🍓 EXIT STATUS 🍓

sercomp exits with:

• 0 — on success. slay. 💖
• 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. go read it, bestie, it's the director's cut. 📖

---

and that's the whole page! 💜 this one's sercomp, from June 2025, and yes the man page literally just calls itself sercomp for the source/version, no fancy build string, no drama. mwah. 💋