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
stdpp
Commits
38b9c399
Commit
38b9c399
authored
Sep 20, 2017
by
Ralf Jung
Browse files
update build system
parent
9b0f7c75
Pipeline
#4471
passed with stages
in 4 minutes and 53 seconds
Changes
2
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
Makefile
View file @
38b9c399
...
...
@@ -4,11 +4,13 @@
all
:
Makefile.coq
+@make
-f
Makefile.coq all
.PHONY
:
all
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
rm
-f
Makefile.coq
.PHONY
:
clean
# Create Coq Makefile. POSIX awk can't do in-place editing, but coq_makefile wants the real
# filename, so we do some file gymnastics.
...
...
@@ -17,16 +19,19 @@ Makefile.coq: _CoqProject Makefile awk.Makefile
mv
Makefile.coq Makefile.coq.tmp
&&
awk
-f
awk.Makefile Makefile.coq.tmp
>
Makefile.coq
&&
rm
Makefile.coq.tmp
# Install build-dependencies
build-dep
:
phony
build-dep/opam
:
# Create the build-dep package.
@
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
build-dep
:
build-dep/opam phony
@
# We want opam to not just instal the build-deps now, but to also keep satisfying these
@
# constraints. Otherwise, `opam upgrade` may well update some packages to versions
@
# 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.
mkdir
-p
build-dep
# Create the build-dep package, add the pin and
(
re
)
install
it.
@
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
# Add the pin and
(
re
)
install
build-dep package.
@
# 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"
.dev
"
$
$(pwd)
/build-dep"
-k
path
$(OPAMFLAGS)
&&
\
...
...
@@ -37,6 +42,6 @@ Makefile: ;
_CoqProject
:
;
awk.Makefile
:
;
# Phony
targets (i.e. targets that should be run no matter the timestamps of the involved files)
# Phony
wildcard targets
phony
:
;
.PHONY
:
all clean
phony
.PHONY
:
phony
build/opam-ci.sh
View file @
38b9c399
#!/bin/bash
set
-e
# This script installs the build dependencies for CI builds.
## This script installs the build dependencies for CI builds.
function
run_and_print
()
{
echo
"
$ $@
"
"
$@
"
}
# 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
)
# Make sure we got a good OPAM
.
test
-d
"
$OPAMROOT
"
||
(
mkdir
"
$OPAMROOT
"
&&
run_and_print
opam init
--no-setup
-y
)
eval
`
opam conf
env
`
# Delete old pins from opam.pins times.
run_and_print opam pin remove coq-stdpp
-n
run_and_print opam pin remove coq-iris
-n
# Make sure the pin for the builddep package is not stale.
run_and_print make build-dep/opam
# Get us all the latest repositories
if
test
$(
find
"
$OPAMROOT
/repo/package-index"
-mtime
+0
)
;
then
# last update was more than a day ago
opam update
run_and_print
opam update
else
echo
"[opam-ci] Not updating opam."
# only update iris-dev
if
test
-d
"
$OPAMROOT
/repo/iris-dev"
;
then
run_and_print opam update iris-dev
;
fi
fi
test
-d
"
$OPAMROOT
/repo/coq-extra-dev"
||
opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
-p
5
test
-d
"
$OPAMROOT
/repo/coq-core-dev"
||
opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev
-p
5
test
-d
"
$OPAMROOT
/repo/coq-released"
||
opam repo add coq-released https://coq.inria.fr/opam/released
-p
10
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 add coq-core-dev https://coq.inria.fr/opam/core-dev
-p
5
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
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
# Install fixed versions of some dependencies
.
echo
while
((
"$#"
))
;
do
# while there are arguments left
PACKAGE
=
"
$1
"
;
shift
VERSION
=
"
$1
"
;
shift
# Check if the pin is already set
if
opam pin list | fgrep
"
$PACKAGE
.
$VERSION
"
>
/dev/null
;
then
echo
"[opam-ci]
$PACKAGE
already pinned to
$VERSION
"
else
echo
"[opam-ci] Pinning
$PACKAGE
to
$VERSION
"
opam pin add
"
$PACKAGE
"
"
$VERSION
"
-k
version
-y
run_and_print
opam pin add
"
$PACKAGE
"
"
$VERSION
"
-k
version
-y
fi
done
# Install build-dependencies
# Upgrade cached things.
echo
echo
"[opam-ci] Upgrading opam"
run_and_print opam upgrade
-y
# Install build-dependencies.
echo
make build-dep
Y
=
1
echo
"[opam-ci] Installing build-dependencies"
make build-dep
OPAMFLAGS
=
-y
# done
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