opam

opam-version: "2.0"
maintainer: "simon.cruanes@inria.fr"
authors: "Simon Cruanes"
homepage: "https://www.rocq.inria.fr/deducteam/Zipperposition/index.html"
bug-reports: "https://github.com/c-cube/zipperposition/issues"
tags: ["logic" "unification" "term" "superposition" "prover"]
dev-repo: "git+https://github.com/c-cube/zipperposition.git"
build: [
  [
    "./configure"
    "--bindir"
    "%{bin}%"
    "--disable-tests"
    "--disable-docs"
    "--%{menhir:enable}%-parsers"
    "--disable-solving"
    "--disable-qcheck"
    "--disable-tools"
    "--enable-meta"
  ]
  [make]
]
install: [make "install"]
remove: [
  ["ocamlfind" "remove" "libzipperposition"]
  ["rm" "%{bin}%/zipperposition"]
]
depends: [
  "ocaml" {>= "4.02.3"}
  "ocamlfind" {build}
  "base-bytes"
  "base-unix"
  "zarith"
  "containers" {> "0.16" & < "1.0"}
  "sequence" {>= "0.4" & < "0.9"}
  "gen"
  "oclock"
  "oasis"
  "msat" {>= "0.3" & < "0.4"}
  "num"
]
depopts: [
  "menhir" {build}
  "qcheck" {with-test}
]
conflicts: [
  "containers" { >= "1.2" }
  "sequence" { >= "0.9" }
]
synopsis:
  "Zipperposition is a superposition prover for full first order logic with equality."
description: """
The accent is on flexibility, modularity and simplicity rather than performance, to allow
quick experimenting on automated theorem proving. It generates TSTP traces and features
many simplification rules and redundancy criteria."""
flags: light-uninstall
url {
  src: "https://github.com/c-cube/zipperposition/archive/1.0.tar.gz"
  checksum: [
    "sha256=287a24ec7109b00ff56b97cabce15f3ce6c130fe1f4fb52cb7bec2b64c9e2917"
    "md5=48b8a8319663b6520622fe23f24fc073"
  ]
}