diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2014-09-30 13:10:26 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2014-09-30 13:10:26 +0200 |
| commit | a2bed030e01bfe6e3addbe44f724de5c5fbeab65 (patch) | |
| tree | aeffd4bcba1743dd5fdcc08e2f2e9f51962e4402 /Makefile | |
| parent | e5b59af8a21c42b504b1beeb89208dd0cb0c8b3b (diff) | |
| download | compcert-a2bed030e01bfe6e3addbe44f724de5c5fbeab65.tar.gz compcert-a2bed030e01bfe6e3addbe44f724de5c5fbeab65.zip | |
Change the way the tools like the linker, assembler, etc. are specified by including an .ini file parser. The .ini file is generated in the Makefile instead of the Configuration.ml file and parsed on start.
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 44 |
1 files changed, 23 insertions, 21 deletions
@@ -157,34 +157,34 @@ extraction/STAMP: $(FILES:.v=.vo) extraction/extraction.v $(ARCH)/extractionMach $(COQEXEC) extraction/extraction.v touch extraction/STAMP -ccomp: extraction/STAMP driver/Configuration.ml +ccomp: extraction/STAMP compcert.ini $(OCAMLBUILD) $(OCB_OPTIONS) Driver.native \ && rm -f ccomp && $(SLN) _build/driver/Driver.native ccomp -ccomp.prof: extraction/STAMP driver/Configuration.ml +ccomp.prof: extraction/STAMP compcert.ini $(OCAMLBUILD) $(OCB_OPTIONS) Driver.p.native \ && rm -f ccomp.prof && $(SLN) _build/driver/Driver.p.native ccomp.prof -ccomp.byte: extraction/STAMP driver/Configuration.ml +ccomp.byte: extraction/STAMP compcert.ini $(OCAMLBUILD) $(OCB_OPTIONS) Driver.d.byte \ && rm -f ccomp.byte && $(SLN) _build/driver/Driver.d.byte ccomp.byte runtime: $(MAKE) -C runtime -cchecklink: driver/Configuration.ml +cchecklink: compcert.ini $(OCAMLBUILD) $(OCB_OPTIONS_CHECKLINK) Validator.native \ && rm -f cchecklink && $(SLN) _build/checklink/Validator.native cchecklink -cchecklink.byte: driver/Configuration.ml +cchecklink.byte: compcert.ini $(OCAMLBUILD) $(OCB_OPTIONS_CHECKLINK) Validator.d.byte \ && rm -f cchecklink.byte && $(SLN) _build/checklink/Validator.d.byte cchecklink.byte -clightgen: extraction/STAMP driver/Configuration.ml exportclight/Clightdefs.vo +clightgen: extraction/STAMP compcert.ini exportclight/Clightdefs.vo $(OCAMLBUILD) $(OCB_OPTIONS_CLIGHTGEN) Clightgen.native \ && rm -f clightgen && $(SLN) _build/exportclight/Clightgen.native clightgen -clightgen.byte: extraction/STAMP driver/Configuration.ml exportclight/Clightdefs.vo +clightgen.byte: extraction/STAMP compcert.ini exportclight/Clightdefs.vo $(OCAMLBUILD) $(OCB_OPTIONS_CLIGHTGEN) Clightgen.d.byte \ && rm -f clightgen.byte && $(SLN) _build/exportclight/Clightgen.d.byte clightgen.byte @@ -220,20 +220,20 @@ latexdoc: @tools/ndfun $*.vp > $*.v || { rm -f $*.v; exit 2; } @chmod -w $*.v -driver/Configuration.ml: Makefile.config VERSION - (echo let stdlib_path = "\"$(LIBDIR)\""; \ - echo let prepro = "\"$(CPREPRO)\""; \ - echo let asm = "\"$(CASM)\""; \ - echo let linker = "\"$(CLINKER)\""; \ - echo let arch = "\"$(ARCH)\""; \ - echo let model = "\"$(MODEL)\""; \ - echo let abi = "\"$(ABI)\""; \ - echo let system = "\"$(SYSTEM)\""; \ - echo let has_runtime_lib = $(HAS_RUNTIME_LIB); \ - echo let asm_supports_cfi = $(ASM_SUPPORTS_CFI); \ +compcert.ini: Makefile.config VERSION + (echo stdlib_path=$(LIBDIR); \ + echo prepro=$(CPREPRO); \ + echo asm=$(CASM); \ + echo linker=$(CLINKER); \ + echo arch=$(ARCH); \ + echo model=$(MODEL); \ + echo abi=$(ABI); \ + echo system=$(SYSTEM); \ + echo has_runtime_lib=$(HAS_RUNTIME_LIB); \ + echo asm_supports_cfi=$(ASM_SUPPORTS_CFI); \ version=`cat VERSION`; \ - echo let version = "\"$$version\"") \ - > driver/Configuration.ml + echo version=$$version) \ + > compcert.ini cparser/Parser.v: cparser/Parser.vy $(MENHIR) --coq cparser/Parser.vy @@ -246,6 +246,8 @@ depend: $(FILES) exportclight/Clightdefs.v install: install -d $(BINDIR) install ./ccomp $(BINDIR) + install -d $(SHAREDIR) + install ./compcert.ini $(SHAREDIR) ifeq ($(CCHECKLINK),true) install ./cchecklink $(BINDIR) endif @@ -259,7 +261,7 @@ clean: rm -rf _build rm -rf doc/html doc/*.glob rm -f doc/coq2html.ml doc/coq2html doc/*.cm? doc/*.o - rm -f driver/Configuration.ml + rm -f compcert.ini rm -f extraction/STAMP extraction/*.ml extraction/*.mli rm -f tools/ndfun tools/*.cm? tools/*.o rm -f $(ARCH)/ConstpropOp.v $(ARCH)/SelectOp.v backend/SelectDiv.v backend/SelectLong.v |