Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Iris
examples
Commits
53091bb4
Commit
53091bb4
authored
Oct 28, 2017
by
Ralf Jung
Browse files
test against released Coq 8.7.0; update CI
parent
9b841f5e
Pipeline
#5012
passed with stage
in 4 minutes and 19 seconds
Changes
3
Pipelines
3
Hide whitespace changes
Inline
Side-by-side
.gitlab-ci.yml
View file @
53091bb4
...
...
@@ -23,17 +23,17 @@ variables:
-
master
-
/^ci/
build-coq.8.7
:
build-coq.8.7
.0
:
<<
:
*template
variables
:
OPAM_PINS
:
"
coq
version
8.7.
dev
coq-mathcomp-ssreflect
version
dev
"
OPAM_PINS
:
"
coq
version
8.7.
0
coq-mathcomp-ssreflect
version
1.6.2
"
except
:
-
triggers
build-coq.8.6.1
:
<<
:
*template
variables
:
OPAM_PINS
:
"
coq
version
8.6.1
coq-mathcomp-ssreflect
version
1.6.
1
"
OPAM_PINS
:
"
coq
version
8.6.1
coq-mathcomp-ssreflect
version
1.6.
2
"
VALIDATE
:
"
1"
artifacts
:
paths
:
...
...
@@ -45,6 +45,6 @@ build-coq.8.6.1:
build-iris.dev
:
<<
:
*template
variables
:
OPAM_PINS
:
"
coq
version
8.6.1
coq-mathcomp-ssreflect
version
1.6.
1
coq-iris.dev
git
https://gitlab.mpi-sws.org/FP/iris-coq.git#$IRIS_REV"
OPAM_PINS
:
"
coq
version
8.6.1
coq-mathcomp-ssreflect
version
1.6.
2
coq-iris.dev
git
https://gitlab.mpi-sws.org/FP/iris-coq.git#$IRIS_REV"
only
:
-
triggers
README.md
View file @
53091bb4
...
...
@@ -6,8 +6,8 @@ Some example verification demonstrating the use of Iris.
This version is known to compile with:
-
Coq 8.6.1
-
Ssreflect 1.6.
1
-
Coq 8.6.1
/ 8.7.0
-
Ssreflect 1.6.
2
-
A development version of
[
Iris
](
https://gitlab.mpi-sws.org/FP/iris-coq/
)
The easiest way to install the correct versions of the dependencies is through
...
...
build/opam-ci.sh
View file @
53091bb4
#!/bin/bash
set
-e
set
-x
## This script installs the build dependencies for CI builds.
function
run_and_print
()
{
echo
"
$ $@
"
"
$@
"
}
# Prepare OPAM configuration
export
OPAMROOT
=
"
$(
pwd
)
/opamroot"
...
...
@@ -12,32 +9,27 @@ export OPAMJOBS="$((2*$CPU_CORES))"
export
OPAM_EDITOR
=
"
$(
which
false
)
"
# Make sure we got a good OPAM.
test
-d
"
$OPAMROOT
"
||
(
mkdir
"
$OPAMROOT
"
&&
run_and_print
opam init
--no-setup
-y
)
test
-d
"
$OPAMROOT
"
||
(
mkdir
"
$OPAMROOT
"
&&
opam init
--no-setup
-y
)
eval
`
opam conf
env
`
# Make sure the pin for the builddep package is not stale.
run_and_print
make build-dep/opam
make build-dep/opam
# Update repositories
if
test
$(
find
"
$OPAMROOT
/repo/package-index"
-mtime
+0
)
;
then
# last update was more than a day ago
run_and_print opam update
else
# only update iris-dev, and only if it already exists
if
test
-d
"
$OPAMROOT
/repo/iris-dev"
;
then
run_and_print opam update iris-dev
;
fi
fi
opam update
# Make sure we got the right set of repositories registered
if
echo
"
$@
"
| fgrep
"dev"
;
then
if
echo
"
$@
"
| fgrep
"dev"
>
/dev/null
;
then
# We are compiling against a dev version of something. Get ourselves the dev repositories.
test
-d
"
$OPAMROOT
/repo/coq-extra-dev"
||
run_and_print
opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
-p
0
test
-d
"
$OPAMROOT
/repo/coq-core-dev"
||
run_and_print
opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev
-p
5
test
-d
"
$OPAMROOT
/repo/coq-extra-dev"
||
opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
-p
0
test
-d
"
$OPAMROOT
/repo/coq-core-dev"
||
opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev
-p
5
else
# No dev version, make sure we do not have the dev repositories.
test
-d
"
$OPAMROOT
/repo/coq-extra-dev"
&&
run_and_print
opam repo remove coq-extra-dev
test
-d
"
$OPAMROOT
/repo/coq-core-dev"
&&
run_and_print
opam repo remove coq-core-dev
test
-d
"
$OPAMROOT
/repo/coq-extra-dev"
&&
opam repo remove coq-extra-dev
test
-d
"
$OPAMROOT
/repo/coq-core-dev"
&&
opam repo remove coq-core-dev
fi
test
-d
"
$OPAMROOT
/repo/coq-released"
||
run_and_print
opam repo add coq-released https://coq.inria.fr/opam/released
-p
10
test
-d
"
$OPAMROOT
/repo/iris-dev"
||
run_and_print
opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git
-p
20
test
-d
"
$OPAMROOT
/repo/coq-released"
||
opam repo add coq-released https://coq.inria.fr/opam/released
-p
10
test
-d
"
$OPAMROOT
/repo/iris-dev"
||
opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git
-p
20
echo
# We really want to run all of the following in one opam transaction, but due to opam limitations,
...
...
@@ -56,14 +48,14 @@ while (( "$#" )); do # while there are arguments left
echo
"[opam-ci]
$PACKAGE
already
$KIND
-pinned to
$VERSION
"
else
echo
"[opam-ci]
$KIND
-pinning
$PACKAGE
to
$VERSION
"
run_and_print
opam pin add
-y
-k
"
$KIND
"
"
$PACKAGE
"
"
$VERSION
"
opam pin add
-y
-k
"
$KIND
"
"
$PACKAGE
"
"
$VERSION
"
fi
done
# Upgrade cached things.
echo
echo
"[opam-ci] Upgrading opam"
run_and_print
opam upgrade
-y
opam upgrade
-y
--fixup
# Install build-dependencies.
echo
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new 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