SERTOK(1)

💅 NAME 💅

okay bestie, so this whole page is the manual page for sertok — section 1, User Commands, the whole vibe. no preamble needed, let's get into it ✨

🦋 DESCRIPTION 🦋

💖 NAME 💖

sertok — it's the sertok Coq tokenizer. that's the name. periodt.

🌸 SYNOPSIS 🌸

sertok [OPTION]??? FILE

✨ DESCRIPTION ✨

Experimental Coq tokenizer. (yes bestie, experimental — we'll get to that, stay with me 🙈)

🎀 USAGE 🎀

so if you wanna serialize tokens in the file fs/fun.v with the logical path Funs, you literally just do this:

sertok -Q fs,Funs fs/fun.v > fs/fun.sexp

and boom 💥 that's it. for more info, go check out the documentation on the project's website, iykyk.

🫶 ARGUMENTS 🫶

• FILE (required) — the input file. you GOTTA hand it one, no cap.

👑 OPTIONS 👑

• --async=COQTOP — turns on async support using the Coq binary COQTOP. (experimental, bestie — so, you know.)
• --async-workers=VAL (absent=3) — the max number of async workers. three is the default, iconic.
• --coqlib=COQPATH (absent=/usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq) — loads Coq.Init.Prelude from COQPATH; plugins/ and theories/ should be living right there, fr fr.
• --debug — turns on debug mode for Coq. 🐛
• --disallow-sprop — forbids using the proof irrelevant SProp sort. (it's allowed by default, fyi.)
• --error-recovery — enables Coq's error recovery inside tactics and commands. it's giving resilience 💪
• --exn_on_opaque — [debug option] raise an exception on non-serializeble terms. yes it's spelled that way in the original, we don't touch it, we don't fix it, we respect it 🫡
• -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.)
• --omit_att — [debug option] omit attribute nodes.
• --omit_env — [debug option] turn enviroments into abstract objects. (yes, "enviroments", the typo is canon, we keep it 💅)
• --omit_loc — [debug option] shorten location printing.
• --printer=VAL (absent=sertop) — pick 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.) like, very. tread carefully bestie 😭
• -R DIR,LP, --rec-load-path=DIR,LP — bind a logical loadpath LP to a directory DIR and implicitly open its namespace. the overachiever of the -Q family, honestly 👑

---

🌈 COMMON OPTIONS 🌈

• --help[=FMT] (default=auto) — show this help in format FMT. FMT has to 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. (so like, if your terminal is being weird, it keeps it simple 🫶)
• --version — show version information. slay.

---

💀 EXIT STATUS 💀

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

info sertok

should give you access to the complete manual. 📖✨

---

and that's the whole page bestie — this one's sertok, dated June 2025, and you just read the SERTOK(1) man page. go tokenize something, you absolute icon 👑💖🦋