Commit 64ec23fe authored by Ralf Jung's avatar Ralf Jung
Browse files

update CI and build system and Iris

parent 6d98dc66
......@@ -9,6 +9,6 @@
......@@ -16,7 +16,7 @@ variables:
- 'cat build-log.txt | egrep "[a-zA-Z0-9_/-]+ \(user: [0-9]" | tee build-time.txt'
- 'if test -n "$VALIDATE" && (( RANDOM % 10 == 0 )); then make validate; fi'
key: "coq.$COQ_VERSION-ssr.$SSR_VERSION"
- opamroot/
# Process flags
ifeq ($(Y), 1)
# Forward most targets to Coq makefile (with some trick to make this phony)
%: Makefile.coq phony
+@make -f Makefile.coq $@
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.
# Create Coq Makefile. POSIX awk can't do in-place editing, but coq_makefile wants the real
# filename, so we do some file gymnastics.
Makefile.coq: _CoqProject Makefile awk.Makefile
coq_makefile -f _CoqProject -o Makefile.coq
mv Makefile.coq Makefile.coq.tmp && awk -f awk.Makefile Makefile.coq.tmp > Makefile.coq && rm Makefile.coq.tmp
# Install build-dependencies
build/ < 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 opam-builddep-temp "$$(pwd)#HEAD" -k git -n -y
opam install opam-builddep-temp --deps-only $(YFLAG)
opam pin remove opam-builddep-temp
build-dep/opam: 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.
# 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) && \
opam reinstall "$$BUILD_DEP_PACKAGE"
# Some files that do *not* need to be forwarded to Makefile.coq
Makefile: ;
_CoqProject: ;
awk.Makefile: ;
opam: ;
# 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
@# This makes sure we also delete stale files in the destination directory
$(HIDE)df="$(COQLIBINSTALL)/`$(COQMKFILE) -destination-of "theories/base.v" $(COQLIBS)`" &&\
echo "RM in $$df" &&\
if [ -d "$$df" ]; then find "$$df" \( -name "*.vo" -o -name "*.v" -o -name "*.glob" -o \( -type d -empty \) \) -print -delete; fi
......@@ -11,7 +11,8 @@
# Patch the uninstall target to work properly, and to also uninstall stale files.
# Also see <>.
/^uninstall:/ {
# This (and the section above) can be removed once we no longer support Coq 8.6.
/^uninstall: / {
print "uninstall:";
print "\tif [ -d \"$(DSTROOT)\"$(COQLIBINSTALL)/"PROJECT"/ ]; then find \"$(DSTROOT)\"$(COQLIBINSTALL)/"PROJECT"/ \\( -name \"*.vo\" -o -name \"*.v\" -o -name \"*.glob\" -o \\( -type d -empty \\) \\) -print -delete; fi";
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
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
test -d "$OPAMROOT/repo/coq-extra-dev" || opam repo add coq-extra-dev -p 5
test -d "$OPAMROOT/repo/coq-core-dev" || opam repo add coq-core-dev -p 5
test -d "$OPAMROOT/repo/coq-released" || opam repo add coq-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 -p 5
test -d "$OPAMROOT/repo/coq-released" || run_and_print opam repo add coq-released -p 10
test -d "$OPAMROOT/repo/iris-dev" || run_and_print opam repo add iris-dev -p 20
# 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.
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"
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
# Install build-dependencies
# Upgrade cached things.
echo "[opam-ci] Upgrading opam"
run_and_print opam upgrade -y
# Install build-dependencies.
make build-dep Y=1
echo "[opam-ci] Installing build-dependencies"
make build-dep OPAMFLAGS=-y
# done
set -e
## Process an opam.pins file from stdin: Add all the given pins, but don't install anything.
## Usage:
## ./ < opam.pins
if ! which curl >/dev/null; then
echo "opam-pins needs curl. Please install curl and try again."
exit 1
# 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/opam.pins" 2>/dev/null | "$0"
if opam pin list | fgrep "$$HASH " > /dev/null; then
echo "[opam-pins] $PACKAGE already at commit $HASH"
echo "[opam-pins] Applying pin: $PACKAGE -> $URL#$HASH"
opam pin add "$$HASH" "$URL#$HASH" -k git -y -n
opam-version: "1.2"
name: "coq-iris-atomic"
version: "dev"
maintainer: "Zhen Zhang, Ralf Jung"
authors: "Zhen Zhang"
homepage: ""
bug-reports: ""
dev-repo: ""
build: [
[make "-j%{jobs}%"]
build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris_atomic" ]
depends: [
"coq-iris" { (= "dev.2017-09-21.3") | (= "dev") }
coq-iris 398bae9d092b6568cf8d504ca98d8810979eea33
((coq-mode . ((coq-prog-name . "/usr/local/bin/coqtop"))))
......@@ -154,7 +154,7 @@ Section proof.
iModIntro. wp_match. wp_proj. wp_proj.
wp_bind (f _). iApply wp_wand_r. iSplitL "Hpx Hf' HR".
{ iApply "Hf'". iFrame. }
iIntros (v) "[HR HQ]". wp_value.
iIntros (v) "[HR HQ]".
iInv N as "Hx" "Hclose".
iDestruct "Hx" as "[Hp | [Hp | [Hp | Hp]]]"; subst.
* iDestruct "Hp" as (?) "(_ & >Ho1' & _)".
......@@ -191,12 +191,12 @@ Section proof.
induction xs as [|x xs' IHxs].
- iIntros (hd Φ) "[Hxs ?] HΦ".
simpl. wp_rec. wp_value. wp_let.
simpl. wp_rec. wp_let.
iDestruct "Hxs" as (?) "Hhd".
wp_load. wp_match. by iApply "HΦ".
- iIntros (hd Φ) "[Hxs HRf] HΦ". simpl.
iDestruct "Hxs" as (hd' ?) "(Hhd & #Hinv & Hxs')".
wp_rec. wp_value. wp_let. wp_bind (! _)%E.
wp_rec. wp_let. wp_bind (! _)%E.
iInv N as "H" "Hclose".
iDestruct "H" as (ts p) "[>% #?]". subst.
wp_load. iMod ("Hclose" with "[]").
......@@ -291,7 +291,7 @@ Section proof.
iDestruct "Hs" as (Q') "(Hx' & HoQ' & HQ')".
destruct (decide (x = a)) as [->|Hneq].
- iDestruct (saved_prop_agree with "[$HoQ] [HoQ']") as "Heq"; first by iFrame.
wp_let. iDestruct (uPred.cofe_funC_equivI with "Heq") as "Heq".
wp_let. iDestruct (uPred.ofe_funC_equivI with "Heq") as "Heq".
iSpecialize ("Heq" $! a0). by iRewrite -"Heq" in "HQ'".
- iExFalso. iCombine "Hx" "Hx'" as "Hx".
iDestruct (own_valid with "Hx") as %[_ H1].
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