From 153651d6f959f9a18a47441f2e7280046b590f1e Mon Sep 17 00:00:00 2001 From: François Pottier 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 From dfa2941c7df7641872464ff07466f754718df1c1 Mon Sep 17 00:00:00 2001 From: François Pottier Date: Fri, 16 Oct 2015 11:37:25 +0200 Subject: It is probably more efficient to eagerly evaluate $(MENHIR_INCLUDES). This should save a lot of calls to the shell, menhir, and ocamlfind. --- Makefile.menhir | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Makefile.menhir') diff --git a/Makefile.menhir b/Makefile.menhir index 414279ab..72b54b14 100644 --- a/Makefile.menhir +++ b/Makefile.menhir @@ -52,7 +52,7 @@ ifeq ($(MENHIR_TABLE),true) MENHIR_SUGGESTION = $(MENHIR) --suggest-comp-flags - MENHIR_INCLUDES = $(shell \ + MENHIR_INCLUDES := $(shell \ if $(MENHIR_SUGGESTION) | grep -e "-package" >/dev/null ; then \ echo "-I `ocamlfind query menhirLib`" ; \ else \ -- cgit From 1ea7d1d09c350d0f0613f0bd763c3e01a70ddbb9 Mon Sep 17 00:00:00 2001 From: François Pottier Date: Fri, 23 Oct 2015 09:57:02 +0200 Subject: Distinguish [MENHIR] and [MENHIR_MODE]. Cleaner, more flexible. --- Makefile.menhir | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) (limited to 'Makefile.menhir') diff --git a/Makefile.menhir b/Makefile.menhir index 72b54b14..db28ffaa 100644 --- a/Makefile.menhir +++ b/Makefile.menhir @@ -1,5 +1,9 @@ # This is a Makefile fragment for Menhir-specific aspects. +# Executable. + +MENHIR = menhir + # 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 @@ -7,12 +11,12 @@ MENHIR_TABLE = false -# Executable. +# To pass or not to pass --table. ifeq ($(MENHIR_TABLE),true) - MENHIR = menhir --table + MENHIR_MODE = --table else - MENHIR = menhir + MENHIR_MODE = endif # Options. @@ -30,7 +34,7 @@ endif # The compilation rule. %.ml %.mli: %.mly - $(MENHIR) $(MENHIR_FLAGS) $< + $(MENHIR) $(MENHIR_MODE) $(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, @@ -50,7 +54,7 @@ endif ifeq ($(MENHIR_TABLE),true) - MENHIR_SUGGESTION = $(MENHIR) --suggest-comp-flags + MENHIR_SUGGESTION = $(MENHIR) $(MENHIR_MODE) --suggest-comp-flags MENHIR_INCLUDES := $(shell \ if $(MENHIR_SUGGESTION) | grep -e "-package" >/dev/null ; then \ -- cgit From ed549acd7d71d274c7e39480900b14d1b65c3cd1 Mon Sep 17 00:00:00 2001 From: François Pottier Date: Fri, 23 Oct 2015 09:59:07 +0200 Subject: Switch to --table mode. This is slightly slower but otherwise changes nothing. --- Makefile.menhir | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Makefile.menhir') diff --git a/Makefile.menhir b/Makefile.menhir index db28ffaa..82f44e5f 100644 --- a/Makefile.menhir +++ b/Makefile.menhir @@ -9,7 +9,7 @@ MENHIR = menhir # bit slower, but supports more features, including advanced error # reporting. -MENHIR_TABLE = false +MENHIR_TABLE = true # To pass or not to pass --table. -- cgit From 1f74fdf503d3c501d2e261e76337452f6401d63a Mon Sep 17 00:00:00 2001 From: François Pottier Date: Fri, 23 Oct 2015 13:59:40 +0200 Subject: Added copyright banners to the new files. --- Makefile.menhir | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'Makefile.menhir') diff --git a/Makefile.menhir b/Makefile.menhir index 82f44e5f..74bd14e2 100644 --- a/Makefile.menhir +++ b/Makefile.menhir @@ -1,3 +1,15 @@ +####################################################################### +# # +# The Compcert verified compiler # +# # +# François Pottier, INRIA Paris-Rocquencourt # +# # +# Copyright Institut National de Recherche en Informatique et en # +# Automatique. All rights reserved. This file is distributed # +# under the terms of the INRIA Non-Commercial License Agreement. # +# # +####################################################################### + # This is a Makefile fragment for Menhir-specific aspects. # Executable. -- cgit From ff7aa1352d4171724963bb834e09a6abdf0e630e Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 27 Oct 2015 09:45:33 +0100 Subject: Allow the MENHIR_INCLUDE path to be set by environment. Bug 17481 --- Makefile.menhir | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) (limited to 'Makefile.menhir') diff --git a/Makefile.menhir b/Makefile.menhir index 74bd14e2..e845352d 100644 --- a/Makefile.menhir +++ b/Makefile.menhir @@ -14,7 +14,7 @@ # Executable. -MENHIR = menhir +MENHIR = menhir # 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 @@ -28,7 +28,7 @@ MENHIR_TABLE = true ifeq ($(MENHIR_TABLE),true) MENHIR_MODE = --table else - MENHIR_MODE = + MENHIR_MODE = endif # Options. @@ -68,7 +68,7 @@ ifeq ($(MENHIR_TABLE),true) MENHIR_SUGGESTION = $(MENHIR) $(MENHIR_MODE) --suggest-comp-flags - MENHIR_INCLUDES := $(shell \ + MENHIR_INCLUDES ?= $(shell \ if $(MENHIR_SUGGESTION) | grep -e "-package" >/dev/null ; then \ echo "-I `ocamlfind query menhirLib`" ; \ else \ @@ -80,4 +80,3 @@ else MENHIR_INCLUDES = endif - -- cgit From ef770408caabffed0844a72e45e1346f327ee016 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 27 Oct 2015 10:50:18 +0100 Subject: Test if menhir includes is set before trying to set it. Bug 17481. --- Makefile.menhir | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'Makefile.menhir') diff --git a/Makefile.menhir b/Makefile.menhir index e845352d..bbfc2495 100644 --- a/Makefile.menhir +++ b/Makefile.menhir @@ -64,11 +64,13 @@ endif # can instead ask ocamlfind where Menhir's library was installed. Otherwise, # Menhir answers directly with a "-I ..." directive, which we use. +ifndef $(MENHIR_INCLUDES) + ifeq ($(MENHIR_TABLE),true) MENHIR_SUGGESTION = $(MENHIR) $(MENHIR_MODE) --suggest-comp-flags - MENHIR_INCLUDES ?= $(shell \ + MENHIR_INCLUDES := $(shell \ if $(MENHIR_SUGGESTION) | grep -e "-package" >/dev/null ; then \ echo "-I `ocamlfind query menhirLib`" ; \ else \ @@ -80,3 +82,5 @@ else MENHIR_INCLUDES = endif + +endif -- cgit From bfad82a13ed2536040ab76bf861c39293c6e5282 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 27 Oct 2015 12:02:53 +0100 Subject: Use ifndef correct. Bug 17481 --- Makefile.menhir | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Makefile.menhir') diff --git a/Makefile.menhir b/Makefile.menhir index bbfc2495..b72c52f3 100644 --- a/Makefile.menhir +++ b/Makefile.menhir @@ -64,7 +64,7 @@ endif # can instead ask ocamlfind where Menhir's library was installed. Otherwise, # Menhir answers directly with a "-I ..." directive, which we use. -ifndef $(MENHIR_INCLUDES) +ifndef MENHIR_INCLUDES ifeq ($(MENHIR_TABLE),true) -- cgit