OTT(1) User Commands OTT(1)

Ott - manual page for Ott version 0.33 distribution of Mon 16 Jan 15:32:01 GMT 2023

Ott version 0.33 distribution of Mon 16 Jan 15:32:01 GMT 2023

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>)
Input file (can be used multiple times)
Output file (can be used multiple times)
Output system definition
Input system definition
Files to TeX filter
Files to Coq filter
Files to HOL filter
Files to HOL filter
Files to Isabelle filter
Files to OCaml filter
merge grammar and definition rules
Test parse symterm,eg ":nontermroot: term"
do not parse :rulename: pseudoterminals
return >0 if there are bad defns
Picky about multiple parses
Quotient rules, as per {{ quotient-with ntr }} homs
Generate auxiliary rules or constructor arguments from {{ aux ... }} homs
Auxiliary rules (true) vs constructor arguments (false)
Include source location info in output (0=none, 1=drules, 2=grammar+drules)
Use (vt220) colour for ASCII pretty print
Show ASCII pretty print of syntax
Show ASCII pretty print defns
Include meta prods and rules in TeX output
Signal production flags in TeX output
Suppress productions and rules with this category in TeX output
Suppress nonterminal root in TeX output
Colour parse errors in TeX output
Wrap TeX output in document pre/postamble
Prefix for tex commands (default "ott")
Use "primrec" instead of "fun" for functions
Use "inductive" instead of "inductive_set" for relations
Use fancy syntax in Isabelle output
Lemmas for collapsed functions in Isabelle
coq type-name avoidance (0=nothing, 1=avoid, 2=secondaryify)
Expand list types in Coq output
lngen compatibility
Copy user names in rule definitions
Use list_filter instead of list_minus2 in substitutions
Include terminals in OCaml output (experimental!)
<target.ml filename> generate OCaml AST pretty printer files (experimental!) (also included in .mly target)
override default OCaml module name for AST module (experimental!)
Include JSON output in pretty printer (experimental)
(debug) print term grammar
(debug) dot graph of syntax dependencies
(debug) alltt output of single source file
(debug) do topological sort
(debug) process inductive reln definitions
(debug) show raw grammar
(debug) use ugly ASCII output
(debug) remove relevant bind clauses
(debug) print lem debug locations
Display this list of options
Display this list of options
April 2024 Ott version 0.33 distribution of Mon 16 Jan 15:32:01 GMT 2023