LEM(1)

👑 NAME 👑

so this is lem(1) — a User Commands page, bestie — and it's the tool that merges math and logic for executable definitions. that's the whole personality. math + logic = executable ✨

---

🎀 DESCRIPTION 🎀

okay so here's the 2026-05-01 example usage, verbatim, because we know how to read:

lem -hol -ocaml test.lem

yeah. one command, two backends, main character energy 💅

and now literally every single flag, no skips, no "oh you can figure it out":

• -ocaml — generate OCaml
• -tex — generate LaTeX for each module separately
• -tex_all — generate LaTeX in a single file
• -html — generate Html
• -hol — generate HOL
• -isa — generate Isabelle
• -coq — generate Coq
• -lem — generate Lem output after simple transformations
• -ident — generate input on stdout
• -lib — add a library path, on top of the standard library at /build/lem-3IxgiG/lem-2026-05-01+dfsg/debian/tmp/bin/library. wanna change that one instead? set the LEMLIB environment variable, babe. dirs in the library path can optionally be associated with Isabelle session names, e.g. -lib MyLib=path/to/mylib. the standard library is associated with the session name LEM by default. 🦋
• -no_dep_reorder — prohibit reordering modules given to lem as explicit arguments in order during dependency resolution
• -outdir — the output directory (the default is the dir the files reside in)
• -i — treat the file as input only and generate no output for it
• -only_changed_output — generate only output files, whose content really changed compared to the existing file
• -only_auxiliary — generate only auxiliary output files
• -auxiliary_level {none|auto|all} — generate no (none) auxiliary-information, only auxiliaries that can be handled automatically (auto) or all (all) auxiliary information
• -debug — print a backtrace for all errors (heads up: lem needs to be compiled in debug mode for this 💀)
• -cerberus_pp — special case HTML and LaTeX output for Cerberus Ail and Core
• -print_env — print the environment signature on stdout
• -add_loc_annots — add location annotations to the output
• -isa_path_imports — use paths in Isabelle import statements instead of session-qualified imports
• -use_datatype_record — use datatype_record instead of record in Isabelle output
• -v — print version
• -ident_pat_compile — activates pattern compilation for the identity backend. this is used for debugging, bestie
• -ident_dict_passing — activates dictionary passing transformations for the identity backend. also literally just for debugging
• -tex_suppress_target_names — prints target-specific let-bindings as normal let bindings in the TeX backend
• -tex_include_libraries — include libraries in the TeX backend
• -hol_remove_matches — try to remove toplevel matches in HOL4 output
• -prover_remove_failwith — remove failwith branches in match statements in the prover backends
• -suppress_renaming — suppresses Lem's renaming facilities
• -tex_all_force_library_output — force library output with tex_all
• -report_default_instance_invocation — reports the name of any default instance invoked at a given type
• -no_lifting_toplevel_match_for <type> — Do not move cases over the given type to toplevel function case splits
• -wl {ign|warn|verb|err} — warning level of all warnings

and then the whole warning-level girl gang, each with its own {ign|warn|verb|err} {ign|warn|verb|err} set:

• -wl_gen {ign|warn|verb|err} — warning level of miscellaneous warnings (default warn)
• -wl_amb_code {ign|warn|verb|err} — warning level of ambiguous code (default warn)
• -wl_auto_import {ign|warn|verb|err} — warning level of automatically imported modules (default ign)
• -wl_comp_message {ign|warn|verb|err} — warning level of compile messages (default warn)
• -wl_inst_over {ign|warn|verb|err} — warning level of overridden instance declarations (default ign)
• -wl_no_dec_eq {ign|warn|verb|err} — warning level of equality of type is undecidable (default ign)
• -wl_pat_comp {ign|warn|verb|err} — warning level of pattern compilation (default warn)
• -wl_pat_exh {ign|warn|verb|err} — warning level of non-exhaustive pattern matches (default warn)
• -wl_pat_fail {ign|warn|verb|err} — warning level of failed pattern compilation (default warn)
• -wl_pat_red {ign|warn|verb|err} — warning level of redundant patterns (default warn)
• -wl_rename {ign|warn|verb|err} — warning level of automatic renamings (default warn)
• -wl_resort {ign|warn|verb|err} — warning level of resorted record fields and function clauses (default warn)
• -wl_unused_vars {ign|warn|verb|err} — warning level of unused variables (default warn)
• -help — Display this list of options
• --help — Display this list of options

super important: both help flags exist. -help and --help. they do the same thing. we support you either way 🫶

---

🌈 SEE ALSO 🌈

ngl the full documentation for lem lives in a Texinfo manual, which is very vintage-chic of it. if the info and lem programs are properly installed at your site, then this command:

info lem

should give you access to the complete manual. go get your reading in, bestie 📖✨

---

lem 2026-05-01+dfsg, fresh out of July 2026 🎀 that's the version, that's the date, that's the whole sign-off. slay, stay executable, bye 💖🦋👑