this repo has no description
1opam-version: "2.0"
2maintainer: "Hannes Mehnert <hannes@mehnert.org>"
3authors: ["Peter Sewell" "Francesco Zappa Nardelli" "Scott Owens"]
4license: ["BSD-3-Clause" "LGPL-2.1-only"]
5homepage: "http://www.cl.cam.ac.uk/~pes20/ott/"
6bug-reports: "https://github.com/ott-lang/ott/issues"
7depends: [
8 "ocaml" {>= "4.02.0" & < "5.0"}
9]
10build: [make "world"]
11dev-repo: "git+https://github.com/ott-lang/ott.git"
12synopsis: "A tool for writing definitions of programming languages and calculi"
13description: """
14Ott takes as input a definition of a language syntax and semantics, in a
15concise and readable ASCII notation that is close to what one would write in
16informal mathematics. It generates output:
17- a LaTeX source file that defines commands to build a typeset version of the definition;
18- a Coq version of the definition;
19- a HOL version of the definition;
20- an Isabelle/HOL version of the definition;
21- a Lem version of the definition;
22- an OCaml version of the syntax of the definition.
23Additionally, it can be run as a filter, taking a
24LaTeX/Coq/Isabelle/HOL/Lem/OCaml source file
25with embedded (symbolic) terms of the defined language, parsing them and
26replacing them by typeset terms.
27"""
28url {
29 src: "https://github.com/ott-lang/ott/archive/0.29.tar.gz"
30 checksum: [
31 "sha256=42208e47a9dab3ca89da79c4b1063a728532343a4bf5709393bb3d673a9eaeed"
32 "md5=6284382d02bd01ed00fe0e09fe3b777f"
33 ]
34}
35conflicts: [ "pprint" {>= "20220103"} ]