diff options
44 files changed, 580 insertions, 262 deletions
diff --git a/.circleci/config.yml b/.circleci/config.yml index 14c102cede..79f83d4720 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -160,22 +160,22 @@ workflows: requires: - build - bignums - - compcert: *req-main - - coq-dpdgraph: *req-main - - coquelicot: *req-main - - cross-crypto: *req-main - - elpi: *req-main - - equations: *req-main - - geocoq: *req-main - - fcsl-pcm: *req-main - - fiat-crypto: *req-main - - fiat-parsers: *req-main - - flocq: *req-main + # - compcert: *req-main + # - coq-dpdgraph: *req-main + # - coquelicot: *req-main + # - cross-crypto: *req-main + # - elpi: *req-main + # - equations: *req-main + # - geocoq: *req-main + # - fcsl-pcm: *req-main + # - fiat-crypto: *req-main + # - fiat-parsers: *req-main + # - flocq: *req-main - math-classes: requires: - build - bignums - - mtac2: *req-main + # - mtac2: *req-main - corn: requires: - build @@ -184,11 +184,11 @@ workflows: requires: - build - corn - - hott: *req-main - - iris-lambda-rust: *req-main - - ltac2: *req-main - - math-comp: *req-main - - pidetop: *req-main - - sf: *req-main - - unimath: *req-main - - vst: *req-main + # - hott: *req-main + # - iris-lambda-rust: *req-main + # - ltac2: *req-main + # - math-comp: *req-main + # - pidetop: *req-main + # - sf: *req-main + # - unimath: *req-main + # - vst: *req-main diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index ab9725c967..2ca8274929 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -8,9 +8,13 @@ ########## CI infrastructure ########## -/dev/ci/*.sh @ejgallego +/dev/ci/ @ejgallego # Secondary maintainer @SkySkimmer +/dev/ci/user-overlays/*.sh @ghost +# Trick to avoid getting review requests +# each time someone adds an overlay + /.circleci/ @SkySkimmer # Secondary maintainer @ejgallego @@ -20,7 +24,9 @@ /.gitlab-ci.yml @SkySkimmer # Secondary maintainer @ejgallego -/appveyor.yml @maximedenes +/appveyor.yml @maximedenes +/dev/ci/appveyor.* @maximedenes +/dev/ci/*.bat @maximedenes # Secondary maintainer @SkySkimmer /default.nix @Zimmi48 @@ -338,3 +344,6 @@ /dev/tools/pre-commit @SkySkimmer /dev/tools/sudo-apt-get-update @JasonGross + +/dev/tools/check-owners*.sh @SkySkimmer +# Secondary maintainer @maximedenes diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 496444f7d1..656fd741f7 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -134,6 +134,24 @@ before_script: OPAM_SWITCH: "edge" OPAM_VARIANT: "+flambda" +.windows-template: &windows-template + stage: test + artifacts: + name: "%CI_JOB_NAME%" + paths: + - dev\nsis\*.exe + - coq-opensource-archive-windows-*.zip + expire_in: 1 week + dependencies: [] + tags: + - windows + before_script: [] + script: + - call dev/ci/gitlab.bat + only: + variables: + - $WINDOWS == "enabled" + build:base: <<: *build-template variables: @@ -160,6 +178,16 @@ build:edge+flambda: COQ_EXTRA_CONF: "-native-compiler no -coqide opt -flambda-opts " COQ_EXTRA_CONF_QUOTE: "-O3 -unbox-closures" +windows64: + <<: *windows-template + variables: + ARCH: "64" + +windows32: + <<: *windows-template + variables: + ARCH: "32" + warnings:base: <<: *warnings-template diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 1a3c993697..7fb976ee0e 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -28,7 +28,13 @@ Please make pull requests against the `master` branch. If it's your first significant contribution to Coq (significant means: more than fixing a typo), your pull request should include a commit adding your name to the [`CREDITS`](/CREDITS) file (possibly with the name of your institution / employer if relevant to your contribution, an ORCID if you have one —you may log into https://orcid.org/ using your institutional account to get one—, and the year of your contribution). -It's helpful to run the Coq test suite with `make test-suite` before submitting your change. Travis CI runs this test suite and a much larger one including external Coq developments on every pull request, but these results take significantly longer to come back (on the order of a few hours). Running the test suite locally will take somewhere around 10-15 minutes. Refer to [`dev/ci/README.md`](/dev/ci/README.md#information-for-developers) for more information on Travis CI tests. +It's helpful to run the Coq test suite with `make test-suite` before submitting +your change. Our CI runs this test suite and lots of other tests, including +building external Coq developments, on every pull request, but these results +take significantly longer to come back (on the order of a few hours). Running +the test suite locally will take somewhere around 10-15 minutes. Refer to +[`dev/ci/README.md`](/dev/ci/README.md#information-for-developers) for more +information on CI tests, including how to run them on your private branches. If your pull request fixes a bug, please consider adding a regression test as well. See [`test-suite/README.md`](/test-suite/README.md) for how to do so. diff --git a/Makefile.doc b/Makefile.doc index d13d0c09e3..41ae11b869 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -49,7 +49,11 @@ DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex doc: sphinx stdlib -sphinx: coq +ifndef QUICK +SPHINX_DEPS := coq +endif + +sphinx: $(SPHINX_DEPS) $(SHOW)'SPHINXBUILD doc/sphinx' $(HIDE)COQBIN="$(PWD)/bin" $(SPHINXBUILD) -W -b html $(ALLSPHINXOPTS) doc/sphinx $(SPHINXBUILDDIR)/html @echo @@ -1,5 +1,6 @@ # Coq +[](https://gitlab.com/coq/coq/commits/master) [](https://travis-ci.org/coq/coq/builds) [](https://ci.appveyor.com/project/coq/coq/branch/master) [](https://circleci.com/gh/coq/workflows/coq/tree/master) diff --git a/appveyor.yml b/appveyor.yml index 44a93d15d4..cd3b88d007 100644 --- a/appveyor.yml +++ b/appveyor.yml @@ -10,10 +10,6 @@ image: environment: CYGMIRROR: http://ftp.inf.tu-dresden.de/software/windows/cygwin32 matrix: - - USEOPAM: false - ARCH: 32 - - USEOPAM: false - ARCH: 64 - USEOPAM: true ARCH: 64 @@ -21,11 +17,3 @@ build_script: - cmd: 'call %APPVEYOR_BUILD_FOLDER%\dev\ci\appveyor.bat' test: off - -artifacts: - - path: 'dev\nsis\*.exe' - name: installer - - - path: 'coq-opensource-archive-*.zip' - name: opensource-archive - diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index f4ec218b6b..3608f7305d 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -970,6 +970,10 @@ function make_lablgtk { # These changes are included in dev/build/windows/patches_coq/lablgtk-2.18.3.patch log2 make world + + # lablgtk does not escape FINDLIBDIR path, which can contain backslashes + sed -i "s|^FINDLIBDIR=.*|FINDLIBDIR=$PREFIXOCAML/libocaml/site-lib|" config.make + log2 make install log2 make clean build_post diff --git a/dev/ci/README.md b/dev/ci/README.md index bb13587e94..87f03aa994 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -36,9 +36,8 @@ On the condition that: - You do not push, to the branches that we test, commits that haven't been first tested to compile with the corresponding branch(es) of Coq. -- Your development compiles in less than 35 minutes with just two threads. - If this is not the case, consider adding a "lite" target that compiles just - part of it. +- You maintain a reasonable build time for your development, or you provide + a "lite" target that we can use. In case you forget to comply with these last three conditions, we would reach out to you and give you a 30-day grace period during which your development @@ -54,9 +53,10 @@ Add a new `ci-mydev.sh` script to [`dev/ci`](/dev/ci) (have a look at set the corresponding variables in [`ci-basic-overlay.sh`](/dev/ci/ci-basic-overlay.sh); add the corresponding target to [`Makefile.ci`](/Makefile.ci); add new jobs to -[`.travis.yml`](/.travis.yml) and [`.gitlab-ci.yml`](/.gitlab-ci.yml) so that -this new target is run. **Do not hesitate to submit an incomplete pull request -if you need help to finish it.** +[`.gitlab-ci.yml`](/.gitlab-ci.yml), +[`.circleci/config.yml`](/.circleci/config.yml) and +[`.travis.yml`](/.travis.yml) so that this new target is run. **Do not +hesitate to submit an incomplete pull request if you need help to finish it.** You may also be interested in having your development tested in our performance benchmark. Currently this is done by providing an OPAM package @@ -71,24 +71,38 @@ When you submit a pull request (PR) on Coq GitHub repository, this will automatically launch a battery of CI tests. The PR will not be integrated unless these tests pass. -Currently, we have two CI platforms: +We are currently running tests on the following platforms: -- Travis is the main CI platform. It tests the compilation of Coq, of the +- GitLab CI is the main CI platform. It tests the compilation of Coq, of the documentation, and of CoqIDE on Linux with several versions of OCaml / camlp5, and with warnings as errors; it runs the test-suite and tests the - compilation of several external developments. It also tests the compilation - of Coq on OS X. + compilation of several external developments. + +- Circle CI runs tests that are redundant with GitLab CI and may be removed + eventually. + +- Travis CI is used to test the compilation of Coq and run the test-suite on + macOS. It also runs a linter that checks whitespace discipline. A + [pre-commit hook](/dev/tools/pre-commit) is automatically installed by + `./configure`. It should allow complying with this discipline without pain. - AppVeyor is used to test the compilation of Coq and run the test-suite on Windows. -You can anticipate the results of these tests prior to submitting your PR -by having them run of your fork of Coq, on GitHub or GitLab. This can be -especially helpful given that our Travis platform is often overloaded and -therefore there can be a significant delay before these tests are actually -run on your PR. To take advantage of this, simply create a Travis account -and link it to your GitHub account, or activate the pipelines on your GitLab -fork. +You can anticipate the results of most of these tests prior to submitting your +PR by running GitLab CI on your private branches. To do so follow these steps: + +1. Log into GitLab CI (the easiest way is to sign in with your GitHub account). +2. Click on "New Project". +3. Choose "CI / CD for external repository" then click on "GitHub". +4. Find your fork of the Coq repository and click on "Connect". +5. You are encouraged to go to the CI / CD general settings and increase the + timeout from 1h to 2h for better reliability. + +Now everytime you push (including force-push unless you changed the default +GitLab setting) to your fork on GitHub, it will be synchronized on GitLab and +CI will be run. You will receive an e-mail with a report of the failures if +there are some. You can also run one CI target locally (using `make ci-somedev`). @@ -97,36 +111,29 @@ so that it doesn't, or provide a branch fixing these developments (or at least work with the author of the development / other Coq developers to prepare these fixes). Then, add an overlay in [`dev/ci/user-overlays`](/dev/ci/user-overlays) (see the README there) -in a separate commit in your PR. +as part of your PR. The process to merge your PR is then to submit PRs to the external development repositories, merge the latter first (if the fixes are -backward-compatible), drop the overlay commit and merge the PR on Coq then. +backward-compatible), and merge the PR on Coq then. See also [`test-suite/README.md`](/test-suite/README.md) for information about adding new tests to the test-suite. -Travis specific information ---------------------------- - -Travis rebuilds all of Coq's executables and stdlib for each job. Coq -is built with `./configure -local`, then used for the job's test. - - -GitLab specific information ---------------------------- +Advanced GitLab CI information +------------------------------ -GitLab is set up to use the "build artifact" feature to avoid -rebuilding Coq. In one job, Coq is built with `./configure -prefix -install` and `make install` is run, then the `install` directory +GitLab CI is set up to use the "build artifact" feature to avoid +rebuilding Coq. In one job, Coq is built with `./configure -prefix _install_ci` +and `make install` is run, then the `_install_ci` directory persists to and is used by the next jobs. Artifacts can also be downloaded from the GitLab repository. Currently, available artifacts are: - the Coq executables and stdlib, in three copies varying in - architecture and Ocaml version used to build Coq. -- the Coq documentation, in two different copies varying in the OCaml - version used to build Coq + architecture and OCaml version used to build Coq. +- the Coq documentation, built only in the `build:base` job. When submitting + a documentation PR, this can help reviewers checking the rendered result. As an exception to the above, jobs testing that compilation triggers -no Ocaml warnings build Coq in parallel with other tests. +no OCaml warnings build Coq in parallel with other tests. diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 189734a0bc..2a14ed352a 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -10,6 +10,10 @@ if [ -n "${GITLAB_CI}" ]; then export COQBIN="$PWD/_install_ci/bin" export CI_BRANCH="$CI_COMMIT_REF_NAME" + if [[ ${CI_BRANCH#pr-} =~ ^[0-9]*$ ]] + then + export CI_PULL_REQUEST="${CI_BRANCH#pr-}" + fi else if [ -n "${TRAVIS}" ]; then diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat new file mode 100644 index 0000000000..70278e6d09 --- /dev/null +++ b/dev/ci/gitlab.bat @@ -0,0 +1,50 @@ +@ECHO OFF + +REM This script builds and signs the Windows packages on Gitlab + +if %ARCH% == 32 ( + SET ARCHLONG=i686 + SET CYGROOT=C:\cygwin + SET SETUP=setup-x86.exe +) + +if %ARCH% == 64 ( + SET ARCHLONG=x86_64 + SET CYGROOT=C:\cygwin64 + SET SETUP=setup-x86_64.exe +) + +powershell -Command "(New-Object Net.WebClient).DownloadFile('http://www.cygwin.com/%SETUP%', '%SETUP%')" +SET CYGCACHE=%CYGROOT%\var\cache\setup +SET CI_PROJECT_DIR_MFMT=%CI_PROJECT_DIR:\=/% +SET CI_PROJECT_DIR_CFMT=%CI_PROJECT_DIR_MFMT:C:/=/cygdrive/c/% +SET DESTCOQ=C:\coq%ARCH%_inst +SET COQREGTESTING=Y +SET PATH=%PATH%;C:\Program Files\7-Zip\;C:\Program Files\Microsoft SDKs\Windows\v7.1\Bin + +if exist %CYGROOT%\build\ rd /s /q %CYGROOT%\build +if exist %DESTCOQ%\ rd /s /q %DESTCOQ% + +call %CI_PROJECT_DIR%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^ + -arch=%ARCH% -installer=Y -coqver=%CI_PROJECT_DIR_CFMT% ^ + -destcyg=%CYGROOT% -destcoq=%DESTCOQ% -cygcache=%CYGCACHE% ^ + -addon=bignums -make=N ^ + -setup %CI_PROJECT_DIR%\%SETUP% || GOTO ErrorExit + +copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" dev\nsis || GOTO ErrorExit +7z a coq-opensource-archive-windows-%ARCHLONG%.zip %CYGROOT%\build\tarballs\* || GOTO ErrorExit + +REM DO NOT echo the signing command below, as this would leak secrets in the logs +IF DEFINED WIN_CERTIFICATE_PATH ( + IF DEFINED WIN_CERTIFICATE_PASSWORD ( + ECHO Signing package + @signtool sign /f %WIN_CERTIFICATE_PATH% /p %WIN_CERTIFICATE_PASSWORD% dev\nsis\*.exe + signtool verify /pa dev\nsis\*.exe + ) +) + +GOTO :EOF + +:ErrorExit + ECHO ERROR %0 failed + EXIT /b 1 diff --git a/dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh b/dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh new file mode 100644 index 0000000000..517088a247 --- /dev/null +++ b/dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "7213" ] || [ "$CI_BRANCH" = "fast-constr-match-no-context" ]; then + + ltac2_CI_BRANCH=fast-constr-match-no-context + ltac2_CI_GITURL=https://github.com/ppedrot/ltac2 + +fi diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md index 84ff94c66a..a466124c1c 100644 --- a/dev/doc/MERGING.md +++ b/dev/doc/MERGING.md @@ -109,9 +109,8 @@ There are two cases to consider: The merge script passes option `-S` to `git merge` to ensure merge commits are signed. Consequently, it depends on the GnuPG command utility being -installed and a GPG key being available. Here is a short tutorial to -creating your own GPG key: -<https://ekaia.org/blog/2009/05/10/creating-new-gpgkey/> +installed and a GPG key being available. Here is a short documentation on +how to use GPG, git & GitHub: https://help.github.com/articles/signing-commits-with-gpg/. The script depends on a few other utilities. If you are a Nix user, the simplest way of getting them is to run `nix-shell` first. diff --git a/dev/tools/check-owners-pr.sh b/dev/tools/check-owners-pr.sh new file mode 100755 index 0000000000..d2910279b5 --- /dev/null +++ b/dev/tools/check-owners-pr.sh @@ -0,0 +1,32 @@ +#!/usr/bin/env sh + +usage() { + { echo "usage: $0 PR [ARGS]..." + echo "A wrapper around check-owners.sh to check owners for a PR." + echo "Assumes upstream is the canonical Coq repository." + echo "Assumes the PR is against master." + echo + echo " PR: PR number" + echo " ARGS: passed through to check-owners.sh" + } >&2 +} + +case "$1" in + "--help"|"-h") + usage + if [ $# = 1 ]; then exit 0; else exit 1; fi;; + "") + usage + exit 1;; +esac + +PR="$1" +shift + +# this puts both refs in the FETCH_HEAD file but git rev-parse will use the first +git fetch upstream "+refs/pull/$PR/head" master + +head=$(git rev-parse FETCH_HEAD) +base=$(git merge-base upstream/master "$head") + +git diff --name-only -z "$base" "$head" | xargs -0 dev/tools/check-owners.sh "$@" diff --git a/dev/tools/check-owners.sh b/dev/tools/check-owners.sh new file mode 100755 index 0000000000..1a97508abb --- /dev/null +++ b/dev/tools/check-owners.sh @@ -0,0 +1,138 @@ +#!/usr/bin/env bash + +# Determine CODEOWNERS of the files given in argument +# For a given commit range: +# git diff --name-only -z COMMIT1 COMMIT2 | xargs -0 dev/tools/check-owners.sh [opts] + +# NB: gitignore files will be messed up if you interrupt the script. +# You should be able to just move the .gitignore.bak files back manually. + +usage() { + { echo "usage: $0 [--show-patterns] [--owner OWNER] [FILE]..." + echo " --show-patterns: instead of printing file names print the matching patterns (more compact)" + echo " --owner: show only files/patterns owned by OWNER (use Nobody to see only non-owned files)" + } >&2 +} + +case "$1" in + "--help"|"-h") + usage + if [ $# = 1 ]; then exit 0; else exit 1; fi +esac + +if ! [ -e .github/CODEOWNERS ]; then + >&2 echo "No CODEOWNERS set up or calling from wrong directory." + exit 1 +fi + +files=() +show_patterns=false + +target_owner="" + +while [[ "$#" -gt 0 ]]; do + case "$1" in + "--show-patterns") + show_patterns=true + shift;; + "--owner") + if [[ "$#" = 1 ]]; then + >&2 echo "Missing argument to --owner" + usage + exit 1 + elif [[ "$target_owner" != "" ]]; then + >&2 echo "Only one --owner allowed" + usage + exit 1 + fi + target_owner="$2" + shift 2;; + *) + files+=("$@") + break;; + esac +done + +# CODEOWNERS uses .gitignore patterns so we want to use git to parse it +# The only available tool for that is git check-ignore +# However it provides no way to use alternate .gitignore files +# so we rename them temporarily + +find . -name .gitignore -print0 | while IFS= read -r -d '' f; do + if [ -e "$f.bak" ]; then + >&2 echo "$f.bak exists!" + exit 1 + else + mv "$f" "$f.bak" + fi +done + +# CODEOWNERS is not quite .gitignore patterns: +# after the pattern is the owner (space separated) +# git would interpret that as a big pattern containing spaces +# so we create a valid .gitignore by removing all but the first field + +while read -r pat _; do + printf '%s\n' "$pat" >> .gitignore +done < .github/CODEOWNERS + +# associative array [file => owner] +declare -A owners + +for f in "${files[@]}"; do + data=$(git check-ignore --verbose --no-index "./$f") + code=$? + + if [[ "$code" = 1 ]] || ! [[ "$data" =~ .gitignore:.* ]] ; then + # no match, or match from non tracked gitignore (eg global gitignore) + if [ "$target_owner" != "" ] && [ "$target_owner" != Nobody ] ; then + owner="" + else + owner="Nobody" + pat="$f" # no patterns for unowned files + fi + else + # data looks like [.gitignore:$line:$pattern $file] + # extract the line to look it up in CODEOWNERS + data=${data#'.gitignore:'} + line=${data%%:*} + + # NB: supports multiple owners + # Does not support secondary owners declared in comment + read -r pat fowners < <(sed "${line}q;d" .github/CODEOWNERS) + + owner="" + if [ "$target_owner" != "" ]; then + for o in $fowners; do # do not quote: multiple owners possible + if [ "$o" = "$target_owner" ]; then + owner="$o" + fi + done + else + owner="$fowners" + fi + fi + + if [ "$owner" != "" ]; then + if $show_patterns; then + owners[$pat]="$owner" + else + owners[$f]="$owner" + fi + fi +done + +for f in "${!owners[@]}"; do + printf '%s: %s\n' "$f" "${owners[$f]}" +done | sort -k 2 -k 1 # group by owner + +# restore gitignore files +rm .gitignore +find . -name .gitignore.bak -print0 | while IFS= read -r -d '' f; do + base=${f%.bak} + if [ -e "$base" ]; then + >&2 echo "$base exists!" + else + mv "$f" "$base" + fi +done diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el index 62fdaec802..9dd12087a6 100644 --- a/dev/tools/coqdev.el +++ b/dev/tools/coqdev.el @@ -103,5 +103,17 @@ Note that this function is executed before _Coqproject is read if it exists." 2 (3 . 4) (5 . 6))) (add-to-list 'compilation-error-regexp-alist 'coq-backtrace)) +(defvar bug-reference-bug-regexp) +(defvar bug-reference-url-format) +(defun coqdev-setup-bug-reference-mode () + "Setup `bug-reference-bug-regexp' and `bug-reference-url-format' for Coq. + +This does not enable `bug-reference-mode'." + (let ((dir (coqdev-default-directory))) + (when dir + (setq-local bug-reference-bug-regexp "#\\(?2:[0-9]+\\)") + (setq-local bug-reference-url-format "https://github.com/coq/coq/issues/%s")))) +(add-hook 'hack-local-variables-hook #'coqdev-setup-bug-reference-mode) + (provide 'coqdev) ;;; coqdev ends here diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index f5237e4fbf..e10e16c107 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -599,6 +599,7 @@ Notice that the syntax is not completely backward compatible since the identifier was not required. .. cmd:: Add Morphism f : @ident + :name: Add Morphism The latter command also is restricted to the declaration of morphisms without parameters. It is not fully backward compatible since the @@ -616,7 +617,7 @@ the same signature. Finally, the :tacn:`replace` and :tacn:`rewrite` tactics can used to replace terms in contexts that were refused by the old implementation. As discussed in the next section, the semantics of the new :tacn:`setoid_rewrite` tactic differs slightly from the old one and -tacn:`rewrite`. +:tacn:`rewrite`. Extensions diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index 5f8c064840..152f4f6552 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -263,9 +263,12 @@ Activating the Printing of Coercions .. cmd:: Add Printing Coercion @qualid - This command forces coercion denoted by :n:`@qualid` to be printed. To skip - the printing of coercion :n:`@qualid`, use :cmd:`Remove Printing Coercion`. By - default, a coercion is never printed. + This command forces coercion denoted by :n:`@qualid` to be printed. + By default, a coercion is never printed. + +.. cmd:: Remove Printing Coercion @qualid + + Use this command, to skip the printing of coercion :n:`@qualid`. .. _coercions-classes-as-records: diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst index 009efd0d25..80ce016200 100644 --- a/doc/sphinx/addendum/omega.rst +++ b/doc/sphinx/addendum/omega.rst @@ -26,6 +26,11 @@ solvable. This is the restriction meant by "Presburger arithmetic". If the tactic cannot solve the goal, it fails with an error message. In any case, the computation eventually stops. +.. tacv:: romega + :name: romega + + To be documented. + Arithmetical goals recognized by ``omega`` ------------------------------------------ diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 8746897e75..53b993eddc 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1175,52 +1175,53 @@ component is equal ``nat`` and hence ``M1.T`` as specified. If `qualid` denotes a valid basic module (i.e. its module type is a signature), makes its components available by their short names. -.. example:: + .. example:: - .. coqtop:: reset all + .. coqtop:: reset all - Module Mod. + Module Mod. - Definition T:=nat. + Definition T:=nat. - Check T. + Check T. - End Mod. + End Mod. - Check Mod.T. + Check Mod.T. - Fail Check T. + Fail Check T. - Import Mod. + Import Mod. - Check T. + Check T. -Some features defined in modules are activated only when a module is -imported. This is for instance the case of notations (see :ref:`Notations`). + Some features defined in modules are activated only when a module is + imported. This is for instance the case of notations (see :ref:`Notations`). -Declarations made with the Local flag are never imported by theImport -command. Such declarations are only accessible through their fully -qualified name. + Declarations made with the ``Local`` flag are never imported by the :cmd:`Import` + command. Such declarations are only accessible through their fully + qualified name. -.. example:: + .. example:: - .. coqtop:: all + .. coqtop:: all - Module A. + Module A. - Module B. + Module B. - Local Definition T := nat. + Local Definition T := nat. - End B. + End B. - End A. + End A. - Import A. + Import A. - Fail Check B.T. + Fail Check B.T. .. cmdv:: Export @qualid + :name: Export When the module containing the command Export qualid is imported, qualid is imported as well. @@ -1231,16 +1232,17 @@ qualified name. .. cmd:: Print Module @ident - Prints the module type and (optionally) the body of the module `ident`. + Prints the module type and (optionally) the body of the module :n:`@ident`. .. cmd:: Print Module Type @ident - Prints the module type corresponding to `ident`. + Prints the module type corresponding to :n:`@ident`. .. opt:: Short Module Printing - This option (off by default) disables the printing of the types of fields, - leaving only their names, for the commands ``Print Module`` and ``Print Module Type``. + This option (off by default) disables the printing of the types of fields, + leaving only their names, for the commands :cmd:`Print Module` and + :cmd:`Print Module Type`. Libraries and qualified names --------------------------------- @@ -1510,9 +1512,8 @@ implicitly applied to the implicit arguments it is waiting for: one says that the implicit argument is maximally inserted. Each implicit argument can be declared to have to be inserted maximally or non -maximally. This can be governed argument per argument by the command ``Implicit -Arguments`` (see Section :ref:`declare-implicit-args`) or globally by the -:opt:`Maximal Implicit Insertion` option. +maximally. This can be governed argument per argument by the command +:cmd:`Arguments (implicits)` or globally by the :opt:`Maximal Implicit Insertion` option. See also :ref:`displaying-implicit-args`. @@ -1565,7 +1566,7 @@ absent in every situation but still be able to specify it if needed: The syntax is supported in all top-level definitions: -``Definition``, ``Fixpoint``, ``Lemma`` and so on. For (co-)inductive datatype +:cmd:`Definition`, :cmd:`Fixpoint`, :cmd:`Lemma` and so on. For (co-)inductive datatype declarations, the semantics are the following: an inductive parameter declared as an implicit argument need not be repeated in the inductive definition but will become implicit for the constructors of the diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 46e684b122..aa41f8058d 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -609,6 +609,7 @@ of any section is equivalent to using ``Local Parameter``. Adds blocks of variables with different specifications. .. cmdv:: Variables {+ ( {+ @ident } : @term) } + :name: Variables .. cmdv:: Hypothesis {+ ( {+ @ident } : @term) } :name: Hypothesis @@ -672,6 +673,7 @@ Section :ref:`typing-rules`. You have to explicitly give their fully qualified name to refer to them. .. cmdv:: Example @ident := @term + :name: Example .. cmdv:: Example @ident : @term := @term @@ -1243,37 +1245,37 @@ inhabitant of the type) is interactively built using tactics. The interactive proof mode is described in Chapter :ref:`proofhandling` and the tactics in Chapter :ref:`Tactics`. The basic assertion command is: -.. cmd:: Theorem @ident : @type +.. cmd:: Theorem @ident {? @binders } : @type -After the statement is asserted, Coq needs a proof. Once a proof of -:token:`type` under the assumptions represented by :token:`binders` is given and -validated, the proof is generalized into a proof of forall , :token:`type` and -the theorem is bound to the name :token:`ident` in the environment. + After the statement is asserted, Coq needs a proof. Once a proof of + :token:`type` under the assumptions represented by :token:`binders` is given and + validated, the proof is generalized into a proof of :n:`forall @binders, @type` and + the theorem is bound to the name :token:`ident` in the environment. -.. exn:: The term @term has type @type which should be Set, Prop or Type. + .. exn:: The term @term has type @type which should be Set, Prop or Type. -.. exn:: @ident already exists. - :name: @ident already exists. (Theorem) + .. exn:: @ident already exists. + :name: @ident already exists. (Theorem) - The name you provided is already defined. You have then to choose - another name. + The name you provided is already defined. You have then to choose + another name. -.. cmdv:: Lemma @ident : @type - :name: Lemma + The following commands are synonyms of :n:`Theorem @ident {? @binders } : type`: -.. cmdv:: Remark @ident : @type - :name: Remark + .. cmdv:: Lemma @ident {? @binders } : @type + :name: Lemma -.. cmdv:: Fact @ident : @type - :name: Fact + .. cmdv:: Remark @ident {? @binders } : @type + :name: Remark -.. cmdv:: Corollary @ident : @type - :name: Corollary + .. cmdv:: Fact @ident {? @binders } : @type + :name: Fact -.. cmdv:: Proposition @ident : @type - :name: Proposition + .. cmdv:: Corollary @ident {? @binders } : @type + :name: Corollary - These commands are synonyms of ``Theorem`` :token:`ident` : :token:`type`. + .. cmdv:: Proposition @ident {? @binders } : @type + :name: Proposition .. cmdv:: Theorem @ident : @type {* with @ident : @type} @@ -1300,13 +1302,13 @@ the theorem is bound to the name :token:`ident` in the environment. .. cmdv:: Definition @ident : @type This allows defining a term of type :token:`type` using the proof editing - mode. It behaves as Theorem but is intended to be used in conjunction with + mode. It behaves as :cmd:`Theorem` but is intended to be used in conjunction with :cmd:`Defined` in order to define a constant of which the computational behavior is relevant. The command can be used also with :cmd:`Example` instead of :cmd:`Definition`. - See also :cmd:`Opaque`, :cmd:`Transparent`, :tacn:`unfold`. + .. seealso:: :cmd:`Opaque`, :cmd:`Transparent`, :tacn:`unfold`. .. cmdv:: Let @ident : @type @@ -1326,21 +1328,14 @@ the theorem is bound to the name :token:`ident` in the environment. This generalizes the syntax of CoFixpoint so that one or more bodies can be defined interactively using the proof editing mode. -.. cmd:: Proof - - A proof starts by the keyword Proof. Then Coq enters the proof editing mode - until the proof is completed. The proof editing mode essentially contains - tactics that are described in chapter :ref:`Tactics`. Besides tactics, there - are commands to manage the proof editing mode. They are described in Chapter - :ref:`proofhandling`. - -.. cmd:: Qed - - When the proof is completed it should be validated and put in the environment - using the keyword Qed. +A proof starts by the keyword :cmd:`Proof`. Then Coq enters the proof editing mode +until the proof is completed. The proof editing mode essentially contains +tactics that are described in chapter :ref:`Tactics`. Besides tactics, there +are commands to manage the proof editing mode. They are described in Chapter +:ref:`proofhandling`. -.. exn:: @ident already exists. - :name: @ident already exists. (Qed) +When the proof is completed it should be validated and put in the environment +using the keyword :cmd:`Qed`. .. note:: @@ -1349,28 +1344,19 @@ the theorem is bound to the name :token:`ident` in the environment. #. Not only other assertions but any vernacular command can be given while in the process of proving a given assertion. In this case, the command is understood as if it would have been given before the - statements still to be proved. - - #. Proof is recommended but can currently be omitted. On the opposite - side, Qed (or Defined, see below) is mandatory to validate a proof. + statements still to be proved. Nonetheless, this practice is discouraged + and may stop working in future versions. - #. Proofs ended by Qed are declared opaque. Their content cannot be + #. Proofs ended by :cmd:`Qed` are declared opaque. Their content cannot be unfolded (see :ref:`performingcomputations`), thus realizing some form of *proof-irrelevance*. To be able to unfold a - proof, the proof should be ended by Defined (see below). - -.. cmdv:: Defined - :name: Defined - - Same as :cmd:`Qed` but the proof is then declared transparent, which means - that its content can be explicitly used for type-checking and that it can be - unfolded in conversion tactics (see :ref:`performingcomputations`, - :cmd:`Opaque`, :cmd:`Transparent`). + proof, the proof should be ended by :cmd:`Defined`. -.. cmdv:: Admitted - :name: Admitted + #. :cmd:`Proof` is recommended but can currently be omitted. On the opposite + side, :cmd:`Qed` (or :cmd:`Defined`) is mandatory to validate a proof. - Turns the current asserted statement into an axiom and exits the proof mode. + #. One can also use :cmd:`Admitted` in place of :cmd:`Qed` to turn the + current asserted statement into an axiom and exit the proof editing mode. .. [1] This is similar to the expression “*entry* :math:`\{` sep *entry* diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index c5ee724caf..2b128b98fe 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -245,7 +245,7 @@ focused goals with: :name: ... : ... (goal selector) We can also use selectors as a tactical, which allows to use them nested - in a tactic expression, by using the keyword :tacn:`only`: + in a tactic expression, by using the keyword ``only``: .. tacv:: only selector : expr :name: only ... : ... @@ -826,6 +826,7 @@ We can make pattern matching on goals using the following expression: .. we should provide the full grammar here .. tacn:: match goal with {+| {+ hyp} |- @cpattern => @expr } | _ => @expr end + :name: match goal If each hypothesis pattern :n:`hyp`\ :sub:`1,i`, with i=1,...,m\ :sub:`1` is matched (non-linear first-order unification) by an hypothesis of the diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 069cf8a6dc..892ddbc165 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -60,7 +60,6 @@ list of assertion commands is given in :ref:`Assertions`. The command used for another statement). .. cmd:: Qed - :name: Qed (interactive proof) This command is available in interactive editing proof mode when the proof is completed. Then :cmd:`Qed` extracts a proof term from the proof @@ -82,9 +81,12 @@ list of assertion commands is given in :ref:`Assertions`. The command even incur a memory overflow. .. cmdv:: Defined - :name: Defined (interactive proof) + :name: Defined - Defines the proved term as a transparent constant. + Same as :cmd:`Qed` but the proof is then declared transparent, which means + that its content can be explicitly used for type-checking and that it can be + unfolded in conversion tactics (see :ref:`performingcomputations`, + :cmd:`Opaque`, :cmd:`Transparent`). .. cmdv:: Save @ident :name: Save @@ -94,7 +96,6 @@ list of assertion commands is given in :ref:`Assertions`. The command has been opened using the :cmd:`Goal` command. .. cmd:: Admitted - :name: Admitted (interactive proof) This command is available in interactive editing mode to give up the current proof and declare the initial goal as an axiom. @@ -125,7 +126,6 @@ list of assertion commands is given in :ref:`Assertions`. The command proof term (see Section :ref:`applyingtheorems`). .. cmd:: Proof - :name: Proof (interactive proof) Is a no-op which is useful to delimit the sequence of tactic commands which start a proof, after a :cmd:`Theorem` command. It is a good practice to diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 20a362c4c6..0318bddde4 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -648,6 +648,7 @@ be applied or the goal is not head-reducible. .. exn:: @ident is already used. .. tacv:: intros + :name: intros This repeats ``intro`` until it meets the head-constant. It never reduces head-constants and it never fails. @@ -714,7 +715,7 @@ be applied or the goal is not head-reducible. These tactics behave as previously but naming the introduced hypothesis :n:`@ident`. It is equivalent to :n:`intro @ident` followed by the - appropriate call to move (see :tacn:`move ... after`). + appropriate call to ``move`` (see :tacn:`move ... after ...`). .. tacn:: intros @intro_pattern_list :name: intros ... @@ -917,7 +918,7 @@ the inverse of :tacn:`intro`. depend on it. .. tacn:: move @ident after @ident - :name: move .. after ... + :name: move ... after ... This moves the hypothesis named :n:`@ident` in the local context after the hypothesis named :n:`@ident`, where “after” is in reference to the @@ -2148,7 +2149,7 @@ See also: :ref:`advanced-recursive-functions` :n:`dependent inversion_clear @ident`. .. tacv:: dependent inversion @ident with @term - :name: dependent inversion ... + :name: dependent inversion ... with ... This variant allows you to specify the generalization of the goal. It is useful when the system fails to generalize the goal automatically. If @@ -2163,7 +2164,7 @@ See also: :ref:`advanced-recursive-functions` .. tacv:: dependent inversion_clear @ident with @term - Like :tacn:`dependent inversion ...` with but clears :n:`@ident` from the + Like :tacn:`dependent inversion ... with ...` with but clears :n:`@ident` from the local context. .. tacv:: dependent inversion_clear @ident as @intro_pattern with @term @@ -3193,7 +3194,7 @@ can solve such a goal: Goal forall P:nat -> Prop, P 0 -> exists n, P n. eauto. -Note that :tacn:`ex_intro` should be declared as a hint. +Note that ``ex_intro`` should be declared as a hint. .. tacv:: {? info_}eauto {? @num} {? using {+ @lemma}} {? with {+ @ident}} @@ -3444,6 +3445,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is Declares each :n:`@ident` as a transparent or opaque constant. .. cmdv:: Hint Extern @num {? @pattern} => tactic + :name: Hint Extern This hint type is to extend :tacn:`auto` with tactics other than :tacn:`apply` and :tacn:`unfold`. For that, we must specify a cost, an optional :n:`@pattern` and a @@ -3664,6 +3666,7 @@ option which accepts three flags allowing for a fine-grained handling of non-imported hints. .. opt:: Loose Hint Behavior %( "Lax" %| "Warn" %| "Strict" %) + :name: Loose Hint Behavior This option accepts three values, which control the behavior of hints w.r.t. :cmd:`Import`: @@ -3808,14 +3811,15 @@ some incompatibilities. .. tacv:: intuition - Is equivalent to :g:`intuition auto with *`. + Is equivalent to :g:`intuition auto with *`. .. tacv:: dintuition + :name: dintuition - While :tacn:`intuition` recognizes inductively defined connectives - isomorphic to the standard connective ``and, prod, or, sum, False, - Empty_set, unit, True``, :tacn:`dintuition` recognizes also all inductive - types with one constructors and no indices, i.e. record-style connectives. + While :tacn:`intuition` recognizes inductively defined connectives + isomorphic to the standard connective ``and``, ``prod``, ``or``, ``sum``, ``False``, + ``Empty_set``, ``unit``, ``True``, :tacn:`dintuition` recognizes also all inductive + types with one constructors and no indices, i.e. record-style connectives. .. opt:: Intuition Negation Unfolding @@ -3844,11 +3848,14 @@ first- order reasoning, written by Pierre Corbineau. It is not restricted to usual logical connectives but instead may reason about any first-order class inductive definition. -.. opt:: Firstorder Solver +.. opt:: Firstorder Solver @tactic The default tactic used by :tacn:`firstorder` when no rule applies is - :g:`auto with *`, it can be reset locally or globally using this option and - printed using :cmd:`Print Firstorder Solver`. + :g:`auto with *`, it can be reset locally or globally using this option. + + .. cmd:: Print Firstorder Solver + + Prints the default tactic used by :tacn:`firstorder` when no rule applies. .. tacv:: firstorder @tactic @@ -4011,8 +4018,8 @@ solved by :tacn:`f_equal`. :name: reflexivity This tactic applies to a goal that has the form :g:`t=u`. It checks that `t` -and `u` are convertible and then solves the goal. It is equivalent to apply -:tacn:`refl_equal`. +and `u` are convertible and then solves the goal. It is equivalent to +``apply refl_equal``. .. exn:: The conclusion is not a substitutive equation. @@ -4104,7 +4111,7 @@ symbol :g:`=`. :n:`intro @ident; simplify_eq @ident`. .. tacn:: dependent rewrite -> @ident - :name: dependent rewrite + :name: dependent rewrite -> This tactic applies to any goal. If :n:`@ident` has type :g:`(existT B a b)=(existT B a' b')` in the local context (i.e. each @@ -4115,6 +4122,7 @@ symbol :g:`=`. :tacn:`injection` and :tacn:`inversion` tactics. .. tacv:: dependent rewrite <- @ident + :name: dependent rewrite <- Analogous to :tacn:`dependent rewrite ->` but uses the equality from right to left. @@ -4374,19 +4382,20 @@ This tactics reverses the list of the focused goals. unification, or they can be called back into focus with the command :cmd:`Unshelve`. -.. tacv:: shelve_unifiable + .. tacv:: shelve_unifiable + :name: shelve_unifiable - Shelves only the goals under focus that are mentioned in other goals. - Goals that appear in the type of other goals can be solved by unification. + Shelves only the goals under focus that are mentioned in other goals. + Goals that appear in the type of other goals can be solved by unification. -.. example:: + .. example:: - .. coqtop:: all reset + .. coqtop:: all reset - Goal exists n, n=0. - refine (ex_intro _ _ _). - all:shelve_unifiable. - reflexivity. + Goal exists n, n=0. + refine (ex_intro _ _ _). + all: shelve_unifiable. + reflexivity. .. cmd:: Unshelve diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 7ba103b222..c37233734b 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -360,6 +360,7 @@ Requests to the environment Search (?x * _ + ?x * _)%Z outside OmegaLemmas. .. cmdv:: SearchAbout + :name: SearchAbout .. deprecated:: 8.5 @@ -416,7 +417,7 @@ Requests to the environment current goal (if any) and theorems of the current context whose statement’s conclusion or last hypothesis and conclusion matches the expressionterm where holes in the latter are denoted by `_`. - It is a variant of Search @term_pattern that does not look for subterms + It is a variant of :n:`Search @term_pattern` that does not look for subterms but searches for statements whose conclusion has exactly the expected form, or whose statement finishes by the given series of hypothesis/conclusion. @@ -625,6 +626,7 @@ file is a particular case of module called *library file*. .. cmdv:: Require Import @qualid + :name: Require Import This loads and declares the module :n:`@qualid` and its dependencies then imports the contents of :n:`@qualid` as described @@ -637,10 +639,11 @@ file is a particular case of module called *library file*. :cmd:`Import` :n:`@qualid` would. .. cmdv:: Require Export @qualid + :name: Require Export - This command acts as ``Require Import`` :n:`@qualid`, - but if a further module, say `A`, contains a command ``Require Export`` `B`, - then the command ``Require Import`` `A` also imports the module `B.` + This command acts as :cmd:`Require Import` :n:`@qualid`, + but if a further module, say `A`, contains a command :cmd:`Require Export` `B`, + then the command :cmd:`Require Import` `A` also imports the module `B.` .. cmdv:: Require [Import | Export] {+ @qualid } @@ -653,7 +656,7 @@ file is a particular case of module called *library file*. .. cmdv:: From @dirpath Require @qualid - This command acts as ``Require``, but picks + This command acts as :cmd:`Require`, but picks any library whose absolute name is of the form dirpath.dirpath’.qualid for some `dirpath’`. This is useful to ensure that the :n:`@qualid` library comes from a given package by making explicit its absolute root. @@ -895,6 +898,7 @@ interactively, they cannot be part of a vernacular file loaded via necessary. .. cmdv:: Backtrack @num @num @num + :name: Backtrack .. deprecated:: 8.4 @@ -1022,12 +1026,14 @@ Controlling display output, printing only identifiers. .. opt:: Printing Width @num + :name: Printing Width This command sets which left-aligned part of the width of the screen is used for display. At the time of writing this documentation, the default value is 78. .. opt:: Printing Depth @num + :name: Printing Depth This option controls the nesting depth of the formatter used for pretty- printing. Beyond this depth, display of subterms is replaced by dots. At the @@ -1208,28 +1214,29 @@ scope of their effect. There are four kinds of commands: + Commands whose default is to extend their effect both outside the section and the module or library file they occur in. For these commands, the Local modifier limits the effect of the command to the - current section or module it occurs in. As an example, the ``Coercion`` - (see Section :ref:`coercions`) and ``Strategy`` (see :ref:`here <vernac-strategy>`) - commands belong to this category. + current section or module it occurs in. As an example, the :cmd:`Coercion` + and :cmd:`Strategy` commands belong to this category. + Commands whose default behavior is to stop their effect at the end of the section they occur in but to extent their effect outside the module or library file they occur in. For these commands, the Local modifier limits the effect of the command to the current module if the command does not occur in a section and the Global modifier extends the effect outside the current sections and current module if the command occurs in a section. As an example, - the :cmd:`Implicit Arguments`, :cmd:`Ltac` or :cmd:`Notation` commands belong + the :cmd:`Arguments`, :cmd:`Ltac` or :cmd:`Notation` commands belong to this category. Notice that a subclass of these commands do not support extension of their scope outside sections at all and the Global is not applicable to them. + Commands whose default behavior is to stop their effect at the end - of the section or module they occur in. For these commands, the Global + of the section or module they occur in. For these commands, the ``Global`` modifier extends their effect outside the sections and modules they - occurs in. The ``Transparent`` and ``Opaque`` (see Section :ref:`vernac-controlling-the-reduction-strategies`) commands belong to this category. + occurs in. The :cmd:`Transparent` and :cmd:`Opaque` + (see Section :ref:`vernac-controlling-the-reduction-strategies`) commands + belong to this category. + Commands whose default behavior is to extend their effect outside sections but not outside modules when they occur in a section and to extend their effect outside the module or library file they occur in when no section contains them.For these commands, the Local modifier limits the effect to the current section or module while the Global modifier extends the effect outside the module even when the command - occurs in a section. The ``Set`` and ``Unset`` commands belong to this + occurs in a section. The :cmd:`Set` and :cmd:`Unset` commands belong to this category. diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst index e12e4d897a..682553c31b 100644 --- a/doc/sphinx/user-extensions/proof-schemes.rst +++ b/doc/sphinx/user-extensions/proof-schemes.rst @@ -26,6 +26,7 @@ induction for objects in type `identᵢ`. natural in case of inductively defined relations. .. cmdv:: Scheme Equality for @ident + :name: Scheme Equality Tries to generate a Boolean equality and a proof of the decidability of the usual equality. If `ident` involves some other inductive types, their equality has to be defined first. diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 6958b5f265..3b95a37ed3 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -916,9 +916,8 @@ Binding arguments of a constant to an interpretation scope .. seealso:: - :cmd:`About @qualid` - The command to show the scopes bound to the arguments of a - function is described in Section 2. + The command :cmd:`About` can be used to show the scopes bound to the + arguments of a function. .. note:: diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index f09ed4b55c..21093bd904 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -732,14 +732,14 @@ class CoqDomain(Domain): roles = { # Each of these roles lives in a different semantic “subdomain” - 'cmd': XRefRole(), - 'tac': XRefRole(), - 'tacn': XRefRole(), - 'opt': XRefRole(), - 'thm': XRefRole(), - 'prodn' : XRefRole(), - 'exn': XRefRole(), - 'warn': XRefRole(), + 'cmd': XRefRole(warn_dangling=True), + 'tac': XRefRole(warn_dangling=True), + 'tacn': XRefRole(warn_dangling=True), + 'opt': XRefRole(warn_dangling=True), + 'thm': XRefRole(warn_dangling=True), + 'prodn' : XRefRole(warn_dangling=True), + 'exn': XRefRole(warn_dangling=True), + 'warn': XRefRole(warn_dangling=True), # This one is special 'index': IndexXRefRole(), # These are used for highlighting diff --git a/engine/evd.ml b/engine/evd.ml index af22de5cd4..20a7c80ea0 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -842,12 +842,12 @@ let universe_rigidity evd l = else UnivRigid let normalize_universe evd = - let vars = ref (UState.subst evd.universes) in + let vars = UState.subst evd.universes in let normalize = Universes.normalize_universe_opt_subst vars in normalize let normalize_universe_instance evd l = - let vars = ref (UState.subst evd.universes) in + let vars = UState.subst evd.universes in let normalize = Universes.level_subst_of (Universes.normalize_univ_variable_opt_subst vars) in Univ.Instance.subst_fn normalize l diff --git a/engine/uState.ml b/engine/uState.ml index 6c8dbe3f44..df50bae86e 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -156,7 +156,7 @@ let process_universe_constraints ctx cstrs = let univs = ctx.uctx_universes in let vars = ref ctx.uctx_univ_variables in let weak = ref ctx.uctx_weak_constraints in - let normalize = normalize_univ_variable_opt_subst vars in + let normalize u = normalize_univ_variable_opt_subst !vars u in let nf_constraint = function | ULub (u, v) -> ULub (level_subst_of normalize u, level_subst_of normalize v) | UWeak (u, v) -> UWeak (level_subst_of normalize u, level_subst_of normalize v) diff --git a/engine/universes.ml b/engine/universes.ml index 938f5ad9cb..a13663cbad 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -605,31 +605,25 @@ let fresh_universe_context_set_instance ctx = let cst' = subst_univs_level_constraints subst cst in subst, (univs', cst') -let normalize_univ_variable ~find ~update = +let normalize_univ_variable ~find = let rec aux cur = let b = find cur in let b' = subst_univs_universe aux b in if Universe.equal b' b then b - else update cur b' + else b' in aux let normalize_univ_variable_opt_subst ectx = let find l = - match Univ.LMap.find l !ectx with + match Univ.LMap.find l ectx with | Some b -> b | None -> raise Not_found in - let update l b = - assert (match Universe.level b with Some l' -> not (Level.equal l l') | None -> true); - try ectx := Univ.LMap.add l (Some b) !ectx; b with Not_found -> assert false - in normalize_univ_variable ~find ~update + normalize_univ_variable ~find let normalize_univ_variable_subst subst = - let find l = Univ.LMap.find l !subst in - let update l b = - assert (match Universe.level b with Some l' -> not (Level.equal l l') | None -> true); - try subst := Univ.LMap.set l b !subst; b with Not_found -> assert false in - normalize_univ_variable ~find ~update + let find l = Univ.LMap.find l subst in + normalize_univ_variable ~find let normalize_universe_opt_subst subst = let normlevel = normalize_univ_variable_opt_subst subst in @@ -640,13 +634,10 @@ let normalize_universe_subst subst = subst_univs_universe normlevel let normalize_opt_subst ctx = - let ectx = ref ctx in - let normalize = normalize_univ_variable_opt_subst ectx in - let () = - Univ.LMap.iter (fun u v -> - if Option.is_empty v then () - else try ignore(normalize u) with Not_found -> assert(false)) ctx - in !ectx + let normalize = normalize_universe_opt_subst ctx in + Univ.LMap.mapi (fun u -> function + | None -> None + | Some v -> Some (normalize v)) ctx type universe_opt_subst = Universe.t option universe_map @@ -655,7 +646,7 @@ let subst_univs_fn_puniverses f (c, u as cu) = if u' == u then cu else (c, u') let nf_evars_and_universes_opt_subst f subst = - let subst = normalize_univ_variable_opt_subst (ref subst) in + let subst = normalize_univ_variable_opt_subst subst in let lsubst = level_subst_of subst in let rec aux c = match kind c with @@ -975,7 +966,7 @@ let normalize_context_set g ctx us algs weak = (* Process weak constraints: when one side is flexible and the 2 universes are unrelated unify them. *) let ctx, us, g = UPairSet.fold (fun (u,v) (ctx, us, g as acc) -> - let norm = let us = ref us in level_subst_of (normalize_univ_variable_opt_subst us) in + let norm = level_subst_of (normalize_univ_variable_opt_subst us) in let u = norm u and v = norm v in let set_to a b = (LSet.remove a ctx, @@ -994,7 +985,6 @@ let normalize_context_set g ctx us algs weak = (* Noneqs is now in canonical form w.r.t. equality constraints, and contains only inequality constraints. *) let noneqs = - let us = ref us in let norm = level_subst_of (normalize_univ_variable_opt_subst us) in Constraint.fold (fun (u,d,v) noneqs -> let u = norm u and v = norm v in diff --git a/engine/universes.mli b/engine/universes.mli index e6bee42bb3..df2e961d60 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -184,19 +184,18 @@ val normalize_univ_variables : universe_opt_subst -> val normalize_univ_variable : find:(Level.t -> Universe.t) -> - update:(Level.t -> Universe.t -> Universe.t) -> Level.t -> Universe.t -val normalize_univ_variable_opt_subst : universe_opt_subst ref -> +val normalize_univ_variable_opt_subst : universe_opt_subst -> (Level.t -> Universe.t) -val normalize_univ_variable_subst : universe_subst ref -> +val normalize_univ_variable_subst : universe_subst -> (Level.t -> Universe.t) -val normalize_universe_opt_subst : universe_opt_subst ref -> +val normalize_universe_opt_subst : universe_opt_subst -> (Universe.t -> Universe.t) -val normalize_universe_subst : universe_subst ref -> +val normalize_universe_subst : universe_subst -> (Universe.t -> Universe.t) (** Create a fresh global in the global environment, without side effects. diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index c66d69c036..d8fdfdb1bd 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -352,7 +352,6 @@ let about () = { } let handle_exn (e, info) = - let (e, info) = ExplainErr.process_vernac_interp_error (e, info) in let dummy = Stateid.dummy in let loc_of e = match Loc.get_loc e with | Some loc -> Some (Loc.unloc loc) diff --git a/interp/notation.ml b/interp/notation.ml index 20e46bfe3f..e6df7b96c9 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -1051,7 +1051,7 @@ let locate_notation prglob ntn scope = | [] -> str "Unknown notation" | _ -> str "Notation" ++ fnl () ++ - prlist (fun (ntn,l) -> + prlist_with_sep fnl (fun (ntn,l) -> let scope = find_default ntn scopes in prlist (fun (sc,r,(_,df)) -> @@ -1060,8 +1060,7 @@ let locate_notation prglob ntn scope = (if String.equal sc default_scope then mt () else (spc () ++ str ": " ++ str sc)) ++ (if Option.equal String.equal (Some sc) scope - then spc () ++ str "(default interpretation)" else mt ()) - ++ fnl ())) + then spc () ++ str "(default interpretation)" else mt ()))) l) ntns let collect_notation_in_scope scope sc known = diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 6a282624e4..b806dce0b1 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -165,15 +165,15 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc = | NApp (a,args) -> GApp (f e a, List.map (f e) args) | NList (x,y,iter,tail,swap) -> let t = f e tail in let it = f e iter in - let innerl = (ldots_var,t)::(if swap then [] else [x, lt @@ GVar y]) in + let innerl = (ldots_var,t)::(if swap then [y, lt @@ GVar x] else []) in let inner = lt @@ GApp (lt @@ GVar (ldots_var),[subst_glob_vars innerl it]) in - let outerl = (ldots_var,inner)::(if swap then [x, lt @@ GVar y] else []) in + let outerl = (ldots_var,inner)::(if swap then [] else [y, lt @@ GVar x]) in DAst.get (subst_glob_vars outerl it) | NBinderList (x,y,iter,tail,swap) -> let t = f e tail in let it = f e iter in - let innerl = (ldots_var,t)::(if swap then [] else [x, lt @@ GVar y]) in + let innerl = (ldots_var,t)::(if swap then [y, lt @@ GVar x] else []) in let inner = lt @@ GApp (lt @@ GVar ldots_var,[subst_glob_vars innerl it]) in - let outerl = (ldots_var,inner)::(if swap then [x, lt @@ GVar y] else []) in + let outerl = (ldots_var,inner)::(if swap then [] else [y, lt @@ GVar x]) in DAst.get (subst_glob_vars outerl it) | NLambda (na,ty,c) -> let e',disjpat,na = g e na in GLambda (na,Explicit,f e ty,Option.fold_right (apply_cases_pattern ?loc) disjpat (f e' c)) diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml index b6462c8106..c949589e22 100644 --- a/plugins/ltac/tactic_matching.ml +++ b/plugins/ltac/tactic_matching.ml @@ -46,7 +46,7 @@ let adjust : Constr_matching.bound_ident_map * Ltac_pretype.patvar_map -> (** Adds a binding to a {!Id.Map.t} if the identifier is [Some id] *) let id_map_try_add id x m = match id with - | Some id -> Id.Map.add id x m + | Some id -> Id.Map.add id (Lazy.force x) m | None -> m (** Adds a binding to a {!Id.Map.t} if the name is [Name id] *) diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 89d490a410..b4e1a1b102 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -427,7 +427,7 @@ let special_meta = (-1) type matching_result = { m_sub : bound_ident_map * patvar_map; - m_ctx : constr; } + m_ctx : constr Lazy.t; } let mkresult s c n = IStream.Cons ( { m_sub=s; m_ctx=c; } , (IStream.thunk n) ) @@ -451,7 +451,7 @@ let authorized_occ env sigma closed pat c mk_ctx = let subst = matches_core_closed env sigma pat c in if closed && Id.Map.exists (fun _ c -> not (closed0 sigma c)) (snd subst) then (fun next -> next ()) - else (fun next -> mkresult subst (mk_ctx (mkMeta special_meta)) next) + else (fun next -> mkresult subst (lazy (mk_ctx (mkMeta special_meta))) next) with PatternMatchingFailure -> (fun next -> next ()) let subargs env v = Array.map_to_list (fun c -> (env, c)) v diff --git a/pretyping/constr_matching.mli b/pretyping/constr_matching.mli index 3c2c73915f..d19789ef42 100644 --- a/pretyping/constr_matching.mli +++ b/pretyping/constr_matching.mli @@ -61,7 +61,7 @@ val is_matching_head : env -> Evd.evar_map -> constr_pattern -> constr -> bool (whose hole is denoted here with [special_meta]) *) type matching_result = { m_sub : bound_ident_map * patvar_map; - m_ctx : EConstr.t } + m_ctx : EConstr.t Lazy.t } (** [match_subterm pat c] returns the substitution and the context corresponding to each **closed** subterm of [c] matching [pat], diff --git a/test-suite/bugs/closed/4722.v b/test-suite/bugs/closed/4722.v deleted file mode 100644 index 2d41828f19..0000000000 --- a/test-suite/bugs/closed/4722.v +++ /dev/null @@ -1 +0,0 @@ -(* -*- coq-prog-args: ("-R" "4722" "Foo") -*- *) diff --git a/test-suite/bugs/closed/4722/tata b/test-suite/bugs/closed/4722/tata deleted file mode 120000 index b38e66e75f..0000000000 --- a/test-suite/bugs/closed/4722/tata +++ /dev/null @@ -1 +0,0 @@ -toto
\ No newline at end of file diff --git a/test-suite/misc/.gitignore b/test-suite/misc/.gitignore new file mode 100644 index 0000000000..a4083e9314 --- /dev/null +++ b/test-suite/misc/.gitignore @@ -0,0 +1,2 @@ +4722/ +4722.v diff --git a/test-suite/misc/4722.sh b/test-suite/misc/4722.sh new file mode 100755 index 0000000000..86bc50b5cd --- /dev/null +++ b/test-suite/misc/4722.sh @@ -0,0 +1,15 @@ +#!/bin/sh +set -e + +# create test files +mkdir -p misc/4722 +ln -sf toto misc/4722/tata +touch misc/4722.v + +# run test +$coqtop "-R" "misc/4722" "Foo" -top Top -load-vernac-source misc/4722.v + +# clean up test files +rm misc/4722/tata +rmdir misc/4722 +rm misc/4722.v diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index 304353f559..996af59270 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -231,3 +231,13 @@ fun l : list nat => match l with : list nat -> list nat Argument scope is [list_scope] +Notation +"'exists' x .. y , p" := ex (fun x => .. (ex (fun y => p)) ..) : type_scope +(default interpretation) +"'exists' ! x .. y , p" := ex + (unique + (fun x => .. (ex (unique (fun y => p))) ..)) +: type_scope (default interpretation) +Notation +"( x , y , .. , z )" := pair .. (pair x y) .. z : core_scope +(default interpretation) diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index d2d1369468..3cf0c913f7 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -380,3 +380,8 @@ Definition foo (l : list nat) := end. Print foo. End Issue7110. + +Module LocateNotations. +Locate "exists". +Locate "( _ , _ , .. , _ )". +End LocateNotations. |