From 153651d6f959f9a18a47441f2e7280046b590f1e Mon Sep 17 00:00:00 2001
From: François Pottier <francois.pottier@inria.fr>
Date: Fri, 16 Oct 2015 11:30:16 +0200
Subject: 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.

---
 Makefile.menhir | 67 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 67 insertions(+)
 create mode 100644 Makefile.menhir

(limited to 'Makefile.menhir')

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
+
-- 
cgit