From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- tools/CoqMakefile.in | 799 ++++++++++++++++++++ tools/TimeFileMaker.py | 219 ++++++ tools/beautify-archive | 2 +- tools/check-translate | 2 +- tools/coq-inferior.el | 324 -------- tools/coq_makefile.ml | 1279 ++++++++++---------------------- tools/coq_tex.ml | 10 +- tools/coqc.ml | 29 +- tools/coqdep.ml | 63 +- tools/coqdep_boot.ml | 16 +- tools/coqdep_common.ml | 70 +- tools/coqdep_common.mli | 18 +- tools/coqdep_lexer.mli | 10 +- tools/coqdep_lexer.mll | 73 +- tools/coqdoc/alpha.ml | 29 +- tools/coqdoc/alpha.mli | 10 +- tools/coqdoc/cdglobals.ml | 34 +- tools/coqdoc/cdglobals.mli | 49 ++ tools/coqdoc/cpretty.mli | 10 +- tools/coqdoc/cpretty.mll | 29 +- tools/coqdoc/index.ml | 30 +- tools/coqdoc/index.mli | 10 +- tools/coqdoc/main.ml | 10 +- tools/coqdoc/output.ml | 62 +- tools/coqdoc/output.mli | 11 +- tools/coqdoc/tokens.ml | 10 +- tools/coqdoc/tokens.mli | 10 +- tools/coqmktop.ml | 305 -------- tools/coqwc.mll | 14 +- tools/coqworkmgr.ml | 27 +- tools/fake_ide.ml | 82 +- tools/gallina-db.el | 2 +- tools/gallina-syntax.el | 4 +- tools/gallina.ml | 10 +- tools/gallina_lexer.mll | 11 +- tools/inferior-coq.el | 324 ++++++++ tools/make-both-single-timing-files.py | 12 + tools/make-both-time-files.py | 16 + tools/make-one-time-file.py | 21 + tools/md5sum.ml | 24 + tools/ocamllibdep.mll | 41 +- 41 files changed, 2281 insertions(+), 1830 deletions(-) create mode 100644 tools/CoqMakefile.in create mode 100644 tools/TimeFileMaker.py delete mode 100644 tools/coq-inferior.el create mode 100644 tools/coqdoc/cdglobals.mli delete mode 100644 tools/coqmktop.ml create mode 100644 tools/inferior-coq.el create mode 100755 tools/make-both-single-timing-files.py create mode 100755 tools/make-both-time-files.py create mode 100755 tools/make-one-time-file.py create mode 100644 tools/md5sum.ml (limited to 'tools') diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in new file mode 100644 index 00000000..f7e30eae --- /dev/null +++ b/tools/CoqMakefile.in @@ -0,0 +1,799 @@ +############################################################################### +## v # The Coq Proof Assistant ## +## /dev/null 2>/dev/null; echo $$?)) +STDTIME?=command time -f $(TIMEFMT) +else +ifeq (0,$(shell gtime -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?)) +STDTIME?=gtime -f $(TIMEFMT) +else +STDTIME?=command time +endif +endif +else +STDTIME?=command time -f $(TIMEFMT) +endif + +# Coq binaries +COQC ?= "$(COQBIN)coqc" +COQTOP ?= "$(COQBIN)coqtop" +COQCHK ?= "$(COQBIN)coqchk" +COQDEP ?= "$(COQBIN)coqdep" +GALLINA ?= "$(COQBIN)gallina" +COQDOC ?= "$(COQBIN)coqdoc" +COQMKFILE ?= "$(COQBIN)coq_makefile" + +# Timing scripts +COQMAKE_ONE_TIME_FILE ?= "$(COQLIB)/tools/make-one-time-file.py" +COQMAKE_BOTH_TIME_FILES ?= "$(COQLIB)/tools/make-both-time-files.py" +COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQLIB)/tools/make-both-single-timing-files.py" +BEFORE ?= +AFTER ?= + +# FIXME this should be generated by Coq (modules already linked by Coq) +CAMLDONTLINK=camlp5.gramlib,unix,str + +# OCaml binaries +CAMLC ?= "$(OCAMLFIND)" ocamlc -c +CAMLOPTC ?= "$(OCAMLFIND)" opt -c +CAMLLINK ?= "$(OCAMLFIND)" ocamlc -linkpkg -dontlink $(CAMLDONTLINK) +CAMLOPTLINK ?= "$(OCAMLFIND)" opt -linkpkg -dontlink $(CAMLDONTLINK) +CAMLDOC ?= "$(OCAMLFIND)" ocamldoc +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 ?= + +# Extra packages to be linked in (as in findlib -package) +CAMLPKGS ?= + +# Option for making timing files +TIMING?= +# Option for changing sorting of timing output file +TIMING_SORT_BY ?= auto +# Output file names for timed builds +TIME_OF_BUILD_FILE ?= time-of-build.log +TIME_OF_BUILD_BEFORE_FILE ?= time-of-build-before.log +TIME_OF_BUILD_AFTER_FILE ?= time-of-build-after.log +TIME_OF_PRETTY_BUILD_FILE ?= time-of-build-pretty.log +TIME_OF_PRETTY_BOTH_BUILD_FILE ?= time-of-build-both.log +TIME_OF_PRETTY_BUILD_EXTRA_FILES ?= - # also output to the command line + +########## 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:=.cma +DYNLIB:=.cma +else +USEBYTE:= +DYNOBJ:=.cmxs +DYNLIB:=.cmxs +endif + +COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) +COQCHKFLAGS?=-silent -o $(COQLIBS) +COQDOCFLAGS?=-interpolate -utf8 +COQDOCLIBS?=$(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 $(CAMLP5LIB) + +# ocamldoc fails with unknown argument otherwise +CAMLDOCFLAGS=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS))) + +# FIXME This should be generated by Coq +GRAMMARS:=grammar.cma +CAMLP5EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo + +CAMLLIB:=$(shell "$(OCAMLFIND)" printconf stdlib 2> /dev/null) +ifeq (,$(CAMLLIB)) +PP=$(error "Cannot find the 'ocamlfind' binary used to build Coq ($(OCAMLFIND)). Pre-compiled binary packages of Coq do not support compiling plugins this way. Please download the sources of Coq and run the Windows build script.") +else +PP:=-pp '$(CAMLP5O) -I $(CAMLLIB) -I "$(COQLIB)/grammar" $(CAMLP5EXTEND) $(GRAMMARS) $(CAMLP5OPTIONS) -impl' +endif + +ifneq (,$(TIMING)) +TIMING_ARG=-time +ifeq (after,$(TIMING)) +TIMING_EXT=after-timing +else +ifeq (before,$(TIMING)) +TIMING_EXT=before-timing +else +TIMING_EXT=timing +endif +endif +else +TIMING_ARG= +endif + +# Retro compatibility (DESTDIR is standard on Unix, DSTROOT is not) +ifdef DSTROOT +DESTDIR := $(DSTROOT) +endif + +concat_path = $(if $(1),$(1)/$(if $(COQMF_WINDRIVE),$(subst $(COQMF_WINDRIVE),/,$(2)),$(2)),$(2)) + +COQLIBINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)user-contrib) +COQDOCINSTALL = $(call concat_path,$(DESTDIR),$(DOCDIR)user-contrib) +COQTOPINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)toploop) + +# 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 + +VDFILE := .coqdeps + +ALLSRCFILES := \ + $(ML4FILES) \ + $(MLFILES) \ + $(MLPACKFILES) \ + $(MLLIBFILES) \ + $(MLIFILES) + +# helpers +vo_to_obj = $(addsuffix .o,\ + $(filter-out Warning: Error:,\ + $(shell $(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, so that `install` doesn't show +# warnings and `clean` doesn't pass to rm a list of files that is too long for +# the shell. +NATIVEFILES = $(wildcard $(ALLNATIVEFILES)) +FILESTOINSTALL = \ + $(VOFILES) \ + $(VFILES) \ + $(GLOBFILES) \ + $(NATIVEFILES) \ + $(CMIFILESTOINSTALL) +BYTEFILESTOINSTALL = \ + $(CMOFILESTOINSTALL) \ + $(CMAFILES) +ifeq '$(HASNATDYNLINK)' 'true' +DO_NATDYNLINK = yes +FILESTOINSTALL += $(CMXSFILES) $(CMXAFILES) $(CMOFILESTOINSTALL:.cmo=.cmx) +else +DO_NATDYNLINK = +endif + +ALLDFILES = $(addsuffix .d,$(ALLSRCFILES) $(VDFILE)) + +# 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 + +all.timing.diff: + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" pre-all + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" real-all.timing.diff TIME_OF_PRETTY_BUILD_EXTRA_FILES="" + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" post-all +.PHONY: all.timing.diff + +make-pretty-timed-before:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_BEFORE_FILE) +make-pretty-timed-after:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_AFTER_FILE) +make-pretty-timed make-pretty-timed-before make-pretty-timed-after:: + $(HIDE)rm -f pretty-timed-success.ok + $(HIDE)($(MAKE) --no-print-directory -f "$(PARENT)" $(TGTS) TIMED=1 2>&1 && touch pretty-timed-success.ok) | tee -a $(TIME_OF_BUILD_FILE) + $(HIDE)rm pretty-timed-success.ok # must not be -f; must fail if the touch failed +print-pretty-timed:: + $(HIDE)$(COQMAKE_ONE_TIME_FILE) $(TIME_OF_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) +print-pretty-timed-diff:: + $(HIDE)$(COQMAKE_BOTH_TIME_FILES) --sort-by=$(TIMING_SORT_BY) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) +ifeq (,$(BEFORE)) +print-pretty-single-time-diff:: + @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing' + $(HIDE)false +else +ifeq (,$(AFTER)) +print-pretty-single-time-diff:: + @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing' + $(HIDE)false +else +print-pretty-single-time-diff:: + $(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) --sort-by=$(TIMING_SORT_BY) $(AFTER) $(BEFORE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) +endif +endif +pretty-timed: + $(HIDE)$(MAKE) --no-print-directory -f "$(PARENT)" make-pretty-timed + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" print-pretty-timed +.PHONY: pretty-timed make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff + +# 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 + +real-all.timing.diff: $(VOFILES:.vo=.v.timing.diff) +.PHONY: real-all.timing.diff + +bytefiles: $(CMOFILES) $(CMAFILES) +.PHONY: bytefiles + +optfiles: $(if $(DO_NATDYNLINK),$(CMXSFILES)) +.PHONY: optfiles + +# FIXME, see Ralf's bugreport +quick: $(VOFILES:.vo=.vio) +.PHONY: quick + +vio2vo: + $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) \ + -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio) +.PHONY: vio2vo + +quick2vo: + $(HIDE)make -j $(J) quick + $(HIDE)VIOFILES=$$(for vofile in $(VOFILES); do \ + viofile="$$(echo "$$vofile" | sed "s/\.vo$$/.vio/")"; \ + if [ "$$vofile" -ot "$$viofile" -o ! -e "$$vofile" ]; then printf "$$viofile "; fi; \ + done); \ + echo "VIO2VO: $$VIOFILES"; \ + if [ -n "$$VIOFILES" ]; then \ + $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $$VIOFILES; \ + fi +.PHONY: quick2vo + +checkproofs: + $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) \ + -schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio) +.PHONY: checkproofs + +validate: $(VOFILES) + $(TIMER) $(COQCHK) $(COQCHKFLAGS) $^ +.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)'CAMLDOC -d $@' + $(HIDE)mkdir $@ || rm -rf $@/* + $(HIDE)$(CAMLDOC) -html \ + -d $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES) + +all-mli.tex: $(MLIFILES:.mli=.cmi) + $(SHOW)'CAMLDOC -latex $@' + $(HIDE)$(CAMLDOC) -latex \ + -o $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(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: + $(HIDE)for f in $(FILESTOINSTALL); do\ + df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\ + if [ "$$?" != "0" -o -z "$$df" ]; then\ + echo SKIP "$$f" since it has no logical path;\ + else\ + install -d "$(COQLIBINSTALL)/$$df" &&\ + install -m 0644 "$$f" "$(COQLIBINSTALL)/$$df" &&\ + echo INSTALL "$$f" "$(COQLIBINSTALL)/$$df";\ + fi;\ + done + $(HIDE)$(MAKE) install-extra -f "$(SELF)" +install-extra:: + @# Extension point +.PHONY: install install-extra + +install-byte: + $(HIDE)for f in $(BYTEFILESTOINSTALL); do\ + df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\ + if [ "$$?" != "0" -o -z "$$df" ]; then\ + echo SKIP "$$f" since it has no logical path;\ + else\ + install -d "$(COQLIBINSTALL)/$$df" &&\ + install -m 0644 "$$f" "$(COQLIBINSTALL)/$$df" &&\ + echo INSTALL "$$f" "$(COQLIBINSTALL)/$$df";\ + fi;\ + done + +install-doc:: html mlihtml + @# Extension point + $(HIDE)install -d "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html" + $(HIDE)for i in html/*; do \ + dest="$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\ + install -m 0644 "$$i" "$$dest";\ + echo INSTALL "$$i" "$$dest";\ + done + $(HIDE)install -d \ + "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml" + $(HIDE)for i in mlihtml/*; do \ + dest="$(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="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`" &&\ + instf="$(COQLIBINSTALL)/$$df/`basename $$f`" &&\ + rm -f "$$instf" &&\ + echo RM "$$instf" &&\ + (rmdir "$(call concat_path,,$(COQLIBINSTALL)/$$df/)" 2>/dev/null || true); \ + done +.PHONY: uninstall + +uninstall-doc:: + @# Extension point + $(SHOW)'RM $(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html' + $(HIDE)rm -rf "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html" + $(SHOW)'RM $(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml' + $(HIDE)rm -rf "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml" + $(HIDE) rmdir "$(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 $(NATIVEFILES) + $(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 -f pretty-timed-success.ok + $(HIDE)rm -rf html mlihtml +.PHONY: clean + +cleanall:: clean + @# Extension point + $(SHOW)'CLEAN *.aux *.timing' + $(HIDE)rm -f $(foreach f,$(VFILES:.v=),$(dir $(f)).$(notdir $(f)).aux) + $(HIDE)rm -f $(TIME_OF_BUILD_FILE) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) + $(HIDE)rm -f $(VOFILES:.vo=.v.timing) + $(HIDE)rm -f $(VOFILES:.vo=.v.before-timing) + $(HIDE)rm -f $(VOFILES:.vo=.v.after-timing) + $(HIDE)rm -f $(VOFILES:.vo=.v.timing.diff) +.PHONY: cleanall + +archclean:: + @# Extension point + $(SHOW)'CLEAN *.cmx *.o' + $(HIDE)rm -f $(NATIVEFILES) + $(HIDE)rm -f $(CMOFILES:%.cmo=%.cmx) +.PHONY: archclean + + +# Compilation rules ########################################################### + +$(MLIFILES:.mli=.cmi): %.cmi: %.mli + $(SHOW)'CAMLC -c $<' + $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $< + +$(ML4FILES:.ml4=.cmo): %.cmo: %.ml4 + $(SHOW)'CAMLC -pp -c $<' + $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(PP) -impl $< + +$(ML4FILES:.ml4=.cmx): %.cmx: %.ml4 + $(SHOW)'CAMLOPT -pp -c $(FOR_PACK) $<' + $(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(PP) $(FOR_PACK) -impl $< + +$(MLFILES:.ml=.cmo): %.cmo: %.ml + $(SHOW)'CAMLC -c $<' + $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $< + +$(MLFILES:.ml=.cmx): %.cmx: %.ml + $(SHOW)'CAMLOPT -c $(FOR_PACK) $<' + $(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(FOR_PACK) $< + + +$(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa + $(SHOW)'CAMLOPT -shared -o $@' + $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \ + -linkall -shared -o $@ $< + +$(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib + $(SHOW)'CAMLC -a -o $@' + $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^ + +$(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib + $(SHOW)'CAMLOPT -a -o $@' + $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^ + + +$(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmxa + $(SHOW)'CAMLOPT -shared -o $@' + $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \ + -shared -linkall -o $@ $< + +$(MLPACKFILES:.mlpack=.cmxa): %.cmxa: %.cmx + $(SHOW)'CAMLOPT -a -o $@' + $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $< + +$(MLPACKFILES:.mlpack=.cma): %.cma: %.cmo | %.mlpack + $(SHOW)'CAMLC -a -o $@' + $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -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) $(CAMLPKGS) \ + -shared -o $@ $< + +ifneq (,$(TIMING)) +TIMING_EXTRA = > $<.$(TIMING_EXT) +else +TIMING_EXTRA = +endif + +$(VOFILES): %.vo: %.v + $(SHOW)COQC $< + $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $< $(TIMING_EXTRA) + +# FIXME ?merge with .vo / .vio ? +$(GLOBFILES): %.glob: %.v + $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $< + +$(VFILES:.v=.vio): %.vio: %.v + $(SHOW)COQC -quick $< + $(HIDE)$(TIMER) $(COQC) -quick $(COQDEBUG) $(COQFLAGS) $< + +$(addsuffix .timing.diff,$(VFILES)): %.timing.diff : %.before-timing %.after-timing + $(SHOW)PYTHON TIMING-DIFF $< + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" print-pretty-single-time-diff BEFORE=$*.before-timing AFTER=$*.after-timing TIME_OF_PRETTY_BUILD_FILE="$@" + +$(BEAUTYFILES): %.v.beautified: %.v + $(SHOW)'BEAUTIFY $<' + $(HIDE)$(TIMER) $(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 make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff,$(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) + +# If this makefile is created using a _CoqProject we have coqdep get +# options from it. This avoids argument length limits for pathological +# projects. Note that extra options might be on the command line. +VDFILE_FLAGS:=$(if @PROJECT_FILE@,-f @PROJECT_FILE@,) $(CMDLINE_COQLIBS) $(CMDLINE_VFILES) + +$(VDFILE).d: $(VFILES) + $(SHOW)'COQDEP VFILES' + $(HIDE)$(COQDEP) -dyndep var $(VDFILE_FLAGS) $(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 'CAMLP5O = $(CAMLP5O)' + @echo 'CAMLP5BIN = $(CAMLP5BIN)' + @echo 'CAMLP5LIB = $(CAMLP5LIB)' + @echo 'CAMLP5OPTIONS = $(CAMLP5OPTIONS)' + @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 $(COQMF_CAMLFLAGS)' > .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/TimeFileMaker.py b/tools/TimeFileMaker.py new file mode 100644 index 00000000..8564aeff --- /dev/null +++ b/tools/TimeFileMaker.py @@ -0,0 +1,219 @@ +from __future__ import with_statement +from __future__ import division +from __future__ import unicode_literals +from __future__ import print_function +import os, sys, re +from io import open + +# This script parses the output of `make TIMED=1` into a dictionary +# mapping names of compiled files to the number of minutes and seconds +# that they took to compile. + +STRIP_REG = re.compile('^(coq/|contrib/|)(?:theories/|src/)?') +STRIP_REP = r'\1' +INFINITY = '\u221e' + +def parse_args(argv, USAGE, HELP_STRING): + sort_by = 'auto' + if any(arg.startswith('--sort-by=') for arg in argv[1:]): + sort_by = [arg for arg in argv[1:] if arg.startswith('--sort-by=')][-1][len('--sort-by='):] + args = [arg for arg in argv if not arg.startswith('--sort-by=')] + if len(args) < 3 or '--help' in args[1:] or '-h' in args[1:] or sort_by not in ('auto', 'absolute', 'diff'): + print(USAGE) + if '--help' in args[1:] or '-h' in args[1:]: + print(HELP_STRING) + if len(args) == 2: sys.exit(0) + sys.exit(1) + return sort_by, args + + +def reformat_time_string(time): + seconds, milliseconds = time.split('.') + seconds = int(seconds) + minutes, seconds = divmod(seconds, 60) + return '%dm%02d.%ss' % (minutes, seconds, milliseconds) + +def get_times(file_name): + ''' + Reads the contents of file_name, which should be the output of + 'make TIMED=1', and parses it to construct a dict mapping file + names to compile durations, as strings. Removes common prefixes + using STRIP_REG and STRIP_REP. + ''' + if file_name == '-': + lines = sys.stdin.read() + else: + with open(file_name, 'r', encoding="utf-8") as f: + lines = f.read() + reg = re.compile(r'^([^\s]+) \([^\)]*?user: ([0-9\.]+)[^\)]*?\)\s*$', re.MULTILINE) + times = reg.findall(lines) + if all(time in ('0.00', '0.01') for name, time in times): + reg = re.compile(r'^([^\s]*) \([^\)]*?real: ([0-9\.]+)[^\)]*?\)\s*$', re.MULTILINE) + times = reg.findall(lines) + if all(STRIP_REG.search(name.strip()) for name, time in times): + times = tuple((STRIP_REG.sub(STRIP_REP, name.strip()), time) for name, time in times) + return dict((name, reformat_time_string(time)) for name, time in times) + +def get_single_file_times(file_name): + ''' + Reads the contents of file_name, which should be the output of + 'coqc -time', and parses it to construct a dict mapping lines to + to compile durations, as strings. + ''' + if file_name == '-': + lines = sys.stdin.read() + else: + with open(file_name, 'r', encoding="utf-8") as f: + lines = f.read() + reg = re.compile(r'^Chars ([0-9]+) - ([0-9]+) ([^ ]+) ([0-9\.]+) secs (.*)$', re.MULTILINE) + times = reg.findall(lines) + if len(times) == 0: return dict() + longest = max(max((len(start), len(stop))) for start, stop, name, time, extra in times) + FORMAT = 'Chars %%0%dd - %%0%dd %%s' % (longest, longest) + return dict((FORMAT % (int(start), int(stop), name), reformat_time_string(time)) for start, stop, name, time, extra in times) + +def fix_sign_for_sorting(num, descending=True): + return -num if descending else num + +def make_sorting_key(times_dict, descending=True): + def get_key(name): + minutes, seconds = times_dict[name].replace('s', '').split('m') + return (fix_sign_for_sorting(int(minutes), descending=descending), + fix_sign_for_sorting(float(seconds), descending=descending), + name) + return get_key + +def get_sorted_file_list_from_times_dict(times_dict, descending=True): + ''' + Takes the output dict of get_times and returns the list of keys, + sorted by duration. + ''' + return sorted(times_dict.keys(), key=make_sorting_key(times_dict, descending=descending)) + +def to_seconds(time): + ''' + Converts a string time into a number of seconds. + ''' + minutes, seconds = time.replace('s', '').split('m') + sign = -1 if time[0] == '-' else 1 + return sign * (abs(int(minutes)) * 60 + float(seconds)) + +def from_seconds(seconds, signed=False): + ''' + Converts a number of seconds into a string time. + ''' + sign = ('-' if seconds < 0 else '+') if signed else '' + seconds = abs(seconds) + minutes = int(seconds) // 60 + seconds -= minutes * 60 + full_seconds = int(seconds) + partial_seconds = int(100 * (seconds - full_seconds)) + return sign + '%dm%02d.%02ds' % (minutes, full_seconds, partial_seconds) + +def sum_times(times, signed=False): + ''' + Takes the values of an output from get_times, parses the time + strings, and returns their sum, in the same string format. + ''' + # sort the times before summing because floating point addition is not associative + return from_seconds(sum(sorted(map(to_seconds, times))), signed=signed) + +def format_percentage(num, signed=True): + sign = ('-' if num < 0 else '+') if signed else '' + num = abs(num) + whole_part = int(num * 100) + frac_part = int(100 * (num * 100 - whole_part)) + return sign + '%d.%02d%%' % (whole_part, frac_part) + +def make_diff_table_string(left_times_dict, right_times_dict, + sort_by='auto', + descending=True, + left_tag="After", tag="File Name", right_tag="Before", with_percent=True, + change_tag="Change", percent_change_tag="% Change"): + # We first get the names of all of the compiled files: all files + # that were compiled either before or after. + all_names_dict = dict() + all_names_dict.update(right_times_dict) + all_names_dict.update(left_times_dict) # do the left (after) last, so that we give precedence to those ones + if len(all_names_dict.keys()) == 0: return 'No timing data' + prediff_times = tuple((name, to_seconds(left_times_dict.get(name,'0m0.0s')), to_seconds(right_times_dict.get(name,'0m0.0s'))) + for name in all_names_dict.keys()) + diff_times_dict = dict((name, from_seconds(lseconds - rseconds, signed=True)) + for name, lseconds, rseconds in prediff_times) + percent_diff_times_dict = dict((name, ((format_percentage((lseconds - rseconds) / rseconds)) + if rseconds != 0 else (INFINITY if lseconds > 0 else 'N/A'))) + for name, lseconds, rseconds in prediff_times) + # update to sort by approximate difference, first + get_key_abs = make_sorting_key(all_names_dict, descending=descending) + get_key_diff_float = (lambda name: fix_sign_for_sorting(to_seconds(diff_times_dict[name]), descending=descending)) + get_key_diff_absint = (lambda name: fix_sign_for_sorting(int(abs(to_seconds(diff_times_dict[name]))), descending=descending)) + if sort_by == 'absolute': + get_key = get_key_abs + elif sort_by == 'diff': + get_key = get_key_diff_float + else: # sort_by == 'auto' + get_key = (lambda name: (get_key_diff_absint(name), get_key_abs(name))) + names = sorted(all_names_dict.keys(), key=get_key) + #names = get_sorted_file_list_from_times_dict(all_names_dict, descending=descending) + # set the widths of each of the columns by the longest thing to go in that column + left_sum = sum_times(left_times_dict.values()) + right_sum = sum_times(right_times_dict.values()) + left_sum_float = sum(sorted(map(to_seconds, left_times_dict.values()))) + right_sum_float = sum(sorted(map(to_seconds, right_times_dict.values()))) + diff_sum = from_seconds(left_sum_float - right_sum_float, signed=True) + percent_diff_sum = (format_percentage((left_sum_float - right_sum_float) / right_sum_float) + if right_sum_float > 0 else 'N/A') + left_width = max(max(map(len, ['N/A'] + list(left_times_dict.values()))), len(left_sum)) + right_width = max(max(map(len, ['N/A'] + list(right_times_dict.values()))), len(right_sum)) + far_right_width = max(max(map(len, ['N/A', change_tag] + list(diff_times_dict.values()))), len(diff_sum)) + far_far_right_width = max(max(map(len, ['N/A', percent_change_tag] + list(percent_diff_times_dict.values()))), len(percent_diff_sum)) + middle_width = max(map(len, names + [tag, "Total"])) + format_string = ("%%(left)-%ds | %%(middle)-%ds | %%(right)-%ds || %%(far_right)-%ds" + % (left_width, middle_width, right_width, far_right_width)) + if with_percent: + format_string += " | %%(far_far_right)-%ds" % far_far_right_width + header = format_string % {'left': left_tag, 'middle': tag, 'right': right_tag, 'far_right': change_tag, 'far_far_right': percent_change_tag} + total = format_string % {'left': left_sum, 'middle': "Total", 'right': right_sum, 'far_right': diff_sum, 'far_far_right': percent_diff_sum} + # separator to go between headers and body + sep = '-' * len(header) + # the representation of the default value (0), to get replaced by N/A + left_rep, right_rep, far_right_rep, far_far_right_rep = ("%%-%ds | " % left_width) % 0, (" | %%-%ds || " % right_width) % 0, ("|| %%-%ds" % far_right_width) % 0, ("| %%-%ds" % far_far_right_width) % 0 + return '\n'.join([header, sep, total, sep] + + [format_string % {'left': left_times_dict.get(name, 0), + 'middle': name, + 'right': right_times_dict.get(name, 0), + 'far_right': diff_times_dict.get(name, 0), + 'far_far_right': percent_diff_times_dict.get(name, 0)} + for name in names]).replace(left_rep, 'N/A'.center(len(left_rep) - 3) + ' | ').replace(right_rep, ' | ' + 'N/A'.center(len(right_rep) - 7) + ' || ').replace(far_right_rep, '|| ' + 'N/A'.center(len(far_right_rep) - 3)).replace(far_far_right_rep, '| ' + 'N/A'.center(len(far_far_right_rep) - 2)) + +def make_table_string(times_dict, + descending=True, + tag="Time"): + if len(times_dict.keys()) == 0: return 'No timing data' + # We first get the names of all of the compiled files, sorted by + # duration + names = get_sorted_file_list_from_times_dict(times_dict, descending=descending) + # compute the widths of the columns + times_width = max(max(map(len, times_dict.values())), len(sum_times(times_dict.values()))) + names_width = max(map(len, names + ["File Name", "Total"])) + format_string = "%%-%ds | %%-%ds" % (times_width, names_width) + header = format_string % (tag, "File Name") + total = format_string % (sum_times(times_dict.values()), + "Total") + sep = '-' * len(header) + return '\n'.join([header, sep, total, sep] + + [format_string % (times_dict[name], + name) + for name in names]) + +def print_or_write_table(table, files): + if len(files) == 0 or '-' in files: + try: + binary_stdout = sys.stdout.buffer + except AttributeError: + binary_stdout = sys.stdout + print(table.encode("utf-8"), file=binary_stdout) + for file_name in files: + if file_name != '-': + with open(file_name, 'w', encoding="utf-8") as f: + f.write(table) diff --git a/tools/beautify-archive b/tools/beautify-archive index 6bfa974a..a327ea44 100755 --- a/tools/beautify-archive +++ b/tools/beautify-archive @@ -23,7 +23,7 @@ cp -pr /tmp/$OLDARCHIVE.$$ $NEWARCHIVE cd $NEWARCHIVE rm description || true make clean -make COQFLAGS='-beautify -q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)' || \ +make COQFLAGS='-beautify -q $(OPT) $(COQLIBS) $(OTHERFLAGS)' || \ { echo ---- Failed to beautify; exit 1; } echo -------- Upgrading files in the beautification directory -------------- beaufiles=`find . -name \*.v$BEAUTIFYSUFFIX` diff --git a/tools/check-translate b/tools/check-translate index 3dd82405..acb6f459 100755 --- a/tools/check-translate +++ b/tools/check-translate @@ -2,7 +2,7 @@ echo -------------- Producing translated files --------------------- rm */*/*.v8 >& /dev/null -make COQ_XML=-translate theories || { echo ---- Failed to translate; exit 1; } +make COQOPTS=-translate theories || { echo ---- Failed to translate; exit 1; } if [ -e translated ]; then rm -r translated; fi if [ -e successful-translation ]; then rm -r successful-translation; fi if [ -e failed-translation ]; then rm -r failed-translation; fi diff --git a/tools/coq-inferior.el b/tools/coq-inferior.el deleted file mode 100644 index b79d97d6..00000000 --- a/tools/coq-inferior.el +++ /dev/null @@ -1,324 +0,0 @@ -;;; inferior-coq.el --- Run an inferior Coq process. -;;; -;;; Copyright (C) Marco Maggesi -;;; Time-stamp: "2002-02-28 12:15:04 maggesi" - - -;; Emacs Lisp Archive Entry -;; Filename: inferior-coq.el -;; Version: 1.0 -;; Keywords: process coq -;; Author: Marco Maggesi -;; Maintainer: Marco Maggesi -;; Description: Run an inferior Coq process. -;; URL: http://www.math.unifi.it/~maggesi/ -;; Compatibility: Emacs20, Emacs21, XEmacs21 - -;; This is free software; you can redistribute it and/or modify it under -;; the terms of the GNU General Public License as published by the Free -;; Software Foundation; either version 2, or (at your option) any later -;; version. -;; -;; This is distributed in the hope that it will be useful, but WITHOUT -;; ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or -;; FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License -;; for more details. -;; -;; You should have received a copy of the GNU General Public License -;; along with GNU Emacs; see the file COPYING. If not, write to the -;; Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, -;; MA 02111-1307, USA. - -;;; Commentary: - -;; Coq is a proof assistant (http://coq.inria.fr/). This code run an -;; inferior Coq process and defines functions to send bits of code -;; from other buffers to the inferior process. This is a -;; customisation of comint-mode (see comint.el). For a more complex -;; and full featured Coq interface under Emacs look at Proof General -;; (http://zermelo.dcs.ed.ac.uk/~proofgen/). -;; -;; Written by Marco Maggesi with code heavly -;; borrowed from emacs cmuscheme.el -;; -;; Please send me bug reports, bug fixes, and extensions, so that I can -;; merge them into the master source. - -;;; Installation: - -;; You need to have gallina.el already installed (it comes with the -;; standard Coq distribution) in order to use this code. Put this -;; file somewhere in you load-path and add the following lines in your -;; "~/.emacs": -;; -;; (setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist)) -;; (autoload 'coq-mode "gallina" "Major mode for editing Coq vernacular." t) -;; (autoload 'run-coq "inferior-coq" "Run an inferior Coq process." t) -;; (autoload 'run-coq-other-window "inferior-coq" -;; "Run an inferior Coq process in a new window." t) -;; (autoload 'run-coq-other-frame "inferior-coq" -;; "Run an inferior Coq process in a new frame." t) - -;;; Usage: - -;; Call `M-x "run-coq'. -;; -;; Functions and key bindings (Learn more keys with `C-c C-h' or `C-h m'): -;; C-return ('M-x coq-send-line) send the current line. -;; C-c C-r (`M-x coq-send-region') send the current region. -;; C-c C-a (`M-x coq-send-abort') send the command "Abort". -;; C-c C-t (`M-x coq-send-restart') send the command "Restart". -;; C-c C-s (`M-x coq-send-show') send the command "Show". -;; C-c C-u (`M-x coq-send-undo') send the command "Undo". -;; C-c C-v (`M-x coq-check-region') run command "Check" on region. -;; C-c . (`M-x coq-come-here') Restart and send until current point. - -;;; Change Log: - -;; From -0.0 to 1.0 brought into existence. - - -(require 'gallina) -(require 'comint) - -(setq coq-program-name "coqtop") - -(defgroup inferior-coq nil - "Run a coq process in a buffer." - :group 'coq) - -(defcustom inferior-coq-mode-hook nil - "*Hook for customising inferior-coq mode." - :type 'hook - :group 'coq) - -(defvar inferior-coq-mode-map - (let ((m (make-sparse-keymap))) - (define-key m "\C-c\C-r" 'coq-send-region) - (define-key m "\C-c\C-a" 'coq-send-abort) - (define-key m "\C-c\C-t" 'coq-send-restart) - (define-key m "\C-c\C-s" 'coq-send-show) - (define-key m "\C-c\C-u" 'coq-send-undo) - (define-key m "\C-c\C-v" 'coq-check-region) - m)) - -;; Install the process communication commands in the coq-mode keymap. -(define-key coq-mode-map [(control return)] 'coq-send-line) -(define-key coq-mode-map "\C-c\C-r" 'coq-send-region) -(define-key coq-mode-map "\C-c\C-a" 'coq-send-abort) -(define-key coq-mode-map "\C-c\C-t" 'coq-send-restart) -(define-key coq-mode-map "\C-c\C-s" 'coq-send-show) -(define-key coq-mode-map "\C-c\C-u" 'coq-send-undo) -(define-key coq-mode-map "\C-c\C-v" 'coq-check-region) -(define-key coq-mode-map "\C-c." 'coq-come-here) - -(defvar coq-buffer) - -(define-derived-mode inferior-coq-mode comint-mode "Inferior Coq" - "\ -Major mode for interacting with an inferior Coq process. - -The following commands are available: -\\{inferior-coq-mode-map} - -A Coq process can be fired up with M-x run-coq. - -Customisation: Entry to this mode runs the hooks on comint-mode-hook -and inferior-coq-mode-hook (in that order). - -You can send text to the inferior Coq process from other buffers -containing Coq source. - -Functions and key bindings (Learn more keys with `C-c C-h'): - C-return ('M-x coq-send-line) send the current line. - C-c C-r (`M-x coq-send-region') send the current region. - C-c C-a (`M-x coq-send-abort') send the command \"Abort\". - C-c C-t (`M-x coq-send-restart') send the command \"Restart\". - C-c C-s (`M-x coq-send-show') send the command \"Show\". - C-c C-u (`M-x coq-send-undo') send the command \"Undo\". - C-c C-v (`M-x coq-check-region') run command \"Check\" on region. - C-c . (`M-x coq-come-here') Restart and send until current point. -" - ;; Customise in inferior-coq-mode-hook - (setq comint-prompt-regexp "^[^<]* < *") - (coq-mode-variables) - (setq mode-line-process '(":%s")) - (setq comint-input-filter (function coq-input-filter)) - (setq comint-get-old-input (function coq-get-old-input))) - -(defcustom inferior-coq-filter-regexp "\\`\\s *\\S ?\\S ?\\s *\\'" - "*Input matching this regexp are not saved on the history list. -Defaults to a regexp ignoring all inputs of 0, 1, or 2 letters." - :type 'regexp - :group 'inferior-coq) - -(defun coq-input-filter (str) - "Don't save anything matching `inferior-coq-filter-regexp'." - (not (string-match inferior-coq-filter-regexp str))) - -(defun coq-get-old-input () - "Snarf the sexp ending at point." - (save-excursion - (let ((end (point))) - (backward-sexp) - (buffer-substring (point) end)))) - -(defun coq-args-to-list (string) - (let ((where (string-match "[ \t]" string))) - (cond ((null where) (list string)) - ((not (= where 0)) - (cons (substring string 0 where) - (coq-args-to-list (substring string (+ 1 where) - (length string))))) - (t (let ((pos (string-match "[^ \t]" string))) - (if (null pos) - nil - (coq-args-to-list (substring string pos - (length string))))))))) - -;;;###autoload -(defun run-coq (cmd) - "Run an inferior Coq process, input and output via buffer *coq*. -If there is a process already running in `*coq*', switch to that buffer. -With argument, allows you to edit the command line (default is value -of `coq-program-name'). Runs the hooks `inferior-coq-mode-hook' -\(after the `comint-mode-hook' is run). -\(Type \\[describe-mode] in the process buffer for a list of commands.)" - - (interactive (list (if current-prefix-arg - (read-string "Run Coq: " coq-program-name) - coq-program-name))) - (if (not (comint-check-proc "*coq*")) - (let ((cmdlist (coq-args-to-list cmd))) - (set-buffer (apply 'make-comint "coq" (car cmdlist) - nil (cdr cmdlist))) - (inferior-coq-mode))) - (setq coq-program-name cmd) - (setq coq-buffer "*coq*") - (switch-to-buffer "*coq*")) -;;;###autoload (add-hook 'same-window-buffer-names "*coq*") - -;;;###autoload -(defun run-coq-other-window (cmd) - "Run an inferior Coq process, input and output via buffer *coq*. -If there is a process already running in `*coq*', switch to that buffer. -With argument, allows you to edit the command line (default is value -of `coq-program-name'). Runs the hooks `inferior-coq-mode-hook' -\(after the `comint-mode-hook' is run). -\(Type \\[describe-mode] in the process buffer for a list of commands.)" - - (interactive (list (if current-prefix-arg - (read-string "Run Coq: " coq-program-name) - coq-program-name))) - (if (not (comint-check-proc "*coq*")) - (let ((cmdlist (coq-args-to-list cmd))) - (set-buffer (apply 'make-comint "coq" (car cmdlist) - nil (cdr cmdlist))) - (inferior-coq-mode))) - (setq coq-program-name cmd) - (setq coq-buffer "*coq*") - (pop-to-buffer "*coq*")) -;;;###autoload (add-hook 'same-window-buffer-names "*coq*") - -(defun run-coq-other-frame (cmd) - "Run an inferior Coq process, input and output via buffer *coq*. -If there is a process already running in `*coq*', switch to that buffer. -With argument, allows you to edit the command line (default is value -of `coq-program-name'). Runs the hooks `inferior-coq-mode-hook' -\(after the `comint-mode-hook' is run). -\(Type \\[describe-mode] in the process buffer for a list of commands.)" - - (interactive (list (if current-prefix-arg - (read-string "Run Coq: " coq-program-name) - coq-program-name))) - (if (not (comint-check-proc "*coq*")) - (let ((cmdlist (coq-args-to-list cmd))) - (set-buffer (apply 'make-comint "coq" (car cmdlist) - nil (cdr cmdlist))) - (inferior-coq-mode))) - (setq coq-program-name cmd) - (setq coq-buffer "*coq*") - (switch-to-buffer-other-frame "*coq*")) - -(defun switch-to-coq (eob-p) - "Switch to the coq process buffer. -With argument, position cursor at end of buffer." - (interactive "P") - (if (get-buffer coq-buffer) - (pop-to-buffer coq-buffer) - (error "No current process buffer. See variable `coq-buffer'")) - (cond (eob-p - (push-mark) - (goto-char (point-max))))) - -(defun coq-send-region (start end) - "Send the current region to the inferior Coq process." - (interactive "r") - (comint-send-region (coq-proc) start end) - (comint-send-string (coq-proc) "\n")) - -(defun coq-send-line () - "Send the current line to the Coq process." - (interactive) - (save-excursion - (end-of-line) - (let ((end (point))) - (beginning-of-line) - (coq-send-region (point) end))) - (next-line 1)) - -(defun coq-send-abort () - "Send the command \"Abort.\" to the inferior Coq process." - (interactive) - (comint-send-string (coq-proc) "Abort.\n")) - -(defun coq-send-restart () - "Send the command \"Restart.\" to the inferior Coq process." - (interactive) - (comint-send-string (coq-proc) "Restart.\n")) - -(defun coq-send-undo () - "Reset coq to the initial state and send the region between the - beginning of file and the point." - (interactive) - (comint-send-string (coq-proc) "Undo.\n")) - -(defun coq-check-region (start end) - "Run the commmand \"Check\" on the current region." - (interactive "r") - (comint-proc-query (coq-proc) - (concat "Check " - (buffer-substring start end) - ".\n"))) - -(defun coq-send-show () - "Send the command \"Show.\" to the inferior Coq process." - (interactive) - (comint-send-string (coq-proc) "Show.\n")) - -(defun coq-come-here () - "Reset coq to the initial state and send the region between the - beginning of file and the point." - (interactive) - (comint-send-string (coq-proc) "Reset Initial.\n") - (coq-send-region 1 (point))) - -(defvar coq-buffer nil "*The current coq process buffer.") - -(defun coq-proc () - "Return the current coq process. See variable `coq-buffer'." - (let ((proc (get-buffer-process (if (eq major-mode 'inferior-coq-mode) - (current-buffer) - coq-buffer)))) - (or proc - (error "No current process. See variable `coq-buffer'")))) - -(defcustom inferior-coq-load-hook nil - "This hook is run when inferior-coq is loaded in. -This is a good place to put keybindings." - :type 'hook - :group 'inferior-coq) - -(run-hooks 'inferior-coq-load-hook) - -(provide 'inferior-coq) diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index eab909f5..5402765f 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -1,24 +1,24 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* ) f g = fun x -> g (f x) + 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 +31,58 @@ 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"; +let usage_coq_makefile () = + 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"; + output_string stderr "\ +\nFull list of options:\ +\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 (recommended)\ +\n Output file outside the current directory is forbidden.\ +\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 +95,348 @@ 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"; - 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)"; + 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 quote s = if String.contains s ' ' || CString.is_empty s then "'" ^ s ^ "'" else s + +let generate_makefile oc conf_file local_file args project = + let makefile_template = + let template = "/tools/CoqMakefile.in" in + Envars.coqlib () ^ template in + let s = read_whole_file makefile_template in + let s = List.fold_left + (* We use global_substitute to avoid running into backslash issues due to \1 etc. *) + (fun s (k,v) -> Str.global_substitute (Str.regexp_string k) (fun _ -> 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; - 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"; + fprintf oc "%s %s %s\n\t%s\n\n" + target + (if List.mem target clean_tgts then ":: " else ": ") + dependencies + command + in + if sps <> [] then + section oc "Extra targets. (-extra and -extra-phony, DEPRECATED)"; + List.iter (forget_source > pr_path) sps + +let generate_conf_subdirs oc sds = + if sds <> [] then section oc "Subdirectories. (DEPRECATED)"; + let iter f = List.iter (forget_source > f) in + iter (fprintf oc ".PHONY:%s\n") sds; + iter (fprintf oc "post-all::\n\tcd \"%s\" && $(MAKE) all\n") sds; + iter (fprintf oc "clean::\n\tcd \"%s\" && $(MAKE) clean\n") sds; + iter (fprintf oc "archclean::\n\tcd \"%s\" && $(MAKE) archclean\n") sds; + 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 map = map_sourced_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)); + fprintf oc "COQMF_CMDLINE_COQLIBS = %s %s %s\n" + (S.concat " " (map_cmdline (fun { path } -> dash1 "I" path) ml_includes)) + (S.concat " " (map_cmdline (fun ({ path },l) -> dash2 "Q" path l) q_includes)) + (S.concat " " (map_cmdline (fun ({ path },l) -> dash2 "R" path l) r_includes)); +;; + +let windrive s = + if Coq_config.arch_is_win32 && Str.(string_match (regexp "^[a-zA-Z]:") s 0) + then Str.matched_string s + else "" +;; + +let generate_conf_coq_config oc args = + section oc "Coq configuration."; + let src_dirs = Coq_config.all_src_dirs in + Envars.print_config ~prefix_var_name:"COQMF_" oc src_dirs; + fprintf oc "COQMF_WINDRIVE=%s\n" (windrive Coq_config.coqlib) +;; + +let generate_conf_files oc + { v_files; mli_files; ml4_files; ml_files; mllib_files; mlpack_files; } += + let module S = String in + let map = map_sourced_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 cmdline_vfiles = filter_cmdline v_files in + fprintf oc "COQMF_CMDLINE_VFILES = %s\n" (S.concat " " (List.map quote cmdline_vfiles)); +;; + +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 (forget_source > 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.exists (fun x -> fst x.thing = "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 (forget_source > (fun (k,v) -> Printf.fprintf oc "%s = %s\n" k v)) defs; + Printf.fprintf oc "COQMF_OTHERFLAGS = %s\n" + (String.concat " " (List.map forget_source extra_args)) + +let generate_conf oc project args = + fprintf oc "# This configuration file was generated by running:\n"; + fprintf oc "# %s\n\n" (String.concat " " (List.map quote args)); + generate_conf_files oc project; + generate_conf_includes oc project; + generate_conf_coq_config oc args; + generate_conf_defs oc project; + generate_conf_doc oc project; + generate_conf_extra_target oc project.extra_targets; + generate_conf_subdirs oc project.subdirs; +;; + +let ensure_root_dir + ({ ml_includes; r_includes; q_includes; + v_files; ml_files; mli_files; ml4_files; + mllib_files; mlpack_files } as project) + = + let exists f = List.exists (forget_source > f) in + let here = Sys.getcwd () in + let not_tops = List.for_all (fun s -> s.thing <> Filename.basename s.thing) in + if exists (fun { canonical_path = x } -> x = here) ml_includes + || exists (fun ({ canonical_path = x },_) -> is_prefix x here) r_includes + || exists (fun ({ canonical_path = x },_) -> is_prefix x here) q_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 + project + else + let source x = {thing=x; source=CmdLine} in + let here_path = { path = "."; canonical_path = here } in + { project with + ml_includes = source here_path :: ml_includes; + r_includes = source (here_path, "Top") :: r_includes } +;; + +let warn_install_at_root_directory + ({ q_includes; r_includes; } as project) += + let open CList in + let inc_top_p = + map_filter + (fun {thing=({ path } ,ldir)} -> if ldir = "" then Some path else None) + (r_includes @ q_includes) in + let files = all_files project in + let bad = filter (fun f -> mem (Filename.dirname f.thing) 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.thing) bad; + eprintf "\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 $(patsubst %.v,.%.aux,$(VFILES))\n\n" in - print "archclean::\n"; - print "\trm -f *.cmx *.o\n"; - List.iter - (fun x -> print "\t+cd "; print x; print " && $(MAKE) archclean\n") - sds; - print "\n"; - print "printenv:\n\t@\"$(COQBIN)coqtop\" -config\n"; - print "\t@echo 'OCAMLFIND =\t$(OCAMLFIND)'\n\t@echo 'PP =\t$(PP)'\n\t@echo 'COQFLAGS =\t$(COQFLAGS)'\n"; - print "\t@echo 'COQLIBINSTALL =\t$(COQLIBINSTALL)'\n\t@echo 'COQDOCINSTALL =\t$(COQDOCINSTALL)'\n\n" - -let header_includes () = () - -let implicit () = - section "Implicit rules."; - let mli_rules () = - print "$(MLIFILES:.mli=.cmi): %.cmi: %.mli\n"; - print "\t$(SHOW)'CAMLC -c $<'\n"; - print "\t$(HIDE)$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; - print "$(addsuffix .d,$(MLIFILES)): %.mli.d: %.mli\n"; - print "\t$(SHOW)'CAMLDEP $<'\n"; - print "\t$(HIDE)$(CAMLDEP) $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" - in - let ml4_rules () = - print "$(ML4FILES:.ml4=.cmo): %.cmo: %.ml4\n"; - print "\t$(SHOW)'CAMLC -pp -c $<'\n"; - print "\t$(HIDE)$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n"; - print "$(filter-out $(addsuffix .cmx,$(foreach lib,$(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(ML4FILES:.ml4=.cmx)): %.cmx: %.ml4\n"; - print "\t$(SHOW)'CAMLOPT -pp -c $<'\n"; - print "\t$(HIDE)$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n"; - print "$(addsuffix .d,$(ML4FILES)): %.ml4.d: %.ml4\n"; - print "\t$(SHOW)'CAMLDEP -pp $<'\n"; - print "\t$(HIDE)$(CAMLDEP) $(OCAMLLIBS) $(PP) -impl \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in - let ml_rules () = - print "$(MLFILES:.ml=.cmo): %.cmo: %.ml\n"; - print "\t$(SHOW)'CAMLC -c $<'\n"; - print "\t$(HIDE)$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; - print "$(filter-out $(addsuffix .cmx,$(foreach lib,$(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(MLFILES:.ml=.cmx)): %.cmx: %.ml\n"; - print "\t$(SHOW)'CAMLOPT -c $<'\n"; - print "\t$(HIDE)$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; - print "$(addsuffix .d,$(MLFILES)): %.ml.d: %.ml\n"; - print "\t$(SHOW)'CAMLDEP $<'\n"; - print "\t$(HIDE)$(CAMLDEP) $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in - let cmxs_rules () = (* order is important here when there is foo.ml and foo.mllib *) - print "$(filter-out $(MLLIBFILES:.mllib=.cmxs),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs) $(MLPACKFILES:.mlpack=.cmxs)): %.cmxs: %.cmx\n"; - print "\t$(SHOW)'CAMLOPT -shared -o $@'\n"; - print "\t$(HIDE)$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $<\n\n"; - print "$(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa\n"; - print "\t$(SHOW)'CAMLOPT -shared -o $@'\n"; - print "\t$(HIDE)$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -linkall -shared -o $@ $<\n\n" - in - let mllib_rules () = - print "$(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib\n"; - print "\t$(SHOW)'CAMLC -a -o $@'\n"; - print "\t$(HIDE)$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n"; - print "$(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib\n"; - print "\t$(SHOW)'CAMLOPT -a -o $@'\n"; - print "\t$(HIDE)$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n"; - print "$(addsuffix .d,$(MLLIBFILES)): %.mllib.d: %.mllib\n"; - print "\t$(SHOW)'COQDEP $<'\n"; - print "\t$(HIDE)$(COQDEP) $(OCAMLLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" - in - let mlpack_rules () = - print "$(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack\n"; - print "\t$(SHOW)'CAMLC -pack -o $@'\n"; - print "\t$(HIDE)$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^\n\n"; - print "$(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack\n"; - print "\t$(SHOW)'CAMLOPT -pack -o $@'\n"; - print "\t$(HIDE)$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^\n\n"; - print "$(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack\n"; - print "\t$(SHOW)'COQDEP $<'\n"; - print "\t$(HIDE)$(COQDEP) $(OCAMLLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" +let check_overlapping_include { q_includes; r_includes } = + let pwd = Sys.getcwd () in + let aux = function + | [] -> () + | {thing = { 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 {thing={ 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 - 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" + 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 {thing={ canonical_path }, logic} -> + if is_prefix canonical_path file_dir then + Some(mk_destination logic canonical_path) + else None) includes 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"; + match candidates with + | [] -> + (* BACKWARD COMPATIBILITY: -I into the only logical root *) + begin match + r_includes, + List.find (fun {thing={ canonical_path = p }} -> is_prefix p file_dir) + ml_includes + with + | [{thing={ canonical_path }, logic}], {thing={ 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 _fhandle = Feedback.(add_feeder (console_feedback_listener Format.err_formatter)) in + let prog, args = + let args = Array.to_list Sys.argv in + let prog = List.hd args in + prog, List.tl args in + + 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_coq_makefile () in + + if only_destination <> None then begin + destination_of project (Option.get only_destination); + exit 0 end; - print "\n" -let double_colon = ["clean"; "cleanall"; "archclean"] + 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 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."; - List.iter pr_path sps + let conf_file = Option.default "CoqMakefile" project.makefile ^ ".conf" in + let local_file = Option.default "CoqMakefile" project.makefile ^ ".local" in -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 + 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; - 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; + + if project.subdirs <> [] then begin + eprintf "Warning: Subdirectories are deprecated.\n"; + eprintf "Warning: Use double colon rules in %s.\n\n" local_file; 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; + + let project = ensure_root_dir project in + + if project.install_kind <> (Some CoqProject_file.NoInstall) then begin + warn_install_at_root_directory project; 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 ## -## 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 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) - then - inc - 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 check_overlapping_include (_,inc_i,inc_r) = - 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 - in - List.iter (fun (_,dependencies,_,_) -> - List.iter check_dep (Str.split (Str.regexp "[ \t]+") dependencies)) sps; + check_overlapping_include project; - let inc = ensure_root_dir targets inc in - if is_install <> Project_file.NoInstall then begin - warn_install_at_root_directory targets inc; - 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; + Envars.set_coqlib ~fail:(fun x -> Printf.eprintf "Error: %s\n" x; exit 1); + + 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/coq_tex.ml b/tools/coq_tex.ml index e17011b3..0ffa5bd7 100644 --- a/tools/coq_tex.ml +++ b/tools/coq_tex.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 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" | "--print-version") :: _ -> + Usage.machine_readable_version 0 (* Options for coqtop : a) options with 0 argument *) - | ("-notactics"|"-bt"|"-debug"|"-nolib"|"-boot"|"-time"|"-profile-ltac" + | ("-bt"|"-debug"|"-nolib"|"-boot"|"-time"|"-profile-ltac" |"-batch"|"-noinit"|"-nois"|"-noglob"|"-no-glob" - |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet" - |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-beautify"|"-strict-implicit" - |"-dont-load-proofs"|"-load-proofs"|"-force-load-proofs" + |"-q"|"-profile"|"-echo" |"-quiet" + |"-silent"|"-m"|"-beautify"|"-strict-implicit" |"-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 @@ -106,7 +111,7 @@ let parse_args () = |"-load-ml-source"|"-require"|"-load-ml-object" |"-init-file"|"-dump-glob"|"-compat"|"-coqlib"|"-top" |"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs" |"-w" - |"-o"|"-profile-ltac-cutoff" + |"-o"|"-profile-ltac-cutoff"|"-mangle-names" as o) :: rem -> begin match rem with diff --git a/tools/coqdep.ml b/tools/coqdep.ml index a7c32e1d..12b5cab0 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 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,9 +443,10 @@ 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 " -f file : read -I, -Q, -R and filenames from _CoqProject-formatted FILE."; eprintf " -I dir -as logname : add (non recursively) dir to coq load path under logical name logname\n"; eprintf " -I dir : add (non recursively) dir to ocaml path\n"; eprintf " -R dir -as logname : add and import dir recursively to coq load path under logical name logname\n"; (* deprecate? *) @@ -449,10 +458,24 @@ 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\n"; exit 1 let split_period = Str.split (Str.regexp (Str.quote ".")) +let add_q_include path l = add_rec_dir_no_import add_known path (split_period l) + +let add_r_include path l = add_rec_dir_import add_known path (split_period l) + +let treat_coqproject f = + let open CoqProject_file in + let iter_sourced f = List.iter (fun {thing} -> f thing) in + let project = read_project_file f in + iter_sourced (fun { path } -> add_caml_dir path) project.ml_includes; + iter_sourced (fun ({ path }, l) -> add_q_include path l) project.q_includes; + iter_sourced (fun ({ path }, l) -> add_r_include path l) project.r_includes; + iter_sourced (fun f -> treat_file None f) (all_files project) + let rec parse = function | "-c" :: ll -> option_c := true; parse ll | "-D" :: ll -> option_D := true; parse ll @@ -460,10 +483,11 @@ let rec parse = function | "-boot" :: ll -> option_boot := true; parse ll | "-sort" :: ll -> option_sort := true; parse ll | ("-noglob" | "-no-glob") :: ll -> option_noglob := true; parse ll + | "-f" :: f :: ll -> treat_coqproject f; parse ll | "-I" :: r :: ll -> add_caml_dir r; parse ll | "-I" :: [] -> usage () - | "-R" :: r :: ln :: ll -> add_rec_dir_import add_known r (split_period ln); parse ll - | "-Q" :: r :: ln :: ll -> add_rec_dir_no_import add_known r (split_period ln); parse ll + | "-R" :: r :: ln :: ll -> add_r_include r ln; parse ll + | "-Q" :: r :: ln :: ll -> add_q_include r ln; parse ll | "-R" :: ([] | [_]) -> usage () | "-dumpgraph" :: f :: ll -> option_dump := Some (false, f); parse ll | "-dumpgraphbox" :: f :: ll -> option_dump := Some (true, f); parse ll @@ -476,17 +500,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 +524,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 +555,5 @@ let _ = try coqdep () with CErrors.UserError(s,p) -> - let pp = if s <> "_" then Pp.(str s ++ str ": " ++ p) else p in - Feedback.msg_error pp + let pp = (match s with | None -> p | Some s -> Pp.(str s ++ str ": " ++ p)) in + Format.eprintf "%a@\n%!" Pp.pp_with pp diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml index 6fc82683..aa023e69 100644 --- a/tools/coqdep_boot.ml +++ b/tools/coqdep_boot.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 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 0064aebd..db69a3b7 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* "." | Some s -> nf s in + let s' = match s' with None -> "." | Some s' -> nf s' in + s = s' + let warning_ml_clash x s suff s' suff' = - if suff = suff' then + if suff = suff' && not (same_path_opt s s') then eprintf "*** Warning: %s%s already found in %s (discarding %s%s)\n" x suff (match s with None -> "." | Some d -> d) @@ -219,7 +237,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 +310,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 +397,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 +466,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 +476,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 +571,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 633c474a..d0d79324 100644 --- a/tools/coqdep_common.mli +++ b/tools/coqdep_common.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 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 +69,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.mli b/tools/coqdep_lexer.mli index bb17fdf9..0e2b332f 100644 --- a/tools/coqdep_lexer.mli +++ b/tools/coqdep_lexer.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* s + | Some _ -> syntax_error lexbuf + + let get_ident lexbuf = + let s = Lexing.lexeme lexbuf in check_valid lexbuf s + + let get_field_name lexbuf = + let s = Lexing.lexeme lexbuf in + check_valid lexbuf (String.sub s 1 (String.length s - 1)) + + [@@@ocaml.warning "-3"] (* String.uncapitalize_ascii since 4.03.0 GPR#124 *) + let uncapitalize = String.uncapitalize + [@@@ocaml.warning "+3"] } let space = [' ' '\t' '\n' '\r'] -let lowercase = ['a'-'z' '\223'-'\246' '\248'-'\255'] -let uppercase = ['A'-'Z' '\192'-'\214' '\216'-'\222'] -let identchar = - ['A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9'] +let lowercase = ['a'-'z'] +let uppercase = ['A'-'Z'] +let identchar = ['A'-'Z' 'a'-'z' '_' '\'' '0'-'9'] let caml_up_ident = uppercase identchar* let caml_low_ident = lowercase identchar* -let coq_firstchar = - (* This is only an approximation, refer to lib/util.ml for correct def *) - ['A'-'Z' 'a'-'z' '_'] | - (* superscript 1 *) - '\194' '\185' | - (* utf-8 latin 1 supplement *) - '\195' ['\128'-'\150'] | '\195' ['\152'-'\182'] | '\195' ['\184'-'\191'] | - (* utf-8 letters *) - '\206' (['\145'-'\161'] | ['\163'-'\187']) - '\226' ('\130' [ '\128'-'\137' ] (* subscripts *) - | '\129' [ '\176'-'\187' ] (* superscripts *) - | '\132' ['\128'-'\191'] | '\133' ['\128'-'\143']) -let coq_identchar = coq_firstchar | ['\'' '0'-'9'] -let coq_ident = coq_firstchar coq_identchar* +(* This is an overapproximation, we check correctness afterwards *) +let coq_ident = ['A'-'Z' 'a'-'z' '_' '\128'-'\255'] ['A'-'Z' 'a'-'z' '_' '\'' '0'-'9' '\128'-'\255']* let coq_field = '.' coq_ident let dot = '.' ( space+ | eof) @@ -70,7 +73,9 @@ let dot = '.' ( space+ | eof) rule coq_action = parse | "Require" space+ { require_modifiers None lexbuf } - | "Local"? "Declare" space+ "ML" space+ "Module" space+ + | "Local" space+ "Declare" space+ "ML" space+ "Module" space+ + { modules [] lexbuf } + | "Declare" space+ "ML" space+ "Module" space+ { modules [] lexbuf } | "Load" space+ { load_file lexbuf } @@ -97,7 +102,7 @@ and from_rule = parse | space+ { from_rule lexbuf } | coq_ident - { let from = coq_qual_id_tail [Lexing.lexeme lexbuf] lexbuf in + { let from = coq_qual_id_tail [get_ident lexbuf] lexbuf in consume_require (Some from) lexbuf } | eof { syntax_error lexbuf } @@ -154,7 +159,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 } @@ -236,7 +241,7 @@ and load_file = parse parse_dot lexbuf; Load (unquote_vfile_string s) } | coq_ident - { let s = lexeme lexbuf in skip_to_dot lexbuf; Load s } + { let s = get_ident lexbuf in skip_to_dot lexbuf; Load s } | eof { syntax_error lexbuf } | _ @@ -248,7 +253,7 @@ and require_file from = parse | space+ { require_file from lexbuf } | coq_ident - { let name = coq_qual_id_tail [Lexing.lexeme lexbuf] lexbuf in + { let name = coq_qual_id_tail [get_ident lexbuf] lexbuf in let qid = coq_qual_id_list [name] lexbuf in parse_dot lexbuf; Require (from, qid) } @@ -273,7 +278,7 @@ and coq_qual_id = parse | space+ { coq_qual_id lexbuf } | coq_ident - { coq_qual_id_tail [Lexing.lexeme lexbuf] lexbuf } + { coq_qual_id_tail [get_ident lexbuf] lexbuf } | _ { syntax_error lexbuf } @@ -283,7 +288,7 @@ and coq_qual_id_tail module_name = parse | space+ { coq_qual_id_tail module_name lexbuf } | coq_field - { coq_qual_id_tail (field_name (Lexing.lexeme lexbuf) :: module_name) lexbuf } + { coq_qual_id_tail (get_field_name lexbuf :: module_name) lexbuf } | eof { syntax_error lexbuf } | _ @@ -296,7 +301,7 @@ and coq_qual_id_list module_names = parse | space+ { coq_qual_id_list module_names lexbuf } | coq_ident - { let name = coq_qual_id_tail [Lexing.lexeme lexbuf] lexbuf in + { let name = coq_qual_id_tail [get_ident lexbuf] lexbuf in coq_qual_id_list (name :: module_names) lexbuf } | eof @@ -321,12 +326,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 f817ed5a..269c1a1d 100644 --- a/tools/coqdoc/alpha.ml +++ b/tools/coqdoc/alpha.ml @@ -1,14 +1,20 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 'A' | '\199' -> 'C' | '\200'..'\203' -> 'E' @@ -19,19 +25,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/alpha.mli b/tools/coqdoc/alpha.mli index f6d47a55..86303450 100644 --- a/tools/coqdoc/alpha.mli +++ b/tools/coqdoc/alpha.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 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 00000000..2c9b3fb8 --- /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/cpretty.mli b/tools/coqdoc/cpretty.mli index 58b19184..7732610f 100644 --- a/tools/coqdoc/cpretty.mli +++ b/tools/coqdoc/cpretty.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Cdglobals.coq_module -> unit diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index 919f37b9..1be440a7 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* >" space* nl { Output.verbatim_char inline '\n'; Output.stop_verbatim inline } | nl ">>" { Output.verbatim_char inline '\n'; Output.stop_verbatim inline } | ">>" { Output.stop_verbatim inline } - | "*)" { Output.stop_verbatim inline; backtrack lexbuf } + | "(*" { Output.verbatim_char inline '('; + Output.verbatim_char inline '*'; + verbatim (depth+1) inline lexbuf } + | "*)" { if (depth == 0) + then (Output.stop_verbatim inline; backtrack lexbuf) + else (Output.verbatim_char inline '*'; + Output.verbatim_char inline ')'; + verbatim (depth-1) inline lexbuf) } | eof { Output.stop_verbatim inline } - | _ { Output.verbatim_char inline (lexeme_char lexbuf 0); verbatim inline lexbuf } + | _ { Output.verbatim_char inline (lexeme_char lexbuf 0); verbatim depth inline lexbuf } and url = parse | "}}" { Output.url (Buffer.contents url_buffer) None; Buffer.clear url_buffer } diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml index 9be791a8..df493fdf 100644 --- a/tools/coqdoc/index.ml +++ b/tools/coqdoc/index.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Unknown @@ -155,10 +157,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 +203,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 +211,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/index.mli b/tools/coqdoc/index.mli index e44bbd59..5cd30138 100644 --- a/tools/coqdoc/index.mli +++ b/tools/coqdoc/index.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* on 9 & 10 Mar 2004: diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 82d3d62b..d2522700 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* %s" (translate s) let ident s loc = - if is_keyword s then begin - printf "%s" (translate s) - end else begin - try - match loc with - | None -> raise Not_found - | Some loc -> - reference (translate s) (Index.find (get_module false) loc) - with Not_found -> - if is_tactic s then - printf "%s" (translate s) - else - if !Cdglobals.interpolate && !in_doc (* always a var otherwise *) - then - try reference (translate s) (Index.find_string (get_module false) s) - with _ -> Tokens.output_tagged_ident_string s - else - Tokens.output_tagged_ident_string s - end + try + match loc with + | None -> raise Not_found + | Some loc -> + reference (translate s) (Index.find (get_module false) loc) + with Not_found -> + if is_tactic s then + printf "%s" (translate s) + else if is_keyword s then + printf "%s" (translate s) + else if !Cdglobals.interpolate && !in_doc (* always a var otherwise *) then + try reference (translate s) (Index.find_string (get_module false) s) + with Not_found -> Tokens.output_tagged_ident_string s + else + Tokens.output_tagged_ident_string s let proofbox () = printf "☐" @@ -846,7 +848,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 +866,7 @@ module Html = struct (* Impression de la table d'index *) let print_index_table_item i = - printf "\n%s Index\n" (String.capitalize i.idx_name); + printf "\n%s Index\n" (capitalize i.idx_name); List.iter (fun (c,l) -> if l <> [] then @@ -912,7 +914,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 "
\n

%s Index

\n" (String.capitalize i.idx_name); + printf "
\n

%s Index

\n" (capitalize i.idx_name); all_letters i end in diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli index 853bc29a..a8a50d75 100644 --- a/tools/coqdoc/output.mli +++ b/tools/coqdoc/output.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 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/coqdoc/tokens.ml b/tools/coqdoc/tokens.ml index b6a1057a..49f7ef2f 100644 --- a/tools/coqdoc/tokens.ml +++ b/tools/coqdoc/tokens.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Str.split spaces str - -let (/) = Filename.concat - -(** Which user files do we support (and propagate to ocamlopt) ? -*) -let supported_suffix f = match CUnix.get_extension f with - | ".ml" | ".cmx" | ".cmo" | ".cmxa" | ".cma" | ".c" -> true - | _ -> false - -(** From bytecode extension to native -*) -let native_suffix f = match CUnix.get_extension f with - | ".cmo" -> (Filename.chop_suffix f ".cmo") ^ ".cmx" - | ".cma" -> (Filename.chop_suffix f ".cma") ^ ".cmxa" - | ".a" -> f - | _ -> failwith ("File "^f^" has not extension .cmo, .cma or .a") - -(** 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) - -(** Run a command [prog] with arguments [args]. - We do not use [Sys.command] anymore, see comment in [CUnix.sys_command]. -*) -let run_command prog args = - match CUnix.sys_command prog args with - | Unix.WEXITED 127 -> failwith ("no such command "^prog) - | Unix.WEXITED n -> n - | Unix.WSIGNALED n -> failwith (prog^" killed by signal "^string_of_int n) - | Unix.WSTOPPED n -> failwith (prog^" stopped by signal "^string_of_int n) - - - -(** {6 Coqmktop options} *) - -let opt = ref false -let top = ref false -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} *) - -(** Since the Coq core .cma are given with their relative paths - (e.g. "lib/clib.cma"), we only need to include directories mentionned in - the temp main ml file below (for accessing the corresponding .cmi). *) - -let std_includes basedir = - let rebase d = match basedir with None -> d | Some base -> base / d in - ["-I"; rebase "."; - "-I"; rebase "lib"; - "-I"; rebase "toplevel"; - "-I"; rebase "kernel/byterun"; - "-I"; Envars.camlp4lib () ] @ - (if is_ocaml4 then ["-I"; "+compiler-libs"] else []) - -(** For the -R option, visit all directories under [dir] and add - corresponding -I to the [opts] option list (in reversed order) *) -let incl_all_subdirs dir opts = - let l = ref opts in - let add f = l := f :: "-I" :: !l in - let rec traverse dir = - if Sys.file_exists dir && Sys.is_directory dir then - let () = add dir in - let subdirs = try Sys.readdir dir with any -> [||] in - Array.iter (fun f -> traverse (dir/f)) subdirs - in - traverse dir; !l - - -(** {6 Objects to link} *) - -(** NB: dynlink is now always linked, it is used for loading plugins - and compiled vm code (see native-compiler). We now reject platforms - with ocamlopt but no dynlink.cmxa during ./configure, and give - instructions there about how to build a dummy dynlink.cmxa, - cf. dev/dynlink.ml. *) - -(** 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 libobjs = ocaml_libs @ camlp4_libs - -(** Toplevel objects *) - -let ocaml_topobjs = - if is_ocaml4 then - ["ocamlcommon.cma";"ocamlbytecomp.cma";"ocamltoplevel.cma"] - 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 topobjs = ocaml_topobjs @ camlp4_topobjs - -(** Coq Core objects *) - -let copts = (split_list Coq_config.osdeplibs) @ (split_list Tolink.copts) -let core_objs = split_list Tolink.core_objs -let core_libs = split_list Tolink.core_libs - -(** Build the list of files to link and the list of modules names -*) -let files_to_link userfiles = - let top = if !top then topobjs else [] in - let modules = List.map module_of_file (top @ core_objs @ userfiles) in - let objs = libobjs @ top @ core_libs in - let objs' = (if !opt then List.map native_suffix objs else objs) @ userfiles - in (modules, objs') - - -(** {6 Parsing of the command-line} *) - -let usage () = - prerr_endline "Usage: coqmktop files\ -\nFlags are:\ -\n -coqlib dir Specify where the Coq object files are\ -\n -ocamlfind dir Specify where the ocamlfind binary is\ -\n -camlp4bin dir Specify where the Camlp4/5 binaries are\ -\n -o exec-file Specify the name of the resulting toplevel\ -\n -boot Run in boot mode\ -\n -echo Print calls to external commands\ -\n -opt Compile in native code\ -\n -top Build Coq on a OCaml toplevel (incompatible with -opt)\ -\n -R dir Add recursively dir to OCaml search path\ -\n"; - exit 1 - -let parse_args () = - let rec parse (op,fl) = function - | [] -> List.rev op, List.rev fl - - (* Directories *) - | "-coqlib" :: d :: rem -> - Flags.coqlib_spec := true; Flags.coqlib := d ; parse (op,fl) rem - | "-ocamlfind" :: d :: rem -> - Flags.ocamlfind_spec := true; Flags.ocamlfind := d ; parse (op,fl) rem - | "-camlp4bin" :: d :: rem -> - Flags.camlp4bin_spec := true; Flags.camlp4bin := d ; parse (op,fl) rem - | "-R" :: d :: rem -> parse (incl_all_subdirs d op,fl) rem - | ("-coqlib"|"-camlbin"|"-camlp4bin"|"-R") :: [] -> usage () - - (* Boolean options of coqmktop *) - | "-boot" :: rem -> Flags.boot := true; parse (op,fl) rem - | "-opt" :: rem -> opt := true ; parse (op,fl) rem - | "-top" :: rem -> top := true ; parse (op,fl) rem - | "-no-start" :: rem -> no_start:=true; parse (op, fl) rem - | "-echo" :: rem -> echo := true ; parse (op,fl) rem - | ("-v8"|"-full" as o) :: rem -> - Printf.eprintf "warning: option %s deprecated\n" o; parse (op,fl) rem - - (* Extra options with arity 0 or 1, directly passed to ocamlc/ocamlopt *) - | ("-noassert"|"-compact"|"-g"|"-p"|"-thread"|"-dtypes" as o) :: rem -> - parse (o::op,fl) rem - | ("-cclib"|"-ccopt"|"-I"|"-o"|"-w" as o) :: rem' -> - begin - match rem' with - | a :: rem -> parse (a::o::op,fl) rem - | [] -> usage () - end - - | ("-h"|"-help"|"--help") :: _ -> usage () - | f :: rem when supported_suffix f -> parse (op,f::fl) rem - | f :: _ -> prerr_endline ("Don't know what to do with " ^ f); exit 1 - in - parse ([],[]) (List.tl (Array.to_list Sys.argv)) - - -(** {6 Temporary main file} *) - -(** remove the temporary main file -*) -let clean file = - let rm f = if Sys.file_exists f then Sys.remove f in - let basename = Filename.chop_suffix file ".ml" in - if not !echo then begin - rm file; - rm (basename ^ ".o"); - rm (basename ^ ".cmi"); - rm (basename ^ ".cmo"); - rm (basename ^ ".cmx") - end - -(** Initializes the kind of loading in the main program -*) -let declare_loading_string () = - if not !top then - "Mltop.remove ();;" - else - "begin try\ -\n (* Enable rectypes in the toplevel if it has the directive #rectypes *)\ -\n begin match Hashtbl.find Toploop.directive_table \"rectypes\" with\ -\n | Toploop.Directive_none f -> f ()\ -\n | _ -> ()\ -\n end\ -\n with\ -\n | Not_found -> ()\ -\n end;;\ -\n\ -\n let ppf = Format.std_formatter;;\ -\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 Mltop.use_file=Topdirs.dir_use ppf;\ -\n Mltop.add_dir=Topdirs.dir_directory;\ -\n Mltop.ml_loop=(fun () -> Toploop.loop ppf) };;\ -\n" - -(** create a temporary main file to link -*) -let create_tmp_main_file modules = - let main_name,oc = Filename.open_temp_file "coqmain" ".ml" in - try - (* Add the pre-linked modules *) - output_string oc "List.iter Mltop.add_known_module [\""; - output_string oc (String.concat "\";\"" modules); - output_string oc "\"];;\n"; - (* Initializes the kind of loading *) - output_string oc (declare_loading_string()); - (* Start the toplevel loop *) - if not !no_start then output_string oc "Coqtop.start();;\n"; - close_out oc; - main_name - with reraise -> - clean main_name; raise reraise - - -(** {6 Main } *) - -let main () = - let (options, userfiles) = parse_args () in - (* Directories: *) - let () = Envars.set_coqlib ~fail:CErrors.error 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 !"; - 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 - let main_file = create_tmp_main_file modules in - try - (* - We add topstart.cmo explicitly because we shunted ocamlmktop wrapper. - - With the coq .cma, we MUST use the -linkall option. *) - let args = - "-linkall" :: "-rectypes" :: "-w" :: "-31" :: flags @ copts @ options @ - (std_includes basedir) @ tolink @ [ main_file ] @ topstart - in - if !echo then begin - let command = String.concat " " (Envars.ocamlfind ()::prog::args) in - print_endline command; - print_endline - ("(command length is " ^ - (string_of_int (String.length command)) ^ " characters)"); - flush Pervasives.stdout - end; - let exitcode = run_command (Envars.ocamlfind ()) (prog::args) in - clean main_file; - exitcode - with reraise -> clean main_file; raise reraise - -let pr_exn = function - | Failure msg -> msg - | Unix.Unix_error (err,fn,arg) -> fn^" "^arg^" : "^Unix.error_message err - | any -> Printexc.to_string any - -let _ = - try exit (main ()) - with any -> Printf.eprintf "Error: %s\n" (pr_exn any); exit 1 diff --git a/tools/coqwc.mll b/tools/coqwc.mll index b4fc738d..f0f13874 100644 --- a/tools/coqwc.mll +++ b/tools/coqwc.mll @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 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 d7bdf907..68aadcfc 100644 --- a/tools/coqworkmgr.ml +++ b/tools/coqworkmgr.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* List.rev acc, [] - | (_, { priority = Flags.Low }) :: _ as l -> List.rev acc, l + | (_, { priority = Low }) :: _ as l -> List.rev acc, l | x :: xs -> split (x :: acc) xs let push (_,{ priority } as item) q = - if priority = Flags.Low then q := !q @ [item] + if priority = Low then q := !q @ [item] else let high, low = split [] !q in q := high @ (item :: low) @@ -72,10 +74,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 @@ -145,7 +150,7 @@ let check_alive s = | Some s -> let cout = Unix.out_channel_of_descr s in set_binary_mode_out cout true; - output_string cout (print_request (Hello Flags.Low)); flush cout; + output_string cout (print_request (Hello Low)); flush cout; output_string cout (print_request Ping); flush cout; begin match Unix.select [s] [] [] 1.0 with | [s],_,_ -> diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml index 8fcca535..d48c6d0a 100644 --- a/tools/fake_ide.ml +++ b/tools/fake_ide.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 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 +30,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 +174,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 +187,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 +199,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); @@ -261,16 +249,14 @@ let eval_print l coq = let to_id, need_unfocus = get_id id in after_edit_at (to_id, need_unfocus) (base_eval_call (edit_at to_id) coq) | [ Tok(_,"QUERY"); Top []; Tok(_,phrase) ] -> - eval_call (query (phrase,tip_id())) coq + eval_call (query (0,(phrase,tip_id()))) coq | [ Tok(_,"QUERY"); Top [Tok(_,id)]; Tok(_,phrase) ] -> let to_id, _ = get_id id in - eval_call (query (phrase, to_id)) coq + eval_call (query (0,(phrase, to_id))) coq | [ Tok(_,"WAIT") ] -> - let phrase = "Stm Wait." in - eval_call (query (phrase,tip_id())) coq + eval_call (wait ()) coq | [ Tok(_,"JOIN") ] -> - let phrase = "Stm JoinDocument." in - eval_call (query (phrase,tip_id())) coq + eval_call (status true) coq | [ Tok(_,"ASSERT"); Tok(_,"TIP"); Tok(_,id) ] -> let to_id, _ = get_id id in if not(Stateid.equal (Document.tip doc) to_id) then error "Wrong tip" @@ -304,17 +290,31 @@ let usage () = (Filename.basename Sys.argv.(0)) (Parser.print grammar)) -module Coqide = Spawn.Sync(struct end) +module Coqide = Spawn.Sync () let main = - Sys.set_signal Sys.sigpipe + if Sys.os_type = "Unix" then Sys.set_signal Sys.sigpipe (Sys.Signal_handle (fun _ -> prerr_endline "Broken Pipe (coqtop died ?)"; exit 1)); - let coqtop_name, coqtop_args, input_file = match Sys.argv with - | [| _; f |] -> "coqtop",[|"-ideslave"|], f + let def_args = ["--xml_format=Ppcmds"; "-ideslave"] in + let coqtop_name = (* from ide/ideutils.ml *) + let prog_name = "fake_ide" in + let len_prog_name = String.length prog_name in + let fake_ide_path = Sys.executable_name in + let fake_ide_path_len = String.length fake_ide_path in + let pos = fake_ide_path_len - len_prog_name in + let rex = Str.regexp_string prog_name in + try + let i = Str.search_backward rex fake_ide_path pos in + String.sub fake_ide_path 0 i ^ "coqtop" ^ + String.sub fake_ide_path (i + len_prog_name) + (fake_ide_path_len - i - len_prog_name) + with Not_found -> assert false in + let coqtop_args, input_file = match Sys.argv with + | [| _; f |] -> 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 + Array.of_list (def_args @ ct), f | _ -> usage () in let inc = if input_file = "-" then stdin else open_in input_file in let coq = @@ -334,7 +334,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-db.el b/tools/gallina-db.el index baabebb1..9664f69f 100644 --- a/tools/gallina-db.el +++ b/tools/gallina-db.el @@ -163,7 +163,7 @@ for DB structure." (defun coq-sort-menu-entries (menu) (sort menu - '(lambda (x y) (string< + (lambda (x y) (string< (downcase (elt x 0)) (downcase (elt y 0)))))) diff --git a/tools/gallina-syntax.el b/tools/gallina-syntax.el index c25abece..662762b0 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.ml b/tools/gallina.ml index 0bf98a8f..c7ff76be 100644 --- a/tools/gallina.ml +++ b/tools/gallina.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* +;;; Time-stamp: "2002-02-28 12:15:04 maggesi" + + +;; Emacs Lisp Archive Entry +;; Filename: inferior-coq.el +;; Version: 1.0 +;; Keywords: process coq +;; Author: Marco Maggesi +;; Maintainer: Marco Maggesi +;; Description: Run an inferior Coq process. +;; URL: http://www.math.unifi.it/~maggesi/ +;; Compatibility: Emacs20, Emacs21, XEmacs21 + +;; This is free software; you can redistribute it and/or modify it under +;; the terms of the GNU General Public License as published by the Free +;; Software Foundation; either version 2, or (at your option) any later +;; version. +;; +;; This is distributed in the hope that it will be useful, but WITHOUT +;; ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or +;; FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License +;; for more details. +;; +;; You should have received a copy of the GNU General Public License +;; along with GNU Emacs; see the file COPYING. If not, write to the +;; Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, +;; MA 02111-1307, USA. + +;;; Commentary: + +;; Coq is a proof assistant (http://coq.inria.fr/). This code run an +;; inferior Coq process and defines functions to send bits of code +;; from other buffers to the inferior process. This is a +;; customisation of comint-mode (see comint.el). For a more complex +;; and full featured Coq interface under Emacs look at Proof General +;; (http://zermelo.dcs.ed.ac.uk/~proofgen/). +;; +;; Written by Marco Maggesi with code heavly +;; borrowed from emacs cmuscheme.el +;; +;; Please send me bug reports, bug fixes, and extensions, so that I can +;; merge them into the master source. + +;;; Installation: + +;; You need to have gallina.el already installed (it comes with the +;; standard Coq distribution) in order to use this code. Put this +;; file somewhere in you load-path and add the following lines in your +;; "~/.emacs": +;; +;; (setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist)) +;; (autoload 'coq-mode "gallina" "Major mode for editing Coq vernacular." t) +;; (autoload 'run-coq "inferior-coq" "Run an inferior Coq process." t) +;; (autoload 'run-coq-other-window "inferior-coq" +;; "Run an inferior Coq process in a new window." t) +;; (autoload 'run-coq-other-frame "inferior-coq" +;; "Run an inferior Coq process in a new frame." t) + +;;; Usage: + +;; Call `M-x "run-coq'. +;; +;; Functions and key bindings (Learn more keys with `C-c C-h' or `C-h m'): +;; C-return ('M-x coq-send-line) send the current line. +;; C-c C-r (`M-x coq-send-region') send the current region. +;; C-c C-a (`M-x coq-send-abort') send the command "Abort". +;; C-c C-t (`M-x coq-send-restart') send the command "Restart". +;; C-c C-s (`M-x coq-send-show') send the command "Show". +;; C-c C-u (`M-x coq-send-undo') send the command "Undo". +;; C-c C-v (`M-x coq-check-region') run command "Check" on region. +;; C-c . (`M-x coq-come-here') Restart and send until current point. + +;;; Change Log: + +;; From -0.0 to 1.0 brought into existence. + + +(require 'gallina) +(require 'comint) + +(setq coq-program-name "coqtop") + +(defgroup inferior-coq nil + "Run a coq process in a buffer." + :group 'coq) + +(defcustom inferior-coq-mode-hook nil + "*Hook for customising inferior-coq mode." + :type 'hook + :group 'coq) + +(defvar inferior-coq-mode-map + (let ((m (make-sparse-keymap))) + (define-key m "\C-c\C-r" 'coq-send-region) + (define-key m "\C-c\C-a" 'coq-send-abort) + (define-key m "\C-c\C-t" 'coq-send-restart) + (define-key m "\C-c\C-s" 'coq-send-show) + (define-key m "\C-c\C-u" 'coq-send-undo) + (define-key m "\C-c\C-v" 'coq-check-region) + m)) + +;; Install the process communication commands in the coq-mode keymap. +(define-key coq-mode-map [(control return)] 'coq-send-line) +(define-key coq-mode-map "\C-c\C-r" 'coq-send-region) +(define-key coq-mode-map "\C-c\C-a" 'coq-send-abort) +(define-key coq-mode-map "\C-c\C-t" 'coq-send-restart) +(define-key coq-mode-map "\C-c\C-s" 'coq-send-show) +(define-key coq-mode-map "\C-c\C-u" 'coq-send-undo) +(define-key coq-mode-map "\C-c\C-v" 'coq-check-region) +(define-key coq-mode-map "\C-c." 'coq-come-here) + +(defvar coq-buffer) + +(define-derived-mode inferior-coq-mode comint-mode "Inferior Coq" + "\ +Major mode for interacting with an inferior Coq process. + +The following commands are available: +\\{inferior-coq-mode-map} + +A Coq process can be fired up with M-x run-coq. + +Customisation: Entry to this mode runs the hooks on comint-mode-hook +and inferior-coq-mode-hook (in that order). + +You can send text to the inferior Coq process from other buffers +containing Coq source. + +Functions and key bindings (Learn more keys with `C-c C-h'): + C-return ('M-x coq-send-line) send the current line. + C-c C-r (`M-x coq-send-region') send the current region. + C-c C-a (`M-x coq-send-abort') send the command \"Abort\". + C-c C-t (`M-x coq-send-restart') send the command \"Restart\". + C-c C-s (`M-x coq-send-show') send the command \"Show\". + C-c C-u (`M-x coq-send-undo') send the command \"Undo\". + C-c C-v (`M-x coq-check-region') run command \"Check\" on region. + C-c . (`M-x coq-come-here') Restart and send until current point. +" + ;; Customise in inferior-coq-mode-hook + (setq comint-prompt-regexp "^[^<]* < *") + (coq-mode-variables) + (setq mode-line-process '(":%s")) + (setq comint-input-filter (function coq-input-filter)) + (setq comint-get-old-input (function coq-get-old-input))) + +(defcustom inferior-coq-filter-regexp "\\`\\s *\\S ?\\S ?\\s *\\'" + "*Input matching this regexp are not saved on the history list. +Defaults to a regexp ignoring all inputs of 0, 1, or 2 letters." + :type 'regexp + :group 'inferior-coq) + +(defun coq-input-filter (str) + "Don't save anything matching `inferior-coq-filter-regexp'." + (not (string-match inferior-coq-filter-regexp str))) + +(defun coq-get-old-input () + "Snarf the sexp ending at point." + (save-excursion + (let ((end (point))) + (backward-sexp) + (buffer-substring (point) end)))) + +(defun coq-args-to-list (string) + (let ((where (string-match "[ \t]" string))) + (cond ((null where) (list string)) + ((not (= where 0)) + (cons (substring string 0 where) + (coq-args-to-list (substring string (+ 1 where) + (length string))))) + (t (let ((pos (string-match "[^ \t]" string))) + (if (null pos) + nil + (coq-args-to-list (substring string pos + (length string))))))))) + +;;;###autoload +(defun run-coq (cmd) + "Run an inferior Coq process, input and output via buffer *coq*. +If there is a process already running in `*coq*', switch to that buffer. +With argument, allows you to edit the command line (default is value +of `coq-program-name'). Runs the hooks `inferior-coq-mode-hook' +\(after the `comint-mode-hook' is run). +\(Type \\[describe-mode] in the process buffer for a list of commands.)" + + (interactive (list (if current-prefix-arg + (read-string "Run Coq: " coq-program-name) + coq-program-name))) + (if (not (comint-check-proc "*coq*")) + (let ((cmdlist (coq-args-to-list cmd))) + (set-buffer (apply 'make-comint "coq" (car cmdlist) + nil (cdr cmdlist))) + (inferior-coq-mode))) + (setq coq-program-name cmd) + (setq coq-buffer "*coq*") + (switch-to-buffer "*coq*")) +;;;###autoload (add-hook 'same-window-buffer-names "*coq*") + +;;;###autoload +(defun run-coq-other-window (cmd) + "Run an inferior Coq process, input and output via buffer *coq*. +If there is a process already running in `*coq*', switch to that buffer. +With argument, allows you to edit the command line (default is value +of `coq-program-name'). Runs the hooks `inferior-coq-mode-hook' +\(after the `comint-mode-hook' is run). +\(Type \\[describe-mode] in the process buffer for a list of commands.)" + + (interactive (list (if current-prefix-arg + (read-string "Run Coq: " coq-program-name) + coq-program-name))) + (if (not (comint-check-proc "*coq*")) + (let ((cmdlist (coq-args-to-list cmd))) + (set-buffer (apply 'make-comint "coq" (car cmdlist) + nil (cdr cmdlist))) + (inferior-coq-mode))) + (setq coq-program-name cmd) + (setq coq-buffer "*coq*") + (pop-to-buffer "*coq*")) +;;;###autoload (add-hook 'same-window-buffer-names "*coq*") + +(defun run-coq-other-frame (cmd) + "Run an inferior Coq process, input and output via buffer *coq*. +If there is a process already running in `*coq*', switch to that buffer. +With argument, allows you to edit the command line (default is value +of `coq-program-name'). Runs the hooks `inferior-coq-mode-hook' +\(after the `comint-mode-hook' is run). +\(Type \\[describe-mode] in the process buffer for a list of commands.)" + + (interactive (list (if current-prefix-arg + (read-string "Run Coq: " coq-program-name) + coq-program-name))) + (if (not (comint-check-proc "*coq*")) + (let ((cmdlist (coq-args-to-list cmd))) + (set-buffer (apply 'make-comint "coq" (car cmdlist) + nil (cdr cmdlist))) + (inferior-coq-mode))) + (setq coq-program-name cmd) + (setq coq-buffer "*coq*") + (switch-to-buffer-other-frame "*coq*")) + +(defun switch-to-coq (eob-p) + "Switch to the coq process buffer. +With argument, position cursor at end of buffer." + (interactive "P") + (if (get-buffer coq-buffer) + (pop-to-buffer coq-buffer) + (error "No current process buffer. See variable `coq-buffer'")) + (cond (eob-p + (push-mark) + (goto-char (point-max))))) + +(defun coq-send-region (start end) + "Send the current region to the inferior Coq process." + (interactive "r") + (comint-send-region (coq-proc) start end) + (comint-send-string (coq-proc) "\n")) + +(defun coq-send-line () + "Send the current line to the Coq process." + (interactive) + (save-excursion + (end-of-line) + (let ((end (point))) + (beginning-of-line) + (coq-send-region (point) end))) + (forward-line 1)) + +(defun coq-send-abort () + "Send the command \"Abort.\" to the inferior Coq process." + (interactive) + (comint-send-string (coq-proc) "Abort.\n")) + +(defun coq-send-restart () + "Send the command \"Restart.\" to the inferior Coq process." + (interactive) + (comint-send-string (coq-proc) "Restart.\n")) + +(defun coq-send-undo () + "Reset coq to the initial state and send the region between the + beginning of file and the point." + (interactive) + (comint-send-string (coq-proc) "Undo.\n")) + +(defun coq-check-region (start end) + "Run the commmand \"Check\" on the current region." + (interactive "r") + (comint-proc-query (coq-proc) + (concat "Check " + (buffer-substring start end) + ".\n"))) + +(defun coq-send-show () + "Send the command \"Show.\" to the inferior Coq process." + (interactive) + (comint-send-string (coq-proc) "Show.\n")) + +(defun coq-come-here () + "Reset coq to the initial state and send the region between the + beginning of file and the point." + (interactive) + (comint-send-string (coq-proc) "Reset Initial.\n") + (coq-send-region 1 (point))) + +(defvar coq-buffer nil "*The current coq process buffer.") + +(defun coq-proc () + "Return the current coq process. See variable `coq-buffer'." + (let ((proc (get-buffer-process (if (eq major-mode 'inferior-coq-mode) + (current-buffer) + coq-buffer)))) + (or proc + (error "No current process. See variable `coq-buffer'")))) + +(defcustom inferior-coq-load-hook nil + "This hook is run when inferior-coq is loaded in. +This is a good place to put keybindings." + :type 'hook + :group 'inferior-coq) + +(run-hooks 'inferior-coq-load-hook) + +(provide 'inferior-coq) diff --git a/tools/make-both-single-timing-files.py b/tools/make-both-single-timing-files.py new file mode 100755 index 00000000..32c52c7a --- /dev/null +++ b/tools/make-both-single-timing-files.py @@ -0,0 +1,12 @@ +#!/usr/bin/env python +import sys +from TimeFileMaker import * + +if __name__ == '__main__': + USAGE = 'Usage: %s [--sort-by=auto|absolute|diff] AFTER_FILE_NAME BEFORE_FILE_NAME [OUTPUT_FILE_NAME ..]' % sys.argv[0] + HELP_STRING = r'''Formats timing information from the output of two invocations of `coqc -time` into a sorted table''' + sort_by, args = parse_args(sys.argv, USAGE, HELP_STRING) + left_dict = get_single_file_times(args[1]) + right_dict = get_single_file_times(args[2]) + table = make_diff_table_string(left_dict, right_dict, tag="Code", sort_by=sort_by) + print_or_write_table(table, args[3:]) diff --git a/tools/make-both-time-files.py b/tools/make-both-time-files.py new file mode 100755 index 00000000..f730a8d6 --- /dev/null +++ b/tools/make-both-time-files.py @@ -0,0 +1,16 @@ +#!/usr/bin/env python +import sys +from TimeFileMaker import * + +if __name__ == '__main__': + USAGE = 'Usage: %s [--sort-by=auto|absolute|diff] AFTER_FILE_NAME BEFORE_FILE_NAME [OUTPUT_FILE_NAME ..]' % sys.argv[0] + HELP_STRING = r'''Formats timing information from the output of two invocations of `make TIMED=1` into a sorted table. + +The input is expected to contain lines in the format: +FILE_NAME (...user: NUMBER_IN_SECONDS...) +''' + sort_by, args = parse_args(sys.argv, USAGE, HELP_STRING) + left_dict = get_times(args[1]) + right_dict = get_times(args[2]) + table = make_diff_table_string(left_dict, right_dict, sort_by=sort_by) + print_or_write_table(table, args[3:]) diff --git a/tools/make-one-time-file.py b/tools/make-one-time-file.py new file mode 100755 index 00000000..e66136df --- /dev/null +++ b/tools/make-one-time-file.py @@ -0,0 +1,21 @@ +#!/usr/bin/env python +import sys +from TimeFileMaker import * + +if __name__ == '__main__': + USAGE = 'Usage: %s FILE_NAME [OUTPUT_FILE_NAME ..]' % sys.argv[0] + HELP_STRING = r'''Formats timing information from the output of `make TIMED=1` into a sorted table. + +The input is expected to contain lines in the format: +FILE_NAME (...user: NUMBER_IN_SECONDS...) +''' + if len(sys.argv) < 2 or '--help' in sys.argv[1:] or '-h' in sys.argv[1:]: + print(USAGE) + if '--help' in sys.argv[1:] or '-h' in sys.argv[1:]: + print(HELP_STRING) + if len(sys.argv) == 2: sys.exit(0) + sys.exit(1) + else: + times_dict = get_times(sys.argv[1]) + table = make_table_string(times_dict) + print_or_write_table(table, sys.argv[2:]) diff --git a/tools/md5sum.ml b/tools/md5sum.ml new file mode 100644 index 00000000..2fdcacc8 --- /dev/null +++ b/tools/md5sum.ml @@ -0,0 +1,24 @@ +let get_content file = + let ic = open_in_bin file in + let buf = Buffer.create 2048 in + let rec fill () = + match input_char ic with + | '\r' -> fill () (* NOTE: handles the case on Windows where the + git checkout has included return characters. + See: https://github.com/coq/coq/pull/6305 *) + | c -> Buffer.add_char buf c; fill () + | exception End_of_file -> close_in ic; Buffer.contents buf + in + fill () + +let () = + match Sys.argv with + | [|_; file|] -> + let content = get_content file in + let md5 = Digest.to_hex (Digest.string content) in + print_string (md5 ^ " " ^ file) + | _ -> + prerr_endline "Error: This program needs exactly one parameter."; + prerr_endline "Usage: ocaml md5sum.ml "; + prerr_endline "Print MD5 (128-bit) checksum of the file content modulo \\r."; + exit 1 diff --git a/tools/ocamllibdep.mll b/tools/ocamllibdep.mll index bf82be09..382c39d3 100644 --- a/tools/ocamllibdep.mll +++ b/tools/ocamllibdep.mll @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* "." | Some s -> nf s in + let s' = match s' with None -> "." | Some s' -> nf s' in + s = s' + let warning_ml_clash x s suff s' suff' = - if suff = suff' then + if suff = suff' && not (same_path_opt s s') then eprintf "*** Warning: %s%s already found in %s (discarding %s%s)\n" x suff (match s with None -> "." | Some d -> d) @@ -185,7 +204,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 -- cgit v1.2.3