From 62746ef0e7a2629906277ebb1a4d193a414500b1 Mon Sep 17 00:00:00 2001
From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com>
Date: Thu, 12 Dec 2024 09:38:27 +0100
Subject: [PATCH 1/3] Pick 8.20~2025.01: updated oq-mathcomp-multinomials to
 version 2.3.0 and enabled it

---
 .../coq-mathcomp-multinomials.2.3.0/opam      | 31 +++++++++++++++++++
 package_picks/package-pick-8.20~2025.01.sh    |  2 +-
 2 files changed, 32 insertions(+), 1 deletion(-)
 create mode 100644 opam/opam-coq-archive/released/packages/coq-mathcomp-multinomials/coq-mathcomp-multinomials.2.3.0/opam

diff --git a/opam/opam-coq-archive/released/packages/coq-mathcomp-multinomials/coq-mathcomp-multinomials.2.3.0/opam b/opam/opam-coq-archive/released/packages/coq-mathcomp-multinomials/coq-mathcomp-multinomials.2.3.0/opam
new file mode 100644
index 0000000000..7ed3fb7e7b
--- /dev/null
+++ b/opam/opam-coq-archive/released/packages/coq-mathcomp-multinomials/coq-mathcomp-multinomials.2.3.0/opam
@@ -0,0 +1,31 @@
+opam-version: "2.0"
+maintainer: "pierre-yves@strub.nu"
+homepage: "https://github.com/math-comp/multinomials"
+bug-reports: "https://github.com/math-comp/multinomials/issues"
+dev-repo: "git+https://github.com/math-comp/multinomials.git"
+license: "CECILL-B"
+authors: ["Pierre-Yves Strub"]
+build: [
+  [ "dune" "build" "-p" name "-j" jobs ]
+]
+depends: [
+  "coq"                    {(>= "8.16" & < "8.21~") | = "dev"}
+  "coq-elpi"               {< "2.4~"}
+  "dune"                   {>= "3.8"}
+  "coq-mathcomp-ssreflect" {(>= "2.0" & < "2.4~") | = "dev"}
+  "coq-mathcomp-algebra"
+  "coq-mathcomp-bigenough" {(>= "1.0" & < "1.1~") | = "dev"}
+  "coq-mathcomp-finmap"    {(>= "2.0" & < "2.2~") | = "dev"}
+]
+tags: [
+  "keyword:multinomials"
+  "keyword:monoid algebra"
+  "category:Mathematics/Algebra/Multinomials"
+  "category:Mathematics/Algebra/Monoid algebra"
+  "logpath:mathcomp.multinomials"
+]
+synopsis: "A Multivariate polynomial Library for the Mathematical Components Library"
+url {
+  src: "https://github.com/math-comp/multinomials/archive/2.3.0.tar.gz"
+  checksum: "sha512=03c71f246a00c80b7d83f357d9c54fcf485cc17bd3399dd041a36c88ae7532e0db92dd0de0e7b4e94c7d7707ffa6ad745271af1d1e24f009709061d1b21162c8"
+}
diff --git a/package_picks/package-pick-8.20~2025.01.sh b/package_picks/package-pick-8.20~2025.01.sh
index 72567949af..eb1fce9035 100644
--- a/package_picks/package-pick-8.20~2025.01.sh
+++ b/package_picks/package-pick-8.20~2025.01.sh
@@ -89,7 +89,7 @@ then
   PACKAGES="${PACKAGES} coq-mathcomp-finmap.2.1.0"
 # PACKAGES="${PACKAGES} coq-mathcomp-real-closed.2.0.1" # ToDo requires downgrade coq-mathcomp-ssreflect 2.3.0 to 2.2.0, fails with version restriction relaxation
   PACKAGES="${PACKAGES} coq-mathcomp-zify.1.5.0+2.0+8.16"
-# PACKAGES="${PACKAGES} coq-mathcomp-multinomials.2.2.0" # ToDo requires downgrade coq-mathcomp-ssreflect 2.3.0 to 2.2.0, fails with version restriction relaxation
+  PACKAGES="${PACKAGES} coq-mathcomp-multinomials.2.3.0"
   PACKAGES="${PACKAGES} coq-coquelicot.3.4.2"
 
   # Number theory

From d01b30caf75958a4d653e173991ff5e696947114 Mon Sep 17 00:00:00 2001
From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com>
Date: Mon, 16 Dec 2024 19:16:08 +0100
Subject: [PATCH 2/3] Pick 8.20~2025.01: update elpi to version 2.0.6 and
 coq-hierarchy-builder to version 1.8.0

---
 package_picks/package-pick-8.20~2025.01.sh | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/package_picks/package-pick-8.20~2025.01.sh b/package_picks/package-pick-8.20~2025.01.sh
index eb1fce9035..b5b99ea537 100644
--- a/package_picks/package-pick-8.20~2025.01.sh
+++ b/package_picks/package-pick-8.20~2025.01.sh
@@ -77,8 +77,8 @@ then
   PACKAGES="${PACKAGES} coq-stdpp.1.11.0"
 
   # General mathematics
-  PACKAGES="${PACKAGES} elpi.2.0.5 coq-elpi.2.3.0" # This would belong into the "Proof automation" section, but it is required by coq-hierarchy-builder
-  PACKAGES="${PACKAGES} coq-hierarchy-builder.1.7.1"
+  PACKAGES="${PACKAGES} elpi.2.0.6 coq-elpi.2.3.0" # This would belong into the "Proof automation" section, but it is required by coq-hierarchy-builder
+  PACKAGES="${PACKAGES} coq-hierarchy-builder.1.8.0"
   PACKAGES="${PACKAGES} coq-mathcomp-ssreflect.2.3.0"
   PACKAGES="${PACKAGES} coq-mathcomp-fingroup.2.3.0"
   PACKAGES="${PACKAGES} coq-mathcomp-algebra.2.3.0"

From c40acb7ca24f69f22600ef3bb00f626586ad7f44 Mon Sep 17 00:00:00 2001
From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com>
Date: Mon, 16 Dec 2024 19:19:19 +0100
Subject: [PATCH 3/3] Opam: remove local package
 coq-mathcomp-multinomials.2.3.0 (available upstream)

---
 .../coq-mathcomp-multinomials.2.3.0/opam      | 31 -------------------
 1 file changed, 31 deletions(-)
 delete mode 100644 opam/opam-coq-archive/released/packages/coq-mathcomp-multinomials/coq-mathcomp-multinomials.2.3.0/opam

diff --git a/opam/opam-coq-archive/released/packages/coq-mathcomp-multinomials/coq-mathcomp-multinomials.2.3.0/opam b/opam/opam-coq-archive/released/packages/coq-mathcomp-multinomials/coq-mathcomp-multinomials.2.3.0/opam
deleted file mode 100644
index 7ed3fb7e7b..0000000000
--- a/opam/opam-coq-archive/released/packages/coq-mathcomp-multinomials/coq-mathcomp-multinomials.2.3.0/opam
+++ /dev/null
@@ -1,31 +0,0 @@
-opam-version: "2.0"
-maintainer: "pierre-yves@strub.nu"
-homepage: "https://github.com/math-comp/multinomials"
-bug-reports: "https://github.com/math-comp/multinomials/issues"
-dev-repo: "git+https://github.com/math-comp/multinomials.git"
-license: "CECILL-B"
-authors: ["Pierre-Yves Strub"]
-build: [
-  [ "dune" "build" "-p" name "-j" jobs ]
-]
-depends: [
-  "coq"                    {(>= "8.16" & < "8.21~") | = "dev"}
-  "coq-elpi"               {< "2.4~"}
-  "dune"                   {>= "3.8"}
-  "coq-mathcomp-ssreflect" {(>= "2.0" & < "2.4~") | = "dev"}
-  "coq-mathcomp-algebra"
-  "coq-mathcomp-bigenough" {(>= "1.0" & < "1.1~") | = "dev"}
-  "coq-mathcomp-finmap"    {(>= "2.0" & < "2.2~") | = "dev"}
-]
-tags: [
-  "keyword:multinomials"
-  "keyword:monoid algebra"
-  "category:Mathematics/Algebra/Multinomials"
-  "category:Mathematics/Algebra/Monoid algebra"
-  "logpath:mathcomp.multinomials"
-]
-synopsis: "A Multivariate polynomial Library for the Mathematical Components Library"
-url {
-  src: "https://github.com/math-comp/multinomials/archive/2.3.0.tar.gz"
-  checksum: "sha512=03c71f246a00c80b7d83f357d9c54fcf485cc17bd3399dd041a36c88ae7532e0db92dd0de0e7b4e94c7d7707ffa6ad745271af1d1e24f009709061d1b21162c8"
-}