aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
Diffstat (limited to 'tools')
-rw-r--r--tools/CoqMakefile.in658
-rw-r--r--tools/coq_makefile.ml1253
-rw-r--r--tools/coqc.ml10
-rw-r--r--tools/coqdep.ml32
-rw-r--r--tools/coqdep_boot.ml6
-rw-r--r--tools/coqdep_common.ml48
-rw-r--r--tools/coqdep_common.mli8
-rw-r--r--tools/coqdep_lexer.mll10
-rw-r--r--tools/coqdoc/alpha.ml19
-rw-r--r--tools/coqdoc/cdglobals.ml24
-rw-r--r--tools/coqdoc/cdglobals.mli49
-rw-r--r--tools/coqdoc/index.ml18
-rw-r--r--tools/coqdoc/output.ml18
-rw-r--r--tools/coqdoc/output.mli1
-rw-r--r--tools/coqmktop.ml27
-rw-r--r--tools/coqwc.mll2
-rw-r--r--tools/coqworkmgr.ml9
-rw-r--r--tools/fake_ide.ml43
-rw-r--r--tools/gallina-syntax.el4
-rw-r--r--tools/gallina_lexer.mll1
-rw-r--r--tools/ocamllibdep.mll12
21 files changed, 1228 insertions, 1024 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
new file mode 100644
index 0000000000..5e223a0b48
--- /dev/null
+++ b/tools/CoqMakefile.in
@@ -0,0 +1,658 @@
+###############################################################################
+## 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)
+
+@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?=
+
+# The DYNOBJ and DYNLIB variables are used by "coqdep -dyndep var" in .v.d
+ifeq '$(OPT)' '-byte'
+USEBYTE:=true
+DYNOBJ:=.cmo
+DYNLIB:=.cma
+else
+USEBYTE:=
+DYNOBJ:=.cmxs
+DYNLIB:=.cmxs
+endif
+
+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) $(MLPACKFILES:.mlpack=.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=.cmx) \
+ $(OBJFILES:.o=.cmxs)
+# trick: wildcard filters out non-existing files
+NATIVEFILESTOINSTALL = $(foreach f, $(ALLNATIVEFILES), $(wildcard $f))
+FILESTOINSTALL = \
+ $(VOFILES) \
+ $(VFILES) \
+ $(GLOBFILES) \
+ $(NATIVEFILESTOINSTALL) \
+ $(CMIFILESTOINSTALL)
+BYTEFILESTOINSTALL = \
+ $(CMOFILESTOINSTALL) \
+ $(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) $(if $(USEBYTE),bytefiles,optfiles)
+.PHONY: real-all
+
+bytefiles: $(CMOFILES) $(CMAFILES)
+.PHONY: bytefiles
+
+optfiles: $(if $(DO_NATDYNLINK),$(CMXSFILES))
+.PHONY: optfiles
+
+# 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-byte:
+ $(HIDE)for f in $(BYTEFILESTOINSTALL); 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-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 "$(DESTDIR)$(COQLIBINSTALL)/$$df/" || true; \
+ 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 "$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/" || true
+.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=.cma): %.cma: %.cmo | %.mlpack
+ $(SHOW)'CAMLC -a -o $@'
+ $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -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) -dyndep var -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 b7dd5f2a14..e4f1359774 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,85 +27,56 @@ 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"; "ltacprof";
- "toplevel"; "stm"; "grammar"; "config";
- "ltac"; "engine"]
-
-
let usage () =
- output_string stderr "Usage summary:
-
-coq_makefile .... [file.v] ... [file.ml[i4]?] ... [file.ml{lib,pack}]
- ... [any] ... [-extra[-phony] result dependencies command]
- ... [-I dir] ... [-R physicalpath logicalpath]
- ... [-Q physicalpath logicalpath] ... [VARIABLE = value]
- ... [-arg opt] ... [-opt|-byte] [-no-install] [-f file] [-o file]
- [-h] [--help]
-
-[file.v]: Coq file to be compiled
-[file.ml[i4]?]: Objective Caml file to be compiled
-[file.ml{lib,pack}]: ocamlbuild file that describes a Objective Caml
- library/module
-[any] : subdirectory that should be \"made\" and has a Makefile itself
- to do so. Very fragile and discouraged.
-[-extra result dependencies command]: add target \"result\" with command
- \"command\" and dependencies \"dependencies\". If \"result\" is not
- generic (do not contains a %), \"result\" is built by _make all_ and
- deleted by _make clean_.
-[-extra-phony result dependencies command]: add a PHONY target \"result\"
- with command \"command\" and dependencies \"dependencies\". Note that
- _-extra-phony foo bar \"\"_ is a regular way to add the target \"bar\" as
- as a dependencies of an already defined target \"foo\".
-[-I dir]: look for Objective Caml dependencies in \"dir\"
-[-R physicalpath logicalpath]: look for Coq dependencies resursively
- starting from \"physicalpath\". The logical path associated to the
- physical path is \"logicalpath\".
-[-Q physicalpath logicalpath]: look for Coq dependencies starting from
- \"physicalpath\". The logical path associated to the physical path
- is \"logicalpath\".
-[VARIABLE = value]: Add the variable definition \"VARIABLE=value\"
-[-byte]: compile with byte-code version of coq
-[-opt]: compile with native-code version of coq
-[-arg opt]: send option \"opt\" to coqc
-[-install opt]: where opt is \"user\" to force install into user directory,
- \"none\" to build a makefile with no install target or
- \"global\" to force install in $COQLIB directory
-[-f file]: take the contents of file as arguments
-[-o file]: output should go in file file
- Output file outside the current directory is forbidden.
-[-h]: print this usage summary
-[--help]: equivalent to [-h]\n";
+ output_string stderr "Usage summary:\
+\n\
+\ncoq_makefile .... [file.v] ... [file.ml[i4]?] ... [file.ml{lib,pack}]\
+\n ... [any] ... [-extra[-phony] result dependencies command]\
+\n ... [-I dir] ... [-R physicalpath logicalpath]\
+\n ... [-Q physicalpath logicalpath] ... [VARIABLE = value]\
+\n ... [-arg opt] ... [-opt|-byte] [-no-install] [-f file] [-o file]\
+\n [-h] [--help]\
+\n\
+\n[file.v]: Coq file to be compiled\
+\n[file.ml[i4]?]: Objective Caml file to be compiled\
+\n[file.ml{lib,pack}]: ocamlbuild file that describes a Objective Caml\
+\n library/module\
+\n[any] : subdirectory that should be \"made\" and has a Makefile itself\
+\n to do so. Very fragile and discouraged.\
+\n[-extra result dependencies command]: add target \"result\" with command\
+\n \"command\" and dependencies \"dependencies\". If \"result\" is not\
+\n generic (do not contains a %), \"result\" is built by _make all_ and\
+\n deleted by _make clean_.\
+\n[-extra-phony result dependencies command]: add a PHONY target \"result\"\
+\n with command \"command\" and dependencies \"dependencies\". Note that\
+\n _-extra-phony foo bar \"\"_ is a regular way to add the target \"bar\" as\
+\n as a dependencies of an already defined target \"foo\".\
+\n[-I dir]: look for Objective Caml dependencies in \"dir\"\
+\n[-R physicalpath logicalpath]: look for Coq dependencies resursively\
+\n starting from \"physicalpath\". The logical path associated to the\
+\n physical path is \"logicalpath\".\
+\n[-Q physicalpath logicalpath]: look for Coq dependencies starting from\
+\n \"physicalpath\". The logical path associated to the physical path\
+\n is \"logicalpath\".\
+\n[VARIABLE = value]: Add the variable definition \"VARIABLE=value\"\
+\n[-byte]: compile with byte-code version of coq\
+\n[-opt]: compile with native-code version of coq\
+\n[-arg opt]: send option \"opt\" to coqc\
+\n[-install opt]: where opt is \"user\" to force install into user directory,\
+\n \"none\" to build a makefile with no install target or\
+\n \"global\" to force install in $COQLIB directory\
+\n[-f file]: take the contents of file as arguments\
+\n[-o file]: output should go in file file\
+\n Output file outside the current directory is forbidden.\
+\n[-bypass-API]: when compiling plugins, bypass Coq API\
+\n[-h]: print this usage summary\
+\n[--help]: equivalent to [-h]\n";
exit 1
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,836 +89,338 @@ 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 String.copy ldir
+ if le >= 0 && Bytes.get ldir le = '.' then Bytes.sub ldir 0 (le - 1)
+ else Bytes.copy ldir
in
for i = 0 to le - 1 do
- if pdir.[i] = '.' then pdir.[i] <- '/';
+ if Bytes.get pdir i = '.' then Bytes.set pdir i '/';
done;
- 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
- 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";
+ 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 template = "/tools/CoqMakefile.in" in
+ Coq_config.coqlib ^ 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"
+ fprintf oc "%s %s %s\n\t%s\n\n"
+ target
+ (if List.mem target clean_tgts then ":: " else ": ")
+ dependencies
+ command
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 " \\
- -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\n";
- print "CAMLOPTC?=$(OCAMLFIND) opt -c -rectypes -thread\n";
- print "CAMLLINK?=$(OCAMLFIND) ocamlc -rectypes -thread\n";
- print "CAMLOPTLINK?=$(OCAMLFIND) opt -rectypes -thread\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 "ifeq ($(CAMLP4),camlp5)
-CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo
-else
-CAMLP4EXTEND=
-endif\n";
- print "PP?=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(COQLIB)/grammar compat5.cmo \\
- $(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"
- 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;
- 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 -rectypes -d $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n";
- print "all-mli.tex: $(MLIFILES:.mli=.cmi)\n";
- print "\t$(OCAMLFIND) ocamldoc -latex -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
-"#############################################################################
-## v # The Coq Proof Assistant ##
-## <O___,, # INRIA - CNRS - LIX - LRI - PPS ##
-## \\VV/ # ##
-## // # Makefile automagically generated by coq_makefile V%s ##
-#############################################################################
-
-" (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 bypass_API =
+ section oc "Coq configuration.";
+ let src_dirs = if bypass_API
+ then Coq_config.all_src_dirs
+ else Coq_config.api_dirs @ Coq_config.plugins_dirs in
+ Envars.print_config ~prefix_var_name:"COQMF_" oc src_dirs;
+ 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 project.bypass_API;
+ 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' > .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
+ 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
- List.iter (fun (_,dependencies,_,_) ->
- List.iter check_dep (Str.split (Str.regexp "[ \t]+") dependencies)) sps;
+ 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 b12d48710f..c1f0182d9c 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -77,14 +77,17 @@ let parse_args () =
| ("-v"|"--version") :: _ -> Usage.version 0
| ("-where") :: _ ->
- Envars.set_coqlib (fun x -> x);
+ Envars.set_coqlib ~fail:(fun x -> x);
print_endline (Envars.coqlib ());
exit 0
| ("-config" | "--config") :: _ ->
- Envars.set_coqlib (fun x -> x);
- Usage.print_config ();
+ Envars.set_coqlib ~fail:(fun x -> x);
+ Envars.print_config stdout Coq_config.all_src_dirs;
exit 0
+
+ |"--print-version" :: _ ->
+ Usage.machine_readable_version 0
(* Options for coqtop : a) options with 0 argument *)
@@ -96,6 +99,7 @@ let parse_args () =
|"-impredicative-set"|"-vm"|"-native-compiler"
|"-indices-matter"|"-quick"|"-type-in-type"
|"-async-proofs-always-delegate"|"-async-proofs-never-reopen-branch"
+ |"-stm-debug"
as o) :: rem ->
parse (cfiles,o::args) rem
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index a7c32e1d65..cba9c3eb07 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -320,19 +320,25 @@ let treat_coq_file chan =
List.fold_left (fun accu v -> mark_v_done from accu v) acc strl
| Declare sl ->
let declare suff dir s =
- let base = file_name s dir in
- let opt = if !option_natdynlk then " " ^ base ^ ".cmxs" else "" in
- (escape base, suff ^ opt)
+ let base = escape (file_name s dir) in
+ match !option_dynlink with
+ | No -> []
+ | Byte -> [base,suff]
+ | Opt -> [base,".cmxs"]
+ | Both -> [base,suff; base,".cmxs"]
+ | Variable ->
+ if suff=".cmo" then [base,"$(DYNOBJ)"]
+ else [base,"$(DYNLIB)"]
in
let decl acc str =
let s = basename_noext str in
if not (StrSet.mem s !deja_vu_ml) then
let () = deja_vu_ml := StrSet.add s !deja_vu_ml in
match search_mllib_known s with
- | Some mldir -> (declare ".cma" mldir s) :: acc
+ | Some mldir -> (declare ".cma" mldir s) @ acc
| None ->
match search_ml_known s with
- | Some mldir -> (declare ".cmo" mldir s) :: acc
+ | Some mldir -> (declare ".cmo" mldir s) @ acc
| None -> acc
else acc
in
@@ -435,7 +441,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";
@@ -449,6 +455,7 @@ let usage () =
eprintf " -coqlib dir : set the coq standard library directory\n";
eprintf " -suffix s : \n";
eprintf " -slash : deprecated, no effect\n";
+ eprintf " -dyndep (opt|byte|both|no|var) : set how dependencies over ML modules are printed";
exit 1
let split_period = Str.split (Str.regexp (Str.quote "."))
@@ -476,17 +483,22 @@ let rec parse = function
| "-slash" :: ll ->
Printf.eprintf "warning: option -slash has no effect and is deprecated.\n";
parse ll
+ | "-dyndep" :: "no" :: ll -> option_dynlink := No; parse ll
+ | "-dyndep" :: "opt" :: ll -> option_dynlink := Opt; parse ll
+ | "-dyndep" :: "byte" :: ll -> option_dynlink := Byte; parse ll
+ | "-dyndep" :: "both" :: ll -> option_dynlink := Both; parse ll
+ | "-dyndep" :: "var" :: ll -> option_dynlink := Variable; parse ll
| ("-h"|"--help"|"-help") :: _ -> usage ()
| f :: ll -> treat_file None f; parse ll
| [] -> ()
let coqdep () =
if Array.length Sys.argv < 2 then usage ();
+ if not Coq_config.has_natdynlink then option_dynlink := No;
parse (List.tl (Array.to_list Sys.argv));
(* Add current dir with empty logical path if not set by options above. *)
(try ignore (Coqdep_common.find_dir_logpath (Sys.getcwd()))
with Not_found -> add_norec_dir_import add_known "." []);
- if not Coq_config.has_natdynlink then option_natdynlk := false;
(* NOTE: These directories are searched from last to first *)
if !option_boot then begin
add_rec_dir_import add_known "theories" ["Coq"];
@@ -495,14 +507,14 @@ let coqdep () =
add_rec_dir_import (fun _ -> add_caml_known) "theories" ["Coq"];
add_rec_dir_import (fun _ -> add_caml_known) "plugins" ["Coq"];
end else begin
- Envars.set_coqlib ~fail:CErrors.error;
+ Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg));
let coqlib = Envars.coqlib () in
add_rec_dir_import add_coqlib_known (coqlib//"theories") ["Coq"];
add_rec_dir_import add_coqlib_known (coqlib//"plugins") ["Coq"];
let user = coqlib//"user-contrib" in
if Sys.file_exists user then add_rec_dir_no_import add_coqlib_known user [];
List.iter (fun s -> add_rec_dir_no_import add_coqlib_known s [])
- (Envars.xdg_dirs (fun x -> Feedback.msg_warning (Pp.str x)));
+ (Envars.xdg_dirs ~warn:(fun x -> Feedback.msg_warning (Pp.str x)));
List.iter (fun s -> add_rec_dir_no_import add_coqlib_known s []) Envars.coqpath;
end;
List.iter (fun (f,d) -> add_mli_known f d ".mli") !mliAccu;
@@ -526,5 +538,5 @@ let _ =
try
coqdep ()
with CErrors.UserError(s,p) ->
- let pp = if s <> "_" then Pp.(str s ++ str ": " ++ p) else p in
+ let pp = (match s with | None -> p | Some s -> Pp.(str s ++ str ": " ++ p)) in
Feedback.msg_error pp
diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml
index 6fc826833e..25f62d2bec 100644
--- a/tools/coqdep_boot.ml
+++ b/tools/coqdep_boot.ml
@@ -16,7 +16,11 @@ open Coqdep_common
*)
let rec parse = function
- | "-natdynlink" :: "no" :: ll -> option_natdynlk := false; parse ll
+ | "-dyndep" :: "no" :: ll -> option_dynlink := No; parse ll
+ | "-dyndep" :: "opt" :: ll -> option_dynlink := Opt; parse ll
+ | "-dyndep" :: "byte" :: ll -> option_dynlink := Byte; parse ll
+ | "-dyndep" :: "both" :: ll -> option_dynlink := Both; parse ll
+ | "-dyndep" :: "var" :: ll -> option_dynlink := Variable; parse ll
| "-c" :: ll -> option_c := true; parse ll
| "-boot" :: ll -> parse ll (* We're already in boot mode by default *)
| "-mldep" :: ocamldep :: ll ->
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 0064aebdae..bf8bcd0c44 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -15,7 +15,7 @@ open Minisys
behavior is the one of [coqdep -boot]. Its only dependencies
are [Coqdep_lexer], [Unix] and [Minisys], and it should stay so.
If it need someday some additional information, pass it via
- options (see for instance [option_natdynlk] below).
+ options (see for instance [option_dynlink] below).
*)
module StrSet = Set.Make(String)
@@ -26,9 +26,11 @@ module StrListMap = Map.Make(StrList)
let stderr = Pervasives.stderr
let stdout = Pervasives.stdout
+type dynlink = Opt | Byte | Both | No | Variable
+
let option_c = ref false
let option_noglob = ref false
-let option_natdynlk = ref true
+let option_dynlink = ref Both
let option_boot = ref false
let option_mldep = ref None
@@ -36,6 +38,10 @@ let norec_dirs = ref StrSet.empty
let suffixe = ref ".vo"
+[@@@ocaml.warning "-3"] (* String.capitalize_ascii since 4.03.0 GPR#124 *)
+let capitalize = String.capitalize
+[@@@ocaml.warning "+3"]
+
type dir = string option
(** [get_extension f l] checks whether [f] has one of the extensions
@@ -219,7 +225,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 +298,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
@@ -380,10 +385,16 @@ let rec traite_fichier_Coq suffixe verbose f =
end) strl
| Declare sl ->
let declare suff dir s =
- let base = file_name s dir in
- let opt = if !option_natdynlk then " "^base^".cmxs" else "" in
- printf " %s%s%s" (escape base) suff opt
- in
+ let base = escape (file_name s dir) in
+ match !option_dynlink with
+ | No -> ()
+ | Byte -> printf " %s%s" base suff
+ | Opt -> printf " %s.cmxs" base
+ | Both -> printf " %s%s %s.cmxs" base suff base
+ | Variable ->
+ printf " %s%s" base
+ (if suff=".cmo" then "$(DYNOBJ)" else "$(DYNLIB)")
+ in
let decl str =
let s = basename_noext str in
if not (StrSet.mem s !deja_vu_ml) then begin
@@ -443,7 +454,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 +464,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 = 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)
@@ -544,13 +559,6 @@ let add_rec_dir_no_import add_file phys_dir log_dir =
let add_rec_dir_import add_file phys_dir log_dir =
add_directory true (add_file true) phys_dir log_dir
-(** -R semantic but only on immediate capitalized subdirs *)
-
-let add_rec_uppercase_subdirs add_file phys_dir log_dir =
- process_subdirectories (fun phys_dir f ->
- add_directory true (add_file true) phys_dir (log_dir@[String.capitalize f]))
- phys_dir
-
(** -I semantic: do not go in subdirs. *)
let add_caml_dir phys_dir =
add_directory false add_caml_known phys_dir []
diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli
index 633c474ada..8c1787d315 100644
--- a/tools/coqdep_common.mli
+++ b/tools/coqdep_common.mli
@@ -19,7 +19,10 @@ val find_dir_logpath: string -> string list
val option_c : bool ref
val option_noglob : bool ref
val option_boot : bool ref
-val option_natdynlk : bool ref
+
+type dynlink = Opt | Byte | Both | No | Variable
+
+val option_dynlink : dynlink ref
val option_mldep : string option ref
val norec_dirs : StrSet.t ref
val suffixe : string ref
@@ -64,8 +67,5 @@ val add_rec_dir_no_import :
val add_rec_dir_import :
(bool -> string -> string list -> string -> unit) -> string -> string list -> unit
-val add_rec_uppercase_subdirs :
- (bool -> string -> string list -> string -> unit) -> string -> string list -> unit
-
val treat_file : dir -> string -> unit
val error_cannot_parse : string -> int * int -> 'a
diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll
index eb233b8f94..c68c34bbbd 100644
--- a/tools/coqdep_lexer.mll
+++ b/tools/coqdep_lexer.mll
@@ -39,6 +39,10 @@
let syntax_error lexbuf =
raise (Syntax_error (Lexing.lexeme_start lexbuf, Lexing.lexeme_end lexbuf))
+
+ [@@@ocaml.warning "-3"] (* String.uncapitalize_ascii since 4.03.0 GPR#124 *)
+ let uncapitalize = String.uncapitalize
+ [@@@ocaml.warning "+3"]
}
let space = [' ' '\t' '\n' '\r']
@@ -154,7 +158,7 @@ and caml_action = parse
| space +
{ caml_action lexbuf }
| "open" space* (caml_up_ident as id)
- { Use_module (String.uncapitalize id) }
+ { Use_module (uncapitalize id) }
| "module" space+ caml_up_ident
{ caml_action lexbuf }
| caml_low_ident { caml_action lexbuf }
@@ -321,12 +325,12 @@ and modules mllist = parse
and qual_id ml_module_name = parse
| '.' [^ '.' '(' '[']
- { Use_module (String.uncapitalize ml_module_name) }
+ { Use_module (uncapitalize ml_module_name) }
| eof { raise Fin_fichier }
| _ { caml_action lexbuf }
and mllib_list = parse
- | caml_up_ident { let s = String.uncapitalize (Lexing.lexeme lexbuf)
+ | caml_up_ident { let s = uncapitalize (Lexing.lexeme lexbuf)
in s :: mllib_list lexbuf }
| "*predef*" { mllib_list lexbuf }
| space+ { mllib_list lexbuf }
diff --git a/tools/coqdoc/alpha.ml b/tools/coqdoc/alpha.ml
index f817ed5a2a..6a6db95567 100644
--- a/tools/coqdoc/alpha.ml
+++ b/tools/coqdoc/alpha.ml
@@ -8,7 +8,11 @@
open Cdglobals
-let norm_char_latin1 c = match Char.uppercase c with
+[@@@ocaml.warning "-3"] (* Char.uppercase_ascii since 4.03.0 GPR#124 *)
+let uppercase = Char.uppercase
+[@@@ocaml.warning "+3"]
+
+let norm_char_latin1 c = match uppercase c with
| '\192'..'\198' -> 'A'
| '\199' -> 'C'
| '\200'..'\203' -> 'E'
@@ -19,19 +23,14 @@ let norm_char_latin1 c = match Char.uppercase c with
| '\221' -> 'Y'
| c -> c
-let norm_char_utf8 c = Char.uppercase c
+let norm_char_utf8 c = uppercase c
let norm_char c =
if !utf8 then norm_char_utf8 c else
if !latin1 then norm_char_latin1 c else
- Char.uppercase c
-
-let norm_string s =
- let u = String.copy s in
- for i = 0 to String.length s - 1 do
- u.[i] <- norm_char s.[i]
- done;
- u
+ uppercase c
+
+let norm_string = String.map (fun s -> norm_char s)
let compare_char c1 c2 = match norm_char c1, norm_char c2 with
| ('A'..'Z' as c1), ('A'..'Z' as c2) -> compare c1 c2
diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
index 5d48473d8c..ef203960b5 100644
--- a/tools/coqdoc/cdglobals.ml
+++ b/tools/coqdoc/cdglobals.ml
@@ -70,23 +70,21 @@ let normalize_filename f =
let dirname = Filename.dirname f in
normalize_path dirname, basename
+(** Add a local installation suffix (unless the suffix is itself
+ absolute in which case the prefix does not matter) *)
+let use_suffix prefix suffix =
+ if String.length suffix > 0 && suffix.[0] = '/' then suffix else prefix / suffix
+
(** A weaker analog of the function in Envars *)
let guess_coqlib () =
let file = "theories/Init/Prelude.vo" in
- match Coq_config.coqlib with
- | Some coqlib when Sys.file_exists (coqlib / file) -> coqlib
- | Some _ | None ->
- let coqbin = normalize_path (Filename.dirname Sys.executable_name) in
- let prefix = Filename.dirname coqbin in
- let rpath =
- if Coq_config.local then []
- else if Coq_config.arch_is_win32 then ["lib"]
- else ["lib/coq"]
- in
- let coqlib = List.fold_left (/) prefix rpath in
- if Sys.file_exists (coqlib / file) then coqlib
- else prefix
+ let coqbin = normalize_path (Filename.dirname Sys.executable_name) in
+ let prefix = Filename.dirname coqbin in
+ let coqlib = use_suffix prefix Coq_config.coqlibsuffix in
+ if Sys.file_exists (coqlib / file) then coqlib else
+ if not Coq_config.local && Sys.file_exists (Coq_config.coqlib / file)
+ then Coq_config.coqlib else prefix
let header_trailer = ref true
let header_file = ref ""
diff --git a/tools/coqdoc/cdglobals.mli b/tools/coqdoc/cdglobals.mli
new file mode 100644
index 0000000000..2c9b3fb8e8
--- /dev/null
+++ b/tools/coqdoc/cdglobals.mli
@@ -0,0 +1,49 @@
+type target_language = LaTeX | HTML | TeXmacs | Raw
+val target_language : target_language ref
+type output_t = StdOut | MultFiles | File of string
+val output_dir : string ref
+val out_to : output_t ref
+val out_channel : out_channel ref
+val ( / ) : string -> string -> string
+val coqdoc_out : string -> string
+val open_out_file : string -> unit
+val close_out_file : unit -> unit
+type glob_source_t = NoGlob | DotGlob | GlobFile of string
+val glob_source : glob_source_t ref
+val normalize_path : string -> string
+val normalize_filename : string -> string * string
+val guess_coqlib : unit -> string
+val header_trailer : bool ref
+val header_file : string ref
+val header_file_spec : bool ref
+val footer_file : string ref
+val footer_file_spec : bool ref
+val quiet : bool ref
+val light : bool ref
+val gallina : bool ref
+val short : bool ref
+val index : bool ref
+val multi_index : bool ref
+val index_name : string ref
+val toc : bool ref
+val page_title : string ref
+val title : string ref
+val externals : bool ref
+val coqlib : string ref
+val coqlib_path : string ref
+val raw_comments : bool ref
+val parse_comments : bool ref
+val plain_comments : bool ref
+val toc_depth : int option ref
+val lib_name : string ref
+val lib_subtitles : bool ref
+val interpolate : bool ref
+val inline_notmono : bool ref
+val charset : string ref
+val inputenc : string ref
+val latin1 : bool ref
+val utf8 : bool ref
+val set_latin1 : unit -> unit
+val set_utf8 : unit -> unit
+type coq_module = string
+type file = Vernac_file of string * coq_module | Latex_file of string
diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml
index 9be791a8de..4d118b9788 100644
--- a/tools/coqdoc/index.ml
+++ b/tools/coqdoc/index.ml
@@ -155,10 +155,14 @@ let sort_entries el =
let display_letter c = if c = '*' then "other" else String.make 1 c
+[@@@ocaml.warning "-3"] (* String.lowercase_ascii since 4.03.0 GPR#124 *)
+let lowercase = String.lowercase
+[@@@ocaml.warning "+3"]
+
let type_name = function
| Library ->
let ln = !lib_name in
- if ln <> "" then String.lowercase ln else "library"
+ if ln <> "" then lowercase ln else "library"
| Module -> "module"
| Definition -> "definition"
| Inductive -> "inductive"
@@ -197,7 +201,7 @@ let prepare_entry s = function
let h = try String.index_from s 0 ':' with _ -> err () in
let i = try String.index_from s (h+1) ':' with _ -> err () in
let sc = String.sub s (h+1) (i-h-1) in
- let ntn = String.make (String.length s - i) ' ' in
+ let ntn = Bytes.make (String.length s - i) ' ' in
let k = ref 0 in
let j = ref (i+1) in
let quoted = ref false in
@@ -205,22 +209,22 @@ let prepare_entry s = function
while !j <= l do
if not !quoted then begin
(match s.[!j] with
- | '_' -> ntn.[!k] <- ' '; incr k
- | 'x' -> ntn.[!k] <- '_'; incr k
+ | '_' -> Bytes.set ntn !k ' '; incr k
+ | 'x' -> Bytes.set ntn !k '_'; incr k
| '\'' -> quoted := true
| _ -> assert false)
end
else
if s.[!j] = '\'' then
if (!j = l || s.[!j+1] = '_') then quoted := false
- else (incr j; ntn.[!k] <- s.[!j]; incr k)
+ else (incr j; Bytes.set ntn !k s.[!j]; incr k)
else begin
- ntn.[!k] <- s.[!j];
+ Bytes.set ntn !k s.[!j];
incr k
end;
incr j
done;
- let ntn = String.sub ntn 0 !k in
+ let ntn = Bytes.sub_string ntn 0 !k in
if sc = "" then ntn else ntn ^ " (" ^ sc ^ ")"
| _ ->
s
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 82d3d62b59..9723905790 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -19,6 +19,10 @@ let printf s = Printf.fprintf !out_channel s
let sprintf = Printf.sprintf
+[@@@ocaml.warning "-3"] (* String.{capitalize,lowercase}_ascii since 4.03.0 GPR#124 *)
+let capitalize = String.capitalize
+let lowercase = String.lowercase
+[@@@ocaml.warning "+3"]
(*s Coq keywords *)
@@ -36,7 +40,7 @@ let is_keyword =
"Hypothesis"; "Hypotheses";
"Resolve"; "Unfold"; "Immediate"; "Extern"; "Constructors"; "Rewrite";
"Implicit"; "Import"; "Inductive";
- "Infix"; "Lemma"; "Let"; "Load"; "Local"; "Ltac";
+ "Infix"; "Lemma"; "Let"; "Load"; "Local"; "Locate"; "Ltac";
"Module"; "Module Type"; "Declare Module"; "Include";
"Mutual"; "Parameter"; "Parameters"; "Print"; "Printing"; "All"; "Proof"; "Proof with"; "Qed";
"Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme"; "Assumptions"; "Axioms"; "Universes";
@@ -58,9 +62,9 @@ let is_keyword =
(*i (* coq terms *) *)
"forall"; "match"; "as"; "in"; "return"; "with"; "end"; "let"; "fun";
"if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="; "where"; "struct"; "wf"; "measure";
- "fix"; "cofix";
+ "fix"; "cofix"; "is";
(* Ltac *)
- "before"; "after"; "constr"; "ltac"; "goal"; "context"; "beta"; "delta"; "iota"; "zeta"; "lazymatch";
+ "before"; "after"; "constr"; "ltac"; "goal"; "context"; "beta"; "delta"; "iota"; "zeta"; "lazymatch"; "type"; "of"; "rec";
(* Notations *)
"level"; "associativity"; "no"
]
@@ -70,7 +74,7 @@ let is_tactic =
[ "intro"; "intros"; "apply"; "rewrite"; "refine"; "case"; "clear"; "injection";
"elimtype"; "progress"; "setoid_rewrite"; "left"; "right"; "constructor";
"econstructor"; "decide equality"; "abstract"; "exists"; "cbv"; "simple destruct";
- "info"; "fourier"; "field"; "specialize"; "evar"; "solve"; "instanciate";
+ "info"; "fourier"; "field"; "specialize"; "evar"; "solve"; "instanciate"; "info_auto"; "info_eauto";
"quote"; "eexact"; "autorewrite";
"destruct"; "destruction"; "destruct_call"; "dependent"; "elim"; "extensionality";
"f_equal"; "generalize"; "generalize_eqs"; "generalize_eqs_vars"; "induction"; "rename"; "move"; "omega";
@@ -846,7 +850,7 @@ module Html = struct
if t = Library then
let ln = !lib_name in
if ln <> "" then
- "[" ^ String.lowercase ln ^ "]", m ^ ".html", t
+ "[" ^ lowercase ln ^ "]", m ^ ".html", t
else
"[library]", m ^ ".html", t
else
@@ -864,7 +868,7 @@ module Html = struct
(* Impression de la table d'index *)
let print_index_table_item i =
- printf "<tr>\n<td>%s Index</td>\n" (String.capitalize i.idx_name);
+ printf "<tr>\n<td>%s Index</td>\n" (capitalize i.idx_name);
List.iter
(fun (c,l) ->
if l <> [] then
@@ -912,7 +916,7 @@ module Html = struct
let print_table () = print_index_table all_index in
let print_one_index i =
if i.idx_size > 0 then begin
- printf "<hr/>\n<h1>%s Index</h1>\n" (String.capitalize i.idx_name);
+ printf "<hr/>\n<h1>%s Index</h1>\n" (capitalize i.idx_name);
all_letters i
end
in
diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli
index 853bc29aa4..235f2588c8 100644
--- a/tools/coqdoc/output.mli
+++ b/tools/coqdoc/output.mli
@@ -64,7 +64,6 @@ val keyword : string -> loc -> unit
val ident : string -> loc option -> unit
val sublexer : char -> loc -> unit
val sublexer_in_doc : char -> unit
-val initialize : unit -> unit
val proofbox : unit -> unit
diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml
index eaf938e8ce..9bca135127 100644
--- a/tools/coqmktop.ml
+++ b/tools/coqmktop.ml
@@ -20,6 +20,10 @@ let split_list =
let spaces = Str.regexp "[ \t\n]+" in
fun str -> Str.split spaces str
+[@@@ocaml.warning "-3"] (* String.uncapitalize_ascii since 4.03.0 GPR#124 *)
+let capitalize = String.capitalize
+[@@@ocaml.warning "+3"]
+
let (/) = Filename.concat
(** Which user files do we support (and propagate to ocamlopt) ?
@@ -39,8 +43,7 @@ let native_suffix f = match CUnix.get_extension f with
(** Transforms a file name in the corresponding Caml module name.
*)
let module_of_file name =
- String.capitalize
- (try Filename.chop_extension name with Invalid_argument _ -> name)
+ capitalize (try Filename.chop_extension name with Invalid_argument _ -> name)
(** Run a command [prog] with arguments [args].
We do not use [Sys.command] anymore, see comment in [CUnix.sys_command].
@@ -62,8 +65,6 @@ let echo = ref false
let no_start = ref false
let is_ocaml4 = Coq_config.caml_version.[0] <> '3'
-let is_camlp5 = Coq_config.camlp4 = "camlp5"
-
(** {6 Includes options} *)
@@ -75,6 +76,7 @@ let std_includes basedir =
let rebase d = match basedir with None -> d | Some base -> base / d in
["-I"; rebase ".";
"-I"; rebase "lib";
+ "-I"; rebase "vernac"; (* For Mltop *)
"-I"; rebase "toplevel";
"-I"; rebase "kernel/byterun";
"-I"; Envars.camlp4lib () ] @
@@ -105,7 +107,7 @@ let incl_all_subdirs dir opts =
(** OCaml + CamlpX libraries *)
let ocaml_libs = ["str.cma";"unix.cma";"nums.cma";"dynlink.cma";"threads.cma"]
-let camlp4_libs = if is_camlp5 then ["gramlib.cma"] else ["camlp4lib.cma"]
+let camlp4_libs = ["gramlib.cma"]
let libobjs = ocaml_libs @ camlp4_libs
(** Toplevel objects *)
@@ -116,14 +118,7 @@ let ocaml_topobjs =
else
["toplevellib.cma"]
-let camlp4_topobjs =
- if is_camlp5 then
- ["camlp5_top.cma"; "pa_o.cmo"; "pa_extend.cmo"]
- else
- [ "Camlp4Top.cmo";
- "Camlp4Parsers/Camlp4OCamlRevisedParser.cmo";
- "Camlp4Parsers/Camlp4OCamlParser.cmo";
- "Camlp4Parsers/Camlp4GrammarParser.cmo" ]
+let camlp4_topobjs = ["camlp5_top.cma"; "pa_o.cmo"; "pa_extend.cmo"]
let topobjs = ocaml_topobjs @ camlp4_topobjs
@@ -235,7 +230,7 @@ let declare_loading_string () =
\n Mltop.set_top\
\n {Mltop.load_obj=\
\n (fun f -> if not (Topdirs.load_file ppf f)\
-\n then CErrors.error (\"Could not load plugin \"^f));\
+\n then CErrors.user_err Pp.(str (\"Could not load plugin \"^f)));\
\n Mltop.use_file=Topdirs.dir_use ppf;\
\n Mltop.add_dir=Topdirs.dir_directory;\
\n Mltop.ml_loop=(fun () -> Toploop.loop ppf) };;\
@@ -265,12 +260,12 @@ let create_tmp_main_file modules =
let main () =
let (options, userfiles) = parse_args () in
(* Directories: *)
- let () = Envars.set_coqlib ~fail:CErrors.error in
+ let () = Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x)) in
let basedir = if !Flags.boot then None else Some (Envars.coqlib ()) in
(* Which ocaml compiler to invoke *)
let prog = if !opt then "opt" else "ocamlc" in
(* Which arguments ? *)
- if !opt && !top then failwith "no custom toplevel in native code !";
+ if !opt && !top then failwith "no custom toplevel in native code!";
let flags = if !opt then [] else Coq_config.vmbyteflags in
let topstart = if !top then [ "topstart.cmo" ] else [] in
let (modules, tolink) = files_to_link userfiles in
diff --git a/tools/coqwc.mll b/tools/coqwc.mll
index b4fc738d0e..cd07d4216f 100644
--- a/tools/coqwc.mll
+++ b/tools/coqwc.mll
@@ -239,6 +239,7 @@ let process_channel ch =
if !skip_header then read_header lb;
spec lb
+[@@@ocaml.warning "-52"]
let process_file f =
try
let ch = open_in f in
@@ -251,6 +252,7 @@ let process_file f =
flush stdout; eprintf "coqwc: %s: Is a directory\n" f; flush stderr
| Sys_error s ->
flush stdout; eprintf "coqwc: %s\n" s; flush stderr
+[@@@ocaml.warning "+52"]
(*s Parsing of the command line. *)
diff --git a/tools/coqworkmgr.ml b/tools/coqworkmgr.ml
index d7bdf907a2..b8e69d6c6d 100644
--- a/tools/coqworkmgr.ml
+++ b/tools/coqworkmgr.ml
@@ -72,10 +72,13 @@ let really_read_fd fd s off len =
let raw_input_line fd =
try
let b = Buffer.create 80 in
- let s = String.make 1 '\000' in
- while s <> "\n" do
+ let s = Bytes.make 1 '\000' in
+ let endl = Bytes.of_string "\n" in
+ let endr = Bytes.of_string "\r" in
+ while Bytes.compare s endl <> 0 do
really_read_fd fd s 0 1;
- if s <> "\n" && s <> "\r" then Buffer.add_string b s;
+ if Bytes.compare s endl <> 0 && Bytes.compare s endr <> 0
+ then Buffer.add_bytes b s;
done;
Buffer.contents b
with Unix.Unix_error _ -> raise End_of_file
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index 8fcca535d1..932097607b 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -12,24 +12,15 @@ let error s =
prerr_endline ("fake_id: error: "^s);
exit 1
+let pperr_endline pp = Format.eprintf "@[%a@]\n%!" Pp.pp_with pp
+
type coqtop = {
xml_printer : Xml_printer.t;
xml_parser : Xml_parser.t;
}
-let print_xml chan xml =
- let rec print = function
- | Xml_datatype.PCData s -> output_string chan s
- | Xml_datatype.Element (_, _, children) -> List.iter print children
- in
- print xml
-
-let error_xml s =
- Printf.eprintf "fake_id: error: %a\n%!" print_xml s;
- exit 1
-
-let logger level content =
- Printf.eprintf "%a\n%! " print_xml (Richpp.repr content)
+let print_error msg =
+ Format.eprintf "fake_id: error: @[%a@]\n%!" Pp.pp_with msg
let base_eval_call ?(print=true) ?(fail=true) call coqtop =
if print then prerr_endline (Xmlprotocol.pr_call call);
@@ -37,20 +28,15 @@ let base_eval_call ?(print=true) ?(fail=true) call coqtop =
Xml_printer.print coqtop.xml_printer xml_query;
let rec loop () =
let xml = Xml_parser.parse coqtop.xml_parser in
- match Xmlprotocol.is_message xml with
- | Some (level, _loc, content) ->
- logger level content;
+ if Xmlprotocol.is_feedback xml then
loop ()
- | None ->
- if Xmlprotocol.is_feedback xml then
- loop ()
- else Xmlprotocol.to_answer call xml
+ else Xmlprotocol.to_answer call xml
in
let res = loop () in
if print then prerr_endline (Xmlprotocol.pr_full_value call res);
match res with
- | Interface.Fail (_,_,s) when fail -> error_xml (Richpp.repr s)
- | Interface.Fail (_,_,s) as x -> Printf.eprintf "%a\n%!" print_xml (Richpp.repr s); x
+ | Interface.Fail (_,_,s) when fail -> print_error s; exit 1
+ | Interface.Fail (_,_,s) as x -> print_error s; x
| x -> x
let eval_call c q = ignore(base_eval_call c q)
@@ -186,7 +172,7 @@ let print_document () =
Str.global_replace (Str.regexp "^[\n ]*") ""
(if String.length s > 20 then String.sub s 0 17 ^ "..."
else s) in
- prerr_endline (Pp.string_of_ppcmds
+ pperr_endline (
(Document.print doc
(fun b state_id { name; text } ->
Pp.str (Printf.sprintf "%s[%10s, %3s] %s"
@@ -199,7 +185,7 @@ let print_document () =
module GUILogic = struct
let after_add = function
- | Interface.Fail (_,_,s) -> error_xml (Richpp.repr s)
+ | Interface.Fail (_,_,s) -> print_error s; exit 1
| Interface.Good (id, (Util.Inl (), _)) ->
Document.assign_tip_id doc id
| Interface.Good (id, (Util.Inr tip, _)) ->
@@ -211,7 +197,7 @@ module GUILogic = struct
let at id id' _ = Stateid.equal id' id
let after_edit_at (id,need_unfocus) = function
- | Interface.Fail (_,_,s) -> error_xml (Richpp.repr s)
+ | Interface.Fail (_,_,s) -> print_error s; exit 1
| Interface.Good (Util.Inl ()) ->
if need_unfocus then Document.unfocus doc;
ignore(Document.cut_at doc id);
@@ -310,11 +296,12 @@ let main =
Sys.set_signal Sys.sigpipe
(Sys.Signal_handle
(fun _ -> prerr_endline "Broken Pipe (coqtop died ?)"; exit 1));
+ let def_args = ["--xml_format=Ppcmds"; "-ideslave"] in
let coqtop_name, coqtop_args, input_file = match Sys.argv with
- | [| _; f |] -> "coqtop",[|"-ideslave"|], f
+ | [| _; f |] -> "coqtop", Array.of_list def_args, f
| [| _; f; ct |] ->
let ct = Str.split (Str.regexp " ") ct in
- List.hd ct, Array.of_list ("-ideslave" :: List.tl ct), f
+ List.hd ct, Array.of_list (def_args @ List.tl ct), f
| _ -> usage () in
let inc = if input_file = "-" then stdin else open_in input_file in
let coq =
@@ -334,7 +321,7 @@ let main =
let finish () =
match base_eval_call (Xmlprotocol.status true) coq with
| Interface.Good _ -> exit 0
- | Interface.Fail (_,_,s) -> error_xml (Richpp.repr s) in
+ | Interface.Fail (_,_,s) -> print_error s; exit 1 in
(* The main loop *)
init ();
while true do
diff --git a/tools/gallina-syntax.el b/tools/gallina-syntax.el
index c25abece15..662762b08c 100644
--- a/tools/gallina-syntax.el
+++ b/tools/gallina-syntax.el
@@ -390,7 +390,7 @@
("Corollary" "cor" "Corollary # : #.\nProof.\n#\nQed." t "Corollary")
("Declare Module :" "dmi" "Declare Module # : #.\n#\nEnd #." t)
("Declare Module <:" "dmi2" "Declare Module # <: #.\n#\nEnd #." t)
- ("Definition goal" "defg" "Definition #:#.\n#\nSave." t);; careful
+ ("Definition goal" "defg" "Definition #:#.\n#\nQed." t);; careful
("Fact" "fct" "Fact # : #." t "Fact")
("Goal" nil "Goal #." t "Goal")
("Lemma" "l" "Lemma # : #.\nProof.\n#\nQed." t "Lemma")
@@ -492,7 +492,6 @@
("Require" nil "Require #." t "Require")
("Reserved Notation" nil "Reserved Notation" nil "Reserved\\s-+Notation")
("Reset Extraction Inline" nil "Reset Extraction Inline." t "Reset\\s-+Extraction\\s-+Inline")
- ("Save" nil "Save." t "Save")
("Search" nil "Search #" nil "Search")
("SearchAbout" nil "SearchAbout #" nil "SearchAbout")
("SearchPattern" nil "SearchPattern #" nil "SearchPattern")
@@ -710,7 +709,6 @@ Used by `coq-goal-command-p'"
(defvar coq-keywords-save-strict
'("Defined"
- "Save"
"Qed"
"End"
"Admitted"
diff --git a/tools/gallina_lexer.mll b/tools/gallina_lexer.mll
index 449efd57cd..432b18e645 100644
--- a/tools/gallina_lexer.mll
+++ b/tools/gallina_lexer.mll
@@ -105,7 +105,6 @@ and end_of_line = parse
| _ { print (Lexing.lexeme lexbuf) }
and skip_proof = parse
- | "Save." { end_of_line lexbuf }
| "Save" space
{ skip_until_point lexbuf }
| "Qed." { end_of_line lexbuf }
diff --git a/tools/ocamllibdep.mll b/tools/ocamllibdep.mll
index bf82be09f1..5d11e30089 100644
--- a/tools/ocamllibdep.mll
+++ b/tools/ocamllibdep.mll
@@ -11,6 +11,12 @@
let syntax_error lexbuf =
raise (Syntax_error (Lexing.lexeme_start lexbuf, Lexing.lexeme_end lexbuf))
+
+ [@@@ocaml.warning "-3"] (* String.(un)capitalize_ascii since 4.03.0 GPR#124 *)
+ let uncapitalize = String.uncapitalize
+
+ let capitalize = String.capitalize
+ [@@@ocaml.warning "+3"]
}
let space = [' ' '\t' '\n' '\r']
@@ -22,7 +28,9 @@ let caml_up_ident = uppercase identchar*
let caml_low_ident = lowercase identchar*
rule mllib_list = parse
- | caml_up_ident { let s = String.uncapitalize (Lexing.lexeme lexbuf)
+ | uppercase+ { let s = Lexing.lexeme lexbuf in
+ s :: mllib_list lexbuf }
+ | caml_up_ident { let s = uncapitalize (Lexing.lexeme lexbuf)
in s :: mllib_list lexbuf }
| "*predef*" { mllib_list lexbuf }
| space+ { mllib_list lexbuf }
@@ -185,7 +193,7 @@ let mlpack_dependencies () =
List.iter
(fun (name,dirname) ->
let fullname = file_name name dirname in
- let modname = String.capitalize name in
+ let modname = capitalize name in
let deps = traite_fichier_modules fullname ".mlpack" in
let sdeps = String.concat " " deps in
let efullname = escape fullname in
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 12:03:09 +0000