From 831ceb0f81385aa7b47c126b076d8766aca6067e Mon Sep 17 00:00:00 2001
From: Claude Marche <Claude.Marche@inria.fr>
Date: Sat, 6 Dec 2014 08:50:25 +0100
Subject: [PATCH] do not rebuild isabelle heap at each run of make

---
 Makefile.in | 36 ++++++++++++++++++++----------------
 1 file changed, 20 insertions(+), 16 deletions(-)

diff --git a/Makefile.in b/Makefile.in
index f15488693..d358a94aa 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -1114,28 +1114,31 @@ drivers/isabelle-realizations.aux: Makefile
 	echo 'theory option.'"$$f"' meta "realized_theory" "option.'"$$f"'", "" end'; done; \
 	) > $@
 
-install_no_local::
-	cp -r lib/isabelle "$(LIBDIR)/why3"
-	cp drivers/isabelle-realizations.aux "$(DATADIR)/why3/drivers/"
-	@(if isabelle components -l | grep -q "$(LIBDIR)/why3/isabelle$$"; then \
-	    echo "Building the Why3 heap for Isabelle/HOL:"; \
-	    isabelle build -bc Why3; true; \
-	  else \
-	    echo "[Warning] Cannot pre-build the Isabelle heap because"; \
-	    echo "  the Isabelle component configuration does not contain"; \
-            echo "  [$(LIBDIR)/why3/isabelle]"; \
-	  fi)
+ifeq (@enable_local@,yes)
+  ISABELLE_TARGET_DIR=`pwd`/lib/isabelle
+else
+  ISABELLE_TARGET_DIR=$(LIBDIR)/why3/isabelle
+endif
 
-install_local::
-	@(if isabelle components -l | grep -q "`pwd`/lib/isabelle$$"; then \
+lib/isabelle/last_build: $(ISABELLELIBS_INT) $(ISABELLELIBS_BOOL) $(ISABELLELIBS_REAL) $(ISABELLELIBS_NUMBER) $(ISABELLELIBS_SET) $(ISABELLELIBS_MAP) $(ISABELLELIBS_LIST) $(ISABELLELIBS_OPTION)
+	@(if isabelle components -l | grep -q "$(ISABELLE_TARGET_DIR)$$"; then \
 	    echo "Building the Why3 heap for Isabelle/HOL:"; \
-	    isabelle build -bc Why3; true; \
+	    isabelle build -bc Why3; \
+	    touch $@; \
 	  else \
 	    echo "[Warning] Cannot pre-build the Isabelle heap because"; \
 	    echo "  the Isabelle component configuration does not contain"; \
-            echo "  [`pwd`/lib/isabelle]"; \
+	    echo "  [$(ISABELLE_TARGET_DIR)]"; \
 	  fi)
 
+install_no_local::
+	cp -r lib/isabelle "$(LIBDIR)/why3"
+	cp drivers/isabelle-realizations.aux "$(DATADIR)/why3/drivers/"
+
+install_no_local:: lib/isabelle/last_build
+
+install_local:: lib/isabelle/last_build
+
 update-isabelle: $(ISABELLELIBS_INT) $(ISABELLELIBS_BOOL) $(ISABELLELIBS_REAL) $(ISABELLELIBS_NUMBER) $(ISABELLELIBS_SET) $(ISABELLELIBS_MAP) $(ISABELLELIBS_LIST) $(ISABELLELIBS_OPTION)
 
 $(ISABELLELIBS_INT): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
@@ -1178,7 +1181,8 @@ $(ISABELLELIBS_OPTION): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realization
 	mkdir -p lib/isabelle/option
 	WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/isabelle-realize.drv -T option.$(notdir $(basename $@)) -o lib/isabelle/option/
 
-opt byte: update-isabelle
+# do not update isabelle realizations systematically
+# opt byte: update-isabelle
 
 clean::
 	rm -f lib/isabelle/*/*.xml
-- 
GitLab