diff options
author | François Pottier <francois.pottier@inria.fr> | 2015-10-23 15:08:33 +0200 |
---|---|---|
committer | François Pottier <francois.pottier@inria.fr> | 2015-10-23 15:17:50 +0200 |
commit | 136986c204af19341aeb455d72fe817b16fa6fff (patch) | |
tree | 02e9178d9f2cf942bd32366891d480ff161406f6 /Makefile.extr | |
parent | c46723c0169145d41d1879c236f53314456f1ba1 (diff) | |
parent | 1cb3d93ff278ebbd0c6967c5f9401a97f9b618b4 (diff) | |
download | compcert-136986c204af19341aeb455d72fe817b16fa6fff.tar.gz compcert-136986c204af19341aeb455d72fe817b16fa6fff.zip |
Merge remote branch 'upstream/master' into clean
Conflicts:
Makefile.extr
Diffstat (limited to 'Makefile.extr')
-rw-r--r-- | Makefile.extr | 56 |
1 files changed, 3 insertions, 53 deletions
diff --git a/Makefile.extr b/Makefile.extr index 4e2549cc..ed46e3f2 100644 --- a/Makefile.extr +++ b/Makefile.extr @@ -26,23 +26,13 @@ include Makefile.menhir cparser/pre_parser_messages.ml: $(MAKE) -C cparser correct -# Directories containing plain Caml code (no preprocessing) +# Directories containing plain Caml code DIRS=extraction \ lib common $(ARCH) backend cfrontend cparser driver \ exportclight debug -# Directories containing Caml code that must be preprocessed by Camlp4 - -ifeq ($(CCHECKLINK),true) -DIRS_P4=checklink -else -DIRS_P4= -endif - -ALLDIRS=$(DIRS) $(DIRS_P4) - -INCLUDES=$(patsubst %,-I %, $(ALLDIRS)) $(MENHIR_INCLUDES) +INCLUDES=$(patsubst %,-I %, $(DIRS)) $(MENHIR_INCLUDES) # Control of warnings: # warning 3 = deprecated feature. Turned off for OCaml 4.02 (bytes vs strings) @@ -54,10 +44,6 @@ extraction/%.cmo: WARNINGS +=-w -20 COMPFLAGS=-g $(INCLUDES) $(WARNINGS) -# Using the bitstring library and syntax extension (for checklink) - -BITSTRING=-package bitstring,bitstring.syntax -syntax bitstring.syntax,camlp4o - # Using .opt compilers if available ifeq ($(OCAML_OPT_COMP),true) @@ -66,19 +52,10 @@ else DOTOPT= endif -# Compilers used for non-preprocessed code - OCAMLC=ocamlc$(DOTOPT) $(COMPFLAGS) OCAMLOPT=ocamlopt$(DOTOPT) $(COMPFLAGS) OCAMLDEP=ocamldep$(DOTOPT) -slash $(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) - OCAMLLEX=ocamllex -q MODORDER=tools/modorder .depend.extr @@ -108,20 +85,6 @@ ccomp.byte: $(CCOMP_OBJS:.cmx=.cmo) @echo "Linking $@" @$(OCAMLC) -o $@ $(LIBS_BYTE) $+ -ifeq ($(CCHECKLINK),true) - -CCHECKLINK_OBJS:=$(shell $(MODORDER) checklink/Validator.cmx) - -cchecklink: $(CCHECKLINK_OBJS) - @echo "Linking $@" - @$(OCAMLOPT_P4) -linkpkg -o $@ $(CHECKLINK_LIBS) $+ - -cchecklink.byte: $(CCHECKLINK_OBJS:.cmx=.cmo) - @echo "Linking $@" - @$(OCAMLC_P4) -linkpkg -o $@ $(CHECKLINK_LIBS:.cmxa=.cma) $+ - -endif - CLIGHTGEN_OBJS:=$(shell $(MODORDER) exportclight/Clightgen.cmx) clightgen: $(CLIGHTGEN_OBJS) @@ -138,16 +101,6 @@ endif # End of part that assumes .depend.extr already exists -checklink/%.cmi: checklink/%.mli - @echo "OCAMLC $<" - @$(OCAMLC_P4) -c $< -checklink/%.cmo: checklink/%.ml - @echo "OCAMLC $<" - @$(OCAMLC_P4) -c $< -checklink/%.cmx: checklink/%.ml - @echo "OCAMLOPT $<" - @$(OCAMLOPT_P4) -c $< - %.cmi: %.mli @echo "OCAMLC $<" @$(OCAMLC) -c $< @@ -164,7 +117,7 @@ checklink/%.cmx: checklink/%.ml clean: rm -f $(EXECUTABLES) rm -f $(GENERATED) - for d in $(ALLDIRS); do rm -f $$d/*.cm[iox] $$d/*.o; done + for d in $(DIRS); do rm -f $$d/*.cm[iox] $$d/*.o; done rm -f backend/CMparser.automaton $(MAKE) -C cparser clean @@ -173,8 +126,5 @@ clean: depend: $(GENERATED) @echo "Analyzing OCaml dependencies" @$(OCAMLDEP) $(foreach d,$(DIRS),$(wildcard $(d)/*.mli $(d)/*.ml)) $(GENERATED) >.depend.extr || { rm -f .depend.extr; exit 2; } -ifneq ($(strip $(DIRS_P4)),) - @$(OCAMLDEP_P4) $(foreach d,$(DIRS_P4),$(wildcard $(d)/*.mli $(d)/*.ml)) >>.depend.extr || { rm -f .depend.extr; exit 2; } -endif |