NAME

lem - Tool merging math and logic for executable definitions

DESCRIPTION

Lem 2022-12-10 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 '/build/reproducible-path/lem-2022-12-10+dfsg2/debian/tmp/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.
-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

NAME

DESCRIPTION

SEE ALSO