lem1

Overview

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