diff options
| -rw-r--r-- | Makefile.extr | 17 | ||||
| -rw-r--r-- | Makefile.menhir | 67 |
2 files changed, 77 insertions, 7 deletions
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 + |