|
| 1 | +opam-version: "2.0" |
| 2 | +maintainer: "Thibaut Pérami < [email protected]>" |
| 3 | +authors: ["Peter Sewell" "Francesco Zappa Nardelli" "Scott Owens"] |
| 4 | +license: "BSD-3-Clause" |
| 5 | +homepage: "http://www.cl.cam.ac.uk/~pes20/ott/" |
| 6 | +bug-reports: "https://github.com/ott-lang/ott/issues" |
| 7 | +depends: [ |
| 8 | + "ocaml" {>= "4.07.0"} |
| 9 | + "ocamlbuild" {with-test} |
| 10 | + "ocamlfind" {build | with-test} |
| 11 | + "ocamlgraph" |
| 12 | + "pprint" {with-test} |
| 13 | + "menhir" {>= "20151112" & with-test} |
| 14 | +] |
| 15 | +build: [ |
| 16 | + [make "world"] { ocaml:native } |
| 17 | + [make "world.byt"] { !ocaml:native } |
| 18 | + ["rm" "src/ott"] {os = "win32"} |
| 19 | + ["cp" "src/ott.opt" "src/ott"] {os = "win32" & ocaml:native} |
| 20 | + ["cp" "src/ott.byte" "src/ott"] {os = "win32" & !ocaml:native} |
| 21 | + [make "ott.install"] |
| 22 | +] |
| 23 | +run-test: [ |
| 24 | + [make "-C" "tests/menhir_tests/test_if"] |
| 25 | + [make "-C" "tests/menhir_tests/test10menhir"] |
| 26 | + [make "-C" "tests/menhir_tests/test10menhir_with_aux_args"] |
| 27 | + [make "-C" "tests/menhir_tests/test10menhir_with_aux_rules"] |
| 28 | +] |
| 29 | +dev-repo: "git+https://github.com/ott-lang/ott.git" |
| 30 | +synopsis: "A tool for writing definitions of programming languages and calculi" |
| 31 | +description: """ |
| 32 | +Ott takes as input a definition of a language syntax and semantics, in a |
| 33 | +concise and readable ASCII notation that is close to what one would write in |
| 34 | +informal mathematics. It generates output: |
| 35 | +- a LaTeX source file that defines commands to build a typeset version of the definition; |
| 36 | +- a Coq version of the definition; |
| 37 | +- a HOL version of the definition; |
| 38 | +- an Isabelle/HOL version of the definition; |
| 39 | +- a Lem version of the definition; |
| 40 | +- an OCaml version of the syntax of the definition. |
| 41 | +Additionally, it can be run as a filter, taking a |
| 42 | +LaTeX/Coq/Isabelle/HOL/Lem/OCaml source file |
| 43 | +with embedded (symbolic) terms of the defined language, parsing them and |
| 44 | +replacing them by typeset terms. |
| 45 | +""" |
| 46 | +url { |
| 47 | + src: "https://github.com/ott-lang/ott/archive/0.34.tar.gz" |
| 48 | + checksum: "sha512=371b59c0dc35207f8e85a939f03ae63fc654df50540ed5e656c5a40c5062ebfdfb1e02cfd499074f9d0b43afc165606b57dec4c96a4ca44ee91d1c1dcfa4deaf" |
| 49 | +} |
0 commit comments