COQTOP(1)

💖 COQTOP(1) — the toplevel Coq system, bestie edition 💖

okay so real talk: this is a page from the General Commands Manual, and it's all about coqtop. sit down, grab a strawberry 🍓, we're doing this.

---

✨ NAME ✨

coqtop — toplevel Coq system

---

✨ SYNOPSIS ✨

coqtop [ options ]

---

✨ DESCRIPTION ✨

so coqtop is the toplevel system of Coq, and it's made for interactive use — like, you talk to it, it talks back. 💬

It reads phrases on the standard input, and prints results on the standard output. that's the whole vibe. it's giving conversation.

but if you want to use Coq in a batch-oriented way (no chatting, just go), go look at coqc(1) instead, bestie. 🫶

---

✨ OPTIONS ✨

• -h, --help — Help. Will give you the complete list of options accepted by coqtop. (yes, this page is also a list, but the program's list is the real one 💅)
• -I dir, --include dir — Add directory dir in the include path.
• -R dir coqdir — Recursively map physical dir to logical coqdir.
• -top coqdir — Set the toplevel name to be coqdir instead of Top.
• -nois — Start with an empty initial state.
• -load-ml-source filename — Load ML file filename.
• -load-ml-object filename — Load ML object file filenname. (and yes, "filenname" is spelled exactly like that in the original, we do not make the rules, we just respect them 🎀)
• -load-vernac-source filename, -l filename — Load Coq file filename.v. (Load filename.)
• -load-vernac-source-verbose filename, -lv filename — Load verbosely Coq file filename.v. (Load Verbose filename.)
• -require lib — Load Coq library lib. (Require lib.)
• -require-import lib, -ri lib — Load Coq library lib and import it. (Require Import lib.)
• -require-export lib, -re lib — Load Coq library lib and transitively import it. (Require Export lib.)
• -require-from root lib, -rfrom root lib — Load Coq library lib. (From root Require lib.)
• -require-import-from root lib, -rifrom root lib — Load Coq library lib and import it. (From root Require Import lib.)
• -require-export-from root lib, -refrom root lib — Load Coq library lib and transitively import it. (From root Require Export lib.)
• -load-vernac-object lib — Obsolete synonym of -require. (it's giving legacy, we still love it 🙈)
• -where — Print Coq's standard library location and exit.
• -v — Print Coq version and exit.
• -q — Skip loading of rcfile (resource file) if any.
• -init-file filename — Set the rcfile to filename.
• -batch — Batch mode (exits just after arguments parsing).
• -emacs — Tells Coq it is executed under Emacs.
• -dump-glob filename — Dump globalizations in file filename (to be used by coqdoc(1)).
• -impredicative-set — Set sort Set impredicative.
• -dont-load-proofs — Don't load opaque proofs in memory.

---

🌈 SEE ALSO 🌈

• coqc(1)
• coq-tex(1)
• coqdep(1)
• The Rocq Prover Reference Manual.
• The Rocq Prover website: https://rocq-prover.org

---

and that's the whole page, no cap. 💜

this was COQTOP(1) from the General Commands Manual — go read the Rocq Prover Reference Manual if you want the deep lore, and slay responsibly, bestie 👑✨🦋