Commit 2d8a4eb4 authored by Ralf Jung's avatar Ralf Jung

update build system, CI and README

parent 10c2f692
image: ralfjung/opam-ci:latest
stdpp-coq8.5:
tags:
- coq
script:
# prepare
- . build/opam-ci.sh coq 8.5.3
# build
- 'time make -j8'
cache:
key: "coq8.5"
paths:
- opamroot/
only:
- master
- ci
- timing
stdpp-coq8.6:
tags:
- coq
......@@ -10,7 +27,7 @@ stdpp-coq8.6:
- 'time make -j8 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_/-]+ \(user: [0-9]" | tee build-time.txt'
- 'make validate'
- 'if (( RANDOM % 10 == 0 )); then make validate; fi'
cache:
key: "coq8.6"
paths:
......
......@@ -32,9 +32,9 @@ Makefile.coq: _CoqProject Makefile awk.Makefile
build-dep:
build/opam-pins.sh < opam.pins
opam upgrade $(YFLAG) # it is not nice that we upgrade *all* packages here, but I found no nice way to upgrade only those that we pinned
opam pin add coq-stdpp "$$(pwd)#HEAD" -k git -n -y
opam install coq-stdpp --deps-only $(YFLAG)
opam pin remove coq-stdpp
opam pin add opam-builddep-temp "$$(pwd)#HEAD" -k git -n -y
opam install opam-builddep-temp --deps-only $(YFLAG)
opam pin remove opam-builddep-temp
# Some files that do *not* need to be forwarded to Makefile.coq
Makefile: ;
......
......@@ -18,7 +18,7 @@ The key features of this library are as follows:
`naive_solver`, an equality simplifier `simplify_eq`, a solver `solve_proper`
for proving compatibility of functions with respect to relations, and a solver
`set_solver` for goals involving set operations.
- It is entirely axiom free.
- It is entirely dependency- and axiom-free.
## History
......@@ -32,8 +32,8 @@ developed by Robbert Krebbers, Ralf Jung, and Jacques Henri-Jourdan.
This version is known to compile with:
- Coq 8.5pl3 and Coq 8.6
- Coq 8.5pl3 / 8.6
## Building Instructions
Run `make` to build the full development.
Run `make` to build the full development. Run `make install` to install the library.
......@@ -4,18 +4,23 @@ set -e
## Usage:
## ./opam-pins.sh < opam.pins
if ! which curl >/dev/null; then
echo "opam-pins needs curl. Please install curl and try again."
exit 1
fi
# Process stdin
while read PACKAGE URL HASH; do
if echo "$URL" | egrep '^https://gitlab\.mpi-sws\.org' > /dev/null; then
echo "[opam-pins] Recursing into $URL"
# an MPI URL -- try doing recursive pin processing
curl -f "$URL/raw/$HASH" 2> /dev/null | "$0"
curl -f "$URL/raw/$HASH/opam.pins" 2>/dev/null | "$0"
fi
if opam pin list | fgrep "$PACKAGE.dev.$HASH " > /dev/null; then
echo "[opam-pins] $PACKAGE already at commit $HASH"
else
echo "[opam-pins] Applying pin: $PACKAGE -> $URL#$HASH"
opam pin add "$PACKAGE.dev.$HASH" "$URL#$HASH" -k git -y -n
echo
fi
echo
done
......@@ -12,5 +12,5 @@ build: [
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/coq-stdpp'" ]
depends: [
"coq" { ((>= "8.6" & < "8.7~") | (= "dev"))}
"coq" { ((>= "8.5.3" & < "8.7~") | (= "dev"))}
]
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment