summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2009-02-01 09:42:17 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2009-02-01 11:09:59 +0100
commit10d514272045c3c2551de78c95bcc3175cf29483 (patch)
treea882cecd06cbb125008cc07e28a3dd1da2947cdd
parent7525ef9a5b242fd5246917df663b2967851eafb2 (diff)
Add a build cache (see README.source)
-rw-r--r--debian/README.source9
-rwxr-xr-xdebian/rules11
2 files changed, 17 insertions, 3 deletions
diff --git a/debian/README.source b/debian/README.source
index cdd4070d..a88c4753 100644
--- a/debian/README.source
+++ b/debian/README.source
@@ -38,3 +38,12 @@ option). Debian changelog can be updated based on git changelog using
git-dch. Please consider reading the documentation of these tools.
It was versioned with subversion until Wed, 23 Jul 2008.
+
+
+Build cache
+-----------
+
+Since Coq takes so much time to compile, there is a build cache to
+speed-up Debian development and debugging. Just copy a previous build
+to ../coq.cache, and debian/rules will detect its presence and rsync
+from there instead of really compiling Coq...
diff --git a/debian/rules b/debian/rules
index 16f51676..3de9b108 100755
--- a/debian/rules
+++ b/debian/rules
@@ -4,6 +4,9 @@
# Uncomment this to turn on verbose mode.
#export DH_VERBOSE=1
+# Build cache (for accelerating Debian debugging)
+BUILDCACHE := $(wildcard ../coq.cache)
+
# This has to be exported to make some magic below work.
export COQTEST_SKIPCOMPLEXITY = true
export CAML_LD_LIBRARY_PATH = $(shell pwd)/kernel/byterun
@@ -53,10 +56,12 @@ configure-stamp: patch-stamp ocamlinit-stamp
build: build-stamp
build-stamp: configure-stamp
dh_testdir
+ifeq ($(BUILDCACHE),)
$(MAKE) STRIP=true check
- if [ -f bin/coqtop.opt ]; then touch opt-stamp; fi
- $(MAKE) COQDOC="bin/coqdoc --coqlib_path `pwd`" \
- DOC_TARGETS=$(HTMLDOC) $(HTMLDOC)
+ $(MAKE) DOC_TARGETS=$(HTMLDOC) $(HTMLDOC)
+else
+ rsync -a --exclude=debian --exclude=.git $(BUILDCACHE)/ .
+endif
dh build --after dh_auto_test
touch $@