diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 627 | ||||
| -rw-r--r-- | tools/coq_makefile.ml | 1166 | ||||
| -rw-r--r-- | tools/coqc.ml | 5 | ||||
| -rw-r--r-- | tools/coqdep.ml | 2 | ||||
| -rw-r--r-- | tools/coqdep_common.ml | 17 |
5 files changed, 966 insertions, 851 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in new file mode 100644 index 000000000..5231899c6 --- /dev/null +++ b/tools/CoqMakefile.in @@ -0,0 +1,627 @@ +############################################################################### +## v # The Coq Proof Assistant ## +## <O___,, # INRIA - CNRS - LIX - LRI - PPS ## +## \VV/ # ## +## // # ## +############################################################################### +## GNUMakefile for Coq @COQ_VERSION@ + +# For debugging purposes (must stay here, don't move below) +INITIAL_VARS := $(.VARIABLES) +# To implement recursion we save the name of the main Makefile +SELF := $(lastword $(MAKEFILE_LIST)) + +# This file is generated by coq_makefile and contains many variable +# definitions, like the list of .v files or the path to Coq +include @CONF_FILE@ + +# Put in place old names +VFILES := $(COQMF_VFILES) +MLIFILES := $(COQMF_MLIFILES) +MLFILES := $(COQMF_MLFILES) +ML4FILES := $(COQMF_ML4FILES) +MLPACKFILES := $(COQMF_MLPACKFILES) +MLLIBFILES := $(COQMF_MLLIBFILES) +INSTALLCOQDOCROOT := $(COQMF_INSTALLCOQDOCROOT) +OTHERFLAGS := $(COQMF_OTHERFLAGS) +COQ_SRC_SUBDIRS := $(COQMF_COQ_SRC_SUBDIRS) +OCAMLLIBS := $(COQMF_OCAMLLIBS) +SRC_SUBDIRS := $(COQMF_SRC_SUBDIRS) +COQLIBS := $(COQMF_COQLIBS) +COQLIBS_NOML := $(COQMF_COQLIBS_NOML) +LOCAL := $(COQMF_LOCAL) +COQLIB := $(COQMF_COQLIB) +DOCDIR := $(COQMF_DOCDIR) +OCAMLFIND := $(COQMF_OCAMLFIND) +CAMLP4 := $(COQMF_CAMLP4) +CAMLP4O := $(COQMF_CAMLP4O) +CAMLP4BIN := $(COQMF_CAMLP4BIN) +CAMLP4LIB := $(COQMF_CAMLP4LIB) +CAMLP4OPTIONS := $(COQMF_CAMLP4OPTIONS) +HASNATDYNLINK := $(COQMF_HASNATDYNLINK) +COQ_SRC_SUBDIRS := $(COQMF_COQ_SRC_SUBDIRS) + +@CONF_FILE@: @PROJECT_FILE@ + @COQ_MAKEFILE_INVOCATION@ + +# This file can be created by the user to hook into double colon rules or +# add any other Makefile code he may need +-include @LOCAL_FILE@ + +# Parameters ################################################################## +# +# Parameters are make variable assignments. +# They can be passed to (each call to) make on the command line. +# They can also be put in @LOCAL_FILE@ once an forall. +# For retro-compatibility reasons they can be put in the _CoqProject, but this +# practice is discouraged since _CoqProject better not contain make specific +# code (be nice to user interfaces). + +# Print shell commands (set to non empty) +VERBOSE ?= + +# Time the Coq process (set to non empty), and how (see default value) +TIMED?= +TIMECMD?= +STDTIME?=/usr/bin/time -f "$* (user: %U mem: %M ko)" + +# Coq binaries +COQC ?= $(TIMER) "$(COQBIN)coqc" +COQCHK ?= $(TIMER) "$(COQBIN)coqchk" +COQDEP ?= "$(COQBIN)coqdep" +GALLINA ?= "$(COQBIN)gallina" +COQDOC ?= "$(COQBIN)coqdoc" +COQMKTOP ?= "$(COQBIN)coqmktop" + +# OCaml binaries +CAMLC ?= $(OCAMLFIND) ocamlc -c -rectypes -thread +CAMLOPTC ?= $(OCAMLFIND) opt -c -rectypes -thread +CAMLLINK ?= $(OCAMLFIND) ocamlc -rectypes -thread +CAMLOPTLINK ?= $(OCAMLFIND) opt -rectypes -thread +CAMLDEP ?= $(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack + +# DESTDIR is prepended to all installation paths +DESTDIR ?= + +# Debug builds, typically -g to OCaml, -debug to Coq. +CAMLDEBUG ?= +COQDEBUG ?= + + + +########## End of parameters ################################################## +# What follows may be relevant to you only if you need to +# extend this Makefile. If so, look for 'Extension point' here and +# put in @LOCAL_FILE@ double colon rules accordingly. +# E.g. to perform some work after the all target completes you can write +# +# post-all:: +# echo "All done!" +# +# in @LOCAL_FILE@ +# +############################################################################### + + + + +# Flags ####################################################################### +# +# We define a bunch of variables combining the parameters + +SHOW := $(if $(VERBOSE),@true "",@echo "") +HIDE := $(if $(VERBOSE),,@) + +TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) + +OPT?= + +COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) +COQCHKFLAGS?=-silent -o $(COQLIBS) +COQDOCFLAGS?=-interpolate -utf8 $(COQLIBS_NOML) + +# The version of Coq being run and the version of coq_makefile that +# generated this makefile +COQ_VERSION:=$(shell $(COQC) --print-version | cut -d ' ' -f 1) +COQMAKEFILE_VERSION:=@COQ_VERSION@ + +COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)") + +CAMLFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB) + +CAMLLIB:=$(shell $(OCAMLFIND) printconf stdlib) + +# FIXME This should be generated by Coq +GRAMMARS:=grammar.cma +ifeq ($(CAMLP4),camlp5) +CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo +else +CAMLP4EXTEND= +endif + +PP:=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(COQLIB)/grammar compat5.cmo $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl' + +COQLIBINSTALL = $(COQLIB)user-contrib +COQDOCINSTALL = $(DOCDIR)user-contrib +COQTOPINSTALL = $(COQLIB)toploop + +# Retro compatibility (DESTDIR is standard on Unix, DESTROOT is not) +ifneq "$(DSTROOT)" "" +DESTDIR := $(DSTROOT) +endif + +# Files ####################################################################### +# +# We here define a bunch of variables about the files being part of the +# Coq project in order to ease the writing of build target and build rules + +ALLSRCFILES := \ + $(VFILES) \ + $(ML4FILES) \ + $(MLFILES) \ + $(MLPACKFILES) \ + $(MLLIBFILES) \ + $(MLIFILES) + +# helpers +vo_to_obj = $(addsuffix .o,\ + $(filter-out Warning: Error:,\ + $(shell $(COQBIN)coqtop -q -noinit -batch -quiet -print-mod-uid $(1)))) +strip_dotslash = $(patsubst ./%,%,$(1)) +VO = vo + +VOFILES = $(VFILES:.v=.$(VO)) +GLOBFILES = $(VFILES:.v=.glob) +GFILES = $(VFILES:.v=.g) +HTMLFILES = $(VFILES:.v=.html) +GHTMLFILES = $(VFILES:.v=.g.html) +BEAUTYFILES = $(addsuffix .beautified,$(VFILES)) +TEXFILES = $(VFILES:.v=.tex) +GTEXFILES = $(VFILES:.v=.g.tex) +CMOFILES = \ + $(ML4FILES:.ml4=.cmo) \ + $(MLFILES:.ml=.cmo) \ + $(MLPACKFILES:.mlpack=.cmo) +CMXFILES = $(CMOFILES:.cmo=.cmx) +OFILES = $(CMXFILES:.cmx=.o) +CMAFILES = $(MLLIBFILES:.mllib=.cma) +CMXAFILES = $(CMAFILES:.cma=.cmxa) +CMIFILES = \ + $(CMOFILES:.cmo=.cmi) \ + $(MLIFILES:.mli=.cmi) +# the /if/ is because old _CoqProject did not list a .ml(pack|lib) but just +# a .ml4 file +CMXSFILES = \ + $(MLPACKFILES:.mlpack=.cmxs) \ + $(CMXAFILES:.cmxa=.cmxs) \ + $(if $(MLPACKFILES)$(CMXAFILES),,\ + $(ML4FILES:.ml4=.cmxs) $(MLFILES:.ml=.cmxs)) + +# files that are packed into a plugin (no extension) +PACKEDFILES = \ + $(call strip_dotslash, \ + $(foreach lib, \ + $(call strip_dotslash, \ + $(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES)),$($(lib)))) +# files that are archived into a .cma (mllib) +LIBEDFILES = \ + $(call strip_dotslash, \ + $(foreach lib, \ + $(call strip_dotslash, \ + $(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES)),$($(lib)))) +CMIFILESTOINSTALL = $(filter-out $(addsuffix .cmi,$(PACKEDFILES)),$(CMIFILES)) +CMOFILESTOINSTALL = $(filter-out $(addsuffix .cmo,$(PACKEDFILES)),$(CMOFILES)) +OBJFILES = $(call vo_to_obj,$(VOFILES)) +ALLNATIVEFILES = \ + $(OBJFILES:.o=.cmi) \ + $(OBJFILES:.o=.cmo) \ + $(OBJFILES:.o=.cmx) \ + $(OBJFILES:.o=.cmxs) +# trick: wildcard filters out non-existing files +NATIVEFILESTOINSTALL = $(foreach f, $(ALLNATIVEFILES), $(wildcard $f)) +FILESTOINSTALL = \ + $(VOFILES) \ + $(VFILES) \ + $(GLOBFILES) \ + $(NATIVEFILESTOINSTALL) \ + $(CMOFILESTOINSTALL) \ + $(CMIFILESTOINSTALL) \ + $(CMAFILES) +ifeq '$(HASNATDYNLINK)' 'true' +DO_NATDYNLINK = yes +FILESTOINSTALL += $(CMXSFILES) $(CMXAFILES) $(CMOFILESTOINSTALL:.cmo=.cmx) +else +DO_NATDYNLINK = +endif + +ALLDFILES = $(addsuffix .d,$(ALLSRCFILES)) + +# Compilation targets ######################################################### + +all: + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" pre-all + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" real-all + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" post-all +.PHONY: all + +# Extension points for actions to be performed before/after the all target +pre-all:: + @# Extension point + $(HIDE)if [ "$(COQMAKEFILE_VERSION)" != "$(COQ_VERSION)" ]; then\ + echo "W: This Makefile was generated by Coq $(COQMAKEFILE_VERSION)";\ + echo "W: while the current Coq version is $(COQ_VERSION)";\ + fi +.PHONY: pre-all + +post-all:: + @# Extension point +.PHONY: post-all + +real-all: $(VOFILES) $(CMOFILES) $(CMAFILES) $(if $(DO_NATDYNLINK),$(CMXSFILES)) +.PHONY: real-all + +# FIXME, see Ralph's bugreport +quick: $(VOFILES:.vo=.vio) +.PHONY: quick + +vio2vo: + $(COQC) $(COQDEBUG) $(COQFLAGS) \ + -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio) +.PHONY: vio2vo + +checkproofs: + $(COQC) $(COQDEBUG) $(COQFLAGS) \ + -schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio) +.PHONY: checkproofs + +validate: $(VOFILES) + $(COQCHK) $(COQCHKFLAGS) $(notdir $(^:.vo=)) +.PHONY: validate + +only: $(TGTS) +.PHONY: only + +# Documentation targets ####################################################### + +html: $(GLOBFILES) $(VFILES) + $(SHOW)'COQDOC -d html $(GAL)' + $(HIDE)mkdir -p html + $(HIDE)$(COQDOC) \ + -toc $(COQDOCFLAGS) -html $(GAL) $(COQDOCLIBS) -d html $(VFILES) + +mlihtml: $(MLIFILES:.mli=.cmi) + $(SHOW)'OCAMLDOC -d $@' + $(HIDE)mkdir $@ || rm -rf $@/* + $(HIDE)$(OCAMLFIND) ocamldoc -html -rectypes \ + -d $@ -m A $(CAMLDEBUG) $(CAMLFLAGS) $(MLIFILES) + +all-mli.tex: $(MLIFILES:.mli=.cmi) + $(SHOW)'OCAMLDOC -latex $@' + $(OCAMLFIND) ocamldoc -latex -rectypes \ + -o $@ -m A $(CAMLDEBUG) $(CAMLFLAGS) $(MLIFILES) + +gallina: $(GFILES) + +all.ps: $(VFILES) + $(SHOW)'COQDOC -ps $(GAL)' + $(HIDE)$(COQDOC) \ + -toc $(COQDOCFLAGS) -ps $(GAL) $(COQDOCLIBS) \ + -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)` + +all.pdf: $(VFILES) + $(SHOW)'COQDOC -pdf $(GAL)' + $(HIDE)$(COQDOC) \ + -toc $(COQDOCFLAGS) -pdf $(GAL) $(COQDOCLIBS) \ + -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)` + +# FIXME: not quite right, since the output name is different +gallinahtml: GAL=g +gallinahtml: html + +all-gal.ps: GAL=-g +all-gal.ps: all.ps + +all-gal.pdf: GAL=-g +all-gal.pdf: all.pdf + +# ? +beautify: $(BEAUTYFILES) + for file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done + @echo 'Do not do "make clean" until you are sure that everything went well!' + @echo 'If there were a problem, execute "for file in $$(find . -name \*.v.old -print); do mv $${file} $${file%.old}; done" in your shell/' +.PHONY: beautify + +# Installation targets ######################################################## +# +# There rules can be extended in @LOCAL_FILE@ +# Extensions can't assume when they run. + +install: install-extra + $(HIDE)for f in $(FILESTOINSTALL); do\ + df="`$(COQMF_MAKEFILE) -destination-of "$$f" $(COQLIBS)`";\ + if [ -z "$$df" ]; then\ + echo SKIP "$$f" since it has no logical path;\ + else\ + install -d "$(DESTDIR)$(COQLIBINSTALL)/$$df"; \ + install -m 0644 "$$f" "$(DESTDIR)$(COQLIBINSTALL)/$$df"; \ + echo INSTALL "$$f" "$(DESTDIR)$(COQLIBINSTALL)/$$df";\ + fi;\ + done +install-extra:: + @# Extension point +.PHONY: install install-extra + +install-doc:: html mlihtml + @# Extension point + $(HIDE)install -d "$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html" + $(HIDE)for i in html/*; do \ + dest="$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\ + install -m 0644 "$$i" "$$dest";\ + echo INSTALL "$$i" "$$dest";\ + done + $(HIDE)install -d \ + "$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml" + $(HIDE)for i in mlihtml/*; do \ + dest="$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\ + install -m 0644 "$$i" "$$dest";\ + echo INSTALL "$$i" "$$dest";\ + done +.PHONY: install-doc + +uninstall:: + @# Extension point + $(HIDE)for f in $(FILESTOINSTALL); do \ + df="`$(COQMF_MAKEFILE) -destination-of "$$f" $(COQLIBS)`";\ + instf="$(DESTDIR)$(COQLIBINSTALL)/$$df/`basename $$f`"; \ + rm -f "$$instf";\ + echo RM "$$instf"; \ + rmdir --ignore-fail-on-non-empty "$(DESTDIR)$(COQLIBINSTALL)/$$df/"; \ + done +.PHONY: uninstall + +uninstall-doc:: + @# Extension point + $(SHOW)'RM $(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html' + $(HIDE)rm -rf "$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html" + $(SHOW)'RM $(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml' + $(HIDE)rm -rf "$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml" + $(HIDE)rmdir --ignore-fail-on-non-empty \ + "$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/" +.PHONY: uninstall-doc + +# Cleaning #################################################################### +# +# There rules can be extended in @LOCAL_FILE@ +# Extensions can't assume when they run. + +clean:: + @# Extension point + $(SHOW)'CLEAN' + $(HIDE)rm -f $(CMOFILES) + $(HIDE)rm -f $(CMIFILES) + $(HIDE)rm -f $(CMAFILES) + $(HIDE)rm -f $(CMOFILES:.cmo=.cmx) + $(HIDE)rm -f $(CMXAFILES) + $(HIDE)rm -f $(CMXSFILES) + $(HIDE)rm -f $(CMOFILES:.cmo=.o) + $(HIDE)rm -f $(CMXAFILES:.cmxa=.a) + $(HIDE)rm -f $(ALLDFILES) + $(HIDE)rm -f $(ALLNATIVEFILES) + $(HIDE)find . -name .coq-native -type d -empty -delete + $(HIDE)rm -f $(VOFILES) + $(HIDE)rm -f $(VOFILES:.vo=.vio) + $(HIDE)rm -f $(GFILES) + $(HIDE)rm -f $(BEAUTYFILES) $(VFILES:=.old) + $(HIDE)rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob all-mli.tex + $(HIDE)rm -f $(VFILES:.v=.glob) + $(HIDE)rm -f $(VFILES:.v=.tex) + $(HIDE)rm -f $(VFILES:.v=.g.tex) + $(HIDE)rm -rf html mlihtml +.PHONY: clean + +cleanall:: clean + @# Extension point + $(SHOW)'CLEAN *.aux' + $(HIDE)rm -f $(foreach f,$(VFILES:.v=),$(dir $(f)).$(notdir $(f)).aux) +.PHONY: cleanall + +archclean:: + @# Extension point + $(SHOW)'CLEAN *.cmx *.o' + $(HIDE)rm -f $(ALLNATIVEFILES) + $(HIDE)rm -f $(CMOFILES:%.cmo=%.cmx) +.PHONY: archclean + + +# Compilation rules ########################################################### + +$(MLIFILES:.mli=.cmi): %.cmi: %.mli + $(SHOW)'CAMLC -c $<' + $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $< + +$(ML4FILES:.ml4=.cmo): %.cmo: %.ml4 + $(SHOW)'CAMLC -pp -c $<' + $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(PP) -impl $< + +$(ML4FILES:.ml4=.cmx): %.cmx: %.ml4 + $(SHOW)'CAMLOPT -pp -c $(FOR_PACK) $<' + $(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(PP) $(FOR_PACK) -impl $< + +$(MLFILES:.ml=.cmo): %.cmo: %.ml + $(SHOW)'CAMLC -c $<' + $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $< + +$(MLFILES:.ml=.cmx): %.cmx: %.ml + $(SHOW)'CAMLOPT -c $(FOR_PACK) $<' + $(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(FOR_PACK) $< + + +$(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa + $(SHOW)'CAMLOPT -shared -o $@' + $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) \ + -linkall -shared -o $@ $< + +$(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib + $(SHOW)'CAMLC -a -o $@' + $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $^ + +$(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib + $(SHOW)'CAMLOPT -a -o $@' + $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $^ + + +$(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmx + $(SHOW)'CAMLOPT -shared -o $@' + $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -shared -o $@ $< + +$(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack + $(SHOW)'CAMLC -pack -o $@' + $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^ + +$(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack + $(SHOW)'CAMLOPT -pack -o $@' + $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^ + +# This rule is for _CoqProject with no .mllib nor .mlpack +$(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix .cmxs,$(PACKEDFILES)) $(addsuffix .cmxs,$(LIBEDFILES)),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs)): %.cmxs: %.cmx + $(SHOW)'[deprecated,use-mllib-or-mlpack] CAMLOPT -shared -o $@' + $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -shared -o $@ $< + +$(VOFILES): %.vo: %.v + $(SHOW)COQC $< + $(HIDE)$(COQC) $(COQDEBUG) $(COQFLAGS) $< + +# FIXME ?merge with .vo / .vio ? +$(GLOBFILES): %.glob: %.v + $(COQC) $(COQDEBUG) $(COQFLAGS) $< + +$(VFILES:.v=.vio): %.vio: %.v + $(SHOW)COQC -quick $< + $(HIDE)$(COQC) -quick $(COQDEBUG) $(COQFLAGS) $< + +$(BEAUTYFILES): %.v.beautified: %.v + $(SHOW)'BEAUTIFY $<' + $(HIDE)$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $< + +$(GFILES): %.g: %.v + $(SHOW)'GALLINA $<' + $(HIDE)$(GALLINA) $< + +$(TEXFILES): %.tex: %.v + $(SHOW)'COQDOC -latex $<' + $(HIDE)$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@ + +$(GTEXFILES): %.g.tex: %.v + $(SHOW)'COQDOC -latex -g $<' + $(HIDE)$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@ + +$(HTMLFILES): %.html: %.v %.glob + $(SHOW)'COQDOC -html $<' + $(HIDE)$(COQDOC) $(COQDOCFLAGS) -html $< -o $@ + +$(GHTMLFILES): %.g.html: %.v %.glob + $(SHOW)'COQDOC -html -g $<' + $(HIDE)$(COQDOC) $(COQDOCFLAGS) -html -g $< -o $@ + +# Dependency files ############################################################ + +ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),) + -include $(ALLDFILES) +else + ifeq ($(MAKECMDGOALS),) + -include $(ALLDFILES) + endif +endif + +.SECONDARY: $(ALLDFILES) + +redir_if_ok = > "$@" || ( RV=$$?; rm -f "$@"; exit $$RV ) + +$(addsuffix .d,$(MLIFILES)): %.mli.d: %.mli + $(SHOW)'CAMLDEP $<' + $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) + +$(addsuffix .d,$(ML4FILES)): %.ml4.d: %.ml4 + $(SHOW)'CAMLDEP -pp $<' + $(HIDE)$(CAMLDEP) $(OCAMLLIBS) $(PP) -impl "$<" $(redir_if_ok) + +$(addsuffix .d,$(MLFILES)): %.ml.d: %.ml + $(SHOW)'CAMLDEP $<' + $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) + +$(addsuffix .d,$(MLLIBFILES)): %.mllib.d: %.mllib + $(SHOW)'COQDEP $<' + $(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" $(redir_if_ok) + +$(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack + $(SHOW)'COQDEP $<' + $(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" $(redir_if_ok) + +$(addsuffix .d,$(VFILES)): %.v.d: %.v + $(SHOW)'COQDEP $<' + $(HIDE)$(COQDEP) $(COQLIBS) -c "$<" $(redir_if_ok) + +# Misc ######################################################################## + +byte: + $(HIDE)$(MAKE) all "OPT:=-byte" -f "$(SELF)" +.PHONY: byte + +opt: + $(HIDE)$(MAKE) all "OPT:=-opt" -f "$(SELF)" +.PHONY: opt + +# This is deprecated. To extend this makefile use +# extension points and @LOCAL_FILE@ +printenv:: + $(warning printenv is deprecated) + $(warning write extensions in @LOCAL_FILE@ or include @CONF_FILE@) + @echo 'LOCAL = $(LOCAL)' + @echo 'COQLIB = $(COQLIB)' + @echo 'DOCDIR = $(DOCDIR)' + @echo 'OCAMLFIND = $(OCAMLFIND)' + @echo 'CAMLP4 = $(CAMLP4)' + @echo 'CAMLP4O = $(CAMLP4O)' + @echo 'CAMLP4BIN = $(CAMLP4BIN)' + @echo 'CAMLP4LIB = $(CAMLP4LIB)' + @echo 'CAMLP4OPTIONS = $(CAMLP4OPTIONS)' + @echo 'HASNATDYNLINK = $(HASNATDYNLINK)' + @echo 'SRC_SUBDIRS = $(SRC_SUBDIRS)' + @echo 'COQ_SRC_SUBDIRS = $(COQ_SRC_SUBDIRS)' + @echo 'OCAMLFIND = $(OCAMLFIND)' + @echo 'PP = $(PP)' + @echo 'COQFLAGS = $(COQFLAGS)' + @echo 'COQLIBINSTALL = $(COQLIBINSTALL)' + @echo 'COQDOCINSTALL = $(COQDOCINSTALL)' +.PHONY: printenv + +# Generate a .merlin file. If you need to append directives to this +# file you can extend the merlin-hook target in @LOCAL_FILE@ +.merlin: + $(SHOW)'FILL .merlin' + $(HIDE)echo 'FLG -rectypes' > .merlin + $(HIDE)echo "B $(COQLIB)" >> .merlin + $(HIDE)echo "S $(COQLIB)" >> .merlin + $(HIDE)$(foreach d,$(COQ_SRC_SUBDIRS), \ + echo "B $(COQLIB)$(d)" >> .merlin;) + $(HIDE)$(foreach d,$(COQ_SRC_SUBDIRS), \ + echo "S $(COQLIB)$(d)" >> .merlin;) + $(HIDE)$(foreach d,$(SRC_SUBDIRS), echo "B $(d)" >> .merlin;) + $(HIDE)$(foreach d,$(SRC_SUBDIRS), echo "S $(d)" >> .merlin;) + $(HIDE)$(MAKE) merlin-hook -f "$(SELF)" +.PHONY: merlin + +merlin-hook:: + @# Extension point +.PHONY: merlin-hook + +# prints all variables +debug: + $(foreach v,\ + $(sort $(filter-out $(INITIAL_VARS) INITIAL_VARS,\ + $(.VARIABLES))),\ + $(info $(v) = $($(v)))) +.PHONY: debug + +.DEFAULT_GOAL := all + diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 4875cb62b..78c92e68b 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -8,17 +8,13 @@ (* Coq_makefile: automatically create a Makefile for a Coq development *) +open CoqProject_file +open Printf + let output_channel = ref stdout let makefile_name = ref "Makefile" let make_name = ref "" -let some_vfile = ref false -let some_mlfile = ref false -let some_mlifile = ref false -let some_ml4file = ref false -let some_mllibfile = ref false -let some_mlpackfile = ref false - let print x = output_string !output_channel x let printf x = Printf.fprintf !output_channel x @@ -31,29 +27,10 @@ let rec print_prefix_list sep = function | x :: l -> print sep; print x; print_prefix_list sep l | [] -> () -let section s = - let l = String.length s in - let print_com s = - print "#"; - print s; - print "#\n" in - print_com (String.make (l+2) '#'); - print_com (String.make (l+2) ' '); - print "# "; print s; print " #\n"; - print_com (String.make (l+2) ' '); - print_com (String.make (l+2) '#'); - print "\n" - (* These are the Coq library directories that are used for * plugin development *) -let lib_dirs = - ["kernel"; "lib"; "library"; "parsing"; - "pretyping"; "interp"; "printing"; "intf"; - "proofs"; "tactics"; "tools"; - "vernac"; "stm"; "toplevel"; "grammar"; "config"; - "engine"] - +let lib_dirs = Envars.coq_src_subdirs let usage () = output_string stderr "Usage summary:\ @@ -104,12 +81,6 @@ let is_genrule r = (* generic rule (like bar%foo: ...) *) let genrule = Str.regexp("%") in Str.string_match genrule r 0 -let string_prefix a b = - let rec aux i = - try if a.[i] = b.[i] then aux (i+1) else i with Invalid_argument _ -> i - in - String.sub a 0 (aux 0) - let is_prefix dir1 dir2 = let l1 = String.length dir1 in let l2 = String.length dir2 in @@ -122,830 +93,341 @@ let is_prefix dir1 dir2 = else false let physical_dir_of_logical_dir ldir = - let le = String.length ldir - 1 in + let ldir = Bytes.of_string ldir in + let le = Bytes.length ldir - 1 in let pdir = - if le >= 0 && ldir.[le] = '.' then String.sub ldir 0 (le - 1) - else ldir - in - String.map (fun c -> if c = '.' then '/' else c) pdir - -let standard opt = - print "byte:\n"; - print "\t$(MAKE) all \"OPT:=-byte\"\n\n"; - print "opt:\n"; - if not opt then print "\t@echo \"WARNING: opt is disabled\"\n"; - print "\t$(MAKE) all \"OPT:="; print (if opt then "-opt" else "-byte"); - print "\"\n\n" - -let classify_files_by_root var files (inc_ml,inc_i,inc_r) = - if List.exists (fun (pdir,_,_) -> pdir = ".") inc_r || - List.exists (fun (pdir,_,_) -> pdir = ".") inc_i - then () - else - let absdir_of_files =List.rev_map - (fun x -> CUnix.canonical_path_name (Filename.dirname x)) - files - in - (* files in scope of a -I option (assuming they are no overlapping) *) - if List.exists (fun (_,a) -> List.mem a absdir_of_files) inc_ml then - begin - printf "%sINC=" var; - List.iter (fun (pdir,absdir) -> - if List.mem absdir absdir_of_files - then printf "$(filter $(wildcard %s/*),$(%s)) " pdir var) - inc_ml; - printf "\n"; - end; - (* Files in the scope of a -R option (assuming they are disjoint) *) - List.iteri (fun i (pdir,_,abspdir) -> - if List.exists (is_prefix abspdir) absdir_of_files then - printf "%s%d=$(patsubst %s/%%,%%,$(filter %s/%%,$(%s)))\n" - var i pdir pdir var) - (inc_i@inc_r) - -let vars_to_put_by_root var_x_files_l (inc_ml,inc_i,inc_r) = - let var_x_absdirs_l = - List.rev_map - (fun (v,l) -> - (v,List.rev_map - (fun x -> CUnix.canonical_path_name (Filename.dirname x)) l)) - var_x_files_l + if le >= 0 && Bytes.get ldir le = '.' then Bytes.sub ldir 0 (le - 1) + else Bytes.copy ldir in - let var_filter f g = - List.fold_left - (fun acc (var,dirs) -> if f dirs then (g var)::acc else acc) - [] var_x_absdirs_l - in - (* All files caught by a -R . option (assuming it is the only one) *) - match inc_i@inc_r with - |[(".",t,_)] -> - (None,[".",physical_dir_of_logical_dir t,List.rev_map fst var_x_files_l]) - |l -> - try - let out = List.assoc "." (List.rev_map (fun (p,l,_) -> (p,l)) l) in - let () = prerr_string "Warning: install rule assumes that -R/-Q . _ is the only -R/-Q option\n" - in - (None,[".",physical_dir_of_logical_dir out,List.rev_map fst var_x_files_l]) - with Not_found -> - (* vars for -Q options *) - let varq = var_filter - (fun l -> List.exists (fun (_,a) -> List.mem a l) inc_ml) - (fun x -> x) - in - (* (physical dir, physical dir of logical path,vars) for -R options - (assuming physical dirs are disjoint) *) - let other = - if l = [] then - [".","$(INSTALLDEFAULTROOT)",[]] - else - Util.List.fold_left_i (fun i out (pdir,ldir,abspdir) -> - let vars_r = var_filter - (List.exists (is_prefix abspdir)) - (fun x -> x^string_of_int i) - in - let pdir' = physical_dir_of_logical_dir ldir in - (pdir,pdir',vars_r)::out) 0 [] l - in (Some varq, other) - -let install_include_by_root perms = - let install_dir for_i (pdir,pdir',vars) = - let b = vars <> [] in - if b then begin - printf "\tcd \"%s\" && for i in " pdir; - print_list " " (List.rev_map (Format.sprintf "$(%s)") vars); - print "; do \\\n"; - printf "\t install -d \"`dirname \"$(DSTROOT)\"$(COQLIBINSTALL)/%s/$$i`\"; \\\n" pdir'; - printf "\t install -m %s $$i \"$(DSTROOT)\"$(COQLIBINSTALL)/%s/$$i; \\\n" perms pdir'; - printf "\tdone\n"; - end; - for_i b pdir' in - let install_i = function - |[] -> fun _ _ -> () - |l -> fun b d -> - if not b then printf "\tinstall -d \"$(DSTROOT)\"$(COQLIBINSTALL)/%s; \\\n" d; - print "\tfor i in "; - print_list " " (List.rev_map (Format.sprintf "$(%sINC)") l); - print "; do \\\n"; - printf "\t install -m %s $$i \"$(DSTROOT)\"$(COQLIBINSTALL)/%s/`basename $$i`; \\\n" perms d; - printf "\tdone\n" - in function - |None,l -> List.iter (install_dir (fun _ _ -> ())) l - |Some v_i,l -> List.iter (install_dir (install_i v_i)) l - -let uninstall_by_root = - let uninstall_dir for_i (pdir,pdir',vars) = - printf "\tprintf 'cd \"$${DSTROOT}\"$(COQLIBINSTALL)/%s" pdir'; - if vars <> [] then begin - print " && rm -f "; - print_list " " (List.rev_map (Format.sprintf "$(%s)") vars); - end; - for_i (); - print " && find . -type d -and -empty -delete\\n"; - print "cd \"$${DSTROOT}\"$(COQLIBINSTALL) && "; - printf "find \"%s\" -maxdepth 0 -and -empty -exec rmdir -p \\{\\} \\;\\n' >> \"$@\"\n" pdir' -in - let uninstall_i = function - |[] -> () - |l -> - print " && \\\\\\nfor i in "; - print_list " " (List.rev_map (Format.sprintf "$(%sINC)") l); - print "; do rm -f \"`basename \"$$i\"`\"; done" - in function - |None,l -> List.iter (uninstall_dir (fun _ -> ())) l - |Some v_i,l -> List.iter (uninstall_dir (fun () -> uninstall_i v_i)) l - -let where_put_doc = function - |_,[],[] -> "$(INSTALLDEFAULTROOT)"; - |_,((_,lp,_)::q as inc_i),[] -> - let pr = List.fold_left (fun a (_,b,_) -> string_prefix a b) lp q in - if (pr <> "") && - ((List.exists (fun(_,b,_) -> b = pr) inc_i) - || pr.[String.length pr - 1] = '.') - then - physical_dir_of_logical_dir pr - else - let () = prerr_string ("Warning: -Q options don't have a correct common prefix," - ^ " install-doc will put anything in $INSTALLDEFAULTROOT\n") in - "$(INSTALLDEFAULTROOT)" - |_,inc_i,((_,lp,_)::q as inc_r) -> - let pr = List.fold_left (fun a (_,b,_) -> string_prefix a b) lp q in - let pr = List.fold_left (fun a (_,b,_) -> string_prefix a b) pr inc_i in - if (pr <> "") && - ((List.exists (fun(_,b,_) -> b = pr) inc_r) - || (List.exists (fun(_,b,_) -> b = pr) inc_i) - || pr.[String.length pr - 1] = '.') - then - physical_dir_of_logical_dir pr - else - let () = prerr_string ("Warning: -R/-Q options don't have a correct common prefix," - ^ " install-doc will put anything in $INSTALLDEFAULTROOT\n") in - "$(INSTALLDEFAULTROOT)" - -let install (vfiles,(mlis,ml4s,mls,mllibs,mlpacks),_,sds) inc = function - |Project_file.NoInstall -> () - |is_install -> - let not_empty = function |[] -> false |_::_ -> true in - let cmos = List.rev_append mlpacks (List.rev_append mls ml4s) in - let cmis = List.rev_append mlis cmos in - let cmxss = List.rev_append cmos mllibs in - let where_what_cmxs = vars_to_put_by_root [("CMXSFILES",cmxss)] inc in - let where_what_oth = vars_to_put_by_root - [("VOFILES",vfiles);("VFILES",vfiles); - ("GLOBFILES",vfiles);("NATIVEFILES",vfiles); - ("CMOFILES",cmos);("CMIFILES",cmis);("CMAFILES",mllibs)] - inc in - let doc_dir = where_put_doc inc in - if is_install = Project_file.UnspecInstall then begin - print "userinstall:\n\t+$(MAKE) USERINSTALL=true install\n\n" - end; - if not_empty cmxss then begin - print "install-natdynlink:\n"; - install_include_by_root "0755" where_what_cmxs; - print "\n"; + for i = 0 to le - 1 do + if Bytes.get pdir i = '.' then Bytes.set pdir i '/'; + done; + Bytes.to_string pdir + +let read_whole_file s = + let ic = open_in s in + let b = Buffer.create (1 lsl 12) in + try + while true do + let s = input_line ic in + Buffer.add_string b s; + Buffer.add_char b '\n'; + done; + assert false; + with End_of_file -> + close_in ic; + Buffer.contents b + +let makefile_template = + let open Filename in + let template = "/tools/CoqMakefile.in" in + if Coq_config.local then + let coqbin = CUnix.canonical_path_name (dirname Sys.executable_name) in + dirname coqbin ^ template + else match Coq_config.coqlib with + | None -> assert false + | Some dir -> dir ^ template + +let quote s = if String.contains s ' ' then "\"" ^ s ^ "\"" else s + +let generate_makefile oc conf_file local_file args project = + let s = read_whole_file makefile_template in + let s = List.fold_left + (fun s (k,v) -> Str.global_replace (Str.regexp_string k) v s) s + [ "@CONF_FILE@", conf_file; + "@LOCAL_FILE@", local_file; + "@COQ_VERSION@", Coq_config.version; + "@PROJECT_FILE@", (Option.default "" project.project_file); + "@COQ_MAKEFILE_INVOCATION@",String.concat " " (List.map quote args); + ] in + output_string oc s +;; + +let section oc s = + let pad = String.make (76 - String.length s) ' ' in + let sharps = String.make 79 '#' in + let spaces = "#" ^ String.make 77 ' ' ^ "#" in + fprintf oc "\n%s\n" sharps; + fprintf oc "%s\n" spaces; + fprintf oc "# %s%s#\n" s pad; + fprintf oc "%s\n" spaces; + fprintf oc "%s\n\n" sharps +;; + +let clean_tgts = ["clean"; "cleanall"; "archclean"] + +let generate_conf_extra_target oc sps = + let pr_path { target; dependencies; phony; command } = + let target = if target = "all" then "custom-all" else target in + if phony then fprintf oc ".PHONY: %s\n" target; + if not (is_genrule target) && not phony then begin + fprintf oc "post-all::\n\t$(MAKE) -f $(SELF) %s\n" target; + if not phony then + fprintf oc "clean::\n\trm -f %s\n" target; end; - if not_empty cmxss then begin - print "install-toploop: $(MLLIBFILES:.mllib=.cmxs)\n"; - printf "\t install -d \"$(DSTROOT)\"$(COQTOPINSTALL)/\n"; - printf "\t install -m 0755 $? \"$(DSTROOT)\"$(COQTOPINSTALL)/\n"; - print "\n"; - end; - print "install:"; - if not_empty cmxss then begin - print "$(if $(HASNATDYNLINK_OR_EMPTY),install-natdynlink)"; - end; - print "\n"; - install_include_by_root "0644" where_what_oth; - List.iter - (fun x -> - printf "\t+cd %s && $(MAKE) DSTROOT=\"$(DSTROOT)\" INSTALLDEFAULTROOT=\"$(INSTALLDEFAULTROOT)/%s\" install\n" x x) - sds; - print "\n"; - let install_one_kind kind dir = - printf "\tinstall -d \"$(DSTROOT)\"$(COQDOCINSTALL)/%s/%s\n" dir kind; - printf "\tfor i in %s/*; do \\\n" kind; - printf "\t install -m 0644 $$i \"$(DSTROOT)\"$(COQDOCINSTALL)/%s/$$i;\\\n" dir; - print "\tdone\n" in - print "install-doc:\n"; - if not_empty vfiles then install_one_kind "html" doc_dir; - if not_empty mlis then install_one_kind "mlihtml" doc_dir; - print "\n"; - let uninstall_one_kind kind dir = - printf "\tprintf 'cd \"$${DSTROOT}\"$(COQDOCINSTALL)/%s \\\\\\n' >> \"$@\"\n" dir; - printf "\tprintf '&& rm -f $(shell find \"%s\" -maxdepth 1 -and -type f -print)\\n' >> \"$@\"\n" kind; - print "\tprintf 'cd \"$${DSTROOT}\"$(COQDOCINSTALL) && "; - printf "find %s/%s -maxdepth 0 -and -empty -exec rmdir -p \\{\\} \\;\\n' >> \"$@\"\n" dir kind - in - printf "uninstall_me.sh: %s\n" !makefile_name; - print "\techo '#!/bin/sh' > $@\n"; - if not_empty cmxss then uninstall_by_root where_what_cmxs; - uninstall_by_root where_what_oth; - if not_empty vfiles then uninstall_one_kind "html" doc_dir; - if not_empty mlis then uninstall_one_kind "mlihtml" doc_dir; - print "\tchmod +x $@\n"; - print "\n"; - print "uninstall: uninstall_me.sh\n"; - print "\tsh $<\n\n" - -let make_makefile sds = - if !make_name <> "" then begin - printf "%s: %s\n" !makefile_name !make_name; - print "\tmv -f $@ $@.bak\n"; - print "\t\"$(COQBIN)coq_makefile\" -f $< -o $@\n\n"; - List.iter - (fun x -> print "\t+cd "; print x; print " && $(MAKE) Makefile\n") - sds; - print "\n"; - end - -let clean sds sps = - print "clean::\n"; - if !some_mlfile || !some_mlifile || !some_ml4file - || !some_mllibfile || !some_mlpackfile - then - begin - print "\trm -f $(ALLCMOFILES) $(CMIFILES) $(CMAFILES)\n"; - print "\trm -f $(ALLCMOFILES:.cmo=.cmx) $(CMXAFILES) $(CMXSFILES) $(ALLCMOFILES:.cmo=.o) $(CMXAFILES:.cmxa=.a)\n"; - print "\trm -f $(addsuffix .d,$(MLFILES) $(MLIFILES) $(ML4FILES) $(MLLIBFILES) $(MLPACKFILES))\n"; - end; - if !some_vfile then - begin - print "\trm -f $(OBJFILES) $(OBJFILES:.o=.native) $(NATIVEFILES)\n"; - print "\tfind . -name .coq-native -type d -empty -delete\n"; - print "\trm -f $(VOFILES) $(VOFILES:.vo=.vio) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)\n" - end; - print "\trm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) all-mli.tex\n"; - print "\t- rm -rf html mlihtml uninstall_me.sh\n"; - List.iter - (fun (file,_,is_phony,_) -> - if not (is_phony || is_genrule file) then - (print "\t- rm -rf "; print file; print "\n")) - sps; - List.iter - (fun x -> print "\t+cd "; print x; print " && $(MAKE) clean\n") - sds; - print "\n"; - let () = - if !some_vfile then - let () = print "cleanall:: clean\n" in - print "\trm -f $(foreach f,$(VFILES:.v=),$(dir $(f)).$(notdir $(f)).aux)\n\n" in - print "archclean::\n"; - print "\trm -f *.cmx *.o\n"; - List.iter - (fun x -> print "\t+cd "; print x; print " && $(MAKE) archclean\n") - sds; - print "\n"; - print "printenv:\n\t@\"$(COQBIN)coqtop\" -config\n"; - print "\t@echo 'OCAMLFIND =\t$(OCAMLFIND)'\n\t@echo 'PP =\t$(PP)'\n\t@echo 'COQFLAGS =\t$(COQFLAGS)'\n"; - print "\t@echo 'COQLIBINSTALL =\t$(COQLIBINSTALL)'\n\t@echo 'COQDOCINSTALL =\t$(COQDOCINSTALL)'\n\n" - -let header_includes () = () - -let implicit () = - section "Implicit rules."; - let mli_rules () = - print "$(MLIFILES:.mli=.cmi): %.cmi: %.mli\n"; - print "\t$(SHOW)'CAMLC -c $<'\n"; - print "\t$(HIDE)$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; - print "$(addsuffix .d,$(MLIFILES)): %.mli.d: %.mli\n"; - print "\t$(SHOW)'CAMLDEP $<'\n"; - print "\t$(HIDE)$(CAMLDEP) $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" - in - let ml4_rules () = - print "$(ML4FILES:.ml4=.cmo): %.cmo: %.ml4\n"; - print "\t$(SHOW)'CAMLC -pp -c $<'\n"; - print "\t$(HIDE)$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n"; - print "$(filter-out $(addsuffix .cmx,$(foreach lib,$(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(ML4FILES:.ml4=.cmx)): %.cmx: %.ml4\n"; - print "\t$(SHOW)'CAMLOPT -pp -c $<'\n"; - print "\t$(HIDE)$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n"; - print "$(addsuffix .d,$(ML4FILES)): %.ml4.d: %.ml4\n"; - print "\t$(SHOW)'CAMLDEP -pp $<'\n"; - print "\t$(HIDE)$(CAMLDEP) $(OCAMLLIBS) $(PP) -impl \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in - let ml_rules () = - print "$(MLFILES:.ml=.cmo): %.cmo: %.ml\n"; - print "\t$(SHOW)'CAMLC -c $<'\n"; - print "\t$(HIDE)$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; - print "$(filter-out $(addsuffix .cmx,$(foreach lib,$(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(MLFILES:.ml=.cmx)): %.cmx: %.ml\n"; - print "\t$(SHOW)'CAMLOPT -c $<'\n"; - print "\t$(HIDE)$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; - print "$(addsuffix .d,$(MLFILES)): %.ml.d: %.ml\n"; - print "\t$(SHOW)'CAMLDEP $<'\n"; - print "\t$(HIDE)$(CAMLDEP) $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in - let cmxs_rules () = (* order is important here when there is foo.ml and foo.mllib *) - print "$(filter-out $(MLLIBFILES:.mllib=.cmxs),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs) $(MLPACKFILES:.mlpack=.cmxs)): %.cmxs: %.cmx\n"; - print "\t$(SHOW)'CAMLOPT -shared -o $@'\n"; - print "\t$(HIDE)$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $<\n\n"; - print "$(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa\n"; - print "\t$(SHOW)'CAMLOPT -shared -o $@'\n"; - print "\t$(HIDE)$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -linkall -shared -o $@ $<\n\n" - in - let mllib_rules () = - print "$(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib\n"; - print "\t$(SHOW)'CAMLC -a -o $@'\n"; - print "\t$(HIDE)$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n"; - print "$(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib\n"; - print "\t$(SHOW)'CAMLOPT -a -o $@'\n"; - print "\t$(HIDE)$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n"; - print "$(addsuffix .d,$(MLLIBFILES)): %.mllib.d: %.mllib\n"; - print "\t$(SHOW)'COQDEP $<'\n"; - print "\t$(HIDE)$(COQDEP) $(OCAMLLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" - in - let mlpack_rules () = - print "$(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack\n"; - print "\t$(SHOW)'CAMLC -pack -o $@'\n"; - print "\t$(HIDE)$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^\n\n"; - print "$(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack\n"; - print "\t$(SHOW)'CAMLOPT -pack -o $@'\n"; - print "\t$(HIDE)$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^\n\n"; - print "$(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack\n"; - print "\t$(SHOW)'COQDEP $<'\n"; - print "\t$(HIDE)$(COQDEP) $(OCAMLLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" - in - let v_rules () = - print "$(VOFILES): %.vo: %.v\n"; - print "\t$(SHOW)COQC $<\n"; - print "\t$(HIDE)$(COQC) $(COQDEBUG) $(COQFLAGS) $<\n\n"; - print "$(GLOBFILES): %.glob: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $<\n\n"; - print "$(VFILES:.v=.vio): %.vio: %.v\n\t$(COQC) -quick $(COQDEBUG) $(COQFLAGS) $<\n\n"; - print "$(GFILES): %.g: %.v\n\t$(GALLINA) $<\n\n"; - print "$(VFILES:.v=.tex): %.tex: %.v\n\t$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@\n\n"; - print "$(HTMLFILES): %.html: %.v %.glob\n\t$(COQDOC) $(COQDOCFLAGS) -html $< -o $@\n\n"; - print "$(VFILES:.v=.g.tex): %.g.tex: %.v\n\t$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@\n\n"; - print "$(GHTMLFILES): %.g.html: %.v %.glob\n\t$(COQDOC) $(COQDOCFLAGS) -html -g $< -o $@\n\n"; - print "$(addsuffix .d,$(VFILES)): %.v.d: %.v\n"; - print "\t$(SHOW)'COQDEP $<'\n"; - print "\t$(HIDE)$(COQDEP) $(COQLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n"; - print "$(addsuffix .beautified,$(VFILES)): %.v.beautified:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*.v\n\n" - in - if !some_mlifile then mli_rules (); - if !some_ml4file then ml4_rules (); - if !some_mlfile then ml_rules (); - if !some_mlfile || !some_ml4file then cmxs_rules (); - if !some_mllibfile then mllib_rules (); - if !some_mlpackfile then mlpack_rules (); - if !some_vfile then v_rules () - -let variables is_install opt (args,defs) = - let var_aux (v,def) = print v; print "="; print def; print "\n" in - section "Variables definitions."; - List.iter var_aux defs; - print "\n"; - if not opt then - print "override OPT:=-byte\n" - else - print "OPT?=\n"; - begin - match args with - |[] -> () - |h::t -> print "OTHERFLAGS="; - print h; - List.iter (fun s -> print " ";print s) t; - print "\n"; - end; - (* Coq executables and relative variables *) - if !some_vfile || !some_mlpackfile || !some_mllibfile then - print "COQDEP?=\"$(COQBIN)coqdep\" -c\n"; - if !some_vfile then begin - print "COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)\n"; - print "COQCHKFLAGS?=-silent -o\n"; - print "COQDOCFLAGS?=-interpolate -utf8\n"; - print "COQC?=$(TIMER) \"$(COQBIN)coqc\"\n"; - print "GALLINA?=\"$(COQBIN)gallina\"\n"; - print "COQDOC?=\"$(COQBIN)coqdoc\"\n"; - print "COQCHK?=\"$(COQBIN)coqchk\"\n"; - print "COQMKTOP?=\"$(COQBIN)coqmktop\"\n\n"; - end; - (* Caml executables and relative variables *) - if !some_ml4file || !some_mlfile || !some_mlifile then begin - print "COQSRCLIBS?=" ; - List.iter (fun c -> print "-I \"$(COQLIB)"; print c ; print "\" \\\n") lib_dirs ; - List.iter (fun c -> print " \\\ -\n -I \"$(COQLIB)/"; print c; print "\"") Coq_config.plugins_dirs; print "\n"; - print "ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)\n\n"; - print "CAMLC?=$(OCAMLFIND) ocamlc -c -rectypes -thread -safe-string\n"; - print "CAMLOPTC?=$(OCAMLFIND) opt -c -rectypes -thread -safe-string\n"; - print "CAMLLINK?=$(OCAMLFIND) ocamlc -rectypes -thread -safe-string\n"; - print "CAMLOPTLINK?=$(OCAMLFIND) opt -rectypes -thread -safe-string\n"; - print "CAMLDEP?=$(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack\n"; - print "CAMLLIB?=$(shell $(OCAMLFIND) printconf stdlib)\n"; - print "GRAMMARS?=grammar.cma\n"; - print "CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo\n"; - print "PP?=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(COQLIB)/grammar compat5.cmo \\\ -\n $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'\n\n"; - end; - match is_install with - | Project_file.NoInstall -> () - | Project_file.UnspecInstall -> - section "Install Paths."; - print "ifdef USERINSTALL\n"; - print "XDG_DATA_HOME?=\"$(HOME)/.local/share\"\n"; - print "COQLIBINSTALL=$(XDG_DATA_HOME)/coq\n"; - print "COQDOCINSTALL=$(XDG_DATA_HOME)/doc/coq\n"; - print "else\n"; - print "COQLIBINSTALL=\"${COQLIB}user-contrib\"\n"; - print "COQDOCINSTALL=\"${DOCDIR}user-contrib\"\n"; - print "COQTOPINSTALL=\"${COQLIB}toploop\"\n"; - print "endif\n\n" - | Project_file.TraditionalInstall -> - section "Install Paths."; - print "COQLIBINSTALL=\"${COQLIB}user-contrib\"\n"; - print "COQDOCINSTALL=\"${DOCDIR}user-contrib\"\n"; - print "COQTOPINSTALL=\"${COQLIB}toploop\"\n"; - print "\n" - | Project_file.UserInstall -> - section "Install Paths."; - print "XDG_DATA_HOME?=\"$(HOME)/.local/share\"\n"; - print "COQLIBINSTALL=$(XDG_DATA_HOME)/coq\n"; - print "COQDOCINSTALL=$(XDG_DATA_HOME)/doc/coq\n"; - print "COQTOPINSTALL=$(XDG_DATA_HOME)/coq/toploop\n"; - print "\n" - -let parameters () = - print ".DEFAULT_GOAL := all\n\n"; - print "# This Makefile may take arguments passed as environment variables:\n"; - print "# COQBIN to specify the directory where Coq binaries resides;\n"; - print "# TIMECMD set a command to log .v compilation time;\n"; - print "# TIMED if non empty, use the default time command as TIMECMD;\n"; - print "# ZDEBUG/COQDEBUG to specify debug flags for ocamlc&ocamlopt/coqc;\n"; - print "# DSTROOT to specify a prefix to install path.\n"; - print "# VERBOSE to disable the short display of compilation rules.\n\n"; - print "VERBOSE?=\n"; - print "SHOW := $(if $(VERBOSE),@true \"\",@echo \"\")\n"; - print "HIDE := $(if $(VERBOSE),,@)\n\n"; - print "# Here is a hack to make $(eval $(shell works:\n"; - print "define donewline\n\n\nendef\n"; - print "includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) | tr -d '\\r' | tr '\\n' '@'; })))\n"; - print "$(call includecmdwithout@,$(COQBIN)coqtop -config)\n\n"; - print "TIMED?=\nTIMECMD?=\nSTDTIME?=/usr/bin/time -f \"$* (user: %U mem: %M ko)\"\n"; - print "TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))\n\n"; - print "vo_to_obj = $(addsuffix .o,\\\n"; - print " $(filter-out Warning: Error:,\\\n"; - print " $(shell $(COQBIN)coqtop -q -noinit -batch -quiet -print-mod-uid $(1))))\n\n" - -let include_dirs (inc_ml,inc_q,inc_r) = - let parse_ml_includes l = List.map (fun (x,_) -> "-I \"" ^ x ^ "\"") l in - let includes = - List.map (fun (p,l,_) -> - let l' = if l = "" then "\"\"" else l in - " \"" ^ p ^ "\" " ^ l' ^"") in - let str_ml = parse_ml_includes inc_ml in - section "Libraries definitions."; - if !some_ml4file || !some_mlfile || !some_mlifile then begin - print "OCAMLLIBS?="; print_list "\\\n " str_ml; print "\n"; - end; - if !some_vfile || !some_mllibfile || !some_mlpackfile then begin - print "COQLIBS?="; - print_prefix_list "\\\n -Q" (includes inc_q); - print_prefix_list "\\\n -R" (includes inc_r); - print_prefix_list "\\\n " str_ml; - print "\n"; - end; - if !some_vfile then begin - print "COQCHKLIBS?="; - print_prefix_list "\\\n -R" (includes inc_q); - print_prefix_list "\\\n -R" (includes inc_r); - print "\n"; - print "COQDOCLIBS?="; - print_prefix_list "\\\n -R" (includes inc_q); - print_prefix_list "\\\n -R" (includes inc_r); - print "\n"; - end; - print "\n" - -let double_colon = ["clean"; "cleanall"; "archclean"] - -let custom sps = - let pr_path (file,dependencies,is_phony,com) = - print file; - print (if List.mem file double_colon then ":: " else ": "); - print dependencies; print "\n"; - if com <> "" then (print "\t"; print com; print "\n"); - print "\n" + fprintf oc "%s %s %s\n\t%s\n\n" + target + (if List.mem target clean_tgts then ":: " else ": ") + dependencies + command in - if sps <> [] then section "Custom targets."; + if sps <> [] then + section oc "Extra targets. (-extra and -extra-phony, DEPRECATED)"; List.iter pr_path sps -let subdirs sds = - let pr_subdir s = - print s; print ":\n\t+cd \""; print s; print "\" && $(MAKE) all\n\n" - in - if sds <> [] then - let () = - Format.eprintf "@[Warning: Targets for subdirectories are very fragile.@ " in - let () = - Format.eprintf "For example,@ nothing is done to handle dependencies@ with them.@]@." in - section "Subdirectories."; - List.iter pr_subdir sds - -let forpacks l = - let () = if l <> [] then section "Ad-hoc implicit rules for mlpack." in - List.iter (fun it -> - let h = Filename.chop_extension it in - let pk = String.capitalize (Filename.basename h) in - printf "$(addsuffix .cmx,$(filter $(basename $(MLFILES)),$(%s_MLPACK_DEPENDENCIES))): %%.cmx: %%.ml\n" h; - printf "\t$(SHOW)'CAMLOPT -c -for-pack %s $<'\n" pk; - printf "\t$(HIDE)$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -for-pack %s $<\n\n" pk; - printf "$(addsuffix .cmx,$(filter $(basename $(ML4FILES)),$(%s_MLPACK_DEPENDENCIES))): %%.cmx: %%.ml4\n" h; - printf "\t$(SHOW)'CAMLOPT -c -pp -for-pack %s $<'\n" pk; - printf "\t$(HIDE)$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -for-pack %s $(PP) -impl $<\n\n" pk - ) l - -let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other_targets inc = - let decl_var var = function - |[] -> () - |l -> - printf "%s:=" var; print_list "\\\n " l; print "\n\n"; - print "ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),)\n"; - printf "-include $(addsuffix .d,$(%s))\n" var; - print "else\nifeq ($(MAKECMDGOALS),)\n"; - printf "-include $(addsuffix .d,$(%s))\n" var; - print "endif\nendif\n\n"; - printf ".SECONDARY: $(addsuffix .d,$(%s))\n\n" var - in - section "Files dispatching."; - decl_var "VFILES" vfiles; - begin match vfiles with - |[] -> () - |l -> - print "VO=vo\n"; - print "VOFILES:=$(VFILES:.v=.$(VO))\n"; - classify_files_by_root "VOFILES" l inc; - classify_files_by_root "VFILES" l inc; - print "GLOBFILES:=$(VFILES:.v=.glob)\n"; - print "GFILES:=$(VFILES:.v=.g)\n"; - print "HTMLFILES:=$(VFILES:.v=.html)\n"; - print "GHTMLFILES:=$(VFILES:.v=.g.html)\n"; - print "OBJFILES=$(call vo_to_obj,$(VOFILES))\n"; - print "ALLNATIVEFILES=$(OBJFILES:.o=.cmi) $(OBJFILES:.o=.cmo) $(OBJFILES:.o=.cmx) $(OBJFILES:.o=.cmxs)\n"; - print "NATIVEFILES=$(foreach f, $(ALLNATIVEFILES), $(wildcard $f))\n"; - classify_files_by_root "NATIVEFILES" l inc - end; - decl_var "ML4FILES" ml4files; - decl_var "MLFILES" mlfiles; - decl_var "MLPACKFILES" mlpackfiles; - decl_var "MLLIBFILES" mllibfiles; - decl_var "MLIFILES" mlifiles; - let mlsfiles = match ml4files,mlfiles,mlpackfiles with - |[],[],[] -> [] - |[],[],_ -> Printf.eprintf "Mlpack cannot work without ml[4]?"; [] - |[],ml,[] -> - print "ALLCMOFILES:=$(MLFILES:.ml=.cmo)\n"; - ml - |ml4,[],[] -> - print "ALLCMOFILES:=$(ML4FILES:.ml4=.cmo)\n"; - ml4 - |ml4,ml,[] -> - print "ALLCMOFILES:=$(ML4FILES:.ml4=.cmo) $(MLFILES:.ml=.cmo)\n"; - List.rev_append ml ml4 - |[],ml,mlpack -> - print "ALLCMOFILES:=$(MLFILES:.ml=.cmo) $(MLPACKFILES:.mlpack=.cmo)\n"; - List.rev_append mlpack ml - |ml4,[],mlpack -> - print "ALLCMOFILES:=$(ML4FILES:.ml4=.cmo) $(MLPACKFILES:.mlpack=.cmo)\n"; - List.rev_append mlpack ml4 - |ml4,ml,mlpack -> - print "ALLCMOFILES:=$(ML4FILES:.ml4=.cmo) $(MLFILES:.ml=.cmo) $(MLPACKFILES:.mlpack=.cmo)\n"; - List.rev_append mlpack (List.rev_append ml ml4) in - begin match mlsfiles with - |[] -> () - |l -> - print "CMOFILES=$(filter-out $(addsuffix .cmo,$(foreach lib,$(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES) $(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(ALLCMOFILES))\n"; - classify_files_by_root "CMOFILES" l inc; - print "CMXFILES=$(CMOFILES:.cmo=.cmx)\n"; - print "OFILES=$(CMXFILES:.cmx=.o)\n"; - end; - begin match mllibfiles with - |[] -> () - |l -> - print "CMAFILES:=$(MLLIBFILES:.mllib=.cma)\n"; - classify_files_by_root "CMAFILES" l inc; - print "CMXAFILES:=$(CMAFILES:.cma=.cmxa)\n"; - end; - begin match mlifiles,mlsfiles with - |[],[] -> () - |l,[] -> - print "CMIFILES:=$(MLIFILES:.mli=.cmi)\n"; - classify_files_by_root "CMIFILES" l inc; - |[],l -> - print "CMIFILES=$(ALLCMOFILES:.cmo=.cmi)\n"; - classify_files_by_root "CMIFILES" l inc; - |l1,l2 -> - print "CMIFILES=$(sort $(ALLCMOFILES:.cmo=.cmi) $(MLIFILES:.mli=.cmi))\n"; - classify_files_by_root "CMIFILES" (l1@l2) inc; - end; - begin match mllibfiles,mlsfiles with - |[],[] -> () - |l,[] -> - print "CMXSFILES:=$(CMXAFILES:.cmxa=.cmxs)\n"; - classify_files_by_root "CMXSFILES" l inc; - |[],l -> - print "CMXSFILES=$(CMXFILES:.cmx=.cmxs)\n"; - classify_files_by_root "CMXSFILES" l inc; - |l1,l2 -> - print "CMXSFILES=$(CMXFILES:.cmx=.cmxs) $(CMXAFILES:.cmxa=.cmxs)\n"; - classify_files_by_root "CMXSFILES" (l1@l2) inc; - end; - print "ifeq '$(HASNATDYNLINK)' 'true'\n"; - print "HASNATDYNLINK_OR_EMPTY := yes\n"; - print "else\n"; - print "HASNATDYNLINK_OR_EMPTY :=\n"; - print "endif\n\n"; - section "Definition of the toplevel targets."; - print "all: "; - if !some_vfile then print "$(VOFILES) "; - if !some_mlfile || !some_ml4file || !some_mlpackfile then print "$(CMOFILES) "; - if !some_mllibfile then print "$(CMAFILES) "; - if !some_mlfile || !some_ml4file || !some_mllibfile || !some_mlpackfile - then print "$(if $(HASNATDYNLINK_OR_EMPTY),$(CMXSFILES)) "; - print_list "\\\n " other_targets; print "\n\n"; - if !some_mlifile then - begin - print "mlihtml: $(MLIFILES:.mli=.cmi)\n"; - print "\t mkdir $@ || rm -rf $@/*\n"; - print "\t$(OCAMLFIND) ocamldoc -html -safe-string -rectypes -d $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n"; - print "all-mli.tex: $(MLIFILES:.mli=.cmi)\n"; - print "\t$(OCAMLFIND) ocamldoc -latex -safe-string -rectypes -o $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n"; - end; - if !some_vfile then - begin - print "quick: $(VOFILES:.vo=.vio)\n\n"; - print "vio2vo:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio)\n"; - print "checkproofs:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio)\n"; - print "gallina: $(GFILES)\n\n"; - print "html: $(GLOBFILES) $(VFILES)\n"; - print "\t- mkdir -p html\n"; - print "\t$(COQDOC) -toc $(COQDOCFLAGS) -html $(COQDOCLIBS) -d html $(VFILES)\n\n"; - print "gallinahtml: $(GLOBFILES) $(VFILES)\n"; - print "\t- mkdir -p html\n"; - print "\t$(COQDOC) -toc $(COQDOCFLAGS) -html -g $(COQDOCLIBS) -d html $(VFILES)\n\n"; - print "all.ps: $(VFILES)\n"; - print "\t$(COQDOC) -toc $(COQDOCFLAGS) -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n"; - print "all-gal.ps: $(VFILES)\n"; - print "\t$(COQDOC) -toc $(COQDOCFLAGS) -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n"; - print "all.pdf: $(VFILES)\n"; - print "\t$(COQDOC) -toc $(COQDOCFLAGS) -pdf $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n"; - print "all-gal.pdf: $(VFILES)\n"; - print "\t$(COQDOC) -toc $(COQDOCFLAGS) -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n"; - print "validate: $(VOFILES)\n"; - print "\t$(COQCHK) $(COQCHKFLAGS) $(COQCHKLIBS) $(notdir $(^:.vo=))\n\n"; - print "beautify: $(VFILES:=.beautified)\n"; - print "\tfor file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done\n"; - print "\t@echo \'Do not do \"make clean\" until you are sure that everything went well!\'\n"; - print "\t@echo \'If there were a problem, execute \"for file in $$(find . -name \\*.v.old -print); do mv $${file} $${file%.old}; done\" in your shell/'\n\n" - end - -let all_target (vfiles, (_,_,_,_,mlpackfiles as mlfiles), sps, sds) inc = - let other_targets = - CList.map_filter - (fun (n,_,is_phony,_) -> if not (is_phony || is_genrule n) then Some n else None) - sps @ sds in - main_targets vfiles mlfiles other_targets inc; - print ".PHONY: "; - print_list - " " - ("all" :: "archclean" :: "beautify" :: "byte" :: "clean" :: "cleanall" - :: "gallina" :: "gallinahtml" :: "html" :: "install" :: "install-doc" - :: "install-natdynlink" :: "install-toploop" :: "opt" :: "printenv" - :: "quick" :: "uninstall" :: "userinstall" :: "validate" :: "vio2vo" - :: (sds@(CList.map_filter - (fun (n,_,is_phony,_) -> - if is_phony then Some n else None) sps))); - print "\n\n"; - custom sps; - subdirs sds; - forpacks mlpackfiles - -let banner () = - print (Printf.sprintf -"#############################################################################\ -\n## v # The Coq Proof Assistant ##\ -\n## <O___,, # INRIA - CNRS - LIX - LRI - PPS ##\ -\n## \\VV/ # ##\ -\n## // # Makefile automagically generated by coq_makefile V%s ##\ -\n#############################################################################\ -\n\n" -(Coq_config.version ^ String.make (10 - String.length Coq_config.version) ' ')) - -let warning () = - print "# WARNING\n#\n"; - print "# This Makefile has been automagically generated\n"; - print "# Edit at your own risks !\n"; - print "#\n# END OF WARNING\n\n" - -let print_list l = List.iter (fun x -> print x; print " ") l - -let command_line args = - print "#\n# This Makefile was generated by the command line :\n"; - print "# coq_makefile "; - print_list args; - print "\n#\n\n" - -let ensure_root_dir (vfiles,(mlis,ml4s,mls,mllibs,mlpacks),_,_) inc = - let (ml_inc,i_inc,r_inc) = inc in +let generate_conf_subdirs oc sds = + if sds <> [] then section oc "Subdirectories. (DEPRECATED)"; + List.iter (fprintf oc ".PHONY:%s\n") sds; + List.iter (fprintf oc "post-all::\n\tcd \"%s\" && $(MAKE) all\n") sds; + List.iter (fprintf oc "clean::\n\tcd \"%s\" && $(MAKE) clean\n") sds; + List.iter (fprintf oc "archclean::\n\tcd \"%s\" && $(MAKE) archclean\n") sds; + List.iter (fprintf oc "install-extra::\n\tcd \"%s\" && $(MAKE) install\n") sds + + +let generate_conf_includes oc { ml_includes; r_includes; q_includes } = + section oc "Path directives (-I, -R, -Q)."; + let module S = String in + let open List in + let dash1 opt v = sprintf "-%s %s" opt (quote v) in + let dash2 opt v1 v2 = sprintf "-%s %s %s" opt (quote v1) (quote v2) in + fprintf oc "COQMF_OCAMLLIBS = %s\n" + (S.concat " " (map (fun { path } -> dash1 "I" path) ml_includes)); + fprintf oc "COQMF_SRC_SUBDIRS = %s\n" + (S.concat " " (map (fun { path } -> quote path) ml_includes)); + fprintf oc "COQMF_COQLIBS = %s %s %s\n" + (S.concat " " (map (fun { path } -> dash1 "I" path) ml_includes)) + (S.concat " " (map (fun ({ path },l) -> dash2 "Q" path l) q_includes)) + (S.concat " " (map (fun ({ path },l) -> dash2 "R" path l) r_includes)); + fprintf oc "COQMF_COQLIBS_NOML = %s %s\n" + (S.concat " " (map (fun ({ path },l) -> dash2 "Q" path l) q_includes)) + (S.concat " " (map (fun ({ path },l) -> dash2 "R" path l) r_includes)) +;; + +let generate_conf_coq_config oc args = + section oc "Coq configuration."; + Envars.print_config ~prefix_var_name:"COQMF_" oc; + fprintf oc "COQMF_MAKEFILE=%s\n" (quote (List.hd args)); +;; + +let generate_conf_files oc + { v_files; mli_files; ml4_files; ml_files; mllib_files; mlpack_files } += + let module S = String in + let open List in + section oc "Project files."; + fprintf oc "COQMF_VFILES = %s\n" (S.concat " " (map quote v_files)); + fprintf oc "COQMF_MLIFILES = %s\n" (S.concat " " (map quote mli_files)); + fprintf oc "COQMF_MLFILES = %s\n" (S.concat " " (map quote ml_files)); + fprintf oc "COQMF_ML4FILES = %s\n" (S.concat " " (map quote ml4_files)); + fprintf oc "COQMF_MLPACKFILES = %s\n" (S.concat " " (map quote mlpack_files)); + fprintf oc "COQMF_MLLIBFILES = %s\n" (S.concat " " (map quote mllib_files)); +;; + +let rec all_start_with prefix = function + | [] -> true + | [] :: _ -> false + | (x :: _) :: rest -> x = prefix && all_start_with prefix rest + +let rec logic_gcd acc = function + | [] -> acc + | [] :: _ -> acc + | (hd :: tl) :: rest -> + if all_start_with hd rest + then logic_gcd (acc @ [hd]) (tl :: List.map List.tl rest) + else acc + +let generate_conf_doc oc { defs; q_includes; r_includes } = + let includes = List.map snd (q_includes @ r_includes) in + let logpaths = List.map (CString.split '.') includes in + let gcd = logic_gcd [] logpaths in + let root = + if gcd = [] then + if not (List.mem_assoc "INSTALLDEFAULTROOT" defs) then begin + let destination = "orphan_" ^ (String.concat "_" includes) in + eprintf "Warning: no common logical root\n"; + eprintf "Warning: in such case INSTALLDEFAULTROOT must be defined\n"; + eprintf "Warning: the install-doc target is going to install files\n"; + eprintf "Warning: in %s\n" destination; + destination + end else "$(INSTALLDEFAULTROOT)" + else String.concat "/" gcd in + Printf.fprintf oc "COQMF_INSTALLCOQDOCROOT = %s\n" (quote root) + +let generate_conf_defs oc { defs; extra_args } = + section oc "Extra variables."; + List.iter (fun (k,v) -> Printf.fprintf oc "%s = %s\n" k v) defs; + Printf.fprintf oc "COQMF_OTHERFLAGS = %s\n" + (String.concat " " extra_args) + +let generate_conf oc project args = + fprintf oc "# This configuration file was generated by running:\n"; + fprintf oc "# %s\n\n" (String.concat " " (List.map quote args)); + generate_conf_files oc project; + generate_conf_includes oc project; + generate_conf_coq_config oc args; + generate_conf_defs oc project; + generate_conf_doc oc project; + generate_conf_extra_target oc project.extra_targets; + generate_conf_subdirs oc project.subdirs; +;; + +let ensure_root_dir + ({ ml_includes; r_includes; + v_files; ml_files; mli_files; ml4_files; + mllib_files; mlpack_files } as project) += + let open List in let here = Sys.getcwd () in - let not_tops = List.for_all (fun s -> s <> Filename.basename s) in - if List.exists (fun (_,_,x) -> x = here) i_inc - || List.exists (fun (_,_,x) -> is_prefix x here) r_inc - || (not_tops vfiles && not_tops mlis && not_tops ml4s && not_tops mls - && not_tops mllibs && not_tops mlpacks) + let not_tops = List.for_all (fun s -> s <> Filename.basename s) in + if exists (fun { canonical_path = x } -> x = here) ml_includes + || exists (fun ({ canonical_path = x },_) -> is_prefix x here) r_includes + || (not_tops v_files && + not_tops mli_files && not_tops ml4_files && not_tops ml_files && + not_tops mllib_files && not_tops mlpack_files) then - inc + project else - ((".",here)::ml_inc,i_inc,(".","Top",here)::r_inc) - -let warn_install_at_root_directory (vfiles,(mlis,ml4s,mls,mllibs,mlpacks),_,_) inc = - let (inc_ml,inc_i,inc_r) = inc in - let inc_top = List.filter (fun (_,ldir,_) -> ldir = "") (inc_r@inc_i) in - let inc_top_p = List.map (fun (p,_,_) -> p) inc_top in - let files = vfiles @ mlis @ ml4s @ mls @ mllibs @ mlpacks in - if List.exists (fun f -> List.mem (Filename.dirname f) inc_top_p) files - then - Printf.eprintf "Warning: install target will copy files at the first level of the coq contributions installation directory; option -R or -Q %sis recommended\n" - (if inc_top = [] then "" else "with non trivial logical root ") + let here_path = { path = "."; canonical_path = here } in + { project with + ml_includes = here_path :: ml_includes; + r_includes = (here_path, "Top") :: r_includes } +;; + +let warn_install_at_root_directory + { q_includes; r_includes; + v_files; ml_files; mli_files; ml4_files; + mllib_files; mlpack_files } += + let open CList in + let inc_top_p = + map_filter + (fun ({ path } ,ldir) -> if ldir = "" then Some path else None) + (r_includes @ q_includes) in + let files = + v_files @ mli_files @ ml4_files @ ml_files @ mllib_files @ mlpack_files in + let bad = filter (fun f -> mem (Filename.dirname f) inc_top_p) files in + if bad <> [] then begin + eprintf "Warning: No file should be installed at the root of Coq's library.\n"; + eprintf "Warning: No logical path (-R, -Q) applies to these files:\n"; + List.iter (fun x -> eprintf "Warning: %s\n" x) bad; + eprintf "\n"; + end +;; -let check_overlapping_include (_,inc_i,inc_r) = +let check_overlapping_include { q_includes; r_includes } = let pwd = Sys.getcwd () in let aux = function | [] -> () - | (pdir,_,abspdir)::l -> - if not (is_prefix pwd abspdir) then - Printf.eprintf "Warning: in option -R/-Q, %s is not a subdirectory of the current directory\n" pdir; - List.iter (fun (pdir',_,abspdir') -> - if is_prefix abspdir abspdir' || is_prefix abspdir' abspdir then - Printf.eprintf "Warning: in options -R/-Q, %s and %s overlap\n" pdir pdir') l; - in aux (inc_i@inc_r) - -(* Generate a .merlin file that references the standard library and - * any -I included paths. - *) -let merlin targets (ml_inc,_,_) = - print ".merlin:\n"; - print "\t@echo 'FLG -rectypes -safe-string' > .merlin\n" ; - List.iter (fun c -> - printf "\t@echo \"B $(COQLIB)%s\" >> .merlin\n" c) - lib_dirs ; - List.iter (fun (_,c) -> - printf "\t@echo \"B %s\" >> .merlin\n" c; - printf "\t@echo \"S %s\" >> .merlin\n" c) - ml_inc; - print "\n" - -let do_makefile args = - let has_file var = function - |[] -> var := false - |_::_ -> var := true in - let (project_file,makefile,is_install,opt),l = - try - Project_file.process_cmd_line Filename.current_dir_name - (None,None,Project_file.UnspecInstall,true) [] args - with Project_file.Parsing_error -> usage () in - let (v_f,(mli_f,ml4_f,ml_f,mllib_f,mlpack_f),sps,sds as targets), inc, defs = - Project_file.split_arguments l in - - let () = match project_file with |None -> () |Some f -> make_name := f in - let () = match makefile with - |None -> () - |Some f -> makefile_name := f; output_channel := open_out f in - has_file some_vfile v_f; has_file some_mlifile mli_f; - has_file some_mlfile ml_f; has_file some_ml4file ml4_f; - has_file some_mllibfile mllib_f; has_file some_mlpackfile mlpack_f; - let check_dep f = - if Filename.check_suffix f ".v" then some_vfile := true - else if (Filename.check_suffix f ".mli") then some_mlifile := true - else if (Filename.check_suffix f ".ml4") then some_ml4file := true - else if (Filename.check_suffix f ".ml") then some_mlfile := true - else if (Filename.check_suffix f ".mllib") then some_mllibfile := true - else if (Filename.check_suffix f ".mlpack") then some_mlpackfile := true + | ({ path; canonical_path }, _) :: l -> + if not (is_prefix pwd canonical_path) then + eprintf "Warning: %s (used in -R or -Q) is not a subdirectory of the current directory\n\n" path; + List.iter (fun ({ path = p; canonical_path = cp }, _) -> + if is_prefix canonical_path cp || is_prefix cp canonical_path then + eprintf "Warning: %s and %s overlap (used in -R or -Q)\n\n" + path p) l in - List.iter (fun (_,dependencies,_,_) -> - List.iter check_dep (Str.split (Str.regexp "[ \t]+") dependencies)) sps; + aux (q_includes @ r_includes) +;; + +let chop_prefix p f = + let len_p = String.length p in + let len_f = String.length f in + String.sub f len_p (len_f - len_p) + +let clean_path p = + Str.global_replace (Str.regexp_string "//") "/" p + +let destination_of { ml_includes; q_includes; r_includes; } file = + let file_dir = CUnix.canonical_path_name (Filename.dirname file) in + let includes = q_includes @ r_includes in + let mk_destination logic canonical_path = + clean_path (physical_dir_of_logical_dir logic ^ "/" ^ + chop_prefix canonical_path file_dir ^ "/") in + let candidates = + CList.map_filter (fun ({ canonical_path }, logic) -> + if is_prefix canonical_path file_dir then + Some(mk_destination logic canonical_path) + else None) includes + in + match candidates with + | [] -> + (* BACKWARD COMPATIBILITY: -I into the only logical root *) + begin match + r_includes, + List.find (fun { canonical_path = p } -> is_prefix p file_dir) + ml_includes + with + | [{ canonical_path }, logic], { canonical_path = p } -> + let destination = + clean_path (physical_dir_of_logical_dir logic ^ "/" ^ + chop_prefix p file_dir ^ "/") in + Printf.printf "%s" (quote destination) + | _ -> () (* skip *) + | exception Not_found -> () (* skip *) + end + | [s] -> Printf.printf "%s" (quote s) + | _ -> assert false + +let share_prefix s1 s2 = + let s1 = CString.split '.' s1 in + let s2 = CString.split '.' s2 in + match s1, s2 with + | x :: _ , y :: _ -> x = y + | _ -> false + +let _ = + let prog, args = + if Array.length Sys.argv = 1 then usage (); + let args = Array.to_list Sys.argv in + let prog = List.hd args in + prog, List.tl args in - let inc = ensure_root_dir targets inc in - if is_install <> Project_file.NoInstall then begin - warn_install_at_root_directory targets inc; + let only_destination, args = match args with + | "-destination-of" :: tgt :: rest -> Some tgt, rest + | _ -> None, args in + + let project = + try cmdline_args_to_project ~curdir:Filename.current_dir_name args + with Parsing_error s -> prerr_endline s; usage () in + + if only_destination <> None then begin + destination_of project (Option.get only_destination); + exit 0 + end; + + if project.makefile = None then + eprintf "Warning: Omitting -o is deprecated\n\n"; + (* We want to know the name of the Makefile (say m) in order to + * generate m.conf and include m.local *) + + let conf_file = Option.default "CoqMakefile" project.makefile ^ ".conf" in + let local_file = Option.default "CoqMakefile" project.makefile ^ ".local" in + + if project.extra_targets <> [] then begin + eprintf "Warning: -extra and -extra-phony are deprecated.\n"; + eprintf "Warning: Write the extra targets in %s.\n\n" local_file; + end; + + if project.subdirs <> [] then begin + eprintf "Warning: Subdirectories are deprecated.\n"; + eprintf "Warning: Use double colon rules in %s.\n\n" local_file; end; - check_overlapping_include inc; - banner (); - header_includes (); - warning (); - command_line args; - parameters (); - include_dirs inc; - variables is_install opt defs; - all_target targets inc; - section "Special targets."; - standard opt; - install targets inc is_install; - merlin targets inc; - clean sds sps; - make_makefile sds; - implicit (); - warning (); - if not (makefile = None) then close_out !output_channel; + + let project = ensure_root_dir project in + + if project.install_kind <> (Some CoqProject_file.NoInstall) then begin + warn_install_at_root_directory project; + end; + + check_overlapping_include project; + + Envars.set_coqlib ~fail:(fun x -> x); + + let ocm = Option.cata open_out stdout project.makefile in + generate_makefile ocm conf_file local_file (prog :: args) project; + close_out ocm; + let occ = open_out conf_file in + generate_conf occ project (prog :: args); + close_out occ; exit 0 -let _ = - let args = - if Array.length Sys.argv = 1 then usage (); - List.tl (Array.to_list Sys.argv) - in - do_makefile args diff --git a/tools/coqc.ml b/tools/coqc.ml index 552a943c8..9857d4318 100644 --- a/tools/coqc.ml +++ b/tools/coqc.ml @@ -83,8 +83,11 @@ let parse_args () = | ("-config" | "--config") :: _ -> Envars.set_coqlib ~fail:(fun x -> x); - Usage.print_config (); + Envars.print_config stdout; exit 0 + + |"--print-version" :: _ -> + Usage.machine_readable_version 0 (* Options for coqtop : a) options with 0 argument *) diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 1c1c1be6a..930b092d3 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -435,7 +435,7 @@ let usage () = ML Module\" commands in coq files.\n"; *) (* Does not work anymore: *) (* eprintf " -D : Prints the missing ocmal module names. No dependency computed.\n"; *) - eprintf " -boot : For coq developpers, prints dependencies over coq library files (omitted by default).\n"; + eprintf " -boot : For coq developers, prints dependencies over coq library files (omitted by default).\n"; eprintf " -sort : output the given file name ordered by dependencies\n"; eprintf " -noglob | -no-glob : \n"; eprintf " -I dir -as logname : add (non recursively) dir to coq load path under logical name logname\n"; diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 93b25e2ed..6e7935d09 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -219,7 +219,6 @@ let register_dir_logpath,find_dir_logpath = let file_name s = function | None -> s - | Some "." -> s | Some d -> d // s let depend_ML str = @@ -293,15 +292,15 @@ let traite_fichier_modules md ext = (fun a_faire str -> match search_mlpack_known str with | Some mldir -> let file = file_name str mldir in - a_faire^" "^file + a_faire @ [file] | None -> match search_ml_known str with | Some mldir -> let file = file_name str mldir in - a_faire^" "^file - | None -> a_faire) "" list + a_faire @ [file] + | None -> a_faire) [] list with - | Sys_error _ -> "" + | Sys_error _ -> [] | Syntax_error (i,j) -> error_cannot_parse (md^ext) (i,j) (* Makefile's escaping rules are awful: $ is escaped by doubling and @@ -443,7 +442,7 @@ let mL_dependencies () = let fullname = file_name name dirname in let dep = traite_fichier_modules fullname ".mllib" in let efullname = escape fullname in - printf "%s_MLLIB_DEPENDENCIES:=%s\n" efullname dep; + printf "%s_MLLIB_DEPENDENCIES:=%s\n" efullname (String.concat " " dep); printf "%s.cma:$(addsuffix .cmo,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname; printf "%s.cmxa:$(addsuffix .cmx,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname; flush stdout) @@ -453,9 +452,13 @@ let mL_dependencies () = let fullname = file_name name dirname in let dep = traite_fichier_modules fullname ".mlpack" in let efullname = escape fullname in - printf "%s_MLPACK_DEPENDENCIES:=%s\n" efullname dep; + printf "%s_MLPACK_DEPENDENCIES:=%s\n" efullname (String.concat " " dep); printf "%s.cmo:$(addsuffix .cmo,$(%s_MLPACK_DEPENDENCIES))\n" efullname efullname; printf "%s.cmx:$(addsuffix .cmx,$(%s_MLPACK_DEPENDENCIES))\n" efullname efullname; + let efullname_capital = String.capitalize (Filename.basename efullname) in + List.iter (fun dep -> + printf "%s.cmx : FOR_PACK=-for-pack %s\n" dep efullname_capital) + dep; flush stdout) (List.rev !mlpackAccu) |