Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Iris
Iris
Commits
ff2b1d90
Commit
ff2b1d90
authored
May 16, 2022
by
Ralf Jung
Browse files
use Coq 8.15.1, and enable flambda
parent
de41b20f
Pipeline
#66073
passed with stage
in 28 minutes and 23 seconds
Changes
2
Pipelines
2
Hide whitespace changes
Inline
Side-by-side
.gitlab-ci.yml
View file @
ff2b1d90
...
@@ -5,7 +5,7 @@ stages:
...
@@ -5,7 +5,7 @@ stages:
variables
:
variables
:
CPU_CORES
:
"
10"
CPU_CORES
:
"
10"
OCAML
:
"
ocaml-
base-compiler.4.14.0
"
OCAML
:
"
ocaml-
variants.4.14.0+options
ocaml-option-flambda
"
.only_branches
:
&only_branches
.only_branches
:
&only_branches
only
:
only
:
...
@@ -42,19 +42,12 @@ variables:
...
@@ -42,19 +42,12 @@ variables:
## Build jobs
## Build jobs
build-coq.8.15.
0
:
build-coq.8.15.
1
:
<<
:
*template
<<
:
*template
variables
:
variables
:
OPAM_PINS
:
"
coq
version
8.15.
0
"
OPAM_PINS
:
"
coq
version
8.15.
1
"
DENY_WARNINGS
:
"
1"
DENY_WARNINGS
:
"
1"
MANGLE_NAMES
:
"
1"
MANGLE_NAMES
:
"
1"
build-coq.8.14.1
:
<<
:
*template
variables
:
OPAM_PINS
:
"
coq
version
8.14.1"
MANGLE_NAMES
:
"
1"
DENY_WARNINGS
:
"
1"
OPAM_PKG
:
"
1"
OPAM_PKG
:
"
1"
DOC_DIR
:
"
coqdoc@center.mpi-sws.org:iris"
DOC_DIR
:
"
coqdoc@center.mpi-sws.org:iris"
DOC_OPTS
:
"
--external
https://plv.mpi-sws.org/coqdoc/stdpp/
stdpp"
DOC_OPTS
:
"
--external
https://plv.mpi-sws.org/coqdoc/stdpp/
stdpp"
...
@@ -62,14 +55,14 @@ build-coq.8.14.1:
...
@@ -62,14 +55,14 @@ build-coq.8.14.1:
-
fp-timing
-
fp-timing
interruptible
:
false
interruptible
:
false
# Separate MR job that does not run on fp-timing.
build-coq.8.14.1
:
build-coq.8.14.1-mr
:
<<
:
*template
<<
:
*template
<<
:
*
only
_mr
<<
:
*
branches_and
_mr
variables
:
variables
:
OPAM_PINS
:
"
coq
version
8.14.1"
OPAM_PINS
:
"
coq
version
8.14.1"
MANGLE_NAMES
:
"
1"
MANGLE_NAMES
:
"
1"
DENY_WARNINGS
:
"
1"
DENY_WARNINGS
:
"
1"
OCAML
:
"
ocaml-base-compiler.4.07.1"
build-coq.8.13.2
:
build-coq.8.13.2
:
<<
:
*template
<<
:
*template
...
@@ -77,14 +70,15 @@ build-coq.8.13.2:
...
@@ -77,14 +70,15 @@ build-coq.8.13.2:
variables
:
variables
:
OPAM_PINS
:
"
coq
version
8.13.2"
OPAM_PINS
:
"
coq
version
8.13.2"
DENY_WARNINGS
:
"
1"
DENY_WARNINGS
:
"
1"
OCAML
:
"
ocaml-base-compiler.4.07.1"
# Nightly job with a known-to-work Coq version
# Nightly job with a known-to-work Coq version
# (so failures must be caused by std++)
# (so failures must be caused by std++)
trigger-stdpp.dev-coq.8.1
4
.1
:
trigger-stdpp.dev-coq.8.1
5
.1
:
<<
:
*template
<<
:
*template
variables
:
variables
:
STDPP_REPO
:
"
iris/stdpp"
STDPP_REPO
:
"
iris/stdpp"
OPAM_PINS
:
"
coq
version
8.1
4
.1
git+https://gitlab.mpi-sws.org/$STDPP_REPO#$STDPP_REV"
OPAM_PINS
:
"
coq
version
8.1
5
.1
git+https://gitlab.mpi-sws.org/$STDPP_REPO#$STDPP_REV"
except
:
except
:
only
:
only
:
-
triggers
-
triggers
...
...
README.md
View file @
ff2b1d90
...
@@ -30,7 +30,7 @@ Importing Iris has some side effects as the library sets some global options.
...
@@ -30,7 +30,7 @@ Importing Iris has some side effects as the library sets some global options.
This version is known to compile with:
This version is known to compile with:
-
Coq 8.13.2 / 8.14.1 / 8.15.
0
-
Coq 8.13.2 / 8.14.1 / 8.15.
1
-
A development version of
[
std++
](
https://gitlab.mpi-sws.org/iris/stdpp
)
-
A development version of
[
std++
](
https://gitlab.mpi-sws.org/iris/stdpp
)
If you need to work with older versions of Coq, you can check out the
If you need to work with older versions of Coq, you can check out the
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment