diff options
41 files changed, 373 insertions, 480 deletions
diff --git a/.circleci/config.yml b/.circleci/config.yml index 950674b34..adab42c62 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -11,7 +11,7 @@ defaults: - image: $CI_REGISTRY_IMAGE:$CACHEKEY environment: &envvars - CACHEKEY: "bionic_coq-V2018-07-02-V4" + CACHEKEY: "bionic_coq-V2018-07-11-V2" CI_REGISTRY_IMAGE: registry.gitlab.com/coq/coq version: 2 diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 192a2b181..bbd2d349c 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -8,22 +8,15 @@ ########## CI infrastructure ########## -/dev/ci/ @ejgallego -# Secondary maintainer @SkySkimmer +/dev/ci/ @coq/ci-maintainers +/.circleci/ @coq/ci-maintainers +/.travis.yml @coq/ci-maintainers +/.gitlab-ci.yml @coq/ci-maintainers /dev/ci/user-overlays/*.sh @ghost # Trick to avoid getting review requests # each time someone adds an overlay -/.circleci/ @SkySkimmer -# Secondary maintainer @ejgallego - -/.travis.yml @ejgallego -# Secondary maintainer @SkySkimmer - -/.gitlab-ci.yml @SkySkimmer -# Secondary maintainer @ejgallego - /appveyor.yml @maximedenes /dev/ci/appveyor.* @maximedenes /dev/ci/*.bat @maximedenes diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 7c451af26..be19a93a3 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -9,7 +9,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: "bionic_coq-V2018-07-02-V4" + CACHEKEY: "bionic_coq-V2018-07-11-V2" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" @@ -71,7 +71,7 @@ after_script: - echo 'end:coq.clean' - echo 'start:coq.config' - - ./configure -prefix "$(pwd)/_install_ci" ${COQ_EXTRA_CONF}"$COQ_EXTRA_CONF_QUOTE" + - ./configure -warn-error yes -prefix "$(pwd)/_install_ci" ${COQ_EXTRA_CONF}"$COQ_EXTRA_CONF_QUOTE" - echo 'end:coq.config' - echo 'start:coq.build' @@ -88,28 +88,6 @@ after_script: - set +e -.warnings-template: &warnings-template - # keep warnings in test stage so we can test things even when warnings occur - stage: test - script: - - set -e - - - echo 'start:coq.clean' - - make clean # ensure that `make clean` works on a fresh clone - - echo 'end:coq.clean' - - - echo 'start:coq.config' - - ./configure -local ${COQ_EXTRA_CONF} - - echo 'end:coq.config' - - - echo 'start:coq.build' - - make -j "$NJOBS" coqocaml - - echo 'end:coq:build' - - - set +e - variables: &warnings-variables - COQ_EXTRA_CONF: "-native-compiler yes -coqide byte -byte-only -warn-error yes" - # every non build job must set dependencies otherwise all build # artifacts are used together and we may get some random Coq. To that # purpose, we add a spurious dependency `not-a-real-job` that must be @@ -264,20 +242,6 @@ pkg:nix: paths: - nix-build-coq.drv-0/*/test-suite/logs -warnings:base: - <<: *warnings-template - -# warnings:32bit: -# <<: *warnings-template -# variables: -# <<: *warnings-variables - -warnings:edge: - <<: *warnings-template - variables: - <<: *warnings-variables - OPAM_SWITCH: edge - documentation: <<: *doc-template dependencies: diff --git a/.travis.yml b/.travis.yml index ce178c8a6..53fbe5821 100644 --- a/.travis.yml +++ b/.travis.yml @@ -39,13 +39,14 @@ env: - NJOBS=2 # system is == 4.02.3 - COMPILER="system" - - COMPILER_BE="4.06.1" + - COMPILER_BE="4.07.0" + - DUNE_VER=".1.0.0" - CAMLP5_VER=".6.14" - - CAMLP5_VER_BE=".7.05" + - CAMLP5_VER_BE=".7.06" - FINDLIB_VER=".1.4.1" - FINDLIB_VER_BE=".1.8.0" - - LABLGTK="lablgtk.2.18.3 lablgtk-extras.1.6" - - LABLGTK_BE="lablgtk.2.18.6 lablgtk-extras.1.6" + - LABLGTK="lablgtk.2.18.3 conf-gtksourceview.2" + - LABLGTK_BE="lablgtk.2.18.6 conf-gtksourceview.2" - NATIVE_COMP="yes" - COQ_DEST="-local" - MAIN_TARGET="world" @@ -163,41 +164,12 @@ matrix: - avsm packages: *extra-packages - # Ocaml warnings with two compilers - - if: NOT (type = pull_request) - env: - - MAIN_TARGET="coqocaml" - - EXTRA_CONF="-byte-only -coqide byte -warn-error yes" - - EXTRA_OPAM="${LABLGTK}" - addons: - apt: - sources: - - avsm - packages: &coqide-packages - - opam - - aspcud - - libgtk2.0-dev - - libgtksourceview2.0-dev - - - if: NOT (type = pull_request) + - os: osx env: - - MAIN_TARGET="coqocaml" + - TEST_TARGET="test-suite" - COMPILER="${COMPILER_BE}" - FINDLIB_VER="${FINDLIB_VER_BE}" - CAMLP5_VER="${CAMLP5_VER_BE}" - - EXTRA_CONF="-byte-only -coqide byte -warn-error yes" - - EXTRA_OPAM="${LABLGTK_BE}" - addons: - apt: - sources: - - avsm - packages: *coqide-packages - - - os: osx - env: - - TEST_TARGET="test-suite" - - COMPILER="4.02.3" - - CAMLP5_VER=".6.17" - NATIVE_COMP="no" - COQ_DEST="-local" - EXTRA_OPAM="ounit" @@ -211,12 +183,13 @@ matrix: osx_image: xcode7.3 env: - TEST_TARGET="" - - COMPILER="4.02.3" - - CAMLP5_VER=".6.17" + - COMPILER="${COMPILER_BE}" + - FINDLIB_VER="${FINDLIB_VER_BE}" + - CAMLP5_VER="${CAMLP5_VER_BE}" - NATIVE_COMP="no" - COQ_DEST="-prefix ${PWD}/_install" - EXTRA_CONF="-coqide opt -warn-error yes" - - EXTRA_OPAM="${LABLGTK}" + - EXTRA_OPAM="${LABLGTK_BE}" before_install: - brew update - brew unlink python @@ -246,7 +219,7 @@ install: - opam switch "$COMPILER" && opam update - eval $(opam config env) - opam config list -- opam install -j ${NJOBS} -y num ocamlfind${FINDLIB_VER} jbuilder camlp5${CAMLP5_VER} ${EXTRA_OPAM} +- opam install -j ${NJOBS} -y num ocamlfind${FINDLIB_VER} dune${DUNE_VER} camlp5${CAMLP5_VER} ${EXTRA_OPAM} - opam list script: @@ -257,7 +230,7 @@ script: - echo -en 'travis_fold:end:coq.clean\\r' - echo 'Configuring Coq...' && echo -en 'travis_fold:start:coq.config\\r' -- ./configure ${COQ_DEST} -native-compiler ${NATIVE_COMP} ${EXTRA_CONF} +- ./configure ${COQ_DEST} -warn-error yes -native-compiler ${NATIVE_COMP} ${EXTRA_CONF} - echo -en 'travis_fold:end:coq.config\\r' - echo 'Building Coq...' && echo -en 'travis_fold:start:coq.build\\r' @@ -38,6 +38,8 @@ Tactics without adding new ones. Preexisting tactic `constr_eq_nounivs` can still be used if you really want to ignore universe constraints. +- Tactics and tactic notations now understand the `deprecated` attribute. + Tools - Coq_makefile lets one override or extend the following variables from @@ -29,8 +29,9 @@ WHAT DO YOU NEED ? To compile Coq yourself, you need: - - OCaml version 4.02.3 or later + - OCaml (version >= 4.02.3) (available at https://ocaml.org/) + (This version of Coq has been tested up to OCaml 4.07.0) - The Num package, which used to be part of the OCaml standard library, if you are using an OCaml version >= 4.06.0 @@ -68,7 +69,7 @@ WHAT DO YOU NEED ? profit from Flambda, a special build of the OCaml compiler that has the Flambda optimizer enabled must be installed. For OPAM users, this amounts to installing a compiler switch ending in `+flambda`, - such as `4.06.1+flambda`. For other users, YMMV. Once `ocamlopt + such as `4.07.0+flambda`. For other users, YMMV. Once `ocamlopt -config` reports that Flambda is available, some further optimization options can be used; see the entry about -flambda-opts below for more details. diff --git a/Makefile.build b/Makefile.build index 84f86c99a..c100eda40 100644 --- a/Makefile.build +++ b/Makefile.build @@ -195,7 +195,7 @@ TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) # the output format of the unix command time. For instance: # TIME="%C (%U user, %S sys, %e total, %M maxres)" -COQOPTS=$(NATIVECOMPUTE) +COQOPTS=$(NATIVECOMPUTE) $(COQWARNERROR) BOOTCOQC=$(TIMER) $(COQTOPBEST) -boot $(COQOPTS) -compile LOCALINCLUDES=$(addprefix -I ,$(SRCDIRS)) diff --git a/configure.ml b/configure.ml index 194f47c49..c08e8dfcc 100644 --- a/configure.ml +++ b/configure.ml @@ -647,8 +647,10 @@ let camltag = match caml_version_list with 48: implicit elimination of optional arguments: too common 50: unexpected documentation comment: too common and annoying to avoid 56: unreachable match case: the [_ -> .] syntax doesn't exist in 4.02.3 + 58: "no cmx file was found in path": See https://github.com/ocaml/num/issues/9 + 59: "potential assignment to a non-mutable value": See Coq's issue #8043 *) -let coq_warnings = "-w +a-4-9-27-41-42-44-45-48-50" +let coq_warnings = "-w +a-4-9-27-41-42-44-45-48-50-58-59" let coq_warn_error = if !prefs.warn_error then "-warn-error +a" @@ -1337,6 +1339,7 @@ let write_makefile f = pr "WITHDOC=%s\n\n" (if !prefs.withdoc then "all" else "no"); pr "# Option to produce precompiled files for native_compute\n"; pr "NATIVECOMPUTE=%s\n" (if !prefs.nativecompiler then "-native-compiler" else ""); + pr "COQWARNERROR=%s\n" (if !prefs.warn_error then "-w +default" else ""); close_out o; Unix.chmod f 0o444 diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 94e90bf4f..da5ac2b15 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -793,7 +793,7 @@ function make_ln { function make_ocaml { get_flex_dll_link_bin - if build_prep http://caml.inria.fr/pub/distrib/ocaml-4.06 ocaml-4.06.1 tar.gz 1 ; then + if build_prep http://caml.inria.fr/pub/distrib/ocaml-4.07 ocaml-4.07.0 tar.gz 1 ; then # See README.win32.adoc cp config/m-nt.h byterun/caml/m.h cp config/s-nt.h byterun/caml/s.h @@ -933,7 +933,7 @@ function make_camlp5 { make_ocaml make_findlib - if build_prep https://github.com/camlp5/camlp5/archive rel705 tar.gz 1 camlp5-rel705; then + if build_prep https://github.com/camlp5/camlp5/archive rel706 tar.gz 1 camlp5-rel706; then logn configure ./configure # Somehow my virus scanner has the boot.new/SAVED directory locked after the move for a second => repeat until success sed -i 's/mv boot.new boot/until mv boot.new boot; do sleep 1; done/' Makefile diff --git a/dev/ci/appveyor.sh b/dev/ci/appveyor.sh index 7bf9ad8c9..d2176e326 100644 --- a/dev/ci/appveyor.sh +++ b/dev/ci/appveyor.sh @@ -2,7 +2,7 @@ set -e -x -APPVEYOR_OPAM_SWITCH=4.06.1+mingw64c +APPVEYOR_OPAM_SWITCH=4.07.0+mingw64c wget https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.1/opam64.tar.xz tar -xf opam64.tar.xz diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index a4ee6a379..1361392dc 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2018-07-02-V4" +# CACHEKEY: "bionic_coq-V2018-07-11-V2" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -28,7 +28,7 @@ RUN opam init -a -y -j $NJOBS --compiler="$COMPILER" default https://opam.ocaml. # Common OPAM packages. # `num` does not have a version number as the right version to install varies # with the compiler version. -ENV BASE_OPAM="num ocamlfind.1.8.0 jbuilder.1.0+beta20 ounit.2.0.8" \ +ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.0.0 ounit.2.0.8" \ CI_OPAM="menhir.20180530 elpi.1.0.4 ocamlgraph.1.8.8" # BASE switch; CI_OPAM contains Coq's CI dependencies. @@ -43,8 +43,8 @@ RUN opam switch -y -j $NJOBS "${COMPILER}+32bit" && eval $(opam config env) && \ opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER # EDGE switch -ENV COMPILER_EDGE="4.06.1" \ - CAMLP5_VER_EDGE="7.05" \ +ENV COMPILER_EDGE="4.07.0" \ + CAMLP5_VER_EDGE="7.06" \ COQIDE_OPAM_EDGE="lablgtk.2.18.6 conf-gtksourceview.2" RUN opam switch -y -j $NJOBS $COMPILER_EDGE && eval $(opam config env) && \ diff --git a/dev/ci/user-overlays/07746-cleanup-unused-various.sh b/dev/ci/user-overlays/07746-cleanup-unused-various.sh deleted file mode 100644 index 8688b0d53..000000000 --- a/dev/ci/user-overlays/07746-cleanup-unused-various.sh +++ /dev/null @@ -1,6 +0,0 @@ -#!/bin/sh - -if [ "$CI_PULL_REQUEST" = "7746" ] || [ "$CI_BRANCH" = "cleanup-unused-various" ]; then - Equations_CI_BRANCH="adapt-unused" - Equations_CI_GITURL="https://github.com/SkySkimmer/Coq-Equations.git" -fi diff --git a/dev/ci/user-overlays/07820-mattam82-hints-constants.sh b/dev/ci/user-overlays/07820-mattam82-hints-constants.sh deleted file mode 100644 index 2ae86ae22..000000000 --- a/dev/ci/user-overlays/07820-mattam82-hints-constants.sh +++ /dev/null @@ -1,6 +0,0 @@ -_OVERLAY_BRANCH=hints-variables-overlay - -if [ "$CI_PULL_REQUEST" = "7820" ] || [ "$CI_BRANCH" = "_OVERLAY_BRANCH" ]; then - - Equations_CI_BRANCH="$_OVERLAY_BRANCH" -fi diff --git a/dev/ci/user-overlays/07898-ppedrot-rm-campl4-remains.sh b/dev/ci/user-overlays/07898-ppedrot-rm-campl4-remains.sh deleted file mode 100644 index 9c4c905fa..000000000 --- a/dev/ci/user-overlays/07898-ppedrot-rm-campl4-remains.sh +++ /dev/null @@ -1,8 +0,0 @@ -_OVERLAY_BRANCH=rm-campl4-remains - -if [ "$CI_PULL_REQUEST" = "7898" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then - - pidetop_CI_BRANCH="$_OVERLAY_BRANCH" - pidetop_CI_GITURL=https://github.com/ppedrot/pidetop - -fi diff --git a/dev/ci/user-overlays/07902-ppedrot-camlp5-parser.sh b/dev/ci/user-overlays/07902-ppedrot-camlp5-parser.sh deleted file mode 100644 index 735153ebd..000000000 --- a/dev/ci/user-overlays/07902-ppedrot-camlp5-parser.sh +++ /dev/null @@ -1,8 +0,0 @@ -_OVERLAY_BRANCH=camlp5-parser - -if [ "$CI_PULL_REQUEST" = "7902" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then - - ltac2_CI_BRANCH="$_OVERLAY_BRANCH" - ltac2_CI_GITURL=https://github.com/ppedrot/ltac2 - -fi diff --git a/dev/doc/README.md b/dev/doc/README.md index 1a4e40f68..223cf6286 100644 --- a/dev/doc/README.md +++ b/dev/doc/README.md @@ -7,7 +7,7 @@ Assuming one is running Ubuntu (if not, replace `apt` with the package manager o ``` $ sudo apt-get install make opam git -# At the time of writing, <latest-ocaml-version> is 4.06.1. +# At the time of writing, <latest-ocaml-version> is 4.07.0. # The latest version number is available at: https://ocaml.org/releases/ $ opam init --comp <latest-ocaml-version> diff --git a/dev/tools/check-overlays.sh b/dev/tools/check-overlays.sh index f7e05b51c..33a9ff058 100755 --- a/dev/tools/check-overlays.sh +++ b/dev/tools/check-overlays.sh @@ -1,8 +1,8 @@ #!/usr/bin/env bash -for f in dev/ci/user-overlays/* +for f in $(git ls-files "dev/ci/user-overlays/") do - if ! ([[ $f = dev/ci/user-overlays/README.md ]] || [[ $f == *.sh ]]) + if ! ([[ "$f" = dev/ci/user-overlays/README.md ]] || [[ "$f" == *.sh ]]) then >&2 echo "Bad overlay '$f'." >&2 echo "User overlays need to have extension .sh to be picked up!" diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits.rst index 5d9324a65..2988b194e 100644 --- a/doc/sphinx/credits.rst +++ b/doc/sphinx/credits.rst @@ -40,7 +40,7 @@ foundation of mathematics on constructive principles. The second one, Girard’s polymorphic :math:`\lambda`-calculus :math:`F_\omega`, is a very strong functional system in which we may represent higher-order logic proof structures. Combining both systems in a higher-order -extension of the Automath languages, T. Coquand presented in 1985 the +extension of the Automath language, T. Coquand presented in 1985 the first version of the *Calculus of Constructions*, CoC. This strong logical system allowed powerful axiomatizations, but direct inductive definitions were not possible, and inductive notions had to be defined @@ -246,14 +246,14 @@ pretty-printing rules has also changed. Eduardo Giménez redesigned the internal tactic libraries, giving uniform names to Caml functions corresponding to |Coq| tactic names. -Bruno Barras wrote new more efficient reductions functions. +Bruno Barras wrote new, more efficient reduction functions. Hugo Herbelin introduced more uniform notations in the |Coq| specification language: the definitions by fixpoints and pattern-matching have a more readable syntax. Patrick Loiseleur introduced user-friendly notations for arithmetic expressions. -New tactics were introduced: Eduardo Giménez improved a mechanism to +New tactics were introduced: Eduardo Giménez improved the mechanism to introduce macros for tactics, and designed special tactics for (co)inductive definitions; Patrick Loiseleur designed a tactic to simplify polynomial expressions in an arbitrary commutative ring which @@ -279,12 +279,12 @@ Loiseleur. Credits: addendum for version 6.3 ================================= -The main changes in version V6.3 was the introduction of a few new +The main changes in version V6.3 were the introduction of a few new tactics and the extension of the guard condition for fixpoint definitions. B. Barras extended the unification algorithm to complete partial terms -and solved various tricky bugs related to universes. +and fixed various tricky bugs related to universes. D. Delahaye developed the ``AutoRewrite`` tactic. He also designed the new behavior of ``Intro`` and provided the tacticals ``First`` and @@ -318,8 +318,8 @@ internal architecture of the system. The |Coq| version 7.0 was distributed in March 2001, version 7.1 in September 2001, version 7.2 in January 2002, version 7.3 in May 2002 and version 7.4 in February 2003. -Jean-Christophe Filliâtre designed the architecture of the new system, -he introduced a new representation for environments and wrote a new +Jean-Christophe Filliâtre designed the architecture of the new system. +He introduced a new representation for environments and wrote a new kernel for type-checking terms. His approach was to use functional data-structures in order to get more sharing, to prepare the addition of modules and also to get closer to a certified kernel. @@ -351,7 +351,7 @@ Letouzey adapted user contributions to extract ML programs when it was sensible. Jean-Christophe Filliâtre wrote ``coqdoc``, a documentation tool for |Coq| libraries usable from version 7.2. -Bruno Barras improved the reduction algorithms efficiency and the +Bruno Barras improved the efficiency of the reduction algorithm and the confidence level in the correctness of |Coq| critical type-checking algorithm. @@ -368,8 +368,8 @@ propositional inductive types. Loïc Pottier developed Fourier, a tactic solving linear inequalities on real numbers. -Pierre Crégut developed a new version based on reflexion of the Omega -decision tactic. +Pierre Crégut developed a new, reflection-based version of the Omega +decision procedure. Claudio Sacerdoti Coen designed an XML output for the |Coq| modules to be used in the Hypertextual Electronic Library of Mathematics (HELM cf @@ -419,7 +419,7 @@ main motivations were with a functional programming perfume (e.g. abstraction is now written fun), and more directly accessible to the novice (e.g. dependent product is now written forall and allows omission of - types). Also, parentheses and are no longer mandatory for function + types). Also, parentheses are no longer mandatory for function application. - extensibility: some standard notations (e.g. “<” and “>”) were @@ -438,8 +438,8 @@ language and of the language of commands has been carried out. The purpose here is a better uniformity making the tactics and commands easier to use and to remember. -Thirdly, a restructuration and uniformisation of the standard library of -Coq has been performed. There is now just one Leibniz’ equality usable +Thirdly, a restructuring and uniformization of the standard library of +Coq has been performed. There is now just one Leibniz equality usable for all the different kinds of |Coq| objects. Also, the set of real numbers now lies at the same level as the sets of natural and integer numbers. Finally, the names of the standard properties of numbers now @@ -447,7 +447,7 @@ follow a standard pattern and the symbolic notations for the standard definitions as well. The fourth point is the release of |CoqIDE|, a new graphical gtk2-based -interface fully integrated to |Coq|. Close in style from the Proof General +interface fully integrated with |Coq|. Close in style to the Proof General Emacs interface, it is faster and its integration with |Coq| makes interactive developments more friendly. All mathematical Unicode symbols are usable within |CoqIDE|. @@ -461,18 +461,17 @@ improved tactics (including a new tactic for solving first-order statements), new management commands, extended libraries. Bruno Barras and Hugo Herbelin have been the main contributors of the -reflexion and the implementation of the new syntax. The smart automatic +reflection and the implementation of the new syntax. The smart automatic translator from old to new syntax released with |Coq| is also their work with contributions by Olivier Desmettre. -Hugo Herbelin is the main designer and implementor of the notion of +Hugo Herbelin is the main designer and implementer of the notion of interpretation scopes and of the commands for easily adding new notations. -Hugo Herbelin is the main implementor of the restructuration of the -standard library. +Hugo Herbelin is the main implementer of the restructured standard library. -Pierre Corbineau is the main designer and implementor of the new tactic +Pierre Corbineau is the main designer and implementer of the new tactic for solving first-order statements in presence of inductive types. He is also the maintainer of the non-domain specific automation tactics. @@ -487,14 +486,14 @@ Pierre Letouzey and Jacek Chrząszcz respectively maintained the extraction tool and module system of |Coq|. Jean-Christophe Filliâtre, Pierre Letouzey, Hugo Herbelin and other -contributors from Sophia-Antipolis and Nijmegen participated to the -extension of the library. +contributors from Sophia-Antipolis and Nijmegen participated in +extending the library. Julien Narboux built a NSIS-based automatic |Coq| installation tool for the Windows platform. Hugo Herbelin and Christine Paulin coordinated the development which was -under the responsability of Christine Paulin. +under the responsibility of Christine Paulin. | Palaiseau & Orsay, Apr. 2004 | Hugo Herbelin & Christine Paulin @@ -525,12 +524,12 @@ arbitrary transition systems. Claudio Sacerdoti Coen added new features to the module system. -Benjamin Grégoire, Assia Mahboubi and Bruno Barras developed a new more -efficient and more general simplification algorithm on rings and +Benjamin Grégoire, Assia Mahboubi and Bruno Barras developed a new, more +efficient and more general simplification algorithm for rings and semi-rings. -Laurent Théry and Bruno Barras developed a new significantly more -efficient simplification algorithm on fields. +Laurent Théry and Bruno Barras developed a new, significantly more +efficient simplification algorithm for fields. Hugo Herbelin, Pierre Letouzey, Julien Forest, Julien Narboux and Claudio Sacerdoti Coen added new tactic features. @@ -554,7 +553,7 @@ Jean-Christophe Filliâtre’s contribution on finite maps have been integrated to the |Coq| standard library. Pierre Letouzey developed a library about finite sets “à la Objective Caml”. With Jean-Marc Notin, he extended the library on lists. Pierre Letouzey’s contribution on -rational numbers has been integrated and extended.. +rational numbers has been integrated and extended. Pierre Corbineau extended his tactic for solving first-order statements. He wrote a reflection-based intuitionistic tautology solver. @@ -589,8 +588,8 @@ various aspects. Regarding the language of |Coq|, the main novelty is the introduction by Matthieu Sozeau of a package of commands providing Haskell-style type classes. Type classes, that come with a few convenient features such as -type-based resolution of implicit arguments, plays a new role of -landmark in the architecture of |Coq| with respect to automatization. For +type-based resolution of implicit arguments, play a new landmark role +in the architecture of |Coq| with respect to automation. For instance, thanks to type classes support, Matthieu Sozeau could implement a new resolution-based version of the tactics dedicated to rewriting on arbitrary transitive relations. @@ -599,13 +598,13 @@ Another major improvement of |Coq| 8.2 is the evolution of the arithmetic libraries and of the tools associated to them. Benjamin Grégoire and Laurent Théry contributed a modular library for building arbitrarily large integers from bounded integers while Evgeny Makarov contributed a -modular library of abstract natural and integer arithmetics together +modular library of abstract natural and integer arithmetic together with a few convenient tactics. On his side, Pierre Letouzey made numerous extensions to the arithmetic libraries on :math:`\mathbb{Z}` -and :math:`\mathbb{Q}`, including extra support for automatization in +and :math:`\mathbb{Q}`, including extra support for automation in presence of various number-theory concepts. -Frédéric Besson contributed a reflexive tactic based on Krivine-Stengle +Frédéric Besson contributed a reflective tactic based on Krivine-Stengle Positivstellensatz (the easy way) for validating provability of systems of inequalities. The platform is flexible enough to support the validation of any algorithm able to produce a “certificate” for the @@ -620,10 +619,10 @@ relying on Benjamin Grégoire and Laurent Théry’s library, delivered a library of unbounded integers in base :math:`2^{31}`. As importantly, he developed a notion of “retro-knowledge” so as to safely extend the kernel-located bytecode-based efficient evaluation algorithm of |Coq| -version 8.1 to use 31-bits machine arithmetics for efficiently computing +version 8.1 to use 31-bits machine arithmetic for efficiently computing with the library of integers he developed. -Beside the libraries, various improvements contributed to provide a more +Beside the libraries, various improvements were contributed to provide a more comfortable end-user language and more expressive tactic language. Hugo Herbelin and Matthieu Sozeau improved the pattern-matching compilation algorithm (detection of impossible clauses in pattern-matching, @@ -632,7 +631,7 @@ and Matthieu Sozeau contributed various new convenient syntactic constructs and new tactics or tactic features: more inference of redundant information, better unification, better support for proof or definition by fixpoint, more expressive rewriting tactics, better -support for meta-variables, more convenient notations, ... +support for meta-variables, more convenient notations... Élie Soubiran improved the module system, adding new features (such as an “include” command) and making it more flexible and more general. He @@ -641,7 +640,7 @@ mechanism. Matthieu Sozeau extended the Russell language, ending in an convenient way to write programs of given specifications, Pierre Corbineau extended -the Mathematical Proof Language and the automatization tools that +the Mathematical Proof Language and the automation tools that accompany it, Pierre Letouzey supervised and extended various parts of the standard library, Stéphane Glondu contributed a few tactics and improvements, Jean-Marc Notin provided help in debugging, general @@ -662,7 +661,7 @@ adaptation of the interface of the old “setoid rewrite” tactic to the new version. Lionel Mamane worked on the interaction between |Coq| and its external interfaces. With Samuel Mimram, he also helped making |Coq| compatible with recent software tools. Russell O’Connor, Cezary -Kaliscyk, Milad Niqui contributed to improve the libraries of integers, +Kaliszyk, Milad Niqui contributed to improve the libraries of integers, rational, and real numbers. We also thank many users and partners for suggestions and feedback, in particular Pierre Castéran and Arthur Charguéraud, the INRIA Marelle team, Georges Gonthier and the @@ -704,8 +703,8 @@ The module system evolved significantly. Besides the resolution of some efficiency issues and a more flexible construction of module types, Élie Soubiran brought a new model of name equivalence, the :math:`\Delta`-equivalence, which respects as much as possible the names -given by the users. He also designed with Pierre Letouzey a new -convenient operator ``<+`` for nesting functor application, that +given by the users. He also designed with Pierre Letouzey a new, +convenient operator ``<+`` for nesting functor application that provides a light notation for inheriting the properties of cascading modules. @@ -719,7 +718,7 @@ the extraction mechanism. Bruno Barras and Élie Soubiran maintained the Coq checker, Julien Forest maintained the Function mechanism for reasoning over recursively defined functions. Matthieu Sozeau, Hugo Herbelin and Jean-Marc Notin maintained coqdoc. Frédéric Besson -maintained the Micromega plateform for deciding systems of inequalities. +maintained the Micromega platform for deciding systems of inequalities. Pierre Courtieu maintained the support for the Proof General Emacs interface. Claude Marché maintained the plugin for calling external provers (dp). Yves Bertot made some improvements to the libraries of @@ -736,7 +735,7 @@ support for benchmarking and archiving. Many users helped by reporting problems, providing patches, suggesting improvements or making useful comments, either on the bug tracker or on -the Coq-club mailing list. This includes but not exhaustively Cédric +the Coq-Club mailing list. This includes but not exhaustively Cédric Auger, Arthur Charguéraud, François Garillot, Georges Gonthier, Robin Green, Stéphane Lescuyer, Eelis van der Weegen, ... @@ -772,8 +771,8 @@ structured scripts (bullets and proof brackets) but, even if yet not user-available, the new engine also provides the basis for refining existential variables using tactics, for applying tactics to several goals simultaneously, for reordering goals, all features which are -planned for the next release. The new proof engine forced to reimplement -info and Show Script differently, what was done by Pierre Letouzey. +planned for the next release. The new proof engine forced Pierre Letouzey +to reimplement info and Show Script differently. Before version 8.4, |CoqIDE| was linked to |Coq| with the graphical interface living in a separate thread. From version 8.4, |CoqIDE| is a @@ -784,7 +783,7 @@ sessions in parallel. Relying on the infrastructure work made by Vincent Gross, Pierre Letouzey, Pierre Boutillier and Pierre-Marie Pédrot contributed many various refinements of |CoqIDE|. -Coq 8.4 also comes with a bunch of many various smaller-scale changes +Coq 8.4 also comes with a bunch of various smaller-scale changes and improvements regarding the different components of the system. The underlying logic has been extended with :math:`\eta`-conversion @@ -831,7 +830,7 @@ Pierre Letouzey added a tactic timeout and the interruptibility of vm\_compute. Bug fixes and miscellaneous improvements of the tactic language came from Hugo Herbelin, Pierre Letouzey and Matthieu Sozeau. -Regarding decision tactics, Loïc Pottier maintained Nsatz, moving in +Regarding decision tactics, Loïc Pottier maintained nsatz, moving in particular to a type-class based reification of goals while Frédéric Besson maintained Micromega, adding in particular support for division. @@ -894,7 +893,7 @@ Boutillier (MacOS), Stéphane Glondu (Debian). Releasing, testing and benchmarking support was provided by Jean-Marc Notin. Many suggestions for improvements were motivated by feedback from users, -on either the bug tracker or the coq-club mailing list. Special thanks +on either the bug tracker or the Coq-Club mailing list. Special thanks are going to the users who contributed patches, starting with Tom Prince. Other patch contributors include Cédric Auger, David Baelde, Dan Grayson, Paolo Herms, Robbert Krebbers, Marc Lasson, Hendrik Tews and @@ -1036,7 +1035,7 @@ X). Maxime Dénès improved significantly the testing and benchmarking support. Many power users helped to improve the design of the new features via -the bug tracker, the coq development mailing list or the coq-club +the bug tracker, the coq development mailing list or the Coq-Club mailing list. Special thanks are going to the users who contributed patches and intensive brain-storming, starting with Jason Gross, Jonathan Leivent, Greg Malecha, Clément Pit-Claudel, Marc Lasson, Lionel @@ -1154,13 +1153,13 @@ Gregory Malecha, and Matthieu Sozeau. Matej Košík maintained and greatly improved the continuous integration setup and the testing of |Coq| contributions. He also contributed many API -improvement and code cleanups throughout the system. +improvements and code cleanups throughout the system. The contributors for this version are Bruno Barras, C.J. Bell, Yves Bertot, Frédéric Besson, Pierre Boutillier, Tej Chajed, Guillaume Claret, Xavier Clerc, Pierre Corbineau, Pierre Courtieu, Maxime Dénès, Ricky Elrod, Emilio Jesús Gallego Arias, Jason Gross, Hugo Herbelin, -Sébastien Hinderer, Jacques-Henri Jourdan, Matej Kosik, Xavier Leroy, +Sébastien Hinderer, Jacques-Henri Jourdan, Matej Košík, Xavier Leroy, Pierre Letouzey, Gregory Malecha, Cyprien Mangin, Erik Martin-Dorel, Guillaume Melquiond, Clément Pit–Claudel, Pierre-Marie Pédrot, Daniel de Rauglaudre, Lionel Rieg, Gabriel Scherer, Thomas Sibut-Pinote, Matthieu @@ -1171,7 +1170,7 @@ Dénès, who was also in charge of the release process. Many power users helped to improve the design of the new features via the bug tracker, the pull request system, the |Coq| development mailing -list or the coq-club mailing list. Special thanks to the users who +list or the Coq-Club mailing list. Special thanks to the users who contributed patches and intensive brain-storming and code reviews, starting with Cyril Cohen, Jason Gross, Robbert Krebbers, Jonathan Leivent, Xavier Leroy, Gregory Malecha, Clément Pit–Claudel, Gabriel @@ -1279,7 +1278,7 @@ the maintainer of this release. Many power users helped to improve the design of the new features via the bug tracker, the pull request system, the |Coq| development mailing list or the -coq-club mailing list. Special thanks to the users who contributed patches and +Coq-Club mailing list. Special thanks to the users who contributed patches and intensive brain-storming and code reviews, starting with Jason Gross, Ralf Jung, Robbert Krebbers, Xavier Leroy, Clément Pit–Claudel and Gabriel Scherer. It would however be impossible to mention exhaustively the names of everybody who diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst index c7bc69db4..1a610396e 100644 --- a/doc/sphinx/introduction.rst +++ b/doc/sphinx/introduction.rst @@ -12,7 +12,7 @@ https://github.com/coq/coq/wiki#coq-tutorials). The |Coq| system is designed to develop mathematical proofs, and especially to write formal specifications, programs and to verify that -programs are correct with respect to their specification. It provides a +programs are correct with respect to their specifications. It provides a specification language named |Gallina|. Terms of |Gallina| can represent programs as well as properties of these programs and proofs of these properties. Using the so-called *Curry-Howard isomorphism*, programs, @@ -52,7 +52,7 @@ are processed from a file. How to read this book ===================== -This is a Reference Manual, so it is not made for a continuous reading. +This is a Reference Manual, so it is not intended for continuous reading. We recommend using the various indexes to quickly locate the documentation you are looking for. There is a global index, and a number of specific indexes for tactics, vernacular commands, and error messages and warnings. diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index ac6a20198..8250b4b3d 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -1430,6 +1430,12 @@ the following attributes names are recognized: Takes as value the optional attributes ``since`` and ``note``; both have a string value. + This attribute can trigger the following warnings: + + .. warn:: Tactic @qualid is deprecated since @string. @string. + + .. warn:: Tactic Notation @qualid is deprecated since @string. @string. + Here are a few examples: .. coqtop:: all reset @@ -1440,7 +1446,7 @@ Here are a few examples: exact O. Defined. - #[deprecated(since="8.9.0", note="use idtac instead")] + #[deprecated(since="8.9.0", note="Use idtac instead.")] Ltac foo := idtac. Goal True. diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp index cea0bed59..02da61ef7 100644 --- a/grammar/tacextend.mlp +++ b/grammar/tacextend.mlp @@ -49,13 +49,17 @@ EXTEND GLOBAL: str_item; str_item: [ [ "TACTIC"; "EXTEND"; s = tac_name; + depr = OPT [ "DEPRECATED"; depr = LIDENT -> depr ]; level = OPT [ "AT"; UIDENT "LEVEL"; level = INT -> level ]; OPT "|"; l = LIST1 tacrule SEP "|"; "END" -> let level = match level with Some i -> int_of_string i | None -> 0 in let level = mlexpr_of_int level in + let depr = mlexpr_of_option (fun l -> <:expr< $lid:l$ >>) depr in let l = <:expr< Tacentries.($mlexpr_of_list (fun x -> x) l$) >> in - declare_str_items loc [ <:str_item< Tacentries.tactic_extend $plugin_name$ $str:s$ ~{ level = $level$ } $l$ >> ] ] ] + declare_str_items loc [ <:str_item< Tacentries.tactic_extend + $plugin_name$ $str:s$ ~{ level = $level$ } ?{ deprecation = + $depr$ } $l$ >> ] ] ] ; tacrule: [ [ "["; l = LIST1 tacargs; "]"; diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 39f7de942..ec6c5b297 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -278,7 +278,6 @@ type primitive = | Mk_rel of int | Mk_var of Id.t | Mk_proj - | Is_accu | Is_int | Cast_accu | Upd_cofix @@ -319,7 +318,6 @@ let eq_primitive p1 p2 = | Mk_cofix i1, Mk_cofix i2 -> Int.equal i1 i2 | Mk_rel i1, Mk_rel i2 -> Int.equal i1 i2 | Mk_var id1, Mk_var id2 -> Id.equal id1 id2 - | Is_accu, Is_accu -> true | Cast_accu, Cast_accu -> true | Upd_cofix, Upd_cofix -> true | Force_cofix, Force_cofix -> true @@ -345,7 +343,6 @@ let primitive_hash = function combinesmall 8 (Int.hash i) | Mk_var id -> combinesmall 9 (Id.hash id) - | Is_accu -> 10 | Is_int -> 11 | Cast_accu -> 12 | Upd_cofix -> 13 @@ -396,6 +393,7 @@ type mllambda = | MLsetref of string * mllambda | MLsequence of mllambda * mllambda | MLarray of mllambda array + | MLisaccu of string * inductive * mllambda and mllam_branches = ((constructor * lname option array) list * mllambda) array @@ -467,7 +465,12 @@ let rec eq_mllambda gn1 gn2 n env1 env2 t1 t2 = | MLarray arr1, MLarray arr2 -> Array.equal (eq_mllambda gn1 gn2 n env1 env2) arr1 arr2 - | _, _ -> false + | MLisaccu (s1, ind1, ml1), MLisaccu (s2, ind2, ml2) -> + String.equal s1 s2 && eq_ind ind1 ind2 && + eq_mllambda gn1 gn2 n env1 env2 ml1 ml2 + | (MLlocal _ | MLglobal _ | MLprimitive _ | MLlam _ | MLletrec _ | MLlet _ | + MLapp _ | MLif _ | MLmatch _ | MLconstruct _ | MLint _ | MLuint _ | + MLsetref _ | MLsequence _ | MLarray _ | MLisaccu _), _ -> false and eq_letrec gn1 gn2 n env1 env2 defs1 defs2 = let eq_def (_,args1,ml1) (_,args2,ml2) = @@ -542,6 +545,8 @@ let rec hash_mllambda gn n env t = combinesmall 14 (combine hml hml') | MLarray arr -> combinesmall 15 (hash_mllambda_array gn n env 1 arr) + | MLisaccu (s, ind, c) -> + combinesmall 16 (combine (String.hash s) (combine (ind_hash ind) (hash_mllambda gn n env c))) and hash_mllambda_letrec gn n env init defs = let hash_def (_,args,ml) = @@ -608,6 +613,7 @@ let fv_lam l = | MLsetref(_,l) -> aux l bind fv | MLsequence(l1,l2) -> aux l1 bind (aux l2 bind fv) | MLarray arr -> Array.fold_right (fun a fv -> aux a bind fv) arr fv + | MLisaccu (_, _, body) -> aux body bind fv in aux l LNset.empty LNset.empty @@ -1142,7 +1148,7 @@ let ml_of_instance instance u = mkMLapp (MLapp (MLglobal cn, fv_args env fvn fvr)) [|force|] | Lif(t,bt,bf) -> MLif(ml_of_lam env l t, ml_of_lam env l bt, ml_of_lam env l bf) - | Lfix ((rec_pos,start), (ids, tt, tb)) -> + | Lfix ((rec_pos, inds, start), (ids, tt, tb)) -> (* let type_f fvt = [| type fix |] let norm_f1 fv f1 .. fn params1 = body1 .. @@ -1211,8 +1217,9 @@ let ml_of_instance instance u = let paramsi = t_params.(i) in let reci = MLlocal (paramsi.(rec_pos.(i))) in let pargsi = Array.map (fun id -> MLlocal id) paramsi in + let (prefix, ind) = inds.(i) in let body = - MLif(MLapp(MLprimitive Is_accu,[|reci|]), + MLif(MLisaccu (prefix, ind, reci), mkMLapp (MLapp(MLprimitive (Mk_fix(rec_pos,i)), [|mk_type; mk_norm|])) @@ -1374,6 +1381,7 @@ let subst s l = | MLsetref(s,l1) -> MLsetref(s,aux l1) | MLsequence(l1,l2) -> MLsequence(aux l1, aux l2) | MLarray arr -> MLarray (Array.map aux arr) + | MLisaccu (s, ind, l) -> MLisaccu (s, ind, aux l) in aux l @@ -1471,7 +1479,7 @@ let optimize gdef l = let b1 = optimize s b1 in let b2 = optimize s b2 in begin match t, b2 with - | MLapp(MLprimitive Is_accu,[| l1 |]), MLmatch(annot, l2, _, bs) + | MLisaccu (_, _, l1), MLmatch(annot, l2, _, bs) when eq_mllambda l1 l2 -> MLmatch(annot, l1, b1, bs) | _, _ -> MLif(t, b1, b2) end @@ -1483,6 +1491,7 @@ let optimize gdef l = | MLsetref(r,l) -> MLsetref(r, optimize s l) | MLsequence(l1,l2) -> MLsequence(optimize s l1, optimize s l2) | MLarray arr -> MLarray (Array.map (optimize s) arr) + | MLisaccu (pf, ind, l) -> MLisaccu (pf, ind, optimize s l) in optimize LNmap.empty l @@ -1645,7 +1654,11 @@ let pp_mllam fmt l = pp_mllam fmt arr.(len-1) end; Format.fprintf fmt "|]@]" - + | MLisaccu (prefix, (mind, i), c) -> + let accu = Format.sprintf "%sAccu_%s_%i" prefix (string_of_mind mind) i in + Format.fprintf fmt + "@[begin match Obj.magic (%a) with@\n| %s _ ->@\n true@\n| _ ->@\n false@\nend@]" + pp_mllam c accu and pp_letrec fmt defs = let len = Array.length defs in @@ -1738,7 +1751,6 @@ let pp_mllam fmt l = | Mk_var id -> Format.fprintf fmt "mk_var_accu (Names.id_of_string \"%s\")" (string_of_id id) | Mk_proj -> Format.fprintf fmt "mk_proj_accu" - | Is_accu -> Format.fprintf fmt "is_accu" | Is_int -> Format.fprintf fmt "is_int" | Cast_accu -> Format.fprintf fmt "cast_accu" | Upd_cofix -> Format.fprintf fmt "upd_cofix" @@ -1884,7 +1896,7 @@ let compile_constant env sigma prefix ~interactive con cb = let t = Mod_subst.force_constr t in let code = lambda_of_constr env sigma t in if !Flags.debug then Feedback.msg_debug (Pp.str "Generated lambda code"); - let is_lazy = is_lazy prefix t in + let is_lazy = is_lazy env prefix t in let code = if is_lazy then mk_lazy code else code in let name = if interactive then LinkedInteractive prefix diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli index eaad8ee0c..5075bd3d1 100644 --- a/kernel/nativeinstr.mli +++ b/kernel/nativeinstr.mli @@ -36,7 +36,7 @@ and lambda = | Lcase of annot_sw * lambda * lambda * lam_branches (* annotations, term being matched, accu, branches *) | Lif of lambda * lambda * lambda - | Lfix of (int array * int) * fix_decl + | Lfix of (int array * (string * inductive) array * int) * fix_decl | Lcofix of int * fix_decl (* must be in eta-expanded form *) | Lmakeblock of prefix * pconstructor * int * lambda array (* prefix, constructor name, constructor tag, arguments *) diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 5843cd543..a5cdd0a19 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -333,54 +333,13 @@ let rec get_alias env (kn, u as p) = (*i Global environment *) -let global_env = ref empty_env - -let set_global_env env = global_env := env - let get_names decl = let decl = Array.of_list decl in Array.map fst decl -(* Rel Environment *) -module Vect = - struct - type 'a t = { - mutable elems : 'a array; - mutable size : int; - } - - let make n a = { - elems = Array.make n a; - size = 0; - } - - let extend v = - if Int.equal v.size (Array.length v.elems) then - let new_size = min (2*v.size) Sys.max_array_length in - if new_size <= v.size then invalid_arg "Vect.extend"; - let new_elems = Array.make new_size v.elems.(0) in - Array.blit v.elems 0 new_elems 0 (v.size); - v.elems <- new_elems - - let push v a = - extend v; - v.elems.(v.size) <- a; - v.size <- v.size + 1 - - let popn v n = - v.size <- max 0 (v.size - n) - - let pop v = popn v 1 - - let get_last v n = - if v.size <= n then invalid_arg "Vect.get:index out of bounds"; - v.elems.(v.size - n - 1) - - end - let empty_args = [||] -module Renv = +module Cache = struct module ConstrHash = @@ -394,45 +353,20 @@ module Renv = type constructor_info = tag * int * int (* nparam nrealargs *) - type t = { - name_rel : Name.t Vect.t; - construct_tbl : constructor_info ConstrTable.t; - - } - - - let make () = { - name_rel = Vect.make 16 Anonymous; - construct_tbl = ConstrTable.create 111 - } - - let push_rel env id = Vect.push env.name_rel id - - let push_rels env ids = - Array.iter (push_rel env) ids - - let pop env = Vect.pop env.name_rel - - let popn env n = - for _i = 1 to n do pop env done - - let get env n = - Lrel (Vect.get_last env.name_rel (n-1), n) - - let get_construct_info env c = - try ConstrTable.find env.construct_tbl c + let get_construct_info cache env c : constructor_info = + try ConstrTable.find cache c with Not_found -> let ((mind,j), i) = c in - let oib = lookup_mind mind !global_env in + let oib = lookup_mind mind env in let oip = oib.mind_packets.(j) in let tag,arity = oip.mind_reloc_tbl.(i-1) in let nparams = oib.mind_nparams in let r = (tag, nparams, arity) in - ConstrTable.add env.construct_tbl c r; + ConstrTable.add cache c r; r end -let is_lazy prefix t = +let is_lazy env prefix t = match kind t with | App (f,args) -> begin match kind f with @@ -440,7 +374,7 @@ let is_lazy prefix t = let entry = mkInd (fst c) in (try let _ = - Retroknowledge.get_native_before_match_info (!global_env).retroknowledge + Retroknowledge.get_native_before_match_info env.retroknowledge entry prefix c Llazy; in false @@ -463,73 +397,85 @@ let empty_evars = let empty_ids = [||] -let rec lambda_of_constr env sigma c = +(** Extract the inductive type over which a fixpoint is decreasing *) +let rec get_fix_struct env i t = match kind (Reduction.whd_all env t) with +| Prod (na, dom, t) -> + if Int.equal i 0 then + let dom = Reduction.whd_all env dom in + let (dom, _) = decompose_appvect dom in + match kind dom with + | Ind (ind, _) -> ind + | _ -> assert false + else + let env = Environ.push_rel (RelDecl.LocalAssum (na, dom)) env in + get_fix_struct env (i - 1) t +| _ -> assert false + +let rec lambda_of_constr cache env sigma c = match kind c with | Meta mv -> let ty = meta_type sigma mv in - Lmeta (mv, lambda_of_constr env sigma ty) + Lmeta (mv, lambda_of_constr cache env sigma ty) | Evar (evk,args as ev) -> (match evar_value sigma ev with | None -> let ty = evar_type sigma ev in - let args = Array.map (lambda_of_constr env sigma) args in - Levar(evk, lambda_of_constr env sigma ty, args) - | Some t -> lambda_of_constr env sigma t) + let args = Array.map (lambda_of_constr cache env sigma) args in + Levar(evk, lambda_of_constr cache env sigma ty, args) + | Some t -> lambda_of_constr cache env sigma t) - | Cast (c, _, _) -> lambda_of_constr env sigma c + | Cast (c, _, _) -> lambda_of_constr cache env sigma c - | Rel i -> Renv.get env i + | Rel i -> Lrel (RelDecl.get_name (Environ.lookup_rel i env), i) | Var id -> Lvar id | Sort s -> Lsort s | Ind (ind,u as pind) -> - let prefix = get_mind_prefix !global_env (fst ind) in + let prefix = get_mind_prefix env (fst ind) in Lind (prefix, pind) | Prod(id, dom, codom) -> - let ld = lambda_of_constr env sigma dom in - Renv.push_rel env id; - let lc = lambda_of_constr env sigma codom in - Renv.pop env; + let ld = lambda_of_constr cache env sigma dom in + let env = Environ.push_rel (RelDecl.LocalAssum (id, dom)) env in + let lc = lambda_of_constr cache env sigma codom in Lprod(ld, Llam([|id|], lc)) | Lambda _ -> let params, body = Term.decompose_lam c in + let fold (na, t) env = Environ.push_rel (RelDecl.LocalAssum (na, t)) env in + let env = List.fold_right fold params env in + let lb = lambda_of_constr cache env sigma body in let ids = get_names (List.rev params) in - Renv.push_rels env ids; - let lb = lambda_of_constr env sigma body in - Renv.popn env (Array.length ids); mkLlam ids lb - | LetIn(id, def, _, body) -> - let ld = lambda_of_constr env sigma def in - Renv.push_rel env id; - let lb = lambda_of_constr env sigma body in - Renv.pop env; + | LetIn(id, def, t, body) -> + let ld = lambda_of_constr cache env sigma def in + let env = Environ.push_rel (RelDecl.LocalDef (id, def, t)) env in + let lb = lambda_of_constr cache env sigma body in Llet(id, ld, lb) - | App(f, args) -> lambda_of_app env sigma f args + | App(f, args) -> lambda_of_app cache env sigma f args - | Const _ -> lambda_of_app env sigma c empty_args + | Const _ -> lambda_of_app cache env sigma c empty_args - | Construct _ -> lambda_of_app env sigma c empty_args + | Construct _ -> lambda_of_app cache env sigma c empty_args | Proj (p, c) -> - let pb = lookup_projection p !global_env in + let pb = lookup_projection p env in let ind = pb.proj_ind in - let prefix = get_mind_prefix !global_env (fst ind) in - mkLapp (Lproj (prefix, ind, pb.proj_arg)) [|lambda_of_constr env sigma c|] + let prefix = get_mind_prefix env (fst ind) in + mkLapp (Lproj (prefix, ind, pb.proj_arg)) [|lambda_of_constr cache env sigma c|] | Case(ci,t,a,branches) -> let (mind,i as ind) = ci.ci_ind in - let mib = lookup_mind mind !global_env in + let mib = lookup_mind mind env in let oib = mib.mind_packets.(i) in let tbl = oib.mind_reloc_tbl in (* Building info *) - let prefix = get_mind_prefix !global_env mind in + let prefix = get_mind_prefix env mind in let annot_sw = { asw_ind = ind; asw_ci = ci; @@ -538,21 +484,21 @@ let rec lambda_of_constr env sigma c = asw_prefix = prefix} in (* translation of the argument *) - let la = lambda_of_constr env sigma a in + let la = lambda_of_constr cache env sigma a in let entry = mkInd ind in let la = try - Retroknowledge.get_native_before_match_info (!global_env).retroknowledge + Retroknowledge.get_native_before_match_info (env).retroknowledge entry prefix (ind,1) la with Not_found -> la in (* translation of the type *) - let lt = lambda_of_constr env sigma t in + let lt = lambda_of_constr cache env sigma t in (* translation of branches *) let mk_branch i b = let cn = (ind,i+1) in let _, arity = tbl.(i) in - let b = lambda_of_constr env sigma b in + let b = lambda_of_constr cache env sigma b in if Int.equal arity 0 then (cn, empty_ids, b) else match b with @@ -565,86 +511,90 @@ let rec lambda_of_constr env sigma c = let bs = Array.mapi mk_branch branches in Lcase(annot_sw, lt, la, bs) - | Fix(rec_init,(names,type_bodies,rec_bodies)) -> - let ltypes = lambda_of_args env sigma 0 type_bodies in - Renv.push_rels env names; - let lbodies = lambda_of_args env sigma 0 rec_bodies in - Renv.popn env (Array.length names); - Lfix(rec_init, (names, ltypes, lbodies)) + | Fix((pos, i), (names,type_bodies,rec_bodies)) -> + let ltypes = lambda_of_args cache env sigma 0 type_bodies in + let map i t = + let ind = get_fix_struct env i t in + let prefix = get_mind_prefix env (fst ind) in + (prefix, ind) + in + let inds = Array.map2 map pos type_bodies in + let env = Environ.push_rec_types (names, type_bodies, rec_bodies) env in + let lbodies = lambda_of_args cache env sigma 0 rec_bodies in + Lfix((pos, inds, i), (names, ltypes, lbodies)) | CoFix(init,(names,type_bodies,rec_bodies)) -> - let rec_bodies = Array.map2 (Reduction.eta_expand !global_env) rec_bodies type_bodies in - let ltypes = lambda_of_args env sigma 0 type_bodies in - Renv.push_rels env names; - let lbodies = lambda_of_args env sigma 0 rec_bodies in - Renv.popn env (Array.length names); + let rec_bodies = Array.map2 (Reduction.eta_expand env) rec_bodies type_bodies in + let ltypes = lambda_of_args cache env sigma 0 type_bodies in + let env = Environ.push_rec_types (names, type_bodies, rec_bodies) env in + let lbodies = lambda_of_args cache env sigma 0 rec_bodies in Lcofix(init, (names, ltypes, lbodies)) -and lambda_of_app env sigma f args = +and lambda_of_app cache env sigma f args = match kind f with | Const (kn,u as c) -> - let kn,u = get_alias !global_env c in - let cb = lookup_constant kn !global_env in + let kn,u = get_alias env c in + let cb = lookup_constant kn env in (try - let prefix = get_const_prefix !global_env kn in + let prefix = get_const_prefix env kn in (* We delay the compilation of arguments to avoid an exponential behavior *) let f = Retroknowledge.get_native_compiling_info - (!global_env).retroknowledge (mkConst kn) prefix in - let args = lambda_of_args env sigma 0 args in + (env).retroknowledge (mkConst kn) prefix in + let args = lambda_of_args cache env sigma 0 args in f args with Not_found -> begin match cb.const_body with | Def csubst -> (* TODO optimize if f is a proj and argument is known *) if cb.const_inline_code then - lambda_of_app env sigma (Mod_subst.force_constr csubst) args + lambda_of_app cache env sigma (Mod_subst.force_constr csubst) args else - let prefix = get_const_prefix !global_env kn in + let prefix = get_const_prefix env kn in let t = - if is_lazy prefix (Mod_subst.force_constr csubst) then + if is_lazy env prefix (Mod_subst.force_constr csubst) then mkLapp Lforce [|Lconst (prefix, (kn,u))|] else Lconst (prefix, (kn,u)) in - mkLapp t (lambda_of_args env sigma 0 args) + mkLapp t (lambda_of_args cache env sigma 0 args) | OpaqueDef _ | Undef _ -> - let prefix = get_const_prefix !global_env kn in - mkLapp (Lconst (prefix, (kn,u))) (lambda_of_args env sigma 0 args) + let prefix = get_const_prefix env kn in + mkLapp (Lconst (prefix, (kn,u))) (lambda_of_args cache env sigma 0 args) end) | Construct (c,u) -> - let tag, nparams, arity = Renv.get_construct_info env c in + let tag, nparams, arity = Cache.get_construct_info cache env c in let expected = nparams + arity in let nargs = Array.length args in - let prefix = get_mind_prefix !global_env (fst (fst c)) in + let prefix = get_mind_prefix env (fst (fst c)) in if Int.equal nargs expected then try try Retroknowledge.get_native_constant_static_info - (!global_env).retroknowledge + (env).retroknowledge f args with NotClosed -> assert (Int.equal nparams 0); (* should be fine for int31 *) - let args = lambda_of_args env sigma nparams args in + let args = lambda_of_args cache env sigma nparams args in Retroknowledge.get_native_constant_dynamic_info - (!global_env).retroknowledge f prefix c args + (env).retroknowledge f prefix c args with Not_found -> - let args = lambda_of_args env sigma nparams args in - makeblock !global_env c u tag args + let args = lambda_of_args cache env sigma nparams args in + makeblock env c u tag args else - let args = lambda_of_args env sigma 0 args in + let args = lambda_of_args cache env sigma 0 args in (try Retroknowledge.get_native_constant_dynamic_info - (!global_env).retroknowledge f prefix c args + (env).retroknowledge f prefix c args with Not_found -> mkLapp (Lconstruct (prefix, (c,u))) args) | _ -> - let f = lambda_of_constr env sigma f in - let args = lambda_of_args env sigma 0 args in + let f = lambda_of_constr cache env sigma f in + let args = lambda_of_args cache env sigma 0 args in mkLapp f args -and lambda_of_args env sigma start args = +and lambda_of_args cache env sigma start args = let nargs = Array.length args in if start < nargs then Array.init (nargs - start) - (fun i -> lambda_of_constr env sigma args.(start + i)) + (fun i -> lambda_of_constr cache env sigma args.(start + i)) else empty_args let optimize lam = @@ -657,11 +607,8 @@ let optimize lam = lam let lambda_of_constr env sigma c = - set_global_env env; - let env = Renv.make () in - let ids = List.rev_map RelDecl.get_name (rel_context !global_env) in - Renv.push_rels env (Array.of_list ids); - let lam = lambda_of_constr env sigma c in + let cache = Cache.ConstrTable.create 91 in + let lam = lambda_of_constr cache env sigma c in (* if Flags.vm_draw_opt () then begin (msgerrnl (str "Constr = \n" ++ pr_constr c);flush_all()); (msgerrnl (str "Lambda = \n" ++ pp_lam lam);flush_all()); diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli index 26bfeb7e0..efe1700cd 100644 --- a/kernel/nativelambda.mli +++ b/kernel/nativelambda.mli @@ -23,7 +23,7 @@ val empty_evars : evars val decompose_Llam : lambda -> Name.t array * lambda val decompose_Llam_Llet : lambda -> (Name.t * lambda option) array * lambda -val is_lazy : prefix -> constr -> bool +val is_lazy : env -> prefix -> constr -> bool val mk_lazy : lambda -> lambda val get_mind_prefix : env -> MutInd.t -> string diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli index 649853f06..6bbf15160 100644 --- a/kernel/nativevalues.mli +++ b/kernel/nativevalues.mli @@ -110,9 +110,6 @@ type kind_of_value = val kind_of_value : t -> kind_of_value -(* *) -val is_accu : t -> bool - val str_encode : 'a -> string val str_decode : string -> 'a diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml index d76b05a8b..34f62defb 100644 --- a/kernel/retroknowledge.ml +++ b/kernel/retroknowledge.ml @@ -25,22 +25,6 @@ open Constr (* aliased type for clarity purpose*) type entry = Constr.t -(* [field]-s are the roles the kernel can learn of. *) -type nat_field = - | NatType - | NatPlus - | NatTimes - -type n_field = - | NPositive - | NType - | NTwice - | NTwicePlusOne - | NPhi - | NPhiInv - | NPlus - | NTimes - type int31_field = | Int31Bits | Int31Type @@ -69,9 +53,6 @@ type int31_field = | Int31Lxor type field = - (* | KEq - | KNat of nat_field - | KN of n_field *) | KInt31 of string*int31_field diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index 281c37b85..02d961d89 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.mli @@ -18,21 +18,6 @@ type entry = Constr.t (** the following types correspond to the different "things" the kernel can learn about.*) -type nat_field = - | NatType - | NatPlus - | NatTimes - -type n_field = - | NPositive - | NType - | NTwice - | NTwicePlusOne - | NPhi - | NPhiInv - | NPlus - | NTimes - type int31_field = | Int31Bits | Int31Type @@ -61,13 +46,8 @@ type int31_field = | Int31Lxor type field = - -(** | KEq - | KNat of nat_field - | KN of n_field *) | KInt31 of string*int31_field - (** This type represent an atomic action of the retroknowledge. It is stored in the compiled libraries As per now, there is only the possibility of registering things diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index dae2582bd..dbbdbfa39 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -297,25 +297,6 @@ END (* spiwack: the print functions are incomplete, but I don't know what they are used for *) -let pr_r_nat_field natf = - str "nat " ++ - match natf with - | Retroknowledge.NatType -> str "type" - | Retroknowledge.NatPlus -> str "plus" - | Retroknowledge.NatTimes -> str "times" - -let pr_r_n_field nf = - str "binary N " ++ - match nf with - | Retroknowledge.NPositive -> str "positive" - | Retroknowledge.NType -> str "type" - | Retroknowledge.NTwice -> str "twice" - | Retroknowledge.NTwicePlusOne -> str "twice plus one" - | Retroknowledge.NPhi -> str "phi" - | Retroknowledge.NPhiInv -> str "phi inv" - | Retroknowledge.NPlus -> str "plus" - | Retroknowledge.NTimes -> str "times" - let pr_r_int31_field i31f = str "int31 " ++ match i31f with @@ -353,26 +334,6 @@ let pr_retroknowledge_field f = | Retroknowledge.KInt31 (group, i31f) -> (pr_r_int31_field i31f) ++ spc () ++ str "in " ++ qs group -VERNAC ARGUMENT EXTEND retroknowledge_nat -PRINTED BY pr_r_nat_field -| [ "nat" "type" ] -> [ Retroknowledge.NatType ] -| [ "nat" "plus" ] -> [ Retroknowledge.NatPlus ] -| [ "nat" "times" ] -> [ Retroknowledge.NatTimes ] -END - - -VERNAC ARGUMENT EXTEND retroknowledge_binary_n -PRINTED BY pr_r_n_field -| [ "binary" "N" "positive" ] -> [ Retroknowledge.NPositive ] -| [ "binary" "N" "type" ] -> [ Retroknowledge.NType ] -| [ "binary" "N" "twice" ] -> [ Retroknowledge.NTwice ] -| [ "binary" "N" "twice" "plus" "one" ] -> [ Retroknowledge.NTwicePlusOne ] -| [ "binary" "N" "phi" ] -> [ Retroknowledge.NPhi ] -| [ "binary" "N" "phi" "inv" ] -> [ Retroknowledge.NPhiInv ] -| [ "binary" "N" "plus" ] -> [ Retroknowledge.NPlus ] -| [ "binary" "N" "times" ] -> [ Retroknowledge.NTimes ] -END - VERNAC ARGUMENT EXTEND retroknowledge_int31 PRINTED BY pr_r_int31_field | [ "int31" "bits" ] -> [ Retroknowledge.Int31Bits ] diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index 9d86f21d4..c13bd69da 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -287,12 +287,14 @@ GEXTEND Gram (* Definitions for tactics *) tacdef_body: - [ [ name = Constr.global; it=LIST1 input_fun; redef = ltac_def_kind; body = tactic_expr -> + [ [ name = Constr.global; it=LIST1 input_fun; + redef = ltac_def_kind; body = tactic_expr -> if redef then Tacexpr.TacticRedefinition (name, TacFun (it, body)) else let id = reference_to_id name in Tacexpr.TacticDefinition (id, TacFun (it, body)) - | name = Constr.global; redef = ltac_def_kind; body = tactic_expr -> + | name = Constr.global; redef = ltac_def_kind; + body = tactic_expr -> if redef then Tacexpr.TacticRedefinition (name, body) else let id = reference_to_id name in @@ -468,7 +470,8 @@ VERNAC COMMAND FUNCTIONAL EXTEND VernacTacticNotation [ VtSideff [], VtNow ] -> [ fun ~atts ~st -> let open Vernacinterp in let n = Option.default 0 n in - Tacentries.add_tactic_notation (Locality.make_module_locality atts.locality) n r e; + let deprecation = atts.deprecated in + Tacentries.add_tactic_notation (Locality.make_module_locality atts.locality) n ?deprecation r e; st ] END @@ -512,7 +515,8 @@ VERNAC COMMAND FUNCTIONAL EXTEND VernacDeclareTacticDefinition | TacticDefinition ({CAst.v=r},_) -> r | TacticRedefinition (qid,_) -> qualid_basename qid) l), VtLater ] -> [ fun ~atts ~st -> let open Vernacinterp in - Tacentries.register_ltac (Locality.make_module_locality atts.locality) l; + let deprecation = atts.deprecated in + Tacentries.register_ltac (Locality.make_module_locality atts.locality) ?deprecation l; st ] END diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index fac464a62..4b834d66d 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -252,7 +252,7 @@ type tactic_grammar_obj = { tacobj_key : KerName.t; tacobj_local : locality_flag; tacobj_tacgram : tactic_grammar; - tacobj_body : Id.t list * Tacexpr.glob_tactic_expr; + tacobj_body : Tacenv.alias_tactic; tacobj_forml : bool; } @@ -288,10 +288,11 @@ let load_tactic_notation i (_, tobj) = extend_tactic_grammar key tobj.tacobj_forml tobj.tacobj_tacgram let subst_tactic_notation (subst, tobj) = - let (ids, body) = tobj.tacobj_body in + let open Tacenv in + let alias = tobj.tacobj_body in { tobj with tacobj_key = Mod_subst.subst_kn subst tobj.tacobj_key; - tacobj_body = (ids, Tacsubst.subst_tactic subst body); + tacobj_body = { alias with alias_body = Tacsubst.subst_tactic subst alias.alias_body }; } let classify_tactic_notation tacobj = Substitute tacobj @@ -308,25 +309,26 @@ let cons_production_parameter = function | TacTerm _ -> None | TacNonTerm (_, (_, ido)) -> ido -let add_glob_tactic_notation local ~level prods forml ids tac = +let add_glob_tactic_notation local ~level ?deprecation prods forml ids tac = let parule = { tacgram_level = level; tacgram_prods = prods; } in + let open Tacenv in let tacobj = { tacobj_key = make_fresh_key prods; tacobj_local = local; tacobj_tacgram = parule; - tacobj_body = (ids, tac); + tacobj_body = { alias_args = ids; alias_body = tac; alias_deprecation = deprecation }; tacobj_forml = forml; } in Lib.add_anonymous_leaf (inTacticGrammar tacobj) -let add_tactic_notation local n prods e = +let add_tactic_notation local n ?deprecation prods e = let ids = List.map_filter cons_production_parameter prods in let prods = List.map interp_prod_item prods in let tac = Tacintern.glob_tactic_env ids (Global.env()) e in - add_glob_tactic_notation local ~level:n prods false ids tac + add_glob_tactic_notation local ~level:n ?deprecation prods false ids tac (**********************************************************************) (* ML Tactic entries *) @@ -366,7 +368,7 @@ let extend_atomic_tactic name entries = in List.iteri add_atomic entries -let add_ml_tactic_notation name ~level prods = +let add_ml_tactic_notation name ~level ?deprecation prods = let len = List.length prods in let iter i prods = let open Tacexpr in @@ -378,7 +380,7 @@ let add_ml_tactic_notation name ~level prods = let entry = { mltac_name = name; mltac_index = len - i - 1 } in let map id = Reference (Locus.ArgVar (CAst.make id)) in let tac = TacML (Loc.tag (entry, List.map map ids)) in - add_glob_tactic_notation false ~level prods true ids tac + add_glob_tactic_notation false ~level ?deprecation prods true ids tac in List.iteri iter (List.rev prods); (** We call [extend_atomic_tactic] only for "basic tactics" (the ones at @@ -430,7 +432,7 @@ let warn_unusable_identifier = (fun id -> strbrk "The Ltac name" ++ spc () ++ Id.print id ++ spc () ++ strbrk "may be unusable because of a conflict with a notation.") -let register_ltac local tacl = +let register_ltac local ?deprecation tacl = let map tactic_body = match tactic_body with | Tacexpr.TacticDefinition ({CAst.loc;v=id}, body) -> @@ -483,10 +485,10 @@ let register_ltac local tacl = let defs = States.with_state_protection defs () in let iter (def, tac) = match def with | NewTac id -> - Tacenv.register_ltac false local id tac; + Tacenv.register_ltac false local id tac ?deprecation; Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is defined") | UpdateTac kn -> - Tacenv.redefine_ltac local kn tac; + Tacenv.redefine_ltac local kn tac ?deprecation; let name = Tacenv.shortest_qualid_of_tactic kn in Flags.if_verbose Feedback.msg_info (Libnames.pr_qualid name ++ str " is redefined") in @@ -658,7 +660,7 @@ let lift_constr_tac_to_ml_tac vars tac = end in tac -let tactic_extend plugin_name tacname ~level sign = +let tactic_extend plugin_name tacname ~level ?deprecation sign = let open Tacexpr in let ml_tactic_name = { mltac_tactic = tacname; @@ -687,10 +689,10 @@ let tactic_extend plugin_name tacname ~level sign = This is the rôle of the [lift_constr_tac_to_ml_tac] function. *) let body = Tacexpr.TacFun (vars, Tacexpr.TacML (Loc.tag (ml, [])))in let id = Names.Id.of_string name in - let obj () = Tacenv.register_ltac true false id body in + let obj () = Tacenv.register_ltac true false id body ?deprecation in let () = Tacenv.register_ml_tactic ml_tactic_name [|tac|] in Mltop.declare_cache_obj obj plugin_name | _ -> - let obj () = add_ml_tactic_notation ml_tactic_name ~level (List.map clause_of_ty_ml sign) in + let obj () = add_ml_tactic_notation ml_tactic_name ~level ?deprecation (List.map clause_of_ty_ml sign) in Tacenv.register_ml_tactic ml_tactic_name @@ Array.of_list (List.map eval sign); Mltop.declare_cache_obj obj plugin_name diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index f873631ff..138a584e0 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -12,10 +12,12 @@ open Vernacexpr open Tacexpr +open Vernacinterp (** {5 Tactic Definitions} *) -val register_ltac : locality_flag -> Tacexpr.tacdef_body list -> unit +val register_ltac : locality_flag -> ?deprecation:deprecation -> + Tacexpr.tacdef_body list -> unit (** Adds new Ltac definitions to the environment. *) (** {5 Tactic Notations} *) @@ -34,8 +36,8 @@ type argument = Genarg.ArgT.any Extend.user_symbol leaves. *) val add_tactic_notation : - locality_flag -> int -> raw_argument grammar_tactic_prod_item_expr list -> - raw_tactic_expr -> unit + locality_flag -> int -> ?deprecation:deprecation -> raw_argument + grammar_tactic_prod_item_expr list -> raw_tactic_expr -> unit (** [add_tactic_notation local level prods expr] adds a tactic notation in the environment at level [level] with locality [local] made of the grammar productions [prods] and returning the body [expr] *) @@ -47,7 +49,7 @@ val register_tactic_notation_entry : string -> ('a, 'b, 'c) Genarg.genarg_type - to finding an argument by name (as in {!Genarg}) if there is none matching. *) -val add_ml_tactic_notation : ml_tactic_name -> level:int -> +val add_ml_tactic_notation : ml_tactic_name -> level:int -> ?deprecation:deprecation -> argument grammar_tactic_prod_item_expr list list -> unit (** A low-level variant of {!add_tactic_notation} used by the TACTIC EXTEND ML-side macro. *) @@ -78,4 +80,5 @@ type _ ty_sig = type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml -val tactic_extend : string -> string -> level:Int.t -> ty_ml list -> unit +val tactic_extend : string -> string -> level:Int.t -> + ?deprecation:deprecation -> ty_ml list -> unit diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml index d5ab2d690..0bb9ccb1d 100644 --- a/plugins/ltac/tacenv.ml +++ b/plugins/ltac/tacenv.ml @@ -52,7 +52,11 @@ let shortest_qualid_of_tactic kn = (** Tactic notations (TacAlias) *) type alias = KerName.t -type alias_tactic = Id.t list * glob_tactic_expr +type alias_tactic = + { alias_args: Id.t list; + alias_body: glob_tactic_expr; + alias_deprecation: Vernacinterp.deprecation option; + } let alias_map = Summary.ref ~name:"tactic-alias" (KNmap.empty : alias_tactic KNmap.t) @@ -118,6 +122,7 @@ type ltac_entry = { tac_for_ml : bool; tac_body : glob_tactic_expr; tac_redef : ModPath.t list; + tac_deprecation : Vernacinterp.deprecation option } let mactab = @@ -130,8 +135,12 @@ let interp_ltac r = (KNmap.find r !mactab).tac_body let is_ltac_for_ml_tactic r = (KNmap.find r !mactab).tac_for_ml -let add kn b t = - let entry = { tac_for_ml = b; tac_body = t; tac_redef = [] } in +let add ~deprecation kn b t = + let entry = { tac_for_ml = b; + tac_body = t; + tac_redef = []; + tac_deprecation = deprecation; + } in mactab := KNmap.add kn entry !mactab let replace kn path t = @@ -139,34 +148,38 @@ let replace kn path t = let entry _ e = { e with tac_body = t; tac_redef = path :: e.tac_redef } in mactab := KNmap.modify kn entry !mactab -let load_md i ((sp, kn), (local, id, b, t)) = match id with +let tac_deprecation kn = + try (KNmap.find kn !mactab).tac_deprecation with Not_found -> None + +let load_md i ((sp, kn), (local, id, b, t, deprecation)) = match id with | None -> let () = if not local then push_tactic (Until i) sp kn in - add kn b t + add ~deprecation kn b t | Some kn0 -> replace kn0 kn t -let open_md i ((sp, kn), (local, id, b, t)) = match id with +let open_md i ((sp, kn), (local, id, b, t, deprecation)) = match id with | None -> let () = if not local then push_tactic (Exactly i) sp kn in - add kn b t + add ~deprecation kn b t | Some kn0 -> replace kn0 kn t -let cache_md ((sp, kn), (local, id ,b, t)) = match id with +let cache_md ((sp, kn), (local, id ,b, t, deprecation)) = match id with | None -> let () = push_tactic (Until 1) sp kn in - add kn b t + add ~deprecation kn b t | Some kn0 -> replace kn0 kn t let subst_kind subst id = match id with | None -> None | Some kn -> Some (Mod_subst.subst_kn subst kn) -let subst_md (subst, (local, id, b, t)) = - (local, subst_kind subst id, b, Tacsubst.subst_tactic subst t) +let subst_md (subst, (local, id, b, t, deprecation)) = + (local, subst_kind subst id, b, Tacsubst.subst_tactic subst t, deprecation) -let classify_md (local, _, _, _ as o) = Substitute o +let classify_md (local, _, _, _, _ as o) = Substitute o -let inMD : bool * ltac_constant option * bool * glob_tactic_expr -> obj = +let inMD : bool * ltac_constant option * bool * glob_tactic_expr * + Vernacinterp.deprecation option -> obj = declare_object {(default_object "TAC-DEFINITION") with cache_function = cache_md; load_function = load_md; @@ -174,8 +187,8 @@ let inMD : bool * ltac_constant option * bool * glob_tactic_expr -> obj = subst_function = subst_md; classify_function = classify_md} -let register_ltac for_ml local id tac = - ignore (Lib.add_leaf id (inMD (local, None, for_ml, tac))) +let register_ltac for_ml local ?deprecation id tac = + ignore (Lib.add_leaf id (inMD (local, None, for_ml, tac, deprecation))) -let redefine_ltac local kn tac = - Lib.add_anonymous_leaf (inMD (local, Some kn, false, tac)) +let redefine_ltac local ?deprecation kn tac = + Lib.add_anonymous_leaf (inMD (local, Some kn, false, tac, deprecation)) diff --git a/plugins/ltac/tacenv.mli b/plugins/ltac/tacenv.mli index 3af2f2a46..7143f5185 100644 --- a/plugins/ltac/tacenv.mli +++ b/plugins/ltac/tacenv.mli @@ -12,6 +12,7 @@ open Names open Libnames open Tacexpr open Geninterp +open Vernacinterp (** This module centralizes the various ways of registering tactics. *) @@ -29,7 +30,11 @@ val shortest_qualid_of_tactic : ltac_constant -> qualid type alias = KerName.t (** Type of tactic alias, used in the [TacAlias] node. *) -type alias_tactic = Id.t list * glob_tactic_expr +type alias_tactic = + { alias_args: Id.t list; + alias_body: glob_tactic_expr; + alias_deprecation: Vernacinterp.deprecation option; + } (** Contents of a tactic notation *) val register_alias : alias -> alias_tactic -> unit @@ -43,7 +48,8 @@ val check_alias : alias -> bool (** {5 Coq tactic definitions} *) -val register_ltac : bool -> bool -> Id.t -> glob_tactic_expr -> unit +val register_ltac : bool -> bool -> ?deprecation:deprecation -> Id.t -> + glob_tactic_expr -> unit (** Register a new Ltac with the given name and body. The first boolean indicates whether this is done from ML side, rather than @@ -51,7 +57,8 @@ val register_ltac : bool -> bool -> Id.t -> glob_tactic_expr -> unit definition. It also puts the Ltac name in the nametab, so that it can be used unqualified. *) -val redefine_ltac : bool -> KerName.t -> glob_tactic_expr -> unit +val redefine_ltac : bool -> ?deprecation:deprecation -> KerName.t -> + glob_tactic_expr -> unit (** Replace a Ltac with the given name and body. If the boolean flag is set to true, then this is a local redefinition. *) @@ -61,6 +68,9 @@ val interp_ltac : KerName.t -> glob_tactic_expr val is_ltac_for_ml_tactic : KerName.t -> bool (** Whether the tactic is defined from ML-side *) +val tac_deprecation : KerName.t -> deprecation option +(** The tactic deprecation notice, if any *) + type ltac_entry = { tac_for_ml : bool; (** Whether the tactic is defined from ML-side *) @@ -68,6 +78,8 @@ type ltac_entry = { (** The current body of the tactic *) tac_redef : ModPath.t list; (** List of modules redefining the tactic in reverse chronological order *) + tac_deprecation : deprecation option; + (** Deprecation notice to be printed when the tactic is used *) } val ltac_entries : unit -> ltac_entry KNmap.t diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml index 06d2711ad..59b748e25 100644 --- a/plugins/ltac/tacexpr.ml +++ b/plugins/ltac/tacexpr.ml @@ -398,5 +398,5 @@ type ltac_call_kind = type ltac_trace = ltac_call_kind Loc.located list type tacdef_body = - | TacticDefinition of lident * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *) - | TacticRedefinition of qualid * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *) + | TacticDefinition of lident * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *) + | TacticRedefinition of qualid * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *) diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 71e1edfd7..3a0badb28 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -398,5 +398,5 @@ type ltac_call_kind = type ltac_trace = ltac_call_kind Loc.located list type tacdef_body = - | TacticDefinition of lident * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *) - | TacticRedefinition of qualid * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *) + | TacticDefinition of lident * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *) + | TacticRedefinition of qualid * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *) diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 481fc30df..144480062 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -117,9 +117,26 @@ let intern_constr_reference strict ist qid = (* Internalize an isolated reference in position of tactic *) +let warn_deprecated_tactic = + CWarnings.create ~name:"deprecated-tactic" ~category:"deprecated" + (fun (qid,depr) -> str "Tactic " ++ pr_qualid qid ++ + strbrk " is deprecated" ++ + pr_opt (fun since -> str "since " ++ str since) depr.Vernacinterp.since ++ + str "." ++ pr_opt (fun note -> str note) depr.Vernacinterp.note) + +let warn_deprecated_alias = + CWarnings.create ~name:"deprecated-tactic-notation" ~category:"deprecated" + (fun (kn,depr) -> str "Tactic Notation " ++ Pptactic.pr_alias_key kn ++ + strbrk " is deprecated since" ++ + pr_opt (fun since -> str "since " ++ str since) depr.Vernacinterp.since ++ + str "." ++ pr_opt (fun note -> str note) depr.Vernacinterp.note) + let intern_isolated_global_tactic_reference qid = let loc = qid.CAst.loc in - TacCall (Loc.tag ?loc (ArgArg (loc,Tacenv.locate_tactic qid),[])) + let kn = Tacenv.locate_tactic qid in + Option.iter (fun depr -> warn_deprecated_tactic ?loc (qid,depr)) @@ + Tacenv.tac_deprecation kn; + TacCall (Loc.tag ?loc (ArgArg (loc,kn),[])) let intern_isolated_tactic_reference strict ist qid = (* An ltac reference *) @@ -137,7 +154,11 @@ let intern_isolated_tactic_reference strict ist qid = (* Internalize an applied tactic reference *) let intern_applied_global_tactic_reference qid = - ArgArg (qid.CAst.loc,Tacenv.locate_tactic qid) + let loc = qid.CAst.loc in + let kn = Tacenv.locate_tactic qid in + Option.iter (fun depr -> warn_deprecated_tactic ?loc (qid,depr)) @@ + Tacenv.tac_deprecation kn; + ArgArg (loc,kn) let intern_applied_tactic_reference ist qid = (* An ltac reference *) @@ -643,6 +664,8 @@ and intern_tactic_seq onlytac ist = function (* For extensions *) | TacAlias (loc,(s,l)) -> + let alias = Tacenv.interp_alias s in + Option.iter (fun o -> warn_deprecated_alias ?loc (s,o)) @@ alias.Tacenv.alias_deprecation; let l = List.map (intern_tacarg !strict_check false ist) l in ist.ltacvars, TacAlias (Loc.tag ?loc (s,l)) | TacML (loc,(opn,l)) -> diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index d9ac96d89..77b5b06d4 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1125,17 +1125,17 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with | TacSelect (sel, tac) -> Tacticals.New.tclSELECT sel (interp_tactic ist tac) (* For extensions *) | TacAlias (loc,(s,l)) -> - let (ids, body) = Tacenv.interp_alias s in + let alias = Tacenv.interp_alias s in let (>>=) = Ftactic.bind in let interp_vars = Ftactic.List.map (fun v -> interp_tacarg ist v) l in let tac l = let addvar x v accu = Id.Map.add x v accu in - let lfun = List.fold_right2 addvar ids l ist.lfun in + let lfun = List.fold_right2 addvar alias.Tacenv.alias_args l ist.lfun in Ftactic.lift (push_trace (loc,LtacNotationCall s) ist) >>= fun trace -> let ist = { lfun = lfun; extra = TacStore.set ist.extra f_trace trace; } in - val_interp ist body >>= fun v -> + val_interp ist alias.Tacenv.alias_body >>= fun v -> Ftactic.lift (tactic_of_value ist v) in let tac = @@ -1147,7 +1147,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with some more elaborate solution will have to be used. *) in let tac = - let len1 = List.length ids in + let len1 = List.length alias.Tacenv.alias_args in let len2 = List.length l in if len1 = len2 then tac else Tacticals.New.tclZEROMSG (str "Arguments length mismatch: \ diff --git a/test-suite/output/Deprecation.out b/test-suite/output/Deprecation.out new file mode 100644 index 000000000..7e290847c --- /dev/null +++ b/test-suite/output/Deprecation.out @@ -0,0 +1,3 @@ +File "stdin", line 5, characters 0-3: +Warning: Tactic foo is deprecated since X.Y. Use idtac instead. +[deprecated-tactic,deprecated] diff --git a/test-suite/output/Deprecation.v b/test-suite/output/Deprecation.v new file mode 100644 index 000000000..04d5eb3d4 --- /dev/null +++ b/test-suite/output/Deprecation.v @@ -0,0 +1,6 @@ +#[deprecated(since = "X.Y", note = "Use idtac instead.")] + Ltac foo := idtac. + +Goal True. +foo. +Abort. diff --git a/test-suite/success/LtacDeprecation.v b/test-suite/success/LtacDeprecation.v new file mode 100644 index 000000000..633a5e474 --- /dev/null +++ b/test-suite/success/LtacDeprecation.v @@ -0,0 +1,32 @@ +Set Warnings "+deprecated". + +#[deprecated(since = "8.8", note = "Use idtac instead")] +Ltac foo x := idtac. + +Goal True. +Fail (foo true). +Abort. + +Fail Ltac bar := foo. +Fail Tactic Notation "bar" := foo. + +#[deprecated(since = "8.8", note = "Use idtac instead")] +Tactic Notation "bar" := idtac. + +Goal True. +Fail bar. +Abort. + +Fail Ltac zar := bar. + +Set Warnings "-deprecated". + +Ltac zar := foo. +Ltac zarzar := bar. + +Set Warnings "+deprecated". + +Goal True. +zar x. +zarzar. +Abort. |