coqhammer/coq-hammer.opam at rocq-9.1 · lukaszcz/coqhammer · GitHub

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
opam-version: "2.0"
version: "9.1.dev"
maintainer: "palmskog@gmail.com"

homepage: "https://github.com/lukaszcz/coqhammer"
dev-repo: "git+https://github.com/lukaszcz/coqhammer.git"
bug-reports: "https://github.com/lukaszcz/coqhammer/issues"
license: "LGPL-2.1-only"

synopsis: "General-purpose automated reasoning hammer tool for Coq"
description: """
A general-purpose automated reasoning hammer tool for Coq that combines
learning from previous proofs with the translation of problems to the
logics of automated systems and the reconstruction of successfully found proofs.
"""

build: [make "-j%{jobs}%" "plugin"]
install: [
  [make "install-plugin"]
  [make "test-plugin"] {with-test}
]
depends: [
  "ocaml" {>= "4.09.0"}
  "coq" {>= "9.1" & < "9.2~"}
  ("conf-g++" {build} | "conf-clang" {build})
  "coq-hammer-tactics" {= version}
]

tags: [
  "category:Miscellaneous/Coq Extensions"
  "keyword:automation"
  "keyword:hammer"
  "logpath:Hammer.Plugin"
]

authors: [
  "Lukasz Czajka <lukaszcz@mimuw.edu.pl>"
  "Cezary Kaliszyk <cezary.kaliszyk@uibk.ac.at>"
]