From 76ab524320e3d4c006c6c94372e0cfda2b62c76e Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 22 Oct 2020 15:30:30 +0200
Subject: Build all_stdlib.v in test suite makefile

instead of recursive make
---
 .gitlab-ci.yml      | 2 --
 Makefile.build      | 8 ++------
 Makefile.common     | 2 --
 Makefile.make       | 1 -
 test-suite/Makefile | 3 ++-
 5 files changed, 4 insertions(+), 12 deletions(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 18ea50d77b..99ae4c23ce 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -78,7 +78,6 @@ before_script:
       - config/Makefile
       - config/coq_config.py
       - config/coq_config.ml
-      - test-suite/misc/universes/all_stdlib.v
       - dmesg.txt
     expire_in: 1 week
   script:
@@ -95,7 +94,6 @@ before_script:
     - echo 'start:coq.build'
     - make -j "$NJOBS" byte
     - make -j "$NJOBS" world $EXTRA_TARGET
-    - make test-suite/misc/universes/all_stdlib.v
     - echo 'end:coq:build'
 
     - echo 'start:coq.install'
diff --git a/Makefile.build b/Makefile.build
index 526a8c5831..b307bde5df 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -603,7 +603,7 @@ $(CSDPCERTBYTE): $(CSDPCERTCMO)
 # tests
 ###########################################################################
 
-.PHONY: validate check test-suite $(ALLSTDLIB).v
+.PHONY: validate check test-suite
 
 VALIDOPTS=$(if $(VERBOSE),,-silent) -o -m -coqlib .
 
@@ -611,15 +611,11 @@ validate: $(CHICKEN) | $(ALLVO:.$(VO)=.vo)
 	$(SHOW)'COQCHK <theories & plugins>'
 	$(HIDE)$(CHICKEN) $(VALIDOPTS) $(ALLVO)
 
-$(ALLSTDLIB).v:
-	$(SHOW)'MAKE $(notdir $@)'
-	$(HIDE)echo "Require $(ALLMODS)." > $@
-
 MAKE_TSOPTS=-C test-suite -s VERBOSE=$(VERBOSE)
 
 check: validate test-suite
 
-test-suite: world byte $(ALLSTDLIB).v
+test-suite: world byte
 	$(MAKE) $(MAKE_TSOPTS) clean
 	$(MAKE) $(MAKE_TSOPTS) all
 
diff --git a/Makefile.common b/Makefile.common
index 1f59bff183..82d9b89c4f 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -179,8 +179,6 @@ PLUGINSOPT:=$(PLUGINSCMO:.cmo=.cmxs)
 LINKCMO:=$(CORECMA) $(STATICPLUGINS)
 LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cmo=.cmx)
 
-ALLSTDLIB := test-suite/misc/universes/all_stdlib
-
 PLUGINTUTO := doc/plugin_tutorial
 
 # For emacs:
diff --git a/Makefile.make b/Makefile.make
index 34f5707ae8..2f6781439c 100644
--- a/Makefile.make
+++ b/Makefile.make
@@ -253,7 +253,6 @@ docclean:
 
 archclean: clean-ide optclean voclean plugin-tutorialclean
 	rm -rf _build _build_boot
-	rm -f $(ALLSTDLIB).*
 
 optclean:
 	rm -f $(COQTOPEXE) $(CHICKEN) $(TOPBINOPT)
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 279f32c903..cee54f691c 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -144,6 +144,7 @@ bugs: $(BUGS)
 clean:
 	rm -f trace .csdp.cache .nia.cache .lia.cache output/MExtraction.out
 	rm -f vos/Makefile vos/Makefile.conf
+	rm -f misc/universes/all_stdlib.v
 	$(SHOW) 'RM        <**/*.stamp> <**/*.vo> <**/*.vio> <**/*.log> <**/*.glob>'
 	$(HIDE)find . \( \
 	  -name '*.stamp' -o -name '*.vo' -o -name '*.vio' -o -name '*.vos' -o -name '*.vok' -o -name '*.log' -o -name '*.glob' \
@@ -649,7 +650,7 @@ misc: $(patsubst %.sh,%.log,$(wildcard misc/*.sh))
 misc/universes.log: misc/universes/all_stdlib.v
 
 misc/universes/all_stdlib.v:
-	cd .. && $(MAKE) test-suite/$@
+	cd misc/universes && ./build_all_stdlib.sh > all_stdlib.v
 
 $(patsubst %.sh,%.log,$(wildcard misc/*.sh)): %.log: %.sh $(PREREQUISITELOG)
 	@echo "TEST      $<"
-- 
cgit v1.2.3