---
name: "ott"
section: "1"
platform: "linux"
package: "ott-tools"
version: "0.34+ds-1+b4"
release: "Debian 13 (Trixie)"
platforms: ["linux"]
url: "https://new.carta.tech/ott"
---

# ott(1)

manual page for Ott version 0.34 distribution of Mon Dec 30 10:12:45 GMT 2024

## 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