CAFEOBJ(1)

💖 CAFEOBJ(1) — the cafeobj manual, bestie edition 💖

okay so this is cafeobj, from the General Commands Manual section of your local man pages, and honestly? she's iconic. let's get into it 🎀

---

✨ NAME ✨

cafeobj — algebraic specification and programming language

🌸 SYNOPSIS 🌸

cafeobj [OPTION]... [FILES]...

🦋 DESCRIPTION 🦋

Starts the CafeOBJ interpreter. that's the whole vibe, she boots up and she's ready 💅

CafeOBJ is a most advanced formal specification language, and the way she got there is by inheriting a whole stack of advanced features from OBJ (or, to be exact, OBJ3) algebraic specification language. the receipts: flexible mix-fix syntax, a powerful and clear typing system with ordered sorts, parameteric modules and views for instantiating the parameters, and module expressions, etc. all of it, inherited, no cap ✨

CafeOBJ is a language for writing formal (i.e. mathematical) specifications of models for wide varieties of software and systems, and for verifying properties of them. she implements equational logic by rewriting, which means she can also be used as a powerful interactive theorem proving system. specifiers can write proof scores in CafeOBJ too, and do proofs by executing those proof scores. it's giving math but make it executable 😭

CafeOBJ has state-of-art rigorous logical semantics based on institutions. the CafeOBJ cube shows the structure of the various logics underlying the combination of the various paradigms implemented by the language. proof scores in CafeOBJ are also based on institution based rigorous semantics, and can be constructed using a complete set of proof rules. the rigor? immaculate. the cube? cube-ing 👑

---

🔥 OPTIONS 🔥

okay bestie, there are two classes of options here and you need to know which class you're in before you start flinging flags around. the first class is for the cafeobj wrapper script, and it lets you pick the underlying Common Lisp interpreter and adjust search path parameters. 💖

• -engine NAME — selects the underlying common lisp engine. if you don't give this one, the first one selected during build time is used. (default behavior, she picks for you 🫶)
• -list-engines — lists all available common lisp engines. window shopping, but for lisp 🛍️
• -wrapper-libpath PATH — sets the path where memory dumps of the lisp interpreters are found
• -wrapper-sharepath PATH — sets the path where CafeOBJ initialization files are searched

---

then the second set of options, and these ones are directed at the CafeOBJ interpreter directly. no middleman 🧚

• -help — print a help message
• -q — do not load user's initialization file
• -batch — run in batch mode
• -p PATH — gives the standard prelude file defining modules
• +p PATH — load additional prelude file
• -l DIR-LIST — set list of pathnames for module search path, separated by colons
• +l DIR-LIST — adds a list of pathname for module search path
• FILES — files that are loaded at startup time in order.

💀 quick reminder that -p and +p are not the same thing and neither are -l and +l. one sets, one adds. she is particular about this. do not mix them up, i'm begging 🙈

---

🌈 AUTHOR 🌈

Toshimi Sawada and Norbert Preining. Contact: info@cafeobj.org

💜 COPYRIGHT 💜

Copyright © 2000-2014 Toshima Sawada, Norbert Preining. License BSD.

THIS SOFTWARE IS SUPPLIED COMPLETELY "AS IS". CafeOBJ is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANT-ABILITY of FITNESS FOR A PARTICULAR PURPOSE.

😭 yes the all-caps is doing a lot but it's real and it matters — no warranty, none, zero, she said what she said. "AS IS" is the whole mood. respect the terms bestie 🫶

---

and that's the page!! this one came out of the User Manuals collection, dated September 2014, filed under the name CAFEOBJ with the number 1 because that's just how the section works. ok bye, go write some proof scores, ily 💖✨🎀