lem - Man Page
Convert markdown to HTML
Description
Lem 2025-03-13 example usage: lem -hol -ocaml test.lem
- -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, in addition to the standard library at '/builddir/build/BUILD/lem-2025.03.13-build/BUILDROOT/usr/bin/library'. To change the latter, set the LEMLIB environment variable. Directories in the library path may 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 (lem needs to be compiled in debug mode)
- -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.
- -ident_dict_passing
activates dictionary passing transformations for the identity backend. This is used 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
- -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