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
4f73ad57
Commit
4f73ad57
authored
Apr 24, 2018
by
Ralf Jung
Browse files
update CI
parent
a66aa086
Pipeline
#8233
canceled with stage
Changes
6
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
.gitlab-ci.yml
View file @
4f73ad57
...
...
@@ -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
:
...
...
@@ -33,16 +26,14 @@ variables:
## Build jobs
build-coq.8.7.
1
:
build-coq.8.7.
2
:
<<
:
*template
variables
:
OPAM_PINS
:
"
coq
version
8.7.1
coq-mathcomp-ssreflect
version
1.6.4"
OPAM_PINS
:
"
coq
version
8.7.2
coq-mathcomp-ssreflect
version
1.6.4"
TIMING_PROJECT
:
"
iris-examples"
TIMING_CONF
:
"
coq-8.7.2"
tags
:
-
fp-timing
artifacts
:
paths
:
-
build-time.txt
-
build-env.txt
build-coq.8.6.1
:
<<
:
*template
...
...
@@ -52,7 +43,7 @@ build-coq.8.6.1:
build-iris.dev
:
<<
:
*template
variables
:
OPAM_PINS
:
"
coq
version
8.7.
1
coq-mathcomp-ssreflect
version
1.6.4
coq-iris.dev
git
https://gitlab.mpi-sws.org/FP/iris-coq.git#$IRIS_REV"
OPAM_PINS
:
"
coq
version
8.7.
2
coq-mathcomp-ssreflect
version
1.6.4
coq-iris.dev
git
https://gitlab.mpi-sws.org/FP/iris-coq.git#$IRIS_REV"
except
:
only
:
-
triggers
...
...
.gitmodules
0 → 100644
View file @
4f73ad57
[submodule "ci"]
path = ci
url = https://gitlab.mpi-sws.org/FP/iris-ci.git
Makefile
View file @
4f73ad57
...
...
@@ -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,13 @@ 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.
@
# Reinstalling is needed in case the pin already exists, but the builddep package changed.
@
# Once we depend on opam 2, we can remove that last step.
@
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
"#
Updat
ing build-dep package."
&&
\
opam
upgrade
"
$$
BUILD_DEP_PACKAGE"
echo
"#
Reinstall
ing build-dep package."
&&
\
opam
reinstall
$(OPAMFLAGS)
"
$$
BUILD_DEP_PACKAGE"
# Some files that do *not* need to be forwarded to Makefile.coq
Makefile
:
;
...
...
README.md
View file @
4f73ad57
...
...
@@ -6,7 +6,7 @@ Some example verification demonstrating the use of Iris.
This version is known to compile with:
-
Coq 8.6.1 / 8.7.
1
-
Coq 8.6.1 / 8.7.
2
-
Ssreflect 1.6.4
-
A development version of
[
Iris
](
https://gitlab.mpi-sws.org/FP/iris-coq/
)
-
The coq86-devel branch of
[
Autosubst
](
https://github.com/uds-psl/autosubst
)
...
...
awk.Makefile
View file @
4f73ad57
...
...
@@ -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
ci
@
40b71102
Subproject commit 40b71102efe051c777a785035aebcbaa4c2ec19f
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