diff options
Diffstat (limited to 'Makefile.extr')
-rw-r--r-- | Makefile.extr | 168 |
1 files changed, 168 insertions, 0 deletions
diff --git a/Makefile.extr b/Makefile.extr new file mode 100644 index 00000000..266be7c3 --- /dev/null +++ b/Makefile.extr @@ -0,0 +1,168 @@ +####################################################################### +# # +# The Compcert verified compiler # +# # +# Xavier Leroy, 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 GNU General Public License as published by # +# the Free Software Foundation, either version 2 of the License, or # +# (at your option) any later version. This file is also distributed # +# under the terms of the INRIA Non-Commercial License Agreement. # +# # +####################################################################### + +# Second-stage Makefile, after Coq extraction + +include Makefile.config + +# Directories containing plain Caml code (no preprocessing) + +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)) + +# 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 $(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) +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 +MODORDER=tools/modorder .depend.extr + +PARSERS=backend/CMparser.mly cparser/pre_parser.mly +LEXERS=backend/CMlexer.mll cparser/Lexer.mll lib/Tokenize.mll + +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) + +ccomp: $(CCOMP_OBJS) + @echo "Linking $@" + @$(OCAMLOPT) -o $@ $(LIBS) $+ + +ccomp.byte: $(CCOMP_OBJS:.cmx=.cmo) + @echo "Linking $@" + @$(OCAMLC) -o $@ $(LIBS:.cmxa=.cma) $+ + +ifeq ($(CCHECKLINK),true) + +CCHECKLINK_OBJS:=$(shell $(MODORDER) checklink/Validator.cmx) + +cchecklink: $(CCHECKLINK_OBJS) + @echo "Linking $@" + @$(OCAMLOPT_P4) -linkpkg -o $@ $(LIBS) $+ + +cchecklink.byte: $(CCHECKLINK_OBJS:.cmx=.cmo) + @echo "Linking $@" + @$(OCAMLC_P4) -linkpkg -o $@ $(LIBS:.cmxa=.cma) $+ + +endif + +CLIGHTGEN_OBJS:=$(shell $(MODORDER) exportclight/Clightgen.cmx) + +clightgen: $(CLIGHTGEN_OBJS) + @echo "Linking $@" + @$(OCAMLOPT) -o $@ $(LIBS) $+ + +clightgen.byte: $(CLIGHTGEN_OBJS:.cmx=.cmo) + @echo "Linking $@" + @$(OCAMLC) -o $@ $(LIBS:.cmxa=.cma) $+ + +include .depend.extr + +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 $< +%.cmo: %.ml + @echo "OCAMLC $<" + @$(OCAMLC) -c $< +%.cmx: %.ml + @echo "OCAMLOPT $<" + @$(OCAMLOPT) -c $< + +%.ml %.mli: %.mly + $(MENHIR) $< +%.ml: %.mll + $(OCAMLLEX) $< + +clean: + rm -f $(EXECUTABLES) + 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 +ifneq ($(strip $(DIRS_P4)),) + @for d in $(DIRS_P4); do $(OCAMLDEP_P4) $$d/*.mli $$d/*.ml; done >> .depend.extr +endif + + |