diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2014-12-17 15:24:17 +0100 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2014-12-17 15:24:17 +0100 |
commit | 20c70573181f81c99ea4e8797615dac8308a9b18 (patch) | |
tree | 5961b1f9c653e6ded4a1c180bb7794930a587425 /Makefile.extr | |
parent | 0c80820c3850fa2b0713f7519c7085e949cc7cb2 (diff) | |
download | compcert-20c70573181f81c99ea4e8797615dac8308a9b18.tar.gz compcert-20c70573181f81c99ea4e8797615dac8308a9b18.zip |
Use OCaml's .opt compilers when available.
Cleanups in configure.
Diffstat (limited to 'Makefile.extr')
-rw-r--r-- | Makefile.extr | 65 |
1 files changed, 49 insertions, 16 deletions
diff --git a/Makefile.extr b/Makefile.extr index 60fee407..732df31e 100644 --- a/Makefile.extr +++ b/Makefile.extr @@ -17,30 +17,58 @@ include Makefile.config +# Directories containing plain Caml code (no preprocessing) + DIRS=extraction \ lib common $(ARCH) backend cfrontend cparser driver \ exportclight -ALLDIRS=$(DIRS) +# Directories containing Caml code that must be preprocessed by Camlp4 + ifeq ($(CCHECKLINK),true) -ALLDIRS+=checklink +DIRS_P4=checklink +else +DIRS_P4= endif +ALLDIRS=$(DIRS) $(DIRS_P4) + INCLUDES=$(patsubst %,-I %, $(ALLDIRS)) +# Control of warnings: +# warning 3 = deprecated feature. Turned off for OCaml 4.02 (bytes vs strings) +# warning 20 = unused function argument. There are some in extracted code + WARNINGS=-w -3 extraction/%.cmx: WARNINGS +=-w -20 extraction/%.cmo: WARNINGS +=-w -20 +COMPFLAGS=-g $(INCLUDE) $(WARNINGS) + +# Using the bitstring library and syntax extension (for checklink) + BITSTRING=-package bitstring,bitstring.syntax -syntax bitstring.syntax,camlp4o -OCAMLC=ocamlc -g $(INCLUDES) $(WARNINGS) -OCAMLOPT=ocamlopt -g $(INCLUDES) $(WARNINGS) -OCAMLDEP=ocamldep $(INCLUDES) +# Using .opt compilers if available -OCAMLC_P4=ocamlfind $(OCAMLC) $(BITSTRING) -OCAMLOPT_P4=ocamlfind $(OCAMLOPT) $(BITSTRING) -OCAMLDEP_P4=ocamlfind $(OCAMLDEP) $(BITSTRING) +ifeq ($(OCAML_OPT_COMP),true) +DOTOPT=.opt +else +DOTOPT= +endif + +# Compilers used for non-preprocessed code + +OCAMLC=ocamlc$(DOTOPT) $(COMPFLAGS) +OCAMLOPT=ocamlopt$(DOTOPT) $(COMPFLAGS) +OCAMLDEP=ocamldep$(DOTOPT) $(INCLUDES) + +# Compilers used for Camlp4-preprocessed code. Note that we cannot +# use the .opt compilers (because ocamlfind doesn't support them). + +OCAMLC_P4=ocamlfind ocamlc $(COMPFLAGS) $(BITSTRING) +OCAMLOPT_P4=ocamlfind ocamlopt $(COMPFLAGS) $(BITSTRING) +OCAMLDEP_P4=ocamlfind ocamldep $(INCLUDES) $(BITSTRING) MENHIR=menhir --explain OCAMLLEX=ocamllex -q @@ -54,6 +82,8 @@ LIBS=str.cmxa EXECUTABLES=ccomp ccomp.byte cchecklink cchecklink.byte clightgen clightgen.byte GENERATED=$(PARSERS:.mly=.mli) $(PARSERS:.mly=.ml) $(LEXERS:.mll=.ml) +# Beginning of part that assumes .depend.extr already exists + ifeq ($(wildcard .depend.extr),.depend.extr) CCOMP_OBJS:=$(shell $(MODORDER) driver/Driver.cmx) @@ -94,15 +124,17 @@ include .depend.extr endif -checklink/%.cmx: checklink/%.ml - @echo "OCAMLOPT $<" - @$(OCAMLOPT_P4) -c $< -checklink/%.cmo: checklink/%.ml +# End of part that assumes .depend.extr already exists + +checklink/%.cmi: checklink/%.mli @echo "OCAMLC $<" @$(OCAMLC_P4) -c $< -checklink/%.cmi: checklink/%.mli +checklink/%.cmo: checklink/%.ml @echo "OCAMLC $<" @$(OCAMLC_P4) -c $< +checklink/%.cmx: checklink/%.ml + @echo "OCAMLOPT $<" + @$(OCAMLOPT_P4) -c $< %.cmi: %.mli @echo "OCAMLC $<" @@ -124,11 +156,12 @@ clean: rm -f $(GENERATED) for d in $(ALLDIRS); do rm -f $$d/*.cm[iox] $$d/*.o; done +# Generation of .depend.extr + depend: $(GENERATED) @echo "Analyzing OCaml dependencies" @for d in $(DIRS); do $(OCAMLDEP) $$d/*.mli $$d/*.ml; done > .depend.extr -ifeq ($(CCHECKLINK),true) - @$(OCAMLDEP_P4) checklink/*.mli checklink/*.ml >> .depend.extr -endif +ifneq ($(strip $(DIRS_P4)),) + @for d in $(DIRS_P4); do $(OCAMLDEP_P4) $$d/*.mli $$d/*.ml; done >> .dependif |