Ubuntu Manpage: lem - Tool merging math and logic for executable definitions

Provided by: lem_2025-03-13+dfsg-1build1_amd64

NAME

       lem - Tool merging math and logic for executable definitions

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
              '/build/lem-sZAePu/lem-2025-03-13+dfsg/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.

       -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

NAME

DESCRIPTION

SEE ALSO