From 6b01e638cc0eea47cd58d6d4a6b67628d6dd85ce Mon Sep 17 00:00:00 2001
From: Karl Palmskog <palmskog@gmail.com>
Date: Sat, 7 Oct 2023 08:30:48 +0200
Subject: [PATCH] add coq-buchberger.8.17.0

---
 .../coq-buchberger/coq-buchberger.8.17.0/opam | 38 +++++++++++++++++++
 1 file changed, 38 insertions(+)
 create mode 100644 released/packages/coq-buchberger/coq-buchberger.8.17.0/opam

diff --git a/released/packages/coq-buchberger/coq-buchberger.8.17.0/opam b/released/packages/coq-buchberger/coq-buchberger.8.17.0/opam
new file mode 100644
index 000000000..ceaa3e753
--- /dev/null
+++ b/released/packages/coq-buchberger/coq-buchberger.8.17.0/opam
@@ -0,0 +1,38 @@
+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 in Coq of Buchberger's algorithm for computing Gröbner bases"
+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.17" & < "8.19~"}
+]
+
+tags: [
+  "category:Mathematics/Algebra"
+  "category:Miscellaneous/Extracted Programs/Combinatorics"
+  "keyword:Gröbner basis"
+  "keyword:polynomial ideal"
+  "keyword:Buchberger's algorithm"
+  "logpath:Buchberger"
+  "date:2023-10-06"
+]
+authors: [
+  "Laurent Théry"
+  "Henrik Persson"
+]
+
+url {
+  src: "https://github.com/coq-community/buchberger/archive/v8.17.0.tar.gz"
+  checksum: "sha512=923ab0126c3389e1e8e2cb8460a437c8252f69b2ed3c876a5c66025bd4ee3d683fcf1a818ff1a5f00e4025e4b5e27aae59556c1fa6bfebc939684c022b5e983f"
+}