COQNATIVE(1)

💖 COQNATIVE(1) 💖

okay bestie, so this is the manual page for coqnative, and it lives in the General Commands Manual section of your friendly neighbourhood Unix docs. grab a snack, we're doing compilers 🍓

---

✨ NAME ✨

coqnative — the native Coq compiler 👑

---

🌸 SYNOPSIS 🌸

coqnative [ options ] filename

---

🦋 DESCRIPTION 🦋

so what does she actually do. coqnative takes vo files and compiles them into binary files — the kind the native compute mechanism of the Coq Proof Assistant uses. that's the whole vibe. if you want the deep lore, go read the Reference Manual, she's got all of it.

exit code tea ☕: she returns with exit code 0 if all the requested tasks succeeded. a non-zero return code means something went wrong. no cap, that's your red flag 🚩

filename is a Coq object file (a .vo) that you want compiled into a native binary. that's the one job. iconic of her honestly.

---

💅 OPTIONS 💅

• -Q dir coqdir — maps a physical dir to a logical coqdir. lowkey a glow-up for your paths ✨
• -R dir coqdir — synonymous to -Q. literally the same thing, just a different name, we love a flexible queen 🫶
• -I dir — ignored, kept around for compatibility. she's just there, existing, doing nothing, and honestly? respect 💀
• -noinit — also ignored, also for compatibility. another ghost in the machine 👻
• -boot — boot mode. yes bestie, we're booting 🥾
• -coqlib dir — overrides the default location of the standard library. moving the whole library, no big deal, main character energy 👑
• -nI dir — adds dir to the set of paths for the native files of the dependencies. dependency errand run, but make it ✨
• -native-output-dir dir — outputs the generated files into dir. your files, your folder, your rules 🎀
• -h, --help — prints the list of options. the classic "help me pls" move, always valid 🙈

---

🌈 SEE ALSO 🌈

• coqtop(1)
• coqc(1)
• coq_makefile(1)
• coqdep(1)
• The Rocq Prover Reference Manual 📖
• The Rocq Prover website: https://rocq-prover.org 🌐

---

⭐ quick reminder bestie: -I and -noinit are ignored, for compatibility. they're decorative. they're accessories. they do nothing and that's on purpose 💅

---

and that's the page!! this was the coqnative(1) manpage, filed under the General Commands Manual, and she said goodbye in the exact same font she said hello in. mwah, go compile something cute 💖🦋✨