SERNAME(1)

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

💖 NAME 💖

okay so bestie, meet sername — it's the manual page for sername, and yes the tool is also literally called sername. same name, no confusion, we love a consistent queen 💅

✨ SYNOPSIS ✨

sername [OPTION]??? FILE

(yes that ??? is really in there, she's mysterious like that 🌸)

🦋 DESCRIPTION 🦋

🎀 sername — the sername Coq tool 🎀

It's the experimental Coq name serializer. experimental!! she's in her lab era 🔬✨

🌸 USAGE 🌸

Say you wanna serialize the names listed in names.txt inside the module Funs.mod — you'd run, like, this exact thing:

sername -Q fs,Funs --require-lib=Funs.mod names.txt

and if you want the whole lore, the project's webpage has the full documentation. go read it, it's giving scholarly 👑

🌈 ARGUMENTS 🌈

  • FILE (required) — the input file. you literally cannot skip this one bestie, it's required, no cap 🫶

💅 OPTIONS 💅

  • --async=COQTOP — turn on async support using the Coq binary COQTOP. lowkey experimental, just so you know 🧚
  • --async-workers=VAL — max number of async workers. (absent = 3)
  • --body — prints the bodies of constrs. show us the bodiesss 👀
  • --coqlib=COQPATH — load Coq.Init.Prelude from COQPATH; plugins/ and theories/ should live there. (absent = /usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq)
  • --de-bruijn — print constrs with de Bruijn indices. fancy math girlie behaviour ✨
  • --debug — enable debug mode for Coq. we're going in deep 🔍
  • --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 recovers, she heals 🌱
  • --exn_on_opaque — [debug option] raise an exception on non-serializeble terms. screaming, crying, throwing up 😭
  • -I DIR, --ml-include-path=DIR — include DIR in the default loadpath, for locating ML files.
  • --impredicative-set — enable Coq's -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. (that's the original spelling, bestie, I don't make the rules 🙈)
  • --omit_loc — [debug option] shorten location printing.
  • --printer=VAL — pick your printer, 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. (absent = sertop) — choose your fighter 🎀
  • -Q DIR,LP, --load-path=DIR,LP — bind a logical loadpath LP to a directory DIR.
  • --quick — skip checking opaque proofs (very experimental). very experimental. she's reckless, we stan 🔥
  • -R DIR,LP, --rec-load-path=DIR,LP — bind a logical loadpath LP to a directory DIR and implicitly open its namespace. the extra-commitment version of -Q 💜
  • --require-lib=VAL — the Coq module to require.
  • --str-pp — pretty-print constr strings. pretty privilege, but for strings ✨

👑 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 if your terminal's being a hater, she adapts 🫶)
  • --version — show version information. drop the number bestie 📢

💀 EXIT STATUS 💀

sername exits with:

  1. 0 — on success. slay, we ate 🎉
  2. 123 — on indiscriminate errors reported on standard error.
  3. 124 — on command line parsing errors.
  4. 125 — on unexpected internal errors (bugs).
not me memorising these like they're my star signs 💅 123, 124, 125 — the cursed little trio fr fr

🍓 SEE ALSO 🍓

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

info sername

should give you access to the complete manual. iykyk, go read the real thing 📚✨

and that's the whole page!! 🦋 this little beauty is sername, dated June 2025, and it lives in the SERNAME(1) section of the manual — periodt, no cap, take care of her 💖🎀🫶

📦 where this page comes from