diff options
Diffstat (limited to 'tools/CoqMakefile.in')
| -rw-r--r-- | tools/CoqMakefile.in | 623 |
1 files changed, 623 insertions, 0 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in new file mode 100644 index 000000000..0145dd51f --- /dev/null +++ b/tools/CoqMakefile.in @@ -0,0 +1,623 @@ +############################################################################### +## 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?=/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), $(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)) +uniform_dotslash = $(addprefix ./,$(call strip_dotslash,$(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 uniform_dotslash, \ + $(foreach lib, \ + $(call strip_dotslash, \ + $(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES)),$($(lib)))) +# files that are archived into a .cma (mllib) +LIBEDFILES = \ + $(call uniform_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 + +# 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:: + @# Extension point + $(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 +.PHONY: install + +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 + |