diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-01-20 16:58:57 +0100 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-01-20 16:58:57 +0100 |
commit | fe7da33a1992c3023a2e7e3f36c532ad10e3f236 (patch) | |
tree | 4f1acbaa51bea8bb405858660e68cc5e3cd2ab93 | |
parent | 9f2ca1049957004161834090a697cd4118e2fb08 (diff) | |
parent | 860e340b9a383964773d9c4523fb02a1de407e7f (diff) | |
download | compcert-fe7da33a1992c3023a2e7e3f36c532ad10e3f236.tar.gz compcert-fe7da33a1992c3023a2e7e3f36c532ad10e3f236.zip |
Merge branch containing changes for windows compile.
-rw-r--r-- | Makefile | 8 | ||||
-rw-r--r-- | Makefile.extr | 8 | ||||
-rwxr-xr-x | configure | 7 |
3 files changed, 15 insertions, 8 deletions
@@ -49,7 +49,7 @@ FLOCQ=\ # General-purpose libraries (in lib/) -LIB=Axioms.v Coqlib.v Intv.v Maps.v Heaps.v Lattice.v Ordered.v \ +VLIB=Axioms.v Coqlib.v Intv.v Maps.v Heaps.v Lattice.v Ordered.v \ Iteration.v Integers.v Archi.v Fappli_IEEE_extra.v Floats.v \ Parmov.v UnionFind.v Wfsimpl.v \ Postorder.v FSetAVLplus.v IntvSets.v @@ -112,7 +112,7 @@ DRIVER=Compopts.v Compiler.v Complements.v # All source files -FILES=$(LIB) $(COMMON) $(BACKEND) $(CFRONTEND) $(DRIVER) $(FLOCQ) \ +FILES=$(VLIB) $(COMMON) $(BACKEND) $(CFRONTEND) $(DRIVER) $(FLOCQ) \ $(PARSERVALIDATOR) $(PARSER) all: @@ -174,9 +174,9 @@ doc/coq2html.ml: doc/coq2html.mll ocamllex -q doc/coq2html.mll tools/ndfun: tools/ndfun.ml - ocamlopt -o tools/ndfun str.cmxa tools/ndfun.ml + ocamlopt -o tools/ndfun str.cmxa tools/ndfun.ml $(LINKERSPEC) tools/modorder: tools/modorder.ml - ocamlopt -o tools/modorder str.cmxa tools/modorder.ml + ocamlopt -o tools/modorder str.cmxa tools/modorder.ml $(LINKERSPEC) latexdoc: cd doc; $(COQDOC) --latex -o doc/doc.tex -g $(FILES) diff --git a/Makefile.extr b/Makefile.extr index 35ae5f7b..2afd6e31 100644 --- a/Makefile.extr +++ b/Makefile.extr @@ -90,11 +90,11 @@ CCOMP_OBJS:=$(shell $(MODORDER) driver/Driver.cmx) ccomp: $(CCOMP_OBJS) @echo "Linking $@" - @$(OCAMLOPT) -o $@ $(LIBS) $+ + @$(OCAMLOPT) -o $@ $(LIBS) $+ $(LINKERSPEC) ccomp.byte: $(CCOMP_OBJS:.cmx=.cmo) @echo "Linking $@" - @$(OCAMLC) -o $@ $(LIBS:.cmxa=.cma) $+ + @$(OCAMLC) -o $@ $(LIBS:.cmxa=.cma) $+ $(LINKERSPEC) ifeq ($(CCHECKLINK),true) @@ -156,6 +156,10 @@ clean: rm -f $(GENERATED) for d in $(ALLDIRS); do rm -f $$d/*.cm[iox] $$d/*.o; done +cleansource: + rm -f $(EXECUTABLES) + for d in $(ALLDIRS); do rm -f $$d/*.cm[iox] $$d/*.o; done + # Generation of .depend.extr depend: $(GENERATED) @@ -18,6 +18,7 @@ libdir='$(PREFIX)/lib/compcert' toolprefix='' target='' has_runtime_lib=true +build_checklink=true usage='Usage: ./configure [options] target @@ -64,6 +65,8 @@ while : ; do toolprefix="$2"; shift;; -no-runtime-lib) has_runtime_lib=false; shift;; + -no-checklink) + build_checklink=false; shift;; *) if test -n "$target"; then echo "$usage" 1>&2; exit 2; fi target="$1";; @@ -89,7 +92,7 @@ case "$target" in casmruntime="${toolprefix}gcc -c -Wa,-mregnames" clinker="${toolprefix}gcc" libmath="-lm" - cchecklink=true;; + cchecklink=${build_checklink};; powerpc-eabi-diab|ppc-eabi-diab) arch="powerpc" model="standard" @@ -101,7 +104,7 @@ case "$target" in asm_supports_cfi=false clinker="${toolprefix}dcc" libmath="-lm" - cchecklink=true;; + cchecklink=${build_checklink};; arm*-*) arch="arm" case "$target" in |