table of contents
OTT(1) | User Commands | OTT(1) |
NAME¶
Ott - manual page for Ott version 0.32 distribution of Wed 9 Mar 16:05:28 GMT 2022
DESCRIPTION¶
Ott version 0.32 distribution of Wed 9 Mar 16:05:28 GMT 2022
usage: ott <options> <filename1> .. <filenamen>
- (use "OCAMLRUNPARAM=p
- ott ..." to show the ocamlyacc trace)
- (ott <options> <filename1> .. <filenamen>
- is equivalent to
- ott -i <filename1> .. -i <filenamen> <options>)
- -i <filename>
- Input file (can be used multiple times)
- -o <filename>
- Output file (can be used multiple times)
- -writesys <filename>
- Output system definition
- -readsys <filename>
- Input system definition
- -tex_filter <src><dst>
- Files to TeX filter
- -coq_filter <src><dst>
- Files to Coq filter
- -hol_filter <src><dst>
- Files to HOL filter
- -lem_filter <src><dst>
- Files to HOL filter
- -isa_filter <src><dst>
- Files to Isabelle filter
- -ocaml_filter <src><dst>
- Files to OCaml filter
- -merge <false>
- merge grammar and definition rules
- -parse <string>
- Test parse symterm,eg ":nontermroot: term"
- -fast_parse <false>
- do not parse :rulename: pseudoterminals
- -signal_parse_errors <false>
- return >0 if there are bad defns
- -picky_multiple_parses <false>
- Picky about multiple parses
- -quotient_rules <true>
- Quotient rules, as per {{ quotient-with ntr }} homs
- -generate_aux_rules <true>
- Generate auxiliary rules or constructor arguments from {{ aux ... }} homs
- -aux_style_rules <true>
- Auxiliary rules (true) vs constructor arguments (false)
- -output_source_locations <0>
- Include source location info in output (0=none, 1=drules, 2=grammar+drules)
- -colour <true>
- Use (vt220) colour for ASCII pretty print
- -show_sort <false>
- Show ASCII pretty print of syntax
- -show_defns <false>
- Show ASCII pretty print defns
- -tex_show_meta <true>
- Include meta prods and rules in TeX output
- -tex_show_categories <false>
- Signal production flags in TeX output
- -tex_suppress_category <[]>
- Suppress productions and rules with this category in TeX output
- -tex_suppress_ntr <[]>
- Suppress nonterminal root in TeX output
- -tex_colour <true>
- Colour parse errors in TeX output
- -tex_wrap <true>
- Wrap TeX output in document pre/postamble
- -tex_name_prefix <string>
- Prefix for tex commands (default "ott")
- -isabelle_primrec <true>
- Use "primrec" instead of "fun" for functions
- -isabelle_inductive <true>
- Use "inductive" instead of "inductive_set" for relations
- -isa_syntax <false>
- Use fancy syntax in Isabelle output
- -isa_generate_lemmas <false>
- Lemmas for collapsed functions in Isabelle
- -coq_avoid <1>
- coq type-name avoidance (0=nothing, 1=avoid, 2=secondaryify)
- -coq_expand_list_types <false>
- Expand list types in Coq output
- -coq_lngen <false>
- lngen compatibility
- -coq_names_in_rules <true>
- Copy user names in rule definitions
- -coq_use_filter_fn <false>
- Use list_filter instead of list_minus2 in substitutions
- -ocaml_include_terminals <false>
- Include terminals in OCaml output (experimental!)
- -ocaml_pp
- <target.ml filename> generate OCaml AST pretty printer files (experimental!) (also included in .mly target)
- -ocaml_pp_ast_module
- override default OCaml module name for AST module (experimental!)
- -ocaml_pp_json <false>
- Include JSON output in pretty printer (experimental)
- -pp_grammar
- (debug) print term grammar
- -dot <filename>
- (debug) dot graph of syntax dependencies
- -alltt <filename>
- (debug) alltt output of single source file
- -sort <true>
- (debug) do topological sort
- -process_defns <true>
- (debug) process inductive reln definitions
- -showraw <false>
- (debug) show raw grammar
- -ugly <false>
- (debug) use ugly ASCII output
- -no_rbcatn <true>
- (debug) remove relevant bind clauses
- -lem_debug
- (debug) print lem debug locations
- -help
- Display this list of options
- --help
- Display this list of options
February 2023 | Ott version 0.32 distribution of Wed 9 Mar 16:05:28 GMT 2022 |