diff options
| author | Gaëtan Gilbert | 2020-10-22 15:30:30 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-11-20 16:52:58 +0100 |
| commit | 76ab524320e3d4c006c6c94372e0cfda2b62c76e (patch) | |
| tree | 043f0194d8956e15701cb083ebcd68c21b1aa13c | |
| parent | 614675fa5337cca0621ae7a65d4fd47a6ad8f788 (diff) | |
Build all_stdlib.v in test suite makefile
instead of recursive make
| -rw-r--r-- | .gitlab-ci.yml | 2 | ||||
| -rw-r--r-- | Makefile.build | 8 | ||||
| -rw-r--r-- | Makefile.common | 2 | ||||
| -rw-r--r-- | Makefile.make | 1 | ||||
| -rw-r--r-- | 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 $<" |