package ott
A tool for writing definitions of programming languages and calculi
Install
Dune Dependency
Authors
Maintainers
Sources
0.34.tar.gz
sha512=371b59c0dc35207f8e85a939f03ae63fc654df50540ed5e656c5a40c5062ebfdfb1e02cfd499074f9d0b43afc165606b57dec4c96a4ca44ee91d1c1dcfa4deaf
Description
Ott 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. It generates 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. 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.
Published: 31 Dec 2024
Dependencies (2)
- ocamlgraph
-
ocaml
>= "4.07.0"
Dev Dependencies (4)
-
menhir
>= "20151112" & with-test -
pprint
with-test -
ocamlfind
build | with-test -
ocamlbuild
with-test
Conflicts
None
On This Page