From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- Makefile.build | 631 ++++++++++++++++++++++++++++++++++----------------------- 1 file changed, 378 insertions(+), 253 deletions(-) (limited to 'Makefile.build') diff --git a/Makefile.build b/Makefile.build index 8d3045cc..0d87d98e 100644 --- a/Makefile.build +++ b/Makefile.build @@ -13,11 +13,10 @@ # Starting rule ########################################################################### -# build and install the three subsystems: coq, coqide -world: revision coq coqide -install: install-coq install-coqide +# build the different subsystems: coq, coqide +world: revision coq coqide documentation -.PHONY: world install +.PHONY: world ########################################################################### # Includes @@ -26,29 +25,29 @@ install: install-coq install-coqide include Makefile.common include Makefile.doc -ifeq ($(WITHDOC),all) -world: doc -install: install-doc +# In a first phase, we restrict to the basic .ml4 (the ones without grammar.cma) + +ifdef BUILDGRAMMAR + MLFILES := $(MLSTATICFILES) $(GENMLFILES) $(ML4BASEFILES:.ml4=.ml) + CURFILES := $(MLFILES) $(MLIFILES) $(ML4BASEFILES) grammar/grammar.mllib +else + MLFILES := $(MLSTATICFILES) $(GENMLFILES) $(ML4FILES:.ml4=.ml) + CURFILES := $(MLFILES) $(MLIFILES) $(ML4FILES) $(MLLIBFILES) $(CFILES) $(VFILES) endif +CURDEPS:=$(addsuffix .d, $(CURFILES)) + # All dependency includes must be declared secondary, otherwise make will # delete them if it decided to build them by dependency instead of because # of include, and they will then be automatically deleted, leading to an # infinite loop. -MLFILES:=$(MLSTATICFILES) $(MLEXTRAFILES) - -ALLDEPS:=$(addsuffix .d, \ - $(ML4FILES) $(MLFILES) $(MLIFILES) $(CFILES) $(MLLIBFILES) $(VFILES)) +.SECONDARY: $(CURDEPS) $(GENFILES) $(ML4FILES:.ml4=.ml) -.SECONDARY: $(ALLDEPS) $(GENFILES) $(ML4FILES:.ml4=.ml) +# This include below will lauch the build of all concerned .d. +# The - at front is for disabling warnings about currently missing ones. -# NOTA: the -include below will lauch the build of all .d. Some of them -# will _fail_ at first, this is to be expected (no grammar.cma initially). -# These errors (see below "not ready yet") do not discourage make to -# try again and finally succeed. - --include $(ALLDEPS) +-include $(CURDEPS) ########################################################################### @@ -59,21 +58,31 @@ ALLDEPS:=$(addsuffix .d, \ VERBOSE= NO_RECOMPILE_ML4= -NO_RECOMPILE_LIB= NO_RECALC_DEPS= -READABLE_ML4= # non-empty means .ml of .ml4 will be ascii instead of binary +READABLE_ML4=true # non-empty means .ml of .ml4 will be ascii instead of binary VALIDATE= COQ_XML= # is "-xml" when building XML library VM= # is "-no-vm" to not use the vm" -TIMECMD= # is "'time -p'" to get compilation time of .v -# NB: variable TIME, if set, is the formatting string for unix command 'time'. -# For instance: -# TIME="%C (%U user, %S sys, %e total, %M maxres)" +TIMED= # non-empty will activate a default time command + # when compiling .v (see $(STDTIME) below) + +TIMECMD= # if you prefer a specific time command instead of $(STDTIME) + # e.g. "'time -p'" + +# 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 + +# NB: do not use a variable named TIME, since this variable controls +# the output format of the unix command time. For instance: +# TIME="%C (%U user, %S sys, %e total, %M maxres)" + +STDTIME=/usr/bin/time -f "$* (user: %U mem: %M ko)" +TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) COQOPTS=$(COQ_XML) $(VM) -BOOTCOQTOP:=$(TIMECMD) $(BESTCOQTOP) -boot $(COQOPTS) -BOOTCOQC:=$(BOOTCOQTOP) -compile +BOOTCOQC=$(TIMER) $(COQTOPEXE) -boot $(COQOPTS) -compile # The SHOW and HIDE variables control whether make will echo complete commands # or only abbreviated versions. @@ -85,39 +94,50 @@ HIDE := $(if $(VERBOSE),,@) LOCALINCLUDES=$(addprefix -I , $(SRCDIRS) ) MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) -OCAMLC += $(CAMLFLAGS) -OCAMLOPT += $(CAMLFLAGS) +OCAMLC := $(OCAMLC) $(CAMLFLAGS) +OCAMLOPT := $(OCAMLOPT) $(CAMLFLAGS) + +BYTEFLAGS=-thread $(CAMLDEBUG) $(USERFLAGS) +OPTFLAGS=-thread $(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS) +DEPFLAGS= $(LOCALINCLUDES) -I ide -I ide/utils -BAREBYTEFLAGS=$(CAMLDEBUG) $(USERFLAGS) -BAREOPTFLAGS=$(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS) -BYTEFLAGS=$(MLINCLUDES) $(BAREBYTEFLAGS) -OPTFLAGS=$(MLINCLUDES) $(BAREOPTFLAGS) -DEPFLAGS= -slash $(LOCALINCLUDES) +ifeq ($(ARCH),Darwin) +LINKMETADATA=-ccopt "-sectcreate __TEXT __info_plist config/Info-$(notdir $@).plist" +CODESIGN=codesign -s - +else +LINKMETADATA= +CODESIGN=true +endif define bestocaml $(if $(OPT),\ -$(OCAMLOPT) $(OPTFLAGS) -o $@ $(1) $(addsuffix .cmxa,$(2)) $^ && $(STRIP) $@,\ -$(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ $(1) $(addsuffix .cma,$(2)) $^) +$(if $(findstring $@,$(PRIVATEBINARIES)),\ + $(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -o $@ $(1) $(addsuffix .cmxa,$(2)) $^ && $(STRIP) $@,\ + $(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) $(LINKMETADATA) -o $@ $(1) $(addsuffix .cmxa,$(2)) $^ && $(STRIP) $@ && $(CODESIGN) $@),\ +$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(CUSTOM) -o $@ $(1) $(addsuffix .cma,$(2)) $^) endef -CAMLP4DEPS=`LC_ALL=C sed -n -e 's@^(\*.*camlp4deps: "\(.*\)".*@\1@p' $<` +CAMLP4DEPS=$(shell LC_ALL=C sed -n -e 's@^(\*.*camlp4deps: "\(.*\)".*@\1@p' $(1) \#)) ifeq ($(CAMLP4),camlp5) CAMLP4USE=pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION) else CAMLP4USE=-D$(CAMLVERSION) endif +CAMLP4FLAGS=-I $(CAMLLIB) -I $(CAMLLIB)/threads -I $(MYCAMLP4LIB) unix.cma threads.cma + PR_O := $(if $(READABLE_ML4),pr_o.cmo,pr_dump.cmo) # works also with new camlp4 +SYSMOD:=str unix dynlink threads +SYSCMA:=$(addsuffix .cma,$(SYSMOD)) +SYSCMXA:=$(addsuffix .cmxa,$(SYSMOD)) + ifeq ($(CAMLP4),camlp5) -SYSMOD:=str unix gramlib +P4CMA:=gramlib.cma else -SYSMOD:=str unix dynlink camlp4lib +P4CMA:=dynlink.cma camlp4lib.cma endif -SYSCMA:=$(addsuffix .cma,$(SYSMOD)) -SYSCMXA:=$(addsuffix .cmxa,$(SYSMOD)) - ########################################################################### # Infrastructure for the rest of the Makefile @@ -135,19 +155,12 @@ ifndef ORDER_ONLY_SEP $(error This Makefile needs GNU Make 3.81 or later (that is a version that supports the order-only dependency feature without major bugs.)) endif -VO_TOOLS_DEP := $(BESTCOQTOP) +VO_TOOLS_DEP := $(COQTOPEXE) ifdef COQ_XML VO_TOOLS_DEP += $(COQDOC) endif ifdef VALIDATE - VO_TOOLS_DEP += $(BESTCHICKEN) -endif -ifdef NO_RECOMPILE_LIB - VO_TOOLS_ORDER_ONLY:=$(VO_TOOLS_DEP) - VO_TOOLS_STRICT:= -else - VO_TOOLS_ORDER_ONLY:= - VO_TOOLS_STRICT:=$(VO_TOOLS_DEP) + VO_TOOLS_DEP += $(CHICKEN) endif ifdef NO_RECALC_DEPS @@ -193,110 +206,89 @@ kernel/copcodes.ml: kernel/byterun/coq_instruct.h # Main targets (coqmktop, coqtop.opt, coqtop.byte) ########################################################################### -## In Win32, cygwin provides an emulation of ln -s, but this emulation -## won't work outside of cygwin shell (i.e. typically in a Sys.command). -## So we just forget about it, and do a simple copy. - -ifeq ($(ARCH),win32) -LN:=cp -f -else -LN:=ln -sf -endif - .PHONY: coqbinaries coq coqlib coqlight states -coqbinaries:: ${COQBINARIES} ${CSDPCERT} ${FAKEIDE} +coqbinaries: ${COQBINARIES} ${CSDPCERT} ${FAKEIDE} coq: coqlib tools coqbinaries -coqlib:: theories plugins +coqlib: theories plugins coqlight: theories-light tools coqbinaries -states:: states/initial.coq +states: theories/Init/Prelude.vo + +miniopt: $(COQTOPEXE) pluginsopt +minibyte: $(COQTOPBYTE) pluginsbyte -$(COQTOPOPT): $(BESTCOQMKTOP) $(LINKCMX) $(LIBCOQRUN) +ifeq ($(BEST),opt) +$(COQTOPEXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(TOPLOOPCMA:.cma=.cmxs) $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(BESTCOQMKTOP) -boot -opt $(BAREOPTFLAGS) -o $@ + $(HIDE)$(COQMKTOP) -boot -opt $(OPTFLAGS) $(LINKMETADATA) -thread -o $@ $(STRIP) $@ + $(CODESIGN) $@ +else +$(COQTOPEXE): $(COQTOPBYTE) + cp $< $@ +endif -$(COQTOPBYTE): $(BESTCOQMKTOP) $(LINKCMO) $(LIBCOQRUN) +$(COQTOPBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA) $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(BESTCOQMKTOP) -boot -top $(BAREBYTEFLAGS) -o $@ - -$(COQTOPEXE): $(ORDER_ONLY_SEP) $(BESTCOQTOP) - cd bin && $(LN) coqtop.$(BEST)$(EXE) coqtop$(EXE) + $(HIDE)$(COQMKTOP) -boot -top $(BYTEFLAGS) -thread -o $@ LOCALCHKLIBS:=$(addprefix -I , $(CHKSRCDIRS) ) CHKLIBS:=$(LOCALCHKLIBS) -I $(MYCAMLP4LIB) -CHKBYTEFLAGS:=$(CHKLIBS) $(CAMLDEBUG) $(USERFLAGS) -CHKOPTFLAGS:=$(CHKLIBS) $(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS) -$(CHICKENOPT): checker/check.cmxa checker/main.ml +ifeq ($(BEST),opt) +$(CHICKEN): checker/check.cmxa checker/main.ml $(SHOW)'OCAMLOPT -o $@' - $(HIDE)$(OCAMLOPT) $(CHKOPTFLAGS) -o $@ $(SYSCMXA) $^ + $(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) $(LINKMETADATA) -thread -o $@ $(SYSCMXA) $^ $(STRIP) $@ + $(CODESIGN) $@ +else +$(CHICKEN): $(CHICKENBYTE) + cp $< $@ +endif $(CHICKENBYTE): checker/check.cma checker/main.ml $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(CHKBYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ $(SYSCMA) $^ - -$(CHICKEN): $(ORDER_ONLY_SEP) $(BESTCHICKEN) - cd bin && $(LN) coqchk.$(BEST)$(EXE) coqchk$(EXE) - -# coqmktop - -$(COQMKTOPBYTE): $(COQMKTOPCMO) - $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ $(SYSCMA) $^ $(OSDEPLIBS) + $(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) $(CUSTOM) -thread -o $@ $(SYSCMA) $^ -$(COQMKTOPOPT): $(COQMKTOPCMO:.cmo=.cmx) - $(SHOW)'OCAMLOPT -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ $(SYSCMXA) $^ $(OSDEPLIBS) - $(STRIP) $@ - -$(COQMKTOP): $(ORDER_ONLY_SEP) $(BESTCOQMKTOP) - cd bin && $(LN) coqmktop.$(BEST)$(EXE) coqmktop$(EXE) +# coqmktop +$(COQMKTOP): $(patsubst %.cma,%$(BESTLIB),$(COQMKTOPCMO:.cmo=$(BESTOBJ))) + $(SHOW)'OCAMLBEST -o $@' + $(HIDE)$(call bestocaml, $(OSDEPLIBS), $(SYSMOD)) -scripts/tolink.ml: Makefile.build Makefile.common +tools/tolink.ml: Makefile.build Makefile.common $(SHOW)"ECHO... >" $@ $(HIDE)echo "let copts = \"-cclib -lcoqrun\"" > $@ $(HIDE)echo "let core_libs = \""$(LINKCMO)"\"" >> $@ $(HIDE)echo "let core_objs = \""$(OBJSMOD)"\"" >> $@ # coqc - -$(COQCBYTE): $(COQCCMO) | $(COQTOPBYTE) - $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ $(SYSCMA) $^ $(OSDEPLIBS) - -$(COQCOPT): $(COQCCMO:.cmo=.cmx) | $(COQTOPOPT) - $(SHOW)'OCAMLOPT -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ $(SYSCMXA) $^ $(OSDEPLIBS) - $(STRIP) $@ - -$(COQC): $(ORDER_ONLY_SEP) $(BESTCOQC) - cd bin && $(LN) coqc.$(BEST)$(EXE) coqc$(EXE) +$(COQC): $(patsubst %.cma,%$(BESTLIB),$(COQCCMO:.cmo=$(BESTOBJ))) + $(SHOW)'OCAMLBEST -o $@' + $(HIDE)$(call bestocaml, $(OSDEPLIBS), $(SYSMOD)) # target for libraries %.cma: | %.mllib.d $(SHOW)'OCAMLC -a -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $^ + $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -a -o $@ $^ %.cmxa: | %.mllib.d $(SHOW)'OCAMLOPT -a -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $^ + $(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -a -o $@ $^ # For the checker, different flags may be used checker/check.cma: | checker/check.mllib.d $(SHOW)'OCAMLC -a -o $@' - $(HIDE)$(OCAMLC) $(CHKBYTEFLAGS) -a -o $@ $^ + $(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) -a -o $@ $^ checker/check.cmxa: | checker/check.mllib.d $(SHOW)'OCAMLOPT -a -o $@' - $(HIDE)$(OCAMLOPT) $(CHKOPTFLAGS) -a -o $@ $^ + $(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) -a -o $@ $^ ########################################################################### # Csdp to micromega special targets @@ -313,87 +305,191 @@ plugins/micromega/csdpcert$(EXE): $(CSDPCERTCMO:.cmo=$(BESTOBJ)) .PHONY: coqide coqide-binaries coqide-no coqide-byte coqide-opt coqide-files # target to build CoqIde -coqide:: coqide-files coqide-binaries states +coqide: coqide-files coqide-binaries theories/Init/Prelude.vo -COQIDEFLAGS=-thread $(COQIDEINCLUDES) +COQIDEFLAGS=$(addprefix -I , $(IDESRCDIRS)) $(COQIDEINCLUDES) .SUFFIXES:.vo -IDEFILES=ide/coq.png ide/coqide-gtk2rc ide/mac_default_accel_map +IDEFILES=$(wildcard ide/*.lang) ide/coq_style.xml ide/coq.png ide/MacOS/default_accel_map -coqide-binaries: coqide-$(HASCOQIDE) +coqide-binaries: coqide-$(HASCOQIDE) ide-toploop coqide-no: coqide-byte: $(COQIDEBYTE) $(COQIDE) -coqide-opt: $(COQIDEBYTE) $(COQIDEOPT) $(COQIDE) +coqide-opt: $(COQIDEBYTE) $(COQIDE) coqide-files: $(IDEFILES) +ifeq ($(BEST),opt) +ide-toploop: $(IDETOPLOOPCMA) $(IDETOPLOOPCMA:.cma=.cmxs) +else +ide-toploop: $(IDETOPLOOPCMA) +endif -$(COQIDEOPT): $(LINKIDEOPT) | $(COQTOPOPT) +ifeq ($(HASCOQIDE),opt) +$(COQIDE): $(LINKIDEOPT) $(SHOW)'OCAMLOPT -o $@' - $(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ unix.cmxa threads.cmxa \ - lablgtk.cmxa $(IDEOPTFLAGS) gtkThread.cmx str.cmxa $(LINKIDEOPT) + $(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ unix.cmxa threads.cmxa lablgtk.cmxa \ + lablgtksourceview2.cmxa str.cmxa $(IDEFLAGS:.cma=.cmxa) $^ $(STRIP) $@ +else +$(COQIDE): $(COQIDEBYTE) + cp $< $@ +endif -$(COQIDEBYTE): $(LINKIDE) | $(COQTOPBYTE) +$(COQIDEBYTE): $(LINKIDE) $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ unix.cma threads.cma lablgtk.cma gtkThread.cmo\ - str.cma $(COQRUNBYTEFLAGS) $(LINKIDE) - -$(COQIDE): - cd bin && $(LN) coqide.$(HASCOQIDE)$(EXE) coqide$(EXE) + $(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ unix.cma threads.cma lablgtk.cma \ + lablgtksourceview2.cma str.cma $(IDEFLAGS) $(IDECDEPSFLAGS) $^ # install targets -.PHONY: install-coqide install-ide-no install-ide-byte install-ide-opt -.PHONY: install-ide-files install-ide-info install-im +.PHONY: install-coqide install-ide-bin install-ide-toploop install-ide-files install-ide-info install-ide-devfiles -install-coqide:: install-ide-$(HASCOQIDE) install-ide-files install-ide-info - -install-ide-no: +ifeq ($(HASCOQIDE),no) +install-coqide: install-ide-toploop +else +install-coqide: install-ide-bin install-ide-toploop install-ide-files install-ide-info install-ide-devfiles +endif -install-ide-byte: +install-ide-bin: $(MKDIR) $(FULLBINDIR) - $(INSTALLBIN) $(COQIDEBYTE) $(FULLBINDIR) - $(INSTALLSH) $(FULLCOQLIB) $(IDECMA) \ - $(foreach lib,$(IDECMA:.cma=_MLLIB_DEPENDENCIES),$(addsuffix .cmi,$($(lib)))) - cd $(FULLBINDIR) && $(LN) coqide.byte$(EXE) coqide$(EXE) + $(INSTALLBIN) $(COQIDE) $(FULLBINDIR) -install-ide-opt: - $(MKDIR) $(FULLBINDIR) - $(INSTALLBIN) $(COQIDEOPT) $(FULLBINDIR) - $(INSTALLSH) $(FULLCOQLIB) $(IDECMA) $(IDECMA:.cma=.cmxa) $(IDECMA:.cma=.a) \ +install-ide-toploop: + $(MKDIR) $(FULLCOQLIB)/toploop + $(INSTALLBIN) $(IDETOPLOOPCMA) $(FULLCOQLIB)/toploop/ +ifeq ($(BEST),opt) + $(INSTALLBIN) $(IDETOPLOOPCMA:.cma=.cmxs) $(FULLCOQLIB)/toploop/ +endif + +install-ide-devfiles: + $(MKDIR) $(FULLCOQLIB) + $(INSTALLSH) $(FULLCOQLIB) $(IDECMA) \ $(foreach lib,$(IDECMA:.cma=_MLLIB_DEPENDENCIES),$(addsuffix .cmi,$($(lib)))) - cd $(FULLBINDIR) && $(LN) coqide.opt$(EXE) coqide$(EXE) +ifeq ($(BEST),opt) + $(INSTALLSH) $(FULLCOQLIB) $(IDECMA:.cma=.cmxa) $(IDECMA:.cma=.a) +endif -install-ide-files: +install-ide-files: #Please update $(COQIDEAPP)/Contents/Resources/ at the same time $(MKDIR) $(FULLDATADIR) - $(INSTALLLIB) ide/coq.png $(FULLDATADIR) + $(INSTALLLIB) ide/coq.png ide/*.lang ide/coq_style.xml $(FULLDATADIR) $(MKDIR) $(FULLCONFIGDIR) - $(INSTALLLIB) ide/coqide-gtk2rc $(FULLCONFIGDIR) - if [ $(IDEOPTINT) = QUARTZ ] ; then $(INSTALLLIB) ide/mac_default_accel_map $(FULLCONFIGDIR)/coqide.keys ; fi + if [ $(IDEINT) = QUARTZ ] ; then $(INSTALLLIB) ide/mac_default_accel_map $(FULLCONFIGDIR)/coqide.keys ; fi install-ide-info: $(MKDIR) $(FULLDOCDIR) $(INSTALLLIB) ide/FAQ $(FULLDOCDIR)/FAQ-CoqIde +########################################################################### +# CoqIde MacOS special targets +########################################################################### + +.PHONY: $(COQIDEAPP)/Contents + +$(COQIDEAPP)/Contents: + rm -rdf $@ + $(MKDIR) $@ + sed -e "s/VERSION/$(VERSION)/g" ide/MacOS/Info.plist.template > $@/Info.plist + $(MKDIR) "$@/MacOS" + +$(COQIDEINAPP): ide/macos_prehook.cmx $(LINKIDEOPT) | $(COQIDEAPP)/Contents + $(SHOW)'OCAMLOPT -o $@' + $(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ \ + unix.cmxa lablgtk.cmxa lablgtksourceview2.cmxa str.cmxa \ + threads.cmxa $(IDEFLAGS:.cma=.cmxa) $^ + $(STRIP) $@ + +$(COQIDEAPP)/Contents/Resources/share: $(COQIDEAPP)/Contents + $(MKDIR) $@/coq/ + $(INSTALLLIB) ide/coq.png ide/*.lang ide/coq_style.xml $@/coq/ + $(MKDIR) $@/gtksourceview-2.0/{language-specs,styles} + $(INSTALLLIB) "$(GTKSHARE)/"gtksourceview-2.0/language-specs/{def.lang,language2.rng} $@/gtksourceview-2.0/language-specs/ + $(INSTALLLIB) "$(GTKSHARE)/"gtksourceview-2.0/styles/{styles.rng,classic.xml} $@/gtksourceview-2.0/styles/ + cp -R "$(GTKSHARE)/"locale $@ + cp -R "$(GTKSHARE)/"icons $@ + cp -R "$(GTKSHARE)/"themes $@ + +$(COQIDEAPP)/Contents/Resources/loaders: $(COQIDEAPP)/Contents + $(MKDIR) $@ + $(INSTALLLIB) $$("$(GTKBIN)/gdk-pixbuf-query-loaders" | sed -n -e '5 s!.*= \(.*\)$$!\1!p')/libpixbufloader-png.so $@ + +$(COQIDEAPP)/Contents/Resources/immodules: $(COQIDEAPP)/Contents + $(MKDIR) $@ + $(INSTALLLIB) "$(GTKLIBS)/gtk-2.0/2.10.0/immodules/"*.so $@ + + +$(COQIDEAPP)/Contents/Resources/etc: $(COQIDEAPP)/Contents/Resources/lib + $(MKDIR) $@/xdg/coq + $(INSTALLLIB) ide/MacOS/default_accel_map $@/xdg/coq/coqide.keys + $(MKDIR) $@/gtk-2.0 + { "$(GTKBIN)/gdk-pixbuf-query-loaders" $@/../loaders/*.so |\ + sed -e "s!/.*\(/loaders/.*.so\)!@executable_path/../Resources/\1!"; } \ + > $@/gtk-2.0/gdk-pixbuf.loaders + { "$(GTKBIN)/gtk-query-immodules-2.0" $@/../immodules/*.so |\ + sed -e "s!/.*\(/immodules/.*.so\)!@executable_path/../Resources/\1!" |\ + sed -e "s!/.*\(/share/locale\)!@executable_path/../Resources/\1!"; } \ + > $@/gtk-2.0/gtk-immodules.loaders + $(MKDIR) $@/pango + echo "[Pango]" > $@/pango/pangorc + +$(COQIDEAPP)/Contents/Resources/lib: $(COQIDEAPP)/Contents/Resources/immodules $(COQIDEAPP)/Contents/Resources/loaders $(COQIDEAPP)/Contents $(COQIDEINAPP) + $(MKDIR) $@ + $(INSTALLLIB) $(GTKLIBS)/charset.alias $@/ + $(MKDIR) $@/pango/1.8.0/modules + $(INSTALLLIB) "$(GTKLIBS)/pango/1.8.0/modules/"*.so $@/pango/1.8.0/modules/ + { "$(GTKBIN)/pango-querymodules" $@/pango/1.8.0/modules/*.so |\ + sed -e "s!/.*\(/pango/1.8.0/modules/.*.so\)!@executable_path/../Resources/lib\1!"; } \ + > $@/pango/1.8.0/modules.cache + + for i in $$(otool -L $(COQIDEINAPP) |sed -n -e "\@$(GTKLIBS)@ s/[^/]*\(\/[^ ]*\) .*$$/\1/p"); \ + do cp $$i $@/; \ + ide/MacOS/relatify_with-respect-to_.sh $@/$$(basename $$i) $(GTKLIBS) $@; \ + done + for i in $@/../loaders/*.so $@/../immodules/*.so $@/pango/1.8.0/modules/*.so; \ + do \ + for j in $$(otool -L $$i | sed -n -e "\@$(GTKLIBS)@ s/[^/]*\(\/[^ ]*\) .*$$/\1/p"); \ + do cp $$j $@/; ide/MacOS/relatify_with-respect-to_.sh $@/$$(basename $$j) $(GTKLIBS) $@; done; \ + ide/MacOS/relatify_with-respect-to_.sh $$i $(GTKLIBS) $@; \ + done + EXTRAWORK=1; \ + while [ $${EXTRAWORK} -eq 1 ]; \ + do EXTRAWORK=0; \ + for i in $@/*.dylib; \ + do for j in $$(otool -L $$i | sed -n -e "\@$(GTKLIBS)@ s/[^/]*\(\/[^ ]*\) .*$$/\1/p"); \ + do EXTRAWORK=1; cp $$j $@/; ide/MacOS/relatify_with-respect-to_.sh $@/$$(basename $$j) $(GTKLIBS) $@; done; \ + done; \ + done + ide/MacOS/relatify_with-respect-to_.sh $(COQIDEINAPP) $(GTKLIBS) $@ + +$(COQIDEAPP)/Contents/Resources:$(COQIDEAPP)/Contents/Resources/etc $(COQIDEAPP)/Contents/Resources/share + $(INSTALLLIB) ide/MacOS/*.icns $@ + +$(COQIDEAPP):$(COQIDEAPP)/Contents/Resources + $(CODESIGN) $@ + ########################################################################### # tests ########################################################################### -.PHONY: validate check test-suite $(ALLSTDLIB).v +.PHONY: validate check test-suite $(ALLSTDLIB).v md5chk -VALIDOPTS=-silent -o -m +md5chk: + $(SHOW)'MD5SUM cic.mli' + $(HIDE)if grep -q `$(MD5SUM) checker/cic.mli` checker/values.ml; \ + then true; else echo "Error: outdated checker/values.ml"; false; fi -validate:: $(BESTCHICKEN) $(ALLVO) +VALIDOPTS=$(if $(VERBOSE),,-silent) -o -m + +validate: $(CHICKEN) md5chk | $(ALLVO) $(SHOW)'COQCHK ' - $(HIDE)$(BESTCHICKEN) -boot $(VALIDOPTS) $(ALLMODS) + $(HIDE)$(CHICKEN) -boot $(VALIDOPTS) $(ALLMODS) $(ALLSTDLIB).v: $(SHOW)'MAKE $(notdir $@)' $(HIDE)echo "Require $(ALLMODS)." > $@ -MAKE_TSOPTS=-C test-suite -s BEST=$(BEST) VERBOSE=$(VERBOSE) +MAKE_TSOPTS=-C test-suite -s VERBOSE=$(VERBOSE) -check:: validate test-suite +check: validate test-suite test-suite: world $(ALLSTDLIB).v $(MAKE) $(MAKE_TSOPTS) clean @@ -405,9 +501,9 @@ test-suite: world $(ALLSTDLIB).v ################################################################## .PHONY: lib kernel byterun library proofs tactics interp parsing pretyping -.PHONY: highparsing toplevel hightactics +.PHONY: highparsing stm toplevel hightactics -lib: lib/lib.cma +lib: lib/clib.cma lib/lib.cma kernel: kernel/kernel.cma byterun: $(BYTERUN) library: library/library.cma @@ -417,6 +513,7 @@ interp: interp/interp.cma parsing: parsing/parsing.cma pretyping: pretyping/pretyping.cma highparsing: parsing/highparsing.cma +stm: stm/stm.cma toplevel: toplevel/toplevel.cma hightactics: tactics/hightactics.cma @@ -455,45 +552,39 @@ program: $(PROGRAMVO) structures: $(STRUCTURESVO) vectors: $(VECTORSVO) -noreal: logic arith bool zarith qarith lists sets fsets relations \ - wellfounded setoids sorting +noreal: unicode logic arith bool zarith qarith lists sets fsets \ + relations wellfounded setoids sorting ########################################################################### # 3) plugins ########################################################################### -.PHONY: plugins omega micromega ring setoid_ring nsatz xml extraction -.PHONY: field fourier funind cc subtac rtauto pluginsopt +.PHONY: plugins omega micromega setoid_ring nsatz extraction +.PHONY: fourier funind cc rtauto btauto pluginsopt pluginsbyte plugins: $(PLUGINSVO) omega: $(OMEGAVO) $(OMEGACMA) $(ROMEGAVO) $(ROMEGACMA) micromega: $(MICROMEGAVO) $(MICROMEGACMA) $(CSDPCERT) -ring: $(RINGVO) $(RINGCMA) -setoid_ring: $(NEWRINGVO) $(NEWRINGCMA) +setoid_ring: $(RINGVO) $(RINGCMA) nsatz: $(NSATZVO) $(NSATZCMA) -xml: $(XMLVO) $(XMLCMA) extraction: $(EXTRACTIONCMA) -field: $(FIELDVO) $(FIELDCMA) fourier: $(FOURIERVO) $(FOURIERCMA) funind: $(FUNINDCMA) $(FUNINDVO) cc: $(CCVO) $(CCCMA) -subtac: $(SUBTACCMA) rtauto: $(RTAUTOVO) $(RTAUTOCMA) +btauto: $(BTAUTOVO) $(BTAUTOCMA) pluginsopt: $(PLUGINSOPT) +pluginsbyte: $(PLUGINS) ########################################################################### -# rules to make theories, plugins and states +# rules to make theories and plugins ########################################################################### -states/initial.coq: states/MakeInitial.v $(INITVO) $(VO_TOOLS_STRICT) | states/MakeInitial.v.d $(VO_TOOLS_ORDER_ONLY) - $(SHOW)'BUILD $@' - $(HIDE)$(BOOTCOQTOP) -batch -notop -silent -nois -load-vernac-source states/MakeInitial.v -outputstate states/initial.coq - -theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_STRICT) | theories/Init/%.v.d $(VO_TOOLS_ORDER_ONLY) - $(SHOW)'COQC -nois $<' +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/$* -nois + $(HIDE)$(BOOTCOQC) theories/Init/$* -noinit -R theories Coq theories/Numbers/Natural/BigN/NMake_gen.v: theories/Numbers/Natural/BigN/NMake_gen.ml $(OCAML) $< $(TOTARGET) @@ -506,7 +597,7 @@ theories/Numbers/Natural/BigN/NMake_gen.v: theories/Numbers/Natural/BigN/NMake_g printers: $(DEBUGPRINTERS) -tools:: $(TOOLS) $(DEBUGPRINTERS) $(COQDEPBOOT) +tools: $(TOOLS) $(DEBUGPRINTERS) $(COQDEPBOOT) # coqdep_boot : a basic version of coqdep, with almost no dependencies. @@ -525,7 +616,7 @@ $(COQDEPBOOT): $(COQDEPBOOTSRC) # the full coqdep -$(COQDEP): $(COQDEPCMO:.cmo=$(BESTOBJ)) +$(COQDEP): $(patsubst %.cma,%$(BESTLIB),$(COQDEPCMO:.cmo=$(BESTOBJ))) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml, $(OSDEPLIBS), $(SYSMOD)) @@ -533,9 +624,9 @@ $(GALLINA): $(addsuffix $(BESTOBJ), tools/gallina_lexer tools/gallina) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml,,) -$(COQMAKEFILE): $(addsuffix $(BESTOBJ),config/coq_config ide/minilib ide/project_file tools/coq_makefile) +$(COQMAKEFILE): $(patsubst %.cma,%$(BESTLIB),$(COQMAKEFILECMO:.cmo=$(BESTOBJ))) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml,,str unix) + $(HIDE)$(call bestocaml,,str unix threads) $(COQTEX): tools/coq_tex$(BESTOBJ) $(SHOW)'OCAMLBEST -o $@' @@ -545,24 +636,35 @@ $(COQWC): tools/coqwc$(BESTOBJ) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml,,) -$(COQDOC): $(COQDOCCMO:.cmo=$(BESTOBJ)) +$(COQDOC): $(patsubst %.cma,%$(BESTLIB),$(COQDOCCMO:.cmo=$(BESTOBJ))) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml,,str unix) +$(COQWORKMGR): $(addsuffix $(BESTOBJ), stm/coqworkmgrApi tools/coqworkmgr) \ + $(addsuffix $(BESTLIB), lib/clib) + $(SHOW)'OCAMLBEST -o $@' + $(HIDE)$(call bestocaml,, $(SYSMOD) clib) + # fake_ide : for debugging or test-suite purpose, a fake ide simulating # a connection to coqtop -ideslave -$(FAKEIDE): lib/xml_lexer$(BESTOBJ) lib/xml_parser$(BESTOBJ) lib/xml_utils$(BESTOBJ) toplevel/ide_intf$(BESTOBJ) tools/fake_ide$(BESTOBJ) +$(FAKEIDE): lib/clib$(BESTLIB) lib/xml_lexer$(BESTOBJ) lib/xml_parser$(BESTOBJ) lib/xml_printer$(BESTOBJ) lib/errors$(BESTOBJ) lib/spawn$(BESTOBJ) ide/document$(BESTOBJ) ide/xmlprotocol$(BESTOBJ) tools/fake_ide$(BESTOBJ) | $(IDETOPLOOPCMA:.cma=$(BESTDYN)) + $(SHOW)'OCAMLBEST -o $@' + $(HIDE)$(call bestocaml,-I ide,str unix threads) + +# votour: a small vo explorer (based on the checker) + +bin/votour: lib/cObj$(BESTOBJ) checker/values$(BESTOBJ) checker/votour.ml $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml,,unix) + $(HIDE)$(call bestocaml, -I checker,) # Special rule for the compatibility-with-camlp5 extension for camlp4 ifeq ($(CAMLP4),camlp4) tools/compat5.cmo: tools/compat5.mlp - $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) -impl' -impl $< + $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) $(CAMLP4FLAGS) -impl' -impl $< tools/compat5b.cmo: tools/compat5b.mlp - $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) -impl' -impl $< + $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) $(CAMLP4FLAGS) -impl' -impl $< else tools/compat5.cmo: tools/compat5.ml $(OCAMLC) -c $< @@ -570,10 +672,32 @@ tools/compat5b.cmo: tools/compat5b.ml $(OCAMLC) -c $< endif +########################################################################### +# Documentation : cf Makefile.doc +########################################################################### + +documentation: doc-$(WITHDOC) +doc-all: doc +doc-no: + +.PHONY: documentation doc-all doc-no + ########################################################################### # Installation ########################################################################### +ifeq ($(LOCAL),true) +install: + @echo "Nothing to install in a local build!" +else +install: install-coq install-coqide install-doc-$(WITHDOC) +endif + +install-doc-all: install-doc +install-doc-no: + +.PHONY: install install-doc-all install-doc-no + #These variables are intended to be set by the caller to make #COQINSTALLPREFIX= #OLDROOT= @@ -602,25 +726,23 @@ FULLDOCDIR=$(DOCDIR) endif .PHONY: install-coq install-coqlight install-binaries install-byte install-opt -.PHONY: install-tools install-library install-library-light +.PHONY: install-tools install-library install-library-light install-devfiles .PHONY: install-coq-info install-coq-manpages install-emacs install-latex -install-coq: install-binaries install-library install-coq-info +install-coq: install-binaries install-library install-coq-info install-devfiles install-coqlight: install-binaries install-library-light -install-binaries:: install-$(BEST) install-tools - -install-byte:: +install-binaries: install-tools $(MKDIR) $(FULLBINDIR) - $(INSTALLBIN) $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(CHICKEN) $(FULLBINDIR) - cd $(FULLBINDIR); $(LN) coqtop.byte$(EXE) coqtop$(EXE); $(LN) coqchk.byte$(EXE) coqchk$(EXE) + $(INSTALLBIN) $(COQC) $(COQTOPBYTE) $(COQTOPEXE) $(CHICKEN) $(FULLBINDIR) + $(MKDIR) $(FULLCOQLIB)/toploop + $(INSTALLBIN) $(TOPLOOPCMA) $(FULLCOQLIB)/toploop/ +ifeq ($(BEST),opt) + $(INSTALLBIN) $(TOPLOOPCMA:.cma=.cmxs) $(FULLCOQLIB)/toploop/ +endif -install-opt:: - $(MKDIR) $(FULLBINDIR) - $(INSTALLBIN) $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(COQTOPOPT) $(CHICKEN) $(CHICKENOPT) $(FULLBINDIR) - cd $(FULLBINDIR); $(LN) coqtop.opt$(EXE) coqtop$(EXE); $(LN) coqchk.opt$(EXE) coqchk$(EXE) -install-tools:: +install-tools: $(MKDIR) $(FULLBINDIR) # recopie des fichiers de style pour coqide $(MKDIR) $(FULLCOQLIB)/tools/coqdoc @@ -632,24 +754,29 @@ install-tools:: # from .mli without .ml, and the ones obtained from .ml without .mli INSTALLCMI = $(sort \ - $(CONFIG:.cmo=.cmi) \ $(filter-out checker/% ide/% tools/%, $(MLIFILES:.mli=.cmi)) \ $(foreach lib,$(CORECMA) $(PLUGINSCMA), $(addsuffix .cmi,$($(lib:.cma=_MLLIB_DEPENDENCIES))))) +install-devfiles: + $(MKDIR) $(FULLBINDIR) + $(INSTALLBIN) $(COQMKTOP) $(FULLBINDIR) + $(MKDIR) $(FULLCOQLIB) + $(INSTALLSH) $(FULLCOQLIB) $(LINKCMO) $(GRAMMARCMA) + $(INSTALLSH) $(FULLCOQLIB) $(INSTALLCMI) +ifeq ($(BEST),opt) + $(INSTALLSH) $(FULLCOQLIB) $(LINKCMX) $(CORECMA:.cma=.a) $(STATICPLUGINS:.cma=.a) +endif + install-library: $(MKDIR) $(FULLCOQLIB) $(INSTALLSH) $(FULLCOQLIB) $(LIBFILES) $(PLUGINS) - $(MKDIR) $(FULLCOQLIB)/states - $(INSTALLLIB) states/*.coq $(FULLCOQLIB)/states $(MKDIR) $(FULLCOQLIB)/user-contrib -ifneq ($(COQRUNBYTEFLAGS),"-custom") +ifndef CUSTOM $(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB) endif - $(INSTALLSH) $(FULLCOQLIB) $(CONFIG) $(LINKCMO) $(GRAMMARCMA) - $(INSTALLSH) $(FULLCOQLIB) $(INSTALLCMI) ifeq ($(BEST),opt) $(INSTALLLIB) $(LIBCOQRUN) $(FULLCOQLIB) - $(INSTALLSH) $(FULLCOQLIB) $(CONFIG:.cmo=.cmx) $(CONFIG:.cmo=.o) $(LINKCMO:.cma=.cmxa) $(LINKCMO:.cma=.a) $(PLUGINSOPT) + $(INSTALLSH) $(FULLCOQLIB) $(PLUGINSOPT) endif # csdpcert is not meant to be directly called by the user; we install # it with libraries @@ -661,11 +788,13 @@ endif install-library-light: $(MKDIR) $(FULLCOQLIB) $(INSTALLSH) $(FULLCOQLIB) $(LIBFILESLIGHT) $(INITPLUGINS) - $(MKDIR) $(FULLCOQLIB)/states - $(INSTALLLIB) states/*.coq $(FULLCOQLIB)/states rm -f $(FULLCOQLIB)/revision -$(INSTALLLIB) revision $(FULLCOQLIB) +ifndef CUSTOM + $(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB) +endif ifeq ($(BEST),opt) + $(INSTALLLIB) $(LIBCOQRUN) $(FULLCOQLIB) $(INSTALLSH) $(FULLCOQLIB) $(INITPLUGINSOPT) endif @@ -677,7 +806,7 @@ install-coq-manpages: install-emacs: $(MKDIR) $(FULLEMACSLIB) - $(INSTALLLIB) tools/coq-db.el tools/coq-font-lock.el tools/coq-syntax.el tools/coq.el tools/coq-inferior.el $(FULLEMACSLIB) + $(INSTALLLIB) tools/gallina-db.el tools/coq-font-lock.el tools/gallina-syntax.el tools/gallina.el tools/coq-inferior.el $(FULLEMACSLIB) # command to update TeX' kpathsea database #UPDATETEX = $(MKTEXLSR) /usr/share/texmf /var/spool/texmf $(BASETEXDIR) > /dev/null @@ -695,17 +824,21 @@ install-latex: source-doc: mli-doc $(OCAMLDOCDIR)/coq.pdf -$(OCAMLDOCDIR)/coq.tex:: $(DOCMLIS:.mli=.cmi) +$(OCAMLDOCDIR)/coq.tex: $(DOCMLIS:.mli=.cmi) $(OCAMLDOC) -latex -rectypes -I $(MYCAMLP4LIB) $(MLINCLUDES)\ $(DOCMLIS) -t "Coq mlis documentation" \ -intro $(OCAMLDOCDIR)/docintro -o $@ -mli-doc:: $(DOCMLIS:.mli=.cmi) - $(OCAMLDOC) -html -rectypes -I $(MYCAMLP4LIB) $(MLINCLUDES)\ +mli-doc: $(DOCMLIS:.mli=.cmi) + $(OCAMLDOC) -html -rectypes -I +threads -I $(MYCAMLP4LIB) $(MLINCLUDES) \ $(DOCMLIS) -d $(OCAMLDOCDIR)/html -colorize-code \ -t "Coq mlis documentation" -intro $(OCAMLDOCDIR)/docintro \ -css-style style.css +ml-dot: $(MLFILES) + $(OCAMLDOC) -dot -dot-reduce -rectypes -I +threads -I $(CAMLLIB) -I $(MYCAMLP4LIB) $(MLINCLUDES) \ + $(filter $(addsuffix /%.ml,$(CORESRCDIRS)),$(MLFILES)) -o $(OCAMLDOCDIR)/coq.dot + %_dep.png: %.dot $(DOT) -Tpng $< -o $@ @@ -719,11 +852,14 @@ OCAMLDOC_MLLIBD = $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ \ $(OCAMLDOC_MLLIBD) ml-doc: - $(OCAMLDOC) -html -rectypes $(LOCALINCLUDES) -d $(SOURCEDOCDIR) $(MLSTATICFILES) + $(OCAMLDOC) -html -rectypes -I +threads $(MLINCLUDES) $(COQIDEFLAGS) -d $(OCAMLDOCDIR) $(MLSTATICFILES) parsing/parsing.dot : | parsing/parsing.mllib.d parsing/highparsing.mllib.d $(OCAMLDOC_MLLIBD) +grammar/grammar.dot : | grammar/grammar.mllib.d + $(OCAMLDOC_MLLIBD) + tactics/tactics.dot: | tactics/tactics.mllib.d tactics/hightactics.mllib.d $(OCAMLDOC_MLLIBD) @@ -739,46 +875,23 @@ $(OCAMLDOCDIR)/%.pdf: $(OCAMLDOCDIR)/%.tex dev/printers.cma: | dev/printers.mllib.d $(SHOW)'Testing $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(SYSCMA) $^ -o test-printer + $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -thread $(SYSCMA) $(P4CMA) $^ -o test-printer @rm -f test-printer $(SHOW)'OCAMLC -a $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) $^ -linkall -a -o $@ + $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -thread $(SYSCMA) $^ -linkall -a -o $@ -parsing/grammar.cma: | parsing/grammar.mllib.d +grammar/grammar.cma: | grammar/grammar.mllib.d $(SHOW)'Testing $@' @touch test.ml4 - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp '$(CAMLP4O) -I $(CAMLLIB) $^ -impl' -impl test.ml4 -o test-grammar + $(HIDE)$(CAMLP4O) $(CAMLP4FLAGS) $^ -impl test.ml4 -o test.ml + $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) test.ml -o test-grammar @rm -f test-grammar test.* $(SHOW)'OCAMLC -a $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) $^ -linkall -a -o $@ - -# toplevel/mltop.ml4 (ifdef Byte) + $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $^ -linkall -a -o $@ -## NB: mltop.ml correspond to the byte version (and hence need no special rules) -## while the opt version is in mltop.optml. Since mltop.optml uses mltop.ml.d -## as dependency file, be sure to import the same modules in the different sections -## of the ml4 - -toplevel/mltop.cmx: toplevel/mltop.optml | toplevel/mltop.ml.d toplevel/mltop.ml4.d - $(SHOW)'OCAMLOPT $<' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -c -impl $< -o $@ - -toplevel/mltop.ml: toplevel/mltop.ml4 config/Makefile # no camlp4deps here - $(SHOW)'CAMLP4O $<' - $(HIDE)$(CAMLP4O) $(PR_O) $(CAMLP4USE) -DByte -DHasDynlink -impl $< -o $@ - -toplevel/mltop.optml: toplevel/mltop.ml4 config/Makefile # no camlp4deps here - $(SHOW)'CAMLP4O $<' - $(HIDE)$(CAMLP4O) $(PR_O) $(CAMLP4USE) $(NATDYNLINKDEF) -impl $< -o $@ - -ide/coqide_main.ml: ide/coqide_main.ml4 +ide/coqide_main.ml: ide/coqide_main.ml4 config/Makefile # no camlp4deps here $(SHOW)'CAMLP4O $<' - $(HIDE)$(CAMLP4O) $(CAMLP4USE) -impl $< -o $@ - -ide/coqide_main_opt.ml: ide/coqide_main.ml4 config/Makefile # no camlp4deps here - $(SHOW)'CAMLP4O $<' - $(HIDE)$(CAMLP4O) $(CAMLP4USE) -D$(IDEOPTINT) -impl $< -o $@ - + $(HIDE)$(CAMLP4O) $(CAMLP4FLAGS) $(PR_O) $(CAMLP4USE) -D$(IDEINT) -impl $< -o $@ # pretty printing of the revision number when compiling a checked out # source tree @@ -834,17 +947,23 @@ endif ## Three flavor of flags: checker/* ide/* and normal files COND_BYTEFLAGS= \ - $(if $(filter checker/%,$<), $(CHKBYTEFLAGS), \ - $(if $(filter ide/%,$<),$(COQIDEFLAGS),) $(BYTEFLAGS)) + $(if $(filter checker/%,$<), $(CHKLIBS) -thread, \ + $(if $(filter ide/%,$<), $(COQIDEFLAGS), \ + $(if $(filter tools/fake_ide% tools/coq_makefile%,$<), -I ide,) $(MLINCLUDES) -thread)) $(BYTEFLAGS) COND_OPTFLAGS= \ - $(if $(filter checker/%,$<), $(CHKOPTFLAGS), \ - $(if $(filter ide/%,$<),$(COQIDEFLAGS),) $(OPTFLAGS)) + $(if $(filter checker/%,$<), $(CHKLIBS) -thread, \ + $(if $(filter ide/%,$<), $(COQIDEFLAGS), \ + $(if $(filter tools/fake_ide% tools/coq_makefile%,$<), -I ide,) $(MLINCLUDES) -thread)) $(OPTFLAGS) %.o: %.c $(SHOW)'OCAMLC $<' $(HIDE)cd $(dir $<) && $(OCAMLC) -ccopt "$(CFLAGS)" -c $(notdir $<) +%.o: %.rc + $(SHOW)'WINDRES $<' + $(HIDE)i686-w64-mingw32-windres -i $< -o $@ + %.cmi: %.mli | %.mli.d $(SHOW)'OCAMLC $<' $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -c $< @@ -910,19 +1029,16 @@ plugins/%_mod.ml: plugins/%.mllib %.ml: %.ml4 | %.ml4.d tools/compat5.cmo tools/compat5b.cmo $(SHOW)'CAMLP4O $<' - $(HIDE)\ - DEPS=$(CAMLP4DEPS); \ - if ls $${DEPS} > /dev/null 2>&1; then \ - $(CAMLP4O) $(PR_O) -I $(CAMLLIB) tools/compat5.cmo $${DEPS} $(CAMLP4USE) $(CAMLP4COMPAT) -impl $< -o $@; \ - else echo $< : Dependency $${DEPS} not ready yet; false; fi + $(HIDE)$(CAMLP4O) $(CAMLP4FLAGS) $(PR_O) tools/compat5.cmo \ + $(call CAMLP4DEPS,$<) $(CAMLP4USE) $(CAMLP4COMPAT) -impl $< -o $@ -%.vo %.glob: %.v states/initial.coq $(INITPLUGINSBEST) $(VO_TOOLS_STRICT) | %.v.d $(VO_TOOLS_ORDER_ONLY) +%.vo %.glob: %.v theories/Init/Prelude.vo $(VO_TOOLS_DEP) | %.v.d $(SHOW)'COQC $<' $(HIDE)rm -f $*.glob $(HIDE)$(BOOTCOQC) $* ifdef VALIDATE $(SHOW)'COQCHK $(call vo_to_mod,$@)' - $(HIDE)$(BESTCHICKEN) -boot -silent -norec $(call vo_to_mod,$@) \ + $(HIDE)$(CHICKEN) -boot -silent -norec $(call vo_to_mod,$@) \ || ( RV=$$?; rm -f "$@"; exit $${RV} ) endif @@ -935,20 +1051,20 @@ endif %.ml4.d: $(D_DEPEND_BEFORE_SRC) %.ml4 $(SHOW)'CAMLP4DEPS $<' - $(HIDE)echo "$*.ml: $(if $(NO_RECOMPILE_ML4),$(ORDER_ONLY_SEP)) $(CAMLP4DEPS)" $(TOTARGET) + $(HIDE)echo "$*.ml: $(if $(NO_RECOMPILE_ML4),$(ORDER_ONLY_SEP)) $(call CAMLP4DEPS,$<)" $(TOTARGET) -# We now use coqdep_boot to wrap around ocamldep -modules, since it is aware -# of .ml4 files +# Since OCaml 3.12.1, we could use again ocamldep directly, thanks to +# the option -ml-synonym -OCAMLDEP_NG = $(COQDEPBOOT) -mldep $(OCAMLDEP) +OCAMLDEP_NG = $(OCAMLDEP) -slash -ml-synonym .ml4 checker/%.ml.d: $(D_DEPEND_BEFORE_SRC) checker/%.ml $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES) $(SHOW)'OCAMLDEP $<' - $(HIDE)$(OCAMLDEP_NG) -slash $(LOCALCHKLIBS) "$<" $(TOTARGET) + $(HIDE)$(OCAMLDEP_NG) $(LOCALCHKLIBS) "$<" $(TOTARGET) checker/%.mli.d: $(D_DEPEND_BEFORE_SRC) checker/%.mli $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES) $(SHOW)'OCAMLDEP $<' - $(HIDE)$(OCAMLDEP_NG) -slash $(LOCALCHKLIBS) "$<" $(TOTARGET) + $(HIDE)$(OCAMLDEP_NG) $(LOCALCHKLIBS) "$<" $(TOTARGET) %.ml.d: $(D_DEPEND_BEFORE_SRC) %.ml $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES) $(SHOW)'OCAMLDEP $<' @@ -960,15 +1076,15 @@ checker/%.mli.d: $(D_DEPEND_BEFORE_SRC) checker/%.mli $(D_DEPEND_AFTER_SRC) $(CO checker/%.mllib.d: $(D_DEPEND_BEFORE_SRC) checker/%.mllib $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES) $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEPBOOT) -slash -I checker -c "$<" $(TOTARGET) + $(HIDE)$(COQDEPBOOT) -I checker -c "$<" $(TOTARGET) %.mllib.d: $(D_DEPEND_BEFORE_SRC) %.mllib $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES) $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEPBOOT) -slash -I kernel -I tools/coqdoc -c "$<" $(TOTARGET) + $(HIDE)$(COQDEPBOOT) -I kernel -I tools/coqdoc -c "$<" $(TOTARGET) %.v.d: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENVFILES) $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEPBOOT) $(DEPNATDYN) -slash "$<" $(TOTARGET) + $(HIDE)$(COQDEPBOOT) $(DEPNATDYN) "$<" $(TOTARGET) %_stubs.c.d: $(D_DEPEND_BEFORE_SRC) %_stubs.c $(D_DEPEND_AFTER_SRC) $(SHOW)'CCDEP $<' @@ -982,11 +1098,20 @@ checker/%.mllib.d: $(D_DEPEND_BEFORE_SRC) checker/%.mllib $(D_DEPEND_AFTER_SRC) # this sets up developper supporting stuff ########################################################################### -.PHONY: devel +.PHONY: devel otags devel: $(DEBUGPRINTERS) +otags: + otags $(MLIFILES) $(MLSTATICFILES) \ + $(foreach i,$(ML4FILES),-pc -pa tools/compat5.cmo -pa op -pa g -pa m -pa rq $(patsubst %,-pa %,$(call CAMLP4DEPS,$i)) -impl $i) + + ########################################################################### +# To speed-up things a bit, let's dissuade make to attempt rebuilding makefiles + +Makefile Makefile.build Makefile.common config/Makefile : ; + # For emacs: # Local Variables: -- cgit v1.2.3