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
ci
Commits
822ab697
Commit
822ab697
authored
May 28, 2021
by
Ralf Jung
Browse files
support for pinning entire git repos, and adjust the way our nightly jobs look
parent
784fdee7
Changes
2
Hide whitespace changes
Inline
Side-by-side
README.md
View file @
822ab697
...
...
@@ -99,7 +99,9 @@ this end, add a job like this:
build-iris.dev:
<<: *template
variables:
OPAM_PINS: "coq version 8.10.dev coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#$IRIS_REV"
STDPP_REV: "iris/stdpp"
IRIS_REV: "iris/iris"
OPAM_PINS: "coq version 8.10.dev git+https://gitlab.mpi-sws.org/$STDPP_REV git+https://gitlab.mpi-sws.org/$IRIS_REV"
except:
only:
- triggers
...
...
@@ -112,8 +114,11 @@ to the repo, and instead make it run when a pipeline is triggered through the
REST API or by a schedule. The pins are set up to install a development version
of all the dependencies, and the
`8.10`
branch of Coq.
Now ask an admin to set up a pipeline schedule. The schedule should set all the
`_REV`
variables to the branches that should be tested against. We usually only
The
`STDPP_REV`
and
`IRIS_REV`
variables can be set via an API request to test
this repository against different branches or even forks of std++ and Iris (see
the
`build-all`
script in the Iris repository.)
Now ask an admin to set up a pipeline schedule. We usually only
do nightly builds for projects in the iris group; those schedules should be
"owned" by the
`iris-dev`
user so that the Iris development team gets the emails
about broken builds. This can be achieved by having an admin follow these steps:
...
...
prepare-opam.sh
View file @
822ab697
...
...
@@ -85,6 +85,15 @@ status "[prepare-opam] Processing pins"
PINNED_PACKAGES
=
""
while
((
"$#"
))
;
do
# while there are arguments left
PACKAGE
=
"
$1
"
;
shift
# If `PACKAGE` starts with `git+https://`, this is a git repo we should pin for all its packages.
if
[[
"
$PACKAGE
"
==
git+https://
*
]]
;
then
status
"[prepare-opam] pinning all packages in
$PACKAGE
"
opam pin add
-y
-n
"
$PACKAGE
"
# Not adding anything to PINNED_PACKAGES; only pick up the right packages via dependencies.
continue
fi
KIND
=
"
$1
"
;
shift
VERSION
=
"
$1
"
;
shift
...
...
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