Basic support for building multiple target architectures in parallel

The builds take place in subdirectories of build/, containing symbolic links
to the actual source files.

Author: xavierleroy

.gitignore

@@ -85,3 +85,5 @@
 .nia.cache
 .nra.cache
 .csdp.cache
+# Build auxiliaries
+/build

Makefile

@@ -245,6 +245,12 @@ ifeq ($(INSTALL_COQDEV),true)
 	$(MAKE) compcert.config
 endif
 
+light:
+	@test -f .depend || $(MAKE) depend
+	$(MAKE) proof
+	$(MAKE) extraction
+	$(MAKE) ccomp
+
 proof: $(FILES:.v=.vo)
 
 extraction: extraction/STAMP
@@ -406,6 +412,7 @@ clean:
 	rm -f tools/ndfun tools/modorder tools/*.cm? tools/*.o
 	rm -f $(GENERATED) .depend
 	rm -f .lia.cache
+	rm -rf build
 	$(MAKE) -f Makefile.extr clean
 	$(MAKE) -C runtime clean
 
@@ -430,6 +437,28 @@ print-includes:
 CoqProject:
 	@echo $(COQINCLUDES) > _CoqProject
 
+ALL_ARCHES=aarch64 arm ppc rv64 x86_32 x86_64
+ALL_BUILDS=$(patsubst %, build/%, $(ALL_ARCHES))
+
+setup-build: FORCE
+	rm -rf build
+	@if [ ! -d .git ]; then echo "build-setup is only available for git checkouts"; exit 2; fi
+	@for a in $(ALL_ARCHES); do \
+           echo "Setting up build/$$a"; \
+           tools/linkhier build/$$a; \
+           (cd build/$$a && ./configure $$a-linux); \
+         done
+
+$(ALL_BUILDS): FORCE
+	@if [ ! -d $@ ]; then echo "$@ is missing, please run 'make setup-build'"; exit 2; fi
+	@echo "$@ started"; \
+         if output=$$($(MAKE) -C $@ light 2>&1); \
+         then echo "$@ succeeded" ; \
+         else echo "$$output"; echo "$@ FAILED"; exit 2; \
+         fi
+
+build-all: $(ALL_BUILDS)
+
 -include .depend
 
 FORCE:

tools/linkhier

@@ -0,0 +1,20 @@
+#!/bin/sh
+# Mirror the hierarchy of source files in the directory given as first argument,
+# using fresh directories and symbolic links for files.
+# The source files are those listed by git ls-files.
+
+set -e
+
+case $# in
+    1) dst="$1";;
+    *) echo "Usage: linkhier <destination directory>" 1>&2; exit 2;;
+esac
+
+src=$(pwd)
+files=$(git ls-files --recurse-submodules)
+mkdir -p "$dst"
+cd "$dst"
+mkdir -p $(dirname $files | sort -u)
+for f in $files; do
+  ln -sf "$src/$f" "$f"
+done