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
Rodolphe Lepigre
Iris
Commits
842e85c0
Commit
842e85c0
authored
Sep 19, 2017
by
Ralf Jung
Browse files
CI: tweaks
parent
01b8c312
Changes
3
Hide whitespace changes
Inline
Side-by-side
.gitlab-ci.yml
View file @
842e85c0
...
...
@@ -21,7 +21,7 @@ variables:
-
'
cat
build-log.txt
|
egrep
"[a-zA-Z0-9_/-]+
\((real|user):
[0-9]"
|
tee
build-time.txt'
-
'
if
test
-n
"$VALIDATE"
&&
((
RANDOM
%
10
==
0
));
then
make
validate;
fi'
cache
:
key
:
"
coq$COQ_VERSION-ssr$SSR_VERSION"
key
:
"
coq
.
$COQ_VERSION-ssr
.
$SSR_VERSION"
paths
:
-
opamroot/
only
:
...
...
Makefile
View file @
842e85c0
...
...
@@ -26,8 +26,8 @@ build-dep: phony
mkdir
-p
build-dep
@
sed
<opam
's/^\(build\|install\|remove\):.*/\1: []/; s/^name: *"\(.*\)" */name: "\1-builddep"/'
>
build-dep/opam
@
fgrep builddep build-dep/opam
>
/dev/null
||
(
echo
"sed failed to fix the package name"
&&
exit
1
)
# sanity check
@
# Compute the package name, add the pin and
(
re
)
install
it.
Reinstallation is needed
@
# in case the pin already exists, but the builddep package changed.
# Compute the package name, add the pin and
(
re
)
install
it.
@
#
Reinstallation is needed
in case the pin already exists, but the builddep package changed.
@
BUILD_DEP_PACKAGE
=
"
$$
(egrep "
^name:
" build-dep/opam | sed 's/^name: *"
\(
.
*
\)
" */
\1
/')"
;
\
opam pin add
"
$$
BUILD_DEP_PACKAGE"
"
$
$(pwd)
/build-dep"
-k
path
$(OPAMFLAGS)
&&
\
opam reinstall
"
$$
BUILD_DEP_PACKAGE"
...
...
build/opam-ci.sh
View file @
842e85c0
#!/bin/bash
set
-e
# This script installs the build dependencies for CI builds.
#
# This script installs the build dependencies for CI builds.
# Prepare OPAM configuration
export
OPAMROOT
=
"
$(
pwd
)
/opamroot"
...
...
@@ -44,10 +44,12 @@ while (( "$#" )); do # while there are arguments left
done
# Upgrade cached things.
echo
"[opam-ci] Upgrading opam"
opam upgrade
-y
# Install build-dependencies.
echo
echo
"[opam-ci] Installing build-dependencies"
make build-dep
OPAMFLAGS
=
-y
# done
...
...
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