diff options
| -rw-r--r-- | .circleci/config.yml | 40 | ||||
| -rw-r--r-- | .github/CODEOWNERS | 13 | ||||
| -rw-r--r-- | .gitlab-ci.yml | 28 | ||||
| -rw-r--r-- | CONTRIBUTING.md | 8 | ||||
| -rw-r--r-- | Makefile.doc | 6 | ||||
| -rw-r--r-- | README.md | 1 | ||||
| -rw-r--r-- | appveyor.yml | 12 | ||||
| -rw-r--r-- | dev/build/windows/makecoq_mingw.sh | 4 | ||||
| -rw-r--r-- | dev/ci/README.md | 77 | ||||
| -rw-r--r-- | dev/ci/gitlab.bat | 50 | ||||
| -rwxr-xr-x | dev/tools/check-owners-pr.sh | 32 | ||||
| -rwxr-xr-x | dev/tools/check-owners.sh | 138 | ||||
| -rw-r--r-- | dev/tools/coqdev.el | 12 | ||||
| -rw-r--r-- | ide/ide_slave.ml | 1 | ||||
| -rw-r--r-- | interp/notation.ml | 5 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 8 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4722.v | 1 | ||||
| l--------- | test-suite/bugs/closed/4722/tata | 1 | ||||
| -rw-r--r-- | test-suite/misc/.gitignore | 2 | ||||
| -rwxr-xr-x | test-suite/misc/4722.sh | 15 | ||||
| -rw-r--r-- | test-suite/output/Notations3.out | 10 | ||||
| -rw-r--r-- | test-suite/output/Notations3.v | 5 |
22 files changed, 388 insertions, 81 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 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/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/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/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/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. |