NAME
Ott - manual page for Ott version 0.34 distribution of Mon Dec 30 10:12:45 GMT 2024
DESCRIPTION
Ott version 0.34 distribution of Mon Dec 30 10:12:45 GMT 2024
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