opam-version: "2.0"
maintainer: "palmskog@gmail.com"

homepage: "https://github.com/coq-community/buchberger"
dev-repo: "git+https://github.com/coq-community/buchberger.git"
bug-reports: "https://github.com/coq-community/buchberger/issues"
license: "LGPL-2.1-or-later"

synopsis: "Verified implementation of Buchberger's algorithm for computing Gröbner bases in Coq"
description: """
A verified implementation of Buchberger's algorithm in Coq,
which computes the Gröbner basis associated with a polynomial ideal.
Also includes a constructive proof of Dickson's lemma."""

build: [make "-j%{jobs}%"]
install: [make "install"]
depends: [
  "coq" {>= "8.7" & < "8.13~"}
]

tags: [
  "category:Mathematics/Algebra"
  "category:Miscellaneous/Extracted Programs/Combinatorics"
  "keyword:Gröbner basis"
  "keyword:polynomial ideal"
  "keyword:Buchberger's algorithm"
  "logpath:Buchberger"
  "date:2020-05-27"
]
authors: [
  "Laurent Théry"
  "Henrik Persson"
]

url {
  src: "https://github.com/coq-community/buchberger/archive/v8.11.0.tar.gz"
  checksum: "sha512=a048ee35574090d2ffa6b8c6a5e4379bb5f7699e0b84c1c4781fb624d151faca02eb9122bae2d21296ba6dbe57adb116edaa1255a5475b1cbafe89d33d364a05"
}