diff options
29 files changed, 468 insertions, 142 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 70f67a8845..2ca8274929 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -344,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 2f5a000169..095099690b 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/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/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/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..39735a6eda 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 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/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/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/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. |