A tool for writing definitions of programming languages and calculi

by Peter Sewell, Francesco Zappa Nardelli, and Scott Owens.

Ott is now available from github, and as an opam package.

We no longer provide non-github tarballs or a Windows distribution.

If you have OPAM installed on your system, opam install ott will install the latest Ott version. The Emacs mode will be in `opam config var prefix`/share/emacs/site-lisp, and documentation in `opam config var prefix`/doc/ott.

To install the Ott auxiliary files for Coq, first activate the coq-released OPAM repository:

opam repo add coq-released https://coq.inria.fr/opam/released

and then run opam install coq-ott.

Ott depends on OCaml version 4.00.0 or later. It builds with (at least) OCaml 4.02.3.

The command make (make world) builds the ott binary in the bin/ subdirectory.

This will compile Ott using ocamlopt. To force it to compile with ocamlc (which may give significantly slower execution of Ott), do make world.byt.

To build the Ott auxiliary files for Coq, go to the coq/ subdirectory and run make. To install the resulting files in Coq's user-contrib, run make install.

Ott runs as a command-line tool. Executing bin/ott shows the usage and options. To run Ott on the test file tests/test10.ott, generating LaTeX in test10.tex and Coq in test10.v, type:

bin/ott -i tests/test10.ott -o test10.tex -o test10.v

Isabelle, HOL, and Lem can be generated with options -o test10.thy, -o test10Script.sml, and -o test10.lem, respectively.

The Makefile has various sample targets, make tests/test10.out, make test7, etc. Typically they generate:

from files test10.ott, test8.ott, etc., in tests/.

• in the Ott github built_doc directory, or
• here (html)

The file emacs/ott-mode.el defines a very simple Emacs mode for syntax highlighting of Ott source files. It can be used by, for example, adding the following to your .emacs file, replacing PATH by a path to your Ott Emacs directory.

(setq load-path (cons (expand-file-name "PATH") load-path))
(require 'ott-mode)

There is a plugin for VSCode, which features syntax highlighting and inline error reporting.

• cl-ott-announce announcement mailing list
• cl-ott-discuss discussion mailing list

• here

The ocamlgraph library is distributed under the LGPL (from http://www.lri.fr/~filliatr/ftp/ocamlgraph/); we include a snapshot for convenience. For its authorship and copyright information see the files therein.

All other files are distributed under the BSD-style licence in LICENCE.