diff options
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 84 |
1 files changed, 45 insertions, 39 deletions
diff --git a/Makefile.build b/Makefile.build index 0f85608f9a..f4319243c5 100644 --- a/Makefile.build +++ b/Makefile.build @@ -94,8 +94,8 @@ HIDE := $(if $(VERBOSE),,@) LOCALINCLUDES=$(addprefix -I , $(SRCDIRS) ) MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) -OCAMLC := $(OCAMLC) $(CAMLFLAGS) -OCAMLOPT := $(OCAMLOPT) $(CAMLFLAGS) +OCAMLC := $(OCAMLFIND) ocamlc $(CAMLFLAGS) +OCAMLOPT := $(OCAMLFIND) opt $(CAMLFLAGS) BYTEFLAGS=-thread $(CAMLDEBUG) $(USERFLAGS) OPTFLAGS=-thread $(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS) @@ -180,7 +180,7 @@ endif TOTARGET = > "$@" || (RV=$$?; rm -f "$@"; exit $${RV}) ########################################################################### -# Compilation option for .c files +# Compilation option for .c files ########################################################################### CINCLUDES= -I $(CAMLHLIB) @@ -190,9 +190,9 @@ CINCLUDES= -I $(CAMLHLIB) # NB: We used to do a ranlib after ocamlmklib, but it seems that # ocamlmklib is already doing it -$(LIBCOQRUN): kernel/byterun/coq_jumptbl.h $(BYTERUN) +$(LIBCOQRUN): kernel/byterun/coq_jumptbl.h $(BYTERUN) cd $(dir $(LIBCOQRUN)) && \ - $(OCAMLMKLIB) -oc $(COQRUN) $(foreach u,$(BYTERUN),$(notdir $(u))) + $(OCAMLFIND) ocamlmklib -oc $(COQRUN) $(foreach u,$(BYTERUN),$(notdir $(u))) #coq_jumptbl.h is required only if you have GCC 2.0 or later kernel/byterun/coq_jumptbl.h : kernel/byterun/coq_instruct.h @@ -503,12 +503,13 @@ test-suite: world $(ALLSTDLIB).v ################################################################## .PHONY: lib kernel byterun library proofs tactics interp parsing pretyping -.PHONY: highparsing stm toplevel hightactics +.PHONY: engine highparsing stm toplevel hightactics lib: lib/clib.cma lib/lib.cma kernel: kernel/kernel.cma byterun: $(BYTERUN) library: library/library.cma +engine: engine/engine.cma proofs: proofs/proofs.cma tactics: tactics/tactics.cma interp: interp/interp.cma @@ -602,7 +603,7 @@ theories/Numbers/Natural/BigN/NMake_gen.v: theories/Numbers/Natural/BigN/NMake_g printers: $(DEBUGPRINTERS) -tools: $(TOOLS) $(DEBUGPRINTERS) $(COQDEPBOOT) +tools: $(TOOLS) $(DEBUGPRINTERS) $(OCAMLLIBDEP) # coqdep_boot : a basic version of coqdep, with almost no dependencies. @@ -610,12 +611,9 @@ tools: $(TOOLS) $(DEBUGPRINTERS) $(COQDEPBOOT) # 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 +OCAMLLIBDEPSRC:= tools/ocamllibdep.ml -$(COQDEPBOOT): $(COQDEPBOOTSRC) +$(OCAMLLIBDEP): $(OCAMLLIBDEPSRC) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml, -I tools, unix) @@ -830,34 +828,40 @@ install-latex: source-doc: mli-doc $(OCAMLDOCDIR)/coq.pdf $(OCAMLDOCDIR)/coq.tex: $(DOCMLIS:.mli=.cmi) - $(OCAMLDOC) -latex -rectypes -I $(MYCAMLP4LIB) $(MLINCLUDES)\ - $(DOCMLIS) -t "Coq mlis documentation" \ - -intro $(OCAMLDOCDIR)/docintro -o $@ + $(SHOW)'OCAMLDOC -latex -o $@' + $(HIDE)$(OCAMLFIND) ocamldoc -latex -rectypes -I $(MYCAMLP4LIB) $(MLINCLUDES)\ + $(DOCMLIS) -noheader -t "Coq mlis documentation" \ + -intro $(OCAMLDOCDIR)/docintro -o $@.tmp + $(SHOW)'OCAMLDOC utf8 fix' + $(HIDE)$(OCAMLDOCDIR)/fix-ocamldoc-utf8 $@.tmp + $(HIDE)cat $(OCAMLDOCDIR)/header.tex $@.tmp > $@ + rm $@.tmp mli-doc: $(DOCMLIS:.mli=.cmi) - $(OCAMLDOC) -html -rectypes -I +threads -I $(MYCAMLP4LIB) $(MLINCLUDES) \ + $(SHOW)'OCAMLDOC -html' + $(HIDE)$(OCAMLFIND) ocamldoc -charset utf-8 -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) \ + $(OCAMLFIND) 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 $@ %_types.dot: %.mli - $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -dot-types -o $@ $< + $(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -dot-types -o $@ $< -OCAMLDOC_MLLIBD = $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ \ +OCAMLDOC_MLLIBD = $(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ \ $(foreach lib,$(|:.mllib.d=_MLLIB_DEPENDENCIES),$(addsuffix .ml,$($(lib)))) %.dot: | %.mllib.d $(OCAMLDOC_MLLIBD) ml-doc: - $(OCAMLDOC) -html -rectypes -I +threads $(MLINCLUDES) $(COQIDEFLAGS) -d $(OCAMLDOCDIR) $(MLSTATICFILES) + $(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads $(MLINCLUDES) $(COQIDEFLAGS) -d $(OCAMLDOCDIR) $(MLSTATICFILES) parsing/parsing.dot : | parsing/parsing.mllib.d parsing/highparsing.mllib.d $(OCAMLDOC_MLLIBD) @@ -869,10 +873,12 @@ tactics/tactics.dot: | tactics/tactics.mllib.d tactics/hightactics.mllib.d $(OCAMLDOC_MLLIBD) %.dot: %.mli - $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $< + $(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $< $(OCAMLDOCDIR)/%.pdf: $(OCAMLDOCDIR)/%.tex - (cd $(OCAMLDOCDIR) ; pdflatex $*.tex && pdflatex $*.tex) + $(SHOW)'PDFLATEX $*.tex' + $(HIDE)(cd $(OCAMLDOCDIR) ; pdflatex -interaction=batchmode $*.tex && pdflatex -interaction=batchmode $*.tex) + $(HIDE)(cd doc/tools/; show_latex_messages -no-overfull ../../$(OCAMLDOCDIR)/$*.log) ########################################################################### ### Special rules @@ -1018,10 +1024,6 @@ endif $(SHOW)'OCAMLLEX $<' $(HIDE)$(OCAMLLEX) -o $@ "$*.mll" -%.ml %.mli: %.mly - $(SHOW)'OCAMLYACC $<' - $(HIDE)$(OCAMLYACC) $< - plugins/%_mod.ml: plugins/%.mllib $(SHOW)'ECHO... > $@' $(HIDE)sed -e "s/\([^ ]\{1,\}\)/let _=Mltop.add_known_module\"\1\" /g" $< > $@ @@ -1061,35 +1063,39 @@ endif # Since OCaml 3.12.1, we could use again ocamldep directly, thanks to # the option -ml-synonym -OCAMLDEP_NG = $(OCAMLDEP) -slash -ml-synonym .ml4 +OCAMLDEP_NG = $(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 -checker/%.ml.d: $(D_DEPEND_BEFORE_SRC) checker/%.ml $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES) +checker/%.ml.d: $(D_DEPEND_BEFORE_SRC) checker/%.ml $(D_DEPEND_AFTER_SRC) $(GENFILES) $(SHOW)'OCAMLDEP $<' $(HIDE)$(OCAMLDEP_NG) $(LOCALCHKLIBS) "$<" $(TOTARGET) -checker/%.mli.d: $(D_DEPEND_BEFORE_SRC) checker/%.mli $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES) +checker/%.mli.d: $(D_DEPEND_BEFORE_SRC) checker/%.mli $(D_DEPEND_AFTER_SRC) $(GENFILES) $(SHOW)'OCAMLDEP $<' $(HIDE)$(OCAMLDEP_NG) $(LOCALCHKLIBS) "$<" $(TOTARGET) -%.ml.d: $(D_DEPEND_BEFORE_SRC) %.ml $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES) +%.ml.d: $(D_DEPEND_BEFORE_SRC) %.ml $(D_DEPEND_AFTER_SRC) $(GENFILES) $(SHOW)'OCAMLDEP $<' $(HIDE)$(OCAMLDEP_NG) $(DEPFLAGS) "$<" $(TOTARGET) -%.mli.d: $(D_DEPEND_BEFORE_SRC) %.mli $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES) +%.mli.d: $(D_DEPEND_BEFORE_SRC) %.mli $(D_DEPEND_AFTER_SRC) $(GENFILES) $(SHOW)'OCAMLDEP $<' $(HIDE)$(OCAMLDEP_NG) $(DEPFLAGS) "$<" $(TOTARGET) -checker/%.mllib.d: $(D_DEPEND_BEFORE_SRC) checker/%.mllib $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES) - $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEPBOOT) -I checker -c "$<" $(TOTARGET) +checker/%.mllib.d: $(D_DEPEND_BEFORE_SRC) checker/%.mllib $(D_DEPEND_AFTER_SRC) $(OCAMLLIBDEP) $(GENFILES) + $(SHOW)'OCAMLLIBDEP $<' + $(HIDE)$(OCAMLLIBDEP) $(LOCALCHKLIBS) "$<" $(TOTARGET) + +dev/%.mllib.d: $(D_DEPEND_BEFORE_SRC) dev/%.mllib $(D_DEPEND_AFTER_SRC) $(OCAMLLIBDEP) $(GENFILES) + $(SHOW)'OCAMLLIBDEP $<' + $(HIDE)$(OCAMLLIBDEP) $(DEPFLAGS) -I dev "$<" $(TOTARGET) -%.mllib.d: $(D_DEPEND_BEFORE_SRC) %.mllib $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES) - $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEPBOOT) -I kernel -I tools/coqdoc -c "$<" $(TOTARGET) +%.mllib.d: $(D_DEPEND_BEFORE_SRC) %.mllib $(D_DEPEND_AFTER_SRC) $(OCAMLLIBDEP) $(GENFILES) + $(SHOW)'OCAMLLIBDEP $<' + $(HIDE)$(OCAMLLIBDEP) $(DEPFLAGS) "$<" $(TOTARGET) -%.v.d: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENVFILES) +%.v.d: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEP) $(GENVFILES) $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEPBOOT) $(DEPNATDYN) "$<" $(TOTARGET) + $(HIDE)$(COQDEP) -boot $(DEPNATDYN) "$<" $(TOTARGET) %_stubs.c.d: $(D_DEPEND_BEFORE_SRC) %_stubs.c $(D_DEPEND_AFTER_SRC) $(SHOW)'CCDEP $<' |