Skip to content
Snippets Groups Projects
Commit afeb6f07 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Bump Iris. Bump Coq version to 8.17.

parent 39f3c84e
No related branches found
No related tags found
No related merge requests found
Pipeline #81756 failed
Stage: build
Hide whitespace changes
Inline Side-by-side
.gitlab-ci.yml
+ 5
− 5
View file @ afeb6f07
...@@ -47,11 +47,11 @@ build-coq.dev: ...@@ -47,11 +47,11 @@ build-coq.dev:
variables: variables:
OPAM_PINS: "coq version dev" OPAM_PINS: "coq version dev"
build-coq.8.15.0: build-coq.8.17.0:
<<: *template <<: *template
variables: variables:
OCAML: "ocaml-variants.4.14.0+options ocaml-option-flambda" OCAML: "ocaml-variants.4.14.0+options ocaml-option-flambda"
OPAM_PINS: "coq version 8.15.0" OPAM_PINS: "coq version 8.17.0"
DENY_WARNINGS: "1" DENY_WARNINGS: "1"
MANGLE_NAMES: "1" MANGLE_NAMES: "1"
# Coq bench needs an opam package # Coq bench needs an opam package
...@@ -60,11 +60,11 @@ build-coq.8.15.0: ...@@ -60,11 +60,11 @@ build-coq.8.15.0:
- fp-timing - fp-timing
# Separate MR job that does not run on fp-timing. # Separate MR job that does not run on fp-timing.
build-coq.8.15.0-mr: build-coq.8.17.0-mr:
<<: *template <<: *template
<<: *only_mr <<: *only_mr
variables: variables:
OPAM_PINS: "coq version 8.15.0" OPAM_PINS: "coq version 8.17.0"
MANGLE_NAMES: "1" MANGLE_NAMES: "1"
DENY_WARNINGS: "1" DENY_WARNINGS: "1"
...@@ -72,7 +72,7 @@ trigger-iris.timing: ...@@ -72,7 +72,7 @@ trigger-iris.timing:
<<: *template <<: *template
variables: variables:
OCAML: "ocaml-variants.4.14.0+options ocaml-option-flambda" OCAML: "ocaml-variants.4.14.0+options ocaml-option-flambda"
OPAM_PINS: "coq version 8.15.0 git+https://gitlab.mpi-sws.org/$IRIS_REPO#$IRIS_REV" OPAM_PINS: "coq version 8.17.0 git+https://gitlab.mpi-sws.org/$IRIS_REPO#$IRIS_REV"
tags: tags:
- fp-timing - fp-timing
only: only:
......
README.md
+ 1
− 1
View file @ afeb6f07
...@@ -6,7 +6,7 @@ Some example verification demonstrating the use of Iris. ...@@ -6,7 +6,7 @@ Some example verification demonstrating the use of Iris.
This version is known to compile with: This version is known to compile with:
- Coq 8.15.0 - Coq 8.17.0
- A development version of [Iris](https://gitlab.mpi-sws.org/iris/iris) - A development version of [Iris](https://gitlab.mpi-sws.org/iris/iris)
- A development version of [Autosubst](https://github.com/coq-community/autosubst) - A development version of [Autosubst](https://github.com/coq-community/autosubst)
......
_CoqProject
+ 2
− 0
View file @ afeb6f07
...@@ -4,6 +4,8 @@ ...@@ -4,6 +4,8 @@
# Cannot use non-canonical projections as it causes massive unification failures # Cannot use non-canonical projections as it causes massive unification failures
# (https://github.com/coq/coq/issues/6294). # (https://github.com/coq/coq/issues/6294).
-arg -w -arg -redundant-canonical-projection -arg -w -arg -redundant-canonical-projection
# Fixing this one requires Coq 8.17
-arg -w -arg -future-coercion-class-field
theories/barrier/proof.v theories/barrier/proof.v
theories/barrier/specification.v theories/barrier/specification.v
......
coq-iris-examples.opam
+ 1
− 1
View file @ afeb6f07
...@@ -8,7 +8,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/examples.git" ...@@ -8,7 +8,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/examples.git"
synopsis: "A collection of case studies for Iris -- not meant to be used as a dependency of anything" synopsis: "A collection of case studies for Iris -- not meant to be used as a dependency of anything"
depends: [ depends: [
"coq-iris-heap-lang" { (= "dev.2023-04-12.0.958aad09") | (= "dev") } "coq-iris-heap-lang" { (= "dev.2023-05-02.4.943e9b74") | (= "dev") }
"coq-autosubst" { = "dev" } "coq-autosubst" { = "dev" }
] ]
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment