CI: bump Coq to 8.20 and mathcomp to 2.3.0

.gitlab-ci.yml

@@ -29,7 +29,7 @@ stages:
     - opam install -y -v -j ${NJOBS} coq-prosa-refinements
 
 .preferred-stable-version:
-    image: registry.mpi-sws.org/mathcomp-for-prosa:2.2.0-coq-8.19
+    image: registry.mpi-sws.org/mathcomp-for-prosa:2.3.0-coq-8.20
 
 .build:
   image: registry.mpi-sws.org/mathcomp-for-prosa:${CI_JOB_NAME}
@@ -42,7 +42,7 @@ stages:
     - !reference [.build-common, script]
     - mv /tmp/POET .
     - cd POET
-    - pip3 install -r requirements.txt
+    - pip3 install --break-system-packages -r requirements.txt
     - >-
       for WORKLOAD in examples/*.yaml;
       do
@@ -71,6 +71,11 @@ stages:
     - .build
     - .not_in_wip_branches
 
+2.3.0-coq-8.20:
+  extends:
+    - .build
+    - .not_in_wip_branches
+
 POET:
   extends:
     - .build-and-test-POET
@@ -169,7 +174,7 @@ proof-state:
   extends:
    - .not_in_wip_branches
   stage: build
-  image: registry.mpi-sws.org/alectryon-ci:2.2.0-coq-8.19
+  image: registry.mpi-sws.org/alectryon-ci:2.3.0-coq-8.20
   script:
     - eval $(opam env)
     - make -j ${NJOBS} all

coq-prosa.opam

@@ -12,8 +12,8 @@ build: [
 ]
 install: [make "install"]
 depends: [
-  "coq" {((>= "8.18" & < "8.20~") | = "dev")}
-  "coq-mathcomp-algebra" {((>= "2.2" & < "2.3~") | = "dev")}
+  "coq" {((>= "8.19" & < "8.21~") | = "dev")}
+  "coq-mathcomp-algebra" {((>= "2.2" & < "2.4~") | = "dev")}
   "coq-mathcomp-zify" {>= "1.2.0"}
 ]