diff options
238 files changed, 1290 insertions, 704 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/checker/indtypes.ml b/checker/indtypes.ml index 92e94c1ab0..22c8438126 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -525,10 +525,10 @@ let check_positivity env_ar mind params nrecp inds = Array.iter2 (fun ind wfpi -> check_subtree ind.mind_recargs wfpi) inds wfp (* Check arities and constructors *) -let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : constr) numparams is_arity = +let check_subtyping_arity_constructor env (subst : Univ.Instance.t) (arcn : constr) numparams is_arity = let numchecked = ref 0 in let basic_check ev tp = - if !numchecked < numparams then () else conv_leq ev tp (subst tp); + if !numchecked < numparams then () else conv_leq ev tp (Term.subst_instance_constr subst tp); numchecked := !numchecked + 1 in let check_typ typ typ_env = @@ -548,26 +548,27 @@ let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : con (* Check that the subtyping information inferred for inductive types in the block is correct. *) (* This check produces a value of the unit type if successful or raises an anomaly if check fails. *) -let check_subtyping cumi paramsctxt env_ar inds = +let check_subtyping cumi paramsctxt env inds = + let open Univ in let numparams = rel_context_nhyps paramsctxt in - let sbsubst = Univ.CumulativityInfo.subtyping_susbst cumi in - let other_instnace = Univ.CumulativityInfo.subtyping_other_instance cumi in - let dosubst = subst_univs_level_constr sbsubst in - let uctx = Univ.CumulativityInfo.univ_context cumi in - let uctx_other = Univ.UContext.make (other_instnace, Univ.UContext.constraints uctx) in - let env = Environ.push_context uctx env_ar - in - let env = Environ.push_context uctx_other env - in - let env = Environ.push_context - (Univ.CumulativityInfo.subtyp_context cumi) env - in + (** In [env] we already have [ Var(0) ... Var(n-1) |- cst ] available. + We must produce the substitution σ : [ Var(i) -> Var (i + n) | 0 <= i < n] + and push the constraints [ Var(n) ... Var(2n - 1) |- cst{σ} ], together + with the cumulativity constraints [ cumul_cst ]. *) + let len = AUContext.size (ACumulativityInfo.univ_context cumi) in + let inst = Instance.of_array (Array.init len (fun i -> Level.var (i + len))) in + let other_context = ACumulativityInfo.univ_context cumi in + let uctx_other = UContext.make (inst, AUContext.instantiate inst other_context) in + let cumul_context = AUContext.repr (ACumulativityInfo.subtyp_context cumi) in + let cumul_cst = UContext.constraints cumul_context in + let env = Environ.push_context uctx_other env in + let env = Environ.add_constraints cumul_cst env in (* process individual inductive types: *) Array.iter (fun { mind_user_lc = lc; mind_arity = arity } -> match arity with | RegularArity { mind_user_arity = full_arity} -> - check_subtyping_arity_constructor env dosubst full_arity numparams true; - Array.iter (fun cnt -> check_subtyping_arity_constructor env dosubst cnt numparams false) lc + check_subtyping_arity_constructor env inst full_arity numparams true; + Array.iter (fun cnt -> check_subtyping_arity_constructor env inst cnt numparams false) lc | TemplateArity _ -> () ) inds @@ -579,10 +580,10 @@ let check_inductive env kn mib = (* check mind_constraints: should be consistent with env *) let ind_ctx = match mib.mind_universes with - | Monomorphic_ind ctx -> ctx - | Polymorphic_ind auctx -> Univ.instantiate_univ_context auctx + | Monomorphic_ind _ -> Univ.UContext.empty (** Already in the global environment *) + | Polymorphic_ind auctx -> Univ.AUContext.repr auctx | Cumulative_ind cumi -> - Univ.instantiate_univ_context (Univ.ACumulativityInfo.univ_context cumi) + Univ.AUContext.repr (Univ.ACumulativityInfo.univ_context cumi) in let env = Environ.push_context ind_ctx env in (* check mind_record : TODO ? check #constructor = 1 ? *) @@ -606,8 +607,7 @@ let check_inductive env kn mib = match mib.mind_universes with | Monomorphic_ind _ | Polymorphic_ind _ -> () | Cumulative_ind acumi -> - check_subtyping - (Univ.instantiate_cumulativity_info acumi) params env_ar mib.mind_packets + check_subtyping acumi params env_ar mib.mind_packets in (* check mind_nparams_rec: positivity condition *) check_positivity env_ar kn params mib.mind_nparams_rec mib.mind_packets; diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 15e9ae2951..4948f6008f 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -26,22 +26,21 @@ let refresh_arity ar = let check_constant_declaration env kn cb = Feedback.msg_notice (str " checking cst:" ++ prcon kn); - let env', u = + (** [env'] contains De Bruijn universe variables *) + let env' = match cb.const_universes with - | Monomorphic_const ctx -> push_context ~strict:true ctx env, Univ.Instance.empty + | Monomorphic_const ctx -> push_context ~strict:true ctx env | Polymorphic_const auctx -> - let ctx = Univ.instantiate_univ_context auctx in - push_context ~strict:false ctx env, Univ.UContext.instance ctx + let ctx = Univ.AUContext.repr auctx in + push_context ~strict:false ctx env in let envty, ty = match cb.const_type with RegularArity ty -> - let ty = subst_instance_constr u ty in let ty', cu = refresh_arity ty in let envty = push_context_set cu env' in let _ = infer_type envty ty' in envty, ty | TemplateArity(ctxt,par) -> - assert(Univ.Instance.is_empty u); let _ = check_ctxt env' ctxt in check_polymorphic_arity env' ctxt par; env', it_mkProd_or_LetIn (Sort(Type par.template_level)) ctxt @@ -49,7 +48,6 @@ let check_constant_declaration env kn cb = let () = match body_of_constant cb with | Some bd -> - let bd = subst_instance_constr u bd in (match cb.const_proj with | None -> let j = infer envty bd in conv_leq envty j ty diff --git a/checker/term.ml b/checker/term.ml index 9bcb15bc72..5995dfcc61 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -447,37 +447,3 @@ let subst_instance_constr subst c = let subst_instance_context s ctx = if Univ.Instance.is_empty s then ctx else map_rel_context (fun x -> subst_instance_constr s x) ctx - -let subst_univs_level_constr subst c = - if Univ.is_empty_level_subst subst then c - else - let f = Univ.Instance.subst_fn (Univ.subst_univs_level_level subst) in - let changed = ref false in - let rec aux t = - match t with - | Const (c, u) -> - if Univ.Instance.is_empty u then t - else - let u' = f u in - if u' == u then t - else (changed := true; Const (c, u')) - | Ind (i, u) -> - if Univ.Instance.is_empty u then t - else - let u' = f u in - if u' == u then t - else (changed := true; Ind (i, u')) - | Construct (c, u) -> - if Univ.Instance.is_empty u then t - else - let u' = f u in - if u' == u then t - else (changed := true; Construct (c, u')) - | Sort (Type u) -> - let u' = Univ.subst_univs_level_universe subst u in - if u' == u then t else - (changed := true; Sort (sort_of_univ u')) - | _ -> map_constr aux t - in - let c' = aux c in - if !changed then c' else c diff --git a/checker/term.mli b/checker/term.mli index ccf5b59e0c..679a56ee45 100644 --- a/checker/term.mli +++ b/checker/term.mli @@ -57,4 +57,3 @@ val eq_constr : constr -> constr -> bool (** Instance substitution for polymorphism. *) val subst_instance_constr : Univ.universe_instance -> constr -> constr val subst_instance_context : Univ.universe_instance -> rel_context -> rel_context -val subst_univs_level_constr : Univ.universe_level_subst -> constr -> constr diff --git a/checker/univ.ml b/checker/univ.ml index 2cd4252b20..e3abc436f0 100644 --- a/checker/univ.ml +++ b/checker/univ.ml @@ -1075,6 +1075,7 @@ module Instance : sig val check_eq : t check_function val length : t -> int val append : t -> t -> t + val of_array : Level.t array -> t end = struct type t = Level.t array @@ -1157,7 +1158,9 @@ struct let length = Array.length let append = Array.append - + + let of_array i = i + end (** Substitute instance inst for ctx in csts *) @@ -1231,43 +1234,11 @@ module CumulativityInfo = struct type t = universe_context * universe_context - let make x = - if (Array.length (UContext.instance (snd x))) = - (Array.length (UContext.instance (fst x))) * 2 then x - else anomaly (Pp.str "Invalid subtyping information encountered!") - - let empty = (UContext.empty, UContext.empty) - - let halve_context ctx = - let len = Array.length ctx in - let halflen = len / 2 in - ((Array.sub ctx 0 halflen), (Array.sub ctx halflen halflen)) - let univ_context (univcst, subtypcst) = univcst let subtyp_context (univcst, subtypcst) = subtypcst - let create_trivial_subtyping ctx ctx' = - CArray.fold_left_i - (fun i cst l -> Constraint.add (l, Eq, Array.get ctx' i) cst) - Constraint.empty ctx - - let from_universe_context univcst freshunivs = - let inst = (UContext.instance univcst) in - assert (Array.length freshunivs = Array.length inst); - (univcst, UContext.make (Array.append inst freshunivs, - create_trivial_subtyping inst freshunivs)) - - let subtyping_other_instance (univcst, subtypcst) = - let (_, ctx') = (halve_context (UContext.instance subtypcst)) in ctx' - - let subtyping_susbst (univcst, subtypcst) = - let (ctx, ctx') = (halve_context (UContext.instance subtypcst)) in - Array.fold_left2 (fun subst l1 l2 -> LMap.add l1 l2 subst) LMap.empty ctx ctx' - end -type cumulativity_info = CumulativityInfo.t - module ACumulativityInfo = CumulativityInfo type abstract_cumulativity_info = ACumulativityInfo.t @@ -1315,13 +1286,6 @@ let subst_univs_level_universe subst u = let make_abstract_instance (ctx, _) = Array.mapi (fun i l -> Level.var i) ctx -(** Substitute instance inst for ctx in csts *) -let instantiate_univ_context (ctx, csts) = - (ctx, subst_instance_constraints ctx csts) - -let instantiate_cumulativity_info (ctx, ctx') = - (instantiate_univ_context ctx, instantiate_univ_context ctx') - (** With level to universe substitutions. *) type universe_subst_fn = universe_level -> universe diff --git a/checker/univ.mli b/checker/univ.mli index 01df46fa1e..7f5aa76260 100644 --- a/checker/univ.mli +++ b/checker/univ.mli @@ -18,6 +18,8 @@ sig (** Create a new universe level from a unique identifier and an associated module path. *) + val var : int -> t + val pr : t -> Pp.std_ppcmds (** Pretty-printing *) @@ -179,6 +181,8 @@ sig val length : t -> int (** Compute the length of the instance *) + val of_array : Level.t array -> t + val append : t -> t -> t (** Append two universe instances *) end @@ -208,7 +212,6 @@ module AUContext : sig type t - val instance : t -> Instance.t val size : t -> int val instantiate : Instance.t -> t -> Constraint.t @@ -218,27 +221,6 @@ end type abstract_universe_context = AUContext.t -module CumulativityInfo : -sig - type t - - val make : universe_context * universe_context -> t - - val empty : t - - val univ_context : t -> universe_context - val subtyp_context : t -> universe_context - - val from_universe_context : universe_context -> universe_instance -> t - - val subtyping_other_instance : t -> universe_instance - - val subtyping_susbst : t -> universe_level_subst - -end - -type cumulativity_info = CumulativityInfo.t - module ACumulativityInfo : sig type t @@ -284,10 +266,6 @@ val subst_instance_universe : universe_instance -> universe -> universe (* val make_instance_subst : universe_instance -> universe_level_subst *) (* val make_inverse_instance_subst : universe_instance -> universe_level_subst *) -(** Get the instantiated graph. *) -val instantiate_univ_context : abstract_universe_context -> universe_context -val instantiate_cumulativity_info : abstract_cumulativity_info -> cumulativity_info - (** Build the relative instance corresponding to the context *) val make_abstract_instance : abstract_universe_context -> universe_instance 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/engine/proofview.mli b/engine/proofview.mli index 530204501e..957c9213c4 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -25,7 +25,7 @@ type proofview new nearly identical function everytime. Hence the generic name. *) (* In this version: returns the list of focused goals together with the [evar_map] context. *) -val proofview : proofview -> Goal.goal list * Evd.evar_map +val proofview : proofview -> Evd.evar list * Evd.evar_map (** {6 Starting and querying a proof view} *) @@ -88,7 +88,7 @@ type focus_context new nearly identical function everytime. Hence the generic name. *) (* In this version: the goals in the context, as a "zipper" (the first list is in reversed order). *) -val focus_context : focus_context -> Goal.goal list * Goal.goal list +val focus_context : focus_context -> Evd.evar list * Evd.evar list (** [focus i j] focuses a proofview on the goals from index [i] to index [j] (inclusive, goals are indexed from [1]). I.e. goals @@ -148,7 +148,7 @@ type +'a tactic {!Logic_monad.TacticFailure}*) val apply : Environ.env -> 'a tactic -> proofview -> 'a * proofview - * (bool*Goal.goal list*Goal.goal list) + * (bool*Evd.evar list*Evd.evar list) * Proofview_monad.Info.tree (** {7 Monadic primitives} *) @@ -304,12 +304,12 @@ val shelve : unit tactic (** Shelves the given list of goals, which might include some that are under focus and some that aren't. All the goals are placed on the shelf for later use (or being solved by side-effects). *) -val shelve_goals : Goal.goal list -> unit tactic +val shelve_goals : Evd.evar list -> unit tactic (** [unifiable sigma g l] checks whether [g] appears in another subgoal of [l]. The list [l] may contain [g], but it does not affect the result. Used by [shelve_unifiable]. *) -val unifiable : Evd.evar_map -> Goal.goal -> Goal.goal list -> bool +val unifiable : Evd.evar_map -> Evd.evar -> Evd.evar list -> bool (** Shelves the unifiable goals under focus, i.e. the goals which appear in other goals under focus (the unfocused goals are not @@ -322,15 +322,15 @@ val guard_no_unifiable : Names.Name.t list option tactic (** [unshelve l p] adds all the goals in [l] at the end of the focused goals of p *) -val unshelve : Goal.goal list -> proofview -> proofview +val unshelve : Evd.evar list -> proofview -> proofview (** [depends_on g1 g2 sigma] checks if g1 occurs in the type/ctx of g2 *) -val depends_on : Evd.evar_map -> Goal.goal -> Goal.goal -> bool +val depends_on : Evd.evar_map -> Evd.evar -> Evd.evar -> bool (** [with_shelf tac] executes [tac] and returns its result together with the set of goals shelved by [tac]. The current shelf is unchanged and the returned list contains only unsolved goals. *) -val with_shelf : 'a tactic -> (Goal.goal list * 'a) tactic +val with_shelf : 'a tactic -> (Evd.evar list * 'a) tactic (** If [n] is positive, [cycle n] puts the [n] first goal last. If [n] is negative, then it puts the [n] last goals first.*) @@ -416,14 +416,14 @@ module Unsafe : sig (** [tclNEWGOALS gls] adds the goals [gls] to the ones currently being proved, appending them to the list of focused goals. If a goal is already solved, it is not added. *) - val tclNEWGOALS : Goal.goal list -> unit tactic + val tclNEWGOALS : Evd.evar list -> unit tactic (** [tclSETGOALS gls] sets goals [gls] as the goals being under focus. If a goal is already solved, it is not set. *) - val tclSETGOALS : Goal.goal list -> unit tactic + val tclSETGOALS : Evd.evar list -> unit tactic (** [tclGETGOALS] returns the list of goals under focus. *) - val tclGETGOALS : Goal.goal list tactic + val tclGETGOALS : Evd.evar list tactic (** Sets the evar universe context. *) val tclEVARUNIVCONTEXT : Evd.evar_universe_context -> unit tactic 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" ;; diff --git a/library/declare.ml b/interp/declare.ml index 154793a32d..154793a32d 100644 --- a/library/declare.ml +++ b/interp/declare.ml diff --git a/library/declare.mli b/interp/declare.mli index 6a09434645..6a09434645 100644 --- a/library/declare.mli +++ b/interp/declare.mli diff --git a/library/impargs.ml b/interp/impargs.ml index b7125fc85d..b7125fc85d 100644 --- a/library/impargs.ml +++ b/interp/impargs.ml diff --git a/library/impargs.mli b/interp/impargs.mli index 4b78f54eac..4b78f54eac 100644 --- a/library/impargs.mli +++ b/interp/impargs.mli @@ -153,7 +153,7 @@ let rec pr_com ft s = | None -> () (* pretty printing functions *) -let pp_with ft = +let pp_with ft pp = let cpp_open_box = function | Pp_hbox n -> Format.pp_open_hbox ft () | Pp_vbox n -> Format.pp_open_vbox ft n @@ -175,7 +175,7 @@ let pp_with ft = pp_cmd s; pp_close_tag ft () in - try pp_cmd + try pp_cmd pp with reraise -> let reraise = Backtrace.add_backtrace reraise in let () = Format.pp_print_flush ft () in @@ -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/library/libobject.mli b/library/libobject.mli index 1a21ece2b4..6f935bffea 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -56,6 +56,9 @@ open Mod_subst rebuild the non volatile content of a section from the data collected by the discharge function + Any type defined as a persistent object must be pure (e.g. no references) and + marshallable by the OCaml Marshal module (e.g. no closures). + *) type 'a substitutivity = diff --git a/library/summary.mli b/library/summary.mli index a6ad49950e..d093d95f29 100644 --- a/library/summary.mli +++ b/library/summary.mli @@ -14,6 +14,8 @@ type marshallable = | `No (* Full data will be store in memory, e.g. for Undo *) | `Shallow ] (* Only part of the data will be marshalled to a slave process *) +(** Types of global Coq states. The ['a] type should be pure and marshallable by + the standard OCaml marshalling function. *) type 'a summary_declaration = { (** freeze_function [true] is for marshalling to disk. * e.g. lazy must be forced *) 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/printing/miscprint.ml b/proofs/miscprint.ml index 5d37c8a024..5d37c8a024 100644 --- a/printing/miscprint.ml +++ b/proofs/miscprint.ml diff --git a/printing/miscprint.mli b/proofs/miscprint.mli index 21d410c7b0..21d410c7b0 100644 --- a/printing/miscprint.mli +++ b/proofs/miscprint.mli 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 55df67c6e1..6cc9d3d554 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/vernac/ind_tables.ml b/tactics/ind_tables.ml index 0407c1e36a..0407c1e36a 100644 --- a/vernac/ind_tables.ml +++ b/tactics/ind_tables.ml diff --git a/vernac/ind_tables.mli b/tactics/ind_tables.mli index 005555caa0..005555caa0 100644 --- a/vernac/ind_tables.mli +++ b/tactics/ind_tables.mli 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 *) |