From 069df49e93864a9a46317d40a3ac8dcca4d4ca97 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 2 Oct 2024 17:05:14 +0200
Subject: [PATCH] bump to Coq 8.19
---
.gitlab-ci.yml | 6 +++---
README.md | 2 +-
_CoqProject | 2 ++
3 files changed, 6 insertions(+), 4 deletions(-)
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index c391afb7..166faac3 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -28,10 +28,10 @@ variables:
## Build jobs
-build-coq.8.18.0:
+build-coq.8.19.0:
<<: *template
variables:
- OPAM_PINS: "coq version 8.18.0"
+ OPAM_PINS: "coq version 8.19.0"
DENY_WARNINGS: "1"
MANGLE_NAMES: "1"
# Mostly to make the lifetime logic available
@@ -42,7 +42,7 @@ build-coq.8.18.0:
trigger-iris.timing:
<<: *template
variables:
- OPAM_PINS: "coq version 8.18.0 git+https://gitlab.mpi-sws.org/$IRIS_REPO#$IRIS_REV"
+ OPAM_PINS: "coq version 8.19.0 git+https://gitlab.mpi-sws.org/$IRIS_REPO#$IRIS_REV"
tags:
- fp-timing
only:
diff --git a/README.md b/README.md
index 89744a06..b4c842e3 100644
--- a/README.md
+++ b/README.md
@@ -6,7 +6,7 @@ This is the Coq development accompanying lambda-Rust.
This version is known to compile with:
- - Coq 8.18.0
+ - Coq 8.19.0
- A development version of [Iris](https://gitlab.mpi-sws.org/iris/iris)
## Building from source
diff --git a/_CoqProject b/_CoqProject
index 8a8ef0b0..3a2d7910 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -8,6 +8,8 @@
# Cannot use non-canonical projections as it causes massive unification failures
# (https://github.com/coq/coq/issues/6294).
-arg -w -arg -redundant-canonical-projection
+# Warning seems incorrect, see https://gitlab.mpi-sws.org/iris/stdpp/-/issues/216
+-arg -w -arg -notation-incompatible-prefix
lifetime/model/definitions.v
lifetime/model/faking.v
--
GitLab