From fcea8f31faa47dc58cf190cfcd7712025921bce9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Mon, 16 Dec 2024 17:43:06 +0000
Subject: [PATCH] CI: bump Coq to 8.20 and mathcomp to 2.3.0
---
.gitlab-ci.yml | 11 ++++++++---
coq-prosa.opam | 4 ++--
2 files changed, 10 insertions(+), 5 deletions(-)
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 2b30bc1bc..1d6c9ffce 100644
--- a/.gitlab-ci.yml
+++ b/.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
diff --git a/coq-prosa.opam b/coq-prosa.opam
index c1c6cd004..817f59813 100644
--- a/coq-prosa.opam
+++ b/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"}
]
--
GitLab