diff options
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 656 |
1 files changed, 348 insertions, 308 deletions
diff --git a/Makefile.build b/Makefile.build index 717fcf20..59ee457c 100644 --- a/Makefile.build +++ b/Makefile.build @@ -1,4 +1,4 @@ -###################################################################### +####################################################################### # v # The Coq Proof Assistant / The Coq Development Team # # <O___,, # INRIA-Rocquencourt & LRI-CNRS-Orsay # # \VV/ ############################################################# @@ -6,59 +6,79 @@ # # GNU Lesser General Public License Version 2.1 # ####################################################################### -# $Id: Makefile.build 14090 2011-05-03 13:34:16Z pboutill $ - +# This makefile is normally called by the main Makefile after setting +# some variables. -# Makefile for Coq -# -# To be used with GNU Make. -# -# This is the only Makefile. You won't find Makefiles in sub-directories -# and this is done on purpose. If you are not yet convinced of the advantages -# of a single Makefile, please read -# http://www.pcug.org.au/~millerp/rmch/recu-make-cons-harm.html -# before complaining. -# -# When you are working in a subdir, you can compile without moving to the -# upper directory using "make -C ..", and the output is still understood -# by Emacs' next-error. ########################################################################### - -include Makefile.common -ifndef COQ_CONFIGURED - $(error Please run ./configure first) -endif - -.PHONY: NOARG - -NOARG: world +# Starting rule +########################################################################### # build and install the three subsystems: coq, coqide world: revision coq coqide install: install-coq install-coqide +.PHONY: world install + +########################################################################### +# Includes +########################################################################### + +include Makefile.common +include Makefile.doc + ifeq ($(WITHDOC),all) world: doc install: install-doc endif -#install-manpages: install-coq-manpages +# 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. + +ALLDEPS=$(addsuffix .d, \ + $(ML4FILES) $(MLFILES) $(MLIFILES) $(CFILES) $(MLLIBFILES) $(VFILES)) + +.SECONDARY: $(ALLDEPS) $(GENFILES) $(GENML4FILES) + +# 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) + ########################################################################### # Compilation options ########################################################################### +# Variables meant to be modifiable via the command-line of make + +VERBOSE= +NO_RECOMPILE_ML4= +NO_RECOMPILE_LIB= +NO_RECALC_DEPS= +READABLE_ML4= # 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)" + +COQOPTS=$(COQ_XML) $(VM) +BOOTCOQTOP:=$(TIMECMD) $(BESTCOQTOP) -boot $(COQOPTS) +BOOTCOQC:=$(BOOTCOQTOP) -compile + # The SHOW and HIDE variables control whether make will echo complete commands # or only abbreviated versions. # Quiet mode is ON by default except if VERBOSE=1 option is given to make -ifdef VERBOSE - SHOW = @true "" - HIDE = -else - SHOW = @echo "" - HIDE = @ -endif +SHOW := $(if $(VERBOSE),@true "",@echo "") +HIDE := $(if $(VERBOSE),,@) LOCALINCLUDES=$(addprefix -I , $(SRCDIRS) ) MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) @@ -70,21 +90,30 @@ BYTEFLAGS=$(MLINCLUDES) $(CAMLDEBUG) $(USERFLAGS) OPTFLAGS=$(MLINCLUDES) $(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS) DEPFLAGS= -slash $(LOCALINCLUDES) -CAMLP4EXTENDFLAGS=-I $(CAMLLIB) -I . #grammar dependencies are now in camlp4use statements -CAMLP4DEPS=sed -n -e 's@^(\*.*camlp4deps: "\(.*\)".*\*)@\1@p' -CAMLP4USE=sed -n -e 's/pa_macro.cmo/pa_macro.cmo -D$(CAMLVERSION)/' -e 's@^(\*.*camlp4use: "\(.*\)".*\*)@\1@p' +define bestocaml +$(if $(OPT),\ +$(OCAMLOPT) $(OPTFLAGS) -o $@ $(1) $(addsuffix .cmxa,$(2)) $^ && $(STRIP) $@,\ +$(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ $(1) $(addsuffix .cma,$(2)) $^) +endef -COQ_XML= # is "-xml" when building XML library -VM= # is "-no-vm" to not use the vm" -UNBOXEDVALUES= # is "-unboxed-values" to use unboxed values -COQOPTS=$(COQ_XML) $(VM) $(UNBOXEDVALUES) -TIMECMD= # is "'time -p'" to get compilation time of .v +CAMLP4DEPS=`sed -n -e 's@^(\*.*camlp4deps: "\(.*\)".*@\1@p' $<` +ifeq ($(CAMLP4),camlp5) +CAMLP4USE=pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION) +else +CAMLP4USE=-D$(CAMLVERSION) +endif -# 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)" +PR_O := $(if $(READABLE_ML4),pr_o.cmo,pr_dump.cmo) # works also with new camlp4 + +ifeq ($(CAMLP4),camlp5) +SYSMOD:=str unix gramlib +else +SYSMOD:=str unix dynlink camlp4lib +endif + +SYSCMA:=$(addsuffix .cma,$(SYSMOD)) +SYSCMXA:=$(addsuffix .cmxa,$(SYSMOD)) -BOOTCOQTOP:=$(TIMECMD) $(BESTCOQTOP) -boot $(COQOPTS) ########################################################################### # Infrastructure for the rest of the Makefile @@ -125,6 +154,13 @@ else D_DEPEND_AFTER_SRC:=| endif +## When a rule redirects stdout of a command to the target file : cmd > $@ +## then the target file will be created even if cmd has failed. +## Hence relaunching make will go further, as make thinks the target has been +## done ok. To avoid this, we use the following macro: + +TOTARGET = > "$@" || (RV=$$?; rm -f "$@"; exit $${RV}) + ########################################################################### # Compilation option for .c files ########################################################################### @@ -141,22 +177,19 @@ $(LIBCOQRUN): kernel/byterun/coq_jumptbl.h $(BYTERUN) #coq_jumptbl.h is required only if you have GCC 2.0 or later kernel/byterun/coq_jumptbl.h : kernel/byterun/coq_instruct.h sed -n -e '/^ /s/ \([A-Z]\)/ \&\&coq_lbl_\1/gp' \ - -e '/^}/q' kernel/byterun/coq_instruct.h > \ - kernel/byterun/coq_jumptbl.h \ - || ( RV=$$?; rm -f "$@"; exit $${RV} ) + -e '/^}/q' $< $(TOTARGET) kernel/copcodes.ml: kernel/byterun/coq_instruct.h - sed -n -e '/^enum/p' -e 's/,//g' -e '/^ /p' \ - kernel/byterun/coq_instruct.h | \ - awk -f kernel/make-opcodes > kernel/copcodes.ml \ - || ( RV=$$?; rm -f "$@"; exit $${RV} ) - + sed -n -e '/^enum/p' -e 's/,//g' -e '/^ /p' $< | \ + awk -f kernel/make-opcodes $(TOTARGET) ########################################################################### # Main targets (coqmktop, coqtop.opt, coqtop.byte) ########################################################################### -coqbinaries:: ${COQBINARIES} ${CSDPCERT} +.PHONY: coqbinaries coq coqlib coqlight states + +coqbinaries:: ${COQBINARIES} ${CSDPCERT} ${FAKEIDE} coq: coqlib tools coqbinaries @@ -166,14 +199,14 @@ coqlight: theories-light tools coqbinaries states:: states/initial.coq -$(COQTOPOPT): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) +$(COQTOPOPT): $(BESTCOQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(COQMKTOP) -boot -opt $(OPTFLAGS) -o $@ + $(HIDE)$(BESTCOQMKTOP) -boot -opt $(OPTFLAGS) -o $@ $(STRIP) $@ -$(COQTOPBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) +$(COQTOPBYTE): $(BESTCOQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(COQMKTOP) -boot -top $(BYTEFLAGS) -o $@ + $(HIDE)$(BESTCOQMKTOP) -boot -top $(BYTEFLAGS) -o $@ $(COQTOPEXE): $(ORDER_ONLY_SEP) $(BESTCOQTOP) cd bin; ln -sf coqtop.$(BEST)$(EXE) coqtop$(EXE) @@ -185,12 +218,12 @@ CHKOPTFLAGS:=$(CHKLIBS) $(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS) $(CHICKENOPT): checker/check.cmxa checker/main.ml $(SHOW)'OCAMLOPT -o $@' - $(HIDE)$(OCAMLOPT) $(CHKOPTFLAGS) -o $@ str.cmxa unix.cmxa gramlib.cmxa $^ + $(HIDE)$(OCAMLOPT) $(CHKOPTFLAGS) -o $@ $(SYSCMXA) $^ $(STRIP) $@ $(CHICKENBYTE): checker/check.cma checker/main.ml $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(CHKBYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ str.cma unix.cma gramlib.cma $^ + $(HIDE)$(OCAMLC) $(CHKBYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ $(SYSCMA) $^ $(CHICKEN): $(ORDER_ONLY_SEP) $(BESTCHICKEN) cd bin && ln -sf coqchk.$(BEST)$(EXE) coqchk$(EXE) @@ -199,13 +232,11 @@ $(CHICKEN): $(ORDER_ONLY_SEP) $(BESTCHICKEN) $(COQMKTOPBYTE): $(COQMKTOPCMO) $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma unix.cma gramlib.cma\ - $^ $(OSDEPLIBS) + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ $(SYSCMA) $^ $(OSDEPLIBS) -$(COQMKTOPOPT): $(COQMKTOPCMX) +$(COQMKTOPOPT): $(COQMKTOPCMO:.cmo=.cmx) $(SHOW)'OCAMLOPT -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ str.cmxa unix.cmxa gramlib.cmxa\ - $^ $(OSDEPLIBS) + $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ $(SYSCMXA) $^ $(OSDEPLIBS) $(STRIP) $@ $(COQMKTOP): $(ORDER_ONLY_SEP) $(BESTCOQMKTOP) @@ -216,20 +247,19 @@ scripts/tolink.ml: Makefile.build Makefile.common $(HIDE)echo "let copts = \"-cclib -lcoqrun\"" > $@ $(HIDE)echo "let core_libs = \""$(LINKCMO)"\"" >> $@ $(HIDE)echo "let core_objs = \""$(OBJSMOD)"\"" >> $@ - $(HIDE)echo "let ide = \""$(IDEMOD)"\"" >> $@ # coqc -$(COQCBYTE): $(COQCCMO) $(COQTOPBYTE) $(BESTCOQTOP) +$(COQCBYTE): $(COQCCMO) | $(COQTOPBYTE) $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma unix.cma gramlib.cma $(COQCCMO) $(OSDEPLIBS) + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ $(SYSCMA) $^ $(OSDEPLIBS) -$(COQCOPT): $(COQCCMX) $(COQTOPOPT) $(BESTCOQTOP) +$(COQCOPT): $(COQCCMO:.cmo=.cmx) | $(COQTOPOPT) $(SHOW)'OCAMLOPT -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ str.cmxa unix.cmxa gramlib.cmxa $(COQCCMX) $(OSDEPLIBS) + $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ $(SYSCMXA) $^ $(OSDEPLIBS) $(STRIP) $@ -$(COQC): $(ORDER_ONLY_SEP) $(BESTCOQC) +$(COQC): $(ORDER_ONLY_SEP) $(BESTCOQC) cd bin; ln -sf coqc.$(BEST)$(EXE) coqc$(EXE) # target for libraries @@ -256,21 +286,16 @@ checker/check.cmxa: | checker/check.mllib.d # Csdp to micromega special targets ########################################################################### -ifeq ($(BEST),opt) -plugins/micromega/csdpcert$(EXE): $(CSDPCERTCMX) - $(SHOW)'OCAMLOPT -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) nums.cmxa unix.cmxa -o $@ $^ - $(STRIP) $@ -else -plugins/micromega/csdpcert$(EXE): $(CSDPCERTCMO) - $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) nums.cma unix.cma -o $@ $^ -endif +plugins/micromega/csdpcert$(EXE): $(CSDPCERTCMO:.cmo=$(BESTOBJ)) + $(SHOW)'OCAMLBEST -o $@' + $(HIDE)$(call bestocaml,,nums unix) ########################################################################### # CoqIde special targets ########################################################################### +.PHONY: coqide coqide-binaries coqide-no coqide-byte coqide-opt coqide-files + # target to build CoqIde coqide:: coqide-files coqide-binaries states @@ -278,7 +303,7 @@ COQIDEFLAGS=-thread $(COQIDEINCLUDES) .SUFFIXES:.vo -IDEFILES=ide/coq.png ide/.coqide-gtk2rc +IDEFILES=ide/coq.png ide/coqide-gtk2rc ide/mac_default_accel_map coqide-binaries: coqide-$(HASCOQIDE) coqide-no: @@ -286,75 +311,75 @@ coqide-byte: $(COQIDEBYTE) $(COQIDE) coqide-opt: $(COQIDEBYTE) $(COQIDEOPT) $(COQIDE) coqide-files: $(IDEFILES) -$(COQIDEOPT): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) ide/ide.cmxa - $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(COQMKTOP) -boot -ide -opt $(OPTFLAGS) -o $@ +$(COQIDEOPT): $(LINKIDEOPT) | $(COQTOPOPT) + $(SHOW)'OCAMLOPT -o $@' + $(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) $(IDEOPTFLAGS) -o $@ unix.cmxa threads.cmxa lablgtk.cmxa\ + gtkThread.cmx str.cmxa $(LINKIDEOPT) $(STRIP) $@ -$(COQIDEBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) ide/ide.cma - $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(COQMKTOP) -boot -g -ide -top $(BYTEFLAGS) -o $@ +$(COQIDEBYTE): $(LINKIDE) | $(COQTOPBYTE) + $(SHOW)'OCAMLOPT -o $@' + $(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ unix.cma threads.cma lablgtk.cma gtkThread.cmo\ + str.cma $(COQRUNBYTEFLAGS) $(LINKIDE) $(COQIDE): cd bin; ln -sf coqide.$(HASCOQIDE)$(EXE) coqide$(EXE) -ide/%.cmo: ide/%.ml | ide/%.ml.d - $(SHOW)'OCAMLC $<' - $(HIDE)$(OCAMLC) -g $(COQIDEFLAGS) $(BYTEFLAGS) -c $< - -ide/%.cmi: ide/%.mli | ide/%.mli.d - $(SHOW)'OCAMLC $<' - $(HIDE)$(OCAMLC) -g $(COQIDEFLAGS) $(BYTEFLAGS) -c $< - -ide/%.cmx: ide/%.ml | ide/%.ml.d - $(SHOW)'OCAMLOPT $<' - $(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -c $< - # install targets -FULLIDELIB=$(FULLCOQLIB)/ide +.PHONY: install-coqide install-ide-no install-ide-byte install-ide-opt +.PHONY: install-ide-files install-ide-info install-im install-coqide:: install-ide-$(HASCOQIDE) install-ide-files install-ide-info install-ide-no: -install-ide-byte: +install-ide-byte: $(MKDIR) $(FULLBINDIR) $(INSTALLBIN) $(COQIDEBYTE) $(FULLBINDIR) $(INSTALLSH) $(FULLCOQLIB) $(IDECMA) \ - `cat $(IDECMA:.cma=.mllib.d) | tr ' ' '\n' | sed -n -e "/\.cmo/s/\.cmo/\.cmi/p"` + $(foreach lib,$(IDECMA:.cma=_MLLIB_DEPENDENCIES),$(addsuffix .cmi,$($(lib)))) cd $(FULLBINDIR); ln -sf coqide.byte$(EXE) coqide$(EXE) install-ide-opt: $(MKDIR) $(FULLBINDIR) - $(INSTALLBIN) $(COQIDEBYTE) $(COQIDEOPT) $(FULLBINDIR) + $(INSTALLBIN) $(COQIDEOPT) $(FULLBINDIR) $(INSTALLSH) $(FULLCOQLIB) $(IDECMA) $(IDECMA:.cma=.cmxa) $(IDECMA:.cma=.a) \ - `cat $(IDECMA:.cma=.mllib.d) | tr ' ' '\n' | sed -n -e "/\.cmo/s/\.cmo/\.cmi/p"` + $(foreach lib,$(IDECMA:.cma=_MLLIB_DEPENDENCIES),$(addsuffix .cmi,$($(lib)))) cd $(FULLBINDIR); ln -sf coqide.opt$(EXE) coqide$(EXE) install-ide-files: - $(MKDIR) $(FULLIDELIB) - $(INSTALLLIB) $(IDEFILES) $(FULLIDELIB) + $(MKDIR) $(FULLDATADIR) + $(INSTALLLIB) ide/coq.png $(FULLDATADIR) + $(MKDIR) $(FULLCONFIGDIR) + $(INSTALLLIB) ide/coqide-gtk2rc $(FULLCONFIGDIR) + if [ $(IDEOPTINT) = QUARTZ ] ; then $(INSTALLLIB) ide/mac_default_accel_map $(FULLCONFIGDIR)/coqide.keys ; fi install-ide-info: - $(MKDIR) $(FULLIDELIB) - $(INSTALLLIB) ide/FAQ $(FULLIDELIB) + $(MKDIR) $(FULLDOCDIR) + $(INSTALLLIB) ide/FAQ $(FULLDOCDIR)/FAQ-CoqIde ########################################################################### # tests ########################################################################### +.PHONY: validate check test-suite $(ALLSTDLIB).v + VALIDOPTS=-silent -o -m validate:: $(BESTCHICKEN) $(ALLVO) $(SHOW)'COQCHK <theories & plugins>' $(HIDE)$(BESTCHICKEN) -boot $(VALIDOPTS) $(ALLMODS) +$(ALLSTDLIB).v: + $(SHOW)'MAKE $(notdir $@)' + $(HIDE)echo "Require $(ALLMODS)." > $@ + MAKE_TSOPTS=-C test-suite -s BEST=$(BEST) VERBOSE=$(VERBOSE) check:: validate test-suite -test-suite: world +test-suite: world $(ALLSTDLIB).v $(MAKE) $(MAKE_TSOPTS) clean $(MAKE) $(MAKE_TSOPTS) all $(HIDE)if grep -F 'Error!' test-suite/summary.log ; then false; fi @@ -363,6 +388,9 @@ test-suite: world # partial targets: 1) core ML parts ################################################################## +.PHONY: lib kernel byterun library proofs tactics interp parsing pretyping +.PHONY: highparsing toplevel hightactics + lib: lib/lib.cma kernel: kernel/kernel.cma byterun: $(BYTERUN) @@ -380,6 +408,10 @@ hightactics: tactics/hightactics.cma # 2) theories and plugins files ########################################################################### +.PHONY: init theories theories-light +.PHONY: logic arith bool narith zarith qarith lists strings sets +.PHONY: fsets relations wellfounded reals setoids sorting numbers noreal + init: $(INITVO) theories: $(THEORIESVO) @@ -401,6 +433,11 @@ reals: $(REALSVO) setoids: $(SETOIDSVO) sorting: $(SORTINGVO) numbers: $(NUMBERSVO) +unicode: $(UNICODEVO) +classes: $(CLASSESVO) +program: $(PROGRAMVO) +structures: $(STRUCTURESVO) +vectors: $(VECTORSVO) noreal: logic arith bool zarith qarith lists sets fsets relations \ wellfounded setoids sorting @@ -409,6 +446,9 @@ noreal: logic arith bool zarith qarith lists sets fsets relations \ # 3) plugins ########################################################################### +.PHONY: plugins omega micromega ring setoid_ring nsatz dp xml extraction +.PHONY: field fourier funind cc subtac rtauto pluginsopt + plugins: $(PLUGINSVO) omega: $(OMEGAVO) $(OMEGACMA) $(ROMEGAVO) $(ROMEGACMA) micromega: $(MICROMEGAVO) $(MICROMEGACMA) $(CSDPCERT) @@ -425,6 +465,8 @@ cc: $(CCVO) $(CCCMA) subtac: $(SUBTACCMA) rtauto: $(RTAUTOVO) $(RTAUTOCMA) +pluginsopt: $(PLUGINSOPT) + ########################################################################### # rules to make theories, plugins and states ########################################################################### @@ -436,97 +478,81 @@ states/initial.coq: states/MakeInitial.v $(INITVO) $(VO_TOOLS_STRICT) | states/M theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_STRICT) | theories/Init/%.v.d $(VO_TOOLS_ORDER_ONLY) $(SHOW)'COQC -nois $<' $(HIDE)rm -f theories/Init/$*.glob - $(HIDE)$(BOOTCOQTOP) -nois -compile theories/Init/$* + $(HIDE)$(BOOTCOQC) theories/Init/$* -nois theories/Numbers/Natural/BigN/NMake_gen.v: theories/Numbers/Natural/BigN/NMake_gen.ml - $(OCAML) $< > $@ + $(OCAML) $< $(TOTARGET) ########################################################################### # tools ########################################################################### +.PHONY: printers tools + printers: $(DEBUGPRINTERS) tools:: $(TOOLS) $(DEBUGPRINTERS) $(COQDEPBOOT) -# coqdep_boot : a basic version of coqdep, with almost no dependencies +# coqdep_boot : a basic version of coqdep, with almost no dependencies. -$(COQDEPBOOT): $(COQDEPBOOTML) -ifeq ($(BEST),opt) - $(SHOW)'OCAMLOPT -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ -I tools unix.cmxa $^ - $(STRIP) $@ -else - $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ -I tools unix.cma $^ -endif +# Here it is important to mention .ml files instead of .cmo in order +# to avoid using implicit rules and hence .ml.d files that would need +# coqdep_boot. + +COQDEPBOOTSRC:= \ + tools/coqdep_lexer.mli tools/coqdep_lexer.ml \ + tools/coqdep_common.mli tools/coqdep_common.ml \ + tools/coqdep_boot.ml + +$(COQDEPBOOT): $(COQDEPBOOTSRC) + $(SHOW)'OCAMLBEST -o $@' + $(HIDE)$(call bestocaml, -I tools, unix) # the full coqdep -ifeq ($(BEST),opt) -$(COQDEP): $(COQDEPCMX) - $(SHOW)'OCAMLOPT -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ str.cmxa unix.cmxa gramlib.cmxa $^ $(OSDEPLIBS) - $(STRIP) $@ -else -$(COQDEP): $(COQDEPCMO) - $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ str.cma unix.cma gramlib.cma $^ $(OSDEPLIBS) -endif +$(COQDEP): $(COQDEPCMO:.cmo=$(BESTOBJ)) + $(SHOW)'OCAMLBEST -o $@' + $(HIDE)$(call bestocaml, $(OSDEPLIBS), $(SYSMOD)) -ifeq ($(BEST),opt) -$(GALLINA): $(GALLINACMX) - $(SHOW)'OCAMLOPT -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ $(GALLINACMX) - $(STRIP) $@ -else -$(GALLINA): $(GALLINACMO) - $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ $^ -endif +$(GALLINA): $(addsuffix $(BESTOBJ), tools/gallina_lexer tools/gallina) + $(SHOW)'OCAMLBEST -o $@' + $(HIDE)$(call bestocaml,,) -ifeq ($(BEST),opt) -$(COQMAKEFILE): tools/coq_makefile.cmx config/coq_config.cmx - $(SHOW)'OCAMLOPT -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ str.cmxa config/coq_config.cmx tools/coq_makefile.cmx - $(STRIP) $@ -else -$(COQMAKEFILE): config/coq_config.cmo tools/coq_makefile.cmo - $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ str.cma $^ -endif +$(COQMAKEFILE): $(addsuffix $(BESTOBJ),config/coq_config ide/minilib ide/project_file tools/coq_makefile) + $(SHOW)'OCAMLBEST -o $@' + $(HIDE)$(call bestocaml,,str unix) -ifeq ($(BEST),opt) -$(COQTEX): tools/coq_tex.cmx - $(SHOW)'OCAMLOPT -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ str.cmxa $^ - $(STRIP) $@ -else -$(COQTEX): tools/coq_tex.cmo - $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ str.cma $^ -endif +$(COQTEX): tools/coq_tex$(BESTOBJ) + $(SHOW)'OCAMLBEST -o $@' + $(HIDE)$(call bestocaml,,str) -ifeq ($(BEST),opt) -$(COQWC): tools/coqwc.cmx - $(SHOW)'OCAMLOPT -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ tools/coqwc.cmx - $(STRIP) $@ -else -$(COQWC): tools/coqwc.cmo - $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ $^ -endif +$(COQWC): tools/coqwc$(BESTOBJ) + $(SHOW)'OCAMLBEST -o $@' + $(HIDE)$(call bestocaml,,) -ifeq ($(BEST),opt) -$(COQDOC): $(COQDOCCMX) - $(SHOW)'OCAMLOPT -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ str.cmxa unix.cmxa $(COQDOCCMX) - $(STRIP) $@ +$(COQDOC): $(COQDOCCMO:.cmo=$(BESTOBJ)) + $(SHOW)'OCAMLBEST -o $@' + $(HIDE)$(call bestocaml,,str unix) + +# 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) + $(SHOW)'OCAMLBEST -o $@' + $(HIDE)$(call bestocaml,,unix) + +# 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 $< +tools/compat5b.cmo: tools/compat5b.mlp + $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp "$(CAMLP4O) -impl" -impl $< else -$(COQDOC): $(COQDOCCMO) - $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ str.cma unix.cma $^ +tools/compat5.cmo: tools/compat5.ml + $(OCAMLC) -c $< +tools/compat5b.cmo: tools/compat5b.ml + $(OCAMLC) -c $< endif ########################################################################### @@ -543,6 +569,8 @@ endif ifdef COQINSTALLPREFIX FULLBINDIR=$(BINDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) FULLCOQLIB=$(COQLIBINSTALL:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) +FULLCONFIGDIR=$(CONFIGDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) +FULLDATADIR=$(DATADIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) FULLMANDIR=$(MANDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) FULLEMACSLIB=$(EMACSLIB:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) FULLCOQDOCDIR=$(COQDOCDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) @@ -550,12 +578,18 @@ FULLDOCDIR=$(DOCDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) else FULLBINDIR=$(BINDIR) FULLCOQLIB=$(COQLIBINSTALL) +FULLCONFIGDIR=$(CONFIGDIR) +FULLDATADIR=$(DATADIR) FULLMANDIR=$(MANDIR) FULLEMACSLIB=$(EMACSLIB) FULLCOQDOCDIR=$(COQDOCDIR) FULLDOCDIR=$(DOCDIR) endif +.PHONY: install-coq install-coqlight install-binaries install-byte install-opt +.PHONY: install-tools install-library install-library-light +.PHONY: install-coq-info install-coq-manpages install-emacs install-latex + install-coq: install-binaries install-library install-coq-info install-coqlight: install-binaries install-library-light @@ -579,6 +613,14 @@ install-tools:: $(INSTALLLIB) tools/coqdoc/coqdoc.css tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc $(INSTALLBIN) $(TOOLS) $(FULLBINDIR) +# The list of .cmi to install, including the ones obtained +# 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-library: $(MKDIR) $(FULLCOQLIB) $(INSTALLSH) $(FULLCOQLIB) $(LIBFILES) $(PLUGINS) $(PLUGINSOPT) @@ -587,9 +629,7 @@ install-library: $(MKDIR) $(FULLCOQLIB)/user-contrib $(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB) $(INSTALLSH) $(FULLCOQLIB) $(CONFIG) $(LINKCMO) $(GRAMMARCMA) - # reconstitute the list of core .cmi - $(INSTALLSH) $(FULLCOQLIB) $(CONFIG:.cmo=.cmi) \ - `cat $(CORECMA:.cma=.mllib.d) $(PLUGINSCMA:.cma=.mllib.d) | tr ' ' '\n' | sed -n -e "/\.cmo/s/\.cmo/\.cmi/p"` + $(INSTALLSH) $(FULLCOQLIB) $(INSTALLCMI) ifeq ($(BEST),opt) $(INSTALLLIB) $(LIBCOQRUN) $(FULLCOQLIB) $(INSTALLSH) $(FULLCOQLIB) $(CONFIG:.cmo=.cmx) $(CONFIG:.cmo=.o) $(LINKCMO:.cma=.cmxa) $(LINKCMO:.cma=.a) @@ -598,6 +638,7 @@ endif # it with libraries -$(MKDIR) $(FULLCOQLIB)/plugins/micromega $(INSTALLBIN) $(CSDPCERT) $(FULLCOQLIB)/plugins/micromega + rm -f $(FULLCOQLIB)/revision -$(INSTALLLIB) revision $(FULLCOQLIB) install-library-light: @@ -605,6 +646,7 @@ install-library-light: $(INSTALLSH) $(FULLCOQLIB) $(LIBFILESLIGHT) $(INITPLUGINS) $(INITPLUGINSOPT) $(MKDIR) $(FULLCOQLIB)/states $(INSTALLLIB) states/*.coq $(FULLCOQLIB)/states + rm -f $(FULLCOQLIB)/revision -$(INSTALLLIB) revision $(FULLCOQLIB) install-coq-info: install-coq-manpages install-emacs install-latex @@ -629,12 +671,47 @@ install-latex: # Documentation of the source code (using ocamldoc) ########################################################################### -.PHONY: source-doc +.PHONY: source-doc mli-doc ml-doc + +source-doc: mli-doc $(OCAMLDOCDIR)/coq.pdf -source-doc: - if !(test -d $(SOURCEDOCDIR)); then mkdir $(SOURCEDOCDIR); fi - $(OCAMLDOC) -html -rectypes $(LOCALINCLUDES) -d $(SOURCEDOCDIR) $(MLFILES) +$(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)\ + $(DOCMLIS) -d $(OCAMLDOCDIR)/html -colorize-code \ + -t "Coq mlis documentation" -intro $(OCAMLDOCDIR)/docintro \ + -css-style style.css + +%_dep.png: %.dot + $(DOT) -Tpng $< -o $@ + +%_types.dot: %.mli + $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -dot-types -o $@ $< + +OCAMLDOC_MLLIBD = $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ \ + $(foreach lib,$(|:.mllib.d=_MLLIB_DEPENDENCIES),$(addsuffix .ml,$($(lib)))) + +%.dot: | %.mllib.d + $(OCAMLDOC_MLLIBD) + +ml-doc: + $(OCAMLDOC) -html -rectypes $(LOCALINCLUDES) -d $(SOURCEDOCDIR) $(MLSTATICFILES) + +parsing/parsing.dot : | parsing/parsing.mllib.d parsing/highparsing.mllib.d + $(OCAMLDOC_MLLIBD) + +tactics/tactics.dot: | tactics/tactics.mllib.d tactics/hightactics.mllib.d + $(OCAMLDOC_MLLIBD) + +%.dot: %.mli + $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $< + +$(OCAMLDOCDIR)/%.pdf: $(OCAMLDOCDIR)/%.tex + (cd $(OCAMLDOCDIR) ; pdflatex $*.tex && pdflatex $*.tex) ########################################################################### ### Special rules @@ -642,7 +719,7 @@ source-doc: dev/printers.cma: | dev/printers.mllib.d $(SHOW)'Testing $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) unix.cma gramlib.cma $^ -o test-printer + $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(SYSCMA) $^ -o test-printer @rm -f test-printer $(SHOW)'OCAMLC -a $@' $(HIDE)$(OCAMLC) $(BYTEFLAGS) $^ -linkall -a -o $@ @@ -650,35 +727,38 @@ dev/printers.cma: | dev/printers.mllib.d parsing/grammar.cma: | parsing/grammar.mllib.d $(SHOW)'Testing $@' @touch test.ml4 - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) $^ -impl" -impl test.ml4 -o test-grammar + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) -I $(CAMLLIB) $^ -impl" -impl test.ml4 -o test-grammar @rm -f test-grammar test.* $(SHOW)'OCAMLC -a $@' $(HIDE)$(OCAMLC) $(BYTEFLAGS) $^ -linkall -a -o $@ # toplevel/mltop.ml4 (ifdef Byte) -toplevel/mltop.cmo: toplevel/mltop.byteml | toplevel/mltop.ml4.ml.d toplevel/mltop.ml4.d - $(SHOW)'OCAMLC $<' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -c -impl $< -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.ml4.ml.d toplevel/mltop.ml4.d - $(SHOW)'OCAMLOPT $<' +toplevel/mltop.cmx: toplevel/mltop.optml | toplevel/mltop.ml.d toplevel/mltop.ml4.d + $(SHOW)'OCAMLOPT $<' $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -c -impl $< -o $@ -## This works dependency-wise because the dependencies of the -## .{opt,byte}ml files are those we deduce from the .ml4 file. -## In other words, the Byte-only code doesn't import a new module. -toplevel/mltop.byteml: toplevel/mltop.ml4 config/Makefile # no camlp4deps here - $(SHOW)'CAMLP4O $<' - $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo `$(CAMLP4USE) $<` \ - -DByte -DHasDynlink -impl $< > $@ \ - || ( RV=$$?; rm -f "$@"; exit $${RV} ) +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 + $(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 $@ -toplevel/mltop.optml: toplevel/mltop.ml4 config/Makefile # no camlp4deps here - $(SHOW)'CAMLP4O $<' - $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo `$(CAMLP4USE) $<` \ - $(NATDYNLINKDEF) -impl $< > $@ \ - || ( RV=$$?; rm -f "$@"; exit $${RV} ) # pretty printing of the revision number when compiling a checked out # source tree @@ -731,52 +811,46 @@ endif # Default rules ########################################################################### -checker/%.cmo: checker/%.ml | checker/%.ml.d - $(SHOW)'OCAMLC $<' - $(HIDE)$(OCAMLC) -c $(CHKBYTEFLAGS) $< +## Three flavor of flags: checker/* ide/* and normal files -checker/%.cmx: checker/%.ml | checker/%.ml.d - $(SHOW)'OCAMLOPT $<' - $(HIDE)$(OCAMLOPT) -c $(CHKOPTFLAGS) $< +COND_BYTEFLAGS= \ + $(if $(filter checker/%,$<), $(CHKBYTEFLAGS), \ + $(if $(filter ide/%,$<),$(COQIDEFLAGS),) $(BYTEFLAGS)) -checker/%.cmi: checker/%.mli | checker/%.mli.d - $(SHOW)'OCAMLC $<' - $(HIDE)$(OCAMLC) -c $(CHKBYTEFLAGS) $< +COND_OPTFLAGS= \ + $(if $(filter checker/%,$<), $(CHKOPTFLAGS), \ + $(if $(filter ide/%,$<),$(COQIDEFLAGS),) $(OPTFLAGS)) %.o: %.c $(SHOW)'OCAMLC $<' $(HIDE)cd $(dir $<) && $(OCAMLC) -ccopt "$(CFLAGS)" -c $(notdir $<) -ifdef KEEP_ML4_PREPROCESSED -.PRECIOUS: %.ml4-preprocessed -%.cmo: %.ml4-preprocessed | %.ml4.ml.d +%.cmi: %.mli | %.mli.d $(SHOW)'OCAMLC $<' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -c -impl $< - -%.cmx: %.ml4-preprocessed | %.ml4.ml.d - $(SHOW)'OCAMLOPT $<' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -c -impl $< -else -%.cmo: %.ml4 | %.ml4.ml.d %.ml4.d - $(SHOW)'OCAMLC4 $<' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4USE) $<` `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl" -c -impl $< - -%.cmx: %.ml4 | %.ml4.ml.d %.ml4.d - $(SHOW)'OCAMLOPT4 $<' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4USE) $<` `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl" -c -impl $< -endif + $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -c $< %.cmo: %.ml | %.ml.d $(SHOW)'OCAMLC $<' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -c $< + $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -c $< -%.cmi: %.mli | %.mli.d - $(SHOW)'OCAMLC $<' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -c $< +## NB: for the moment ocamlopt erases and recreates .cmi if there's no .mli around. +## This can lead to nasty things with make -j. To avoid that: +## 1) We make .cmx always depend on .cmi +## 2) This .cmi will be created from the .mli, or trigger the compilation of the +## .cmo if there's no .mli (see rule below about MLWITHOUTMLI) +## 3) We tell ocamlopt to use the .cmi as the interface source file. With this +## hack, everything goes as if there is a .mli, and the .cmi is preserved +## and the .cmx is checked with respect to this .cmi + +HACKMLI = $(if $(wildcard $<i),,-intf-suffix .cmi) + +$(MLWITHOUTMLI:.ml=.cmx): %.cmx: %.cmi # for .ml with .mli this is already the case + +$(MLWITHOUTMLI:.ml=.cmi): %.cmi: %.cmo %.cmx: %.ml | %.ml.d $(SHOW)'OCAMLOPT $<' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -c $< + $(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) -c $< %.cmxs: %.cmxa $(SHOW)'OCAMLOPT -shared -o $@' @@ -803,17 +877,23 @@ plugins/%_mod.ml: plugins/%.mllib $(HIDE)sed -e "s/\([^ ]\{1,\}\)/let _=Mltop.add_known_module\"\1\" /g" $< > $@ $(HIDE)echo "let _=Mltop.add_known_module\"$(notdir $*)\"" >> $@ -.SECONDARY: $(filter plugins/%,$(MLLIBFILES:%.mllib=%_mod.ml)) +# NB: compatibility modules for camlp4: +# - tools/compat5.cmo changes GEXTEND into EXTEND. Safe, always loaded +# - tools/compat5b.cmo changes EXTEND into EXTEND Gram. Interact badly with +# syntax such that VERNAC EXTEND, we only load it for a few files via camlp4deps -%.ml4-preprocessed: %.ml4 | %.ml4.d +%.ml: %.ml4 | %.ml4.d tools/compat5.cmo tools/compat5b.cmo $(SHOW)'CAMLP4O $<' - $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo `$(CAMLP4USE) $<` `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< > $@ \ - || ( RV=$$?; rm -f "$@"; exit $${RV} ) + $(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 %.vo %.glob: %.v states/initial.coq $(INITPLUGINSBEST) $(VO_TOOLS_STRICT) | %.v.d $(VO_TOOLS_ORDER_ONLY) $(SHOW)'COQC $<' $(HIDE)rm -f $*.glob - $(HIDE)$(BOOTCOQTOP) -compile $* + $(HIDE)$(BOOTCOQC) $* ifdef VALIDATE $(SHOW)'COQCHK $(call vo_to_mod,$@)' $(HIDE)$(BESTCHICKEN) -boot -silent -norec $(call vo_to_mod,$@) \ @@ -826,69 +906,51 @@ endif # .ml4.d contains the dependencies to generate the .ml from the .ml4 # NOT to generate object code. -ifdef NO_RECOMPILE_ML4 - SEP:=$(ORDER_ONLY_SEP) -else - SEP:= -endif + %.ml4.d: $(D_DEPEND_BEFORE_SRC) %.ml4 $(SHOW)'CAMLP4DEPS $<' - $(HIDE)( printf "%s" '$*.cmo $*.cmx $*.ml4.ml.d $*.ml4-preprocessed: $(SEP)' && $(CAMLP4DEPS) "$<" ) > "$@" \ - || ( RV=$$?; rm -f "$@"; exit $${RV} ) + $(HIDE)echo "$*.ml: $(if $(NO_RECOMPILE_ML4),$(ORDER_ONLY_SEP)) $(CAMLP4DEPS)" $(TOTARGET) + +# We now use coqdep_boot to wrap around ocamldep -modules, since it is aware +# of .ml4 files -%.ml4.ml.d: $(D_DEPEND_BEFORE_SRC) %.ml4 $(D_DEPEND_AFTER_SRC) $(GENFILES) $(ML4FILESML) %.ml4.d -#Critical section: -# Nobody (in a make -j) should touch the .ml file here. - $(SHOW)'OCAMLDEP4 $<' - $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo `$(CAMLP4USE) $<` `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< -o $*.ml \ - || ( RV=$$?; rm -f "$*.ml"; exit $${RV} ) - $(HIDE)$(OCAMLDEP) $(DEPFLAGS) $*.ml | sed '' > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) - $(HIDE)echo "let keep_ocamldep_happy Do_not_compile_me = assert false" > $*.ml -#End critical section - -checker/%.ml.d: $(D_DEPEND_BEFORE_SRC) checker/%.ml $(D_DEPEND_AFTER_SRC) +OCAMLDEP_NG = $(COQDEPBOOT) -mldep $(OCAMLDEP) + +checker/%.ml.d: $(D_DEPEND_BEFORE_SRC) checker/%.ml $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES) $(SHOW)'OCAMLDEP $<' - $(HIDE)$(OCAMLDEP) -slash $(LOCALCHKLIBS) "$<" | sed '' > "$@" + $(HIDE)$(OCAMLDEP_NG) -slash $(LOCALCHKLIBS) "$<" $(TOTARGET) -checker/%.mli.d: $(D_DEPEND_BEFORE_SRC) checker/%.mli $(D_DEPEND_AFTER_SRC) +checker/%.mli.d: $(D_DEPEND_BEFORE_SRC) checker/%.mli $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES) $(SHOW)'OCAMLDEP $<' - $(HIDE)$(OCAMLDEP) -slash $(LOCALCHKLIBS) "$<" | sed '' > "$@" + $(HIDE)$(OCAMLDEP_NG) -slash $(LOCALCHKLIBS) "$<" $(TOTARGET) -%.ml.d: $(D_DEPEND_BEFORE_SRC) %.ml $(D_DEPEND_AFTER_SRC) $(GENFILES) $(ML4FILESML) +%.ml.d: $(D_DEPEND_BEFORE_SRC) %.ml $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES) $(SHOW)'OCAMLDEP $<' - $(HIDE)$(OCAMLDEP) $(DEPFLAGS) "$<" | sed '' > "$@" + $(HIDE)$(OCAMLDEP_NG) $(DEPFLAGS) "$<" $(TOTARGET) -%.mli.d: $(D_DEPEND_BEFORE_SRC) %.mli $(D_DEPEND_AFTER_SRC) $(GENFILES) $(ML4FILESML) +%.mli.d: $(D_DEPEND_BEFORE_SRC) %.mli $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES) $(SHOW)'OCAMLDEP $<' - $(HIDE)$(OCAMLDEP) $(DEPFLAGS) "$<" | sed '' > "$@" + $(HIDE)$(OCAMLDEP_NG) $(DEPFLAGS) "$<" $(TOTARGET) -checker/%.mllib.d: $(D_DEPEND_BEFORE_SRC) checker/%.mllib $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) +checker/%.mllib.d: $(D_DEPEND_BEFORE_SRC) checker/%.mllib $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES) $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEPBOOT) -slash -boot -I checker -c "$<" > "$@" \ - || ( RV=$$?; rm -f "$@"; exit $${RV} ) + $(HIDE)$(COQDEPBOOT) -slash -I checker -c "$<" $(TOTARGET) -%.mllib.d: $(D_DEPEND_BEFORE_SRC) %.mllib $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) +%.mllib.d: $(D_DEPEND_BEFORE_SRC) %.mllib $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES) $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEPBOOT) -slash -boot -I kernel -I tools/coqdoc -c "$<" > "$@" \ - || ( RV=$$?; rm -f "$@"; exit $${RV} ) - -## Veerry nasty hack to keep ocamldep happy -%.ml: | %.ml4 - $(SHOW)'TOUCH $@' - $(HIDE)echo "let keep_ocamldep_happy Do_not_compile_me = assert false" > $@ \ - || ( RV=$$?; rm -f "$@"; exit $${RV} ) + $(HIDE)$(COQDEPBOOT) -slash -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 -boot "$<" > "$@" \ - || ( RV=$$?; rm -f "$@"; exit $${RV} ) + $(HIDE)$(COQDEPBOOT) $(DEPNATDYN) -slash "$<" $(TOTARGET) + +%_stubs.c.d: $(D_DEPEND_BEFORE_SRC) %_stubs.c $(D_DEPEND_AFTER_SRC) + $(SHOW)'CCDEP $<' + $(HIDE)echo "$@ $(@:.c.d=.o): $(@:.c.d=.c)" > $@ %.c.d: $(D_DEPEND_BEFORE_SRC) %.c $(D_DEPEND_AFTER_SRC) $(GENHFILES) $(SHOW)'CCDEP $<' - $(HIDE)$(CC) -MM -MQ "$@" -MQ "$(<:.c=.o)" $(CFLAGS) -isystem $(CAMLHLIB) $< > $@ \ - || ( RV=$$?; rm -f "$@"; exit $${RV} ) - -.SECONDARY: $(GENFILES) + $(HIDE)$(CC) -MM -MQ "$@" -MQ "$(<:.c=.o)" $(CFLAGS) -isystem $(CAMLHLIB) $< $(TOTARGET) ########################################################################### # this sets up developper supporting stuff @@ -900,28 +962,6 @@ devel: $(DEBUGPRINTERS) ########################################################################### -%.types.dot: %.mli - $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -dot-types -o $@ $< - -%.dep.ps: %.dot - $(DOT) $(DOTOPTS) -o $@ $< - -OCAMLDOC_MLLIBD = $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ \ - `cat $| | tr ' ' '\n' | sed -n -e "/\.cmo/s/\.cmo/\.ml/p"` - -%.dot: | %.mllib.d - $(OCAMLDOC_MLLIBD) - -parsing/parsing.dot : | parsing/parsing.mllib.d parsing/highparsing.mllib.d - $(OCAMLDOC_MLLIBD) - -tactics/tactics.dot: | tactics/tactics.mllib.d tactics/hightactics.mllib.d - $(OCAMLDOC_MLLIBD) - -%.dot: %.mli - $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $< - - # For emacs: # Local Variables: # mode: makefile |