aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile.menhir
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-10-20 17:55:24 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2015-10-20 17:55:24 +0200
commit5111bce03766251ffde8cd3d29a315c3c7c64364 (patch)
treef0192011c801663e531e42dbeb0f15bb4355fc87 /Makefile.menhir
parent5c408186f4f66d6955c9d2a682cec36231343f87 (diff)
parentdfa2941c7df7641872464ff07466f754718df1c1 (diff)
downloadcompcert-5111bce03766251ffde8cd3d29a315c3c7c64364.tar.gz
compcert-5111bce03766251ffde8cd3d29a315c3c7c64364.zip
Merge branch 'clean' of https://github.com/fpottier/CompCert into fpottier-clean
Conflicts: Makefile.extr
Diffstat (limited to 'Makefile.menhir')
-rw-r--r--Makefile.menhir67
1 files changed, 67 insertions, 0 deletions
diff --git a/Makefile.menhir b/Makefile.menhir
new file mode 100644
index 00000000..72b54b14
--- /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
+