diff options
221 files changed, 1237 insertions, 561 deletions
diff --git a/.gitignore b/.gitignore index 5340f081dc..71de7bb8d0 100644 --- a/.gitignore +++ b/.gitignore @@ -9,6 +9,7 @@ *.spot *.o *.a +*.pyc *.log *.aux *.dvi @@ -35,6 +36,10 @@ *.tacind *.v.tex *.v.ps +*.v.timing +*.v.timing.diff +*.v.before-timing +*.v.after-timing *.v.html *.stamp *.native @@ -55,6 +60,10 @@ plugins/micromega/csdpcert plugins/micromega/.micromega.ml.generated kernel/byterun/dllcoqrun.so coqdoc.sty +time-of-build.log +time-of-build-pretty.log +time-of-build-before.log +time-of-build-after.log .csdp.cache test-suite/.lia.cache test-suite/.nra.cache @@ -63,8 +72,9 @@ test-suite/misc/universes/all_stdlib.v test-suite/misc/universes/universes.txt test-suite/coq-makefile/*/actual test-suite/coq-makefile/*/desired -test-suite/coq-makefile/*/Makefile -test-suite/coq-makefile/*/Makefile.conf +test-suite/coq-makefile/**/*.processed +test-suite/coq-makefile/**/Makefile +test-suite/coq-makefile/**/Makefile.conf test-suite/coq-makefile/*/src test-suite/coq-makefile/*/theories test-suite/coq-makefile/*/theories2 diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index e1feabd064..8b43d975ac 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -18,8 +18,10 @@ variables: # some useful values COMPILER_32BIT: "4.02.3+32bit" - COMPILER_BLEEDING_EDGE: "4.04.1" - CAMLP5_VER_BLEEDING_EDGE: "6.17" + COMPILER_BLEEDING_EDGE: "4.05.0" + CAMLP5_VER_BLEEDING_EDGE: "7.01" + + TEST_PACKAGES: "time python" COQIDE_PACKAGES: "libgtk2.0-dev libgtksourceview2.0-dev" #COQIDE_PACKAGES_32BIT: "libgtk2.0-dev:i386 libgtksourceview2.0-dev:i386" @@ -193,6 +195,8 @@ test-suite: <<: *test-suite-template dependencies: - build + variables: + EXTRA_PACKAGES: "$TEST_PACKAGES" test-suite:32bit: <<: *test-suite-template @@ -200,7 +204,7 @@ test-suite:32bit: - build:32bit variables: COMPILER: "$COMPILER_32BIT" - EXTRA_PACKAGES: "gcc-multilib" + EXTRA_PACKAGES: "gcc-multilib $TEST_PACKAGES" test-suite:bleeding-edge: <<: *test-suite-template @@ -209,6 +213,7 @@ test-suite:bleeding-edge: variables: COMPILER: "$COMPILER_BLEEDING_EDGE" CAMLP5_VER: "$CAMLP5_VER_BLEEDING_EDGE" + EXTRA_PACKAGES: "$TEST_PACKAGES" documentation: <<: *documentation-template diff --git a/.travis.yml b/.travis.yml index 6de63d387b..3cd7fdf5e3 100644 --- a/.travis.yml +++ b/.travis.yml @@ -95,8 +95,8 @@ matrix: - env: - TEST_TARGET="test-suite" - - COMPILER="4.04.1" - - CAMLP5_VER="6.17" + - COMPILER="4.05.0" + - CAMLP5_VER="7.01" - EXTRA_CONF="-coqide opt -with-doc yes" - EXTRA_OPAM="lablgtk-extras hevea" addons: @@ -124,8 +124,8 @@ matrix: - env: - TEST_TARGET="coqocaml" - - COMPILER="4.04.1" - - CAMLP5_VER="6.17" + - COMPILER="4.05.0" + - CAMLP5_VER="7.01" - EXTRA_CONF="-coqide opt -warn-error" - EXTRA_OPAM="lablgtk-extras hevea" # dummy target @@ -144,6 +144,7 @@ matrix: before_install: - brew update - brew install opam + - brew install gnu-time before_install: - if [ "${TRAVIS_PULL_REQUEST}" != "false" ]; then echo "Tested commit (followed by parent commits):"; git log -1; for commit in `git log -1 --format="%P"`; do echo; git log -1 $commit; done; fi diff --git a/API/API.ml b/API/API.ml index 093ca97f80..32c664d7b1 100644 --- a/API/API.ml +++ b/API/API.ml @@ -79,6 +79,7 @@ module Nametab = Nametab module Vernacentries = Vernacentries module Mltop = Mltop module Goal = Goal +module Proof_bullet = Proof_bullet module Proof_global = Proof_global module Proof = Proof module Smartlocate = Smartlocate diff --git a/API/API.mli b/API/API.mli index e8418552c4..b1a746e028 100644 --- a/API/API.mli +++ b/API/API.mli @@ -3449,6 +3449,11 @@ sig end end +module Proof_bullet : +sig + val get_default_goal_selector : unit -> Vernacexpr.goal_selector +end + module Proof_global : sig type proof_mode = Proof_global.proof_mode = { @@ -3483,7 +3488,6 @@ sig (unit Proofview.tactic -> Proof.proof -> Proof.proof) -> unit val compact_the_proof : unit -> unit val register_proof_mode : proof_mode -> unit - val get_default_goal_selector : unit -> Vernacexpr.goal_selector exception NoCurrentProof val give_me_the_proof : unit -> Proof.proof @@ -95,6 +95,11 @@ Tools The current version contains code for retro compatibility that prints warnings when a deprecated feature is used. Please upgrade your _CoqProject accordingly. + * Additionally, coq_makefile-made Makefiles now support experimental timing + targets `pretty-timed`, `pretty-timed-before`, `pretty-timed-after`, + `print-pretty-timed-diff`, `print-pretty-single-time-diff`, + `all.timing.diff`, and the variable `TIMING=1` (or `TIMING=before` or + `TIMING=after`); see the documentation for more details. Build Infrastructure @@ -17,7 +17,7 @@ # read # http://miller.emu.id.au/pmiller/books/rmch/ # before complaining. -# +# # When you are working in a subdir, you can compile without moving to the # upper directory using "make -C ..", and the output is still understood # by Emacs' next-error. @@ -168,7 +168,7 @@ Makefile $(wildcard Makefile.*) config/Makefile : ; # Cleaning ########################################################################### -.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide ml4clean depclean cleanconfig distclean voclean devdocclean +.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide ml4clean depclean cleanconfig distclean voclean timingclean devdocclean clean: objclean cruftclean depclean docclean devdocclean @@ -239,16 +239,19 @@ cacheclean: cleanconfig: rm -f config/Makefile config/coq_config.ml myocamlbuild_config.ml dev/ocamldebug-coq dev/camlp4.dbg config/Info-*.plist -distclean: clean cleanconfig cacheclean +distclean: clean cleanconfig cacheclean timingclean voclean: find theories plugins test-suite \( -name '*.vo' -o -name '*.glob' -o -name "*.cmxs" -o -name "*.native" -o -name "*.cmx" -o -name "*.cmi" -o -name "*.o" \) -delete find theories plugins test-suite -name .coq-native -empty -delete +timingclean: + find theories plugins test-suite \( -name '*.v.timing' -o -name '*.v.before-timing' -o -name "*.v.after-timing" -o -name "*.v.timing.diff" -o -name "time-of-build.log" -o -name "time-of-build-before.log" -o -name "time-of-build-after.log" -o -name "time-of-build-pretty.log" -o -name "time-of-build-both.log" \) -delete + devdocclean: find . -name '*.dep.ps' -o -name '*.dot' | xargs rm -f - rm -f $(OCAMLDOCDIR)/*.log $(OCAMLDOCDIR)/*.aux $(OCAMLDOCDIR)/*.toc - rm -f $(OCAMLDOCDIR)/ocamldoc.sty $(OCAMLDOCDIR)/coq.tex + rm -f $(OCAMLDOCDIR)/*.log $(OCAMLDOCDIR)/*.aux $(OCAMLDOCDIR)/*.toc + rm -f $(OCAMLDOCDIR)/ocamldoc.sty $(OCAMLDOCDIR)/coq.tex rm -f $(OCAMLDOCDIR)/html/*.html ########################################################################### @@ -299,4 +302,3 @@ printenv: @env | wc -L @echo -n "Total (win32 limit is 32k) : " @env | wc -m - diff --git a/Makefile.build b/Makefile.build index 05d751f541..7703df08fc 100644 --- a/Makefile.build +++ b/Makefile.build @@ -34,6 +34,12 @@ TIMED ?= # it could be set to "'/usr/bin/time -p'". TIMECMD ?= +# When non-empty, -time is passed to coqc and the output is recorded +# in a timing file for each .v file. If set to "before" or "after", +# the file name for foo.v is foo.v.$(TIMING)-timing; otherwise, it is +# foo.v.timing +TIMING ?= + # Non-empty skips the update of all dependency .d files: NO_RECALC_DEPS ?= @@ -43,6 +49,16 @@ VALIDATE ?= # Is "-xml" when building XML library: COQ_XML ?= +# 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 +BEFORE ?= +AFTER ?= + ########################################################################### # Default starting rule ########################################################################### @@ -53,6 +69,9 @@ world: coq coqide documentation revision coq: coqlib coqbinaries tools +world.timing.diff: coq.timing.diff +coq.timing.diff: coqlib.timing.diff + # Note: 'world' does not build the bytecode binaries anymore. # For that, you can use the 'byte' rule. Native and byte compilations # shouldn't be done in a same make -j... run, otherwise both ocamlc and @@ -60,7 +79,7 @@ coq: coqlib coqbinaries tools byte: coqbyte coqide-byte pluginsbyte printers -.PHONY: world coq byte +.PHONY: world coq byte world.timing.diff coq.timing.diff ########################################################################### # Includes @@ -78,6 +97,53 @@ include Makefile.install include Makefile.dev ## provides the 'printers' and 'revision' rules ########################################################################### +# Timing targets +########################################################################### +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 $(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) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_BUILD_AFTER_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 BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing' + $(HIDE)false +else +ifeq (,$(AFTER)) +print-pretty-single-time-diff:: + @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing' + $(HIDE)false +else +print-pretty-single-time-diff:: + $(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) $(BEFORE) $(AFTER) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) +endif +endif +pretty-timed: + $(HIDE)$(MAKE) --no-print-directory make-pretty-timed + $(HIDE)$(MAKE) --no-print-directory print-pretty-timed +.PHONY: pretty-timed make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff + +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 + +########################################################################### # This include below will lauch the build of all .d. # The - at front is for disabling warnings about currently missing ones. @@ -101,7 +167,21 @@ DEPENDENCIES := \ ########################################################################### # Default timing command -STDTIME=/usr/bin/time -f "$* (real: %e, user: %U, sys: %S, mem: %M ko)" +# Use /usr/bin/time on linux, gtime on Mac OS +TIMEFMT?="$* (real: %e, user: %U, sys: %S, mem: %M ko)" +ifneq (,$(TIMED)) +ifeq (0,$(shell /usr/bin/time -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?)) +STDTIME?=/usr/bin/time -f $(TIMEFMT) +else +ifeq (0,$(shell gtime -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?)) +STDTIME?=gtime -f $(TIMEFMT) +else +STDTIME?=time +endif +endif +else +STDTIME?=/usr/bin/time -f $(TIMEFMT) +endif TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) @@ -112,7 +192,7 @@ TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) COQOPTS=$(COQ_XML) $(NATIVECOMPUTE) BOOTCOQC=$(TIMER) $(COQTOPBEST) -boot $(COQOPTS) -compile -LOCALINCLUDES=$(if $(filter plugins/%,$<),-I lib -I API $(addprefix -I plugins/,$(PLUGINDIRS)),$(addprefix -I ,$(SRCDIRS))) +LOCALINCLUDES=$(if $(filter plugins/%,$<),-I lib -I API -open API $(addprefix -I plugins/,$(PLUGINDIRS)),$(addprefix -I ,$(SRCDIRS))) MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) OCAMLC := $(OCAMLFIND) ocamlc $(CAMLFLAGS) @@ -602,18 +682,28 @@ OCAMLDEP = $(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack # since they are all mentioned in at least one Declare ML Module in some .v coqlib: theories plugins +coqlib.timing.diff: theories.timing.diff plugins.timing.diff theories: $(THEORIESVO) plugins: $(PLUGINSVO) -.PHONY: coqlib theories plugins +theories.timing.diff: $(THEORIESVO:.vo=.v.timing.diff) +plugins.timing.diff: $(PLUGINSVO:.vo=.v.timing.diff) + +.PHONY: coqlib theories plugins coqlib.timing.diff theories.timing.diff plugins.timing.diff # The .vo files in Init are built with the -noinit option +ifneq (,$(TIMING)) +TIMING_EXTRA = > $<.$(TIMING_EXT) +else +TIMING_EXTRA = +endif + theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_DEP) $(SHOW)'COQC $(COQ_XML) -noinit $<' $(HIDE)rm -f theories/Init/$*.glob - $(HIDE)$(BOOTCOQC) $< $(COQ_XML) -noinit -R theories Coq + $(HIDE)$(BOOTCOQC) $< $(COQ_XML) -noinit -R theories Coq $(TIMING_ARG) $(TIMING_EXTRA) # MExtraction.v generates the ml core file of the micromega tactic. # We check that this generated code is still in sync with the version @@ -640,13 +730,18 @@ $(MICROMEGAV:.v=.vo) $(MICROMEGAV:.v=.glob) : $(MICROMEGAV) theories/Init/Prelud %.vo %.glob: %.v theories/Init/Prelude.vo $(VO_TOOLS_DEP) $(SHOW)'COQC $<' $(HIDE)rm -f $*.glob - $(HIDE)$(BOOTCOQC) $< + $(HIDE)$(BOOTCOQC) $< $(TIMING_ARG) $(TIMING_EXTRA) ifdef VALIDATE $(SHOW)'COQCHK $(call vo_to_mod,$@)' $(HIDE)$(CHICKEN) -boot -silent -norec $(call vo_to_mod,$@) \ || ( RV=$$?; rm -f "$@"; exit $${RV} ) endif +%.v.timing.diff: %.v.before-timing %.v.after-timing + $(SHOW)PYTHON TIMING-DIFF $< + $(HIDE)$(MAKE) --no-print-directory print-pretty-single-time-diff BEFORE=$*.v.before-timing AFTER=$*.v.after-timing TIME_OF_PRETTY_BUILD_FILE="$@" + + # Dependencies of .v files %.v.d: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) diff --git a/Makefile.common b/Makefile.common index 100698321a..85ecb1a08d 100644 --- a/Makefile.common +++ b/Makefile.common @@ -12,7 +12,7 @@ # Executables ########################################################################### -COQMKTOP:=bin/coqmktop$(EXE) +COQMKTOP:=bin/coqmktop$(EXE) COQTOPBYTE:=bin/coqtop.byte$(EXE) COQTOPEXE:=bin/coqtop$(EXE) @@ -25,9 +25,15 @@ COQWC:=bin/coqwc$(EXE) COQDOC:=bin/coqdoc$(EXE) COQC:=bin/coqc$(EXE) COQWORKMGR:=bin/coqworkmgr$(EXE) +COQMAKE_ONE_TIME_FILE:=tools/make-one-time-file.py +COQTIME_FILE_MAKER:=tools/TimeFileMaker.py +COQMAKE_BOTH_TIME_FILES:=tools/make-both-time-files.py +COQMAKE_BOTH_SINGLE_TIMING_FILES:=tools/make-both-single-timing-files.py TOOLS:=$(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) $(COQWC) $(COQDOC) $(COQC)\ $(COQWORKMGR) +TOOLS_HELPERS:=tools/CoqMakefile.in $(COQMAKE_ONE_TIME_FILE) $(COQTIME_FILE_MAKER)\ + $(COQMAKE_BOTH_TIME_FILES) $(COQMAKE_BOTH_SINGLE_TIMING_FILES) COQDEPBOOT:=bin/coqdep_boot$(EXE) OCAMLLIBDEP:=bin/ocamllibdep$(EXE) @@ -64,7 +70,7 @@ DYNLIB:=.cma endif INSTALLBIN:=install -INSTALLLIB:=install -m 644 +INSTALLLIB:=install -m 644 INSTALLSH:=./install.sh MKDIR:=install -d @@ -191,7 +197,7 @@ LIBFILES:=$(ALLVO) $(call vo_to_cm,$(ALLVO)) \ $(call vo_to_obj,$(ALLVO)) \ $(VFILES) $(GLOBFILES) -# For emacs: -# Local Variables: -# mode: makefile +# For emacs: +# Local Variables: +# mode: makefile # End: diff --git a/Makefile.install b/Makefile.install index 4a3227620c..02ae724dfe 100644 --- a/Makefile.install +++ b/Makefile.install @@ -107,7 +107,7 @@ install-devfiles: $(MKDIR) $(FULLCOQLIB) $(INSTALLSH) $(FULLCOQLIB) $(GRAMMARCMA) $(INSTALLSH) $(FULLCOQLIB) $(INSTALLCMI) - $(INSTALLSH) $(FULLCOQLIB) tools/CoqMakefile.in + $(INSTALLSH) $(FULLCOQLIB) $(TOOLS_HELPERS) ifeq ($(BEST),opt) $(INSTALLSH) $(FULLCOQLIB) $(LINKCMX) $(CORECMA:.cma=.a) $(STATICPLUGINS:.cma=.a) endif diff --git a/configure.ml b/configure.ml index 9976c19d44..e13fa80fda 100644 --- a/configure.ml +++ b/configure.ml @@ -11,7 +11,7 @@ #load "str.cma" open Printf -let coq_version = "8.7.0~alpha" +let coq_version = "8.7+alpha" let coq_macos_version = "8.6.90" (** "[...] should be a string comprised of three non-negative, period-separated integers [...]" *) let vo_magic = 8691 diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 91337b9013..6560305433 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -79,8 +79,8 @@ ######################################################################## # VST ######################################################################## -: ${VST_CI_BRANCH:=less_init_plugins} -: ${VST_CI_GITURL:=https://github.com/letouzey/VST.git} +: ${VST_CI_BRANCH:=master} +: ${VST_CI_GITURL:=https://github.com/Zimmi48/VST.git} ######################################################################## # fiat_parsers diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh index 27a336d80c..5bfc408e96 100755 --- a/dev/ci/ci-vst.sh +++ b/dev/ci/ci-vst.sh @@ -10,4 +10,4 @@ git_checkout ${VST_CI_BRANCH} ${VST_CI_GITURL} ${VST_CI_DIR} # Targets are: msl veric floyd # Patch to avoid the upper version limit -( cd ${VST_CI_DIR} && sed -i.bak 's/8.6$/8.6 or-else trunk/' Makefile && make ) +( cd ${VST_CI_DIR} && make IGNORECOQVERSION=true ) diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index c3c86ac5c5..57c7a97d58 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -28,6 +28,16 @@ Coq is compiled with -safe-string enabled and requires plugins to do the same. This means that code using `String` in an imperative way will fail to compile now. They should switch to `Bytes.t` +* Plugin API * + +Coq 8.7 offers a new module overlay containing a proposed plugin API +in `API/API.ml`; this overlay is enabled by adding the `-open API` +flag to the OCaml compiler; this happens automatically for +developments in the `plugin` folder and `coq_makefile`. + +However, `coq_makefile` can be instructed not to enable this flag by +passing `-bypass-API`. + * ML API * Added two functions for declaring hooks to be executed in reduction diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex index 5966ac468c..7e07868a38 100644 --- a/doc/refman/Classes.tex +++ b/doc/refman/Classes.tex @@ -486,15 +486,17 @@ where there is a hole in that place. \subsection{\tt Set Typeclasses Legacy Resolution} \optindex{Typeclasses Legacy Resolution} +\emph{Deprecated since 8.7} This option (off by default) uses the 8.5 implementation of resolution. Use for compatibility purposes only (porting and debugging). \subsection{\tt Set Typeclasses Module Eta} \optindex{Typeclasses Modulo Eta} +\emph{Deprecated since 8.7} This option allows eta-conversion for functions and records during -unification of type-classes. This option is now unsupported in 8.6 with +unification of type-classes. This option is unsupported since 8.6 with {\tt Typeclasses Filtered Unification} set, but still affects the default unification strategy, and the one used in {\tt Legacy Resolution} mode. It is \emph{unset} by default. If {\tt Typeclasses @@ -505,7 +507,7 @@ pattern-matching is not up-to eta. \subsection{\tt Set Typeclasses Limit Intros} \optindex{Typeclasses Limit Intros} -This option (on by default in Coq 8.6 and below) controls the ability to +This option (on by default) controls the ability to apply hints while avoiding (functional) eta-expansions in the generated proof term. It does so by allowing hints that conclude in a product to apply to a goal with a matching product directly, avoiding an diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex index 2fc1c8764a..f60908da6c 100644 --- a/doc/refman/Program.tex +++ b/doc/refman/Program.tex @@ -278,7 +278,8 @@ tactic is replaced by the default one if not specified. as implicit arguments of the special constant \texttt{Program.Tactics.obligation}. \item {\tt Set Shrink Obligations}\optindex{Shrink Obligations} - Control whether obligations should have their +\emph{Deprecated since 8.7} + This option (on by default) controls whether obligations should have their context minimized to the set of variables used in the proof of the obligation, to avoid unnecessary dependencies. \end{itemize} diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index f3bc2dd05e..3ce1d4ecd8 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -1131,8 +1131,9 @@ on. This can be obtained thanks to the option below. \optindex{Shrink Abstract} {\tt Set Shrink Abstract} \end{quote} +\emph{Deprecated since 8.7} -When set, all lemmas generated through \texttt{abstract {\tacexpr}} +When set (default), all lemmas generated through \texttt{abstract {\tacexpr}} and \texttt{transparent\_abstract {\tacexpr}} are quantified only over the variables that appear in the term constructed by \texttt{\tacexpr}. diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index ecb89b5fb8..a23c432322 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3485,6 +3485,7 @@ reduced to \texttt{S t}. \optindex{Refolding Reduction} {\tt Refolding Reduction} \end{quote} +\emph{Deprecated since 8.7} This option (off by default) controls the use of the refolding strategy of {\tt cbn} while doing reductions in unification, type inference and diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex index fee4de3364..768d0df763 100644 --- a/doc/refman/RefMan-uti.tex +++ b/doc/refman/RefMan-uti.tex @@ -60,7 +60,7 @@ subdirectory of the sources. The majority of \Coq\ projects are very similar: a collection of {\tt .v} files and eventually some {\tt .ml} ones (a \Coq\ plugin). The main piece -of metadata needed in order to build the project are the command +of metadata needed in order to build the project are the command line options to {\tt coqc} (e.g. {\tt -R, -I}, \SeeAlso Section~\ref{coqoptions}). Collecting the list of files and options is the job of the {\tt \_CoqProject} file. @@ -108,12 +108,171 @@ used in order to decide how to build them. In particular: \end{itemize} The use of \texttt{.mlpack} files has to be preferred over \texttt{.mllib} -files, since it results in a ``packed'' plugin: All auxiliary +files, since it results in a ``packed'' plugin: All auxiliary modules (as {\tt Baz} and {\tt Bazaux}) are hidden inside the plugin's ``name space'' ({\tt Qux\_plugin}). This reduces the chances of begin unable to load two distinct plugins because of a clash in their auxiliary module names. +\paragraph{Timing targets and performance testing} +The generated \texttt{Makefile} supports the generation of two kinds +of timing data: per-file build-times, and per-line times for an +individual file. + +The following targets and \texttt{Makefile} variables allow collection +of per-file timing data: +\begin{itemize} +\item \texttt{TIMED=1} --- passing this variable will cause + \texttt{make} to emit a line describing the user-space build-time + and peak memory usage for each file built. + + \texttt{Note}: On Mac OS, this works best if you've installed + \texttt{gnu-time}. + + \texttt{Example}: For example, the output of \texttt{make TIMED=1} + may look like this: +\begin{verbatim} +COQDEP Fast.v +COQDEP Slow.v +COQC Slow.v +Slow (user: 0.34 mem: 395448 ko) +COQC Fast.v +Fast (user: 0.01 mem: 45184 ko) +\end{verbatim} +\item \texttt{pretty-timed} --- this target stores the output of + \texttt{make TIMED=1} into \texttt{time-of-build.log}, and displays + a table of the times, sorted from slowest to fastest, which is also + stored in \texttt{time-of-build-pretty.log}. If you want to + construct the log for targets other than the default one, you can + pass them via the variable \texttt{TGTS}, e.g., \texttt{make + pretty-timed TGTS="a.vo b.vo"}. + + \texttt{Note}: This target requires \texttt{python} to build the table. + + \texttt{Note}: This target will \emph{append} to the timing log; if + you want a fresh start, you must remove the file + \texttt{time-of-build.log} or run \texttt{make cleanall}. + + \texttt{Example}: For example, the output of \texttt{make + pretty-timed} may look like this: +\begin{verbatim} +COQDEP Fast.v +COQDEP Slow.v +COQC Slow.v +Slow (user: 0.36 mem: 393912 ko) +COQC Fast.v +Fast (user: 0.05 mem: 45992 ko) +Time | File Name +-------------------- +0m00.41s | Total +-------------------- +0m00.36s | Slow +0m00.05s | Fast +\end{verbatim} +\item \texttt{print-pretty-timed-diff} --- this target builds a table + of timing changes between two compilations; run \texttt{make + make-pretty-timed-before} to build the log of the ``before'' + times, and run \texttt{make make-pretty-timed-after} to build the + log of the ``after'' times. The table is printed on the command + line, and stored in \texttt{time-of-build-both.log}. This target is + most useful for profiling the difference between two commits to a + repo. + + \texttt{Note}: This target requires \texttt{python} to build the table. + + \texttt{Note}: The \texttt{make-pretty-timed-before} and + \texttt{make-pretty-timed-after} targets will \emph{append} to the + timing log; if you want a fresh start, you must remove the files + \texttt{time-of-build-before.log} and + \texttt{time-of-build-after.log} or run \texttt{make cleanall} + \emph{before} building either the ``before'' or ``after'' targets. + + \texttt{Note}: The table will be sorted first by absolute time + differences rounded towards zero to a whole-number of seconds, then + by times in the ``after'' column, and finally lexicographically by + file name. This will put the biggest changes in either direction + first, and will prefer sorting by build-time over subsecond changes + in build time (which are frequently noise); lexicographic sorting + forces an order on files which take effectively no time to compile. + + \texttt{Example}: For example, the output table from \texttt{make + print-pretty-timed-diff} may look like this: +\begin{verbatim} +After | File Name | Before || Change | % Change +-------------------------------------------------------- +0m00.39s | Total | 0m00.35s || +0m00.03s | +11.42% +-------------------------------------------------------- +0m00.37s | Slow | 0m00.01s || +0m00.36s | +3600.00% +0m00.02s | Fast | 0m00.34s || -0m00.32s | -94.11% +\end{verbatim} +\end{itemize} + +The following targets and \texttt{Makefile} variables allow collection +of per-line timing data: +\begin{itemize} +\item \texttt{TIMING=1} --- passing this variable will cause + \texttt{make} to use \texttt{coqc -time} to write to a + \texttt{.v.timing} file for each \texttt{.v} file compiled, which + contains line-by-line timing information. + + \texttt{Example}: For example, running \texttt{make all TIMING=1} may + result in a file like this: +\begin{verbatim} +Chars 0 - 26 [Require~Coq.ZArith.BinInt.] 0.157 secs (0.128u,0.028s) +Chars 27 - 68 [Declare~Reduction~comp~:=~vm_c...] 0. secs (0.u,0.s) +Chars 69 - 162 [Definition~foo0~:=~Eval~comp~i...] 0.153 secs (0.136u,0.019s) +Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] 0.239 secs (0.236u,0.s) +\end{verbatim} + +\item \texttt{print-pretty-single-time-diff + BEFORE=path/to/file.v.before-timing + AFTER=path/to/file.v.after-timing} --- this target will make a + sorted table of the per-line timing differences between the timing + logs in the \texttt{BEFORE} and \texttt{AFTER} files, display it, + and save it to the file specified by the + \texttt{TIME\_OF\_PRETTY\_BUILD\_FILE} variable, which defaults to + \texttt{time-of-build-pretty.log}. + + To generate the \texttt{.v.before-timing} or + \texttt{.v.after-timing} files, you should pass + \texttt{TIMING=before} or \texttt{TIMING=after} rather than + \texttt{TIMING=1}. + + \texttt{Note}: The sorting used here is the same as in the + \texttt{print-pretty-timed-diff} target. + + \texttt{Note}: This target requires \texttt{python} to build the table. + + \texttt{Example}: For example, running + \texttt{print-pretty-single-time-diff} might give a table like this: +\begin{verbatim} +After | Code | Before || Change | % Change +--------------------------------------------------------------------------------------------------- +0m00.50s | Total | 0m04.17s || -0m03.66s | -87.96% +--------------------------------------------------------------------------------------------------- +0m00.145s | Chars 069 - 162 [Definition~foo0~:=~Eval~comp~i...] | 0m00.192s || -0m00.04s | -24.47% +0m00.126s | Chars 000 - 026 [Require~Coq.ZArith.BinInt.] | 0m00.143s || -0m00.01s | -11.88% + N/A | Chars 027 - 068 [Declare~Reduction~comp~:=~nati...] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 027 - 068 [Declare~Reduction~comp~:=~vm_c...] | N/A || +0m00.00s | N/A +0m00.231s | Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] | 0m03.836s || -0m03.60s | -93.97% +\end{verbatim} + +\item \texttt{all.timing.diff}, \texttt{path/to/file.v.timing.diff} + --- The \texttt{path/to/file.v.timing.diff} target will make a + \texttt{.v.timing.diff} file for the corresponding \texttt{.v} file, + with a table as would be generated by the + \texttt{print-pretty-single-time-diff} target; it depends on having + already made the corresponding \texttt{.v.before-timing} and + \texttt{.v.after-timing} files, which can be made by passing + \texttt{TIMING=before} and \texttt{TIMING=after}. The + \texttt{all.timing.diff} target will make such timing difference + files for all of the \texttt{.v} files that the \texttt{Makefile} + knows about. It will fail if some \texttt{.v.before-timing} or + \texttt{.v.after-timing} files don't exist. + + \texttt{Note}: This target requires \texttt{python} to build the table. +\end{itemize} + \paragraph{Notes about including the generated Makefile} This practice is discouraged. The contents of this file, including variable names @@ -165,7 +324,7 @@ invoke-coqmakefile: CoqMakefile or after the build (like invoking make on a subdirectory) one can hook in {\tt pre-all} and {\tt post-all} extension points \item \texttt{-extra-phony} and \texttt{-extra} are deprecated. To provide - additional target ({\tt .PHONY} or not) please use + additional target ({\tt .PHONY} or not) please use {\tt CoqMakefile.local} \end{itemize} diff --git a/install.sh b/install.sh index c5835b0143..f8589a3c71 100755 --- a/install.sh +++ b/install.sh @@ -8,7 +8,7 @@ for f; do dn=`dirname $f` install -d "$dest/$dn" case $bn in - *.cmxs) install -m 755 $f "$dest/$dn/$bn" + *.cmxs|*.py) install -m 755 $f "$dest/$dn/$bn" ;; *) install -m 644 $f "$dest/$dn/$bn" ;; @@ -220,23 +220,25 @@ let prlist pr l = Ppcmd_glue (List.map pr l) if a strict behavior is needed, use [prlist_strict] instead. evaluation is done from left to right. *) -let prlist_sep_lastsep no_empty sep lastsep elem = - let rec start = function - |[] -> mt () - |[e] -> elem e - |h::t -> let e = elem h in - if no_empty && ismt e then start t else - let rec aux = function - |[] -> mt () - |h::t -> - let e = elem h and r = aux t in - if no_empty && ismt e then r else - if ismt r - then let s = lastsep () in s ++ e - else let s = sep () in s ++ e ++ r - in let r = aux t in e ++ r - in start - +let prlist_sep_lastsep no_empty sep_thunk lastsep_thunk elem l = + let sep = sep_thunk () in + let lastsep = lastsep_thunk () in + let elems = List.map elem l in + let filtered_elems = + if no_empty then + List.filter (fun e -> not (ismt e)) elems + else + elems + in + let rec insert_seps es = + match es with + | [] -> mt () + | [e] -> e + | h::[e] -> h ++ lastsep ++ e + | h::t -> h ++ sep ++ insert_seps t + in + insert_seps filtered_elems + let prlist_strict pr l = prlist_sep_lastsep true mt mt pr l (* [prlist_with_sep sep pr [a ; ... ; c]] outputs [pr a ++ sep() ++ ... ++ sep() ++ pr c] *) diff --git a/lib/pp.mli b/lib/pp.mli index be255a74fd..96656c8b65 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -145,7 +145,10 @@ val prlist_strict : ('a -> std_ppcmds) -> 'a list -> std_ppcmds val prlist_with_sep : (unit -> std_ppcmds) -> ('a -> std_ppcmds) -> 'a list -> std_ppcmds (** [prlist_with_sep sep pr [a ; ... ; c]] outputs - [pr a ++ sep() ++ ... ++ sep() ++ pr c]. *) + [pr a ++ sep () ++ ... ++ sep () ++ pr c]. + where the thunk sep is memoized, rather than being called each place + its result is used. +*) val prvect : ('a -> std_ppcmds) -> 'a array -> std_ppcmds (** As [prlist], but on arrays. *) diff --git a/plugins/.merlin b/plugins/.merlin new file mode 100644 index 0000000000..dd6678ba09 --- /dev/null +++ b/plugins/.merlin @@ -0,0 +1,2 @@ +REC +FLG -open API diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index 00e80d041f..6281b2675e 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -1,5 +1,3 @@ -open API - let contrib_name = "btauto" let init_constant dir s = diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 3e4febf47c..1828213227 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -10,7 +10,6 @@ (* Downey,Sethi and Tarjan. *) (* Plus some e-matching and constructor handling by P. Corbineau *) -open API open CErrors open Util open Pp diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli index 1441e13fb3..e6abf1ccf0 100644 --- a/plugins/cc/ccalgo.mli +++ b/plugins/cc/ccalgo.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Util open Term open Names diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml index 4c9ebcfc4d..a43a167e86 100644 --- a/plugins/cc/ccproof.ml +++ b/plugins/cc/ccproof.ml @@ -9,7 +9,6 @@ (* This file uses the (non-compressed) union-find structure to generate *) (* proof-trees that will be transformed into proof-terms in cctac.ml4 *) -open API open CErrors open Term open Ccalgo diff --git a/plugins/cc/ccproof.mli b/plugins/cc/ccproof.mli index 0488a5db7c..9f53123db1 100644 --- a/plugins/cc/ccproof.mli +++ b/plugins/cc/ccproof.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Ccalgo open Term diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 4c5d85a5fd..4934b0750b 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -8,7 +8,6 @@ (* This file is the interface between the c-c algorithm and Coq *) -open API open Evd open Names open Inductiveops diff --git a/plugins/cc/cctac.mli b/plugins/cc/cctac.mli index ef32d2b83e..b4bb62be8e 100644 --- a/plugins/cc/cctac.mli +++ b/plugins/cc/cctac.mli @@ -7,7 +7,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open EConstr val proof_tac: Ccproof.proof -> unit Proofview.tactic diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4 index add3f90b1b..6ed4672ce3 100644 --- a/plugins/cc/g_congruence.ml4 +++ b/plugins/cc/g_congruence.ml4 @@ -8,7 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open API open Ltac_plugin open Cctac open Stdarg diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 19d23c0e43..1524079f42 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Context.Named.Declaration let map_const_entry_body (f:Term.constr->Term.constr) (x:Safe_typing.private_constants Entries.const_entry_body) diff --git a/plugins/derive/derive.mli b/plugins/derive/derive.mli index 7ea64a5288..690a7c5083 100644 --- a/plugins/derive/derive.mli +++ b/plugins/derive/derive.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API - (** [start_deriving f suchthat lemma] starts a proof of [suchthat] (which can contain references to [f]) in the context extended by [f:=?x]. When the proof ends, [f] is defined as the value of [?x] diff --git a/plugins/derive/g_derive.ml4 b/plugins/derive/g_derive.ml4 index ce9129bcfe..df701ed802 100644 --- a/plugins/derive/g_derive.ml4 +++ b/plugins/derive/g_derive.ml4 @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Stdarg (*i camlp4deps: "grammar/grammar.cma" i*) diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 19ba31fbbd..9772ebd641 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Pp open Util open Names diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli index 28a7c4d457..d6342b59c6 100644 --- a/plugins/extraction/common.mli +++ b/plugins/extraction/common.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Names open Globnames open Miniml diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 79d602dbe8..7d69cbff1f 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Miniml open Term open Declarations diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index 0629a84a03..f289b63ad4 100644 --- a/plugins/extraction/extract_env.mli +++ b/plugins/extraction/extract_env.mli @@ -8,7 +8,6 @@ (*s This module declares the extraction commands. *) -open API open Names open Libnames open Globnames diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index d638c232bb..3661faadab 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -7,7 +7,6 @@ (************************************************************************) (*i*) -open API open Util open Names open Term diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli index 5ee34103c5..e1d43f3405 100644 --- a/plugins/extraction/extraction.mli +++ b/plugins/extraction/extraction.mli @@ -8,7 +8,6 @@ (*s Extraction from Coq terms to Miniml. *) -open API open Names open Term open Declarations diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index 2fa453e533..4372ea557b 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -8,7 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open API open Grammar_API.Pcoq.Prim DECLARE PLUGIN "extraction_plugin" diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 6146f32bbe..0f537abece 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -8,7 +8,6 @@ (*s Production of Haskell syntax. *) -open API open Pp open CErrors open Util diff --git a/plugins/extraction/json.ml b/plugins/extraction/json.ml index 1bf19f186b..e43c47d050 100644 --- a/plugins/extraction/json.ml +++ b/plugins/extraction/json.ml @@ -1,4 +1,3 @@ -open API open Pp open Util open Names diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli index ea966baee6..be8282da06 100644 --- a/plugins/extraction/miniml.mli +++ b/plugins/extraction/miniml.mli @@ -8,7 +8,6 @@ (*s Target language for extraction: a core ML called MiniML. *) -open API open Pp open Names open Globnames diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index f8c846725e..f1bcde2f3f 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -7,7 +7,6 @@ (************************************************************************) (*i*) -open API open Util open Names open Libnames diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli index 1db96413a8..42d22a7b45 100644 --- a/plugins/extraction/mlutil.mli +++ b/plugins/extraction/mlutil.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Names open Globnames open Miniml diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index 365dc191ab..a896a8d037 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Names open ModPath open Globnames diff --git a/plugins/extraction/modutil.mli b/plugins/extraction/modutil.mli index 1d9db3a5fc..ad60b58d5d 100644 --- a/plugins/extraction/modutil.mli +++ b/plugins/extraction/modutil.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Names open Globnames open Miniml diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 2ac411d06f..9cbc3fd713 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -8,7 +8,6 @@ (*s Production of Ocaml syntax. *) -open API open Pp open CErrors open Util diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml index bb96489ab0..1ccc273704 100644 --- a/plugins/extraction/scheme.ml +++ b/plugins/extraction/scheme.ml @@ -8,7 +8,6 @@ (*s Production of Scheme syntax. *) -open API open Pp open CErrors open Util diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index dff3548fd8..ca98f07e8d 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Names open ModPath open Term diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 0215aa8e48..2b3007f025 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Names open Libnames open Globnames diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index 4319fa71cc..db1a46a035 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Hipattern open Names open Term diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli index 535d757350..106c469c62 100644 --- a/plugins/firstorder/formula.mli +++ b/plugins/firstorder/formula.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Term open EConstr open Globnames diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 81d714aa26..c001ee3829 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -8,7 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open API open Grammar_API open Ltac_plugin open Formula diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml index bd420546ff..f660ba7343 100644 --- a/plugins/firstorder/ground.ml +++ b/plugins/firstorder/ground.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Ltac_plugin open Formula open Sequent diff --git a/plugins/firstorder/ground.mli b/plugins/firstorder/ground.mli index e15af1f23c..d763fe6355 100644 --- a/plugins/firstorder/ground.mli +++ b/plugins/firstorder/ground.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API val ground_tac: unit Proofview.tactic -> ((Sequent.t -> unit Proofview.tactic) -> unit Proofview.tactic) -> unit Proofview.tactic diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 4c8b96be1d..1690736305 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Unify open Rules open CErrors diff --git a/plugins/firstorder/instances.mli b/plugins/firstorder/instances.mli index c2eb1d68c5..ec2a056e32 100644 --- a/plugins/firstorder/instances.mli +++ b/plugins/firstorder/instances.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Globnames open Rules diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index b0fcd98ccd..d6309b057f 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open CErrors open Util open Names diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli index 05f60eccc9..d8d4c1a38a 100644 --- a/plugins/firstorder/rules.mli +++ b/plugins/firstorder/rules.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Term open EConstr open Names diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 6fddaafa32..5ba98fb584 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open EConstr open CErrors open Util diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli index 2488ffded2..0a2e84bb83 100644 --- a/plugins/firstorder/sequent.mli +++ b/plugins/firstorder/sequent.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open EConstr open Formula open Globnames diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml index 2da3dc768c..a1409edd09 100644 --- a/plugins/firstorder/unify.ml +++ b/plugins/firstorder/unify.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Util open Term open EConstr diff --git a/plugins/firstorder/unify.mli b/plugins/firstorder/unify.mli index cf2ef8ba61..d3e8aeee88 100644 --- a/plugins/firstorder/unify.mli +++ b/plugins/firstorder/unify.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Term open EConstr diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index a6299c3c49..68af1b3b63 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -12,7 +12,6 @@ des inéquations et équations sont entiers. En attendant la tactique Field. *) -open API open Term open Tactics open Names diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index dc43ea7c46..15ab396e31 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1,4 +1,3 @@ -open API open Printer open CErrors open Util @@ -1382,7 +1381,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam (* Proof of principles of general functions *) -(* let hrec_id = +(* let hrec_id = Recdef.hrec_id *) (* and acc_inv_id = Recdef.acc_inv_id *) (* and ltof_ref = Recdef.ltof_ref *) (* and acc_rel = Recdef.acc_rel *) diff --git a/plugins/funind/functional_principles_proofs.mli b/plugins/funind/functional_principles_proofs.mli index d03fc475e0..64fbfaeedf 100644 --- a/plugins/funind/functional_principles_proofs.mli +++ b/plugins/funind/functional_principles_proofs.mli @@ -1,4 +1,3 @@ -open API open Names val prove_princ_for_struct : diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index d726c1a2bb..513fce2484 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -1,4 +1,3 @@ -open API open Printer open CErrors open Util diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli index d6ad7ef0d2..5a7ffe0590 100644 --- a/plugins/funind/functional_principles_types.mli +++ b/plugins/funind/functional_principles_types.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Names open Term open Misctypes diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 56048f92e4..c495703eeb 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) (*i camlp4deps: "grammar/grammar.cma" i*) -open API open Grammar_API open Ltac_plugin open Util diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index db2af2be53..379c83b245 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1,4 +1,3 @@ -open API open Printer open Pp open Names diff --git a/plugins/funind/glob_term_to_relation.mli b/plugins/funind/glob_term_to_relation.mli index 7ad7de0792..0cab5a6d35 100644 --- a/plugins/funind/glob_term_to_relation.mli +++ b/plugins/funind/glob_term_to_relation.mli @@ -1,4 +1,3 @@ -open API open Names (* diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 726a8203d7..7cb35838c7 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -1,4 +1,3 @@ -open API open Pp open Glob_term open CErrors diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli index b6d2c45437..99a258de98 100644 --- a/plugins/funind/glob_termops.mli +++ b/plugins/funind/glob_termops.mli @@ -1,4 +1,3 @@ -open API open Names open Glob_term open Misctypes diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index ff7667e991..863c9dc8d5 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -1,4 +1,3 @@ -open API open CErrors open Util open Names diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index fc7da6a338..7a60da44fb 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -1,4 +1,3 @@ -open API open Misctypes val warn_cannot_define_graph : ?loc:Loc.t -> Pp.std_ppcmds * Pp.std_ppcmds -> unit diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 61fbca23f2..f4f9ba2bbb 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -1,4 +1,3 @@ -open API open Names open Pp open Libnames diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index f7a9cedd73..5e425cd18a 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -1,4 +1,3 @@ -open API open Names open Pp diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index e6f10a880c..8dea6c90f5 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Ltac_plugin open Declarations open CErrors diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 63662a4437..52a82b0e5e 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -8,7 +8,6 @@ (* Merging of induction principles. *) -open API open Globnames open Tactics open Indfun_common diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index bc550c8b9c..d3eccb58d7 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API module CVars = Vars diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli index f3d5e73320..63bbdbe7e3 100644 --- a/plugins/funind/recdef.mli +++ b/plugins/funind/recdef.mli @@ -1,4 +1,3 @@ -open API (* val evaluable_of_global_reference : Libnames.global_reference -> Names.evaluable_global_reference *) val tclUSER_if_not_mes : diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4 index 47fd324f97..2769802cf4 100644 --- a/plugins/ltac/coretactics.ml4 +++ b/plugins/ltac/coretactics.ml4 @@ -8,7 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open API open Util open Locus open Misctypes diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml index 4342f5b5e1..4cab6ef336 100644 --- a/plugins/ltac/evar_tactics.ml +++ b/plugins/ltac/evar_tactics.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Util open Names open Term diff --git a/plugins/ltac/evar_tactics.mli b/plugins/ltac/evar_tactics.mli index 0658008c00..122aecd75b 100644 --- a/plugins/ltac/evar_tactics.mli +++ b/plugins/ltac/evar_tactics.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Names open Tacexpr open Locus diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index af1d349db2..72c6f90900 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -8,7 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open API open Grammar_API open Pp open Genarg diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli index e5a2d003a5..419c5e8c45 100644 --- a/plugins/ltac/extraargs.mli +++ b/plugins/ltac/extraargs.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Grammar_API open Tacexpr open Names diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index e56b510be0..6d80ab5494 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -8,7 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open API open Grammar_API open Pp open Genarg diff --git a/plugins/ltac/extratactics.mli b/plugins/ltac/extratactics.mli index fe90f633f2..c423585e5e 100644 --- a/plugins/ltac/extratactics.mli +++ b/plugins/ltac/extratactics.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API val discrHyp : Names.Id.t -> unit Proofview.tactic val injHyp : Names.Id.t -> unit Proofview.tactic diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4 index 6145e373b1..4d13d89a49 100644 --- a/plugins/ltac/g_auto.ml4 +++ b/plugins/ltac/g_auto.ml4 @@ -8,7 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open API open Grammar_API open Pp open Genarg diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4 index 946b99f6c0..dd24aa3dbf 100644 --- a/plugins/ltac/g_class.ml4 +++ b/plugins/ltac/g_class.ml4 @@ -8,7 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open API open Class_tactics open Stdarg open Tacarg diff --git a/plugins/ltac/g_eqdecide.ml4 b/plugins/ltac/g_eqdecide.ml4 index a7c05664f5..5494369022 100644 --- a/plugins/ltac/g_eqdecide.ml4 +++ b/plugins/ltac/g_eqdecide.ml4 @@ -14,7 +14,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open API open Eqdecide DECLARE PLUGIN "ltac_plugin" diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index cf6bd98b38..cc052c8a20 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -8,7 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open API open Grammar_API DECLARE PLUGIN "ltac_plugin" @@ -433,7 +432,7 @@ let is_explicit_terminator = function TacSolve _ -> true | _ -> false VERNAC tactic_mode EXTEND VernacSolve | [ - ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => [ classify_as_proofstep ] -> [ - let g = Option.default (Proof_global.get_default_goal_selector ()) g in + let g = Option.default (Proof_bullet.get_default_goal_selector ()) g in vernac_solve g n t def ] | [ - "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4 index a2e8fc270d..1935d560a4 100644 --- a/plugins/ltac/g_obligations.ml4 +++ b/plugins/ltac/g_obligations.ml4 @@ -12,7 +12,6 @@ Syntax for the subtac terms and types. Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliâtre *) -open API open Grammar_API open Libnames open Constrexpr diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index 8956e21b93..3c27b27475 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 @@ -10,7 +10,6 @@ (* Syntax for rewriting with strategies *) -open API open Grammar_API open Names open Misctypes diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index 49af905d89..e539b58674 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Grammar_API open Pp open CErrors diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml index 898c1d1c31..2adcf02e69 100644 --- a/plugins/ltac/pltac.ml +++ b/plugins/ltac/pltac.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Grammar_API open Pcoq diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli index 782d13a38d..794cb527f3 100644 --- a/plugins/ltac/pltac.mli +++ b/plugins/ltac/pltac.mli @@ -8,7 +8,6 @@ (** Ltac parsing entries *) -open API open Grammar_API open Loc open Names diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 8d8e82c7ce..327b347ec0 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Pp open Names open Namegen diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index c15225ebfc..1127c98319 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -9,7 +9,6 @@ (** This module implements pretty-printers for tactic_expr syntactic objects and their subcomponents. *) -open API open Pp open Genarg open Geninterp diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index e25f1926d5..32494a8793 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Unicode open Pp open Printer diff --git a/plugins/ltac/profile_ltac.mli b/plugins/ltac/profile_ltac.mli index eb4146cfc1..52827cb36b 100644 --- a/plugins/ltac/profile_ltac.mli +++ b/plugins/ltac/profile_ltac.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API (** Ltac profiling primitives *) diff --git a/plugins/ltac/profile_ltac_tactics.ml4 b/plugins/ltac/profile_ltac_tactics.ml4 index 9f171cee66..2b1106ee21 100644 --- a/plugins/ltac/profile_ltac_tactics.ml4 +++ b/plugins/ltac/profile_ltac_tactics.ml4 @@ -10,7 +10,6 @@ (** Ltac profiling entrypoints *) -open API open Profile_ltac open Stdarg diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 3a77f34a1c..bbd7834d58 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Names open Pp open CErrors diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index 73e309cc21..35205ac58a 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Names open Environ open EConstr diff --git a/plugins/ltac/tacarg.ml b/plugins/ltac/tacarg.ml index 610a722fb1..1bf9ea4c1d 100644 --- a/plugins/ltac/tacarg.ml +++ b/plugins/ltac/tacarg.ml @@ -8,7 +8,6 @@ (** Generic arguments based on Ltac. *) -open API open Genarg open Geninterp open Tacexpr diff --git a/plugins/ltac/tacarg.mli b/plugins/ltac/tacarg.mli index 4c3687ec75..6c4f3dd873 100644 --- a/plugins/ltac/tacarg.mli +++ b/plugins/ltac/tacarg.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Genarg open Tacexpr open Constrexpr diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index bdfa6d9896..9e3a54cc86 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Util open Names open Term diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli index ab46455c82..1a67f6f888 100644 --- a/plugins/ltac/taccoerce.mli +++ b/plugins/ltac/taccoerce.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Util open Names open EConstr diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index c6b4feba1c..791b7f48db 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Grammar_API open Pp open CErrors diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index 9980e0961a..ccd44b914e 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -8,7 +8,6 @@ (** Ltac toplevel command entries. *) -open API open Grammar_API open Vernacexpr open Tacexpr diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml index 58d1766ff7..13b44f0e2c 100644 --- a/plugins/ltac/tacenv.ml +++ b/plugins/ltac/tacenv.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Util open Pp open Names diff --git a/plugins/ltac/tacenv.mli b/plugins/ltac/tacenv.mli index 23e12bfc0d..958109e5a7 100644 --- a/plugins/ltac/tacenv.mli +++ b/plugins/ltac/tacenv.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Names open Tacexpr open Geninterp diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 471320684d..64da097deb 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Loc open Names open Constrexpr diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index c3e39ec11a..df03c7b472 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Grammar_API open Pattern open Pp diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli index 4749017e16..ad2e709085 100644 --- a/plugins/ltac/tacintern.mli +++ b/plugins/ltac/tacintern.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Grammar_API open Pp open Names diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index bad3e774de..7b054947b7 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Grammar_API open Constrintern open Patternops diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index ab94e21f0a..73e4f3d6ab 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Names open Tactic_debug open EConstr diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index 750843c9d0..c1ca854334 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Grammar_API open Util open Tacexpr diff --git a/plugins/ltac/tacsubst.mli b/plugins/ltac/tacsubst.mli index c401e67f11..5ac3775676 100644 --- a/plugins/ltac/tacsubst.mli +++ b/plugins/ltac/tacsubst.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Tacexpr open Mod_subst open Genarg diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index 9113b620f0..5394b1e116 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Util open Names open Pp diff --git a/plugins/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli index 469c6bdbca..ef6362270a 100644 --- a/plugins/ltac/tactic_debug.mli +++ b/plugins/ltac/tactic_debug.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Environ open Pattern open Names diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml index 3e96680729..63b8cc4824 100644 --- a/plugins/ltac/tactic_matching.ml +++ b/plugins/ltac/tactic_matching.ml @@ -9,7 +9,6 @@ (** This file extends Matching with the main logic for Ltac's (lazy)match and (lazy)match goal. *) -open API open Names open Tacexpr open Context.Named.Declaration diff --git a/plugins/ltac/tactic_matching.mli b/plugins/ltac/tactic_matching.mli index 304eec463e..01334d36c9 100644 --- a/plugins/ltac/tactic_matching.mli +++ b/plugins/ltac/tactic_matching.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API (** This file extends Matching with the main logic for Ltac's (lazy)match and (lazy)match goal. *) diff --git a/plugins/ltac/tactic_option.ml b/plugins/ltac/tactic_option.ml index 5b95e9c778..fdeab8dc4b 100644 --- a/plugins/ltac/tactic_option.ml +++ b/plugins/ltac/tactic_option.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Libobject open Pp diff --git a/plugins/ltac/tactic_option.mli b/plugins/ltac/tactic_option.mli index dc3bbf7d69..dd91944d48 100644 --- a/plugins/ltac/tactic_option.mli +++ b/plugins/ltac/tactic_option.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Tacexpr open Vernacexpr diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index e809d87dc7..01d3f79c74 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Term open EConstr open Hipattern diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index a662f8bad4..a4103634e0 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -16,7 +16,6 @@ (* *) (************************************************************************) -open API open Pp open Mutils open Goptions diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4 index 37a21cd592..b15dd7ae66 100644 --- a/plugins/micromega/g_micromega.ml4 +++ b/plugins/micromega/g_micromega.ml4 @@ -16,7 +16,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open API open Ltac_plugin open Stdarg open Tacarg diff --git a/plugins/nsatz/g_nsatz.ml4 b/plugins/nsatz/g_nsatz.ml4 index 261f3dab40..01c3d79407 100644 --- a/plugins/nsatz/g_nsatz.ml4 +++ b/plugins/nsatz/g_nsatz.ml4 @@ -8,7 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open API open Ltac_plugin DECLARE PLUGIN "nsatz_plugin" diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml index 7e63b916d3..72934a15d9 100644 --- a/plugins/nsatz/nsatz.ml +++ b/plugins/nsatz/nsatz.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open CErrors open Util open Term diff --git a/plugins/nsatz/nsatz.mli b/plugins/nsatz/nsatz.mli index b692522f2f..d6e3071aa3 100644 --- a/plugins/nsatz/nsatz.mli +++ b/plugins/nsatz/nsatz.mli @@ -6,5 +6,4 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API val nsatz_compute : Term.constr -> unit Proofview.tactic diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 3badb92f59..d07b2e0b45 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -13,7 +13,6 @@ (* *) (**************************************************************************) -open API open CErrors open Util open Names diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4 index 8d24027d88..735af6babc 100644 --- a/plugins/omega/g_omega.ml4 +++ b/plugins/omega/g_omega.ml4 @@ -15,7 +15,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open API DECLARE PLUGIN "omega_plugin" diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4 index 88076dca9e..f7ebd3204a 100644 --- a/plugins/quote/g_quote.ml4 +++ b/plugins/quote/g_quote.ml4 @@ -8,7 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open API open Ltac_plugin open Names open Misctypes diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index 8ee5ce8b1e..e1e73b1c32 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -101,7 +101,6 @@ (*i*) -open API open CErrors open Util open Names diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index 06c80a8256..4ffbd5aa8b 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -6,7 +6,6 @@ *************************************************************************) -open API open Names let module_refl_name = "ReflOmegaCore" diff --git a/plugins/romega/const_omega.mli b/plugins/romega/const_omega.mli index 6dc5d9f7e5..a452b1a917 100644 --- a/plugins/romega/const_omega.mli +++ b/plugins/romega/const_omega.mli @@ -6,7 +6,6 @@ *************************************************************************) -open API (** Coq objects used in romega *) diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4 index 53f6f42c8e..5fd9c94194 100644 --- a/plugins/romega/g_romega.ml4 +++ b/plugins/romega/g_romega.ml4 @@ -8,7 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open API DECLARE PLUGIN "romega_plugin" diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index 60e6e7de79..517df41d93 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -6,7 +6,6 @@ *************************************************************************) -open API open Pp open Util open Const_omega diff --git a/plugins/rtauto/g_rtauto.ml4 b/plugins/rtauto/g_rtauto.ml4 index 69a2043f64..bfa1e5f393 100644 --- a/plugins/rtauto/g_rtauto.ml4 +++ b/plugins/rtauto/g_rtauto.ml4 @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API (*i camlp4deps: "grammar/grammar.cma" i*) diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml index 1158817d62..43a4107add 100644 --- a/plugins/rtauto/proof_search.ml +++ b/plugins/rtauto/proof_search.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open CErrors open Util open Goptions diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 944e0ac5e7..9f02388c39 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API module Search = Explore.Make(Proof_search) diff --git a/plugins/rtauto/refl_tauto.mli b/plugins/rtauto/refl_tauto.mli index 080dcdac27..bec18f6df8 100644 --- a/plugins/rtauto/refl_tauto.mli +++ b/plugins/rtauto/refl_tauto.mli @@ -7,7 +7,6 @@ (************************************************************************) (* raises Not_found if no proof is found *) -open API type atom_env= {mutable next:int; diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4 index ada41274fa..6c82346bca 100644 --- a/plugins/setoid_ring/g_newring.ml4 +++ b/plugins/setoid_ring/g_newring.ml4 @@ -8,7 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open API open Grammar_API open Ltac_plugin open Pp diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 955cc767c7..0f996c65aa 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Ltac_plugin open Pp open Util diff --git a/plugins/setoid_ring/newring.mli b/plugins/setoid_ring/newring.mli index 7f685063c4..d9d32c681d 100644 --- a/plugins/setoid_ring/newring.mli +++ b/plugins/setoid_ring/newring.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Names open EConstr open Libnames diff --git a/plugins/setoid_ring/newring_ast.mli b/plugins/setoid_ring/newring_ast.mli index b7afd2effc..d37582bd79 100644 --- a/plugins/setoid_ring/newring_ast.mli +++ b/plugins/setoid_ring/newring_ast.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Term open Libnames open Constrexpr diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli index 94eaa1d6aa..cdd4ee6459 100644 --- a/plugins/ssr/ssrast.mli +++ b/plugins/ssr/ssrast.mli @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Names open Ltac_plugin diff --git a/plugins/ssr/ssrbwd.ml b/plugins/ssr/ssrbwd.ml index 3988f00bad..cc0e86684e 100644 --- a/plugins/ssr/ssrbwd.ml +++ b/plugins/ssr/ssrbwd.ml @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Printer open Pretyping open Globnames diff --git a/plugins/ssr/ssrbwd.mli b/plugins/ssr/ssrbwd.mli index 20a1263d24..af9f7491ad 100644 --- a/plugins/ssr/ssrbwd.mli +++ b/plugins/ssr/ssrbwd.mli @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API val apply_top_tac : Goal.goal Evd.sigma -> Goal.goal list Evd.sigma diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 411ce6853c..608b778e4f 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Grammar_API open Util open Names diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index f611685769..4b045e989a 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Tacmach open Names open Environ diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index bd9a05891a..832044909c 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Util open Names open Printer diff --git a/plugins/ssr/ssrelim.mli b/plugins/ssr/ssrelim.mli index 825b4758e3..66e202b48f 100644 --- a/plugins/ssr/ssrelim.mli +++ b/plugins/ssr/ssrelim.mli @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Ssrmatching_plugin val ssrelim : diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index b0fe898975..ab6a60f4ee 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Ltac_plugin open Util open Names diff --git a/plugins/ssr/ssrequality.mli b/plugins/ssr/ssrequality.mli index f9ab5d74fe..a3366887fb 100644 --- a/plugins/ssr/ssrequality.mli +++ b/plugins/ssr/ssrequality.mli @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Ssrmatching_plugin open Ssrast diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index 660c2e776c..8e6329a15e 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Names open Tacmach diff --git a/plugins/ssr/ssrfwd.mli b/plugins/ssr/ssrfwd.mli index 7f254074c7..e5b5b58fff 100644 --- a/plugins/ssr/ssrfwd.mli +++ b/plugins/ssr/ssrfwd.mli @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Names open Ltac_plugin diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index 06bbd749e6..023778fdbf 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Names open Pp open Term diff --git a/plugins/ssr/ssripats.mli b/plugins/ssr/ssripats.mli index aefdc8e111..6c36e67e83 100644 --- a/plugins/ssr/ssripats.mli +++ b/plugins/ssr/ssripats.mli @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Ssrmatching_plugin open Ssrast open Ssrcommon diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 09917339a7..228444b82e 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Grammar_API open Names open Pp diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli index 1548206666..c93e104056 100644 --- a/plugins/ssr/ssrparser.mli +++ b/plugins/ssr/ssrparser.mli @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Grammar_API val ssrtacarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml index 427109c1b2..e865ef706d 100644 --- a/plugins/ssr/ssrprinters.ml +++ b/plugins/ssr/ssrprinters.ml @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Pp open Names open Printer diff --git a/plugins/ssr/ssrprinters.mli b/plugins/ssr/ssrprinters.mli index 8da9bc72bc..5c68872b75 100644 --- a/plugins/ssr/ssrprinters.mli +++ b/plugins/ssr/ssrprinters.mli @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Ssrast val pp_term : diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml index b586d05e1c..5e43c83749 100644 --- a/plugins/ssr/ssrtacticals.ml +++ b/plugins/ssr/ssrtacticals.ml @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Names open Termops open Tacmach diff --git a/plugins/ssr/ssrtacticals.mli b/plugins/ssr/ssrtacticals.mli index 297cfdfdc0..c1f65a31e9 100644 --- a/plugins/ssr/ssrtacticals.mli +++ b/plugins/ssr/ssrtacticals.mli @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API val tclSEQAT : Ltac_plugin.Tacinterp.interp_sign -> diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index cb6a2cd695..fbe3cd2b91 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Grammar_API open Names open Term diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index cc142e091c..338ecccc2d 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Util open Names open Term diff --git a/plugins/ssr/ssrview.mli b/plugins/ssr/ssrview.mli index 8a7bd5d6e7..6fd906ff4f 100644 --- a/plugins/ssr/ssrview.mli +++ b/plugins/ssr/ssrview.mli @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Ssrast open Ssrcommon diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 7674a8dde6..74519f6c54 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -8,7 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API open Grammar_API (* Defining grammar rules with "xx" in it automatically declares keywords too, diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index 1853bc35dc..0c09d7bfbf 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -1,7 +1,6 @@ (* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) -open API open Grammar_API open Goal open Genarg diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index 6bf5b8cfca..c41ec39cb4 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -open API (* Poor's man DECLARE PLUGIN *) let __coq_plugin_name = "ascii_syntax_plugin" diff --git a/plugins/syntax/int31_syntax.ml b/plugins/syntax/int31_syntax.ml index fe1eef866c..af64b1479a 100644 --- a/plugins/syntax/int31_syntax.ml +++ b/plugins/syntax/int31_syntax.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API (* Poor's man DECLARE PLUGIN *) let __coq_plugin_name = "int31_syntax_plugin" diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml index c6ee899ed7..524a5c5221 100644 --- a/plugins/syntax/nat_syntax.ml +++ b/plugins/syntax/nat_syntax.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API (* Poor's man DECLARE PLUGIN *) let __coq_plugin_name = "nat_syntax_plugin" diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index 9cfa50071e..06117de79a 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Util open Names open Globnames diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml index a4335a508b..b7f13b0400 100644 --- a/plugins/syntax/string_syntax.ml +++ b/plugins/syntax/string_syntax.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -open API open Globnames open Ascii_syntax_plugin.Ascii_syntax open Glob_term diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml index 719d8b1ccb..af3df28890 100644 --- a/plugins/syntax/z_syntax.ml +++ b/plugins/syntax/z_syntax.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Pp open CErrors open Util diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 21ed8e0a23..1d75fecb15 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -29,7 +29,7 @@ exception Elimconst let refolding_in_reduction = ref false let _ = Goptions.declare_bool_option { - Goptions.optdepr = false; + Goptions.optdepr = true; (* remove in 8.8 *) Goptions.optname = "Perform refolding of fixpoints/constants like cbn during reductions"; Goptions.optkey = ["Refolding";"Reduction"]; diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index a15cadfa0b..a68b569cbe 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -105,7 +105,7 @@ open Decl_kinds | SearchString (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc let pr_search a gopt b pr_p = - pr_opt (fun g -> Proof_global.pr_goal_selector g ++ str ":"++ spc()) gopt + pr_opt (fun g -> Proof_bullet.pr_goal_selector g ++ str ":"++ spc()) gopt ++ match a with | SearchHead c -> keyword "SearchHead" ++ spc() ++ pr_p c ++ pr_in_out_modules b @@ -490,7 +490,7 @@ open Decl_kinds | PrintVisibility s -> keyword "Print Visibility" ++ pr_opt str s | PrintAbout (qid,gopt) -> - pr_opt (fun g -> Proof_global.pr_goal_selector g ++ str ":"++ spc()) gopt + pr_opt (fun g -> Proof_bullet.pr_goal_selector g ++ str ":"++ spc()) gopt ++ keyword "About" ++ spc() ++ pr_smart_global qid | PrintImplicit qid -> keyword "Print Implicit" ++ spc() ++ pr_smart_global qid @@ -1132,7 +1132,7 @@ open Decl_kinds | None -> hov 2 (keyword "Check" ++ spc() ++ pr_lconstr c) in let pr_i = match io with None -> mt () - | Some i -> Proof_global.pr_goal_selector i ++ str ": " in + | Some i -> Proof_bullet.pr_goal_selector i ++ str ": " in return (pr_i ++ pr_mayeval r c) | VernacGlobalCheck c -> return (hov 2 (keyword "Type" ++ pr_constrarg c)) diff --git a/printing/printer.ml b/printing/printer.ml index 2a198d4564..3516788022 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -805,7 +805,7 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () = | _ , _, _ -> let end_cmd = str "This subproof is complete, but there are some unfocused goals." ++ - (let s = Proof_global.Bullet.suggest p in + (let s = Proof_bullet.suggest p in if Pp.ismt s then s else fnl () ++ s) ++ fnl () in diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml new file mode 100644 index 0000000000..f80cb7cc66 --- /dev/null +++ b/proofs/proof_bullet.ml @@ -0,0 +1,248 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Proof + +type t = Vernacexpr.bullet + +let bullet_eq b1 b2 = match b1, b2 with +| Vernacexpr.Dash n1, Vernacexpr.Dash n2 -> n1 = n2 +| Vernacexpr.Star n1, Vernacexpr.Star n2 -> n1 = n2 +| Vernacexpr.Plus n1, Vernacexpr.Plus n2 -> n1 = n2 +| _ -> false + +let pr_bullet b = + match b with + | Vernacexpr.Dash n -> Pp.(str (String.make n '-')) + | Vernacexpr.Star n -> Pp.(str (String.make n '*')) + | Vernacexpr.Plus n -> Pp.(str (String.make n '+')) + + +type behavior = { + name : string; + put : proof -> t -> proof; + suggest: proof -> Pp.t +} + +let behaviors = Hashtbl.create 4 +let register_behavior b = Hashtbl.add behaviors b.name b + +(*** initial modes ***) +let none = { + name = "None"; + put = (fun x _ -> x); + suggest = (fun _ -> Pp.mt ()) +} +let _ = register_behavior none + +module Strict = struct + type suggestion = + | Suggest of t (* this bullet is mandatory here *) + | Unfinished of t (* no mandatory bullet here, but this bullet is unfinished *) + | NoBulletInUse (* No mandatory bullet (or brace) here, no bullet pending, + some focused goals exists. *) + | NeedClosingBrace (* Some unfocussed goal exists "{" needed to focus them *) + | ProofFinished (* No more goal anywhere *) + + (* give a message only if more informative than the standard coq message *) + let suggest_on_solved_goal sugg = + match sugg with + | NeedClosingBrace -> Pp.(str"Try unfocusing with \"}\".") + | NoBulletInUse -> Pp.mt () + | ProofFinished -> Pp.mt () + | Suggest b -> Pp.(str"Focus next goal with bullet " ++ pr_bullet b ++ str".") + | Unfinished b -> Pp.(str"The current bullet " ++ pr_bullet b ++ str" is unfinished.") + + (* give always a message. *) + let suggest_on_error sugg = + match sugg with + | NeedClosingBrace -> Pp.(str"Try unfocusing with \"}\".") + | NoBulletInUse -> assert false (* This should never raise an error. *) + | ProofFinished -> Pp.(str"No more subgoals.") + | Suggest b -> Pp.(str"Expecting " ++ pr_bullet b ++ str".") + | Unfinished b -> Pp.(str"Current bullet " ++ pr_bullet b ++ str" is not finished.") + + exception FailedBullet of t * suggestion + + let _ = + CErrors.register_handler + (function + | FailedBullet (b,sugg) -> + let prefix = Pp.(str"Wrong bullet " ++ pr_bullet b ++ str": ") in + CErrors.user_err ~hdr:"Focus" Pp.(prefix ++ suggest_on_error sugg) + | _ -> raise CErrors.Unhandled) + + + (* spiwack: we need only one focus kind as we keep a stack of (distinct!) bullets *) + let bullet_kind = (new_focus_kind () : t list focus_kind) + let bullet_cond = done_cond ~loose_end:true bullet_kind + + (* spiwack: as it is bullets are reset (locally) by *any* non-bullet focusing command + experience will tell if this is the right discipline of if we want to be finer and + reset them only for a choice of bullets. *) + let get_bullets pr = + if is_last_focus bullet_kind pr then + get_at_focus bullet_kind pr + else + [] + + let has_bullet bul pr = + let rec has_bullet = function + | b'::_ when bullet_eq bul b' -> true + | _::l -> has_bullet l + | [] -> false + in + has_bullet (get_bullets pr) + + (* pop a bullet from proof [pr]. There should be at least one + bullet in use. If pop impossible (pending proofs on this level + of bullet or higher) then raise [Proof.CannotUnfocusThisWay]. *) + let pop pr = + match get_bullets pr with + | b::_ -> unfocus bullet_kind pr () , b + | _ -> assert false + + let push (b:t) pr = + focus bullet_cond (b::get_bullets pr) 1 pr + + (* Used only in the next function. + TODO: use a recursive function instead? *) + exception SuggestFound of t + + let suggest_bullet (prf : proof): suggestion = + if is_done prf then ProofFinished + else if not (no_focused_goal prf) + then (* No suggestion if a bullet is not mandatory, look for an unfinished bullet *) + match get_bullets prf with + | b::_ -> Unfinished b + | _ -> NoBulletInUse + else (* There is no goal under focus but some are unfocussed, + let us look at the bullet needed. If no *) + let pcobaye = ref prf in + try + while true do + let pcobaye', b = pop !pcobaye in + (* pop went well, this means that there are no more goals + *under this* bullet b, see if a new b can be pushed. *) + (try let _ = push b pcobaye' in (* push didn't fail so a new b can be pushed. *) + raise (SuggestFound b) + with SuggestFound _ as e -> raise e + | _ -> ()); (* b could not be pushed, so we must look for a outer bullet *) + pcobaye := pcobaye' + done; + assert false + with SuggestFound b -> Suggest b + | _ -> NeedClosingBrace (* No push was possible, but there are still + subgoals somewhere: there must be a "}" to use. *) + + + let rec pop_until (prf : proof) bul : proof = + let prf', b = pop prf in + if bullet_eq bul b then prf' + else pop_until prf' bul + + let put p bul = + try + if not (has_bullet bul p) then + (* bullet is not in use, so pushing it is always ok unless + no goal under focus. *) + push bul p + else + match suggest_bullet p with + | Suggest suggested_bullet when bullet_eq bul suggested_bullet + -> (* suggested_bullet is mandatory and you gave the right one *) + let p' = pop_until p bul in + push bul p' + (* the bullet you gave is in use but not the right one *) + | sugg -> raise (FailedBullet (bul,sugg)) + with NoSuchGoals _ -> (* push went bad *) + raise (FailedBullet (bul,suggest_bullet p)) + + let strict = { + name = "Strict Subproofs"; + put = put; + suggest = (fun prf -> suggest_on_solved_goal (suggest_bullet prf)) + + } + let _ = register_behavior strict +end + +(* Current bullet behavior, controlled by the option *) +let current_behavior = ref Strict.strict + +let _ = + Goptions.(declare_string_option { + optdepr = false; + optname = "bullet behavior"; + optkey = ["Bullet";"Behavior"]; + optread = begin fun () -> + (!current_behavior).name + end; + optwrite = begin fun n -> + current_behavior := + try Hashtbl.find behaviors n + with Not_found -> + CErrors.user_err Pp.(str ("Unknown bullet behavior: \"" ^ n ^ "\".")) + end + }) + +let put p b = + (!current_behavior).put p b + +let suggest p = + (!current_behavior).suggest p + +(**********************************************************) +(* *) +(* Default goal selector *) +(* *) +(**********************************************************) + + +(* Default goal selector: selector chosen when a tactic is applied + without an explicit selector. *) +let default_goal_selector = ref (Vernacexpr.SelectNth 1) +let get_default_goal_selector () = !default_goal_selector + +let pr_range_selector (i, j) = + if i = j then Pp.int i + else Pp.(int i ++ str "-" ++ int j) + +let pr_goal_selector = function + | Vernacexpr.SelectAll -> Pp.str "all" + | Vernacexpr.SelectNth i -> Pp.int i + | Vernacexpr.SelectList l -> + Pp.(str "[" + ++ prlist_with_sep pr_comma pr_range_selector l + ++ str "]") + | Vernacexpr.SelectId id -> Names.Id.print id + +let parse_goal_selector = function + | "all" -> Vernacexpr.SelectAll + | i -> + let err_msg = "The default selector must be \"all\" or a natural number." in + begin try + let i = int_of_string i in + if i < 0 then CErrors.user_err Pp.(str err_msg); + Vernacexpr.SelectNth i + with Failure _ -> CErrors.user_err Pp.(str err_msg) + end + +let _ = + Goptions.(declare_string_option{optdepr = false; + optname = "default goal selector" ; + optkey = ["Default";"Goal";"Selector"] ; + optread = begin fun () -> + Pp.string_of_ppcmds + (pr_goal_selector !default_goal_selector) + end; + optwrite = begin fun n -> + default_goal_selector := parse_goal_selector n + end + }) + diff --git a/proofs/proof_bullet.mli b/proofs/proof_bullet.mli new file mode 100644 index 0000000000..9ae521d3f0 --- /dev/null +++ b/proofs/proof_bullet.mli @@ -0,0 +1,53 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(**********************************************************) +(* *) +(* Bullets *) +(* *) +(**********************************************************) + +open Proof + +type t = Vernacexpr.bullet + +(** A [behavior] is the data of a put function which + is called when a bullet prefixes a tactic, a suggest function + suggesting the right bullet to use on a given proof, together + with a name to identify the behavior. *) +type behavior = { + name : string; + put : proof -> t -> proof; + suggest: proof -> Pp.t +} + +(** A registered behavior can then be accessed in Coq + through the command [Set Bullet Behavior "name"]. + + Two modes are registered originally: + * "Strict Subproofs": + - If this bullet follows another one of its kind, defocuses then focuses + (which fails if the focused subproof is not complete). + - If it is the first bullet of its kind, then focuses a new subproof. + * "None": bullets don't do anything *) +val register_behavior : behavior -> unit + +(** Handles focusing/defocusing with bullets: + *) +val put : proof -> t -> proof +val suggest : proof -> Pp.t + +(**********************************************************) +(* *) +(* Default goal selector *) +(* *) +(**********************************************************) + +val pr_goal_selector : Vernacexpr.goal_selector -> Pp.std_ppcmds +val get_default_goal_selector : unit -> Vernacexpr.goal_selector + diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 703bdff64e..52d6787d44 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -446,265 +446,6 @@ let set_terminator hook = | [] -> raise NoCurrentProof | p :: ps -> pstates := { p with terminator = CEphemeron.create hook } :: ps - - - -(**********************************************************) -(* *) -(* Bullets *) -(* *) -(**********************************************************) - -module Bullet = struct - - type t = Vernacexpr.bullet - - let bullet_eq b1 b2 = match b1, b2 with - | Vernacexpr.Dash n1, Vernacexpr.Dash n2 -> n1 = n2 - | Vernacexpr.Star n1, Vernacexpr.Star n2 -> n1 = n2 - | Vernacexpr.Plus n1, Vernacexpr.Plus n2 -> n1 = n2 - | _ -> false - - let pr_bullet b = - match b with - | Vernacexpr.Dash n -> str (String.make n '-') - | Vernacexpr.Star n -> str (String.make n '*') - | Vernacexpr.Plus n -> str (String.make n '+') - - - type behavior = { - name : string; - put : Proof.proof -> t -> Proof.proof; - suggest: Proof.proof -> std_ppcmds - } - - let behaviors = Hashtbl.create 4 - let register_behavior b = Hashtbl.add behaviors b.name b - - (*** initial modes ***) - let none = { - name = "None"; - put = (fun x _ -> x); - suggest = (fun _ -> mt ()) - } - let _ = register_behavior none - - module Strict = struct - type suggestion = - | Suggest of t (* this bullet is mandatory here *) - | Unfinished of t (* no mandatory bullet here, but this bullet is unfinished *) - | NoBulletInUse (* No mandatory bullet (or brace) here, no bullet pending, - some focused goals exists. *) - | NeedClosingBrace (* Some unfocussed goal exists "{" needed to focus them *) - | ProofFinished (* No more goal anywhere *) - - (* give a message only if more informative than the standard coq message *) - let suggest_on_solved_goal sugg = - match sugg with - | NeedClosingBrace -> str"Try unfocusing with \"}\"." - | NoBulletInUse -> mt () - | ProofFinished -> mt () - | Suggest b -> str"Focus next goal with bullet " ++ pr_bullet b ++ str"." - | Unfinished b -> str"The current bullet " ++ pr_bullet b ++ str" is unfinished." - - (* give always a message. *) - let suggest_on_error sugg = - match sugg with - | NeedClosingBrace -> str"Try unfocusing with \"}\"." - | NoBulletInUse -> assert false (* This should never raise an error. *) - | ProofFinished -> str"No more subgoals." - | Suggest b -> str"Expecting " ++ pr_bullet b ++ str"." - | Unfinished b -> str"Current bullet " ++ pr_bullet b ++ str" is not finished." - - exception FailedBullet of t * suggestion - - let _ = - CErrors.register_handler - (function - | FailedBullet (b,sugg) -> - let prefix = str"Wrong bullet " ++ pr_bullet b ++ str": " in - CErrors.user_err ~hdr:"Focus" (prefix ++ suggest_on_error sugg) - | _ -> raise CErrors.Unhandled) - - - (* spiwack: we need only one focus kind as we keep a stack of (distinct!) bullets *) - let bullet_kind = (Proof.new_focus_kind () : t list Proof.focus_kind) - let bullet_cond = Proof.done_cond ~loose_end:true bullet_kind - - (* spiwack: as it is bullets are reset (locally) by *any* non-bullet focusing command - experience will tell if this is the right discipline of if we want to be finer and - reset them only for a choice of bullets. *) - let get_bullets pr = - if Proof.is_last_focus bullet_kind pr then - Proof.get_at_focus bullet_kind pr - else - [] - - let has_bullet bul pr = - let rec has_bullet = function - | b'::_ when bullet_eq bul b' -> true - | _::l -> has_bullet l - | [] -> false - in - has_bullet (get_bullets pr) - - (* pop a bullet from proof [pr]. There should be at least one - bullet in use. If pop impossible (pending proofs on this level - of bullet or higher) then raise [Proof.CannotUnfocusThisWay]. *) - let pop pr = - match get_bullets pr with - | b::_ -> Proof.unfocus bullet_kind pr () , b - | _ -> assert false - - let push (b:t) pr = - Proof.focus bullet_cond (b::get_bullets pr) 1 pr - - (* Used only in the next function. - TODO: use a recursive function instead? *) - exception SuggestFound of t - - let suggest_bullet (prf:Proof.proof): suggestion = - if Proof.is_done prf then ProofFinished - else if not (Proof.no_focused_goal prf) - then (* No suggestion if a bullet is not mandatory, look for an unfinished bullet *) - match get_bullets prf with - | b::_ -> Unfinished b - | _ -> NoBulletInUse - else (* There is no goal under focus but some are unfocussed, - let us look at the bullet needed. If no *) - let pcobaye = ref prf in - try - while true do - let pcobaye', b = pop !pcobaye in - (* pop went well, this means that there are no more goals - *under this* bullet b, see if a new b can be pushed. *) - (try let _ = push b pcobaye' in (* push didn't fail so a new b can be pushed. *) - raise (SuggestFound b) - with SuggestFound _ as e -> raise e - | _ -> ()); (* b could not be pushed, so we must look for a outer bullet *) - pcobaye := pcobaye' - done; - assert false - with SuggestFound b -> Suggest b - | _ -> NeedClosingBrace (* No push was possible, but there are still - subgoals somewhere: there must be a "}" to use. *) - - - let rec pop_until (prf:Proof.proof) bul: Proof.proof = - let prf', b = pop prf in - if bullet_eq bul b then prf' - else pop_until prf' bul - - let put p bul = - try - if not (has_bullet bul p) then - (* bullet is not in use, so pushing it is always ok unless - no goal under focus. *) - push bul p - else - match suggest_bullet p with - | Suggest suggested_bullet when bullet_eq bul suggested_bullet - -> (* suggested_bullet is mandatory and you gave the right one *) - let p' = pop_until p bul in - push bul p' - (* the bullet you gave is in use but not the right one *) - | sugg -> raise (FailedBullet (bul,sugg)) - with Proof.NoSuchGoals _ -> (* push went bad *) - raise (FailedBullet (bul,suggest_bullet p)) - - let strict = { - name = "Strict Subproofs"; - put = put; - suggest = (fun prf -> suggest_on_solved_goal (suggest_bullet prf)) - - } - let _ = register_behavior strict - end - - (* Current bullet behavior, controlled by the option *) - let current_behavior = ref Strict.strict - - let _ = - Goptions.(declare_string_option { - optdepr = false; - optname = "bullet behavior"; - optkey = ["Bullet";"Behavior"]; - optread = begin fun () -> - (!current_behavior).name - end; - optwrite = begin fun n -> - current_behavior := - try Hashtbl.find behaviors n - with Not_found -> - CErrors.user_err Pp.(str ("Unknown bullet behavior: \"" ^ n ^ "\".")) - end - }) - - let put p b = - (!current_behavior).put p b - - let suggest p = - (!current_behavior).suggest p -end - - -let _ = - let hook n = - let prf = give_me_the_proof () in - (Bullet.suggest prf) in - Proofview.set_nosuchgoals_hook hook - - -(**********************************************************) -(* *) -(* Default goal selector *) -(* *) -(**********************************************************) - - -(* Default goal selector: selector chosen when a tactic is applied - without an explicit selector. *) -let default_goal_selector = ref (Vernacexpr.SelectNth 1) -let get_default_goal_selector () = !default_goal_selector - -let pr_range_selector (i, j) = - if i = j then int i - else int i ++ str "-" ++ int j - -let pr_goal_selector = function - | Vernacexpr.SelectAll -> str "all" - | Vernacexpr.SelectNth i -> int i - | Vernacexpr.SelectList l -> - str "[" - ++ prlist_with_sep pr_comma pr_range_selector l - ++ str "]" - | Vernacexpr.SelectId id -> Id.print id - -let parse_goal_selector = function - | "all" -> Vernacexpr.SelectAll - | i -> - let err_msg = "The default selector must be \"all\" or a natural number." in - begin try - let i = int_of_string i in - if i < 0 then CErrors.user_err Pp.(str err_msg); - Vernacexpr.SelectNth i - with Failure _ -> CErrors.user_err Pp.(str err_msg) - end - -let _ = - Goptions.(declare_string_option{optdepr = false; - optname = "default goal selector" ; - optkey = ["Default";"Goal";"Selector"] ; - optread = begin fun () -> - string_of_ppcmds - (pr_goal_selector !default_goal_selector) - end; - optwrite = begin fun n -> - default_goal_selector := parse_goal_selector n - end - }) - - module V82 = struct let get_current_initial_conclusions () = let { pid; strength; proof } = cur_pstate () in @@ -733,3 +474,11 @@ let update_global_env () = let tac = Proofview.Unsafe.tclEVARS (Evd.update_sigma_env sigma (Global.env ())) in let (p,(status,info)) = Proof.run_tactic (Global.env ()) tac p in (p, ()))) + +(* XXX: Bullet hook, should be really moved elsewhere *) +let _ = + let hook n = + let prf = give_me_the_proof () in + (Proof_bullet.suggest prf) in + Proofview.set_nosuchgoals_hook hook + diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 2c39389751..52f5f74046 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -121,52 +121,6 @@ val get_used_variables : unit -> Context.Named.t option val get_universe_binders : unit -> universe_binders option -(**********************************************************) -(* *) -(* Bullets *) -(* *) -(**********************************************************) - -module Bullet : sig - type t = Vernacexpr.bullet - - (** A [behavior] is the data of a put function which - is called when a bullet prefixes a tactic, a suggest function - suggesting the right bullet to use on a given proof, together - with a name to identify the behavior. *) - type behavior = { - name : string; - put : Proof.proof -> t -> Proof.proof; - suggest: Proof.proof -> Pp.std_ppcmds - } - - (** A registered behavior can then be accessed in Coq - through the command [Set Bullet Behavior "name"]. - - Two modes are registered originally: - * "Strict Subproofs": - - If this bullet follows another one of its kind, defocuses then focuses - (which fails if the focused subproof is not complete). - - If it is the first bullet of its kind, then focuses a new subproof. - * "None": bullets don't do anything *) - val register_behavior : behavior -> unit - - (** Handles focusing/defocusing with bullets: - *) - val put : Proof.proof -> t -> Proof.proof - val suggest : Proof.proof -> Pp.std_ppcmds -end - - -(**********************************************************) -(* *) -(* Default goal selector *) -(* *) -(**********************************************************) - -val pr_goal_selector : Vernacexpr.goal_selector -> Pp.std_ppcmds -val get_default_goal_selector : unit -> Vernacexpr.goal_selector - module V82 : sig val get_current_initial_conclusions : unit -> Names.Id.t *(EConstr.types list * Decl_kinds.goal_kind) diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index 804a543605..0ea2bd66be 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -5,6 +5,7 @@ Proof_using Logic Refine Proof +Proof_bullet Proof_global Redexpr Refiner diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 7a85956538..6cb56d64f9 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -92,7 +92,7 @@ open Goptions let _ = declare_bool_option - { optdepr = true; + { optdepr = true; (* remove in 8.8 *) optname = "do typeclass search modulo eta conversion"; optkey = ["Typeclasses";"Modulo";"Eta"]; optread = get_typeclasses_modulo_eta; @@ -125,7 +125,7 @@ let _ = let _ = declare_bool_option - { optdepr = false; + { optdepr = true; (* remove in 8.8 *) optname = "compat"; optkey = ["Typeclasses";"Legacy";"Resolution"]; optread = get_typeclasses_legacy_resolution; @@ -494,16 +494,15 @@ let catchable = function | Refiner.FailError _ -> true | e -> Logic.catchable_exception e -(* alternate separators in debug search path output *) -let debug_seps = [| "." ; "-" |] -let next_sep seps = - let num_seps = Array.length seps in - let sep_index = ref 0 in - fun () -> - let sep = seps.(!sep_index) in - sep_index := (!sep_index + 1) mod num_seps; - str sep -let pr_depth l = prlist_with_sep (next_sep debug_seps) int (List.rev l) +let pr_depth l = + let rec fmt elts = + match elts with + | [] -> [] + | [n] -> [string_of_int n] + | n1::n2::rest -> + (string_of_int n1 ^ "." ^ string_of_int n2) :: fmt rest + in + prlist_with_sep (fun () -> str "-") str (fmt (List.rev l)) let is_Prop env sigma concl = let ty = Retyping.get_type_of env sigma concl in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index c979b8b040..8a95ad177d 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -80,15 +80,15 @@ let _ = optread = (fun () -> !Flags.tactic_context_compat) ; optwrite = (fun b -> Flags.tactic_context_compat := b) } -let apply_solve_class_goals = ref (false) -let _ = Goptions.declare_bool_option { - Goptions.optdepr = true; - Goptions.optname = - "Perform typeclass resolution on apply-generated subgoals."; - Goptions.optkey = ["Typeclass";"Resolution";"After";"Apply"]; - Goptions.optread = (fun () -> !apply_solve_class_goals); - Goptions.optwrite = (fun a -> apply_solve_class_goals:=a); -} +let apply_solve_class_goals = ref false + +let _ = + declare_bool_option + { optdepr = true; (* remove in 8.8 *) + optname = "Perform typeclass resolution on apply-generated subgoals."; + optkey = ["Typeclass";"Resolution";"After";"Apply"]; + optread = (fun () -> !apply_solve_class_goals); + optwrite = (fun a -> apply_solve_class_goals := a); } let clear_hyp_by_default = ref false @@ -124,7 +124,7 @@ let shrink_abstract = ref true let _ = declare_bool_option - { optdepr = true; + { optdepr = true; (* remove in 8.8 *) optname = "shrinking of abstracted proofs"; optkey = ["Shrink"; "Abstract"]; optread = (fun () -> !shrink_abstract) ; @@ -143,7 +143,7 @@ let use_bracketing_last_or_and_intro_pattern () = let _ = declare_bool_option - { optdepr = true; (* remove in 8.8 *) + { optdepr = false; optname = "bracketing last or-and introduction pattern"; optkey = ["Bracketing";"Last";"Introduction";"Pattern"]; optread = (fun () -> !bracketing_last_or_and_intro_pattern); diff --git a/test-suite/coq-makefile/timing/after/Fast.v b/test-suite/coq-makefile/timing/after/Fast.v new file mode 100644 index 0000000000..54d3cfc3eb --- /dev/null +++ b/test-suite/coq-makefile/timing/after/Fast.v @@ -0,0 +1,4 @@ +Require Coq.ZArith.BinInt. +Definition foo0 := Eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl. +Definition foo1 := Eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl. +Definition foo2 := Eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl. diff --git a/test-suite/coq-makefile/timing/after/Slow.v b/test-suite/coq-makefile/timing/after/Slow.v new file mode 100644 index 0000000000..8b13789179 --- /dev/null +++ b/test-suite/coq-makefile/timing/after/Slow.v @@ -0,0 +1 @@ + diff --git a/test-suite/coq-makefile/timing/after/_CoqProject b/test-suite/coq-makefile/timing/after/_CoqProject new file mode 100644 index 0000000000..36c3a18c2b --- /dev/null +++ b/test-suite/coq-makefile/timing/after/_CoqProject @@ -0,0 +1,2 @@ +Slow.v +Fast.v diff --git a/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired b/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired new file mode 100644 index 0000000000..729de2f366 --- /dev/null +++ b/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired @@ -0,0 +1,16 @@ +Makefile:69: warning: undefined variable '*' +Makefile:204: warning: undefined variable 'DSTROOT' +COQDEP Fast.v +COQDEP Slow.v +Makefile:69: warning: undefined variable '*' +Makefile:204: warning: undefined variable 'DSTROOT' +Makefile:69: warning: undefined variable '*' +Makefile:204: warning: undefined variable 'DSTROOT' +Makefile:69: warning: undefined variable '*' +Makefile:204: warning: undefined variable 'DSTROOT' +COQC Slow.v +Slow (real: 0.04, user: 0.02, sys: 0.01, mem: 45512 ko) +COQC Fast.v +Fast (real: 0.41, user: 0.37, sys: 0.04, mem: 395200 ko) +Makefile:69: warning: undefined variable '*' +Makefile:204: warning: undefined variable 'DSTROOT' diff --git a/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired b/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired new file mode 100644 index 0000000000..b25bc3683c --- /dev/null +++ b/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired @@ -0,0 +1,16 @@ +Makefile:69: warning: undefined variable '*' +Makefile:204: warning: undefined variable 'DSTROOT' +COQDEP Fast.v +COQDEP Slow.v +Makefile:69: warning: undefined variable '*' +Makefile:204: warning: undefined variable 'DSTROOT' +Makefile:69: warning: undefined variable '*' +Makefile:204: warning: undefined variable 'DSTROOT' +Makefile:69: warning: undefined variable '*' +Makefile:204: warning: undefined variable 'DSTROOT' +COQC Slow.v +Slow (real: 0.40, user: 0.35, sys: 0.04, mem: 394968 ko) +COQC Fast.v +Fast (real: 0.04, user: 0.03, sys: 0.00, mem: 46564 ko) +Makefile:69: warning: undefined variable '*' +Makefile:204: warning: undefined variable 'DSTROOT' diff --git a/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired b/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired new file mode 100644 index 0000000000..56815d241e --- /dev/null +++ b/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired @@ -0,0 +1,6 @@ +After | File Name | Before || Change | % Change +-------------------------------------------------------- +0m00.38s | Total | 0m00.39s || -0m00.01s | -2.56% +-------------------------------------------------------- +0m00.35s | Slow | 0m00.02s || +0m00.32s | +1649.99% +0m00.03s | Fast | 0m00.37s || -0m00.34s | -91.89%
\ No newline at end of file diff --git a/test-suite/coq-makefile/timing/aggregate/Fast.v b/test-suite/coq-makefile/timing/aggregate/Fast.v new file mode 100644 index 0000000000..8b13789179 --- /dev/null +++ b/test-suite/coq-makefile/timing/aggregate/Fast.v @@ -0,0 +1 @@ + diff --git a/test-suite/coq-makefile/timing/aggregate/Slow.v b/test-suite/coq-makefile/timing/aggregate/Slow.v new file mode 100644 index 0000000000..54d3cfc3eb --- /dev/null +++ b/test-suite/coq-makefile/timing/aggregate/Slow.v @@ -0,0 +1,4 @@ +Require Coq.ZArith.BinInt. +Definition foo0 := Eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl. +Definition foo1 := Eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl. +Definition foo2 := Eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl. diff --git a/test-suite/coq-makefile/timing/aggregate/_CoqProject b/test-suite/coq-makefile/timing/aggregate/_CoqProject new file mode 100644 index 0000000000..36c3a18c2b --- /dev/null +++ b/test-suite/coq-makefile/timing/aggregate/_CoqProject @@ -0,0 +1,2 @@ +Slow.v +Fast.v diff --git a/test-suite/coq-makefile/timing/before/Fast.v b/test-suite/coq-makefile/timing/before/Fast.v new file mode 100644 index 0000000000..8b13789179 --- /dev/null +++ b/test-suite/coq-makefile/timing/before/Fast.v @@ -0,0 +1 @@ + diff --git a/test-suite/coq-makefile/timing/before/Slow.v b/test-suite/coq-makefile/timing/before/Slow.v new file mode 100644 index 0000000000..54d3cfc3eb --- /dev/null +++ b/test-suite/coq-makefile/timing/before/Slow.v @@ -0,0 +1,4 @@ +Require Coq.ZArith.BinInt. +Definition foo0 := Eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl. +Definition foo1 := Eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl. +Definition foo2 := Eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl. diff --git a/test-suite/coq-makefile/timing/before/_CoqProject b/test-suite/coq-makefile/timing/before/_CoqProject new file mode 100644 index 0000000000..36c3a18c2b --- /dev/null +++ b/test-suite/coq-makefile/timing/before/_CoqProject @@ -0,0 +1,2 @@ +Slow.v +Fast.v diff --git a/test-suite/coq-makefile/timing/error/A.v b/test-suite/coq-makefile/timing/error/A.v new file mode 100644 index 0000000000..932363a122 --- /dev/null +++ b/test-suite/coq-makefile/timing/error/A.v @@ -0,0 +1 @@ +Check I : I. diff --git a/test-suite/coq-makefile/timing/error/_CoqProject b/test-suite/coq-makefile/timing/error/_CoqProject new file mode 100644 index 0000000000..790e057133 --- /dev/null +++ b/test-suite/coq-makefile/timing/error/_CoqProject @@ -0,0 +1 @@ +A.v diff --git a/test-suite/coq-makefile/timing/per-file-after/A.v b/test-suite/coq-makefile/timing/per-file-after/A.v new file mode 100644 index 0000000000..851e2b9738 --- /dev/null +++ b/test-suite/coq-makefile/timing/per-file-after/A.v @@ -0,0 +1,4 @@ +Require Coq.ZArith.BinInt. +Declare Reduction comp := native_compute. +Definition foo0 := Eval comp in (Coq.ZArith.BinInt.Z.div_eucl, Coq.ZArith.BinInt.Z.div_eucl). +Definition foo1 := Eval comp in (foo0, foo0). diff --git a/test-suite/coq-makefile/timing/per-file-after/A.v.timing.diff.desired b/test-suite/coq-makefile/timing/per-file-after/A.v.timing.diff.desired new file mode 100644 index 0000000000..18f0f34b28 --- /dev/null +++ b/test-suite/coq-makefile/timing/per-file-after/A.v.timing.diff.desired @@ -0,0 +1,9 @@ +After | Code | Before || Change | % Change +--------------------------------------------------------------------------------------------------- +0m00.50s | Total | 0m04.17s || -0m03.66s | -87.96% +--------------------------------------------------------------------------------------------------- +0m00.145s | Chars 069 - 162 [Definition~foo0~:=~Eval~comp~i...] | 0m00.192s || -0m00.04s | -24.47% +0m00.126s | Chars 000 - 026 [Require~Coq.ZArith.BinInt.] | 0m00.143s || -0m00.01s | -11.88% + N/A | Chars 027 - 068 [Declare~Reduction~comp~:=~nati...] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 027 - 068 [Declare~Reduction~comp~:=~vm_c...] | N/A || +0m00.00s | N/A +0m00.231s | Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] | 0m03.836s || -0m03.60s | -93.97%
\ No newline at end of file diff --git a/test-suite/coq-makefile/timing/per-file-after/_CoqProject b/test-suite/coq-makefile/timing/per-file-after/_CoqProject new file mode 100644 index 0000000000..790e057133 --- /dev/null +++ b/test-suite/coq-makefile/timing/per-file-after/_CoqProject @@ -0,0 +1 @@ +A.v diff --git a/test-suite/coq-makefile/timing/per-file-before/A.v b/test-suite/coq-makefile/timing/per-file-before/A.v new file mode 100644 index 0000000000..115c1f95bd --- /dev/null +++ b/test-suite/coq-makefile/timing/per-file-before/A.v @@ -0,0 +1,4 @@ +Require Coq.ZArith.BinInt. +Declare Reduction comp := vm_compute. +Definition foo0 := Eval comp in (Coq.ZArith.BinInt.Z.div_eucl, Coq.ZArith.BinInt.Z.div_eucl). +Definition foo1 := Eval comp in (foo0, foo0). diff --git a/test-suite/coq-makefile/timing/per-file-before/_CoqProject b/test-suite/coq-makefile/timing/per-file-before/_CoqProject new file mode 100644 index 0000000000..790e057133 --- /dev/null +++ b/test-suite/coq-makefile/timing/per-file-before/_CoqProject @@ -0,0 +1 @@ +A.v diff --git a/test-suite/coq-makefile/timing/run.sh b/test-suite/coq-makefile/timing/run.sh new file mode 100755 index 0000000000..9786af10a8 --- /dev/null +++ b/test-suite/coq-makefile/timing/run.sh @@ -0,0 +1,68 @@ +#!/usr/bin/env bash + +#set -x +set -e + +. ../template/init.sh + +cd error +coq_makefile -f _CoqProject -o Makefile +make cleanall +if make pretty-timed TGTS="all" -j1; then + echo "Error: make pretty-timed should have failed" + exit 1 +fi + +cd ../aggregate +coq_makefile -f _CoqProject -o Makefile +make cleanall +make pretty-timed TGTS="all" -j1 || exit $? + +cd ../before +coq_makefile -f _CoqProject -o Makefile +make cleanall +make make-pretty-timed-before TGTS="all" -j1 || exit $? + +cd ../after +coq_makefile -f _CoqProject -o Makefile +make cleanall +make make-pretty-timed-after TGTS="all" -j1 || exit $? +rm -f time-of-build-before.log +make print-pretty-timed-diff TIME_OF_BUILD_BEFORE_FILE=../before/time-of-build-before.log +cp ../before/time-of-build-before.log ./ +make print-pretty-timed-diff || exit $? + +for ext in "" .desired; do + for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do + cat ${file}${ext} | grep -v 'warning: undefined variable' | sed s'/[0-9]//g' | sed s'/ *$//g' | sed s'/^-*$/------/g' | sed s'/ */ /g' | sed s'/\(Total.*\)-\(.*\)-/\1+\2+/g' > ${file}${ext}.processed + done +done +for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do + diff -u $file.desired.processed $file.processed || exit $? +done + +cd ../per-file-before +coq_makefile -f _CoqProject -o Makefile +make cleanall +make all TIMING=before -j2 || exit $? + +cd ../per-file-after +coq_makefile -f _CoqProject -o Makefile +make cleanall +make all TIMING=after -j2 || exit $? + +find ../per-file-before/ -name "*.before-timing" -exec 'cp' '{}' './' ';' +make all.timing.diff -j2 || exit $? +cat A.v.timing.diff +echo + +for ext in "" .desired; do + for file in A.v.timing.diff; do + cat ${file}${ext} | sed s'/[0-9]*\.[0-9]*//g' | sed s'/0//g' | sed s'/ */ /g' | sed s'/+/-/g' | sort > ${file}${ext}.processed + done +done +for file in A.v.timing.diff; do + diff -u $file.desired.processed $file.processed || exit $? +done + +exit 0 diff --git a/test-suite/output/TypeclassDebug.out b/test-suite/output/TypeclassDebug.out new file mode 100644 index 0000000000..73369ab713 --- /dev/null +++ b/test-suite/output/TypeclassDebug.out @@ -0,0 +1,18 @@ +Debug: 1: looking for foo without backtracking +Debug: 1.1: simple apply H on foo, 1 subgoal(s) +Debug: 1.1-2 : foo +Debug: 1.1-2: looking for foo without backtracking +Debug: 1.1-2.1: simple apply H on foo, 1 subgoal(s) +Debug: 1.1-2.1-2 : foo +Debug: 1.1-2.1-2: looking for foo without backtracking +Debug: 1.1-2.1-2.1: simple apply H on foo, 1 subgoal(s) +Debug: 1.1-2.1-2.1-2 : foo +Debug: 1.1-2.1-2.1-2: looking for foo without backtracking +Debug: 1.1-2.1-2.1-2.1: simple apply H on foo, 1 subgoal(s) +Debug: 1.1-2.1-2.1-2.1-2 : foo +Debug: 1.1-2.1-2.1-2.1-2: looking for foo without backtracking +Debug: 1.1-2.1-2.1-2.1-2.1: simple apply H on foo, 1 subgoal(s) +Debug: 1.1-2.1-2.1-2.1-2.1-2 : foo +The command has indeed failed with message: +Ltac call to "typeclasses eauto (int_or_var_opt) with (ne_preident_list)" failed. +Tactic failure: Proof search reached its limit. diff --git a/test-suite/output/TypeclassDebug.v b/test-suite/output/TypeclassDebug.v new file mode 100644 index 0000000000..d38e2a50e4 --- /dev/null +++ b/test-suite/output/TypeclassDebug.v @@ -0,0 +1,8 @@ +(* show alternating separators in typeclass debug output; see discussion in PR #868 *) + +Parameter foo : Prop. +Axiom H : foo -> foo. +Hint Resolve H : foo. +Goal foo. +Typeclasses eauto := debug. +Fail typeclasses eauto 5 with foo. diff --git a/test-suite/output/inference.v b/test-suite/output/inference.v index f761a4dc5a..73169dae65 100644 --- a/test-suite/output/inference.v +++ b/test-suite/output/inference.v @@ -14,6 +14,7 @@ Definition P (e:option L) := Print P. (* Check that plus is folded even if reduction is involved *) +Set Warnings Append "-deprecated-option". Set Refolding Reduction. Check (fun m n p (H : S m <= (S n) + p) => le_S_n _ _ H). diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 99937e8e0f..22e10e2e43 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -336,7 +336,7 @@ Proof. intros. apply CompareSpec2Type; assumption. Defined. (** [identity A a] is the family of datatypes on [A] whose sole non-empty member is the singleton datatype [identity A a a] whose - sole inhabitant is denoted [refl_identity A a] *) + sole inhabitant is denoted [identity_refl A a] *) Inductive identity (A:Type) (a:A) : A -> Type := identity_refl : identity a a. diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 86be54d462..7d281977af 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -10,6 +10,7 @@ INITIAL_VARS := $(.VARIABLES) # To implement recursion we save the name of the main Makefile SELF := $(lastword $(MAKEFILE_LIST)) +PARENT := $(firstword $(MAKEFILE_LIST)) # This file is generated by coq_makefile and contains many variable # definitions, like the list of .v files or the path to Coq @@ -62,7 +63,21 @@ VERBOSE ?= # Time the Coq process (set to non empty), and how (see default value) TIMED?= TIMECMD?= -STDTIME?=/usr/bin/time -f "$* (real: %e, user: %U, sys: %S, mem: %M ko)" +# Use /usr/bin/time on linux, gtime on Mac OS +TIMEFMT?="$* (real: %e, user: %U, sys: %S, mem: %M ko)" +ifneq (,$(TIMED)) +ifeq (0,$(shell /usr/bin/time -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?)) +STDTIME?=/usr/bin/time -f $(TIMEFMT) +else +ifeq (0,$(shell gtime -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?)) +STDTIME?=gtime -f $(TIMEFMT) +else +STDTIME?=time +endif +endif +else +STDTIME?=/usr/bin/time -f $(TIMEFMT) +endif # Coq binaries COQC ?= "$(COQBIN)coqc" @@ -72,6 +87,11 @@ COQDEP ?= "$(COQBIN)coqdep" GALLINA ?= "$(COQBIN)gallina" COQDOC ?= "$(COQBIN)coqdoc" COQMKTOP ?= "$(COQBIN)coqmktop" +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 ?= # OCaml binaries CAMLC ?= "$(OCAMLFIND)" ocamlc -c -rectypes -thread @@ -88,7 +108,15 @@ DESTDIR ?= CAMLDEBUG ?= COQDEBUG ?= - +# Option for making timing files +TIMING?= +# 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 @@ -157,6 +185,21 @@ COQLIBINSTALL = $(COQLIB)user-contrib COQDOCINSTALL = $(DOCDIR)user-contrib COQTOPINSTALL = $(COQLIB)toploop +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, DESTROOT is not) ifneq "$(DSTROOT)" "" DESTDIR := $(DSTROOT) @@ -256,6 +299,41 @@ 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) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_BUILD_AFTER_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 BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing' + $(HIDE)false +else +ifeq (,$(AFTER)) +print-pretty-single-time-diff:: + @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing' + $(HIDE)false +else +print-pretty-single-time-diff:: + $(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) $(BEFORE) $(AFTER) $(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 @@ -272,6 +350,9 @@ post-all:: real-all: $(VOFILES) $(if $(USEBYTE),bytefiles,optfiles) .PHONY: real-all +real-all.timing.diff: $(VOFILES:.vo=.v.timing.diff) +.PHONE: real-all.timing.diff + bytefiles: $(CMOFILES) $(CMAFILES) .PHONY: bytefiles @@ -445,13 +526,19 @@ clean:: $(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' + $(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:: @@ -520,9 +607,15 @@ $(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix $(SHOW)'[deprecated,use-mllib-or-mlpack] CAMLOPT -shared -o $@' $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -shared -o $@ $< +ifneq (,$(TIMING)) +TIMING_EXTRA = > $<.$(TIMING_EXT) +else +TIMING_EXTRA = +endif + $(VOFILES): %.vo: %.v $(SHOW)COQC $< - $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $< + $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $< $(TIMING_EXTRA) # FIXME ?merge with .vo / .vio ? $(GLOBFILES): %.glob: %.v @@ -532,6 +625,10 @@ $(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 $< @@ -558,7 +655,7 @@ $(GHTMLFILES): %.g.html: %.v %.glob # Dependency files ############################################################ -ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),) +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),) diff --git a/tools/TimeFileMaker.py b/tools/TimeFileMaker.py new file mode 100644 index 0000000000..a207c2171b --- /dev/null +++ b/tools/TimeFileMaker.py @@ -0,0 +1,187 @@ +#!/usr/bin/env python +from __future__ import with_statement +import os, sys, re + +# 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 = '\xe2\x88\x9e' + +def reformat_time_string(time): + seconds, milliseconds = time.split('.') + seconds = int(seconds) + minutes, seconds = int(seconds / 60), 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') as f: + lines = f.read() + reg = re.compile(r'^([^\s]+) \([^\)]*?user: ([0-9\.]+)[^\)]*?\)$', 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\.]+)[^\)]*?\)$', 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') 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 make_sorting_key(times_dict, descending=True): + def get_key(name): + minutes, seconds = times_dict[name].replace('s', '').split('m') + def fix_sign(num): + return -num if descending else num + return (fix_sign(int(minutes)), fix_sign(float(seconds)), 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. + ''' + return from_seconds(sum(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, + 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 = make_sorting_key(all_names_dict, descending=descending) + all_names_dict = dict((name, (abs(int(to_seconds(diff_times_dict[name]))), get_key(name))) + for name in all_names_dict.keys()) + names = sorted(all_names_dict.keys(), key=all_names_dict.get) + #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(map(to_seconds, left_times_dict.values())) + right_sum_float = sum(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: + print(table) + for file_name in files: + if file_name != '-': + with open(file_name, 'w') as f: + f.write(table) diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 43f7670a66..c3aedf538e 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -197,7 +197,7 @@ let generate_conf_coq_config oc args bypass_API = section oc "Coq configuration."; let src_dirs = if bypass_API then Coq_config.all_src_dirs - else Coq_config.api_dirs @ Coq_config.plugins_dirs in + else Coq_config.api_dirs @ Coq_config.plugins_dirs @ ["-open API"] in Envars.print_config ~prefix_var_name:"COQMF_" oc src_dirs; fprintf oc "COQMF_MAKEFILE=%s\n" (quote (List.hd args)); ;; diff --git a/tools/make-both-single-timing-files.py b/tools/make-both-single-timing-files.py new file mode 100755 index 0000000000..2d33503c36 --- /dev/null +++ b/tools/make-both-single-timing-files.py @@ -0,0 +1,18 @@ +#!/usr/bin/env python +import sys +from TimeFileMaker import * + +if __name__ == '__main__': + USAGE = 'Usage: %s 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''' + if len(sys.argv) < 3 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: + left_dict = get_single_file_times(sys.argv[1]) + right_dict = get_single_file_times(sys.argv[2]) + table = make_diff_table_string(left_dict, right_dict, tag="Code") + print_or_write_table(table, sys.argv[3:]) diff --git a/tools/make-both-time-files.py b/tools/make-both-time-files.py new file mode 100755 index 0000000000..69ec5a6631 --- /dev/null +++ b/tools/make-both-time-files.py @@ -0,0 +1,22 @@ +#!/usr/bin/env python +import sys +from TimeFileMaker import * + +if __name__ == '__main__': + USAGE = 'Usage: %s 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...) +''' + if len(sys.argv) < 3 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: + left_dict = get_times(sys.argv[1]) + right_dict = get_times(sys.argv[2]) + table = make_diff_table_string(left_dict, right_dict) + print_or_write_table(table, sys.argv[3:]) diff --git a/tools/make-one-time-file.py b/tools/make-one-time-file.py new file mode 100755 index 0000000000..e66136df9d --- /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/vernac/obligations.ml b/vernac/obligations.ml index 4b1565d3ce..10d3317f8d 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -350,7 +350,7 @@ let get_shrink_obligations () = !shrink_obligations let _ = declare_bool_option - { optdepr = true; + { optdepr = true; (* remove in 8.8 *) optname = "Shrinking of Program obligations"; optkey = ["Shrink";"Obligations"]; optread = get_shrink_obligations; diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 8a647c6c18..9650ea19d7 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1811,9 +1811,9 @@ let vernac_end_subproof () = Proof_global.simple_with_current_proof (fun _ p -> Proof.unfocus subproof_kind p ()) -let vernac_bullet (bullet:Proof_global.Bullet.t) = +let vernac_bullet (bullet : Proof_bullet.t) = Proof_global.simple_with_current_proof (fun _ p -> - Proof_global.Bullet.put p bullet) + Proof_bullet.put p bullet) let vernac_show = let open Feedback in function | ShowScript -> assert false (* Only the stm knows the script *) |