Skip to content

Latest commit

 

History

History
441 lines (348 loc) · 17.4 KB

README.md

File metadata and controls

441 lines (348 loc) · 17.4 KB
Raw

Ott

Docker CI

Ott is a tool for writing definitions of programming languages and calculi. It takes as input a definition of a language syntax and semantics, in a concise and readable ASCII notation that is close to what one would write in informal mathematics. With appropriate annotations, it can then generate output:

  • a LaTeX source file that defines commands to build a typeset version of the definition;
  • a Coq version of the definition;
  • a HOL version of the definition;
  • an Isabelle/HOL version of the definition;
  • a Lem version of the definition;
  • an OCaml version of the syntax of the definition; and
  • (experimental) a menhir parser and crude pretty printer for the syntax.

Additionally, it can be run as a filter, taking a LaTeX/Coq/Isabelle/HOL/Lem/OCaml source file with embedded (symbolic) terms of the defined language, parsing them and replacing them by typeset terms.

Most simply, Ott can be used to aid informal LaTeX mathematics. Here it permits the definition, and terms within proofs and exposition, to be written in a clear, editable, ASCII notation, without LaTeX noise. It generates good-quality typeset output. By parsing (and so sort-checking) this input, it quickly catches a range of simple errors, e.g. inconsistent use of judgement forms or metavariable naming conventions.

That same input can be used to generate formal definitions, for Coq, HOL, Isabelle, and Lem. It should thereby enable a smooth transition between use of informal and formal mathematics. Additionally, the tool can automatically generate definitions of functions for free variables, single and multiple substitutions, subgrammar checks (e.g. for value subgrammars), and binding auxiliary functions. At present only a fully concrete representation of binding, without quotienting by alpha equivalence, is fully supported. An experimental backend generates a locally-nameless representation of terms for a subset of the Ott metalanguage: details can be found at http://moscova.inria.fr/~zappa/projects/ln_ott.

The distribution includes several examples, in varying levels of completeness: untyped and simply typed lambda-calculus, a calculus with ML polymorphism, the POPLmark Fsub with and without records, an ML module system taken from (Leroy, JFP 1996) and equipped with an operational semantics, and LJ, a lightweight Java fragment. More substantially, Ott has been used for work on iJAM and LJAM, Java Module Systems, by Rok Strnisa, and semantics for OCaml light, by Scott Owens.

As of 2024, Ott remains in continuous use.

Documentation

Papers

People

Ott has been principally developed by Peter Sewell, Francesco Zappa Nardelli, and Scott Owens, with contributions from many others including Joey Eremondi, Hannes Mehnert, Karl Palmskog, Matthew Parkinson, Thibaut Perami, Gilles Peskine, Alastair Reid, Tom Ridge, Susmit Sarkar, Rok Strnisa, Viktor Vafeiadis.

To install and build

Ott is available as an opam package and a github repo.

With opam (released version)

First, ensure you have opam (the OCaml package manager) installed, version 2.0 or greater (opam 1 versions of ott are no longer supported). You can use your system's package manager e.g. sudo apt-get install opam (e.g. on Ubuntu 20.04) or follow the instructions from the opam website. On older Ubuntu versions you will not be able to use their package manager's opam 1 version, and will need to install opam 2 following the instructions on the opam website.

Then 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.

If you want to use Ott with the Coq proof assistant, 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.

With opam (github checkout)

In the checkout directory, run opam pin add ott ..

To rebuild and reinstall after local changes, run opam upgrade --working-dir ott (or opam upgrade -w ott).

Without opam

Ott depends on OCaml version 4.07.0 or later and the ocamlgraph package. It builds with (at least) OCaml 4.07.0 and 4.14.0, and ocamlgraph 1.8.8.

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

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/.

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

Bug Tracker

  • Please now use the github issue tracker (though our resources for fixing issues are very limited)
  • The previous issue tracker is here

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

Examples

The following LaTeX, Coq, HOL, and Isabelle files, except the proof scripts, are all automatically generated from the Ott sources.

System Rules Ott sources Latex Typeset Dot Coq HOL Isabelle
Defn Proof Defn Proof Defn Proof
Untyped CBV lambda 3 test10.ott test10.tex (ps) test10.v test10Script.sml test10.thy
Simply typed CBV lambda 6 test10st.ott test10st.tex (ps) test10st.v test10st_metatheory.v test10stScript.sml test10st_metatheoryScript.sml test10st.thy test10st_metatheory.thy
ML polymorphism 22 test8.ott test8.tex (ps) test8.v test8Script.sml test8.thy
TAPL roughly-full-simple 63 (sources) (ps) (Coq (including records)) (HOL) (script) (Isabelle) (script)
POPLmark Fsub (*) 48 (sources) (latex) (pdf)   (ps)
Leroy JFP96 module system (*) 67 leroy-jfp96.ott (latex) (ps) (HOL)
LJ: Lightweight Java 85 (sources) (pdf) (Isabelle) (zip)
LJAM: Java Module System 163 (sources) (pdf) (Isabelle) (zip)
OCaml light 310 (sources) (ps) (ps) (Coq) (HOL) (scripts) (Isabelle)



(*) These systems would need explicit alpha conversion in the rules to capture the intended semantics using the fully concrete representation.

Copyright information

Files are distributed under the BSD-style licence in LICENCE.