Skip to content
Projects
Groups
Snippets
Help
Loading...
Help
Support
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
I
iris-atomic
Project
Project
Details
Activity
Releases
Cycle Analytics
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Charts
Issues
3
Issues
3
List
Boards
Labels
Milestones
Merge Requests
0
Merge Requests
0
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Charts
Wiki
Wiki
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Charts
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
FP
iris-atomic
Commits
deacc8fc
Commit
deacc8fc
authored
Jun 08, 2018
by
Ralf Jung
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
update CI and Makefile
parent
22062ce4
Pipeline
#9483
canceled with stage
in 1 minute and 2 seconds
Changes
7
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
Showing
7 changed files
with
16 additions
and
101 deletions
+16
-101
.gitignore
.gitignore
+1
-0
.gitlab-ci.yml
.gitlab-ci.yml
+2
-15
.gitmodules
.gitmodules
+3
-0
Makefile
Makefile
+9
-6
awk.Makefile
awk.Makefile
+0
-12
opam-ci.sh
build/opam-ci.sh
+0
-68
ci
ci
+1
-0
No files found.
.gitignore
View file @
deacc8fc
...
...
@@ -13,3 +13,4 @@ Makefile.coq.conf
.coq-native/
build-dep
_opam
.coqdeps.d
.gitlab-ci.yml
View file @
deacc8fc
...
...
@@ -5,21 +5,14 @@ stages:
variables
:
CPU_CORES
:
"
10"
GIT_SUBMODULE_STRATEGY
:
"
recursive"
.template
:
&template
stage
:
build
tags
:
-
fp
script
:
# prepare
-
. build/opam-ci.sh $OPAM_PINS
-
env | egrep '^(CI_BUILD_REF|CI_RUNNER)' > build-env.txt
# build
-
'
time
make
-k
-j$CPU_CORES
TIMED=y
2>&1
|
tee
build-log.txt'
-
'
if
fgrep
Axiom
build-log.txt
>/dev/null;
then
exit
1;
fi'
-
'
cat
build-log.txt
|
egrep
"[a-zA-Z0-9_/-]+
\((real|user):
[0-9]"
|
tee
build-time.txt'
# maybe validate
-
'
if
[[
-n
"$VALIDATE"
]];
then
make
validate;
fi'
-
ci/buildjob
cache
:
key
:
"
$CI_JOB_NAME"
paths
:
...
...
@@ -37,12 +30,6 @@ build-coq.8.7.1:
<<
:
*template
variables
:
OPAM_PINS
:
"
coq
version
8.7.1
coq-mathcomp-ssreflect
version
1.6.4"
tags
:
-
fp-timing
artifacts
:
paths
:
-
build-time.txt
-
build-env.txt
build-coq.8.6.1
:
<<
:
*template
...
...
.gitmodules
0 → 100644
View file @
deacc8fc
[submodule "ci"]
path = ci
url = https://gitlab.mpi-sws.org/FP/iris-ci.git
Makefile
View file @
deacc8fc
...
...
@@ -8,7 +8,7 @@ all: Makefile.coq
clean
:
Makefile.coq
+@make
-f
Makefile.coq clean
find theories
\(
-name
"*.v.d"
-o
-name
"*.vo"
-o
-name
"*.aux"
-o
-name
"*.cache"
-o
-name
"*.glob"
-o
-name
"*.vio"
\)
-print
-delete
find theories
$$
(
test
-d
tests
&&
echo
tests
)
\(
-name
"*.v.d"
-o
-name
"*.vo"
-o
-name
"*.aux"
-o
-name
"*.cache"
-o
-name
"*.glob"
-o
-name
"*.vio"
\)
-print
-delete
rm
-f
Makefile.coq
.PHONY
:
clean
...
...
@@ -20,7 +20,7 @@ Makefile.coq: _CoqProject Makefile awk.Makefile
# Install build-dependencies
build-dep/opam
:
opam Makefile
# Creating the build-dep package.
@
echo
"# Creating build-dep package."
@
mkdir
-p
build-dep
@
sed
<opam
-E
'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
...
...
@@ -31,12 +31,15 @@ build-dep: build-dep/opam phony
@
# that are incompatible with our build requirements.
@
# To achieve this, we create a fake opam package that has our build-dependencies as
@
# dependencies, but does not actually install anything.
@
# Upgrading 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
/')"
;
\
@
# Reinstalling is needed with opam 1 in case the pin already exists, but the builddep
@
# package changed.
@
BUILD_DEP_PACKAGE
=
"
$$
(egrep "
^name:
" build-dep/opam | sed 's/^name: *"
\(
.
*
\)
" */
\1
/')"
&&
\
echo
"# Pinning build-dep package."
&&
\
opam pin add
-k
path
$(OPAMFLAGS)
"
$$
BUILD_DEP_PACKAGE"
.dev build-dep
&&
\
echo
"# Updating build-dep package."
&&
\
opam upgrade
"
$$
BUILD_DEP_PACKAGE"
((!
opam
--version
|
grep
"^1
\.
"
>
/dev/null
)
||
(
\
echo
"# Reinstalling build-dep package."
&&
\
opam reinstall
$(OPAMFLAGS)
"
$$
BUILD_DEP_PACKAGE"
\
))
# Some files that do *not* need to be forwarded to Makefile.coq
Makefile
:
;
...
...
awk.Makefile
View file @
deacc8fc
...
...
@@ -19,17 +19,5 @@
next
}
# Add new target quick2vo to (a) run "make quick" with the same number of jobs, ensuring
# that the .vio files are up-to-date, and (b) only schedule vio2vo for those
# files where the .vo is *older* than the .vio.
/^vio2vo:/ {
print "quick2vo:";
print "\t@make -j $(J) quick"
print "\t@VIOFILES=$$(for vofile in $(VOFILES); do viofile=\"$$(echo \"$$vofile\" | sed \"s/\\.vo/.vio/\")\"; if [ \"$$vofile\" -ot \"$$viofile\" -o ! -e \"$$vofile\" ]; then echo -n \"$$viofile \"; fi; done); \\"
print "\t echo \"VIO2VO: $$VIOFILES\"; \\"
print "\t if [ -n \"$$VIOFILES\" ]; then $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $$VIOFILES; fi"
print ".PHONY: quick2vo"
}
# This forwards all unchanged lines
1
build/opam-ci.sh
deleted
100755 → 0
View file @
22062ce4
#!/bin/bash
set
-e
set
-x
## This script installs the build dependencies for CI builds.
# Prepare OPAM configuration
export
OPAMROOT
=
"
$(
pwd
)
/opamroot"
export
OPAMJOBS
=
"
$((
2
*
$CPU_CORES
))
"
export
OPAM_EDITOR
=
"
$(
which
false
)
"
# Make sure we got a good OPAM.
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.
make build-dep/opam
# Update repositories
opam update
# Make sure we got the right set of repositories registered
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"
||
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"
&&
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"
||
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,
# that is not currently possible.
# Install fixed versions of some dependencies.
echo
while
((
"$#"
))
;
do
# while there are arguments left
PACKAGE
=
"
$1
"
;
shift
KIND
=
"
$1
"
;
shift
VERSION
=
"
$1
"
;
shift
# Check if the pin is already set
read
-a
PIN
<<<
$(
opam pin list |
(
egrep
"^
$PACKAGE
[. ]"
)
)
if
[[
"
${
PIN
[1]
}
"
==
"
$KIND
"
&&
"
${
PIN
[2]
}
"
==
"
$VERSION
"
]]
;
then
echo
"[opam-ci]
$PACKAGE
already
$KIND
-pinned to
$VERSION
"
else
echo
"[opam-ci]
$KIND
-pinning
$PACKAGE
to
$VERSION
"
opam pin add
-y
-k
"
$KIND
"
"
$PACKAGE
"
"
$VERSION
"
fi
done
# Upgrade cached things.
echo
echo
"[opam-ci] Upgrading opam"
opam upgrade
-y
--fixup
&&
opam upgrade
-y
# Install build-dependencies.
echo
echo
"[opam-ci] Installing build-dependencies"
make build-dep
OPAMFLAGS
=
-y
# done
set
+x
echo
coqc
-v
ci
@
16c8b610
Subproject commit 16c8b6107119db3448b6828d3d2757888f2b2376
Write
Preview
Markdown
is supported
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