From 2d8a4eb49202fb99ca7ba507ed3b6cab771e08e6 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Mon, 6 Feb 2017 16:50:18 +0100
Subject: [PATCH] update build system, CI and README

---
 .gitlab-ci.yml     | 19 ++++++++++++++++++-
 Makefile           |  6 +++---
 README.md          |  6 +++---
 build/opam-pins.sh |  9 +++++++--
 opam               |  2 +-
 5 files changed, 32 insertions(+), 10 deletions(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 9f09343..6ce0d7e 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -1,5 +1,22 @@
 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:
diff --git a/Makefile b/Makefile
index 1a7e330..6394c42 100644
--- a/Makefile
+++ b/Makefile
@@ -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: ;
diff --git a/README.md b/README.md
index 662a72a..11ae0d9 100644
--- a/README.md
+++ b/README.md
@@ -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.
diff --git a/build/opam-pins.sh b/build/opam-pins.sh
index 669cd99..5291cb2 100755
--- a/build/opam-pins.sh
+++ b/build/opam-pins.sh
@@ -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
diff --git a/opam b/opam
index 6cf1701..2b5cdbc 100644
--- a/opam
+++ b/opam
@@ -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"))}
 ]
-- 
GitLab