aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile.menhir
blob: 74bd14e2d955ff150730593e926c13b4238b1438 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
#######################################################################
#                                                                     #
#              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.

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
# reporting.

MENHIR_TABLE = true

# To pass or not to pass --table.

ifeq ($(MENHIR_TABLE),true)
  MENHIR_MODE = --table
else
  MENHIR_MODE = 
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_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,
# 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) $(MENHIR_MODE) --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