Pick 8.20~2025.01: first preview with all packages that work as is

Author: MSoegtropIMC

.github/workflows/macos.yml

@@ -12,8 +12,6 @@ name: Macos
 on:
   push:
     branches:
-      - 2021.02
-      - 2021.09
       - main
   pull_request:
     branches:
@@ -51,8 +49,8 @@ jobs:
       matrix:
         variant:
           # Keep this in sync with the Smoke test below
+          - '8.20~2025.01'
           - '8.19~2024.10'
-          - '8.18~2023.11'
     steps:
       - name: Git checkout
         uses: actions/checkout@v4
@@ -166,8 +164,8 @@ jobs:
       fail-fast: false
       matrix:
         variant:
+          - '8.20~2025.01'
           - '8.19~2024.10'
-          - '8.18~2023.11'
 
     steps:
       - name: Install bash

.github/workflows/ubuntu.yml

@@ -12,8 +12,6 @@ name: Ubuntu
 on:
   push:
     branches:
-      - 2021.02
-      - 2021.09
       - main
   pull_request:
     branches:
@@ -51,6 +49,7 @@ jobs:
       matrix:
         variant:
           # This should contain all picks introduced in the current release + all original picks of all Coq versions
+          - '8.20~2025.01'
           - '8.19~2024.10'
           - '8.18~2023.11'
           - '8.17~2023.08'

.github/workflows/windows.yml

@@ -51,8 +51,8 @@ jobs:
           - '64'
         variant:
           # Keep this in sync with the Smoke test below
+          - '8.20~2025.01'
           - '8.19~2024.10'
-          - '8.18~2023.11'
 
     steps:
       - name: Set git to use LF
@@ -103,8 +103,8 @@ jobs:
         architecture:
           - '64'
         variant:
+          - '8.20~2025.01'
           - '8.19~2024.10'
-          - '8.18~2023.11'
 
     steps:
       - name: 'Download Artifact'

maintainer_scripts/notify-upstream.sh

@@ -4,7 +4,7 @@ echo SHELL="$SHELL"
 
 ###################### COPYRIGHT/COPYLEFT ######################
 
-# (C) 2022 Michael Soegtrop
+# (C) 2024 Michael Soegtrop
 # (C) 2020 Enrico Tassi
 
 # Released to the public under the
@@ -36,18 +36,21 @@ PACKAGE_FILTER_RE="${2:-.}"
 
 ########## Settings ##########
 
+# Extension and release date of the Coq release
 EXT_RELEASE=".0"
-DATE_RELEASE="January 24th, 2024"
+DATE_RELEASE="September 3rd, 2024"
+# Extension and release date of the Coq release, in case the above is a beta
 EXT_FINAL=""
 DATE_FINAL=""
-VERSION_PLATFORM="2024.10"
-DATE_PLATFORM_BETA="March 31st, 2024"
-DATE_PLATFORM_NOTIFY="March 31st, 2024"
-DATE_PLATFORM_EXPECTED="April 30th, 2024"
-DATE_PLATFORM_LATEST="May 15th, 2024"
+# Coq Platform release code and dates
+VERSION_PLATFORM="2025.01"
+DATE_PLATFORM_BETA="Dec 8th, 2024"
+DATE_PLATFORM_NOTIFY="Dec 31st, 2024"
+DATE_PLATFORM_EXPECTED="Jan 31st, 2025"
+DATE_PLATFORM_LATEST="Feb 28th, 2025"
 PLATFORM_MAIN_BRANCH="https://github.com/coq/platform/tree/main"
 
-CC="CC: https://github.com/coq/platform/issues/405"
+CC="CC: https://github.com/coq/platform/issues/449"
 #CC="\n@coqbot column:...."
 
 COQ_PLATFORM_UNIMATH=Y

maintainer_scripts/packages_already_processed.txt

@@ -1,65 +0,0 @@
-coq-bignums
-coq-ext-lib
-coq-stdpp
-coq-mathcomp-ssreflect
-coq-mathcomp-fingroup
-coq-mathcomp-algebra
-coq-mathcomp-solvable
-coq-mathcomp-field
-coq-mathcomp-character
-coq-mathcomp-bigenough
-coq-mathcomp-finmap
-coq-mathcomp-real-closed
-coq-mathcomp-zify
-coq-mathcomp-multinomials
-coq-coquelicot
-coq-coqprime
-coq-coqprime-generator
-coq-flocq
-coq-interval
-coq-gappa
-gappa
-coq-math-classes
-coq-corn
-coq-hott
-coq-unimath
-coq-simple-io
-coq-menhirlib
-coq-equations
-coq-aac-tactics
-coq-unicoq
-coq-mtac2
-elpi
-coq-elpi
-coq-hierarchy-builder
-coq-quickchick
-coq-hammer-tactics
-coq-hammer
-coq-paramcoq
-coq-coqeal
-coq-libhyps
-coq-itauto
-coq-mathcomp-analysis
-coq-mathcomp-algebra-tactics
-coq-relation-algebra
-coq-reglang
-coq-iris
-coq-iris-heap-lang
-coq-ott
-coq-mathcomp-word
-coq-compcert
-coq-vst
-coq-dpdgraph
-coq-deriving
-coq-extructures
-coq-reduction-effects
-coq-record-update
-coq-serapi
-coq-coqutil
-coq-rewriter
-coq-riscv
-coq-bedrock2
-coq-bedrock2-compiler
-coq-rupicola
-coq-fiat-crypto
-coq-metacoq

opam/opam-coq-archive/released/packages/coq-unimath/coq-unimath.20240923/opam

@@ -0,0 +1,18 @@
+opam-version: "2.0"
+maintainer: "The UniMath Development Team"
+homepage: "https://github.com/UniMath/UniMath"
+dev-repo: "git+https://github.com/UniMath/UniMath.git"
+bug-reports: "https://github.com/UniMath/UniMath/issues"
+license: "Similar to MIT license"
+authors: ["The UniMath Development Team"]
+build: [make "BUILD_COQ=no" "-j%{jobs}%"]
+install: [make "BUILD_COQ=no" "install"]
+depends: [
+  "ocaml"
+  "coq" {>= "8.18"}
+]
+synopsis: "Library of Univalent Mathematics"
+url {
+  src: "https://github.com/UniMath/UniMath/archive/refs/tags/v20240923.tar.gz"
+  checksum: "sha512=ffb905217bc6426d6ad00168959961f560a05c040b10de0145ef27e1d93e9ab9ef60f7f5127fc8b9e0b04ad99608b452dbf261bc34072ee4f47ef6b6951bbc47"
+}