diff options
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 73 |
1 files changed, 25 insertions, 48 deletions
@@ -23,30 +23,14 @@ RECDIRS=lib common $(ARCH) backend cfrontend driver flocq exportclight cparser COQINCLUDES=$(foreach d, $(RECDIRS), -R $(d) -as compcert.$(d)) -CAMLINCLUDES=$(patsubst %,-I %, $(DIRS)) -I extraction - -MENHIR=menhir COQC="$(COQBIN)coqc" -q $(COQINCLUDES) COQDEP="$(COQBIN)coqdep" $(COQINCLUDES) COQDOC="$(COQBIN)coqdoc" COQEXEC="$(COQBIN)coqtop" $(COQINCLUDES) -batch -load-vernac-source COQCHK="$(COQBIN)coqchk" $(COQINCLUDES) +MENHIR=menhir CP=cp -OCAMLBUILD=ocamlbuild -OCB_OPTIONS=\ - -j 2 \ - -no-hygiene \ - -no-links \ - $(CAMLINCLUDES) -OCB_OPTIONS_CHECKLINK=\ - $(OCB_OPTIONS) \ - -I checklink \ - -use-ocamlfind -OCB_OPTIONS_CLIGHTGEN=\ - $(OCB_OPTIONS) \ - -I exportclight - VPATH=$(DIRS) GPATH=$(DIRS) @@ -75,7 +59,7 @@ LIB=Axioms.v Coqlib.v Intv.v Maps.v Heaps.v Lattice.v Ordered.v \ COMMON=Errors.v AST.v Events.v Globalenvs.v Memdata.v Memtype.v Memory.v \ Values.v Smallstep.v Behaviors.v Switch.v Determinism.v Unityping.v -# Back-end modules (in backend/, $(ARCH)/, $(ARCH)/$(VARIANT)) +# Back-end modules (in backend/, $(ARCH)/) BACKEND=\ Cminor.v Op.v CminorSel.v \ @@ -151,38 +135,30 @@ extraction/STAMP: $(FILES:.v=.vo) extraction/extraction.v $(ARCH)/extractionMach $(COQEXEC) extraction/extraction.v touch extraction/STAMP -ccomp: extraction/STAMP compcert.ini - $(OCAMLBUILD) $(OCB_OPTIONS) Driver.native \ - && $(CP) _build/driver/Driver.native ccomp +.depend.extr: extraction/STAMP tools/modorder + $(MAKE) -f Makefile.extr depend + +ccomp: .depend.extr compcert.ini FORCE + $(MAKE) -f Makefile.extr ccomp +ccomp.byte: .depend.extr compcert.ini FORCE + $(MAKE) -f Makefile.extr ccomp.byte -ccomp.prof: extraction/STAMP compcert.ini - $(OCAMLBUILD) $(OCB_OPTIONS) Driver.p.native \ - && $(CP) _build/driver/Driver.p.native ccomp.prof +cchecklink: .depend.extr compcert.ini FORCE + $(MAKE) -f Makefile.extr cchecklink +cchecklink.byte: .depend.extr compcert.ini FORCE + $(MAKE) -f Makefile.extr cchecklink.byte -ccomp.byte: extraction/STAMP compcert.ini - $(OCAMLBUILD) $(OCB_OPTIONS) Driver.d.byte \ - && $(CP) _build/driver/Driver.d.byte ccomp.byte +clightgen: .depend.extr compcert.ini exportclight/Clightdefs.vo FORCE + $(MAKE) -f Makefile.extr clightgen +clightgen.byte: .depend.extr compcert.ini exportclight/Clightdefs.vo FORCE + $(MAKE) -f Makefile.extr clightgen.byte runtime: $(MAKE) -C runtime -cchecklink: compcert.ini - $(OCAMLBUILD) $(OCB_OPTIONS_CHECKLINK) Validator.native \ - && $(CP) _build/checklink/Validator.native cchecklink - -cchecklink.byte: compcert.ini - $(OCAMLBUILD) $(OCB_OPTIONS_CHECKLINK) Validator.d.byte \ - && $(CP) _build/checklink/Validator.d.byte cchecklink.byte - -clightgen: extraction/STAMP compcert.ini exportclight/Clightdefs.vo - $(OCAMLBUILD) $(OCB_OPTIONS_CLIGHTGEN) Clightgen.native \ - && $(CP) _build/exportclight/Clightgen.native clightgen - -clightgen.byte: extraction/STAMP compcert.ini exportclight/Clightdefs.vo - $(OCAMLBUILD) $(OCB_OPTIONS_CLIGHTGEN) Clightgen.d.byte \ - && $(CP) _build/exportclight/Clightgen.d.byte clightgen.byte +FORCE: -.PHONY: proof extraction ccomp ccomp.prof ccomp.byte runtime cchecklink cchecklink.byte clightgen clightgen.byte +.PHONY: proof extraction runtime FORCE documentation: doc/coq2html $(FILES) mkdir -p doc/html @@ -195,10 +171,12 @@ doc/coq2html: doc/coq2html.ml ocamlopt -o doc/coq2html str.cmxa doc/coq2html.ml doc/coq2html.ml: doc/coq2html.mll - ocamllex doc/coq2html.mll + ocamllex -q doc/coq2html.mll tools/ndfun: tools/ndfun.ml ocamlopt -o tools/ndfun str.cmxa tools/ndfun.ml +tools/modorder: tools/modorder.ml + ocamlopt -o tools/modorder str.cmxa tools/modorder.ml latexdoc: cd doc; $(COQDOC) --latex -o doc/doc.tex -g $(FILES) @@ -251,14 +229,13 @@ endif clean: rm -f $(patsubst %, %/*.vo, $(DIRS)) - rm -f ccomp ccomp.byte cchecklink cchecklink.byte clightgen clightgen.byte - rm -rf _build rm -rf doc/html doc/*.glob rm -f doc/coq2html.ml doc/coq2html doc/*.cm? doc/*.o rm -f compcert.ini - rm -f extraction/STAMP extraction/*.ml extraction/*.mli - rm -f tools/ndfun tools/*.cm? tools/*.o + rm -f extraction/STAMP extraction/*.ml extraction/*.mli .depend.extr + rm -f tools/ndfun tools/modorder tools/*.cm? tools/*.o rm -f $(ARCH)/ConstpropOp.v $(ARCH)/SelectOp.v backend/SelectDiv.v backend/SelectLong.v + $(MAKE) -f Makefile.extr clean $(MAKE) -C runtime clean $(MAKE) -C test clean |