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.extr   | 17 +++++++++------
 Makefile.menhir | 67 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 77 insertions(+), 7 deletions(-)
 create mode 100644 Makefile.menhir

diff --git a/Makefile.extr b/Makefile.extr
index 8dcbdc33..6c19d1ed 100644
--- a/Makefile.extr
+++ b/Makefile.extr
@@ -17,6 +17,10 @@
 
 include Makefile.config
 
+# Menhir configuration and rules.
+
+include Makefile.menhir
+
 # Directories containing plain Caml code (no preprocessing)
 
 DIRS=extraction \
@@ -33,7 +37,7 @@ endif
 
 ALLDIRS=$(DIRS) $(DIRS_P4)
 
-INCLUDES=$(patsubst %,-I %, $(ALLDIRS))
+INCLUDES=$(patsubst %,-I %, $(ALLDIRS)) $(MENHIR_INCLUDES)
 
 # Control of warnings:
 # warning 3 = deprecated feature.  Turned off for OCaml 4.02 (bytes vs strings)
@@ -70,7 +74,6 @@ OCAMLC_P4=ocamlfind ocamlc $(COMPFLAGS) $(BITSTRING)
 OCAMLOPT_P4=ocamlfind ocamlopt $(COMPFLAGS) $(BITSTRING)
 OCAMLDEP_P4=ocamlfind ocamldep $(INCLUDES) $(BITSTRING)
 
-MENHIR=menhir -v --no-stdlib -la 1
 OCAMLLEX=ocamllex -q
 MODORDER=tools/modorder .depend.extr
 
@@ -78,7 +81,9 @@ PARSERS=backend/CMparser.mly cparser/pre_parser.mly
 LEXERS=backend/CMlexer.mll cparser/Lexer.mll \
        lib/Tokenize.mll lib/Readconfig.mll
 
-LIBS=str.cmxa unix.cmxa
+LIBS=str.cmxa unix.cmxa $(MENHIR_LIBS)
+LIBS_BYTE=$(patsubst %.cmxa,%.cma,$(patsubst %.cmx,%.cmo,$(LIBS)))
+
 CHECKLINK_LIBS=str.cmxa
 
 EXECUTABLES=ccomp ccomp.byte cchecklink cchecklink.byte clightgen clightgen.byte
@@ -96,7 +101,7 @@ ccomp: $(CCOMP_OBJS)
 
 ccomp.byte: $(CCOMP_OBJS:.cmx=.cmo)
 	@echo "Linking $@"
-	@$(OCAMLC) -o $@ $(LIBS:.cmxa=.cma) $+
+	@$(OCAMLC) -o $@ $(LIBS_BYTE) $+
 
 ifeq ($(CCHECKLINK),true)
 
@@ -120,7 +125,7 @@ clightgen: $(CLIGHTGEN_OBJS)
 
 clightgen.byte: $(CLIGHTGEN_OBJS:.cmx=.cmo)
 	@echo "Linking $@"
-	@$(OCAMLC) -o $@ $(LIBS:.cmxa=.cma) $+
+	@$(OCAMLC) -o $@ $(LIBS_BYTE) $+
 
 include .depend.extr
 
@@ -148,8 +153,6 @@ checklink/%.cmx: checklink/%.ml
 	@echo "OCAMLOPT $<"
 	@$(OCAMLOPT) -c $<
 
-%.ml %.mli: %.mly
-	$(MENHIR) $<
 %.ml: %.mll
 	$(OCAMLLEX) $<
 
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