diff options
Diffstat (limited to 'Makefile.build')
-rw-r--r-- | Makefile.build | 22 |
1 files changed, 13 insertions, 9 deletions
diff --git a/Makefile.build b/Makefile.build index 018471b6..0455a247 100644 --- a/Makefile.build +++ b/Makefile.build @@ -69,7 +69,7 @@ TIMED= # non-empty will activate a default time command TIMECMD= # if you prefer a specific time command instead of $(STDTIME) # e.g. "'time -p'" - +CAMLFLAGS:=${CAMLFLAGS} -w -3 # NB: if you want to collect compilation timings of .v and import them # in a spreadsheet, I suggest something like: # make TIMED=1 2> timings.csv @@ -81,7 +81,7 @@ TIMECMD= # if you prefer a specific time command instead of $(STDTIME) STDTIME=/usr/bin/time -f "$* (user: %U mem: %M ko)" TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) -COQOPTS=$(COQ_XML) $(VM) +COQOPTS=$(COQ_XML) $(VM) $(NATIVECOMPUTE) BOOTCOQC=$(TIMER) $(COQTOPEXE) -boot $(COQOPTS) -compile # The SHOW and HIDE variables control whether make will echo complete commands @@ -101,7 +101,7 @@ BYTEFLAGS=-thread $(CAMLDEBUG) $(USERFLAGS) OPTFLAGS=-thread $(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS) DEPFLAGS= $(LOCALINCLUDES) -I ide -I ide/utils -ifeq ($(shell which codesign > /dev/null && echo $(ARCH)),Darwin) +ifeq ($(shell which codesign > /dev/null 2>&1 && echo $(ARCH)),Darwin) LINKMETADATA=-ccopt "-sectcreate __TEXT __info_plist config/Info-$(notdir $@).plist" CODESIGN:=codesign -s - else @@ -282,11 +282,11 @@ $(COQC): $(patsubst %.cma,%$(BESTLIB),$(COQCCMO:.cmo=$(BESTOBJ))) # For the checker, different flags may be used -checker/check.cma: | checker/check.mllib.d +checker/check.cma: | md5chk checker/check.mllib.d $(SHOW)'OCAMLC -a -o $@' $(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) -a -o $@ $^ -checker/check.cmxa: | checker/check.mllib.d +checker/check.cmxa: | md5chk checker/check.mllib.d $(SHOW)'OCAMLOPT -a -o $@' $(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) -a -o $@ $^ @@ -479,7 +479,7 @@ md5chk: VALIDOPTS=$(if $(VERBOSE),,-silent) -o -m -validate: $(CHICKEN) md5chk | $(ALLVO) +validate: $(CHICKEN) | $(ALLVO) $(SHOW)'COQCHK <theories & plugins>' $(HIDE)$(CHICKEN) -boot $(VALIDOPTS) $(ALLMODS) @@ -524,6 +524,7 @@ hightactics: tactics/hightactics.cma .PHONY: init theories theories-light .PHONY: logic arith bool narith zarith qarith lists strings sets .PHONY: fsets relations wellfounded reals setoids sorting numbers noreal +.PHONY: msets mmaps compat init: $(INITVO) @@ -551,6 +552,9 @@ classes: $(CLASSESVO) program: $(PROGRAMVO) structures: $(STRUCTURESVO) vectors: $(VECTORSVO) +msets: $(MSETSVO) +mmaps: $(MMAPSVO) +compat: $(COMPATVO) noreal: unicode logic arith bool zarith qarith lists sets fsets \ relations wellfounded setoids sorting @@ -584,7 +588,7 @@ pluginsbyte: $(PLUGINS) theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_DEP) | theories/Init/%.v.d $(SHOW)'COQC -noinit $<' $(HIDE)rm -f theories/Init/$*.glob - $(HIDE)$(BOOTCOQC) theories/Init/$* -noinit -R theories Coq + $(HIDE)$(BOOTCOQC) $< -noinit -R theories Coq theories/Numbers/Natural/BigN/NMake_gen.v: theories/Numbers/Natural/BigN/NMake_gen.ml $(OCAML) $< $(TOTARGET) @@ -654,7 +658,7 @@ $(FAKEIDE): lib/clib$(BESTLIB) lib/xml_lexer$(BESTOBJ) lib/xml_parser$(BESTOBJ) # votour: a small vo explorer (based on the checker) -bin/votour: lib/cObj$(BESTOBJ) checker/values$(BESTOBJ) checker/votour.ml +bin/votour: lib/cObj$(BESTOBJ) checker/analyze$(BESTOBJ) checker/values$(BESTOBJ) checker/votour.ml $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml, -I checker,) @@ -1035,7 +1039,7 @@ plugins/%_mod.ml: plugins/%.mllib %.vo %.glob: %.v theories/Init/Prelude.vo $(VO_TOOLS_DEP) | %.v.d $(SHOW)'COQC $<' $(HIDE)rm -f $*.glob - $(HIDE)$(BOOTCOQC) $* + $(HIDE)$(BOOTCOQC) $< ifdef VALIDATE $(SHOW)'COQCHK $(call vo_to_mod,$@)' $(HIDE)$(CHICKEN) -boot -silent -norec $(call vo_to_mod,$@) \ |