diff options
author | François Pottier <francois.pottier@inria.fr> | 2015-10-16 11:30:16 +0200 |
---|---|---|
committer | François Pottier <francois.pottier@inria.fr> | 2015-10-16 11:30:16 +0200 |
commit | 153651d6f959f9a18a47441f2e7280046b590f1e (patch) | |
tree | df4a6fb46d1c7b85f0fcb48d9ce84379bf7fea91 /Makefile.menhir | |
parent | 7d68132721bb4c12de8b846717972a25899ecc3f (diff) | |
download | compcert-153651d6f959f9a18a47441f2e7280046b590f1e.tar.gz compcert-153651d6f959f9a18a47441f2e7280046b590f1e.zip |
Added [Makefile.menhir], which gives a choice between Menhir's "code" and "table" back-ends when compiling CompCert.
For now, MENHIR_TABLE is set to false, so CompCert is not affected.
Setting MENHIR_TABLE to true builds CompCert using Menhir's table back-end.
This causes a small but repeatable slowdown on "make test", about 2% (roughly 1 second out of 40).
I have tested building ccomp and ccomp.byte.
I have tested with an ocamlfind-installed menhir and with a manually-installed menhir.
Diffstat (limited to 'Makefile.menhir')
-rw-r--r-- | Makefile.menhir | 67 |
1 files changed, 67 insertions, 0 deletions
diff --git a/Makefile.menhir b/Makefile.menhir new file mode 100644 index 00000000..414279ab --- /dev/null +++ b/Makefile.menhir @@ -0,0 +1,67 @@ +# This is a Makefile fragment for Menhir-specific aspects. + +# This flag can be set to true or false. It controls whether we use +# Menhir's table back-end or code back-end. The table back-end is a +# bit slower, but supports more features, including advanced error +# reporting. + +MENHIR_TABLE = false + +# Executable. + +ifeq ($(MENHIR_TABLE),true) + MENHIR = menhir --table +else + MENHIR = menhir +endif + +# Options. + +MENHIR_FLAGS = -v --no-stdlib -la 1 + +# Using Menhir in --table mode requires MenhirLib. + +ifeq ($(MENHIR_TABLE),true) + MENHIR_LIBS = menhirLib.cmx +else + MENHIR_LIBS = +endif + +# The compilation rule. + +%.ml %.mli: %.mly + $(MENHIR) $(MENHIR_FLAGS) $< + +# Note 1: finding where MenhirLib has been installed would be easier if we +# could depend on ocamlfind, but as far as I understand and as of today, +# CompCert can be compiled and linked even in the absence of ocamlfind. +# So, we should not require ocamlfind. + +# Note 2: Menhir has options --suggest-comp-flags and --suggest-link-flags +# which we are supposed to help solve this difficulty. However, they don't +# work for us out of the box, because if Menhir has been installed using +# ocamlfind, then Menhir will suggest using ocamlfind (i.e. it will suggest +# -package and -linkpkg options), which we don't want to do. + +# Solution: Ask Menhir first. If Menhir answers "-package menhirLib", then +# Menhir was installed with ocamlfind, so we should not ask Menhir, but we +# can instead ask ocamlfind where Menhir's library was installed. Otherwise, +# Menhir answers directly with a "-I ..." directive, which we use. + +ifeq ($(MENHIR_TABLE),true) + + MENHIR_SUGGESTION = $(MENHIR) --suggest-comp-flags + + MENHIR_INCLUDES = $(shell \ + if $(MENHIR_SUGGESTION) | grep -e "-package" >/dev/null ; then \ + echo "-I `ocamlfind query menhirLib`" ; \ + else \ + $(MENHIR_SUGGESTION) ; \ + fi) + +else + + MENHIR_INCLUDES = + +endif + |