-
Notifications
You must be signed in to change notification settings - Fork 15
/
opam
46 lines (45 loc) · 1.39 KB
/
opam
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
opam-version: "2.0"
name: "lem"
version: "2022-12-10"
maintainer: "Lem Devs <[email protected]>"
authors: [
"Dominic Mulligan"
"Francesco Zappa Nardelli"
"Gabriel Kerneis"
"Kathy Gray"
"Peter Boehm"
"Peter Sewell"
"Scott Owens"
"Thomas Tuerk"
"Brian Campbell"
"Shaked Flur"
"Thomas Bauereiss"
"Stephen Kell"
"Thomas Williams"
"Lars Hupel"
"Basile Clement"
]
homepage: "http://www.cl.cam.ac.uk/~pes20/lem/"
bug-reports: "https://github.com/rems-project/lem/issues"
license: ["BSD-3-Clause" "LGPL-2.1-or-later"]
dev-repo: "git+https://github.com/rems-project/lem.git"
build: [make "INSTALL_DIR=%{prefix}%"]
install: [make "INSTALL_DIR=%{prefix}%" "install"]
remove: [make "INSTALL_DIR=%{prefix}%" "uninstall"]
depends: [
"ocaml" {>= "4.07.0"}
"ocamlfind" {build & >= "1.5.1"}
"ocamlbuild" {build}
"conf-findutils" {build}
"zarith" {>= "1.4"}
"num"
]
synopsis: "Lem is a tool for lightweight executable mathematics"
description: """
Lem is a tool for lightweight executable mathematics, for writing,
managing, and publishing large-scale portable semantic definitions,
with export to LaTeX, executable code (currently OCaml) and
interactive theorem provers (currently Coq, HOL4, and Isabelle/HOL).
It is also intended as an intermediate language for generating
definitions from domain-specific tools, and for porting definitions
between interactive theorem proving systems."""