aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-05-29 09:14:53 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-05-29 09:14:53 +0000
commitbf7cfcf92c45af9f559f5bf004e9730d96921850 (patch)
tree3f69021619d4731e559076f0616b3566f2ec341f
parentbdeccec95e1d018ffb18af9209060a9806d0235a (diff)
Makefile: avoid too much exported vars (for win32)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15366 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--Makefile36
-rw-r--r--Makefile.build12
2 files changed, 34 insertions, 14 deletions
diff --git a/Makefile b/Makefile
index 847c403e0..a861a2d0a 100644
--- a/Makefile
+++ b/Makefile
@@ -39,9 +39,13 @@
# File lists
###########################################################################
+# NB: due to limitations in Win32, please refrain using 'export' too much
+# to communicate between make sub-calls (in Win32, 8kb max per env variable,
+# 32kb total)
+
# !! Before using FIND_VCS_CLAUSE, please read how you should in the !!
# !! FIND_VCS_CLAUSE section of dev/doc/build-system.dev.txt !!
-export FIND_VCS_CLAUSE:='(' \
+FIND_VCS_CLAUSE:='(' \
-name '{arch}' -o \
-name '.svn' -o \
-name '_darcs' -o \
@@ -58,8 +62,8 @@ endef
## Files in the source tree
-export YACCFILES:=$(call find, '*.mly')
-export LEXFILES := $(call find, '*.mll')
+YACCFILES:=$(call find, '*.mly')
+LEXFILES := $(call find, '*.mll')
export MLLIBFILES := $(call find, '*.mllib')
export ML4FILES := $(call find, '*.ml4')
export CFILES := $(call find, '*.c')
@@ -73,13 +77,13 @@ EXISTINGMLI := $(call find, '*.mli')
## Files that will be generated
-export GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) \
+GENML4FILES:= $(ML4FILES:.ml4=.ml)
+GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) \
scripts/tolink.ml kernel/copcodes.ml
-export GENMLIFILES:=$(YACCFILES:.mly=.mli)
+GENMLIFILES:=$(YACCFILES:.mly=.mli)
+GENPLUGINSMOD:=$(filter plugins/%,$(MLLIBFILES:%.mllib=%_mod.ml))
export GENHFILES:=kernel/byterun/coq_jumptbl.h
export GENVFILES:=theories/Numbers/Natural/BigN/NMake_gen.v
-export GENPLUGINSMOD:=$(filter plugins/%,$(MLLIBFILES:%.mllib=%_mod.ml))
-export GENML4FILES:= $(ML4FILES:.ml4=.ml)
export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) $(GENVFILES) $(GENPLUGINSMOD)
# NB: all files in $(GENFILES) can be created initially, while
@@ -92,12 +96,9 @@ define diff
$(strip $(foreach f, $(1), $(if $(filter $(f),$(2)),,$f)))
endef
-export MLSTATICFILES := \
- $(call diff, $(EXISTINGML), $(GENMLFILES) $(GENML4FILES) $(GENPLUGINSMOD))
-export MLFILES := \
- $(sort $(EXISTINGML) $(GENMLFILES) $(GENML4FILES) $(GENPLUGINSMOD))
+export MLEXTRAFILES := $(GENMLFILES) $(GENML4FILES) $(GENPLUGINSMOD)
+export MLSTATICFILES := $(call diff, $(EXISTINGML), $(MLEXTRAFILES))
export MLIFILES := $(sort $(GENMLIFILES) $(EXISTINGMLI))
-export MLWITHOUTMLI := $(call diff, $(MLFILES), $(MLIFILES:.mli=.ml))
include Makefile.common
@@ -262,3 +263,14 @@ ifdef COQ_CONFIGURED
else
@echo "Please run ./configure first" >&2; exit 1
endif
+
+# Useful to check that the exported variables are within the win32 limits
+
+printenv:
+ @env
+ @echo
+ @echo -n "Maxsize (win32 limit is 8k) : "
+ @env | wc -L
+ @echo -n "Total (win32 limit is 32k) : "
+ @env | wc -m
+
diff --git a/Makefile.build b/Makefile.build
index bae04da3c..0c14f2354 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -36,10 +36,12 @@ endif
# of include, and they will then be automatically deleted, leading to an
# infinite loop.
-ALLDEPS=$(addsuffix .d, \
+MLFILES:=$(MLSTATICFILES) $(MLEXTRAFILES)
+
+ALLDEPS:=$(addsuffix .d, \
$(ML4FILES) $(MLFILES) $(MLIFILES) $(CFILES) $(MLLIBFILES) $(VFILES))
-.SECONDARY: $(ALLDEPS) $(GENFILES) $(GENML4FILES)
+.SECONDARY: $(ALLDEPS) $(GENFILES) $(ML4FILES:.ml4=.ml)
# NOTA: the -include below will lauch the build of all .d. Some of them
# will _fail_ at first, this is to be expected (no grammar.cma initially).
@@ -839,6 +841,12 @@ COND_OPTFLAGS= \
HACKMLI = $(if $(wildcard $<i),,-intf-suffix .cmi)
+define diff
+ $(strip $(foreach f, $(1), $(if $(filter $(f),$(2)),,$f)))
+endef
+
+MLWITHOUTMLI := $(call diff, $(MLFILES), $(MLIFILES:.mli=.ml))
+
$(MLWITHOUTMLI:.ml=.cmx): %.cmx: %.cmi # for .ml with .mli this is already the case
$(MLWITHOUTMLI:.ml=.cmi): %.cmi: %.cmo