diff options
| author | François Pottier <francois.pottier@inria.fr> | 2015-10-16 11:30:16 +0200 |
|---|---|---|
| committer | François Pottier <francois.pottier@inria.fr> | 2015-10-16 11:30:16 +0200 |
| commit | 153651d6f959f9a18a47441f2e7280046b590f1e (patch) | |
| tree | df4a6fb46d1c7b85f0fcb48d9ce84379bf7fea91 /Makefile.extr | |
| parent | 7d68132721bb4c12de8b846717972a25899ecc3f (diff) | |
| download | compcert-153651d6f959f9a18a47441f2e7280046b590f1e.tar.gz compcert-153651d6f959f9a18a47441f2e7280046b590f1e.zip | |
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.
Diffstat (limited to 'Makefile.extr')
| -rw-r--r-- | Makefile.extr | 17 |
1 files changed, 10 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) $< |