Ott is a tool for writing definitions of programming languages and calculi
Switch branches/tags
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
aux/y2l import manual sources and build machinery from svn Nov 24, 2016
built_doc update manual with today's date; document manual build in doc/Makefile Apr 24, 2018
coq switch from Set to Type sort in all Coq library functions Apr 25, 2018
doc release 0.28; remove orphaned doc built products in doc (now in built… Apr 24, 2018
emacs rename ottmode.el accordingly May 29, 2017
examples custom .gitignore for ocaml_light and tapl examples Apr 27, 2018
hol initial github check-in of Ott release 0.25 Oct 27, 2016
menhir - better handling of parsing/pp for list forms with multiple elements Jun 9, 2017
regression - partial update of user guide Nov 30, 2017
src fix one more Coq deprecation source Apr 27, 2018
tests Add -generate_aux_rules false when generating PDF May 31, 2018
tex add tex file for macros used in -alltt <filename> output Oct 29, 2017
.gitignore Ignore .annot files Jul 17, 2017
LICENCE initial github check-in of Ott release 0.25 Oct 27, 2016
Makefile setup for Jenkins (tmp) Nov 27, 2017
README.md Use improved config Feb 21, 2018
coq-ott.opam Coq library is compatible with Coq 8.8 Apr 24, 2018
ocamlgraph-1.7.tar.gz initial github check-in of Ott release 0.25 Oct 27, 2016
ocamlgraph-safe-string.patch Fix OCamlGraph with safe-string enabled Jul 17, 2017
ott.install adjust ott.install to most recent changes (manual now in built_doc) Apr 25, 2018
ott.opam opam installation via pinning Apr 24, 2018
revision_history.txt release 0.28; remove orphaned doc built products in doc (now in built… Apr 24, 2018

README.md

Ott

A tool for writing definitions of programming languages and calculi

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

Repository and Package

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

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

Directory contents

directory description
aux/ auxiliary code (y2l) used to build the user guide
bin/ the Ott binary
built_doc/ the user guide, in html, pdf, and ps
coq/ auxiliary files for Coq
doc/ the user guide sources
emacs/ an Ott Emacs mode
examples/ some larger example Ott files
tex/ auxiliary files for LaTeX
hol/ auxiliary files for HOL
menhir/ auxiliary files for menhir
ocamlgraph-1.7.tar.gz a copy of the ocamlgraph library
regression/ regression-test machinery
tests/ various small example Ott files
src/ the (OCaml) Ott sources
Makefile a Makefile for the examples
LICENCE the BSD-style licence terms
README.md this file (Section 2 of the user guide)
revisionhistory.txt the revision history

To build

With OPAM

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.

Without OPAM

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.

To run

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:

filename description
out.tex LaTeX source for a definition
out.ps the postscript built from that
out.v Coq source
outScript.sml HOL source
out.thy Isabelle source

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

Manual

Editor Plugins

Emacs mode

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)

For installations using OPAM on *nix systems, it is sufficient to use the following code, which will call opam config var prefix at load-time.

(setq opam-share (substring (shell-command-to-string "opam config var share") 0 -1))
(add-to-list 'load-path (concat opam-share "/emacs/site-lisp"))
(require 'ott-mode)

Visual Studio Code

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

Mailing lists

Web page with examples

Copyright information

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.