-
Notifications
You must be signed in to change notification settings - Fork 1.1k
/
opam
35 lines (35 loc) · 1.07 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
opam-version: "2.0"
homepage: "http://zenon-prover.org/"
dev-repo: "git+https://github.com/zenon-prover/zenon.git"
maintainer: "Damien Doligez <damien.doligez@inria.fr>"
authors: [ "R. Bonichon" "D. Delahaye" "D. Doligez" ]
bug-reports: "https://github.com/zenon-prover/zenon/issues"
depends: [
"ocaml" {>= "4.07.0"}
]
depopts: [
"coq"
]
conflicts: [
"coq" {< "8.6"}
"coq-core"
"ocaml-option-bytecode-only"
]
build: [
["./configure" "--prefix" "%{prefix}%" "--libdir" "%{zenon:lib}%"]
[make]
]
install: [[make "install"]]
synopsis: "An Extensible Automated Theorem Prover Producing Checkable Proofs"
description: """
Automated theorem prover for first order classical logic (with
equality), based on the tableau method. Zenon handles first-order
logic with equality. Its most important feature is that it outputs the
proofs of the theorems, in Coq-checkable form."""
url {
src: "https://github.com/zenon-prover/zenon/archive/0.8.5.tar.gz"
checksum: [
"sha256=73811276ad0aa46e91e346bf38937d37b1b9930e0b9f6b0aa20a5c1959e3006e"
"md5=6c64d2c29bbcb3571f25f7f8c2dbea6c"
]
}