From 69d1bf6fab88629ebd0e818398d7d074a5c1bce0 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 21 Dec 2016 17:58:51 +0100
Subject: [PATCH] ssreflect 1.6.1 is out :)
---
.gitlab-ci.yml | 4 ++--
README.md | 11 +----------
opam | 2 +-
3 files changed, 4 insertions(+), 13 deletions(-)
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index bd4cb61a8..9b50df40f 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -5,7 +5,7 @@ iris-coq8.5.3:
- coq
script:
# prepare
- - . build/opam-ci.sh 'coq 8.5.3' 'coq-mathcomp-ssreflect 1.6'
+ - . build/opam-ci.sh 'coq 8.5.3' 'coq-mathcomp-ssreflect 1.6.1'
# build
- 'time make -j8 TIMED=y 2>&1 | tee build-log.txt'
- 'if fgrep Axiom build-log-full.txt >/dev/null; then exit 1; fi'
@@ -28,7 +28,7 @@ iris-coq8.6:
- coq
script:
# prepare
- - . build/opam-ci.sh 'coq 8.6' 'coq-mathcomp-ssreflect dev'
+ - . build/opam-ci.sh 'coq 8.6' 'coq-mathcomp-ssreflect 1.6.1'
# build
- 'time make -j8'
cache:
diff --git a/README.md b/README.md
index ca6df7fb2..e01c64e53 100644
--- a/README.md
+++ b/README.md
@@ -7,22 +7,13 @@ This is the Coq development of the [Iris Project](http://iris-project.org).
This version is known to compile with:
- Coq 8.5pl3 / 8.6
- - Ssreflect 1.6
+ - Ssreflect 1.6.1
The easiest way to install the correct versions of the dependencies is through
opam. Once you got opam set up, just run `make build-dep` to install the right
versions of the dependencies. When the dependencies change, just run `make
build-dep` again.
-For development, better make sure you have a version of Ssreflect that includes
-commit ad273277 (no such version has been released so far, you will have to
-fetch the development branch yourself). Iris compiles fine even without this
-patch, but proof bullets will only be in 'strict' (enforcing) mode with the
-fixed version of Ssreflect. If you are using opam, you can easily get a fixed
-version by running
-
- opam pin add coq-mathcomp-ssreflect https://github.com/math-comp/math-comp.git#ad273277ab38bfe458e9332dea5f3a79e3885567
-
## Building Instructions
Run `make` to build the full development.
diff --git a/opam b/opam
index e8d2bee54..118d9a61f 100644
--- a/opam
+++ b/opam
@@ -14,5 +14,5 @@ install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris'" ]
depends: [
"coq" { ((>= "8.5.1" & < "8.7~") | (= "dev"))}
- "coq-mathcomp-ssreflect" { ((>= "1.6" & < "1.7~") | (= "dev"))}
+ "coq-mathcomp-ssreflect" { ((>= "1.6.1" & < "1.7~") | (= "dev"))}
]
--
GitLab