diff options
29 files changed, 504 insertions, 652 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 6c6e4bdfcb..a7c0846e35 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -6,126 +6,101 @@ /.github/ @coq/contributing-process-maintainers /CONTRIBUTING.md @coq/contributing-process-maintainers +/dev/doc/shield-icon.png @coq/contributing-process-maintainers /dev/doc/release-process.md @coq/contributing-process-maintainers -/dev/doc/MERGING.md @coq/pushers -# This ensures that all members of the @coq/pushers -# team are notified when the merging doc changes. - ########## Build system ########## -/Makefile* @gares -/dev/tools/make_git_revision.sh @gares +/Makefile* @coq/legacy-build-maintainers +/dev/tools/make_git_revision.sh @coq/legacy-build-maintainers -/configure* @ejgallego +/configure* @coq/legacy-build-maintainers @coq/build-maintainers -/META.coq.in @ejgallego +/META.coq.in @coq/legacy-build-maintainers -/dev/build/windows @MSoegtropIMC -# Secondary maintainer @maximedenes +/dev/build/windows @coq/windows-build-maintainers ########## CI infrastructure ########## -/dev/ci/ @coq/ci-maintainers -/.travis.yml @coq/ci-maintainers -/.gitlab-ci.yml @coq/ci-maintainers -/Makefile.ci @coq/ci-maintainers -/dev/ci/nix @coq/nix-maintainers +/dev/ci/ @coq/ci-maintainers +/.travis.yml @coq/ci-maintainers +/.gitlab-ci.yml @coq/ci-maintainers +/azure-pipelines.yml @coq/ci-maintainers +/Makefile.ci @coq/ci-maintainers + +/dev/ci/nix @coq/nix-maintainers +*.nix @coq/nix-maintainers /dev/ci/user-overlays/*.sh @ghost # Trick to avoid getting review requests # each time someone adds an overlay -/dev/ci/*.bat @coq/ci-maintainers - -*.nix @coq/nix-maintainers - -azure-pipelines.yml @coq/ci-maintainers -/dev/ci/azure* @coq/ci-maintainers - ########## Documentation ########## -/README.md @Zimmi48 -# Secondary maintainer @maximedenes +/README.md @coq/doc-maintainers +/INSTALL.md @coq/doc-maintainers -/INSTALL* @Zimmi48 -# Secondary maintainer @maximedenes +/CODE_OF_CONDUCT.md @coq/code-of-conduct-team -/CODE_OF_CONDUCT.md @Zimmi48 -# Secondary maintainer @mattam82 +/doc/ @coq/doc-maintainers +/Makefile.doc @coq/doc-maintainers -/dev/doc/ @Zimmi48 -# Secondary maintainer @maximedenes +/dev/doc/ @coq/doc-maintainers +/doc/changelog/*/*.rst @ghost /dev/doc/changes.md @ghost # Trick to avoid getting review requests -# each time someone modifies the dev changelog - -/doc/ @coq/doc-maintainers -/Makefile.doc @coq/doc-maintainers +# each time someone modifies the changelog -/man/ @silene -# Secondary maintainer @maximedenes +/man/ @coq/doc-maintainers -/doc/plugin_tutorial/ @coq/plugin-tutorial-maintainers +/doc/plugin_tutorial/ @coq/plugin-tutorial-maintainers ########## Coqchk ########## -/checker/ @ppedrot -/test-suite/coqchk/ @ppedrot -# Secondary maintainers @maximedenes +/checker/ @coq/kernel-maintainers +/test-suite/coqchk/ @coq/kernel-maintainers ########## Coq lib ########## -/clib/ @ppedrot -/test-suite/unit-tests/clib/ @ppedrot -# Secondary maintainer @ejgallego - -/lib/ @ejgallego -# Secondary maintainer @ppedrot - -/lib/cWarnings.* @maximedenes -# Secondary maintainer @ejgallego +/clib/ @coq/lib-maintainers +/test-suite/unit-tests/clib/ @coq/lib-maintainers +/lib/ @coq/lib-maintainers ########## Proof engine ########## -/engine/ @ppedrot -# Secondary maintainer @aspiwack +/engine/ @coq/engine-maintainers -/engine/universes.* @SkySkimmer -/engine/univops.* @SkySkimmer -/engine/uState.* @SkySkimmer -# Secondary maintainer @mattam82 +/engine/univ* @coq/universes-maintainers +/engine/uState.* @coq/universes-maintainers ########## CoqIDE ########## -/ide/ @ppedrot -/test-suite/ide/ @ppedrot -# Secondary maintainers @gares @herbelin +/ide/ @coq/coqide-maintainers +/ide/protocol/ @coq/stm-maintainers +/test-suite/ide/ @coq/stm-maintainers -########## Interpretation ########## +########## Desugaring ########## -/interp/ @herbelin -# Secondary maintainer @ejgallego +/interp/ @coq/extensible-syntax-maintainers ########## Kernel ########## -/kernel/ @maximedenes -# Secondary maintainers @barras @ppedrot +/kernel/ @coq/kernel-maintainers -/kernel/byterun/ @maximedenes -# Secondary maintainer @silene +/kernel/byterun/ @coq/vm-native-maintainers +/kernel/native* @coq/vm-native-maintainers +/kernel/vm* @coq/vm-native-maintainers +/kernel/vconv.* @coq/vm-native-maintainers -/kernel/sorts.* @SkySkimmer -/kernel/uGraph.* @SkySkimmer -/kernel/univ.* @SkySkimmer -# Secondary maintainer @mattam82 +/kernel/sorts.* @coq/universes-maintainers +/kernel/uGraph.* @coq/universes-maintainers +/kernel/univ.* @coq/universes-maintainers ########## Library ########## -/library/ @silene -# Secondary maintainer @gares +/library/ @coq/library-maintainers ########## Parser ########## @@ -135,33 +110,26 @@ azure-pipelines.yml @coq/ci-maintainers ########## Plugins ########## -/plugins/btauto/ @ppedrot -# Secondary maintainer @herbelin +/plugins/btauto/ @coq/btauto-maintainers -/plugins/cc/ @PierreCorbineau -# Secondary maintainer @herbelin +/plugins/cc/ @coq/cc-maintainers -/plugins/derive/ @aspiwack -# Secondary maintainer @ppedrot +/plugins/derive/ @coq/derive-maintainers -/plugins/extraction/ @maximedenes +/plugins/extraction/ @coq/extraction-maintainers -/plugins/firstorder/ @PierreCorbineau -# Secondary maintainer @herbelin +/plugins/firstorder/ @coq/firstorder-maintainers -/plugins/funind/ @forestjulien -# Secondary maintainer @Matafou +/plugins/funind/ @coq/funind-maintainers -/plugins/ltac/ @ppedrot -# Secondary maintainer @herbelin +/plugins/ltac/ @coq/ltac-maintainers /plugins/micromega/ @coq/micromega-maintainers /test-suite/micromega/ @coq/micromega-maintainers -/plugins/nsatz/ @thery -# Secondary maintainer @ppedrot +/plugins/nsatz/ @coq/nsatz-maintainers -/plugins/setoid_ring/ @coq/ring-maintainers +/plugins/setoid_ring/ @coq/ring-maintainers /plugins/ssrmatching/ @coq/ssreflect-maintainers /plugins/ssr/ @coq/ssreflect-maintainers @@ -169,190 +137,101 @@ azure-pipelines.yml @coq/ci-maintainers /plugins/syntax/ @coq/parsing-maintainers -/plugins/rtauto/ @PierreCorbineau -# Secondary maintainer @herbelin +/plugins/rtauto/ @coq/rtauto-maintainers -/user-contrib/Ltac2 @ppedrot +/user-contrib/Ltac2 @coq/ltac2-maintainers ########## Pretyper ########## -/pretyping/ @mattam82 -# Secondary maintainer @gares +/pretyping/ @coq/pretyper-maintainers -/pretyping/vnorm.* @maximedenes -/pretyping/nativenorm.* @maximedenes -# Secondary maintainer @ppedrot +/pretyping/vnorm.* @coq/vm-native-maintainers +/pretyping/nativenorm.* @coq/vm-native-maintainers ########## Pretty printer ########## -/printing/ @herbelin -# Secondary maintainer @mattam82 +/printing/ @coq/extensible-syntax-maintainers ########## Proof infrastructure ########## -/proofs/ @ppedrot -# Secondary maintainer @Zimmi48 +/proofs/ @coq/engine-maintainers ########## STM ########## -/stm/ @gares -/test-suite/interactive/ @gares -/test-suite/stm/ @gares -/test-suite/vio/ @gares -# Secondary maintainer @ejgallego +/stm/ @coq/stm-maintainers +/test-suite/interactive/ @coq/stm-maintainers +/test-suite/stm/ @coq/stm-maintainers +/test-suite/vio/ @coq/stm-maintainers ########## Tactics ########## -/tactics/ @ppedrot -# Secondary maintainer @mattam82 +/tactics/ @coq/tactics-maintainers -/tactics/class_tactics.* @mattam82 -/test-suite/typeclasses/ @mattam82 -# Secondary maintainer @ppedrot +/tactics/class_tactics.* @coq/typeclasses-maintainers +/test-suite/typeclasses/ @coq/typeclasses-maintainers ########## Standard library ########## -/theories/Arith/ @herbelin - -/theories/Bool/ @herbelin - -/theories/Classes/ @mattam82 -# Secondary maintainer @herbelin - -/theories/FSets/ @herbelin - -/theories/Init/ @ppedrot - -/theories/Lists/ @ppedrot - -/theories/Logic/ @herbelin -# Secondary maintainer @ppedrot - -/theories/MSets/ @herbelin - -/theories/NArith/ @herbelin - -/theories/Numbers/ @herbelin - -/theories/PArith/ @herbelin - -/theories/Program/ @mattam82 -# Secondary maintainer @herbelin - -/theories/QArith/ @herbelin - -/theories/Reals/ @coq/reals-library-maintainers +/theories/ @coq/stdlib-maintainers -/theories/Relations/ @mattam82 -# Secondary maintainer @ppedrot +/theories/Classes/ @coq/typeclasses-maintainers -/theories/Setoids/ @mattam82 -# Secondary maintainer @ppedrot +/theories/Reals/ @coq/reals-library-maintainers -/theories/Sets/ @herbelin - -/theories/Sorting/ @herbelin - -/theories/Strings/ @herbelin - -/theories/Structures/ @herbelin - -/theories/Unicode/ @herbelin - -/theories/Wellfounded/ @mattam82 - -/theories/ZArith/ @herbelin - -/theories/Compat/ @JasonGross -# Secondary maintainer @Zimmi48 - -/theories/Vectors/ @herbelin +/theories/Compat/ @coq/compat-maintainers ########## Tools ########## -/tools/coqdoc/ @silene -/test-suite/coqdoc/ @silene -# Secondary maintainer @mattam82 +/tools/coqdoc/ @coq/coqdoc-maintainers +/test-suite/coqdoc/ @coq/coqdoc-maintainers +/tools/coqwc* @coq/coqdoc-maintainers +/test-suite/coqwc/ @coq/coqdoc-maintainers -/tools/coq_makefile* @gares -/tools/CoqMakefile* @gares -/test-suite/coq-makefile/ @gares -# Secondary maintainer @silene +/tools/coq_makefile* @coq/coq-makefile-maintainers +/tools/CoqMakefile* @coq/coq-makefile-maintainers +/test-suite/coq-makefile/ @coq/coq-makefile-maintainers -/tools/coqdep* @ppedrot -# Secondary maintainer @maximedenes +/tools/TimeFileMaker.py @coq/coq-makefile-maintainers +/tools/make-*-tim*.py @coq/coq-makefile-maintainers -/tools/coq_tex* @silene -# Secondary maintainer @gares +/tools/coqdep* @coq/legacy-build-maintainers @coq/build-maintainers -/tools/coqwc* @silene -/test-suite/coqwc/ @silene +/tools/coq_tex* @silene # Secondary maintainer @gares -/tools/TimeFileMaker.py @JasonGross -/tools/make-both-single-timing-files.py @JasonGross -/tools/make-both-time-files.py @JasonGross -/tools/make-one-time-file.py @JasonGross - ########## Toplevel ########## -/toplevel/ @ejgallego -# Secondary maintainer @gares +/toplevel/ @coq/toplevel-maintainers +/topbin/ @coq/toplevel-maintainers ########## Vernacular ########## -/vernac/ @mattam82 -# Secondary maintainer @maximedenes +/vernac/ @coq/vernac-maintainers -/vernac/metasyntax.* @coq/parsing-maintainers +/vernac/metasyntax.* @coq/parsing-maintainers -########## Test suite ########## +/vernac/classes.* @coq/typeclasses-maintainers -/test-suite/Makefile @gares -/test-suite/_CoqProject @gares -/test-suite/README.md @gares -# Secondary maintainer @SkySkimmer +########## Test suite ########## -/test-suite/report.sh @SkySkimmer +/test-suite/Makefile @coq/test-suite-maintainers +/test-suite/README.md @coq/test-suite-maintainers +/test-suite/report.sh @coq/test-suite-maintainers +/test-suite/unit-tests/src/ @coq/test-suite-maintainers /test-suite/complexity/ @herbelin -/test-suite/unit-tests/src/ @jfehrle -# Secondary maintainer @SkySkimmer - -/test-suite/success/Compat*.v @JasonGross +/test-suite/success/Compat*.v @coq/compat-maintainers ########## Developer tools ########## -/dev/tools/backport-pr.sh @Zimmi48 -# Secondary maintainer @maximedenes - -/dev/tools/change-header @herbelin - -/dev/tools/check-eof-newline.sh @SkySkimmer - -/dev/tools/coqdev.el @SkySkimmer - -/dev/tools/github-check-prs.py @SkySkimmer - -/dev/tools/make-changelog.sh @SkySkimmer -# Secondary maintainer @Zimmi48 - -/dev/tools/merge-pr.sh @maximedenes -# Secondary maintainer @gares - -/dev/tools/pre-commit @SkySkimmer - -/dev/tools/check-owners*.sh @SkySkimmer -# Secondary maintainer @maximedenes +/dev/tools/ @coq/dev-tools-maintainers -/dev/tools/update-compat.py @JasonGross -/test-suite/tools/update-compat/ @JasonGross -# Secondary maintainer @Zimmi48 +/dev/tools/update-compat.py @coq/compat-maintainers +/test-suite/tools/update-compat/ @coq/compat-maintainers ########## Dune ########## -/.ocamlinit @ejgallego -*dune* @ejgallego -*.opam @ejgallego -# Secondary maintainer @Zimmi48 +/.ocamlinit @coq/build-maintainers +*dune* @coq/build-maintainers +*.opam @coq/build-maintainers diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index f7661743a2..a0139e422d 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -42,6 +42,7 @@ well. - [Becoming a maintainer](#becoming-a-maintainer) - [Reviewing pull requests](#reviewing-pull-requests) - [Merging pull requests](#merging-pull-requests) + - [Additional notes for pull request reviewers and assignees](#additional-notes-for-pull-request-reviewers-and-assignees) - [Core development team](#core-development-team) - [Release management](#release-management) - [Packaging Coq](#packaging-coq) @@ -56,6 +57,7 @@ well. - [Git documentation, tips and tricks](#git-documentation-tips-and-tricks) - [GitHub documentation, tips and tricks](#github-documentation-tips-and-tricks) - [GitLab documentation, tips and tricks](#gitlab-documentation-tips-and-tricks) + - [Merge script dependencies](#merge-script-dependencies) - [Coqbot](#coqbot) - [Online forum and chat to talk to developers](#online-forum-and-chat-to-talk-to-developers) - [Coq remote working groups](#coq-remote-working-groups) @@ -430,7 +432,7 @@ and merge when it is the case (you can ping them if the PR is ready from your side but nothing happens for a few days). After your PR is accepted and merged, it may get backported to a -stable branch if appropriate, and will eventually make it to a +release branch if appropriate, and will eventually make it to a release. You do not have to worry about this, it is the role of the assignee and the release manager to do so (see Section [Release management](#release-management)). The milestone should give you an @@ -736,28 +738,65 @@ spending time in vain. ### Merging pull requests ### -Our [CODEOWNERS][] file associates a team of maintainers, or a -principal and secondary maintainers, to each component. They will be -responsible for self-assigning and merging PRs (they didn't co-author) -that change this component. When several components are changed in -significant ways, at least a maintainer (other than the PR author) -must approve the PR for each affected component before it can be -merged, and one of them has to assign the PR, and merge it when it is -time. Before merging, the assignee must also select a milestone for -the PR (see also Section [Release management](#release-management)). - -If you feel knowledgeable enough to maintain a component, and have a -good track record of contributing to it, we would be happy to have you -join one of the maintainer teams. - -The merging process is described in more details in [this -document][MERGING]. - -The people with merging powers (either because listed as a principal -or secondary maintainer in [CODEOWNERS][], or because member of a -maintainer team), are the members of the **@coq/pushers** team -([member list][coq-pushers] only visible to the Coq organization -members because of a limitation of GitHub). +Our [CODEOWNERS][] file associates a team of maintainers to each +component. When a PR is opened (or a draft PR is marked as ready for +review), GitHub will automatically request reviews to maintainer teams +of affected components. As soon as it is the case, one available +member of a team that was requested a review should self-assign the +PR, and will act as its shepherd from then on. + +The PR assignee is responsible for making sure that all the proposed +changes have been reviewed by relevant maintainers, that change +requests have been implemented, that CI is passing, and eventually +will be the one who merges the PR. + +*If you have already frequently contributed to a component, we would +be happy to have you join one of the maintainer teams.* + +The complete list of maintainer teams is available [here][coq-pushers] +(link only accessible to people who are already members of the Coq +organization, because of a limitation of GitHub). + +#### Additional notes for pull request reviewers and assignees #### + +- NEVER USE GITHUB'S MERGE BUTTON. Instead, we provide a script + [`dev/tools/merge-pr.sh`][merge-pr] which you should use to merge a + PR (requires having configured gpg with git). In the future, we + will also support merging through a command to **@coqbot**. + +- PR authors or co-authors cannot review, self-assign, or merge the PR + they contributed to. However, reviewers may push small fixes to the + PR branch to facilitate the PR integration. + +- Only PRs targetting the `master` branch can be merged by a + maintainer. For PRs targetting a release branch, the assignee + should always be the RM. + +- Before merging, the assignee must also select a milestone for the PR + (see also Section [Release management](#release-management)). + +- To know which files you are a maintainer of, you can look for black + shields icons in the "Files changed" tab. Alternatively, you may + use the [`dev/tools/check-owners-pr.sh`][check-owners] script for + the same purpose. + +  + +- Sometimes, it is a good practice to announce the intent to merge one + or several days in advance when unsure that everyone had a chance to + voice their opinion, or to finish reviewing the PR. + +- When a PR has [overlays][user-overlays], then: + + - the overlays that are backward-compatible (normally the case for + overlays fixing Coq code) should have been merged *before* the PR + can be merged; + + - the overlays that are not backward-compatible (normally only the + case for overlays fixing OCaml code) should be merged *just after* + the PR has been merged (and thus the assignee should ping the + maintainers of the affected projects to ask them to merge the + overlays). ### Core development team ### @@ -783,23 +822,23 @@ on the wiki. Development of new features, refactorings, deprecations and clean-ups always happens on `master`. Stabilization starts by branching -(creating a new stable `v...` branch from the current `master`), which +(creating a new `v...` release branch from the current `master`), which marks the beginning of a feature freeze (new features will continue to be merged into `master` but won't make it for the upcoming major release, but only for the next one). -After branching, most changes are introduced in the stable branch by a +After branching, most changes are introduced in the release branch by a backporting process. PR authors and assignee can signal a desire to have a PR backported by selecting an appropriate milestone. Most of the time, the choice of milestone is between two options: the next major version that has yet to branch from `master`, or the next -version (beta, final, or patch-level release) of the active stable +version (beta, final, or patch-level release) of the active release branch. In the end, it is the RM who decides whether to follow or not the recommendation of the PR assignee, and who backports PRs to the -stable branch. +release branch. -Very specific changes that are only relevant for the stable branch and -not for the `master` branch can result in a PR targetting the stable +Very specific changes that are only relevant for the release branch and +not for the `master` branch can result in a PR targetting the release branch instead of `master`. In this case, the RM is the only one who can merge the PR, and they may even do so if they are the author of the PR. Examples of such PRs include bug fixes to a feature that has @@ -808,13 +847,13 @@ number in preparation for the next release. Some automation is in place to help the RM in their task: a GitHub project is created at branching time to manage PRs to backport; when a -PR is merged in a milestone corresponding to the stable branch, our +PR is merged in a milestone corresponding to the release branch, our bot will add this PR in a "Request inclusion" column in this project; the RM can browse through the list of PRs waiting to be backported in this column, possibly reject some of them by simply removing the PR from the column (in which case, the bot will update the PR milestone), and proceed to backport others; when a backported PR is pushed to the -stable branch, the bot moves the PR from the "Request inclusion" +release branch, the bot moves the PR from the "Request inclusion" column to a "Shipped" column. More information about the RM tasks can be found in the [release @@ -914,6 +953,16 @@ procedure. We also have a benchmarking infrastructure, which is documented [on the wiki][jenkins-doc]. +##### Restarting failed jobs ##### + +When CI has a few failures which look spurious, restarting the +corresponding jobs is a good way to ensure this was indeed the case. +You can restart jobs on Azure from the "Checks" tab on GitHub. To +restart a job on GitLab CI, you should sign into GitLab (this can be +done using a GitHub account); if you are part of the [Coq organization +on GitLab](https://gitlab.com/coq), you should see a "Retry" button; +otherwise, send a request to join the organization. + #### Code owners, issue and pull request templates #### These files can be found in the [`.github`](.github) directory. The @@ -1029,6 +1078,22 @@ restart failing CI jobs. GitLab too has [extensive documentation][GitLab-doc], in particular on configuring CI. +#### Merge script dependencies #### + +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 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. + +**Note for homebrew (MacOS) users:** it has been reported that +installing GnuPG is not out of the box. Installing explicitly +`pinentry-mac` seems important for typing of passphrase to work +correctly (see also this [Stack Overflow Q-and-A][pinentry-mac]). + #### Coqbot #### Our bot sources can be found at <https://github.com/coq/bot>. Its @@ -1069,6 +1134,7 @@ can be found [on the wiki][wiki-CUDW]. [add-contributor]: https://github.com/orgs/coq/teams/contributors/members?add=true [api-doc]: https://coq.github.io/doc/master/api/ [CEP]: https://github.com/coq/ceps +[check-owners]: dev/tools/check-owners-pr.sh [CI-README-developers]: dev/ci/README-developers.md [CI-README-users]: dev/ci/README-users.md [Code-of-Conduct]: CODE_OF_CONDUCT.md @@ -1084,7 +1150,7 @@ can be found [on the wiki][wiki-CUDW]. [Coq-documentation]: https://coq.inria.fr/documentation [Coq-issue-tracker]: https://github.com/coq/coq/issues [Coq-package-index]: https://coq.inria.fr/packages -[coq-pushers]: https://github.com/orgs/coq/teams/pushers/members +[coq-pushers]: https://github.com/orgs/coq/teams/pushers/teams [coq-repository]: https://github.com/coq/coq [Coq-website-repository]: https://github.com/coq/www [debugging-doc]: dev/doc/debugging.md @@ -1118,7 +1184,7 @@ can be found [on the wiki][wiki-CUDW]. [jenkins-doc]: https://github.com/coq/coq/wiki/Jenkins-(automated-benchmarking) [kind-documentation]: https://github.com/coq/coq/issues?q=is%3Aopen+is%3Aissue+label%3A%22kind%3A+documentation%22 [master-doc]: https://coq.github.io/doc/master/refman/ -[MERGING]: dev/doc/MERGING.md +[merge-pr]: dev/tools/merge-pr.sh [needs-benchmarking]: https://github.com/coq/coq/labels/needs%3A%20benchmarking [needs-changelog]: https://github.com/coq/coq/labels/needs%3A%20changelog%20entry [needs-documentation]: https://github.com/coq/coq/labels/needs%3A%20documentation @@ -1133,6 +1199,7 @@ can be found [on the wiki][wiki-CUDW]. [Octobox]: http://octobox.io/ [old-style-guide]: dev/doc/style.txt [other-standard-libraries]: https://github.com/coq/stdlib2/wiki/Other-%22standard%22-libraries +[pinentry-mac]: https://stackoverflow.com/questions/39494631/gpg-failed-to-sign-the-data-fatal-failed-to-write-commit-object-git-2-10-0 [plugin-tutorial]: doc/plugin_tutorial [ProofGeneral-issues]: https://github.com/ProofGeneral/PG/issues [Reddit]: https://www.reddit.com/r/Coq/ diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md deleted file mode 100644 index 66f5a96802..0000000000 --- a/dev/doc/MERGING.md +++ /dev/null @@ -1,177 +0,0 @@ -# Merging changes in Coq - -This document describes how patches, submitted as pull requests (PRs) on the -`master` branch, should be merged into the main repository -(https://github.com/coq/coq). - -## Code owners - -The [CODEOWNERS](../../.github/CODEOWNERS) file defines owners for each part of -the code. Sometime there is one principal maintainer and one or several -secondary maintainer(s). Sometimes, it is a team of code owners and all of its -members act as principal maintainers for the component. - -When a PR is submitted, GitHub will automatically ask the principal -maintainer (or the code owner team) for a review. If the PR touches several -parts, all the corresponding owners will be asked for a review. - -Maintainers are never assigned as reviewer on their own PRs. - -If a principal maintainer submits a PR or is a co-author of a PR that is -submitted and this PR changes the component they own, they must request a -review from a secondary maintainer. They can also delegate the review if they -know they are not available to do it. - -## Reviewing - -When maintainers receive a review request, they are expected to: - -* Put their name in the assignee field, if they are in charge of the component - that is the main target of the patch (or if they are the only maintainer asked - to review the PR). -* Review the PR, approve it or request changes. -* If they are the assignee, check if all reviewers approved the PR. If not, - regularly ping the author (if changes should be implemented) or the reviewers - (if reviews are missing). The assignee ensures that any requests for more - discussion have been granted. When the discussion has converged and ALL - REVIEWERS(*) have approved the PR, the assignee is expected to follow the merging - process described below. - -To know what files you are a code owner of in a large PR, you can run -`dev/tools/check-owners-pr.sh xxxx`. Results are unfortunately imperfect. - -When a PR received lots of comments or if the PR has not been opened for long -and the assignee thinks that some other developers might want to comment, -it is recommended that they announce their intention to merge and wait a full -working day (or more if deemed useful) before the actual merge, as a sort of -last call for comments. - -In all cases, maintainers can delegate reviews to the other maintainers, -except if it would lead to a maintainer reviewing their own patch. - -A maintainer is expected to be reasonably reactive, but no specific timeframe is -given for reviewing. - -When none of the maintainers have commented nor self-assigned a PR in a delay -of five working days, any maintainer of another component who feels comfortable -reviewing the PR can assign it to themselves. To prevent misunderstandings, -maintainers should not hesitate to announce in advance when they shall be -unavailable for more than five working days. - -(*) In case a component is touched in a trivial way (adding/removing one file in -a `Makefile`, etc), or by applying a systematic refactoring process (global -renaming for instance) that has been reviewed globally, the assignee can -say in a comment they think a review is not required from every code owner and -proceed with the merge. - -### Breaking changes - -If the PR breaks compatibility of some external projects in CI, then fixes to -those external projects should have been prepared (cf. the relevant sub-section -in the [CI README](../ci/README.md#Breaking-changes) and the PR can be tested -with these fixes thanks to ["overlays"](../ci/user-overlays/README.md). - -Moreover the PR author *must* add an entry to the [unreleased -changelog](../../doc/changelog/README.md) or to the -[`dev/doc/changes.md`](changes.md) file. - -If overlays are missing, ask the author to prepare them and label the PR with -the [needs: overlay](https://github.com/coq/coq/labels/needs%3A%20overlay) label. - -When fixes are ready, there are two cases to consider: - -- For patches that are backward compatible (best scenario), you should get the - external project maintainers to integrate them before merging the PR. -- For patches that are not backward compatible (which is often the case when - patching plugins after an update to the Coq API), you can proceed to merge - the PR and then notify the external project maintainers they can merge the - patch. - -## Merging - -Once all reviewers approved the PR, the assignee is expected to check that CI -completed without relevant failures, and that the PR comes with appropriate -documentation and test cases. If not, they should leave a comment on the PR and -put the appropriate label. Otherwise, they are expected to merge the PR using the -[merge script](../tools/merge-pr.sh). - -When CI has a few failures which look spurious, restarting the corresponding -jobs is a good way of ensuring this was indeed the case. -To restart a job on AppVeyor, you should connect using your GitHub -account; being part of the Coq organization on GitHub should give you the -permission to do so. -To restart a job on GitLab CI, you should sign into GitLab (this can be done -using a GitHub account); if you are part of the -[Coq organization on GitLab](https://gitlab.com/coq), you should see a "Retry" -button; otherwise, send a request to join the organization. - -When the PR has conflicts, the assignee can either: -- ask the author to rebase the branch, fixing the conflicts -- warn the author that they are going to rebase the branch, and push to the - branch directly - -In both cases, CI should be run again. - -In some rare cases (e.g. the conflicts are in the `CHANGES.md` file and the PR -is not a candidate for backporting), it is ok to fix -the conflicts in the merge commit (following the same steps as below), and push -to `master` directly. DON'T USE the GitHub interface to fix these conflicts. - -To merge the PR proceed in the following way -``` -$ git checkout master -$ git pull -$ dev/tools/merge-pr.sh XXXX -$ git push upstream -``` -where `XXXX` is the number of the PR to be merged and `upstream` is the name -of your remote pointing to `git@github.com:coq/coq.git`. -Note that you are only supposed to merge PRs into `master`. PRs should rarely -target the stable branch, but when it is the case they are the responsibility -of the release manager. - -This script conducts various checks before proceeding to merge. Don't bypass them -without a good reason to, and in that case, write a comment in the PR thread to -explain the reason. - -Maintainers MUST NOT merge their own patches. - -DON'T USE the GitHub interface for merging, since it will prevent the automated -backport script from operating properly, generates bad commit messages, and a -messy history when there are conflicts. - -### Merge script dependencies - -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 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. - -**Note for homebrew (MacOS) users:** it has been reported that installing GnuPG -is not out of the box. Installing explicitly "pinentry-mac" seems important for -typing of passphrase to work correctly (see also this -[Stack Overflow Q-and-A](https://stackoverflow.com/questions/39494631/gpg-failed-to-sign-the-data-fatal-failed-to-write-commit-object-git-2-10-0)). - -## Addendum for organization admins - -### Adding a new code owner individual - -If someone is added to the [`CODEOWNERS`](../../.github/CODEOWNERS) file and -they did not have merging rights before, they should also be added to the -**@coq/pushers** team. You may do so using -[this link](https://github.com/orgs/coq/teams/pushers/members?add=true). - -Before adding someone to the **@coq/pushers** team, you should ensure that they -have read the present merging documentation, and explicitly tell them not to -use the merging button on the GitHub web interface. - -### Adding a new code owner team - -Go to [that page](https://github.com/orgs/coq/teams/pushers/teams) and click on -the green "Add a team" button. Use a "-maintainer" suffix for the name of your -team. You may then add new members to this team (you don't need to add them to -the **@coq/pushers** team first as this will be done automatically because the -team you created is a sub-team of **@coq/pushers**). diff --git a/dev/doc/shield-icon.png b/dev/doc/shield-icon.png Binary files differnew file mode 100644 index 0000000000..629e51a819 --- /dev/null +++ b/dev/doc/shield-icon.png diff --git a/doc/changelog/01-kernel/11361-fix-11360-discharge-template-param-var.rst b/doc/changelog/01-kernel/11361-fix-11360-discharge-template-param-var.rst new file mode 100644 index 0000000000..8c84648aa7 --- /dev/null +++ b/doc/changelog/01-kernel/11361-fix-11360-discharge-template-param-var.rst @@ -0,0 +1,4 @@ +- **Fixed:** `#11360 <https://github.com/issues/11360>`_ + Broken section closing when a template polymorphic inductive type depends on + a section variable through its parameters (`#11361 + <https://github.com/coq/coq/pull/11361>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/08-tools/11357-master.rst b/doc/changelog/08-tools/11357-master.rst new file mode 100644 index 0000000000..599db5b1da --- /dev/null +++ b/doc/changelog/08-tools/11357-master.rst @@ -0,0 +1,4 @@ +- **Fixed:** + ``coq_makefile`` does not break when using the ``CAMLPKGS`` variable + together with an unpacked (``mllib``) plugin. (`#11357 + <https://github.com/coq/coq/pull/11357>`_, by Gaëtan Gilbert). diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 1d0c937792..33fc211fa5 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -350,11 +350,8 @@ Changes in 8.11+beta1 `iff`. Now, it is also performed for any relation `R1` which has a ``RewriteRelation`` instance (a `RelationClasses.Reflexive` instance being also needed so :tacn:`over` can discharge the ``'Under[ _ ]`` - goal by instantiating the hidden evar.) Also, it is now possible to - manipulate `Under_rel _ R1 (f1 i) (?f2 i)` subgoals directly if `R1` - is a `PreOrder` relation or so, thanks to extra instances proving - that `Under_rel` preserves the properties of the `R1` relation. - These two features generalizing support for setoid-like relations is + goal by instantiating the hidden evar.) + This feature generalizing support for setoid-like relations is enabled as soon as we do both ``Require Import ssreflect.`` and ``Require Setoid.`` Finally, a rewrite rule ``UnderE`` has been added if one wants to "unprotect" the evar, and instantiate it diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 78428be18f..e746096df2 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1629,8 +1629,8 @@ The syntax is supported in all top-level definitions: :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 -inductive only, not the inductive type itself. For example: +definition and will become implicit for the inductive type and the constructors. +For example: .. coqtop:: all @@ -2547,3 +2547,8 @@ the context to help inferring the types of the remaining arguments. Arguments ex_intro _ _ & _ _. Check (ex_intro _ true _ : exists n : nat, n > 0). + +Coq will attempt to produce a term which uses the arguments you +provided, but in some cases involving Program mode the arguments after +the bidirectionality starts may be replaced by convertible but +syntactically different terms. diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 368724f9d2..70dadedd35 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -327,11 +327,8 @@ function on type :g:`A`). The keyword :g:`fun` can be followed by several binders as given in Section :ref:`binders`. Functions over several variables are equivalent to an iteration of one-variable functions. For instance the expression -“fun :token:`ident`\ :math:`_{1}` … :token:`ident`\ :math:`_{n}` -: :token:`type` => :token:`term`” -denotes the same function as “ fun :token:`ident`\ -:math:`_{1}` : :token:`type` => … -fun :token:`ident`\ :math:`_{n}` : :token:`type` => :token:`term`”. If +:n:`fun {+ @ident__i } : @type => @term` +denotes the same function as :n:`{+ fun @ident__i : @type => } @term`. If a let-binder occurs in the list of binders, it is expanded to a let-in definition (see Section :ref:`let-in`). @@ -362,15 +359,14 @@ the propositional implication and function types. Applications ------------ -The expression :token:`term`\ :math:`_0` :token:`term`\ :math:`_1` denotes the -application of :token:`term`\ :math:`_0` to :token:`term`\ :math:`_1`. +The expression :n:`@term__fun @term` denotes the application of +:n:`@term__fun` (which is expected to have a function type) to +:token:`term`. -The expression :token:`term`\ :math:`_0` :token:`term`\ :math:`_1` ... -:token:`term`\ :math:`_n` denotes the application of the term -:token:`term`\ :math:`_0` to the arguments :token:`term`\ :math:`_1` ... then -:token:`term`\ :math:`_n`. It is equivalent to ( … ( :token:`term`\ :math:`_0` -:token:`term`\ :math:`_1` ) … ) :token:`term`\ :math:`_n` : associativity is to the -left. +The expression :n:`@term__fun {+ @term__i }` denotes the application +of the term :n:`@term__fun` to the arguments :n:`@term__i`. It is +equivalent to :n:`( … ( @term__fun @term__1 ) … ) @term__n`: +associativity is to the left. The notation :n:`(@ident := @term)` for arguments is used for making explicit the value of implicit arguments (see diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 750ac86908..ab915e2b8d 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -379,17 +379,25 @@ let check_positivity ~chkpos kn names env_ar_par paramsctxt finite inds = (************************************************************************) (* Build the inductive packet *) -let repair_arity indices = function - | RegularArity ar -> ar.mind_user_arity - | TemplateArity ar -> mkArity (indices,Sorts.sort_of_univ ar.template_level) +let fold_arity f acc params arity indices = match arity with + | RegularArity ar -> f acc ar.mind_user_arity + | TemplateArity _ -> + let fold_ctx acc ctx = + List.fold_left (fun acc d -> + Context.Rel.Declaration.fold_constr (fun c acc -> f acc c) d acc) + acc + ctx + in + fold_ctx (fold_ctx acc params) indices -let fold_inductive_blocks f = +let fold_inductive_blocks f acc params inds = Array.fold_left (fun acc ((arity,lc),(indices,_),_) -> - f (Array.fold_left f acc lc) (repair_arity indices arity)) + fold_arity f (Array.fold_left f acc lc) params arity indices) + acc inds -let used_section_variables env inds = +let used_section_variables env params inds = let fold l c = Id.Set.union (Environ.global_vars_set env c) l in - let ids = fold_inductive_blocks fold Id.Set.empty inds in + let ids = fold_inductive_blocks fold Id.Set.empty params inds in keep_hyps env ids let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i)) @@ -461,7 +469,7 @@ let compute_projections (kn, i as ind) mib = let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite inds nmr recargs = let ntypes = Array.length inds in (* Compute the set of used section variables *) - let hyps = used_section_variables env inds in + let hyps = used_section_variables env paramsctxt inds in let nparamargs = Context.Rel.nhyps paramsctxt in (* Check one inductive *) let build_one_packet (id,cnames) ((arity,lc),(indices,splayed_lc),kelim) recarg = diff --git a/plugins/ssr/ssrsetoid.v b/plugins/ssr/ssrsetoid.v index 609c9d5ab8..7c5cd135fe 100644 --- a/plugins/ssr/ssrsetoid.v +++ b/plugins/ssr/ssrsetoid.v @@ -18,9 +18,7 @@ than [eq] or [iff], e.g. a [RewriteRelation], by doing: [Require Import ssreflect. Require Setoid.] - This file's instances have priority 12 > other stdlib instances - and each [Under_rel] instance comes with a [Hint Cut] directive - (otherwise Ring_polynom.v won't compile because of unbounded search). + This file's instances have priority 12 > other stdlib instances. (Note: this file could be skipped when porting [under] to stdlib2.) *) @@ -38,85 +36,3 @@ Instance compat_Reflexive : RelationClasses.Reflexive R -> ssrclasses.Reflexive R | 12. Proof. now trivial. Qed. - -(** Add instances so that ['Under[ F i ]] terms, - that is, [Under_rel T R (F i) (?G i)] terms, - can be manipulated with rewrite/setoid_rewrite with lemmas on [R]. - Note that this requires that [R] is a [Prop] relation, otherwise - a [bool] relation may need to be "lifted": see the [TestPreOrder] - section in test-suite/ssr/under.v *) - -Instance Under_subrelation {A} (R : relation A) : subrelation R (Under_rel _ R) | 12. -Proof. now rewrite Under_relE. Qed. - -(* see also Morphisms.trans_co_eq_inv_impl_morphism *) - -Instance Under_Reflexive {A} (R : relation A) : - RelationClasses.Reflexive R -> - RelationClasses.Reflexive (Under_rel.Under_rel A R) | 12. -Proof. now rewrite Under_rel.Under_relE. Qed. - -Hint Cut [_* Under_Reflexive Under_Reflexive] : typeclass_instances. - -(* These instances are a bit off-topic given that (Under_rel A R) will - typically be reflexive, to be able to trigger the [over] terminator - -Instance under_Irreflexive {A} (R : relation A) : - RelationClasses.Irreflexive R -> - RelationClasses.Irreflexive (Under_rel.Under_rel A R) | 12. -Proof. now rewrite Under_rel.Under_relE. Qed. - -Hint Cut [_* Under_Irreflexive Under_Irreflexive] : typeclass_instances. - -Instance under_Asymmetric {A} (R : relation A) : - RelationClasses.Asymmetric R -> - RelationClasses.Asymmetric (Under_rel.Under_rel A R) | 12. -Proof. now rewrite Under_rel.Under_relE. Qed. - -Hint Cut [_* Under_Asymmetric Under_Asymmetric] : typeclass_instances. - -Instance under_StrictOrder {A} (R : relation A) : - RelationClasses.StrictOrder R -> - RelationClasses.StrictOrder (Under_rel.Under_rel A R) | 12. -Proof. now rewrite Under_rel.Under_relE. Qed. - -Hint Cut [_* Under_Strictorder Under_Strictorder] : typeclass_instances. - *) - -Instance Under_Symmetric {A} (R : relation A) : - RelationClasses.Symmetric R -> - RelationClasses.Symmetric (Under_rel.Under_rel A R) | 12. -Proof. now rewrite Under_rel.Under_relE. Qed. - -Hint Cut [_* Under_Symmetric Under_Symmetric] : typeclass_instances. - -Instance Under_Transitive {A} (R : relation A) : - RelationClasses.Transitive R -> - RelationClasses.Transitive (Under_rel.Under_rel A R) | 12. -Proof. now rewrite Under_rel.Under_relE. Qed. - -Hint Cut [_* Under_Transitive Under_Transitive] : typeclass_instances. - -Instance Under_PreOrder {A} (R : relation A) : - RelationClasses.PreOrder R -> - RelationClasses.PreOrder (Under_rel.Under_rel A R) | 12. -Proof. now rewrite Under_rel.Under_relE. Qed. - -Hint Cut [_* Under_PreOrder Under_PreOrder] : typeclass_instances. - -Instance Under_PER {A} (R : relation A) : - RelationClasses.PER R -> - RelationClasses.PER (Under_rel.Under_rel A R) | 12. -Proof. now rewrite Under_rel.Under_relE. Qed. - -Hint Cut [_* Under_PER Under_PER] : typeclass_instances. - -Instance Under_Equivalence {A} (R : relation A) : - RelationClasses.Equivalence R -> - RelationClasses.Equivalence (Under_rel.Under_rel A R) | 12. -Proof. now rewrite Under_rel.Under_relE. Qed. - -Hint Cut [_* Under_Equivalence Under_Equivalence] : typeclass_instances. - -(* Don't handle Antisymmetric and PartialOrder classes for now, - as these classes depend on two relation symbols... *) diff --git a/pretyping/cases.ml b/pretyping/cases.ml index aa6ec1c941..cbd04a76ad 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -436,7 +436,7 @@ let adjust_tomatch_to_pattern ~program_mode sigma pb ((current,typ),deps,dep) = | exception Evarconv.UnableToUnify _ -> sigma, current | sigma -> sigma, current else - let sigma, j = Coercion.inh_conv_coerce_to ?loc ~program_mode true !!(pb.env) sigma (make_judge current typ) indt in + let sigma, j, _trace = Coercion.inh_conv_coerce_to ?loc ~program_mode true !!(pb.env) sigma (make_judge current typ) indt in sigma, j.uj_val in sigma, (current, try_find_ind !!(pb.env) sigma indt names)) @@ -1955,8 +1955,12 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign = let inh_conv_coerce_to_tycon ?loc ~program_mode env sigma j tycon = match tycon with - | Some p -> Coercion.inh_conv_coerce_to ?loc ~program_mode true env sigma - ~flags:(default_flags_of TransparentState.full) j p + | Some p -> + let (evd,v,_trace) = + Coercion.inh_conv_coerce_to ?loc ~program_mode true env sigma + ~flags:(default_flags_of TransparentState.full) j p + in + (evd,v) | None -> sigma, j (* We put the tycon inside the arity signature, possibly discovering dependencies. *) diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index c980d204ca..3c7f9a8f00 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -136,20 +136,6 @@ let lift_args n sign = in liftrec (List.length sign) sign -let mu env evdref t = - let rec aux v = - let v' = hnf env !evdref v in - match disc_subset !evdref v' with - | Some (u, p) -> - let f, ct = aux u in - let p = hnf_nodelta env !evdref p in - (Some (fun x -> - app_opt env evdref - f (papp evdref sig_proj1 [| u; p; x |])), - ct) - | None -> (None, v) - in aux t - let coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr) : (EConstr.constr -> EConstr.constr) option = @@ -367,36 +353,97 @@ let saturate_evd env evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~split:true ~fail:false env evd +type coercion_trace = + | IdCoe + | PrimProjCoe of { + proj : Projection.Repr.t; + args : econstr list; + previous : coercion_trace; + } + | Coe of { + head : econstr; + args : econstr list; + previous : coercion_trace; + } + | ProdCoe of { na : Name.t binder_annot; ty : econstr; dom : coercion_trace; body : coercion_trace } + +let empty_coercion_trace = IdCoe + +(* similar to iterated apply_coercion_args *) +let rec reapply_coercions sigma trace c = match trace with + | IdCoe -> c + | PrimProjCoe { proj; args; previous } -> + let c = reapply_coercions sigma previous c in + let args = args@[c] in + let head, args = match args with [] -> assert false | hd :: tl -> hd, tl in + applist (mkProj (Projection.make proj false, head), args) + | Coe {head; args; previous} -> + let c = reapply_coercions sigma previous c in + let args = args@[c] in + applist (head, args) + | ProdCoe { na; ty; dom; body } -> + let x = reapply_coercions sigma dom (mkRel 1) in + let c = beta_applist sigma (lift 1 c, [x]) in + let c = reapply_coercions sigma body c in + mkLambda (na, ty, c) + (* Apply coercion path from p to hj; raise NoCoercion if not applicable *) let apply_coercion env sigma p hj typ_cl = - let j,t,evd = + let j,t,trace,evd = List.fold_left - (fun (ja,typ_cl,sigma) i -> + (fun (ja,typ_cl,trace,sigma) i -> let isid = i.coe_is_identity in let isproj = i.coe_is_projection in let sigma, c = new_global sigma i.coe_value in let typ = Retyping.get_type_of env sigma c in let fv = make_judge c typ in - let argl = (class_args_of env sigma typ_cl)@[ja.uj_val] in - let sigma, jres = - apply_coercion_args env sigma true isproj argl fv + let argl = class_args_of env sigma typ_cl in + let trace = + if isid then trace + else match isproj with + | None -> Coe {head=fv.uj_val;args=argl;previous=trace} + | Some proj -> + let args = List.skipn (Projection.Repr.npars proj) argl in + PrimProjCoe {proj; args; previous=trace } in - (if isid then + let argl = argl@[ja.uj_val] in + let sigma, jres = apply_coercion_args env sigma true isproj argl fv in + let jres = + if isid then { uj_val = ja.uj_val; uj_type = jres.uj_type } else - jres), - jres.uj_type,sigma) - (hj,typ_cl,sigma) p - in evd, j + jres + in + jres, jres.uj_type, trace, sigma) + (hj,typ_cl,IdCoe,sigma) p + in evd, j, trace + +let mu env evdref t = + let rec aux v = + let v' = hnf env !evdref v in + match disc_subset !evdref v' with + | Some (u, p) -> + let f, ct, trace = aux u in + let p = hnf_nodelta env !evdref p in + let p1 = delayed_force sig_proj1 in + let evd, p1 = Evarutil.new_global !evdref p1 in + evdref := evd; + (Some (fun x -> + app_opt env evdref + f (mkApp (p1, [| u; p; x |]))), + ct, + Coe {head=p1; args=[u;p]; previous=trace}) + | None -> (None, v, IdCoe) + in aux t (* Try to coerce to a funclass; raise NoCoercion if not possible *) let inh_app_fun_core ~program_mode env evd j = let t = whd_all env evd j.uj_type in match EConstr.kind evd t with - | Prod _ -> (evd,j) + | Prod _ -> (evd,j,IdCoe) | Evar ev -> let (evd',t) = Evardefine.define_evar_as_product env evd ev in - (evd',{ uj_val = j.uj_val; uj_type = t }) + (evd',{ uj_val = j.uj_val; uj_type = t },IdCoe) | _ -> try let t,p = lookup_path_to_fun_from env evd j.uj_type in @@ -405,11 +452,11 @@ let inh_app_fun_core ~program_mode env evd j = if program_mode then try let evdref = ref evd in - let coercef, t = mu env evdref t in + let coercef, t, trace = mu env evdref t in let res = { uj_val = app_opt env evdref coercef j.uj_val; uj_type = t } in - (!evdref, res) + (!evdref, res, trace) with NoSubtacCoercion | NoCoercion -> - (evd,j) + (evd,j,IdCoe) else raise NoCoercion (* Try to coerce to a funclass; returns [j] if no coercion is applicable *) @@ -417,10 +464,10 @@ let inh_app_fun ~program_mode resolve_tc env evd j = try inh_app_fun_core ~program_mode env evd j with | NoCoercion when not resolve_tc - || not (get_use_typeclasses_for_conversion ()) -> (evd, j) + || not (get_use_typeclasses_for_conversion ()) -> (evd, j, IdCoe) | NoCoercion -> try inh_app_fun_core ~program_mode env (saturate_evd env evd) j - with NoCoercion -> (evd, j) + with NoCoercion -> (evd, j, IdCoe) let type_judgment env sigma j = match EConstr.kind sigma (whd_all env sigma j.uj_type) with @@ -430,7 +477,7 @@ let type_judgment env sigma j = let inh_tosort_force ?loc env evd j = try let t,p = lookup_path_to_sort_from env evd j.uj_type in - let evd,j1 = apply_coercion env evd p j t in + let evd,j1,_trace = apply_coercion env evd p j t in let j2 = Environ.on_judgment_type (whd_evar evd) j1 in (evd,type_judgment env evd j2) with Not_found | NoCoercion -> @@ -449,7 +496,7 @@ let inh_coerce_to_sort ?loc env evd j = let inh_coerce_to_base ?loc ~program_mode env evd j = if program_mode then let evdref = ref evd in - let ct, typ' = mu env evdref j.uj_type in + let ct, typ', trace = mu env evdref j.uj_type in let res = { uj_val = (app_coercion env evdref ct j.uj_val); uj_type = typ' } @@ -459,7 +506,7 @@ let inh_coerce_to_base ?loc ~program_mode env evd j = let inh_coerce_to_prod ?loc ~program_mode env evd t = if program_mode then let evdref = ref evd in - let _, typ' = mu env evdref t in + let _, typ', _trace = mu env evdref t in !evdref, typ' else (evd, t) @@ -468,24 +515,24 @@ let inh_coerce_to_fail flags env evd rigidonly v t c1 = then raise NoCoercion else - let evd, v', t' = + let evd, v', t', trace = try let t2,t1,p = lookup_path_between env evd (t,c1) in - let evd,j = + let evd,j,trace = apply_coercion env evd p {uj_val = v; uj_type = t} t2 in - evd, j.uj_val, j.uj_type + evd, j.uj_val, j.uj_type, trace with Not_found -> raise NoCoercion in - try (unify_leq_delay ~flags env evd t' c1, v') + try (unify_leq_delay ~flags env evd t' c1, v', trace) with UnableToUnify _ -> raise NoCoercion let default_flags_of env = default_flags_of TransparentState.full let rec inh_conv_coerce_to_fail ?loc env evd ?(flags=default_flags_of env) rigidonly v t c1 = - try (unify_leq_delay ~flags env evd t c1, v) + try (unify_leq_delay ~flags env evd t c1, v, IdCoe) with UnableToUnify (best_failed_evd,e) -> try inh_coerce_to_fail flags env evd rigidonly v t c1 with NoCoercion -> @@ -505,24 +552,27 @@ let rec inh_conv_coerce_to_fail ?loc env evd ?(flags=default_flags_of env) rigid | na -> na) name in let open Context.Rel.Declaration in let env1 = push_rel (LocalAssum (name,u1)) env in - let (evd', v1) = + let (evd', v1, trace1) = inh_conv_coerce_to_fail ?loc env1 evd rigidonly (mkRel 1) (lift 1 u1) (lift 1 t1) in let v2 = beta_applist evd' (lift 1 v,[v1]) in let t2 = Retyping.get_type_of env1 evd' v2 in - let (evd'',v2') = inh_conv_coerce_to_fail ?loc env1 evd' rigidonly v2 t2 u2 in - (evd'', mkLambda (name, u1, v2')) + let (evd'',v2',trace2) = inh_conv_coerce_to_fail ?loc env1 evd' rigidonly v2 t2 u2 in + let trace = ProdCoe { na=name; ty=u1; dom=trace1; body=trace2 } in + (evd'', mkLambda (name, u1, v2'), trace) | _ -> raise (NoCoercionNoUnifier (best_failed_evd,e)) (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *) let inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc rigidonly flags env evd cj t = - let (evd', val') = + let (evd', val', otrace) = try - inh_conv_coerce_to_fail ?loc env evd ~flags rigidonly cj.uj_val cj.uj_type t + let (evd', val', trace) = inh_conv_coerce_to_fail ?loc env evd ~flags rigidonly cj.uj_val cj.uj_type t in + (evd', val', Some trace) with NoCoercionNoUnifier (best_failed_evd,e) -> try if program_mode then - coerce_itf ?loc env evd cj.uj_val cj.uj_type t + let (evd', val') = coerce_itf ?loc env evd cj.uj_val cj.uj_type t in + (evd', val', None) else raise NoSubtacCoercion with | NoSubtacCoercion when not resolve_tc || not (get_use_typeclasses_for_conversion ()) -> @@ -533,11 +583,12 @@ let inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc rigidonly flags env evd if evd' == evd then error_actual_type ?loc env best_failed_evd cj t e else - inh_conv_coerce_to_fail ?loc env evd' rigidonly cj.uj_val cj.uj_type t + let (evd', val', trace) = inh_conv_coerce_to_fail ?loc env evd' rigidonly cj.uj_val cj.uj_type t in + (evd', val', Some trace) with NoCoercionNoUnifier (_evd,_error) -> error_actual_type ?loc env best_failed_evd cj t e in - (evd',{ uj_val = val'; uj_type = t }) + (evd',{ uj_val = val'; uj_type = t },otrace) let inh_conv_coerce_to ?loc ~program_mode resolve_tc env evd ?(flags=default_flags_of env) = inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc false flags env evd diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli index fe93a26f4f..b92f3709cc 100644 --- a/pretyping/coercion.mli +++ b/pretyping/coercion.mli @@ -16,13 +16,19 @@ open Glob_term (** {6 Coercions. } *) +type coercion_trace + +val empty_coercion_trace : coercion_trace + +val reapply_coercions : evar_map -> coercion_trace -> EConstr.t -> EConstr.t + (** [inh_app_fun resolve_tc env isevars j] coerces [j] to a function; i.e. it inserts a coercion into [j], if needed, in such a way it gets as type a product; it returns [j] if no coercion is applicable. resolve_tc=false disables resolving type classes (as the last resort before failing) *) val inh_app_fun : program_mode:bool -> bool -> - env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment + env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment * coercion_trace (** [inh_coerce_to_sort env isevars j] coerces [j] to a type; i.e. it inserts a coercion into [j], if needed, in such a way it gets as @@ -48,11 +54,11 @@ val inh_coerce_to_prod : ?loc:Loc.t -> program_mode:bool -> val inh_conv_coerce_to : ?loc:Loc.t -> program_mode:bool -> bool -> env -> evar_map -> ?flags:Evarconv.unify_flags -> - unsafe_judgment -> types -> evar_map * unsafe_judgment + unsafe_judgment -> types -> evar_map * unsafe_judgment * coercion_trace option val inh_conv_coerce_rigid_to : ?loc:Loc.t -> program_mode:bool ->bool -> env -> evar_map -> ?flags:Evarconv.unify_flags -> - unsafe_judgment -> types -> evar_map * unsafe_judgment + unsafe_judgment -> types -> evar_map * unsafe_judgment * coercion_trace option (** [inh_pattern_coerce_to loc env isevars pat ind1 ind2] coerces the Cases pattern [pat] typed in [ind1] into a pattern typed in [ind2]; diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index bfdb471c46..bf61d44a10 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -361,7 +361,7 @@ let adjust_evar_source sigma na c = (* coerce to tycon if any *) let inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma j = function - | None -> sigma, j + | None -> sigma, j, Some Coercion.empty_coercion_trace | Some t -> Coercion.inh_conv_coerce_to ?loc ~program_mode resolve_tc !!env sigma j t @@ -604,16 +604,18 @@ let pretype_instance self ~program_mode ~poly resolve_tc env sigma loc hyps evk module Default = struct + let discard_trace (sigma,t,otrace) = sigma, t + let pretype_ref self (ref, u) = fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> let sigma, t_ref = pretype_ref ?loc sigma env ref u in - inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma t_ref tycon + discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma t_ref tycon let pretype_var self id = fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> let pretype tycon env sigma t = eval_pretyper self ~program_mode ~poly resolve_tc tycon env sigma t in let sigma, t_id = pretype_id (fun e r t -> pretype tycon e r t) loc env sigma id in - inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma t_id tycon + discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma t_id tycon let pretype_evar self (id, inst) ?loc ~program_mode ~poly resolve_tc tycon env sigma = (* Ne faudrait-il pas s'assurer que hyps est bien un @@ -626,7 +628,7 @@ struct let sigma, args = pretype_instance self ~program_mode ~poly resolve_tc env sigma loc hyps evk inst in let c = mkEvar (evk, args) in let j = Retyping.get_judgment_of !!env sigma c in - inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma j tycon + discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma j tycon let pretype_patvar self kind ?loc ~program_mode ~poly resolve_tc tycon env sigma = let sigma, ty = @@ -757,12 +759,12 @@ struct iraise (e, info)); make_judge (mkCoFix cofix) ftys.(i) in - inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma fixj tycon + discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma fixj tycon let pretype_sort self s = fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> let sigma, j = pretype_sort ?loc sigma s in - inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma j tycon + discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma j tycon let pretype_app self (f, args) = fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> @@ -771,12 +773,15 @@ struct let floc = loc_of_glob_constr f in let length = List.length args in let nargs_before_bidi = + if Option.is_empty tycon then length + (* We apply bidirectionality hints only if an expected type is specified *) + else (* if `f` is a global, we retrieve bidirectionality hints *) - try - let (gr,_) = destRef sigma fj.uj_val in - Option.default length @@ GlobRef.Map.find_opt gr !bidi_hints - with DestKO -> - length + try + let (gr,_) = destRef sigma fj.uj_val in + Option.default length @@ GlobRef.Map.find_opt gr !bidi_hints + with DestKO -> + length in let candargs = (* Bidirectional typechecking hint: @@ -813,24 +818,38 @@ struct else fun f v -> applist (f, [v]) | _ -> fun _ f v -> applist (f, [v]) in - let rec apply_rec env sigma n resj candargs bidiargs = function - | [] -> sigma, resj, List.rev bidiargs + let refresh_template env sigma resj = + (* Special case for inductive type applications that must be + refreshed right away. *) + match EConstr.kind sigma resj.uj_val with + | App (f,args) -> + if Termops.is_template_polymorphic_ind !!env sigma f then + let c = mkApp (f, args) in + let sigma, c = Evarsolve.refresh_universes (Some true) !!env sigma c in + let t = Retyping.get_type_of !!env sigma c in + sigma, make_judge c (* use this for keeping evars: resj.uj_val *) t + else sigma, resj + | _ -> sigma, resj + in + let rec apply_rec env sigma n resj resj_before_bidi candargs bidiargs = function + | [] -> sigma, resj, resj_before_bidi, List.rev bidiargs | c::rest -> let bidi = n >= nargs_before_bidi in let argloc = loc_of_glob_constr c in - let sigma, resj = Coercion.inh_app_fun ~program_mode resolve_tc !!env sigma resj in + let sigma, resj, trace = Coercion.inh_app_fun ~program_mode resolve_tc !!env sigma resj in let resty = whd_all !!env sigma resj.uj_type in match EConstr.kind sigma resty with | Prod (na,c1,c2) -> - let tycon = Some c1 in let (sigma, hj), bidiargs = - if bidi && Option.has_some tycon then + if bidi then (* We want to get some typing information from the context before typing the argument, so we replace it by an existential variable *) let sigma, c_hole = new_evar env sigma ~src:(loc,Evar_kinds.InternalHole) c1 in - (sigma, make_judge c_hole c1), (c_hole, c) :: bidiargs - else pretype tycon env sigma c, bidiargs + (sigma, make_judge c_hole c1), (c_hole, c, trace) :: bidiargs + else + let tycon = Some c1 in + pretype tycon env sigma c, bidiargs in let sigma, candargs, ujval = match candargs with @@ -845,29 +864,18 @@ struct in let sigma, ujval = adjust_evar_source sigma na.binder_name ujval in let value, typ = app_f n (j_val resj) ujval, subst1 ujval c2 in - let j = { uj_val = value; uj_type = typ } in - apply_rec env sigma (n+1) j candargs bidiargs rest + let resj = { uj_val = value; uj_type = typ } in + let resj_before_bidi = if bidi then resj_before_bidi else resj in + apply_rec env sigma (n+1) resj resj_before_bidi candargs bidiargs rest | _ -> let sigma, hj = pretype empty_tycon env sigma c in error_cant_apply_not_functional ?loc:(Loc.merge_opt floc argloc) !!env sigma resj [|hj|] in - let sigma, resj, bidiargs = apply_rec env sigma 0 fj candargs [] args in - let sigma, resj = - match EConstr.kind sigma resj.uj_val with - | App (f,args) -> - if Termops.is_template_polymorphic_ind !!env sigma f then - (* Special case for inductive type applications that must be - refreshed right away. *) - let c = mkApp (f, args) in - let sigma, c = Evarsolve.refresh_universes (Some true) !!env sigma c in - let t = Retyping.get_type_of !!env sigma c in - sigma, make_judge c (* use this for keeping evars: resj.uj_val *) t - else sigma, resj - | _ -> sigma, resj - in - let sigma, t = inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon in - let refine_arg sigma (newarg,origarg) = + let sigma, resj, resj_before_bidi, bidiargs = apply_rec env sigma 0 fj fj candargs [] args in + let sigma, resj = refresh_template env sigma resj in + let sigma, resj, otrace = inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon in + let refine_arg n (sigma,t) (newarg,origarg,trace) = (* Refine an argument (originally `origarg`) represented by an evar (`newarg`) to use typing information from the context *) (* Recover the expected type of the argument *) @@ -876,12 +884,25 @@ struct let sigma, j = pretype (Some ty) env sigma origarg in (* Unify the (possibly refined) existential variable with the (typechecked) original value *) - Evarconv.unify_delay !!env sigma newarg (j_val j) + let sigma = Evarconv.unify_delay !!env sigma newarg (j_val j) in + sigma, app_f n (Coercion.reapply_coercions sigma trace t) (j_val j) in (* We now refine any arguments whose typing was delayed for bidirectionality *) - let sigma = List.fold_left refine_arg sigma bidiargs in - (sigma, t) + let t = resj_before_bidi.uj_val in + let sigma, t = List.fold_left_i refine_arg nargs_before_bidi (sigma,t) bidiargs in + (* If we did not get a coercion trace (e.g. with `Program` coercions, we + replaced user-provided arguments with inferred ones. Otherwise, we apply + the coercion trace to the user-provided arguments. *) + let resj = + match otrace with + | None -> resj + | Some trace -> + let resj = { resj with uj_val = t } in + let sigma, resj = refresh_template env sigma resj in + { resj with uj_val = Coercion.reapply_coercions sigma trace t } + in + (sigma, resj) let pretype_lambda self (name, bk, c1, c2) = fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> @@ -903,7 +924,7 @@ struct let sigma, j' = eval_pretyper self ~program_mode ~poly resolve_tc rng env' sigma c2 in let name = get_name var' in let resj = judge_of_abstraction !!env (orelse_name name name'.binder_name) j j' in - inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon + discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon let pretype_prod self (name, bk, c1, c2) = fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> @@ -929,7 +950,7 @@ struct let (e, info) = CErrors.push e in let info = Option.cata (Loc.add_loc info) info loc in iraise (e, info) in - inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon + discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon let pretype_letin self (name, c1, t, c2) = fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> @@ -1122,7 +1143,7 @@ struct mkCase (ci, pred, cj.uj_val, [|b1;b2|]) in let cj = { uj_val = v; uj_type = p } in - inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma cj tycon + discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma cj tycon let pretype_cast self (c, k) = fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> @@ -1165,7 +1186,7 @@ struct in let v = mkCast (cj.uj_val, k, tval) in sigma, { uj_val = v; uj_type = tval } - in inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma cj tycon + in discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma cj tycon let pretype_int self i = fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> @@ -1174,7 +1195,7 @@ struct with Invalid_argument _ -> user_err ?loc ~hdr:"pretype" (str "Type of int63 should be registered first.") in - inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon + discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon let pretype_float self f = fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> @@ -1183,7 +1204,7 @@ struct with Invalid_argument _ -> user_err ?loc ~hdr:"pretype" (str "Type of float should be registered first.") in - inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon + discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon (* [pretype_type valcon env sigma c] coerces [c] into a type *) let pretype_type self c ?loc ~program_mode ~poly resolve_tc valcon (env : GlobEnv.t) sigma = match DAst.get c with diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 48d5fac321..6486435ca2 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1290,7 +1290,7 @@ let is_mimick_head sigma ts f = let try_to_coerce env evd c cty tycon = let j = make_judge c cty in - let (evd',j') = inh_conv_coerce_rigid_to ~program_mode:false true env evd j tycon in + let (evd',j',_trace) = inh_conv_coerce_rigid_to ~program_mode:false true env evd j tycon in let evd' = Evarconv.solve_unif_constraints_with_heuristics env evd' in let evd' = Evd.map_metas_fvalue (fun c -> nf_evar evd' c) evd' in (evd',j'.uj_val) diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 58c0f7db53..e466992721 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -678,7 +678,7 @@ let define_with_type sigma env ev c = let t = Retyping.get_type_of env sigma ev in let ty = Retyping.get_type_of env sigma c in let j = Environ.make_judge c ty in - let (sigma, j) = Coercion.inh_conv_coerce_to ~program_mode:false true env sigma j t in + let (sigma, j, _trace) = Coercion.inh_conv_coerce_to ~program_mode:false true env sigma j t in let (ev, _) = destEvar sigma ev in let sigma = Evd.define ev j.Environ.uj_val sigma in sigma diff --git a/test-suite/Makefile b/test-suite/Makefile index b3a633e528..1d21b4b5e0 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -530,14 +530,16 @@ $(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v $(PREREQUISITELOG) $(HIDE){ \ echo $(call log_intro,$<); \ true "extract effective user time"; \ - res=`$(coqc_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 | sed -n -e "s/Finished transaction in .*(\([0-9]*\.[0-9]*\)u.*)/\1/p" | head -1 | sed "s/\r//g"`; \ + res=`$(coqc_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 | sed -n -e "s/Finished .*transaction in .*(\([0-9]*\.[0-9]*\)u.*)/\1/p" | head -1 | sed "s/\r//g"`; \ R=$$?; times; \ if [ $$R != 0 ]; then \ echo $(log_failure); \ echo " $<...Error! (should be accepted)" ; \ + $(FAIL); \ elif [ "$$res" = "" ]; then \ echo $(log_failure); \ echo " $<...Error! (couldn't find a time measure)"; \ + $(FAIL); \ else \ true "express effective time in centiseconds"; \ resorig="$$res"; \ diff --git a/test-suite/bugs/bug_11140.v b/test-suite/bugs/bug_11140.v new file mode 100644 index 0000000000..ca806ea324 --- /dev/null +++ b/test-suite/bugs/bug_11140.v @@ -0,0 +1,11 @@ +Axiom T : nat -> Prop. +Axiom f : forall x, T x. +Arguments f & x. + +Lemma test : (f (1 + _) : T 2) = f 2. +match goal with +| |- (f (1 + 1) = f 2) => idtac +| |- (f 2 = f 2) => fail (* Issue 11140 *) +| |- _ => fail +end. +Abort. diff --git a/test-suite/bugs/closed/bug_11360.v b/test-suite/bugs/closed/bug_11360.v new file mode 100644 index 0000000000..d8bc4a9f02 --- /dev/null +++ b/test-suite/bugs/closed/bug_11360.v @@ -0,0 +1,6 @@ +Section S. + Variable (A:Type). + #[universes(template)] + Inductive bar (d:A) := . +End S. +Check bar nat 0. diff --git a/test-suite/coq-makefile/findlib-package-unpacked/Makefile.local b/test-suite/coq-makefile/findlib-package-unpacked/Makefile.local new file mode 100644 index 0000000000..0f4a7d9954 --- /dev/null +++ b/test-suite/coq-makefile/findlib-package-unpacked/Makefile.local @@ -0,0 +1 @@ +CAMLPKGS += -package foo diff --git a/test-suite/coq-makefile/findlib-package-unpacked/_CoqProject b/test-suite/coq-makefile/findlib-package-unpacked/_CoqProject new file mode 100644 index 0000000000..cbdb43f842 --- /dev/null +++ b/test-suite/coq-makefile/findlib-package-unpacked/_CoqProject @@ -0,0 +1,10 @@ +-R src test +-R theories test +-I src + +src/test_plugin.mllib +src/test.mlg +src/test.mli +src/test_aux.ml +src/test_aux.mli +theories/test.v diff --git a/test-suite/coq-makefile/findlib-package-unpacked/findlib/foo/META b/test-suite/coq-makefile/findlib-package-unpacked/findlib/foo/META new file mode 100644 index 0000000000..ff5f1c7c96 --- /dev/null +++ b/test-suite/coq-makefile/findlib-package-unpacked/findlib/foo/META @@ -0,0 +1,4 @@ +archive(byte)="foo.cma" +archive(native)="foo.cmxa" +linkopts="-linkall" +requires="str" diff --git a/test-suite/coq-makefile/findlib-package-unpacked/findlib/foo/Makefile b/test-suite/coq-makefile/findlib-package-unpacked/findlib/foo/Makefile new file mode 100644 index 0000000000..1615bfd067 --- /dev/null +++ b/test-suite/coq-makefile/findlib-package-unpacked/findlib/foo/Makefile @@ -0,0 +1,14 @@ +-include ../../Makefile.conf + +CO="$(COQMF_OCAMLFIND)" opt +CB="$(COQMF_OCAMLFIND)" ocamlc + +all: + $(CO) -c foolib.ml + $(CO) -a foolib.cmx -o foo.cmxa + $(CB) -c foolib.ml + $(CB) -a foolib.cmo -o foo.cma + $(CB) -c foo.mli # empty .mli file, to be understood + +clean: + rm -f *.cmo *.cma *.cmx *.cmxa *.cmi *.o *.a diff --git a/test-suite/coq-makefile/findlib-package-unpacked/findlib/foo/foo.mli b/test-suite/coq-makefile/findlib-package-unpacked/findlib/foo/foo.mli new file mode 100644 index 0000000000..e69de29bb2 --- /dev/null +++ b/test-suite/coq-makefile/findlib-package-unpacked/findlib/foo/foo.mli diff --git a/test-suite/coq-makefile/findlib-package-unpacked/findlib/foo/foolib.ml b/test-suite/coq-makefile/findlib-package-unpacked/findlib/foo/foolib.ml new file mode 100644 index 0000000000..81306fb89b --- /dev/null +++ b/test-suite/coq-makefile/findlib-package-unpacked/findlib/foo/foolib.ml @@ -0,0 +1,2 @@ +let foo () = + assert(Str.search_forward (Str.regexp "foo") "barfoobar" 0 = 3) diff --git a/test-suite/coq-makefile/findlib-package-unpacked/run.sh b/test-suite/coq-makefile/findlib-package-unpacked/run.sh new file mode 100755 index 0000000000..e53a7ed0f7 --- /dev/null +++ b/test-suite/coq-makefile/findlib-package-unpacked/run.sh @@ -0,0 +1,20 @@ +#!/usr/bin/env bash + +. ../template/init.sh +mv src/test_plugin.mlpack src/test_plugin.mllib + +echo "let () = Foolib.foo ();;" >> src/test_aux.ml +export OCAMLPATH=$OCAMLPATH:$PWD/findlib +if which cygpath 2>/dev/null; then + # the only way I found to pass OCAMLPATH on win is to have it contain + # only one entry + OCAMLPATH=$(cygpath -w "$PWD"/findlib) + export OCAMLPATH +fi +make -C findlib/foo clean +coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf +cat Makefile.local +make -C findlib/foo +make +make byte diff --git a/test-suite/ssr/under.v b/test-suite/ssr/under.v index c12491138a..0312b9c733 100644 --- a/test-suite/ssr/under.v +++ b/test-suite/ssr/under.v @@ -313,8 +313,7 @@ Qed. End TestGeneric2. Section TestPreOrder. -(* inspired by https://github.com/coq/coq/pull/10022#issuecomment-530101950 - but without needing to do [rewrite UnderE] manually. *) +(* inspired by https://github.com/coq/coq/pull/10022#issuecomment-530101950 *) Require Import Morphisms. @@ -330,7 +329,7 @@ Parameter leq_mul : Local Notation "+%N" := addn (at level 0, only parsing). -(** Context lemma (could *) +(** Context lemma *) Lemma leq'_big : forall I (F G : I -> nat) (r : seq I), (forall i : I, leq' (F i) (G i)) -> (leq' (\big[+%N/0%N]_(i <- r) F i) (\big[+%N/0%N]_(i <- r) G i)). @@ -370,8 +369,10 @@ have lem : forall (i : nat), i < n -> leq' (3 + i) (3 + n). under leq'_big => i. { - (* The "magic" is here: instantiate the evar with the bound "3 + n" *) - rewrite lem ?ltn_ord //. over. + rewrite UnderE. + + (* instantiate the evar with the bound "3 + n" *) + apply: lem; exact: ltn_ord. } cbv beta. diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 7c53ecfe18..7cd5962d86 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -632,7 +632,7 @@ $(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib $(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib $(SHOW)'CAMLOPT -a -o $@' - $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^ + $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $^ $(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmxa |
