diff options
65 files changed, 1912 insertions, 971 deletions
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 0d11d092ba..529a912bb6 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -1,37 +1,282 @@ -# Contributing to Coq +# Guide to contributing to Coq # -Thank you for your interest in contributing to Coq! There are many ways to -contribute, and we appreciate all of them. Please make sure you read and -abide by the [Code of Conduct](CODE_OF_CONDUCT.md). +## Foreword ## -## Bug Reports +As with any documentation, this guide is most useful if it's promptly +updated to reflect changes in processes, development tools, or the Coq +ecosystem. If you notice anything inaccurate or outdated, please +signal it in a new issue, or fix it in a new pull request. If you +find some parts are not sufficiently clear, you may open an issue as +well. -Bug reports are enormously useful to identify issues with Coq; we can't fix -what we don't know about. To report a bug, please open an issue in the -[Coq issue tracker][] (you'll need a GitHub -account). You can file a bug for any of the following: +## Table of contents ## -- An anomaly. These are always considered bugs, so Coq will even ask you to - file a bug report! +- [Introduction](#introduction) +- [Contributing to the ecosystem](#contributing-to-the-ecosystem) + - [Asking and answering questions](#asking-and-answering-questions) + - [Writing tutorials and blog posts](#writing-tutorials-and-blog-posts) + - [Contributing to the wiki](#contributing-to-the-wiki) + - [Creating and maintaining Coq packages](#creating-and-maintaining-coq-packages) + - [Distribution](#distribution) + - [Support](#support) + - [Standard libraries](#standard-libraries) + - [Maintaining existing packages in coq-community](#maintaining-existing-packages-in-coq-community) + - [Contributing to the website or the package archive](#contributing-to-the-website-or-the-package-archive) + - [Other ways of creating content](#other-ways-of-creating-content) +- [Issues](#issues) + - [Reporting a bug, requesting an enhancement](#reporting-a-bug-requesting-an-enhancement) + - [Beta testing](#beta-testing) + - [Helping triage existing issues](#helping-triage-existing-issues) +- [Code changes](#code-changes) + - [Using GitHub pull requests](#using-github-pull-requests) + - [Taking feedback into account](#taking-feedback-into-account) + - [Understanding automatic feedback](#understanding-automatic-feedback) + - [Understanding reviewers' feedback](#understanding-reviewers-feedback) + - [Fixing your branch](#fixing-your-branch) + - [Improving the official documentation](#improving-the-official-documentation) + - [Contributing to the standard library](#contributing-to-the-standard-library) + - [Fixing bugs and performing small changes](#fixing-bugs-and-performing-small-changes) + - [Proposing large changes: Coq Enhancement Proposals](#proposing-large-changes-coq-enhancement-proposals) + - [Collaborating on a pull request](#collaborating-on-a-pull-request) +- [Becoming a maintainer](#becoming-a-maintainer) + - [Reviewing pull requests](#reviewing-pull-requests) + - [Merging pull requests](#merging-pull-requests) + - [Core development team](#core-development-team) +- [Release management](#release-management) + - [Packaging Coq](#packaging-coq) +- [Additional resources](#additional-resources) + - [Developer documentation](#developer-documentation) + - [Where to find the resources](#where-to-find-the-resources) + - [Building Coq](#building-coq) + - [Continuous integration](#continuous-integration) + - [Code owners, issue and pull request templates](#code-owners-issue-and-pull-request-templates) + - [Style guide](#style-guide) + - [OCaml resources](#ocaml-resources) + - [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) + - [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) + - [Coq Users and Developers Workshops](#coq-users-and-developers-workshops) + +## Introduction ## + +Thank you for your interest in contributing to Coq! There are many +ways to contribute, and we appreciate all of them. + +People often begin by making small contributions, and contributions to +the ecosystem, before working their way up incrementally to the core +parts of the system, and start to propose larger changes, or take an +active role in maintaining the system. So this is the way this +contributing guide is organized. However, it is by no means necessary +that you go through these steps in this order. Feel free to use this +guide as a reference and quickly jump to the part that is most +relevant to you at the current time. + +We want to make sure that contributing to Coq is a fun and positive +experience for everyone, so please make sure you read and abide by our +[Code of Conduct][Code-of-conduct]. + +## Contributing to the ecosystem ## + +In this section, we present all the ways to contribute to Coq outside +of the Coq repository itself. + +### Asking and answering questions ### + +One very important way of contributing is by asking and answering +questions, in order to create a body of easily-browsable, +problem-oriented, additional documentation. + +There are two main platforms for this purpose: + +- [Stack Overflow][Stack-Overflow] (or more generally the [Stack + Exchange][Stack-Exchange] platforms, as some Coq questions may be + asked on other sites, such as TCS Stack Exchange); +- Our [Discourse forum][Discourse]. + +In particular, our Discourse forum has several non-English categories +that have yet to find their public, so do not hesitate to advertise +them to people you know who might not be at ease with English. + +Other active places to answer questions include the [Coq-Club][] +mailing list, and the Coq IRC channel (`irc://irc.freenode.net/#coq`). + +### Writing tutorials and blog posts ### + +Writing about Coq, in the form of tutorials or blog posts, is also a +very important contribution. In particular, it can help new users get +interested in Coq, and learn about it, and existing users learn about +advance features. Our official resources, such as the [reference +manual][refman] are not suited for learning Coq, but serve as +reference documentation to which you can link from your tutorials. + +The Coq website has a page listing known +[tutorials][Coq-documentation] and the [wiki][] home page contains a +list too. You can expand the former through a pull request on the +[Coq website repository][Coq-website-repository], while the latter can +be edited directly by anyone with a GitHub account. + +At the current time, we do not have a way of aggregating blog posts on +a single page (like [OCaml planet][OCaml-planet]), but this would +probably be something useful to get, so do not hesitate if you want to +create it. Some people use [Reddit][] for this purpose. + +### Contributing to the wiki ### + +Coq's [wiki][] is an informal source of additional documentation which +anyone with a GitHub account can edit directly. In particular, it +contains the Coq [FAQ][] which has not seen so many updates in the +recent years. You should feel free to fix it, expand it, and even +refactor it (if you are not sure if some changes would be welcome, you +can open an issue to discuss them before performing them). + +People who watch the Coq repository will see recent wiki edits in +their GitHub feed. It is recommended to review them *a posteriori* to +check no mistake was introduced. The wiki is also a standard git +repository, so people can follow the changes using any standard git +tool. + +Coq's wiki is formatted using GitHub's flavored Markdown, with some +wiki-specific extensions. See: + +- [GitHub's Markdown guide][GitHub-markdown] +- [GitHub's wiki extensions][GitHub-wiki-extensions] + +### Creating and maintaining Coq packages ### + +*Note: this sub-section is about packages extending Coq, such as +plugins or libraries. A different, but also very valuable, +contribution is to package Coq for your preferred package manager (see +[Packaging Coq](#packaging-coq)).* + +Sharing reusable assets in the form of new libraries, plugins, and +tools is great so that others can start building new things on top. +Having an extensive and healthy package ecosystem will be key to the +success of Coq. + +#### Distribution #### + +You can distribute your library or plugin through the [Coq package +index][Coq-package-index]. Tools can be advertised on the [tools +page][tools-website] of the Coq website, or the [tools +page][tools-wiki] of the wiki. + +#### Support #### + +You can find advice and best practices about maintaining a Coq project +on the [coq-community wiki][coq-community-wiki]. + +Learn how to write a Coq plugin, and about best practices, in the Coq +[plugin tutorial][plugin-tutorial]. This tutorial is still a work in +progress, so do not hesitate to expand it, or ask questions. + +If you want quick feedback on best practices, or how to talk to the +Coq API, a good place to hang out is the Coq [Gitter channel][Gitter]. + +Finally, we strongly encourage authors of plugins to submit their +plugins to join Coq's continuous integration (CI) early on. Indeed, +the Coq API gets continously reworked, so this is the best way of +ensuring your plugin stays compatible with new Coq versions, as this +means Coq developers will fix your plugin for you. Learn more about +this in the [CI README (user part)][CI-README-users]. + +Pure Coq libraries are also welcome to join Coq's CI, especially if +they test underused / undertested features. + +#### Standard libraries #### + +There are many general purpose Coq libraries, so before you publish +yours, consider whether you could contribute to an existing one +instead (either the official [standard +library](#contributing-to-the-standard-library), or one of the many +[alternative standard libraries][other-standard-libraries]). + +#### Maintaining existing packages in coq-community #### + +Some Coq packages are not maintained by their initial authors anymore +(for instance if they've moved on to new jobs or new projects) even if +they were useful, or interesting. The coq-community organization is a +place for volunteers to take over the maintenance of such packages. + +If you want to contribute by becoming a maintainer, there is [a list +of packages waiting for a +maintainer][coq-community-maintainer-wanted]. You can also propose a +package that is not listed. Find out more about coq-community in [the +manifesto's README][coq-community-manifesto]. + +### Contributing to the editor support packages ### + +Here are the URLs of the repositories of the various editor support +packages: + +- Proof-General (Emacs major mode) <https://github.com/ProofGeneral/PG> +- Company-coq (Emacs minor mode) <https://github.com/cpitclaudel/company-coq> +- Coqtail (Vim) <https://github.com/whonore/Coqtail> +- VsCoq Reloaded (VsCode) <https://github.com/coq-community/vscoq> + +Each of them has their own contribution process. + +### Contributing to the website or the package archive ### + +The website and the package archive have their own repositories: + +- <https://github.com/coq/www> +- <https://github.com/coq/opam-coq-archive> + +You can contribute to them by using issues and pull requests on these +repositories. These repositories should get their own contributing +guides, but they don't have any at the time of writing this. + +### Other ways of creating content ### + +There are many other ways of creating content and making the Coq +community thrive, including many which we might not have thought +about. Feel free to add more references / ideas to this sub-section. + +You can tweet about Coq, you can give talks about Coq both in +academic, and in non-academic venues (such as developer conferences). + +[Codewars][] is a platform where people can try to solve some +programming challenges that were proposed by other community members. +Coq is supported and the community is eager to get more challenges. + +## Issues ## + +### Reporting a bug, requesting an enhancement ### + +Bug reports are enormously useful to identify issues with Coq; we +can't fix what we don't know about. To report a bug, please open an +issue in the [Coq issue tracker][Coq-issue-tracker] (you'll need a +GitHub account). You can file a bug for any of the following: + +- An anomaly. These are always considered bugs, so Coq will even ask + you to file a bug report! - An error you didn't expect. If you're not sure whether it's a bug or - intentional, feel free to file a bug anyway. We may want to improve the - documentation or error message. -- Missing documentation. It's helpful to track where the documentation should - be improved, so please file a bug if you can't find or don't understand some - bit of documentation. -- An error message that wasn't as helpful as you'd like. Bonus points for - suggesting what information would have helped you. -- Bugs in CoqIDE should also be filed in the - [Coq issue tracker][]. - Bugs in the Emacs plugin should be filed against - [ProofGeneral](https://github.com/ProofGeneral/PG/issues), or against - [company-coq](https://github.com/cpitclaudel/company-coq/issues) if they are - specific to company-coq features. - -It would help if you search the existing issues before reporting a bug. This -can be difficult, so consider it extra credit. We don't mind duplicate bug -reports. If unsure, you are always very welcome to ask on our [Discourse forum][] -or [Gitter chat][] before, after, or while writing a bug report + intentional, feel free to file a bug anyway. We may want to improve + the documentation or error message. +- Missing or incorrect documentation. It's helpful to track where the + documentation should be improved, so please file a bug if you can't + find or don't understand some bit of documentation. +- An error message that wasn't as helpful as you'd like. Bonus points + for suggesting what information would have helped you. +- Bugs in CoqIDE should also be filed in the [Coq issue + tracker][Coq-issue-tracker]. Bugs in the Emacs plugin should be + filed against [ProofGeneral][ProofGeneral-issues], or against + [company-coq][company-coq-issues] if they are specific to + company-coq features. + +It would help if you search the existing issues before reporting a +bug. This can be difficult, so consider it extra credit. We don't +mind duplicate bug reports. If unsure, you are always very welcome to +ask on our [Discourse forum][Discourse] or [Gitter chat][Gitter] +before, after, or while writing a bug report. + +It is better if you can test that your bug is still present in the +current testing or development version of Coq (see the [next +sub-section](#beta-testing)) before reporting it, but if you can't, it +should not discourage you from reporting it. When it applies, it's extremely helpful for bug reports to include sample code, and much better if the code is self-contained and complete. It's not @@ -40,177 +285,838 @@ since someone else can often do this if you include a complete example. We tend to include the code in the bug description itself, but if you have a very large input file then you can add it as an attachment. -If you want to minimize your bug (or help minimize someone else's) for more -extra credit, then you can use the -[Coq bug minimizer](https://github.com/JasonGross/coq-tools) (specifically, -the bug minimizer is the `find-bug.py` script in that repo). - -### Triaging bug reports - -Triaging bug reports (adding labels, closing outdated / resolved bugs) -requires you to be granted some permissions. You may request members of the -**@coq/core** team to add you to the contributors team. They can do so using -this link: <https://github.com/orgs/coq/teams/contributors/members?add=true>. - -## Pull requests - -**Beginner's guide to hacking Coq: [`dev/doc/README.md`](dev/doc/README.md)** \ -**Development information and tools: [`dev/README.md`](dev/README.md)** - -If you want to contribute a bug fix or feature yourself, pull requests on -the [GitHub repository](https://github.com/coq/coq) are the way to contribute -directly to the Coq implementation. We recommend you create a fork of the -repository on GitHub and push your changes to a new "topic branch" in that -fork. From there you can follow the -[GitHub pull request documentation](https://help.github.com/articles/about-pull-requests/) -to get your changes reviewed and pulled into the Coq source repository. - -Documentation for getting started with the Coq sources is located in various -files in [`dev/doc`](dev/doc) (for example, [debugging.md](dev/doc/debugging.md)). - -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. Our CI runs this test suite and lots of other tests, including -building external Coq projects, 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-developers.md`](dev/ci/README-developers.md) 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. - -If your pull request fixes a critical bug (a bug allowing a proof of `False`), -please add an entry to [`dev/doc/critical-bugs`](/dev/doc/critical-bugs). - -Don't be alarmed if the pull request process takes some time. It can take a -few days to get feedback, approval on the final changes, and then a merge. -Do not hesitate to ping the reviewers if it takes longer than this. -Coq doesn't release new versions very frequently so it can take a few months -for your change to land in a released version. That said, you can start using -the latest Coq `master` branch to take advantage of all the new features, -improvements, and fixes. - -Whitespace discipline (do not indent using tabs, no trailing spaces, text -files end with newlines) is checked by the `lint` job on GitLab CI (using -`git diff --check`). We ship a [`dev/tools/pre-commit`](/dev/tools/pre-commit) -git hook which fixes these errors at commit time. `configure` automatically -sets you up to use it, unless you already have a hook at `.git/hooks/pre-commit`. - -Each commit in your pull request should compile (this makes bisecting -easier). The `lint` job checks compilation of the OCaml files, please -try to keep the rest of Coq in a functioning state as well. +If you want to minimize your bug (or help minimize someone else's) for +more extra credit, then you can use the [Coq bug +minimizer][JasonGross-coq-tools] (specifically, the bug minimizer is +the `find-bug.py` script in that repo). + +### Beta testing ### + +Coq gets a new major release about every six months. Before a new +major version is released, there is a beta-testing period, which +usually lasts one month (see the [release plan][release-plan]). You +can help make the upcoming release better, by testing the beta +version, and trying to port your projects to it. You should report +any bug you notice, but also any change of behavior that is not +documented in the changelog. Then Coq developers will be able to +check if what you reported is a regression that needs to be fixed, or +an expected change that needs to be mentioned in the changelog. + +You can go even further by using the development version (`master` +branch) of Coq on a day by day basis, and report problems as soon as +you notice them. If you wish to do so, the easiest way to install Coq +is through opam (using the `dev` version of the Coq package, available +in the <https://coq.inria.fr/opam/core-dev> repository) or through +[Nix][]. The documentation of the development version is [available +online][master-doc], including the [unreleased +changelog][unreleased-changelog]. + +### Helping triage existing issues ### + +Coq has too many bug reports for its core developers alone to manage. +You can help a lot by: + +- confirming that reported bugs are still active with the current + version of Coq; +- determining if the bug is a regression (new, and unexpected, + behavior from a recent Coq version); +- more generally, by reproducing a bug, on another system, + configuration, another version of Coq, and by documenting what you + did; +- giving a judgement about whether the reported behavior is really a + bug, or is expected but just improperly documented, or expected and + already documented; +- producing a trace if it is relevant and you know how to do it; +- producing another example exhibiting the same bug, or minimizing the + initial example using the bug minimizer mentioned above; +- using `git bisect` to find the commit that introduced a regression; +- fixing the bug if you have an idea of how to do so (see the + [following section](#code-changes)). + +Once you have some experience with the Coq issue tracker, you can +request to join the **@coq/contributors** team (any member of the +**@coq/core** team can do so using [this link][add-contributor]). +Being in this team will grant you the following access: + +- **Updating labels:** every open issue and pull request should + ideally get one or several `kind:` and `part:` labels. In + particular, valid issues should generally get either a `kind: bug` + (the reported behavior can indeed be considered a bug, this can be + completed with the `kind: anomaly`, and `kind: regression` labels), + `kind: documentation` (e.g. if a reported behavior is expected but + improperly documented), `kind: enhancement` (a request for + enhancement of an existing feature), or `kind: feature` label (an + idea for a new feature). +- **Creating new labels:** if you feel a `part:` label is missing, do + not hesitate to create it. If you are not sure, you may discuss it + with other contributors and developers on [Gitter][] first. +- **Closing issues:** if a bug cannot be reproduced anymore, is a + duplicate, or should not be considered a bug report in the first + place, you should close it. When doing so, try putting an + appropriate `resolved:` label to indicate the reason. If the bug + has been fixed already, and you know in which version, you can add a + milestone to it, even a milestone that's already closed, instead of + a `resolved:` label. When closing a duplicate issue, try to add all + the additional info that could be gathered to the original issue. +- **Editing issue titles:** you may want to do so to better reflect + the current understanding of the underlying issue. +- **Editing comments:** feel free to do so to fix typos and formatting + only (in particular, some old comments from the Bugzilla era or + before are not properly formatted). You may also want to edit the + OP's initial comment (a.k.a. body of the issue) to better reflect + the current understanding of the issue, especially if the discussion + is long. If you do so, only add to the original comment, and mark + it clearly with an `EDITED by @YourNickname:`. +- **Hiding comments:** when the discussion has become too long, this + can be done to hide irrelevant comments (off-topic, outdated or + resolved sub-issues). +- **Deleting things:** please don't delete any comment or issue, our + policy doesn't allow for comments to be deleted, unless done by the + community moderators. You should hide them instead. An audit log + is available to track deleted items if needed (but does not allow + recovering them). +- **Pushing a branch or a tag to the main repository:** please push + changes to your own fork rather than the main repository. (Branches + pushed to the main repository will be removed promptly and without + notice.) + +Yet to be fully specified: use of priority, difficulty, `help wanted`, +and `good first issue` labels, milestones, assignments, and GitHub +projects. + +## Code changes ## + +### Using GitHub pull requests ### + +If you want to contribute a documentation update, bug fix or feature +yourself, pull requests (PRs) on the [GitHub +repository][coq-repository] are the way to contribute directly to the +Coq implementation (all changes, even the smallest changes from core +developers, go through PRs). You will need to create a fork of the +repository on GitHub and push your changes to a new "topic branch" in +that fork (instead of using an existing branch name like `master`). + +PRs should always target the `master` branch. Make sure that your +copy of this branch is up-to-date before starting to do your changes, +and that there are no conflicts before submitting your PR. If you +need to fix conflicts, we generally prefer that you rebase your branch +on top of `master`, instead of creating a merge commit. + +If you are not familiar with `git` or GitHub, Sections [Git +documentation, tips and tricks](#git-documentation-tips-and-tricks), +and [GitHub documentation, tips and +tricks](#github-documentation-tips-and-tricks), should be helpful (and +even if you are, you might learn a few tricks). + +Once you have submitted your PR, it may take some time to get +feedback, in the form of reviews from maintainers, and test results +from our continuous integration system. Our code owner system will +automatically request reviews from relevant maintainers. Then, one +maintainer should self-assign the PR (if that does not happen after a +few days, feel free to ping the maintainers that were requested a +review). The PR assignee will then become your main point of contact +for handling the PR: they should ensure that everything is in order +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. 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 +indication of when to expect your change to be released (this could be +several months after your PR is merged). That said, you can start +using the latest Coq `master` branch to take advantage of all the new +features, improvements, and fixes. + +### Taking feedback into account ### + +#### Understanding automatic feedback #### + +When you open or update a PR, you get automatically some feedback: we +have a bot whose job will be to push a branch to our GitLab mirror to +run some continuous integration (CI) tests. The tests will run on a +commit merging your branch with the base branch, so if there is a +conflict and this merge cannot be performed automatically, the bot +will put a `needs: rebase` label, and the tests won't run. + +Otherwise, a large suite of tests will be run on GitLab, plus some +additional tests on Azure for Windows and macOS compatibility. + +If a test fails on GitLab, you will see in the GitHub PR interface, +both the failure of the whole pipeline, and of the specific failed +job. Most of these failures indicate problems that should be +addressed, but some can still be due to synchronization issues out of +your control. In particular, if you get a failure in one of the +tested plugins but you didn't change the Coq API, it is probably a +transient issue and you shouldn't have to worry about it. In case of +doubt, ask the reviewers. + +##### Test-suite failures ##### + +If you broke the test-suite, you should get many failed jobs, because +the test-suite is run multiple times in various settings. You should +get the same failure locally by running `make test-suite` or `make -f +Makefile.dune test-suite`. It's helpful to run this locally and +ensure the test-suite is not broken before submitting a PR as this +will spare a lot of runtime on distant machines. + +To learn more about the test-suite, you should refer to its +[README][test-suite-README]. + +##### Linter failures ##### + +We have a linter that checks a few different things: + +- **Every commit can build.** This is an important requirement to + allow the use of `git bisect` in the future. It should be possible + to build every commit, and in principle even the test-suite should + pass on every commit (but this isn't tested in CI because it would + take too long). A good way to test this is to use `git rebase + master --exec "make -f Makefile.dune check`. +- **No tabs or end-of-line spaces on updated lines**. We are trying + to get rid of all tabs and all end-of-line spaces from the code base + (except in some very special files that need them). This checks not + only that you didn't introduce new ones, but also that updated lines + are clean (even if they were there before). You can avoid worrying + about tabs and end-of-line spaces by installing our [pre-commit git + hook][git-hook], which will fix these issues at commit time. + Running `./configure` once will install this hook automatically + unless you already have a pre-commit hook installed. If you are + encountering these issues nonetheless, you can fix them by rebasing + your branch with `git rebase --whitespace=fix`. +- **All files should end with a single newline**. See the section + [Style guide](#style-guide) for additional style recommendations. You may run the linter yourself with `dev/lint-repository.sh`. -Here are a few tags Coq developers may add to your PR and what they mean. In -general feedback and requests for you as the pull request author will be in -the comments and tags are only used to organize pull requests. - -- [needs: rebase][rebase-label] indicates the PR should be rebased on top of - the latest base branch (usually `master`). See the - [GitHub documentation](https://help.github.com/articles/about-git-rebase/) - for a brief introduction to using `git rebase`. - We generally ask you to rebase only when there are merge conflicts or if - the PR has been opened for a long time and we want a fresh CI run. -- [needs: fixing][fixing-label] indicates the PR needs a fix, as discussed in the comments. -- [needs: benchmarking][benchmarking-label] and [needs: testing][testing-label] +##### Plugin failures ##### + +If you did change the Coq API, then you may have broken a plugin. +After ensuring that the failure comes from your change, you will have +to provide a fix to the plugin, and the PR assignee will have to +ensure that this fix is merged in the plugin simultaneously with your +PR on the Coq repository. + +If your changes to the API are not straightforward, you should also +document them in `dev/doc/changes.md`. + +The [CI README (developer part)][CI-README-developers] contains more +information on how to fix plugins, test and submit your changes, and +how you can anticipate the results of the CI before opening a PR. + +##### Library failures ##### + +Such a failure can indicate either a bug in your branch, or a breaking +change that you introduced voluntarily. All such breaking changes +should be properly documented in the [user changelog][user-changelog]. +Furthermore, a backward-compatible fix should be found, and this fix +should be merged in the broken projects *before* your PR to the Coq +repository can be. You can use the same documentation as above to +learn about testing and fixing locally the broken libraries. + +#### Understanding reviewers' feedback #### + +The reviews you get are highly dependent on the kind of changes you +did. In any case, you should always remember that reviewers are +friendly volunteers that do their best to help you get your changes in +(and should abide by our [Code of Conduct][Code-of-Conduct]). But at +the same time, they try to ensure that code that is introduced or +updated is of the highest quality and will be easy to maintain in the +future, and that's why they may ask you to perform small or even large +changes. If you need a clarification, do not hesitate to ask. + +Here are a few labels that reviewers may add to your PR to track its +status. In general, this will come in addition to comments from the +reviewers, with specific requests. + +- [needs: rebase][needs-rebase] indicates the PR should be rebased on + top of the latest version of the base branch (usually `master`). We + generally ask you to rebase only when there are merge conflicts or + if the PR has been opened for a long time and we want a fresh CI + run. +- [needs: fixing][needs-fixing] indicates the PR needs a fix, as + discussed in the comments. +- [needs: documentation][needs-documentation] indicates the PR + introduces changes that should be documented before it can be merged. +- [needs: changelog entry][needs-changelog] indicates the PR introduces + changes that should be documented in the [user + changelog][user-changelog]. +- [needs: benchmarking][needs-benchmarking] and [needs: testing][needs-testing] indicate the PR needs testing beyond what the test suite can handle. For example, performance benchmarking is currently performed with a different infrastructure ([documented in the wiki][jenkins-doc]). Unless some followup - is specifically requested you aren't expected to do this additional testing. + is specifically requested, you aren't expected to do this additional testing. -To learn more about the merging process, you can read the -[merging documentation for Coq maintainers](dev/doc/MERGING.md). +More generally, such labels should come with a description that should +allow you to understand what they mean. -[rebase-label]: https://github.com/coq/coq/pulls?utf8=%E2%9C%93&q=is%3Aopen%20is%3Apr%20label%3A%22needs%3A%20rebase%22 -[fixing-label]: https://github.com/coq/coq/pulls?q=is%3Aopen+is%3Apr+label%3A%22needs%3A+fixing%22 -[benchmarking-label]: https://github.com/coq/coq/pulls?q=is%3Aopen+is%3Apr+label%3A%22needs%3A+benchmarking%22 -[testing-label]: https://github.com/coq/coq/pulls?q=is%3Aopen+is%3Apr+label%3A%22needs%3A+testing%22 +#### Fixing your branch #### -[jenkins-doc]: https://github.com/coq/coq/wiki/Jenkins-(automated-benchmarking) +If you have changes to perform before your PR can be merged, you might +want to do them in separate commits at first to ease the reviewers' +task, but we generally appreciate that they are squashed with the +commits that they fix before merging. This is especially true of +commits fixing previously introduced bugs or failures. + +### Improving the official documentation ### + +The documentation is usually a good place to start contributing, +because you can get used to the pull request submitting and review +process, without needing to learn about the code source of Coq at the +same time. + +The official documentation is formed of two components: + +- the [reference manual][refman], +- the [documentation of the standard library][stdlib-doc]. -## Documentation +The sources of the reference manual are located in the +[`doc/sphinx`][refman-sources] directory. They are written in rst +(Sphinx) format with some Coq-specific extensions, which are +documented in the [README][refman-README] in the above directory. +This README was written to be read from begin to end. As soon as your +edits to the documentation are more than changing the textual content, +we strongly encourage you to read this document. -Currently the process for contributing to the documentation is the same as -for changing anything else in Coq, so please submit a pull request as -described above. +The documentation of the standard library is generated with +[coqdoc][coqdoc-documentation] from the comments in the sources of the +standard library. -Our issue tracker includes a flag to mark bugs related to documentation. -You can view a list of documentation-related bugs using a -[GitHub issue search](https://github.com/coq/coq/issues?q=is%3Aopen+is%3Aissue+label%3A%22kind%3A+documentation%22). -Many of these bugs can be fixed by contributing writing, without knowledge -of Coq's OCaml source code. +The [README in the `doc` directory][doc-README] contains more +information about the documentation's build dependencies, and the +`make` targets. -The sources for the [Coq reference manual](https://coq.inria.fr/distrib/current/refman/) -are at [`doc/sphinx`](/doc/sphinx). These are written in reStructuredText -and compiled to HTML and PDF with [Sphinx](http://www.sphinx-doc.org/). +You can browse through the list of open documentation issues using the +[kind: documentation][kind-documentation] label, or the [user +documentation GitHub project][documentation-github-project] (you can +look in particular at the "Writing" and "Fixing" columns). -You will find information on how to build the documentation in -[`doc/README.md`](doc/README.md) and information about the specificities of -the Coq Sphinx format in [`doc/sphinx/README.rst`](doc/sphinx/README.rst). +### Contributing to the standard library ### -You may also contribute to the informal documentation available in -[Cocorico](https://github.com/coq/coq/wiki) (the Coq wiki), and the -[Coq FAQ](https://github.com/coq/coq/wiki/The-Coq-FAQ). Both of these are -editable by anyone with a GitHub account. +Contributing to the standard library is also made easier by not having +to learn about Coq's internals, and its implementation language. -## Where to get help (with the Coq source code, or anything else) +Due to the compatibility constraints created by the many projects that +depend on it, proposing breaking changes, such as changing a +definition, may frequently be rejected, or at the very least might +take a long time before getting approved and merged. This does not +mean that you cannot try. On the other hand, contributing new lemmas +on existing definitions and cleaning up existing proofs are likely to +be accepted. Contributing new operations on existing types are also +likely to be accepted in many cases. In case of doubt, ask in an +issue before spending too much time preparing your PR. -We have a [Discourse forum][] (see in particular the [Coq development category][]) -and a [Gitter chat][]. Feel free to join any of them and ask questions. +If you create a new file, it needs to be listed in +`doc/stdlib/index-list.html`. + +Add coqdoc comments to extend the [standard library +documentation][stdlib-doc]. See the [coqdoc +documentation][coqdoc-documentation] to learn more. + +### Fixing bugs and performing small changes ### + +Just open a PR with your fix. If it is not yet completed, do not +hesitate to open a [*draft PR*][GitHub-draft-PR] to get early +feedback, and talk to developers on [Gitter][]. + +It is generally a good idea to add a regression test to the +test-suite. See the test-suite [README][test-suite-README] for how to +do so. + +Small fixes do not need any documentation, or changelog update. New, +or updated, user-facing features, and major bug fixes do. See above +on how to contribute to the documentation, and the README in +[`doc/changelog`][user-changelog] for how to add a changelog entry. + +### Proposing large changes: Coq Enhancement Proposals ### + +You are always welcome to open a PR for a change of any size. +However, you should be aware that the larger the change, the higher +the chances it will take very long to review, and possibly never get +merged. + +So it is recommended that before spending a lot of time coding, you +seek feedback from maintainers to see if your change would be +supported, and if they have recommendation about its implementation. +You can do this informally by opening an issue, or more formally by +producing a design document as a [Coq Enhancement Proposal][CEP]. + +Another recommendation is that you do not put several unrelated +changes (even if you produced them together) in the same PR. In +particular, make sure you split bug fixes into separate PRs when this +is possible. More generally, smaller-sized PRs, or PRs changing less +components, are more likely to be reviewed and merged promptly. + +### Collaborating on a pull request ### + +Beyond making suggestions to a PR author during the review process, +you may want to collaborate further by checking out the code, making +changes, and pushing them. There are two main ways of doing this: + +- **Pull requests on pull requests:** You can checkout the PR branch + (GitHub provides the link to the remote to pull from and the branch + name on the top and the bottom of the PR discussion thread), + checkout a new personal branch from there, do some changes, commit + them, push to your fork, and open a new PR on the PR author's fork. +- **Pushing to the PR branch:** If the PR author has not unchecked the + "Allow edit from maintainers" checkbox, and you have write-access to + the repository (i.e. you are in the **@coq/contributors** team), + then you can also push (and even force-push) directly to the PR + branch, on the main author's fork. Obviously, don't do it without + coordinating with the PR author first (in particular, in case you + need to force-push). + +When several people have co-authored a single commit (e.g. because +someone fixed something in a commit initially authored by someone +else), this should be reflected by adding ["Co-authored-by:" +tags][GitHub-co-authored-by] at the end of the commit message. The +line should contain the co-author name and committer e-mail address. + +## Becoming a maintainer ## + +### Reviewing pull requests ### + +You can start reviewing PRs as soon as you feel comfortable doing so +(anyone can review anything, although some designated reviewers +will have to give a final approval before a PR can be merged, as is +explained in the next sub-section). + +Reviewers should ensure that the code that is changed or introduced is +in good shape and will not be a burden to maintain, is unlikely to +break anything, or the compatibility-breakage has been identified and +validated, includes documentation, changelog entries, and test files +when necessary. Reviewers can use labels, or change requests to +further emphasize what remains to be changed before they can approve +the PR. Once reviewers are satisfied (regarding the part they +reviewed), they should formally approve the PR, possibly stating what +they reviewed. + +That being said, reviewers should also make sure that they do not make +the contributing process harder than necessary: they should make it +clear which comments are really required to perform before approving, +and which are just suggestions. They should strive to reduce the +number of rounds of feedback that are needed by posting most of their +comments at the same time. If they are opposed to the change, they +should clearly say so from the beginning to avoid the contributor +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). + +### Core development team ### + +The core developers are the active developers with a lengthy and +significant contribution track record. They are the ones with admin +powers over the Coq organization, and the ones who take part in votes +in case of conflicts to take a decision (rare). One of them is +designated as a development coordinator, and has to approve the +changes in the core team membership (until we get a more formal +joining and leaving process). + +The core developers are the members of the **@coq/core** team ([member +list][coq-core] only visible to the Coq organization members because +of a limitation of GitHub). + +## Release management ## + +Coq's major release cycles generally span about six months, with about +4-5 months of development, and 1-2 months of stabilization / +beta-releases. The release manager (RM) role is a rolling position +among core developers. The [release plan][release-plan] is published +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 +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 +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 +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. + +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 +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 +been removed in `master`, and PRs from the RM changing the version +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 +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" +column to a "Shipped" column. + +More information about the RM tasks can be found in the [release +process checklist][RM-checklist]. + +### Packaging Coq ### + +The RM role does not include the task of making Coq available through +the various package managers out there: several contributors (most +often external to the development team) take care of this, and we +thank them for this. If your preferred package manager does not +include Coq, it is a very worthy contribution to make it available +there. But be careful not to let a package get outdated, as this +could lead some users to install an outdated version of Coq without +even being aware of it. + +This [Repology page][repology-coq] lists the versions of Coq which are +packaged in many repositories, although it is missing information on +some repositories, like opam. + +The Windows and macOS installers are auto-generated in our CI, and +this infrastructure has dedicated maintainers within the development +team. + +## Additional resources ## + +### Developer documentation ### + +#### Where to find the resources #### + +- You can find developer resources in the `dev` directory, and more + specifically developer documentation in `dev/doc`. The + [README][dev-README] in the `dev` directory lists what's available. + + For example, [`dev/doc/README.md`][dev-doc-README] is a beginner's + guide to hacking Coq, and documentation on debugging Coq can be + found in [`dev/doc/debugging.md`][debugging-doc]. + +- When it makes sense, the documentation is kept even closer to the + sources, in README files in various directories (e.g. the test-suite + [README][test-suite-README] or the refman [README][refman-README]). + +- Documentation of the Coq API is written directly in comments in + `.mli` files. You can browse it on [the Coq website][api-doc], or + rebuild it locally (`make -f Makefile.dune apidoc`, requires `odoc` + and `dune`). + +- A plugin tutorial is located in + [`doc/plugin_tutorial`][plugin-tutorial]. + +- The Coq [wiki][] contains additional developer resources. + +#### Building Coq #### + +The list of dependencies can be found in the first section of the +[`INSTALL`](INSTALL) file. + +Today, the recommended method for building Coq is to use `dune`. Run +`make -f Makefile.dune` to get help on the various available targets, +Additional documentation can be found in +[`dev/doc/build-system.dune.md`][dev-doc-dune], and in [the official +Dune documentation][dune-doc]. + +The legacy make-based system is still available. If you wish to use +it, you need to start by running `./configure -profile devel`. Most +of the available targets are not documented, so you will need to ask. + +#### Continuous integration #### + +Continuous integration (CI) testing is key in ensuring that the +`master` branch is kept in a well-functioning state at all times, and +that no accidental compatibility breakages are introduced. Our CI is +quite extensive since it includes testing many external projects, some +of them taking more than an hour to compile. However, you can get +partial results much more quickly (when our CI is not overloaded). + +The main documentation resources on our CI are: + +- the [README for users, i.e. plugin and library authors][CI-README-users]; +- the [README for developers, and contributors][CI-README-developers]; +- the README of the [user-overlays][] directory. + +Preparing an overlay (i.e. a patch to an external project that we test +in our CI, to make it compile with the modified version of Coq in your +branch) is a step that everyone goes through at some point. All you +need to know to prepare an overlay manually is in the README in the +[user-overlays][] directory. You might want to use some additional +tooling such as the `make ci-*` targets of `Makefile.ci`, the Nix +support for getting the dependencies of the external projects (see the +README in [`dev/ci/nix`](dev-ci-nix), and the (so far undocumented) +`dev/tools/create_overlays.sh` script. + +More work is to be done on understanding how each developer proceeds +to prepare overlays, and propose a simplified and documented +procedure. + +We also have a benchmarking infrastructure, which is documented [on +the wiki][jenkins-doc]. + +#### Code owners, issue and pull request templates #### + +These files can be found in the [`.github`](.github) directory. The +templates are particularly useful to remind contributors what +information we need for them, and, in the case of PRs, to update the +documentation, changelog, and test-suite when relevant. + +GitHub now supports setting up multiple issue templates, and we could +use this to define distinct requirements for various kind of bugs, +enhancement and feature requests. + +#### Style guide #### + +There exists an [old style guide][old-style-guide] whose content is +still mostly relevant. Yet to be done: extract the parts that are +most relevant, and put them in this section instead. + +We don't use a code formatter at the current time, and we are +reluctant to merge changes to parts of the code that are unchanged +aside from formatting. However, it is still a good idea if you don't +know how to format a block of code to use the formatting that +[ocamlformat][] would give + +#### OCaml resources #### + +You can find lots of OCaml resources on <http://ocaml.org/>, including +documentation, a Discourse forum, the package archive, etc. You may +also want to refer to the [Dune documentation][dune-doc]. + +Another ressource is <https://ocamlverse.github.io/>, especially its +[community page][ocamlverse-community], which lists the various OCaml +discussion platforms. + +#### Git documentation, tips and tricks #### + +Lots of resources about git, the version control system, are available +on the web, starting with the [official website][git]. + +We recommend a setup with two configured remotes, one for the official +Coq repository, called `upstream`, and one for your fork, called +`origin`. Here is a way to do this for a clean clone: + +``` shell +git clone https://github.com/coq/coq -o upstream +cd coq +git remote add origin git@github.com:$YOURNAME/coq +# Make sure you click the fork button on GitHub so that this repository exists +cp dev/tools/pre-commit .git/hooks/ # Setup the pre-commit hook +``` + +Then, if you want to prepare a fix: + +``` shell +# Make sure we start from an up-to-date master +git checkout master +git pull --ff-only # If this fails, then your master branch is messy +git checkout -b my-topic-branch +# Modify some files +git add . +# Every untracked or modified file will be included in the next commit +# You can also replace the dot with an explicit list of files +git commit -m "My commit summary. + +You can add more information on multiple lines, +but you need to skip a line first." +git push -u origin my-topic-branch +# Next time, you push to this branch, you can just do git push +``` + +When you push a new branch for the first time, GitHub gives you a link +to open a PR. + +If you need to fix the last commit in your branch (typically, if your +branch has a single commit on top of `master`), you can do so with + +``` +git add . +git commit --amend --no-edit +``` + +If you need to fix another commit in your branch, or if you need to +fix a conflict with `master`, you will need to learn about `git rebase`. +GitHub provides [a short introduction][GitHub-rebase] to `git rebase`. + +#### GitHub documentation, tips and tricks #### + +GitHub has [extensive documentation][GitHub-doc] about everything you +can do on the platform, and tips about using `git` as well. See in +particular, [how to configure your commit e-mail +address][GitHub-commit-email] and [how to open a PR from a +fork][GitHub-PR-from-fork]. + +##### Watching the repository ##### + +["Watching" this repository][GitHub-watching] can result in a very +large number of notifications. We recommend you, either, [configure +your mailbox][notification-email] to handle incoming notifications +efficiently, or you read your notifications within a web browser. You +can configure how you receive notifications in [your GitHub +settings][GitHub-notification-settings], you can use the GitHub +interface to mark as read, save for later or mute threads. You can +also manage your GitHub web notifications using a tool such as +[Octobox][]. + +#### GitLab documentation, tips and tricks #### + +We use GitLab mostly for its CI service. The [Coq organization on +GitLab][GitLab-coq] hosts a number of CI/CD-only mirrors. If you are +a regular contributor, you can request access to it from [the +organization page][GitLab-coq]: this will grant you permission to +restart failing CI jobs. + +GitLab too has [extensive documentation][GitLab-doc], in particular on +configuring CI. + +#### Coqbot #### + +Our bot sources can be found at <https://github.com/coq/bot>. Its +documentation is still a work-in-progress. + +### Online forum and chat to talk to developers ### + +We have a [Discourse forum][Discourse] (see in particular the [Coq +development category][Discourse-development-category]) and a [Gitter +chat][Gitter]. Feel free to join any of them and ask questions. People are generally happy to help and very reactive. -[Coq development category]: https://coq.discourse.group/c/coq-development - -## Watching the repository - -["Watching" this repository](https://github.com/coq/coq/subscription) -can result in a very large number of notifications. We advise that if -you do, either [configure your mailbox](https://blog.github.com/2017-07-18-managing-large-numbers-of-github-notifications/#prioritize-the-notifications-you-receive) -to handle incoming notifications efficiently, or you read your -notifications within a web browser. You can configure how you receive -notifications in [your GitHub settings](https://github.com/settings/notifications), -you can use the GitHub interface to mark as read, save for later or -mute threads. You can also manage your GitHub web notifications using -a tool such as [Octobox](http://octobox.io/). - -## Contributing outside this repository - -There are many useful ways to contribute to the Coq ecosystem that don't -involve the Coq repository. - -Tutorials to teach Coq, and especially to teach particular advanced features, -are much appreciated. Some tutorials are listed on the -[Coq website](https://coq.inria.fr/documentation). If you would like to add -a link to this list, please make a pull request against the Coq website -repository at <https://github.com/coq/www>. - -External plugins / libraries contribute to create a successful ecosystem -around Coq. If your external development is mature enough, you may consider -submitting it for addition to our CI tests. Refer to -[`dev/ci/README-users.md`](dev/ci/README-users.md) for more information. - -Some Coq packages are not maintained by their authors anymore even if they -were useful (for instance because they changed jobs). The coq-community -organization is a place for people to take over the maintenance of such -useful packages. If you want to contribute by becoming a maintainer, you can -find a list of packages waiting for a maintainer [here](https://github.com/coq-community/manifesto/issues?q=is%3Aissue+is%3Aopen+label%3Amaintainer-wanted). -You can also propose a package that is not listed. Find out more about -coq-community in [the manifesto's README](https://github.com/coq-community/manifesto). - -Ask and answer questions on our [Discourse forum][], on [Stack Exchange][], -and on the Coq IRC channel (`irc://irc.freenode.net/#coq`). - -[Coq issue tracker]: https://github.com/coq/coq/issues -[Discourse forum]: https://coq.discourse.group/ -[Gitter chat]: https://gitter.im/coq/coq -[Stack Exchange]: https://stackexchange.com/filters/299857/questions-tagged-coq-on-stackexchange-sites +Obviously, the issue tracker is also a good place to ask questions, +especially if the development processes are unclear, or the developer +documentation should be improved. + +### Coq remote working groups ### + +We semi-regularly (up to every month) organize remote working groups, +which can be accessed through video-conference, and are most often +live streamed on [YouTube][]. Summary notes and announcements of the +next working group can be found [on the wiki][wiki-WG] + +These working groups are where important decisions are taken, most +often by consensus, but also, if it is needed, by a vote of core +developers. + +### Coq Users and Developers Workshops ### + +We have an annual gathering late Spring in France where most core +developers are present, and whose objective is to help new +contributors get started with the Coq codebase, provide help to plugin +and library authors, and more generally have fun together. + +The list of past (and upcoming, when it's already planned) workshops +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 +[CI-README-developers]: dev/ci/README-developers.md +[CI-README-users]: dev/ci/README-users.md +[Code-of-Conduct]: CODE_OF_CONDUCT.md +[CODEOWNERS]: .github/CODEOWNERS +[Codewars]: https://www.codewars.com/?language=coq +[company-coq-issues]: https://github.com/cpitclaudel/company-coq/issues +[Coq-Club]: https://sympa.inria.fr/sympa/arc/coq-club +[coq-community-maintainer-wanted]: https://github.com/coq-community/manifesto/issues?q=is%3Aissue+is%3Aopen+label%3Amaintainer-wanted +[coq-community-manifesto]: https://github.com/coq-community/manifesto +[coq-community-wiki]: https://github.com/coq-community/manifesto/wiki +[coq-core]: https://github.com/orgs/coq/teams/core/members +[coqdoc-documentation]: https://coq.inria.fr/refman/practical-tools/utilities.html#documenting-coq-files-with-coqdoc +[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-repository]: https://github.com/coq/coq +[Coq-website-repository]: https://github.com/coq/www +[debugging-doc]: dev/doc/debugging.md +[dev-doc-README]: dev/doc/README.md +[dev-doc-dune]: dev/doc/build-system.dune.md +[dev-README]: dev/README.md +[Discourse]: https://coq.discourse.group/ +[Discourse-development-category]: https://coq.discourse.group/c/coq-development +[doc-README]: doc/README.md +[documentation-github-project]: https://github.com/coq/coq/projects/3 +[dune-doc]: https://dune.readthedocs.io/en/latest/ +[FAQ]: https://github.com/coq/coq/wiki/The-Coq-FAQ +[git]: https://git-scm.com/ +[git-hook]: dev/tools/pre-commit +[GitHub-co-authored-by]: https://github.blog/2018-01-29-commit-together-with-co-authors/ +[GitHub-commit-email]: https://help.github.com/en/articles/setting-your-commit-email-address-in-git +[GitHub-doc]: https://help.github.com/ +[GitHub-draft-PR]: https://github.blog/2019-02-14-introducing-draft-pull-requests/ +[GitHub-markdown]: https://guides.github.com/features/mastering-markdown/ +[GitHub-notification-settings]: https://github.com/settings/notifications +[GitHub-PR-from-fork]: https://help.github.com/en/articles/creating-a-pull-request-from-a-fork +[GitHub-rebase]: https://help.github.com/articles/about-git-rebase/ +[GitHub-watching]: https://github.com/coq/coq/subscription +[GitHub-wiki-extensions]: https://help.github.com/en/articles/editing-wiki-content +[GitLab-coq]: https://gitlab.com/coq +[GitLab-doc]: https://docs.gitlab.com/ +[Gitter]: https://gitter.im/coq/coq +[JasonGross-coq-tools]: https://github.com/JasonGross/coq-tools +[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 +[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 +[needs-fixing]: https://github.com/coq/coq/labels/needs%3A%20fixing +[needs-rebase]: https://github.com/coq/coq/labels/needs%3A%20rebase +[needs-testing]: https://github.com/coq/coq/labels/needs%3A%20testing +[Nix]: https://github.com/coq/coq/wiki/Nix +[notification-email]: https://blog.github.com/2017-07-18-managing-large-numbers-of-github-notifications/#prioritize-the-notifications-you-receive +[OCaml-planet]: http://ocaml.org/community/planet/ +[ocamlformat]: https://github.com/ocaml-ppx/ocamlformat +[ocamlverse-community]: https://ocamlverse.github.io/content/community.html +[Octobox]: http://octobox.io/ +[old-style-guide]: dev/doc/style.txt +[other-standard-libraries]: https://github.com/coq/stdlib2/wiki/Other-%22standard%22-libraries +[plugin-tutorial]: doc/plugin_tutorial +[ProofGeneral-issues]: https://github.com/ProofGeneral/PG/issues +[Reddit]: https://www.reddit.com/r/Coq/ +[refman]: https://coq.inria.fr/refman +[refman-sources]: doc/sphinx +[refman-README]: doc/sphinx/README.rst +[release-plan]: https://github.com/coq/coq/wiki/Release-Plan +[repology-coq]: https://repology.org/project/coq/versions +[RM-checklist]: dev/doc/release-process.md +[Stack-Exchange]: https://stackexchange.com/filters/299857/questions-tagged-coq-on-stackexchange-sites +[Stack-Overflow]: https://stackoverflow.com/questions/tagged/coq +[stdlib-doc]: https://coq.inria.fr/stdlib/ +[test-suite-README]: test-suite/README.md +[tools-website]: https://coq.inria.fr/related-tools.html +[tools-wiki]: https://github.com/coq/coq/wiki/Tools +[unreleased-changelog]: https://coq.github.io/doc/master/refman/changes.html#unreleased-changes +[user-changelog]: doc/changelog +[user-overlays]: dev/ci/user-overlays +[wiki]: https://github.com/coq/coq/wiki +[wiki-CUDW]: https://github.com/coq/coq/wiki/CoqImplementorsWorkshop +[wiki-WG]: https://github.com/coq/coq/wiki/Coq-Working-Groups +[YouTube]: https://www.youtube.com/channel/UCbJo6gYYr0OF18x01M4THdQ diff --git a/dev/README.md b/dev/README.md index 9761f7b96f..4cda60a703 100644 --- a/dev/README.md +++ b/dev/README.md @@ -2,7 +2,7 @@ ## Debugging and profiling (`dev/`) -**More info on debugging: [`doc/debugging.md`](doc/debugging.md)** +**More info on debugging: [`dev/doc/debugging.md`](doc/debugging.md)** | File | Description | | ---- | ----------- | diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat index 78ca5e830a..c75acb0560 100755 --- a/dev/build/windows/MakeCoq_MinGW.bat +++ b/dev/build/windows/MakeCoq_MinGW.bat @@ -381,6 +381,7 @@ IF "%RUNSETUP%"=="Y" ( -P pkg-config ^
-P mingw64-%ARCH%-binutils,mingw64-%ARCH%-gcc-core,mingw64-%ARCH%-gcc-g++,mingw64-%ARCH%-windows_default_manifest ^
-P mingw64-%ARCH%-headers,mingw64-%ARCH%-runtime,mingw64-%ARCH%-pthreads,mingw64-%ARCH%-zlib ^
+ -P mingw64-%ARCH%-gmp,mingw64-%ARCH%-mpfr ^
-P adwaita-icon-theme ^
-P libiconv-devel,libunistring-devel,libncurses-devel ^
-P gettext-devel,libgettextpo-devel ^
@@ -389,6 +390,7 @@ IF "%RUNSETUP%"=="Y" ( -P gtk-update-icon-cache ^
-P libtool,automake ^
-P intltool ^
+ -P bison,flex ^
%EXTRAPACKAGES% ^
|| GOTO ErrorExit
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 0699e2bd44..0c8213b8f5 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -315,7 +315,7 @@ function get_expand_source_tar { find "$(ls)" -mindepth 1 -maxdepth 1 -exec mv -- "{}" . \; else echo "Unzip strip count not supported" - return 1 + exit 1 fi else logn untar tar xvaf "$TARBALLS/$name.$3" --strip $strip @@ -323,10 +323,11 @@ function get_expand_source_tar { # Patch if patch file exists # First try specific patch file name then generic patch file name + # Note: set -o errexit does not work inside a function called in an if, so exit explicity. if [ -f "$PATCHES/$name.patch" ] ; then - log1 patch -p1 -i "$PATCHES/$name.patch" + log1 patch -p1 -i "$PATCHES/$name.patch" || exit 1 elif [ -f "$PATCHES/$basename.patch" ] ; then - log1 patch -p1 -i "$PATCHES/$basename.patch" + log1 patch -p1 -i "$PATCHES/$basename.patch" || exit 1 fi # Go back to base folder @@ -1146,7 +1147,8 @@ function make_menhir { make_ocaml make_findlib make_ocamlbuild - if build_prep http://gallium.inria.fr/~fpottier/menhir menhir-20180530 tar.gz 1 ; then + # This is the version required by latest CompCert + if build_prep https://gitlab.inria.fr/fpottier/menhir/-/archive/20190626 menhir-20190626 tar.gz 1 ; then # Note: menhir doesn't support -j 8, so don't pass MAKE_OPT log2 make all PREFIX="$PREFIXOCAML" log2 make install PREFIX="$PREFIXOCAML" @@ -1154,6 +1156,29 @@ function make_menhir { fi } +##### CAMLP5 Ocaml Preprocessor ##### + +function make_camlp5 { + make_ocaml + make_findlib + + if build_prep https://github.com/camlp5/camlp5/archive rel707 tar.gz 1 camlp5-rel707; then + logn configure ./configure + # Somehow my virus scanner has the boot.new/SAVED directory locked after the move for a second => repeat until success + sed -i 's/mv boot.new boot/until mv boot.new boot; do sleep 1; done/' Makefile + # shellcheck disable=SC2086 + log1 make world.opt $MAKE_OPT + log2 make install + log2 make clean + # For some reason META is not built / copied, but it is required + log2 make -C etc META + mkdir -p "$PREFIXOCAML/libocaml/site-lib/camlp5/" + cp etc/META "$PREFIXOCAML/libocaml/site-lib/camlp5/" + log2 make clean + build_post + fi +} + ##### LABLGTK Ocaml GTK binding ##### # Note: when rebuilding lablgtk by deleting the .finished file, @@ -1805,8 +1830,9 @@ function make_addon_coquelicot { installer_addon_dependency_beg coquelicot make_addon_ssreflect installer_addon_dependency_end - if build_prep_overlay Coquelicot; then + if build_prep_overlay coquelicot; then installer_addon_section coquelicot "Coquelicot" "Coq library for real analysis" "" + logn autogen ./autogen.sh logn configure ./configure --libdir="$PREFIXCOQ/lib/coq/user-contrib/Coquelicot" logn remake ./remake logn remake-install ./remake install @@ -1867,6 +1893,84 @@ function make_addon_quickchick { fi } +# Flocq: Floating point library + +function make_addon_flocq { + if build_prep_overlay Flocq; then + installer_addon_section flocq "Flocq" "Coq library for floating point arithmetic" "" + logn autogen ./autogen.sh + logn configure ./configure + logn remake ./remake --jobs=$MAKE_THREADS + logn install ./remake install + build_post + fi +} + +# Coq-Interval: interval arithmetic and inequality proofs + +function make_addon_interval { + installer_addon_dependency_beg interval + make_addon_mathcomp + make_addon_coquelicot + make_addon_bignums + make_addon_flocq + installer_addon_dependency_end + if build_prep_overlay interval; then + installer_addon_section interval "Interval" "Coq library and tactic for proving real inequalities" "" + logn autogen ./autogen.sh + logn configure ./configure + logn remake ./remake --jobs=$MAKE_THREADS + logn install ./remake install + build_post + fi +} + +# Gappa: Automatic generation of arithmetic proofs (mostly on limited precision arithmetic) + +function install_boost { + # The extra tar parameter extracts only the boost headers, not the boost library source code (which is huge and takes a long time) + if build_prep https://dl.bintray.com/boostorg/release/1.69.0/source boost_1_69_0 tar.gz 1 boost_1_69_0 boost boost_1_69_0/boost; then + # Move extracted boost folder where mingw-gcc can find it + mv boost /usr/$TARGET_ARCH/sys-root/mingw/include + build_post + fi +} + +function copy_gappa_dlls { + copy_coq_dll LIBGMP-10.DLL + copy_coq_dll LIBMPFR-6.DLL + copy_coq_dll LIBSTDC++-6.DLL +} + +function make_addon_gappa_tool { + install_boost + if build_prep_overlay gappa_tool; then + installer_addon_section gappa_tool "Gappa tool" "Stand alone tool for automated generation of numerical arithmetic proofs" "" + logn autogen ./autogen.sh + logn configure ./configure --build="$HOST" --host="$HOST" --target="$TARGET" --prefix="$PREFIXCOQ" + logn remake ./remake --jobs=$MAKE_THREADS + logn install ./remake -d install + log1 copy_gappa_dlls + build_post + fi +} + +function make_addon_gappa { + make_camlp5 + installer_addon_dependency_beg gappa + make_addon_gappa_tool + make_addon_flocq + installer_addon_dependency_end + if build_prep_overlay gappa_plugin ; then + installer_addon_section gappa "Gappa plugin" "Coq plugin for the Gappa tool" "" + logn autogen ./autogen.sh + logn configure ./configure + logn remake ./remake + logn install ./remake install + build_post + fi +} + # Main function for building addons function make_addons { diff --git a/dev/build/windows/patches_coq/VST.patch b/dev/build/windows/patches_coq/VST.patch index 2c8c46373f..d047eb107f 100644 --- a/dev/build/windows/patches_coq/VST.patch +++ b/dev/build/windows/patches_coq/VST.patch @@ -1,8 +1,7 @@ diff --git a/Makefile b/Makefile -index 4a119042..fdfac13e 100755 --- a/Makefile +++ b/Makefile -@@ -76,8 +76,8 @@ endif +@@ -82,8 +82,8 @@ endif COMPCERTDIRS=lib common $(ARCHDIRS) cfrontend flocq exportclight $(BACKEND) @@ -10,6 +9,6 @@ index 4a119042..fdfac13e 100755 -EXTFLAGS= $(foreach d, $(COMPCERTDIRS), -Q $(COMPCERT)/$(d) compcert.$(d)) +COMPCERT_R_FLAGS= $(foreach d, $(COMPCERTDIRS), -R $(COMPCERT)/$(d) VST.compcert.$(d)) +EXTFLAGS= $(foreach d, $(COMPCERTDIRS), -Q $(COMPCERT)/$(d) VST.compcert.$(d)) - - # for SSReflect - ifdef MATHCOMP + # for ITrees + ifeq ($(wildcard InteractionTrees/the?ries),"InteractionTrees/theories") + EXTFLAGS:=$(EXTFLAGS) -Q InteractionTrees/theories ITree diff --git a/dev/build/windows/patches_coq/quickchick.patch b/dev/build/windows/patches_coq/quickchick.patch index 1afa6e7f95..4b7b86ff05 100644 --- a/dev/build/windows/patches_coq/quickchick.patch +++ b/dev/build/windows/patches_coq/quickchick.patch @@ -1,12 +1,12 @@ -diff/patch file created on Mon, Aug 27, 2018 9:21:52 AM with: -difftar-folder.sh tarballs/quickchick-v1.0.2.tar.gz quickchick-v1.0.2 1 -TARFILE= tarballs/quickchick-v1.0.2.tar.gz -FOLDER= quickchick-v1.0.2 +diff/patch file created on Wed, Jul 17, 2019 8:06:45 PM with: +difftar-folder.sh tarballs/quickchick-741fb98eb865129a70c4ef7a64db2739c4a5eab0.tar.gz quickchick-741fb98eb865129a70c4ef7a64db2739c4a5eab0 1 +TARFILE= tarballs/quickchick-741fb98eb865129a70c4ef7a64db2739c4a5eab0.tar.gz +FOLDER= quickchick-741fb98eb865129a70c4ef7a64db2739c4a5eab0 TARSTRIP= 1 -TARPREFIX= QuickChick-1.0.2/ -ORIGFOLDER= quickchick-v1.0.2.orig ---- quickchick-v1.0.2.orig/Makefile 2018-08-22 18:21:39.000000000 +0200 -+++ quickchick-v1.0.2/Makefile 2018-08-27 09:21:04.710461100 +0200 +TARPREFIX= QuickChick-741fb98eb865129a70c4ef7a64db2739c4a5eab0/ +ORIGFOLDER= quickchick-741fb98eb865129a70c4ef7a64db2739c4a5eab0.orig +--- quickchick-741fb98eb865129a70c4ef7a64db2739c4a5eab0.orig/Makefile 2019-06-26 12:09:01.000000000 +0200 ++++ quickchick-741fb98eb865129a70c4ef7a64db2739c4a5eab0/Makefile 2019-07-17 20:05:44.322251200 +0200 @@ -2,7 +2,7 @@ .PHONY: plugin install install-plugin clean quickChickTool @@ -16,11 +16,32 @@ ORIGFOLDER= quickchick-v1.0.2.orig QCTOOL_SRC=$(QCTOOL_DIR)/quickChickTool.ml \ $(QCTOOL_DIR)/quickChickToolTypes.ml \ $(QCTOOL_DIR)/quickChickToolLexer.mll \ +@@ -20,8 +20,8 @@ + + all: quickChickTool plugin documentation-check + +-plugin: Makefile.coq +- $(MAKE) -f Makefile.coq ++plugin: Makefile.coq ++ $(MAKE) -f Makefile.coq + + documentation-check: plugin + coqc -R src QuickChick -I src QuickChickInterface.v @@ -32,7 +32,7 @@ install: all $(V)$(MAKE) -f Makefile.coq install > $(TEMPFILE) # Manually copying the remaining files -- $(V)cp $(QCTOOL_EXE) $(shell opam config var bin)/quickChick -+ $(V)cp $(QCTOOL_EXE) "$(COQBIN)/quickChick" +- $(V)cp $(QCTOOL_DIR)/$(QCTOOL_EXE) $(shell opam config var bin)/quickChick ++ $(V)cp $(QCTOOL_DIR)/$(QCTOOL_EXE) "$(COQBIN)/quickChick" # $(V)cp src/quickChickLib.cmx $(COQLIB)/user-contrib/QuickChick # $(V)cp src/quickChickLib.o $(COQLIB)/user-contrib/QuickChick + +@@ -56,7 +56,7 @@ + $(MAKE) -C examples/RedBlack test + # cd examples/stlc; make clean && make + $(MAKE) -C examples/multifile-mutation test +-# This takes too long. ++# This takes too long. + # $(MAKE) -C examples/c-mutation test + # coqc examples/BSTTest.v + coqc examples/DependentTest.v diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index fa39b41565..dadb2bb8f1 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -102,6 +102,27 @@ : "${coquelicot_CI_ARCHIVEURL:=${coquelicot_CI_GITURL}/-/archive}" ######################################################################## +# Coq-interval +######################################################################## +: "${interval_CI_REF:=master}" +: "${interval_CI_GITURL:=https://gitlab.inria.fr/coqinterval/interval}" +: "${interval_CI_ARCHIVEURL:=${interval_CI_GITURL}/-/archive}" + +######################################################################## +# Gappa stand alone tool +######################################################################## +: "${gappa_tool_CI_REF:=master}" +: "${gappa_tool_CI_GITURL:=https://gitlab.inria.fr/gappa/gappa}" +: "${gappa_tool_CI_ARCHIVEURL:=${gappa_tool_CI_GITURL}/-/archive}" + +######################################################################## +# Gappa plugin +######################################################################## +: "${gappa_plugin_CI_REF:=master}" +: "${gappa_plugin_CI_GITURL:=https://gitlab.inria.fr/gappa/coq}" +: "${gappa_plugin_CI_ARCHIVEURL:=${gappa_plugin_CI_GITURL}/-/archive}" + +######################################################################## # CompCert ######################################################################## : "${compcert_CI_REF:=master}" diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat index 6c4ccfc14d..3998fc6514 100755 --- a/dev/ci/gitlab.bat +++ b/dev/ci/gitlab.bat @@ -48,9 +48,13 @@ IF "%WINDOWS%" == "enabled_all_addons" ( -addon=compcert ^
-addon=extlib ^
-addon=quickchick ^
+ -addon=coquelicot ^
-addon=vst ^
- -addon=aactactics
-REM -addon=coquelicot ^
+ -addon=aactactics ^
+ -addon=flocq ^
+ -addon=interval ^
+ -addon=gappa_tool ^
+ -addon=gappa
) ELSE (
SET "EXTRA_ADDONS= "
)
diff --git a/dev/ci/user-overlays/10441-ppedrot-static-poly-section.sh b/dev/ci/user-overlays/10441-ppedrot-static-poly-section.sh new file mode 100644 index 0000000000..00f544f894 --- /dev/null +++ b/dev/ci/user-overlays/10441-ppedrot-static-poly-section.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "10441" ] || [ "$CI_BRANCH" = "static-poly-section" ]; then + + ext_lib_CI_REF=static-poly-section + ext_lib_CI_GITURL=https://github.com/ppedrot/coq-ext-lib + +fi diff --git a/dev/shim/dune b/dev/shim/dune index e307848292..84b2e642e8 100644 --- a/dev/shim/dune +++ b/dev/shim/dune @@ -4,7 +4,7 @@ %{bin:coqtop} %{project_root}/theories/Init/Prelude.vo) (action - (with-outputs-to coqtop-prelude + (with-stdout-to coqtop-prelude (progn (echo "#!/usr/bin/env bash\n") (bash "echo \"$(pwd)/%{bin:coqtop} -coqlib $(pwd)/%{project_root}\" \\$@") @@ -16,7 +16,7 @@ %{bin:coqc} %{project_root}/theories/Init/Prelude.vo) (action - (with-outputs-to coqc-prelude + (with-stdout-to coqc-prelude (progn (echo "#!/usr/bin/env bash\n") (bash "echo \"$(pwd)/%{bin:coqc} -coqlib $(pwd)/%{project_root}\" \\$@") @@ -29,7 +29,7 @@ %{lib:coq.kernel:../../stublibs/dllbyterun_stubs.so} %{project_root}/theories/Init/Prelude.vo) (action - (with-outputs-to %{targets} + (with-stdout-to %{targets} (progn (echo "#!/usr/bin/env bash\n") (bash "echo \"$(pwd)/%{bin:coqtop.byte} -coqlib $(pwd)/%{project_root}\" \\$@") @@ -45,7 +45,7 @@ %{project_root}/coqide-server.install %{project_root}/coqide.install) (action - (with-outputs-to coqide-prelude + (with-stdout-to coqide-prelude (progn (echo "#!/usr/bin/env bash\n") (bash "echo \"$(pwd)/%{bin:coqide} -coqlib $(pwd)/%{project_root}\" \\$@") diff --git a/doc/changelog/02-specification-language/10441-static-poly-section.rst b/doc/changelog/02-specification-language/10441-static-poly-section.rst new file mode 100644 index 0000000000..7f0345d946 --- /dev/null +++ b/doc/changelog/02-specification-language/10441-static-poly-section.rst @@ -0,0 +1,11 @@ +- The universe polymorphism setting now applies from the opening of a section. + In particular, it is not possible anymore to mix polymorphic and monomorphic + definitions in a section when there are no variables nor universe constraints + defined in this section. This makes the behaviour consistent with the + documentation. (`#10441 <https://github.com/coq/coq/pull/10441>`_, + by Pierre-Marie Pédrot) + +- The :cmd:`Section` vernacular command now accepts the "universes" attribute. In + addition to setting the section universe polymorphism, it also locally sets + the universe polymorphic option inside the section. + (`#10441 <https://github.com/coq/coq/pull/10441>`_, by Pierre-Marie Pédrot) diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 395b5ce2d3..7e698bfb66 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -144,6 +144,8 @@ Many other commands support the ``Polymorphic`` flag, including: - ``Lemma``, ``Axiom``, and all the other “definition” keywords support polymorphism. +- :cmd:`Section` will locally set the polymorphism flag inside the section. + - ``Variables``, ``Context``, ``Universe`` and ``Constraint`` in a section support polymorphism. This means that the universe variables (and associated constraints) are discharged polymorphically over definitions that use diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index fd84868a1f..6ac55e7bf4 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -102,10 +102,10 @@ reference manual. Here are the most important user-visible changes: extensionality lemma: - interactive mode: :n:`under @term`, associated terminator: :tacn:`over` - - one-liner mode: `under @term do [@tactic | ...]` + - one-liner mode: :n:`under @term do [@tactic | ...]` It can take occurrence switches, contextual patterns, and intro patterns: - :g:`under {2}[in RHS]eq_big => [i|i ?] do ...` + :g:`under {2}[in RHS]eq_big => [i|i ?]` (`#9651 <https://github.com/coq/coq/pull/9651>`_, by Erik Martin-Dorel and Enrico Tassi). diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index efb5df720a..7d6171285e 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -88,8 +88,6 @@ There are other buttons on the |CoqIDE| toolbar: a button to save the running buffer; a button to close the current buffer (an "X"); buttons to switch among buffers (left and right arrows); an "information" button; and a "gears" button. -The "information" button is described in Section :ref:`try-tactics-automatically`. - The "gears" button submits proof terms to the |Coq| kernel for type checking. When |Coq| uses asynchronous processing (see Chapter :ref:`asynchronousandparallelproofprocessing`), proofs may have been completed without kernel-checking of generated proof terms. @@ -100,27 +98,6 @@ processed color, though their preceding proofs have the processed color. Notice that for all these buttons, except for the "gears" button, their operations are also available in the menu, where their keyboard shortcuts are given. -.. _try-tactics-automatically: - -Trying tactics automatically ------------------------------- - -The menu Try Tactics provides some features for automatically trying -to solve the current goal using simple tactics. If such a tactic -succeeds in solving the goal, then its text is automatically inserted -into the script. There is finally a combination of these tactics, -called the *proof wizard* which will try each of them in turn. This -wizard is also available as a tool button (the "information" button). The set of -tactics tried by the wizard is customizable in the preferences. - -These tactics are general ones, in particular they do not refer to -particular hypotheses. You may also try specific tactics related to -the goal or one of the hypotheses, by clicking with the right mouse -button on the goal or the considered hypothesis. This is the -“contextual menu on goals” feature, that may be disabled in the -preferences if undesirable. - - Proof folding ------------------ @@ -202,13 +179,6 @@ compilation, printing, web browsing. In the browser command, you may use `%s` to denote the URL to open, for example: `firefox -remote "OpenURL(%s)"`. -The `Tactics Wizard` section allows defining the set of tactics that -should be tried, in sequence, to solve the current goal. - -The last section is for miscellaneous boolean settings, such as the -“contextual menu on goals” feature presented in the section -:ref:`Try tactics automatically <try-tactics-automatically>`. - Notice that these settings are saved in the file `.coqiderc` of your home directory. diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 1b9e3ce0f3..ed980bd4de 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -3761,10 +3761,10 @@ involves the following steps: 5. If so :tacn:`under` protects these n goals against an accidental instantiation of the evar. - These protected goals are displayed using the ``Under[ … ]`` - notation (e.g. ``Under[ m - m ]`` in the running example). + These protected goals are displayed using the ``'Under[ … ]`` + notation (e.g. ``'Under[ m - m ]`` in the running example). -6. The expression inside the ``Under[ … ]`` notation can be +6. The expression inside the ``'Under[ … ]`` notation can be proved equivalent to the desired expression by using a regular :tacn:`rewrite` tactic. @@ -3782,7 +3782,7 @@ The over tactic Two equivalent facilities (a terminator and a lemma) are provided to close intermediate subgoals generated by :tacn:`under` (i.e. goals -displayed as ``Under[ … ]``): +displayed as ``'Under[ … ]``): .. tacn:: over :name: over @@ -3792,7 +3792,7 @@ displayed as ``Under[ … ]``): .. tacv:: by rewrite over - This is a variant of :tacn:`over` in order to close ``Under[ … ]`` + This is a variant of :tacn:`over` in order to close ``'Under[ … ]`` goals, relying on the ``over`` rewrite rule. .. _under_one_liner: diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 5f3e82938d..774732825a 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -870,26 +870,6 @@ interactively, they cannot be part of a vernacular file loaded via have to undo some extra commands and end on a state :n:`@num′ ≤ @num` if necessary. - .. cmdv:: Backtrack @num @num @num - :name: Backtrack - - .. deprecated:: 8.4 - - :cmd:`Backtrack` is a *deprecated* form of - :cmd:`BackTo` which allows explicitly manipulating the proof environment. The - three numbers represent the following: - - + *first number* : State label to reach, as for :cmd:`BackTo`. - + *second number* : *Proof state number* to unbury once aborts have been done. - |Coq| will compute the number of :cmd:`Undo` to perform (see Chapter :ref:`proofhandling`). - + *third number* : Number of :cmd:`Abort` to perform, i.e. the number of currently - opened nested proofs that must be canceled (see Chapter :ref:`proofhandling`). - - .. exn:: Invalid backtrack. - - The destination state label is unknown. - - .. _quitting-and-debugging: Quitting and debugging diff --git a/ide/MacOS/default_accel_map b/ide/MacOS/default_accel_map index 54a592a04d..6bcf3b438f 100644 --- a/ide/MacOS/default_accel_map +++ b/ide/MacOS/default_accel_map @@ -7,7 +7,6 @@ ; (gtk_accel_path "<Actions>/Templates/Template Program Lemma" "") (gtk_accel_path "<Actions>/Templates/Lemma" "<Shift><Primary>l") ; (gtk_accel_path "<Actions>/Templates/Template Fact" "") -(gtk_accel_path "<Actions>/Tactics/auto" "<Primary><Control>a") ; (gtk_accel_path "<Actions>/Tactics/Tactic fold" "") ; (gtk_accel_path "<Actions>/Help/About Coq" "") ; (gtk_accel_path "<Actions>/Templates/Template Add Ring A Aplus Amult Aone Azero Ainv Aeq T [ c1 ... cn ]. " "") @@ -19,7 +18,6 @@ ; (gtk_accel_path "<Actions>/Tactics/Tactic inversion" "") ; (gtk_accel_path "<Actions>/Templates/Template Write State" "") ; (gtk_accel_path "<Actions>/Export/Export to" "") -(gtk_accel_path "<Actions>/Tactics/auto with *" "<Primary><Control>asterisk") ; (gtk_accel_path "<Actions>/Tactics/Tactic inversion--clear" "") ; (gtk_accel_path "<Actions>/Templates/Template Implicit Arguments" "") ; (gtk_accel_path "<Actions>/Edit/Copy" "<Primary>c") @@ -50,7 +48,6 @@ ; (gtk_accel_path "<Actions>/Tactics/Tactic fail" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic left" "") (gtk_accel_path "<Actions>/Edit/Undo" "<Primary>u") -(gtk_accel_path "<Actions>/Tactics/eauto with *" "<Primary><Control>ampersand") ; (gtk_accel_path "<Actions>/Templates/Template Infix" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic functional induction" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic clear" "") @@ -149,7 +146,6 @@ (gtk_accel_path "<Actions>/Templates/Theorem" "<Shift><Primary>t") ; (gtk_accel_path "<Actions>/Templates/Template Derive Dependent Inversion--clear" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic unfold" "") -; (gtk_accel_path "<Actions>/Tactics/Try Tactics" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic red in" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic rewrite <- -- in" "") ; (gtk_accel_path "<Actions>/Templates/Template Hint Extern" "") @@ -187,7 +183,6 @@ ; (gtk_accel_path "<Actions>/Tactics/Tactic intro -- after" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic fold -- in" "") ; (gtk_accel_path "<Actions>/Templates/Template Program Definition" "") -(gtk_accel_path "<Actions>/Tactics/Wizard" "<Primary><Control>dollar") ; (gtk_accel_path "<Actions>/Templates/Template Hint Resolve" "") ; (gtk_accel_path "<Actions>/Templates/Template Set Extraction Optimize" "") ; (gtk_accel_path "<Actions>/File/Revert all buffers" "") @@ -228,7 +223,6 @@ ; (gtk_accel_path "<Actions>/Export/Html" "") ; (gtk_accel_path "<Actions>/Templates/Template Extraction Inline" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic absurd" "") -(gtk_accel_path "<Actions>/Tactics/intuition" "<Primary><Control>i") ; (gtk_accel_path "<Actions>/Tactics/Tactic simple induction" "") ; (gtk_accel_path "<Actions>/Queries/Queries" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic rewrite -- in" "") @@ -289,7 +283,6 @@ ; (gtk_accel_path "<Actions>/Templates/Template Add Field" "") ; (gtk_accel_path "<Actions>/Templates/Template Require Export" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic rewrite <-" "") -(gtk_accel_path "<Actions>/Tactics/omega" "<Primary><Control>o") ; (gtk_accel_path "<Actions>/Tactics/Tactic split" "") ; (gtk_accel_path "<Actions>/File/Quit" "<Primary>q") (gtk_accel_path "<Actions>/View/Display existential variable instances" "<Shift><Control>e") @@ -328,7 +321,6 @@ ; (gtk_accel_path "<Actions>/Edit/Edit" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic firstorder" "") ; (gtk_accel_path "<Actions>/Templates/Template C" "") -(gtk_accel_path "<Actions>/Tactics/simpl" "<Primary><Control>s") ; (gtk_accel_path "<Actions>/Tactics/Tactic replace -- with" "") ; (gtk_accel_path "<Actions>/Templates/Template A" "") ; (gtk_accel_path "<Actions>/Templates/Template Remove Printing Record" "") @@ -360,13 +352,11 @@ ; (gtk_accel_path "<Actions>/File/File" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic setoid--replace" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic generalize dependent" "") -(gtk_accel_path "<Actions>/Tactics/trivial" "<Primary><Control>v") ; (gtk_accel_path "<Actions>/Tactics/Tactic fix -- with" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic pose --:=--)" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic auto with" "") ; (gtk_accel_path "<Actions>/Templates/Template Add Printing Record" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic inversion -- in" "") -(gtk_accel_path "<Actions>/Tactics/eauto" "<Primary><Control>e") ; (gtk_accel_path "<Actions>/File/Open" "<Primary>o") ; (gtk_accel_path "<Actions>/Tactics/Tactic elim -- using" "") ; (gtk_accel_path "<Actions>/Templates/Template Hint" "") diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 566654218d..d52f038f1f 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -137,7 +137,6 @@ class type ops = object method go_to_insert : unit task method go_to_mark : GText.mark -> unit task - method tactic_wizard : string list -> unit task method process_next_phrase : unit task method process_until_end_or_error : unit task method handle_reset_initial : unit task @@ -806,48 +805,6 @@ object(self) else Coq.seq (self#backtrack_to_iter ~move_insert:false point) (Coq.lift (fun () -> Sentence.tag_on_insert buffer))) - method tactic_wizard l = - let insert_phrase phrase tag = - let stop = self#get_start_of_input in - let phrase' = if stop#starts_line then phrase else "\n"^phrase in - buffer#insert ~iter:stop phrase'; - Sentence.tag_on_insert buffer; - let start = self#get_start_of_input in - buffer#move_mark ~where:stop (`NAME "start_of_input"); - buffer#apply_tag tag ~start ~stop; - if self#get_insert#compare stop <= 0 then - buffer#place_cursor ~where:stop; - let sentence = - mk_sentence - ~start:(`MARK (buffer#create_mark start)) - ~stop:(`MARK (buffer#create_mark stop)) - [] in - Doc.push document sentence; - messages#default_route#clear; - self#show_goals - in - let display_error (loc, s) = - messages#default_route#add (Ideutils.validate s) in - let try_phrase phrase stop more = - let action = log "Sending to coq now" in - let route_id = 0 in - let query = Coq.query (route_id,(phrase,Stateid.dummy)) in - let next = function - | Fail (_, l, str) -> (* FIXME: check *) - display_error (l, str); - messages#default_route#add (Pp.str ("Unsuccessfully tried: "^phrase)); - more - | Good () -> stop Tags.Script.processed - in - Coq.bind (Coq.seq action query) next - in - let rec loop l = match l with - | [] -> Coq.return () - | p :: l' -> - try_phrase ("progress "^p^".") (insert_phrase (p^".")) (loop l') - in - loop l - method handle_reset_initial = let action () = (* clear the stack *) diff --git a/ide/coqOps.mli b/ide/coqOps.mli index 83ad8c15dc..1e8d87bb15 100644 --- a/ide/coqOps.mli +++ b/ide/coqOps.mli @@ -15,7 +15,6 @@ class type ops = object method go_to_insert : unit task method go_to_mark : GText.mark -> unit task - method tactic_wizard : string list -> unit task method process_next_phrase : unit task method process_until_end_or_error : unit task method handle_reset_initial : unit task diff --git a/ide/coqide.ml b/ide/coqide.ml index 8d95dcee27..2c9f116cc3 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -603,9 +603,6 @@ module Nav = struct let join_document _ = send_to_coq (fun sn -> sn.coqops#join_document) end -let tactic_wizard_callback l _ = - send_to_coq (fun sn -> sn.coqops#tactic_wizard l) - let printopts_callback opts v = let b = v#get_active in let () = List.iter (fun o -> Coq.PrintOpt.set o b) opts in @@ -1106,25 +1103,8 @@ let build_ui () = ("Force", "_Force", `EXECUTE, Nav.join_document, "Fully check the document", "f"); ] end; - let tacitem s sc = - item s ~label:("_"^s) - ~accel:(modifier_for_tactics#get^sc) - ~callback:(tactic_wizard_callback [s]) - in menu tactics_menu [ - item "Try Tactics" ~label:"_Try Tactics"; - item "Wizard" ~label:"<Proof Wizard>" ~stock:`DIALOG_INFO - ~tooltip:"Proof Wizard" ~accel:(modifier_for_tactics#get^"dollar") - ~callback:(tactic_wizard_callback automatic_tactics#get); - tacitem "auto" "a"; - tacitem "auto with *" "asterisk"; - tacitem "eauto" "e"; - tacitem "eauto with *" "ampersand"; - tacitem "intuition" "i"; - tacitem "omega" "o"; - tacitem "simpl" "s"; - tacitem "tauto" "p"; - tacitem "trivial" "v"; + item "Tactics" ~label:"_Tactics"; ]; alpha_items tactics_menu "Tactic" Coq_commands.tactics; diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml index d4a339f4f5..452808490d 100644 --- a/ide/coqide_ui.ml +++ b/ide/coqide_ui.ml @@ -100,18 +100,7 @@ let init () = \n <menuitem action='Previous' />\ \n <menuitem action='Next' />\ \n </menu>\ -\n <menu action='Try Tactics'>\ -\n <menuitem action='auto' />\ -\n <menuitem action='auto with *' />\ -\n <menuitem action='eauto' />\ -\n <menuitem action='eauto with *' />\ -\n <menuitem action='intuition' />\ -\n <menuitem action='omega' />\ -\n <menuitem action='simpl' />\ -\n <menuitem action='tauto' />\ -\n <menuitem action='trivial' />\ -\n <menuitem action='Wizard' />\ -\n <separator />\ +\n <menu action='Tactics'>\ \n %s\ \n </menu>\ \n <menu action='Templates'>\ @@ -173,7 +162,6 @@ let init () = \n <toolitem action='Interrupt' />\ \n <toolitem action='Previous' />\ \n <toolitem action='Next' />\ -\n <toolitem action='Wizard' />\ \n</toolbar>\ \n</ui>" (if Coq_config.gtk_platform <> `QUARTZ then "<menuitem action='Quit' />" else "") diff --git a/ide/preferences.ml b/ide/preferences.ml index ea0495bb19..bf9fe8922a 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -938,16 +938,6 @@ let configure ?(apply=(fun () -> ())) parent = else cmd_browse#get]) cmd_browse#get in -(* - let automatic_tactics = - strings - ~f:automatic_tactics#set - ~add:(fun () -> ["<edit me>"]) - "Wizard tactics to try in order" - automatic_tactics#get - - in -*) let contextual_menus_on_goal = pbool "Contextual menus on goal" contextual_menus_on_goal in @@ -1008,10 +998,6 @@ let configure ?(apply=(fun () -> ())) parent = Section("Externals", None, [cmd_coqtop;cmd_coqc;cmd_make;cmd_coqmakefile; cmd_coqdoc; cmd_print;cmd_editor;cmd_browse]); -(* - Section("Tactics Wizard", None, - [automatic_tactics]); -*) Section("Shortcuts", Some `PREFERENCES, [modifiers_valid; modifier_for_tactics; modifier_for_templates; modifier_for_display; modifier_for_navigation; diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 1cc3dc3975..3fd613e905 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -1075,7 +1075,7 @@ module FNativeEntries = let mkInt env i = check_int env; - { mark = mark Norm KnownR; term = FInt i } + { mark = mark Cstr KnownR; term = FInt i } let mkBool env b = check_bool env; diff --git a/library/lib.ml b/library/lib.ml index d461644d56..59b55cc16b 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -427,46 +427,60 @@ type secentry = | Variable of { id:Names.Id.t; kind:Decl_kinds.binding_kind; - poly:bool; univs:Univ.ContextSet.t; } | Context of Univ.ContextSet.t -let sectab = - Summary.ref ([] : (secentry list * Opaqueproof.work_list * abstr_list) list) - ~name:"section-context" +type section_data = { + sec_entry : secentry list; + sec_workl : Opaqueproof.work_list; + sec_abstr : abstr_list; + sec_poly : bool; +} -let add_section () = - sectab := ([],(Names.Cmap.empty,Names.Mindmap.empty), - (Names.Cmap.empty,Names.Mindmap.empty)) :: !sectab +let empty_section_data ~poly = { + sec_entry = []; + sec_workl = (Names.Cmap.empty,Names.Mindmap.empty); + sec_abstr = (Names.Cmap.empty,Names.Mindmap.empty); + sec_poly = poly; +} -let check_same_poly p vars = - let pred = function Context _ -> p = false | Variable {poly} -> p != poly in - if List.exists pred vars then +let sectab = + Summary.ref ([] : section_data list) ~name:"section-context" + +let check_same_poly p sec = + if p != sec.sec_poly then user_err Pp.(str "Cannot mix universe polymorphic and monomorphic declarations in sections.") +let add_section ~poly () = + List.iter (fun tab -> check_same_poly poly tab) !sectab; + sectab := empty_section_data ~poly :: !sectab + let add_section_variable ~name ~kind ~poly univs = match !sectab with | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *) - | (vars,repl,abs)::sl -> - List.iter (fun tab -> check_same_poly poly (pi1 tab)) !sectab; - sectab := (Variable {id=name;kind;poly;univs}::vars,repl,abs)::sl + | s :: sl -> + List.iter (fun tab -> check_same_poly poly tab) !sectab; + let s = { s with sec_entry = Variable {id=name;kind;univs} :: s.sec_entry } in + sectab := s :: sl let add_section_context ctx = match !sectab with | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *) - | (vars,repl,abs)::sl -> - check_same_poly true vars; - sectab := (Context ctx :: vars,repl,abs)::sl + | s :: sl -> + check_same_poly true s; + let s = { s with sec_entry = Context ctx :: s.sec_entry } in + sectab := s :: sl exception PolyFound of bool (* make this a let exception once possible *) let is_polymorphic_univ u = try let open Univ in - List.iter (fun (vars,_,_) -> + List.iter (fun s -> + let vars = s.sec_entry in List.iter (function - | Variable {poly;univs=(univs,_)} -> - if LSet.mem u univs then raise (PolyFound poly) + | Variable {univs=(univs,_)} -> + if LSet.mem u univs then raise (PolyFound s.sec_poly) | Context (univs,_) -> if LSet.mem u univs then raise (PolyFound true) ) vars @@ -474,12 +488,12 @@ let is_polymorphic_univ u = false with PolyFound b -> b -let extract_hyps (secs,ohyps) = +let extract_hyps poly (secs,ohyps) = let rec aux = function - | (Variable {id;kind;poly;univs}::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) -> + | (Variable {id;kind;univs}::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) -> let l, r = aux (idl,hyps) in (decl,kind) :: l, if poly then Univ.ContextSet.union r univs else r - | (Variable {poly;univs}::idl,hyps) -> + | (Variable {univs}::idl,hyps) -> let l, r = aux (idl,hyps) in l, if poly then Univ.ContextSet.union r univs else r | (Context ctx :: idl, hyps) -> @@ -511,9 +525,9 @@ let name_instance inst = let add_section_replacement f g poly hyps = match !sectab with | [] -> () - | (vars,exps,abs)::sl -> - let () = check_same_poly poly vars in - let sechyps,ctx = extract_hyps (vars,hyps) in + | s :: sl -> + let () = check_same_poly poly s in + let sechyps,ctx = extract_hyps s.sec_poly (s.sec_entry, hyps) in let ctx = Univ.ContextSet.to_context ctx in let inst = Univ.UContext.instance ctx in let nas = name_instance inst in @@ -524,7 +538,11 @@ let add_section_replacement f g poly hyps = abstr_subst = subst; abstr_uctx = ctx; } in - sectab := (vars,f (inst,args) exps, g info abs) :: sl + let s = { s with + sec_workl = f (inst, args) s.sec_workl; + sec_abstr = g info s.sec_abstr; + } in + sectab := s :: sl let add_section_kn ~poly kn = let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in @@ -534,13 +552,13 @@ let add_section_constant ~poly kn = let f x (l1,l2) = (Names.Cmap.add kn x l1,l2) in add_section_replacement f f poly -let replacement_context () = pi2 (List.hd !sectab) +let replacement_context () = (List.hd !sectab).sec_workl let section_segment_of_constant con = - Names.Cmap.find con (fst (pi3 (List.hd !sectab))) + Names.Cmap.find con (fst (List.hd !sectab).sec_abstr) let section_segment_of_mutual_inductive kn = - Names.Mindmap.find kn (snd (pi3 (List.hd !sectab))) + Names.Mindmap.find kn (snd (List.hd !sectab).sec_abstr) let empty_segment = { abstr_ctx = []; @@ -563,20 +581,20 @@ let section_instance = let open GlobRef in function | Variable {id=id'} -> Names.Id.equal id id' | Context _ -> false in - if List.exists eq (pi1 (List.hd !sectab)) + if List.exists eq (List.hd !sectab).sec_entry then Univ.Instance.empty, [||] else raise Not_found | ConstRef con -> - Names.Cmap.find con (fst (pi2 (List.hd !sectab))) + Names.Cmap.find con (fst (List.hd !sectab).sec_workl) | IndRef (kn,_) | ConstructRef ((kn,_),_) -> - Names.Mindmap.find kn (snd (pi2 (List.hd !sectab))) + Names.Mindmap.find kn (snd (List.hd !sectab).sec_workl) let is_in_section ref = try ignore (section_instance ref); true with Not_found -> false (*************) (* Sections. *) -let open_section id = +let open_section ~poly id = let opp = !lib_state.path_prefix in let obj_dir = add_dirpath_suffix opp.Nametab.obj_dir id in let prefix = Nametab.{ obj_dir; obj_mp = opp.obj_mp; obj_sec = add_dirpath_suffix opp.obj_sec id } in @@ -587,7 +605,7 @@ let open_section id = (*Pushed for the lifetime of the section: removed by unfrozing the summary*) Nametab.(push_dir (Until 1) obj_dir (GlobDirRef.DirOpenSection prefix)); lib_state := { !lib_state with path_prefix = prefix }; - add_section () + add_section ~poly () (* Restore lib_stk and summaries as before the section opening, and diff --git a/library/lib.mli b/library/lib.mli index 01366ddfd0..fe6bf69ec4 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -147,7 +147,7 @@ val library_part : GlobRef.t -> DirPath.t (** {6 Sections } *) -val open_section : Id.t -> unit +val open_section : poly:bool -> Id.t -> unit val close_section : unit -> unit (** {6 We can get and set the state of the operations (used in [States]). } *) diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg index 5f859b3e4b..1b75d3d966 100644 --- a/plugins/funind/g_indfun.mlg +++ b/plugins/funind/g_indfun.mlg @@ -148,9 +148,7 @@ END module Vernac = Pvernac.Vernac_ module Tactic = Pltac -type function_rec_definition_loc_argtype = (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) Loc.located - -let (wit_function_rec_definition_loc : function_rec_definition_loc_argtype Genarg.uniform_genarg_type) = +let (wit_function_rec_definition_loc : Vernacexpr.fixpoint_expr Loc.located Genarg.uniform_genarg_type) = Genarg.create_arg "function_rec_definition_loc" let function_rec_definition_loc = @@ -175,10 +173,10 @@ let () = let is_proof_termination_interactively_checked recsl = List.exists (function - | _,((_,( Some { CAst.v = CMeasureRec _ } - | Some { CAst.v = CWfRec _}),_,_,_),_) -> true - | _,((_,Some { CAst.v = CStructRec _ },_,_,_),_) - | _,((_,None,_,_,_),_) -> false) recsl + | _,( Vernacexpr.{ rec_order = Some { CAst.v = CMeasureRec _ } } + | Vernacexpr.{ rec_order = Some { CAst.v = CWfRec _} }) -> true + | _, Vernacexpr.{ rec_order = Some { CAst.v = CStructRec _ } } + | _, Vernacexpr.{ rec_order = None } -> false) recsl let classify_as_Fixpoint recsl = Vernac_classifier.classify_vernac diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 6e19ef4804..1987677d7d 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -1,3 +1,13 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + open CErrors open Sorts open Util @@ -157,17 +167,16 @@ let interp_casted_constr_with_implicits env sigma impls c = and not as a constr *) -let build_newrecursive - lnameargsardef = +let build_newrecursive lnameargsardef = let env0 = Global.env() in let sigma = Evd.from_env env0 in let (rec_sign,rec_impls) = List.fold_left - (fun (env,impls) (({CAst.v=recname},_),bl,arityc,_) -> - let arityc = Constrexpr_ops.mkCProdN bl arityc in + (fun (env,impls) { Vernacexpr.fname={CAst.v=recname}; binders; rtype } -> + let arityc = Constrexpr_ops.mkCProdN binders rtype in let arity,ctx = Constrintern.interp_type env0 sigma arityc in let evd = Evd.from_env env0 in - let evd, (_, (_, impls')) = Constrintern.interp_context_evars ~program_mode:false env evd bl in + let evd, (_, (_, impls')) = Constrintern.interp_context_evars ~program_mode:false env evd binders in let impl = Constrintern.compute_internalization_data env0 evd Constrintern.Recursive arity impls' in let open Context.Named.Declaration in let r = Sorts.Relevant in (* TODO relevance *) @@ -175,26 +184,18 @@ let build_newrecursive (env0,Constrintern.empty_internalization_env) lnameargsardef in let recdef = (* Declare local notations *) - let f (_,bl,_,def) = - let def = abstract_glob_constr def bl in - interp_casted_constr_with_implicits - rec_sign sigma rec_impls def + let f { Vernacexpr.binders; body_def } = + match body_def with + | Some body_def -> + let def = abstract_glob_constr body_def binders in + interp_casted_constr_with_implicits + rec_sign sigma rec_impls def + | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in States.with_state_protection (List.map f) lnameargsardef in recdef,rec_impls -let build_newrecursive l = - let l' = List.map - (fun ((fixna,_,bll,ar,body_opt),lnot) -> - match body_opt with - | Some body -> - (fixna,bll,ar,body) - | None -> user_err ~hdr:"Function" (str "Body of Function must be given") - ) l - in - build_newrecursive l' - let error msg = user_err Pp.(str msg) (* Checks whether or not the mutual bloc is recursive *) @@ -237,8 +238,8 @@ let rec local_binders_length = function | Constrexpr.CLocalAssum (idl,_,_)::bl -> List.length idl + local_binders_length bl | Constrexpr.CLocalPattern _::bl -> assert false -let prepare_body ((name,_,args,types,_),_) rt = - let n = local_binders_length args in +let prepare_body { Vernacexpr.binders; rtype } rt = + let n = local_binders_length binders in (* Pp.msgnl (str "nb lambda to chop : " ++ str (string_of_int n) ++ fnl () ++Printer.pr_glob_constr rt); *) let fun_args,rt' = chop_rlambda_n n rt in (fun_args,rt') @@ -336,13 +337,13 @@ let error_error names e = | _ -> raise e let generate_principle (evd:Evd.evar_map ref) pconstants on_error - is_general do_built (fix_rec_l:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) recdefs interactive_proof + is_general do_built (fix_rec_l : Vernacexpr.fixpoint_expr list) recdefs interactive_proof (continue_proof : int -> Names.Constant.t array -> EConstr.constr array -> int -> Tacmach.tactic) : unit = - let names = List.map (function (({CAst.v=name},_),_,_,_,_),_ -> name) fix_rec_l in + let names = List.map (function { Vernacexpr.fname = {CAst.v=name} } -> name) fix_rec_l in let fun_bodies = List.map2 prepare_body fix_rec_l recdefs in let funs_args = List.map fst fun_bodies in - let funs_types = List.map (function ((_,_,_,types,_),_) -> types) fix_rec_l in + let funs_types = List.map (function { Vernacexpr.rtype } -> rtype) fix_rec_l in try (* We then register the Inductive graphs of the functions *) Glob_term_to_relation.build_inductive !evd pconstants funs_args funs_types recdefs; @@ -359,7 +360,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error locate_ind f_R_mut) in - let fname_kn (((fname,_),_,_,_,_),_) = + let fname_kn { Vernacexpr.fname } = let f_ref = qualid_of_ident ?loc:fname.CAst.loc fname.CAst.v in locate_with_msg (pr_qualid f_ref++str ": Not an inductive type!") @@ -398,23 +399,25 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error with e when CErrors.noncritical e -> on_error names e -let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = +let register_struct is_rec (fixpoint_exprl: Vernacexpr.fixpoint_expr list) = match fixpoint_exprl with - | [(({CAst.v=fname},pl),_,bl,ret_type,body),_] when not is_rec -> - let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in + | [ { Vernacexpr.fname; univs; binders; rtype; body_def } ] when not is_rec -> + let body = match body_def with + | Some body -> body + | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in ComDefinition.do_definition ~program_mode:false - ~name:fname + ~name:fname.CAst.v ~poly:false ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) - ~kind:Decls.Definition pl - bl None body (Some ret_type); + ~kind:Decls.Definition univs + binders None body (Some rtype); let evd,rev_pconstants = List.fold_left - (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) -> + (fun (evd,l) { Vernacexpr.fname } -> let evd,c = Evd.fresh_global - (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in + (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname.CAst.v)) in let (cst, u) = destConst evd c in let u = EInstance.kind evd u in evd,((cst, u) :: l) @@ -427,10 +430,10 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp ComFixpoint.do_fixpoint ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~poly:false fixpoint_exprl; let evd,rev_pconstants = List.fold_left - (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) -> + (fun (evd,l) { Vernacexpr.fname } -> let evd,c = Evd.fresh_global - (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in + (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname.CAst.v)) in let (cst, u) = destConst evd c in let u = EInstance.kind evd u in evd,((cst, u) :: l) @@ -464,7 +467,7 @@ let register_wf interactive_proof ?(is_mes=false) fname rec_impls wf_rel_expr wf let unbounded_eq = let f_app_args = CAst.make @@ Constrexpr.CAppExpl( - (None,qualid_of_ident fname,None) , + (None,qualid_of_ident fname.CAst.v,None) , (List.map (function | {CAst.v=Anonymous} -> assert false @@ -485,13 +488,13 @@ let register_wf interactive_proof ?(is_mes=false) fname rec_impls wf_rel_expr wf (generate_correction_proof_wf f_ref tcc_lemma_ref is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation ); - derive_inversion [fname] + derive_inversion [fname.CAst.v] with e when CErrors.noncritical e -> (* No proof done *) () in Recdef.recursive_definition ~interactive_proof - ~is_mes fname rec_impls + ~is_mes fname.CAst.v rec_impls type_of_f wf_rel_expr rec_arg_num @@ -607,88 +610,93 @@ and rebuild_nal aux bk bl' nal typ = let rebuild_bl aux bl typ = rebuild_bl aux bl typ -let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = - let fixl,ntns = ComFixpoint.extract_fixpoint_components ~structonly:false fixpoint_exprl in - let ((_,_,_,typel),_,ctx,_) = ComFixpoint.interp_fixpoint ~cofix:false fixl ntns in +let recompute_binder_list fixpoint_exprl = + let fixl = + List.map (fun fix -> Vernacexpr.{ + fix + with rec_order = ComFixpoint.adjust_rec_order ~structonly:false fix.binders fix.rec_order }) fixpoint_exprl in + let ((_,_,_,typel),_,ctx,_) = ComFixpoint.interp_fixpoint ~cofix:false fixl in let constr_expr_typel = with_full_print (List.map (fun c -> Constrextern.extern_constr false (Global.env ()) (Evd.from_ctx ctx) (EConstr.of_constr c))) typel in let fixpoint_exprl_with_new_bl = - List.map2 (fun ((lna,rec_order_opt,bl,ret_typ,opt_body),notation_list) fix_typ -> - - let new_bl',new_ret_type = rebuild_bl [] bl fix_typ in - (((lna,rec_order_opt,new_bl',new_ret_type,opt_body),notation_list):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list)) - ) - fixpoint_exprl constr_expr_typel + List.map2 (fun ({ Vernacexpr.binders } as fp) fix_typ -> + let binders, rtype = rebuild_bl [] binders fix_typ in + { fp with Vernacexpr.binders; rtype } + ) fixpoint_exprl constr_expr_typel in fixpoint_exprl_with_new_bl let do_generate_principle_aux pconstants on_error register_built interactive_proof - (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) : Lemmas.t option = - List.iter (fun (_,l) -> if not (List.is_empty l) then error "Function does not support notations for now") fixpoint_exprl; + (fixpoint_exprl : Vernacexpr.fixpoint_expr list) : Lemmas.t option = + List.iter (fun { Vernacexpr.notations } -> + if not (List.is_empty notations) + then error "Function does not support notations for now") fixpoint_exprl; let lemma, _is_struct = match fixpoint_exprl with - | [((_,Some {CAst.v = Constrexpr.CWfRec (wf_x,wf_rel)},_,_,_),_) as fixpoint_expr] -> - let (((({CAst.v=name},pl),_,args,types,body)),_) as fixpoint_expr = - match recompute_binder_list [fixpoint_expr] with - | [e] -> e - | _ -> assert false - in - let fixpoint_exprl = [fixpoint_expr] in - let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in - let recdefs,rec_impls = build_newrecursive fixpoint_exprl in - let using_lemmas = [] in - let pre_hook pconstants = - generate_principle - (ref (Evd.from_env (Global.env ()))) - pconstants - on_error - true - register_built - fixpoint_exprl - recdefs - true - in - if register_built - then register_wf interactive_proof name rec_impls wf_rel wf_x.CAst.v using_lemmas args types body pre_hook, false - else None, false - |[((_,Some {CAst.v = Constrexpr.CMeasureRec(wf_x,wf_mes,wf_rel_opt)},_,_,_),_) as fixpoint_expr] -> - let (((({CAst.v=name},_),_,args,types,body)),_) as fixpoint_expr = - match recompute_binder_list [fixpoint_expr] with - | [e] -> e - | _ -> assert false - in - let fixpoint_exprl = [fixpoint_expr] in - let recdefs,rec_impls = build_newrecursive fixpoint_exprl in - let using_lemmas = [] in - let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in - let pre_hook pconstants = - generate_principle - (ref (Evd.from_env (Global.env ()))) - pconstants - on_error - true - register_built - fixpoint_exprl - recdefs - true - in - if register_built - then register_mes interactive_proof name rec_impls wf_mes wf_rel_opt (map_option (fun x -> x.CAst.v) wf_x) using_lemmas args types body pre_hook, true - else None, true + | [{ Vernacexpr.rec_order = Some {CAst.v = Constrexpr.CWfRec (wf_x,wf_rel)} } as fixpoint_expr] -> + let { Vernacexpr.fname; univs; binders; rtype; body_def } as fixpoint_expr = + match recompute_binder_list [fixpoint_expr] with + | [e] -> e + | _ -> assert false + in + let fixpoint_exprl = [fixpoint_expr] in + let body = match body_def with + | Some body -> body + | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in + let recdefs,rec_impls = build_newrecursive fixpoint_exprl in + let using_lemmas = [] in + let pre_hook pconstants = + generate_principle + (ref (Evd.from_env (Global.env ()))) + pconstants + on_error + true + register_built + fixpoint_exprl + recdefs + true + in + if register_built + then register_wf interactive_proof fname rec_impls wf_rel wf_x.CAst.v using_lemmas binders rtype body pre_hook, false + else None, false + |[{ Vernacexpr.rec_order=Some {CAst.v = Constrexpr.CMeasureRec(wf_x,wf_mes,wf_rel_opt)} } as fixpoint_expr] -> + let { Vernacexpr.fname; univs; binders; rtype; body_def} as fixpoint_expr = + match recompute_binder_list [fixpoint_expr] with + | [e] -> e + | _ -> assert false + in + let fixpoint_exprl = [fixpoint_expr] in + let recdefs,rec_impls = build_newrecursive fixpoint_exprl in + let using_lemmas = [] in + let body = match body_def with + | Some body -> body + | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in + let pre_hook pconstants = + generate_principle + (ref (Evd.from_env (Global.env ()))) + pconstants + on_error + true + register_built + fixpoint_exprl + recdefs + true + in + if register_built + then register_mes interactive_proof fname rec_impls wf_mes wf_rel_opt (map_option (fun x -> x.CAst.v) wf_x) using_lemmas binders rtype body pre_hook, true + else None, true | _ -> - List.iter (function ((_na,ord,_args,_body,_type),_not) -> - match ord with - | Some { CAst.v = (Constrexpr.CMeasureRec _ | Constrexpr.CWfRec _) } -> - error - ("Cannot use mutual definition with well-founded recursion or measure") - | _ -> () + List.iter (function { Vernacexpr.rec_order } -> + match rec_order with + | Some { CAst.v = (Constrexpr.CMeasureRec _ | Constrexpr.CWfRec _) } -> + error + ("Cannot use mutual definition with well-founded recursion or measure") + | _ -> () ) fixpoint_exprl; let fixpoint_exprl = recompute_binder_list fixpoint_exprl in - let fix_names = - List.map (function ((({CAst.v=name},_),_,_,_,_),_) -> name) fixpoint_exprl - in + let fix_names = List.map (function { Vernacexpr.fname } -> fname.CAst.v) fixpoint_exprl in (* ok all the expressions are structural *) let recdefs,rec_impls = build_newrecursive fixpoint_exprl in let is_rec = List.exists (is_rec fix_names) recdefs in @@ -845,59 +853,59 @@ let make_graph (f_ref : GlobRef.t) = | None -> error "Cannot build a graph over an axiom!" | Some (body, _, _) -> let env = Global.env () in - let extern_body,extern_type = - with_full_print (fun () -> - (Constrextern.extern_constr false env sigma (EConstr.of_constr body), - Constrextern.extern_type false env sigma - (EConstr.of_constr (*FIXME*) c_body.const_type) - ) + let extern_body,extern_type = + with_full_print (fun () -> + (Constrextern.extern_constr false env sigma (EConstr.of_constr body), + Constrextern.extern_type false env sigma + (EConstr.of_constr (*FIXME*) c_body.const_type) ) - () - in - let (nal_tas,b,t) = get_args extern_body extern_type in - let expr_list = - match b.CAst.v with - | Constrexpr.CFix(l_id,fixexprl) -> - let l = - List.map - (fun (id,recexp,bl,t,b) -> - let { CAst.loc; v=rec_id } = match Option.get recexp with - | { CAst.v = CStructRec id } -> id - | { CAst.v = CWfRec (id,_) } -> id - | { CAst.v = CMeasureRec (oid,_,_) } -> Option.get oid - in - let new_args = - List.flatten - (List.map - (function - | Constrexpr.CLocalDef (na,_,_)-> [] - | Constrexpr.CLocalAssum (nal,_,_) -> - List.map - (fun {CAst.loc;v=n} -> CAst.make ?loc @@ - CRef(Libnames.qualid_of_ident ?loc @@ Nameops.Name.get_id n,None)) - nal - | Constrexpr.CLocalPattern _ -> assert false - ) - nal_tas - ) - in - let b' = add_args id.CAst.v new_args b in - ((((id,None), ( Some (CAst.make (CStructRec (CAst.make rec_id)))),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list)) - ) - fixexprl + ) () + in + let (nal_tas,b,t) = get_args extern_body extern_type in + let expr_list = + match b.CAst.v with + | Constrexpr.CFix(l_id,fixexprl) -> + let l = + List.map + (fun (id,recexp,bl,t,b) -> + let { CAst.loc; v=rec_id } = match Option.get recexp with + | { CAst.v = CStructRec id } -> id + | { CAst.v = CWfRec (id,_) } -> id + | { CAst.v = CMeasureRec (oid,_,_) } -> Option.get oid + in + let new_args = + List.flatten + (List.map + (function + | Constrexpr.CLocalDef (na,_,_)-> [] + | Constrexpr.CLocalAssum (nal,_,_) -> + List.map + (fun {CAst.loc;v=n} -> CAst.make ?loc @@ + CRef(Libnames.qualid_of_ident ?loc @@ Nameops.Name.get_id n,None)) + nal + | Constrexpr.CLocalPattern _ -> assert false + ) + nal_tas + ) in - l - | _ -> - let id = Label.to_id (Constant.label c) in - [((CAst.make id,None),None,nal_tas,t,Some b),[]] - in - let mp = Constant.modpath c in - let pstate = do_generate_principle_aux [c,Univ.Instance.empty] error_error false false expr_list in - assert (Option.is_empty pstate); - (* We register the infos *) - List.iter - (fun ((({CAst.v=id},_),_,_,_,_),_) -> add_Function false (Constant.make2 mp (Label.of_id id))) - expr_list) + let b' = add_args id.CAst.v new_args b in + { Vernacexpr.fname=id; univs=None + ; rec_order = Some (CAst.make (CStructRec (CAst.make rec_id))) + ; binders = nal_tas@bl; rtype=t; body_def=Some b'; notations = []} + ) fixexprl in + l + | _ -> + let fname = CAst.make (Label.to_id (Constant.label c)) in + [{ Vernacexpr.fname; univs=None; rec_order = None; binders=nal_tas; rtype=t; body_def=Some b; notations=[]}] + in + let mp = Constant.modpath c in + let pstate = do_generate_principle_aux [c,Univ.Instance.empty] error_error false false expr_list in + assert (Option.is_empty pstate); + (* We register the infos *) + List.iter + (fun { Vernacexpr.fname= {CAst.v=id} } -> + add_Function false (Constant.make2 mp (Label.of_id id))) + expr_list) (* *************** statically typed entrypoints ************************* *) diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index 3bc52272ac..bfc9686ae5 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -5,12 +5,9 @@ val warn_cannot_define_graph : ?loc:Loc.t -> Pp.t * Pp.t -> unit val warn_cannot_define_principle : ?loc:Loc.t -> Pp.t * Pp.t -> unit -val do_generate_principle : - (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> unit +val do_generate_principle : Vernacexpr.fixpoint_expr list -> unit -val do_generate_principle_interactive : - (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> - Lemmas.t +val do_generate_principle_interactive : Vernacexpr.fixpoint_expr list -> Lemmas.t val functional_induction : bool -> diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 858a75698a..c09250ade5 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -68,6 +68,25 @@ DECLARE PLUGIN "ssreflect_plugin" { +let ssrtac_name name = { + mltac_plugin = "ssreflect_plugin"; + mltac_tactic = "ssr" ^ name; +} + +let ssrtac_entry name = { + mltac_name = ssrtac_name name; + mltac_index = 0; +} + +let register_ssrtac name f = + Tacenv.register_ml_tactic (ssrtac_name name) [|f|] + +let cast_arg wit v = Taccoerce.Value.cast (Genarg.topwit wit) v + +} + +{ + (* Defining grammar rules with "xx" in it automatically declares keywords too, * we thus save the lexer to restore it at the end of the file *) let frozen_lexer = CLexer.get_keyword_state () ;; @@ -969,14 +988,17 @@ ARGUMENT EXTEND ssrintrosarg TYPED AS (tactic * ssrintros) | [ "YouShouldNotTypeThis" ssrtacarg(arg) ssrintros_ne(ipats) ] -> { arg, ipats } END -TACTIC EXTEND ssrtclintros -| [ "YouShouldNotTypeThis" ssrintrosarg(arg) ] -> - { let tac, intros = arg in - ssrevaltac ist tac <*> tclIPATssr intros } -END - { +let () = register_ssrtac "tclintros" begin fun args ist -> match args with +| [arg] -> + let arg = cast_arg wit_ssrintrosarg arg in + let tac, intros = arg in + ssrevaltac ist tac <*> tclIPATssr intros +| _ -> assert false +end + + (** Defined identifier *) let pr_ssrfwdid id = pr_spc () ++ pr_id id @@ -1701,16 +1723,6 @@ let _ = add_internal_name (is_tagged perm_tag) type ssrargfmt = ArgSsr of string | ArgSep of string -let ssrtac_name name = { - mltac_plugin = "ssreflect_plugin"; - mltac_tactic = "ssr" ^ name; -} - -let ssrtac_entry name n = { - mltac_name = ssrtac_name name; - mltac_index = n; -} - let set_pr_ssrtac name prec afmt = (* FIXME *) () (* let fmt = List.map (function | ArgSep s -> Egramml.GramTerminal s @@ -1718,8 +1730,7 @@ let set_pr_ssrtac name prec afmt = (* FIXME *) () (* | ArgCoq at -> Egramml.GramTerminal "COQ_ARG") afmt in let tacname = ssrtac_name name in () *) -let ssrtac_atom ?loc name args = TacML (CAst.make ?loc (ssrtac_entry name 0, args)) -let ssrtac_expr ?loc name args = ssrtac_atom ?loc name args +let ssrtac_expr ?loc name args = TacML (CAst.make ?loc (ssrtac_entry name, args)) let tclintros_expr ?loc tac ipats = let args = [Tacexpr.TacGeneric (in_gen (rawwit wit_ssrintrosarg) (tac, ipats))] in @@ -1802,15 +1813,15 @@ END (** The "do" tactical. ********************************************************) -(* -type ssrdoarg = ((ssrindex * ssrmmod) * ssrhint) * ssrclauses -*) -TACTIC EXTEND ssrtcldo -| [ "YouShouldNotTypeThis" "do" ssrdoarg(arg) ] -> { V82.tactic (ssrdotac ist arg) } -END - { +let () = register_ssrtac "tcldo" begin fun args ist -> match args with +| [arg] -> + let arg = cast_arg wit_ssrdoarg arg in + V82.tactic (ssrdotac ist arg) +| _ -> assert false +end + let _ = set_pr_ssrtac "tcldo" 3 [ArgSep "do "; ArgSsr "doarg"] let ssrdotac_expr ?loc n m tac clauses = @@ -1849,13 +1860,17 @@ let pr_ssrseqdir _ _ _ = function ARGUMENT EXTEND ssrseqdir TYPED AS ssrdir PRINTED BY { pr_ssrseqdir } END -TACTIC EXTEND ssrtclseq -| [ "YouShouldNotTypeThis" ssrtclarg(tac) ssrseqdir(dir) ssrseqarg(arg) ] -> - { V82.tactic (tclSEQAT ist tac dir arg) } -END - { +let () = register_ssrtac "tclseq" begin fun args ist -> match args with +| [tac; dir; arg] -> + let tac = cast_arg wit_ssrtclarg tac in + let dir = cast_arg wit_ssrseqdir dir in + let arg = cast_arg wit_ssrseqarg arg in + V82.tactic (tclSEQAT ist tac dir arg) +| _ -> assert false +end + let _ = set_pr_ssrtac "tclseq" 5 [ArgSsr "tclarg"; ArgSsr "seqdir"; ArgSsr "seqarg"] let tclseq_expr ?loc tac dir arg = diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index a82eff9cf0..be21a3a60d 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1310,27 +1310,27 @@ let set_of_evctx l = (** Weaken the existentials so that they can be typed in sign and raise an error if the term otherwise mentions variables not bound in sign. *) let thin_evars env sigma sign c = - let evdref = ref sigma in + let sigma = ref sigma in let ctx = set_of_evctx sign in let rec applyrec (env,acc) t = - match kind sigma t with + match kind !sigma t with | Evar (ev, args) -> - let evi = Evd.find_undefined sigma ev in - let filter = Array.map (fun c -> Id.Set.subset (collect_vars sigma c) ctx) args in + let evi = Evd.find_undefined !sigma ev in + let filter = Array.map (fun c -> Id.Set.subset (collect_vars !sigma c) ctx) args in let filter = Filter.make (Array.to_list filter) in let candidates = Option.map (List.map EConstr.of_constr) (evar_candidates evi) in - let evd, ev = restrict_evar !evdref ev filter candidates in - evdref := evd; whd_evar !evdref t + let evd, ev = restrict_evar !sigma ev filter candidates in + sigma := evd; whd_evar !sigma t | Var id -> - if not (Id.Set.mem id ctx) then raise (TypingFailed sigma) + if not (Id.Set.mem id ctx) then raise (TypingFailed !sigma) else t | _ -> - map_constr_with_binders_left_to_right !evdref + map_constr_with_binders_left_to_right !sigma (fun d (env,acc) -> (push_rel d env, acc+1)) applyrec (env,acc) t in let c' = applyrec (env,0) c in - (!evdref, c') + (!sigma, c') let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = try diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 00831b5962..a9eb43e573 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -839,8 +839,9 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e unify_app_pattern true curenvnb pb opt substn cM f1 l1 cN f2 l2 | _ -> raise ex) - | Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) -> - (try + | Case (ci1,p1,c1,cl1), Case (ci2,p2,c2,cl2) -> + (try + if not (eq_ind ci1.ci_ind ci2.ci_ind) then error_cannot_unify curenv sigma (cM,cN); let opt' = {opt with at_top = true; with_types = false} in Array.fold_left2 (unirec_rec curenvnb CONV {opt with at_top = true}) (unirec_rec curenvnb CONV opt' diff --git a/stm/stm.ml b/stm/stm.ml index d5e6e6fd8b..69dbebbc57 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1073,7 +1073,7 @@ let stm_vernac_interp ?route id st { verbose; expr } : Vernacstate.t = *) let is_filtered_command = function | VernacResetName _ | VernacResetInitial | VernacBack _ - | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _ + | VernacRestart | VernacUndo _ | VernacUndoTo _ | VernacAbortAll | VernacAbort _ -> true | _ -> false in @@ -1216,8 +1216,6 @@ end = struct (* {{{ *) match Vcs_.branches vcs with [_] -> `Stop id | _ -> `Cont ()) () id in oid - | VernacBackTo id -> - Stateid.of_int id | _ -> anomaly Pp.(str "incorrect VtMeta classification") with | Not_found -> diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index aaba36287a..5af576dad2 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -106,8 +106,8 @@ let classify_vernac e = else GuaranteesOpacity in let ids, open_proof = - List.fold_left (fun (l,b) ((({v=id},_),_,_,_,p),_) -> - id::l, b || p = None) ([],false) l in + List.fold_left (fun (l,b) {Vernacexpr.fname={CAst.v=id}; body_def} -> + id::l, b || body_def = None) ([],false) l in if open_proof then VtStartProof (guarantee,ids) else VtSideff (ids, VtLater) @@ -118,8 +118,8 @@ let classify_vernac e = else GuaranteesOpacity in let ids, open_proof = - List.fold_left (fun (l,b) ((({v=id},_),_,_,p),_) -> - id::l, b || p = None) ([],false) l in + List.fold_left (fun (l,b) { Vernacexpr.fname={CAst.v=id}; body_def } -> + id::l, b || body_def = None) ([],false) l in if open_proof then VtStartProof (guarantee,ids) else VtSideff (ids, VtLater) @@ -193,7 +193,7 @@ let classify_vernac e = | VernacBack _ | VernacAbortAll | VernacUndoTo _ | VernacUndo _ | VernacResetName _ | VernacResetInitial - | VernacBackTo _ | VernacRestart -> VtMeta + | VernacRestart -> VtMeta (* What are these? *) | VernacRestoreState _ | VernacWriteState _ -> VtSideff ([], VtNow) diff --git a/test-suite/bugs/closed/HoTT_coq_020.v b/test-suite/bugs/closed/HoTT_coq_020.v index 73da464bbe..babd180209 100644 --- a/test-suite/bugs/closed/HoTT_coq_020.v +++ b/test-suite/bugs/closed/HoTT_coq_020.v @@ -26,6 +26,7 @@ Ltac present_obj from to := | [ |- context[from ?obj ?C] ] => progress change (from obj C) with (to obj C) in * end. +#[universes(polymorphic)] Section NaturalTransformationComposition. Set Universe Polymorphism. Context `(C : @Category objC). @@ -58,6 +59,7 @@ Polymorphic Definition Cat0 : Category Empty_set Polymorphic Definition FunctorFrom0 objC (C : Category objC) : Functor Cat0 C := Build_Functor Cat0 C (fun x => match x with end). +#[universes(polymorphic)] Section Law0. Polymorphic Variable objC : Type. Polymorphic Variable C : Category objC. diff --git a/test-suite/bugs/closed/HoTT_coq_098.v b/test-suite/bugs/closed/HoTT_coq_098.v index bdcd8ba97d..3b58605575 100644 --- a/test-suite/bugs/closed/HoTT_coq_098.v +++ b/test-suite/bugs/closed/HoTT_coq_098.v @@ -21,6 +21,7 @@ Polymorphic Definition GraphIndexingCategory : @SpecializedCategory GraphIndex. Admitted. Module success. + #[universes(polymorphic)] Section SpecializedFunctor. Set Universe Polymorphism. Context `(C : @SpecializedCategory objC). @@ -39,6 +40,7 @@ Module success. End success. Module success2. + #[universes(polymorphic)] Section SpecializedFunctor. Polymorphic Context `(C : @SpecializedCategory objC). Polymorphic Context `(D : @SpecializedCategory objD). diff --git a/test-suite/bugs/closed/bug_10300.v b/test-suite/bugs/closed/bug_10300.v new file mode 100644 index 0000000000..374c2cf967 --- /dev/null +++ b/test-suite/bugs/closed/bug_10300.v @@ -0,0 +1,14 @@ +Set Implicit Arguments. + +Definition hprop := nat -> Prop. + +Definition himpl := fun H1 H2 : hprop => forall (h : nat), H1 h -> H2 h. + +Parameter himpl_refl : forall H : hprop, himpl H H. + +Parameter hstar : hprop -> hprop -> hprop. + +Parameter hpure : hprop. + +Lemma test : (forall (H:hprop), himpl (hstar H H) hpure -> True) -> True. +Proof. intros M. eapply M. apply himpl_refl. Abort. diff --git a/test-suite/bugs/closed/bug_10533.v b/test-suite/bugs/closed/bug_10533.v new file mode 100644 index 0000000000..e72957bdee --- /dev/null +++ b/test-suite/bugs/closed/bug_10533.v @@ -0,0 +1,8 @@ + +Require Import Eqdep Setoid. +Goal forall (t : unit) (pf : tt = t), + if (match pf with eq_refl => false end) then True else False. +Proof. + intros. + try setoid_rewrite <-Eqdep.Eq_rect_eq.eq_rect_eq. +Abort. diff --git a/test-suite/bugs/closed/bug_10560.v b/test-suite/bugs/closed/bug_10560.v new file mode 100644 index 0000000000..a9a0949d9a --- /dev/null +++ b/test-suite/bugs/closed/bug_10560.v @@ -0,0 +1,9 @@ +From Coq Require Import Int63. +Open Scope int63_scope. + +Lemma foo : + let n := opp 0 in add n 0 = n. +Proof. +cbv. +apply eq_refl. +Qed. diff --git a/test-suite/bugs/closed/bug_3314.v b/test-suite/bugs/closed/bug_3314.v index a5782298c3..794de93b37 100644 --- a/test-suite/bugs/closed/bug_3314.v +++ b/test-suite/bugs/closed/bug_3314.v @@ -24,10 +24,10 @@ Fail Eval compute in Lift nat : Prop. (* = nat : Prop *) -Section Hurkens. +Monomorphic Definition Type2 := Type. +Monomorphic Definition Type1 := Type : Type2. - Monomorphic Definition Type2 := Type. - Monomorphic Definition Type1 := Type : Type2. +Section Hurkens. (** Assumption of a retract from Type into Prop *) diff --git a/test-suite/bugs/closed/bug_4503.v b/test-suite/bugs/closed/bug_4503.v index 26731e3292..c53d4cabc7 100644 --- a/test-suite/bugs/closed/bug_4503.v +++ b/test-suite/bugs/closed/bug_4503.v @@ -5,11 +5,12 @@ Class PreOrder (A : Type) (r : A -> A -> Type) : Type := (* FAILURE 1 *) +#[universes(polymorphic)] Section foo. Polymorphic Universes A. Polymorphic Context {A : Type@{A}} {rA : A -> A -> Prop} {PO : PreOrder A rA}. - Fail Definition foo := PO. + Fail Monomorphic Definition foo := PO. End foo. @@ -30,8 +31,9 @@ End ILogic. Set Printing Universes. (* There is still a problem if the class is universe polymorphic *) +#[universes(polymorphic)] Section Embed_ILogic_Pre. Polymorphic Universes A T. - Fail Context {A : Type@{A}} {ILA: ILogic.ILogic@{A} A}. + Fail Monomorphic Context {A : Type@{A}} {ILA: ILogic.ILogic@{A} A}. End Embed_ILogic_Pre. diff --git a/test-suite/bugs/closed/bug_4816.v b/test-suite/bugs/closed/bug_4816.v index 00a523842e..0bb05e77ce 100644 --- a/test-suite/bugs/closed/bug_4816.v +++ b/test-suite/bugs/closed/bug_4816.v @@ -1,18 +1,21 @@ +#[universes(polymorphic)] Section foo. Polymorphic Universes A B. -Fail Constraint A <= B. +Fail Monomorphic Constraint A <= B. End foo. (* gives an anomaly Universe undefined *) Universes X Y. +#[universes(polymorphic)] Section Foo. Polymorphic Universes Z W. Polymorphic Constraint W < Z. - Fail Definition bla := Type@{W}. + Fail Monomorphic Definition bla := Type@{W}. Polymorphic Definition bla := Type@{W}. + #[universes(polymorphic)] Section Bar. - Fail Constraint X <= Z. + Fail Monomorphic Constraint X <= Z. End Bar. End Foo. @@ -21,9 +24,11 @@ Require Coq.Classes.RelationClasses. Class PreOrder (A : Type) (r : A -> A -> Type) : Type := { refl : forall x, r x x }. +#[universes(polymorphic)] Section qux. Polymorphic Universes A. + #[universes(polymorphic)] Section bar. - Fail Context {A : Type@{A}} {rA : A -> A -> Prop} {PO : PreOrder A rA}. + Fail Monomorphic Context {A : Type@{A}} {rA : A -> A -> Prop} {PO : PreOrder A rA}. End bar. End qux. diff --git a/test-suite/misc/universes/dune b/test-suite/misc/universes/dune index 0772f95604..c0d925deb5 100644 --- a/test-suite/misc/universes/dune +++ b/test-suite/misc/universes/dune @@ -1,8 +1,9 @@ (rule (targets all_stdlib.v) (deps + build_all_stdlib.sh (source_tree ../../../theories) (source_tree ../../../plugins)) (action - (with-outputs-to all_stdlib.v + (with-stdout-to all_stdlib.v (bash "./build_all_stdlib.sh")))) diff --git a/test-suite/success/namedunivs.v b/test-suite/success/namedunivs.v index f9154ef576..01a2136652 100644 --- a/test-suite/success/namedunivs.v +++ b/test-suite/success/namedunivs.v @@ -6,6 +6,7 @@ Unset Strict Universe Declaration. +#[universes(polymorphic)] Section lift_strict. Polymorphic Definition liftlt := let t := Type@{i} : Type@{k} in diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v index 339f798240..9ab8ace39e 100644 --- a/test-suite/success/polymorphism.v +++ b/test-suite/success/polymorphism.v @@ -122,8 +122,6 @@ Fail Definition id1impred := ((forall A : Type1, A) : Type1). End Hierarchy. -Section structures. - Record hypo : Type := mkhypo { hypo_type : Type; hypo_proof : hypo_type @@ -154,9 +152,6 @@ Polymorphic Definition nest (d : dyn) := {| dyn_proof := d |}. Polymorphic Definition twoprojs (d : dyn) := dyn_proof d = dyn_proof d. -End structures. - - Module binders. Definition mynat@{|} := nat. @@ -201,7 +196,8 @@ Module binders. Definition with_mono@{u|u < M} : Type@{M} := Type@{u}. End binders. - + +#[universes(polymorphic)] Section cats. Local Set Universe Polymorphism. Require Import Utf8. @@ -307,6 +303,7 @@ Fail Check (let A := Set in fooS (id A)). Fail Check (let A := Prop in fooS (id A)). (* Some tests of sort-polymorphisme *) +#[universes(polymorphic)] Section S. Polymorphic Variable A:Type. (* diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v index 9bb16b97e2..c81ba02230 100644 --- a/theories/Numbers/Cyclic/Int63/Int63.v +++ b/theories/Numbers/Cyclic/Int63/Int63.v @@ -812,14 +812,6 @@ Proof. eapply Z.lt_le_trans; [ | apply Zpower2_le_lin ]; auto with zarith. Qed. -Lemma lsr_add_distr x y n: (x + y) << n = ((x << n) + (y << n))%int63. -Proof. - apply to_Z_inj. - rewrite -> add_spec, !lsl_spec, add_spec. - rewrite -> Zmult_mod_idemp_l, <-Zplus_mod. - apply f_equal2 with (f := Zmod); auto with zarith. -Qed. - (* LSL *) Lemma lsl0 i: 0 << i = 0%int63. Proof. @@ -1119,7 +1111,7 @@ Proof. generalize (add_le_r x y); rewrite Heq, lor_le; intro Hb. generalize Heq; rewrite (bit_split x) at 1; rewrite (bit_split y )at 1; clear Heq. rewrite (fun y => add_comm y (bit x 0)), <-!add_assoc, add_comm, - <-!add_assoc, (add_comm (bit y 0)), add_assoc, <-lsr_add_distr. + <-!add_assoc, (add_comm (bit y 0)), add_assoc, <-lsl_add_distr. rewrite (bit_split (x lor y)), lor_spec. intros Heq. assert (F: (bit x 0 + bit y 0)%int63 = (bit x 0 || bit y 0)). diff --git a/theories/Reals/Rtrigo_calc.v b/theories/Reals/Rtrigo_calc.v index 5ed60b0a0f..2428fc495d 100644 --- a/theories/Reals/Rtrigo_calc.v +++ b/theories/Reals/Rtrigo_calc.v @@ -178,7 +178,7 @@ Proof. change (cos (PI / 4) <> 0); rewrite cos_PI4; apply R1_sqrt2_neq_0. Qed. -Lemma cos3PI4 : cos (3 * (PI / 4)) = -1 / sqrt 2. +Lemma cos_3PI4 : cos (3 * (PI / 4)) = -1 / sqrt 2. Proof. replace (3 * (PI / 4)) with (PI / 2 - - (PI / 4)) by field. rewrite cos_shift; rewrite sin_neg; rewrite sin_PI4. @@ -186,12 +186,16 @@ Proof. ring. Qed. -Lemma sin3PI4 : sin (3 * (PI / 4)) = 1 / sqrt 2. +#[deprecated(since="8.10",note="Use cos_3PI4 instead.")] Notation cos3PI4 := cos_3PI4. + +Lemma sin_3PI4 : sin (3 * (PI / 4)) = 1 / sqrt 2. Proof. replace (3 * (PI / 4)) with (PI / 2 - - (PI / 4)) by field. now rewrite sin_shift, cos_neg, cos_PI4. Qed. +#[deprecated(since="8.10",note="Use sin_3PI4 instead.")] Notation sin3PI4 := sin_3PI4. + Lemma cos_PI6 : cos (PI / 6) = sqrt 3 / 2. Proof with trivial. apply Rsqr_inj... diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index e49b1c0c07..2673995a86 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -383,7 +383,7 @@ let rec vernac_loop ~state = try let input = top_buffer.tokens in match read_sentence ~state input with - | Some (VernacBacktrack(bid,_,_)) -> + | Some (VernacBackTo bid) -> let bid = Stateid.of_int bid in let doc, res = Stm.edit_at ~doc:state.doc bid in assert (res = `NewTip); diff --git a/toplevel/g_toplevel.mlg b/toplevel/g_toplevel.mlg index fed337ab03..1a1537113e 100644 --- a/toplevel/g_toplevel.mlg +++ b/toplevel/g_toplevel.mlg @@ -17,7 +17,7 @@ open Vernacexpr (* Vernaculars specific to the toplevel *) type vernac_toplevel = - | VernacBacktrack of int * int * int + | VernacBackTo of int | VernacDrop | VernacQuit | VernacControl of vernac_control @@ -54,8 +54,8 @@ GRAMMAR EXTEND Gram vernac_toplevel: FIRST [ [ IDENT "Drop"; "." -> { Some VernacDrop } | IDENT "Quit"; "." -> { Some VernacQuit } - | IDENT "Backtrack"; n = natural ; m = natural ; p = natural; "." -> - { Some (VernacBacktrack (n,m,p)) } + | IDENT "BackTo"; n = natural; "." -> + { Some (VernacBackTo n) } (* show a goal for the specified proof state *) | test_show_goal; IDENT "Show"; IDENT "Goal"; gid = natural; IDENT "at"; sid = natural; "." -> { Some (VernacShowGoal {gid; sid}) } diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 3f13d772ab..74c9bc2886 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -107,26 +107,20 @@ let check_mutuality env evd isfix fixl = warn_non_full_mutual (x,xge,y,yge,isfix,rest) | _ -> () -type structured_fixpoint_expr = { - fix_name : Id.t; - fix_univs : universe_decl_expr option; - fix_annot : lident option; - fix_binders : local_binder_expr list; - fix_body : constr_expr option; - fix_type : constr_expr -} - let interp_fix_context ~program_mode ~cofix env sigma fix = - let before, after = if not cofix then split_at_annot fix.fix_binders fix.fix_annot else [], fix.fix_binders in + let before, after = + if not cofix + then split_at_annot fix.Vernacexpr.binders fix.Vernacexpr.rec_order + else [], fix.Vernacexpr.binders in let sigma, (impl_env, ((env', ctx), imps)) = interp_context_evars ~program_mode env sigma before in let sigma, (impl_env', ((env'', ctx'), imps')) = interp_context_evars ~program_mode ~impl_env ~shift:(Context.Rel.nhyps ctx) env' sigma after in - let annot = Option.map (fun _ -> List.length (assums_of_rel_context ctx)) fix.fix_annot in + let annot = Option.map (fun _ -> List.length (assums_of_rel_context ctx)) fix.Vernacexpr.rec_order in sigma, ((env'', ctx' @ ctx), (impl_env',imps @ imps'), annot) let interp_fix_ccl ~program_mode sigma impls (env,_) fix = - let sigma, (c, impl) = interp_type_evars_impls ~program_mode ~impls env sigma fix.fix_type in + let sigma, (c, impl) = interp_type_evars_impls ~program_mode ~impls env sigma fix.Vernacexpr.rtype in let r = Retyping.relevance_of_type env sigma c in sigma, (c, r, impl) @@ -135,7 +129,7 @@ let interp_fix_body ~program_mode env_rec sigma impls (_,ctx) fix ccl = Option.cata (fun body -> let env = push_rel_context ctx env_rec in let sigma, body = interp_casted_constr_evars ~program_mode env sigma ~impls body ccl in - sigma, Some (it_mkLambda_or_LetIn body ctx)) (sigma, None) fix.fix_body + sigma, Some (it_mkLambda_or_LetIn body ctx)) (sigma, None) fix.Vernacexpr.body_def let build_fix_type (_,ctx) ccl = EConstr.it_mkProd_or_LetIn ccl ctx @@ -167,16 +161,16 @@ type recursive_preentry = let fix_proto sigma = Evarutil.new_global sigma (Coqlib.lib_ref "program.tactic.fix_proto") -let interp_recursive ~program_mode ~cofix fixl notations = +let interp_recursive ~program_mode ~cofix (fixl : 'a Vernacexpr.fix_expr_gen list) = let open Context.Named.Declaration in let open EConstr in let env = Global.env() in - let fixnames = List.map (fun fix -> fix.fix_name) fixl in + let fixnames = List.map (fun fix -> fix.Vernacexpr.fname.CAst.v) fixl in (* Interp arities allowing for unresolved types *) let all_universes = List.fold_right (fun sfe acc -> - match sfe.fix_univs , acc with + match sfe.Vernacexpr.univs , acc with | None , acc -> acc | x , None -> x | Some ls , Some us -> @@ -222,6 +216,7 @@ let interp_recursive ~program_mode ~cofix fixl notations = (* Interp bodies with rollback because temp use of notations/implicit *) let sigma, fixdefs = Metasyntax.with_syntax_protection (fun () -> + let notations = List.map_append (fun { Vernacexpr.notations } -> notations) fixl in List.iter (Metasyntax.set_notation_for_interpretation env_rec impls) notations; List.fold_left4_map (fun sigma fixctximpenv -> interp_fix_body ~program_mode env_rec sigma (Id.Map.fold Id.Map.add fixctximpenv impls)) @@ -248,8 +243,8 @@ let ground_fixpoint env evd (fixnames,fixrs,fixdefs,fixtypes) = let fixtypes = List.map EConstr.(to_constr evd) fixtypes in Evd.evar_universe_context evd, (fixnames,fixrs,fixdefs,fixtypes) -let interp_fixpoint ~cofix l ntns = - let (env,_,pl,evd),fix,info = interp_recursive ~program_mode:false ~cofix l ntns in +let interp_fixpoint ~cofix l = + let (env,_,pl,evd),fix,info = interp_recursive ~program_mode:false ~cofix l in check_recursive true env evd fix; let uctx,fix = ground_fixpoint env evd fix in (fix,pl,uctx,info) @@ -316,38 +311,29 @@ let extract_decreasing_argument ~structonly = function { CAst.v = v } -> match v | _ -> user_err Pp.(str "Well-founded induction requires Program Fixpoint or Function.") -let extract_fixpoint_components ~structonly l = - let fixl, ntnl = List.split l in - let fixl = List.map (fun (({CAst.v=id},pl),ann,bl,typ,def) -> - (* This is a special case: if there's only one binder, we pick it as the - recursive argument if none is provided. *) - let ann = Option.map (fun ann -> match bl, ann with - | [CLocalAssum([{ CAst.v = Name x }],_,_)], { CAst.v = CMeasureRec(None, mes, rel); CAst.loc } -> - CAst.make ?loc @@ CMeasureRec(Some (CAst.make x), mes, rel) - | [CLocalDef({ CAst.v = Name x },_,_)], { CAst.v = CMeasureRec(None, mes, rel); CAst.loc } -> - CAst.make ?loc @@ CMeasureRec(Some (CAst.make x), mes, rel) - | _, x -> x) ann - in - let ann = Option.map (extract_decreasing_argument ~structonly) ann in - {fix_name = id; fix_annot = ann; fix_univs = pl; - fix_binders = bl; fix_body = def; fix_type = typ}) fixl in - fixl, List.flatten ntnl - -let extract_cofixpoint_components l = - let fixl, ntnl = List.split l in - List.map (fun (({CAst.v=id},pl),bl,typ,def) -> - {fix_name = id; fix_annot = None; fix_univs = pl; - fix_binders = bl; fix_body = def; fix_type = typ}) fixl, - List.flatten ntnl +(* This is a special case: if there's only one binder, we pick it as + the recursive argument if none is provided. *) +let adjust_rec_order ~structonly binders rec_order = + let rec_order = Option.map (fun rec_order -> match binders, rec_order with + | [CLocalAssum([{ CAst.v = Name x }],_,_)], { CAst.v = CMeasureRec(None, mes, rel); CAst.loc } -> + CAst.make ?loc @@ CMeasureRec(Some (CAst.make x), mes, rel) + | [CLocalDef({ CAst.v = Name x },_,_)], { CAst.v = CMeasureRec(None, mes, rel); CAst.loc } -> + CAst.make ?loc @@ CMeasureRec(Some (CAst.make x), mes, rel) + | _, x -> x) rec_order + in + Option.map (extract_decreasing_argument ~structonly) rec_order let check_safe () = let open Declarations in let flags = Environ.typing_flags (Global.env ()) in flags.check_universes && flags.check_guarded -let do_fixpoint_common l = - let fixl, ntns = extract_fixpoint_components ~structonly:true l in - let (_, _, _, info as fix) = interp_fixpoint ~cofix:false fixl ntns in +let do_fixpoint_common (fixl : Vernacexpr.fixpoint_expr list) = + let fixl = List.map (fun fix -> + Vernacexpr.{ fix + with rec_order = adjust_rec_order ~structonly:true fix.binders fix.rec_order }) fixl in + let ntns = List.map_append (fun { Vernacexpr.notations } -> notations ) fixl in + let (_, _, _, info as fix) = interp_fixpoint ~cofix:false fixl in fixl, ntns, fix, List.map compute_possible_guardness_evidences info let do_fixpoint_interactive ~scope ~poly l : Lemmas.t = @@ -361,17 +347,18 @@ let do_fixpoint ~scope ~poly l = declare_fixpoint_generic ~indexes:possible_indexes ~scope ~poly fix ntns; if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () -let do_cofixpoint_common l = - let fixl,ntns = extract_cofixpoint_components l in - ntns, interp_fixpoint ~cofix:true fixl ntns +let do_cofixpoint_common (fixl : Vernacexpr.cofixpoint_expr list) = + let fixl = List.map (fun fix -> {fix with Vernacexpr.rec_order = None}) fixl in + let ntns = List.map_append (fun { Vernacexpr.notations } -> notations ) fixl in + interp_fixpoint ~cofix:true fixl, ntns let do_cofixpoint_interactive ~scope ~poly l = - let ntns, cofix = do_cofixpoint_common l in + let cofix, ntns = do_cofixpoint_common l in let lemma = declare_fixpoint_interactive_generic ~scope ~poly cofix ntns in if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else (); lemma let do_cofixpoint ~scope ~poly l = - let ntns, cofix = do_cofixpoint_common l in + let cofix, ntns = do_cofixpoint_common l in declare_fixpoint_generic ~scope ~poly cofix ntns; if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index 982d316605..4f8e9018de 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -10,7 +10,6 @@ open Names open Constr -open Constrexpr open Vernacexpr (** {6 Fixpoints and cofixpoints} *) @@ -18,39 +17,35 @@ open Vernacexpr (** Entry points for the vernacular commands Fixpoint and CoFixpoint *) val do_fixpoint_interactive : - scope:DeclareDef.locality -> poly:bool -> (fixpoint_expr * decl_notation list) list -> Lemmas.t + scope:DeclareDef.locality -> poly:bool -> fixpoint_expr list -> Lemmas.t val do_fixpoint : - scope:DeclareDef.locality -> poly:bool -> (fixpoint_expr * decl_notation list) list -> unit + scope:DeclareDef.locality -> poly:bool -> fixpoint_expr list -> unit val do_cofixpoint_interactive : - scope:DeclareDef.locality -> poly:bool -> (cofixpoint_expr * decl_notation list) list -> Lemmas.t + scope:DeclareDef.locality -> poly:bool -> cofixpoint_expr list -> Lemmas.t val do_cofixpoint : - scope:DeclareDef.locality -> poly:bool -> (cofixpoint_expr * decl_notation list) list -> unit + scope:DeclareDef.locality -> poly:bool -> cofixpoint_expr list -> unit (************************************************************************) (** Internal API *) (************************************************************************) -type structured_fixpoint_expr = { - fix_name : Id.t; - fix_univs : Constrexpr.universe_decl_expr option; - fix_annot : lident option; - fix_binders : local_binder_expr list; - fix_body : constr_expr option; - fix_type : constr_expr -} - (** Typing global fixpoints and cofixpoint_expr *) +val adjust_rec_order + : structonly:bool + -> Constrexpr.local_binder_expr list + -> Constrexpr.recursion_order_expr option + -> lident option + (** Exported for Program *) val interp_recursive : (* Misc arguments *) program_mode:bool -> cofix:bool -> (* Notations of the fixpoint / should that be folded in the previous argument? *) - structured_fixpoint_expr list -> decl_notation list -> - + lident option fix_expr_gen list -> (* env / signature / univs / evar_map *) (Environ.env * EConstr.named_context * UState.universe_decl * Evd.evar_map) * (* names / defs / types *) @@ -60,25 +55,13 @@ val interp_recursive : (** Exported for Funind *) -(** Extracting the semantical components out of the raw syntax of - (co)fixpoints declarations *) - -val extract_fixpoint_components : structonly:bool -> - (fixpoint_expr * decl_notation list) list -> - structured_fixpoint_expr list * decl_notation list +type recursive_preentry = Id.t list * Sorts.relevance list * constr option list * types list -val extract_cofixpoint_components : - (cofixpoint_expr * decl_notation list) list -> - structured_fixpoint_expr list * decl_notation list - -type recursive_preentry = - Id.t list * Sorts.relevance list * constr option list * types list - -val interp_fixpoint : - cofix:bool -> - structured_fixpoint_expr list -> decl_notation list -> - recursive_preentry * UState.universe_decl * UState.t * - (EConstr.rel_context * Impargs.manual_implicits * int option) list +val interp_fixpoint + : cofix:bool + -> lident option fix_expr_gen list + -> recursive_preentry * UState.universe_decl * UState.t * + (EConstr.rel_context * Impargs.manual_implicits * int option) list (** Very private function, do not use *) val compute_possible_guardness_evidences : diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 65db4401d9..664010c917 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -80,9 +80,6 @@ type structured_one_inductive_expr = { ind_lc : (Id.t * constr_expr) list } -type structured_inductive_expr = - local_binder_expr list * structured_one_inductive_expr list - let minductive_message = function | [] -> user_err Pp.(str "No inductive definition.") | [x] -> (Id.print x ++ str " is defined") @@ -468,9 +465,6 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not InferCumulativity.infer_inductive env_ar mind_ent else mind_ent), Evd.universe_binders sigma, impls -let interp_mutual_inductive ~template udecl (paramsl,indl) notations ~cumulative ~poly ~private_ind finite = - interp_mutual_inductive_gen (Global.env()) ~template udecl ([],paramsl,indl) notations ~cumulative ~poly ~private_ind finite - (* Very syntactical equality *) let eq_local_binders bl1 bl2 = List.equal local_binder_eq bl1 bl2 diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index 97f930c0a1..285be8cd51 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -10,7 +10,6 @@ open Names open Entries -open Libnames open Vernacexpr open Constrexpr @@ -33,12 +32,20 @@ val do_mutual_inductive -> Declarations.recursivity_kind -> unit +(** User-interface API *) + +(** Prepare a "match" template for a given inductive type. + For each branch of the match, we list the constructor name + followed by enough pattern variables. + [Not_found] is raised if the given string isn't the qualid of + a known inductive type. *) + +val make_cases : Names.inductive -> string list list + (************************************************************************) -(** Internal API *) +(** Internal API, exported for Record *) (************************************************************************) -(** Exported for Record and Funind *) - (** Registering a mutual inductive definition together with its associated schemes *) @@ -55,41 +62,3 @@ val should_auto_template : Id.t -> bool -> bool (** [should_auto_template x b] is [true] when [b] is [true] and we automatically use template polymorphism. [x] is the name of the inductive under consideration. *) - -(** Exported for Funind *) - -(** Extracting the semantical components out of the raw syntax of mutual - inductive declarations *) - -type structured_one_inductive_expr = { - ind_name : Id.t; - ind_arity : constr_expr; - ind_lc : (Id.t * constr_expr) list -} - -type structured_inductive_expr = - local_binder_expr list * structured_one_inductive_expr list - -val extract_mutual_inductive_declaration_components : - (one_inductive_expr * decl_notation list) list -> - structured_inductive_expr * (*coercions:*) qualid list * decl_notation list - -(** Typing mutual inductive definitions *) -val interp_mutual_inductive - : template:bool option - -> universe_decl_expr option - -> structured_inductive_expr - -> decl_notation list - -> cumulative:bool - -> poly:bool - -> private_ind:bool - -> Declarations.recursivity_kind - -> mutual_inductive_entry * UnivNames.universe_binders * one_inductive_impls list - -(** Prepare a "match" template for a given inductive type. - For each branch of the match, we list the constructor name - followed by enough pattern variables. - [Not_found] is raised if the given string isn't the qualid of - a known inductive type. *) - -val make_cases : Names.inductive -> string list list diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 0fd65ad9b4..c6e68effd7 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -244,10 +244,10 @@ let collect_evars_of_term evd c ty = Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev)) evars (Evd.from_ctx (Evd.evar_universe_context evd)) -let do_program_recursive ~scope ~poly fixkind fixl ntns = +let do_program_recursive ~scope ~poly fixkind fixl = let cofix = fixkind = DeclareObl.IsCoFixpoint in let (env, rec_sign, pl, evd), fix, info = - interp_recursive ~cofix ~program_mode:true fixl ntns + interp_recursive ~cofix ~program_mode:true fixl in (* Program-specific code *) (* Get the interesting evars, those that were not instantiated *) @@ -289,16 +289,19 @@ let do_program_recursive ~scope ~poly fixkind fixl ntns = | DeclareObl.IsFixpoint _ -> Decls.Fixpoint | DeclareObl.IsCoFixpoint -> Decls.CoFixpoint in + let ntns = List.map_append (fun { Vernacexpr.notations } -> notations ) fixl in Obligations.add_mutual_definitions defs ~poly ~scope ~kind ~univdecl:pl ctx ntns fixkind let do_program_fixpoint ~scope ~poly l = - let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in + let g = List.map (fun { Vernacexpr.rec_order } -> rec_order) l in match g, l with - | [Some { CAst.v = CWfRec (n,r) }], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] -> + | [Some { CAst.v = CWfRec (n,r) }], + [ Vernacexpr.{fname={CAst.v=id}; univs; binders; rtype; body_def; notations} ] -> let recarg = mkIdentC n.CAst.v in - build_wellfounded (id, pl, bl, typ, out_def def) poly r recarg ntn + build_wellfounded (id, univs, binders, rtype, out_def body_def) poly r recarg notations - | [Some { CAst.v = CMeasureRec (n, m, r) }], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] -> + | [Some { CAst.v = CMeasureRec (n, m, r) }], + [Vernacexpr.{fname={CAst.v=id}; univs; binders; rtype; body_def; notations }] -> (* We resolve here a clash between the syntax of Program Fixpoint and the one of funind *) let r = match n, r with | Some id, None -> @@ -308,25 +311,20 @@ let do_program_fixpoint ~scope ~poly l = user_err Pp.(str"Measure takes only two arguments in Program Fixpoint.") | _, _ -> r in - build_wellfounded (id, pl, bl, typ, out_def def) poly - (Option.default (CAst.make @@ CRef (lt_ref,None)) r) m ntn + build_wellfounded (id, univs, binders, rtype, out_def body_def) poly + (Option.default (CAst.make @@ CRef (lt_ref,None)) r) m notations | _, _ when List.for_all (fun ro -> match ro with None | Some { CAst.v = CStructRec _} -> true | _ -> false) g -> - let fixl,ntns = extract_fixpoint_components ~structonly:true l in - let fixkind = DeclareObl.IsFixpoint (List.map (fun d -> d.fix_annot) fixl) in - do_program_recursive ~scope ~poly fixkind fixl ntns + let annots = List.map (fun fix -> + Vernacexpr.(ComFixpoint.adjust_rec_order ~structonly:true fix.binders fix.rec_order)) l in + let fixkind = DeclareObl.IsFixpoint annots in + let l = List.map2 (fun fix rec_order -> { fix with Vernacexpr.rec_order }) l annots in + do_program_recursive ~scope ~poly fixkind l | _, _ -> user_err ~hdr:"do_program_fixpoint" (str "Well-founded fixpoints not allowed in mutually recursive blocks") -let extract_cofixpoint_components l = - let fixl, ntnl = List.split l in - List.map (fun (({CAst.v=id},pl),bl,typ,def) -> - {fix_name = id; fix_annot = None; fix_univs = pl; - fix_binders = bl; fix_body = def; fix_type = typ}) fixl, - List.flatten ntnl - let check_safe () = let open Declarations in let flags = Environ.typing_flags (Global.env ()) in @@ -336,7 +334,7 @@ let do_fixpoint ~scope ~poly l = do_program_fixpoint ~scope ~poly l; if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () -let do_cofixpoint ~scope ~poly l = - let fixl,ntns = extract_cofixpoint_components l in - do_program_recursive ~scope ~poly DeclareObl.IsCoFixpoint fixl ntns; +let do_cofixpoint ~scope ~poly fixl = + let fixl = List.map (fun fix -> { fix with Vernacexpr.rec_order = None }) fixl in + do_program_recursive ~scope ~poly DeclareObl.IsCoFixpoint fixl; if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () diff --git a/vernac/comProgramFixpoint.mli b/vernac/comProgramFixpoint.mli index f25abb95c3..a851e4dff5 100644 --- a/vernac/comProgramFixpoint.mli +++ b/vernac/comProgramFixpoint.mli @@ -1,11 +1,21 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + open Vernacexpr (** Special Fixpoint handling when command is activated. *) val do_fixpoint : (* When [false], assume guarded. *) - scope:DeclareDef.locality -> poly:bool -> (fixpoint_expr * decl_notation list) list -> unit + scope:DeclareDef.locality -> poly:bool -> fixpoint_expr list -> unit val do_cofixpoint : (* When [false], assume guarded. *) - scope:DeclareDef.locality -> poly:bool -> (cofixpoint_expr * decl_notation list) list -> unit + scope:DeclareDef.locality -> poly:bool -> cofixpoint_expr list -> unit diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index 0c45ff11d7..c5cbb095ca 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -29,9 +29,6 @@ type obligation = type obligations = obligation array * int -type notations = - (lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list - type fixpoint_kind = | IsFixpoint of lident option list | IsCoFixpoint @@ -46,7 +43,7 @@ type program_info = ; prg_deps : Id.t list ; prg_fixkind : fixpoint_kind option ; prg_implicits : Impargs.manual_implicits - ; prg_notations : notations + ; prg_notations : Vernacexpr.decl_notation list ; prg_poly : bool ; prg_scope : DeclareDef.locality ; prg_kind : Decls.definition_object_kind diff --git a/vernac/declareObl.mli b/vernac/declareObl.mli index a8dd5040cb..2a8fa734b3 100644 --- a/vernac/declareObl.mli +++ b/vernac/declareObl.mli @@ -24,9 +24,6 @@ type obligation = type obligations = obligation array * int -type notations = - (lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list - type fixpoint_kind = | IsFixpoint of lident option list | IsCoFixpoint @@ -41,7 +38,7 @@ type program_info = ; prg_deps : Id.t list ; prg_fixkind : fixpoint_kind option ; prg_implicits : Impargs.manual_implicits - ; prg_notations : notations + ; prg_notations : Vernacexpr.decl_notation list ; prg_poly : bool ; prg_scope : DeclareDef.locality ; prg_kind : Decls.definition_object_kind diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 2b475f1ef9..ad5d98669d 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -402,16 +402,19 @@ GRAMMAR EXTEND Gram ; (* (co)-fixpoints *) rec_definition: - [ [ id = ident_decl; + [ [ id_decl = ident_decl; bl = binders_fixannot; - ty = type_cstr; - def = OPT [":="; def = lconstr -> { def } ]; ntn = decl_notation -> - { let bl, annot = bl in ((id,annot,bl,ty,def),ntn) } ] ] + rtype = type_cstr; + body_def = OPT [":="; def = lconstr -> { def } ]; notations = decl_notation -> + { let binders, rec_order = bl in + {fname = fst id_decl; univs = snd id_decl; rec_order; binders; rtype; body_def; notations} + } ] ] ; corec_definition: - [ [ id = ident_decl; bl = binders; ty = type_cstr; - def = OPT [":="; def = lconstr -> { def }]; ntn = decl_notation -> - { ((id,bl,ty,def),ntn) } ] ] + [ [ id_decl = ident_decl; binders = binders; rtype = type_cstr; + body_def = OPT [":="; def = lconstr -> { def }]; notations = decl_notation -> + { {fname = fst id_decl; univs = snd id_decl; rec_order = (); binders; rtype; body_def; notations} + } ]] ; type_cstr: [ [ ":"; c=lconstr -> { c } @@ -1138,7 +1141,6 @@ GRAMMAR EXTEND Gram | IDENT "Reset"; id = identref -> { VernacResetName id } | IDENT "Back" -> { VernacBack 1 } | IDENT "Back"; n = natural -> { VernacBack n } - | IDENT "BackTo"; n = natural -> { VernacBackTo n } (* Tactic Debugger *) | IDENT "Debug"; IDENT "On" -> diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index ecea9ae4c9..6a754a0cde 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -113,46 +113,6 @@ let by tac pf = (* Creating a lemma-like constant *) (************************************************************************) -(* Support for mutually proved theorems *) - -let retrieve_first_recthm uctx = function - | GlobRef.VarRef id -> - NamedDecl.get_value (Global.lookup_named id), - Decls.variable_opacity id - | GlobRef.ConstRef cst -> - let cb = Global.lookup_constant cst in - (* we get the right order somehow but surely it could be enforced in a better way *) - let uctx = UState.context uctx in - let inst = Univ.UContext.instance uctx in - let map (c, _, _) = Vars.subst_instance_constr inst c in - (Option.map map (Global.body_of_constant_body Library.indirect_accessor cb), is_opaque cb) - | _ -> assert false - -let adjust_guardness_conditions const = function - | [] -> const (* Not a recursive statement *) - | possible_indexes -> - (* Try all combinations... not optimal *) - let env = Global.env() in - let open Proof_global in - { const with proof_entry_body = - Future.chain const.proof_entry_body - (fun ((body, ctx), eff) -> - match Constr.kind body with - | Fix ((nv,0),(_,_,fixdefs as fixdecls)) -> -(* let possible_indexes = - List.map2 (fun i c -> match i with Some i -> i | None -> - List.interval 0 (List.length ((lam_assum c)))) - lemma_guard (Array.to_list fixdefs) in -*) - let env = Safe_typing.push_private_constants env eff.Evd.seff_private in - let indexes = - search_guard env - possible_indexes fixdecls in - (mkFix ((indexes,0),fixdecls), ctx), eff - | _ -> (body, ctx), eff) } - -let default_thm_id = Id.of_string "Unnamed_thm" - let check_name_freshness locality {CAst.loc;v=id} : unit = (* We check existence here: it's a bit late at Qed time *) if Nametab.exists_cci (Lib.make_path id) || is_section_variable id || @@ -160,52 +120,6 @@ let check_name_freshness locality {CAst.loc;v=id} : unit = then user_err ?loc (Id.print id ++ str " already exists.") -let save_remaining_recthms env sigma ~poly ~scope norm univs body opaq i { Recthm.name; typ; impargs } = - let t_i = norm typ in - let kind = Decls.(IsAssumption Conjectural) in - match body with - | None -> - let open DeclareDef in - (match scope with - | Discharge -> - let impl = false in (* copy values from Vernacentries *) - let univs = match univs with - | Polymorphic_entry (_, univs) -> - (* What is going on here? *) - Univ.ContextSet.of_context univs - | Monomorphic_entry univs -> univs - in - let c = Declare.SectionLocalAssum {typ=t_i; univs; poly; impl} in - let () = Declare.declare_variable ~name ~kind c in - (GlobRef.VarRef name,impargs) - | Global local -> - let kind = Decls.(IsAssumption Conjectural) in - let decl = Declare.ParameterEntry (None,(t_i,univs),None) in - let kn = Declare.declare_constant ~name ~local ~kind decl in - (GlobRef.ConstRef kn,impargs)) - | Some body -> - let body = norm body in - let rec body_i t = match Constr.kind t with - | Fix ((nv,0),decls) -> mkFix ((nv,i),decls) - | CoFix (0,decls) -> mkCoFix (i,decls) - | LetIn(na,t1,ty,t2) -> mkLetIn (na,t1,ty, body_i t2) - | Lambda(na,ty,t) -> mkLambda(na,ty,body_i t) - | App (t, args) -> mkApp (body_i t, args) - | _ -> - anomaly Pp.(str "Not a proof by induction: " ++ Printer.pr_constr_env env sigma body ++ str ".") in - let body_i = body_i body in - let open DeclareDef in - match scope with - | Discharge -> - let const = Declare.definition_entry ~types:t_i ~opaque:opaq ~univs body_i in - let c = Declare.SectionLocalDef const in - let () = Declare.declare_variable ~name ~kind c in - (GlobRef.VarRef name,impargs) - | Global local -> - let const = Declare.definition_entry ~types:t_i ~univs ~opaque:opaq body_i in - let kn = Declare.declare_constant ~name ~local ~kind (Declare.DefinitionEntry const) in - (GlobRef.ConstRef kn,impargs) - let initialize_named_context_for_proof () = let sign = Global.named_context () in List.fold_right @@ -315,9 +229,73 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?inference_hook ?hook thms start_lemma_with_initialization ?hook ~poly ~scope ~kind evd ~udecl recguard thms snl (************************************************************************) -(* Commom constant saving path *) +(* Commom constant saving path, for both Qed and Admitted *) (************************************************************************) +(* Helper for process_recthms *) +let retrieve_first_recthm uctx = function + | GlobRef.VarRef id -> + NamedDecl.get_value (Global.lookup_named id), + Decls.variable_opacity id + | GlobRef.ConstRef cst -> + let cb = Global.lookup_constant cst in + (* we get the right order somehow but surely it could be enforced in a better way *) + let uctx = UState.context uctx in + let inst = Univ.UContext.instance uctx in + let map (c, _, _) = Vars.subst_instance_constr inst c in + (Option.map map (Global.body_of_constant_body Library.indirect_accessor cb), is_opaque cb) + | _ -> assert false + +(* Helper for process_recthms *) +let save_remaining_recthms env sigma ~poly ~scope ~udecl uctx body opaq i { Recthm.name; typ; impargs } = + let norm c = EConstr.to_constr (Evd.from_ctx uctx) c in + let body = Option.map EConstr.of_constr body in + let univs = UState.check_univ_decl ~poly uctx udecl in + let t_i = norm typ in + let kind = Decls.(IsAssumption Conjectural) in + match body with + | None -> + let open DeclareDef in + (match scope with + | Discharge -> + let impl = false in (* copy values from Vernacentries *) + let univs = match univs with + | Polymorphic_entry (_, univs) -> + (* What is going on here? *) + Univ.ContextSet.of_context univs + | Monomorphic_entry univs -> univs + in + let c = Declare.SectionLocalAssum {typ=t_i; univs; poly; impl} in + let () = Declare.declare_variable ~name ~kind c in + GlobRef.VarRef name, impargs + | Global local -> + let kind = Decls.(IsAssumption Conjectural) in + let decl = Declare.ParameterEntry (None,(t_i,univs),None) in + let kn = Declare.declare_constant ~name ~local ~kind decl in + GlobRef.ConstRef kn, impargs) + | Some body -> + let body = norm body in + let rec body_i t = match Constr.kind t with + | Fix ((nv,0),decls) -> mkFix ((nv,i),decls) + | CoFix (0,decls) -> mkCoFix (i,decls) + | LetIn(na,t1,ty,t2) -> mkLetIn (na,t1,ty, body_i t2) + | Lambda(na,ty,t) -> mkLambda(na,ty,body_i t) + | App (t, args) -> mkApp (body_i t, args) + | _ -> + anomaly Pp.(str "Not a proof by induction: " ++ Printer.pr_constr_env env sigma body ++ str ".") in + let body_i = body_i body in + let open DeclareDef in + match scope with + | Discharge -> + let const = Declare.definition_entry ~types:t_i ~opaque:opaq ~univs body_i in + let c = Declare.SectionLocalDef const in + let () = Declare.declare_variable ~name ~kind c in + GlobRef.VarRef name, impargs + | Global local -> + let const = Declare.definition_entry ~types:t_i ~univs ~opaque:opaq body_i in + let kn = Declare.declare_constant ~name ~local ~kind (Declare.DefinitionEntry const) in + GlobRef.ConstRef kn, impargs + (* This declares implicits and calls the hooks for all the theorems, including the main one *) let process_recthms ?fix_exn ?hook env sigma uctx ~udecl ~poly ~scope dref imps other_thms = @@ -325,10 +303,7 @@ let process_recthms ?fix_exn ?hook env sigma uctx ~udecl ~poly ~scope dref imps if List.is_empty other_thms then [] else (* there are several theorems defined mutually *) let body,opaq = retrieve_first_recthm uctx dref in - let norm c = EConstr.to_constr (Evd.from_ctx uctx) c in - let body = Option.map EConstr.of_constr body in - let uctx = UState.check_univ_decl ~poly uctx udecl in - List.map_i (save_remaining_recthms env sigma ~poly ~scope norm uctx body opaq) 1 other_thms in + List.map_i (save_remaining_recthms env sigma ~poly ~scope ~udecl uctx body opaq) 1 other_thms in let thms_data = (dref,imps)::other_thms_data in List.iter (fun (dref,imps) -> maybe_declare_manual_implicits false dref imps; @@ -395,10 +370,33 @@ let save_lemma_admitted ~(lemma : t) : unit = (* Saving a lemma-like constant *) (************************************************************************) +let default_thm_id = Id.of_string "Unnamed_thm" + let check_anonymity id save_ident = if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then user_err Pp.(str "This command can only be used for unnamed theorem.") +(* Support for mutually proved theorems *) + +(* Helper for finish_proved *) +let adjust_guardness_conditions const = function + | [] -> const (* Not a recursive statement *) + | possible_indexes -> + (* Try all combinations... not optimal *) + let env = Global.env() in + let open Proof_global in + { const with + proof_entry_body = + Future.chain const.proof_entry_body + (fun ((body, ctx), eff) -> + match Constr.kind body with + | Fix ((nv,0),(_,_,fixdefs as fixdecls)) -> + let env = Safe_typing.push_private_constants env eff.Evd.seff_private in + let indexes = search_guard env possible_indexes fixdecls in + (mkFix ((indexes,0),fixdecls), ctx), eff + | _ -> (body, ctx), eff) + } + let finish_proved env sigma idopt po info = let open Proof_global in let { Info.hook; compute_guard; impargs; other_thms; scope; kind } = info in diff --git a/vernac/obligations.mli b/vernac/obligations.mli index f97bc784c3..2a0d0aba97 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -18,27 +18,33 @@ val check_evars : env -> evar_map -> unit val evar_dependencies : evar_map -> Evar.t -> Evar.Set.t val sort_dependencies : (Evar.t * evar_info * Evar.Set.t) list -> (Evar.t * evar_info * Evar.Set.t) list -(* env, id, evars, number of function prototypes to try to clear from - evars contexts, object and type *) -val eterm_obligations : env -> Id.t -> evar_map -> int -> - ?status:Evar_kinds.obligation_definition_status -> EConstr.constr -> EConstr.types -> - (Id.t * types * Evar_kinds.t Loc.located * - (bool * Evar_kinds.obligation_definition_status) * Int.Set.t * - unit Proofview.tactic option) array - (* Existential key, obl. name, type as product, - location of the original evar, associated tactic, - status and dependencies as indexes into the array *) - * ((Evar.t * Id.t) list * ((Id.t -> EConstr.constr) -> EConstr.constr -> constr)) * - constr * types - (* Translations from existential identifiers to obligation identifiers - and for terms with existentials to closed terms, given a - translation from obligation identifiers to constrs, new term, new type *) - +(* ident, type, location, (opaque or transparent, expand or define), dependencies, tactic to solve it *) type obligation_info = (Id.t * types * Evar_kinds.t Loc.located * - (bool * Evar_kinds.obligation_definition_status) * Int.Set.t * unit Proofview.tactic option) array - (* ident, type, location, (opaque or transparent, expand or define), - dependencies, tactic to solve it *) + (bool * Evar_kinds.obligation_definition_status) * Int.Set.t * unit Proofview.tactic option) array + +(* env, id, evars, number of function prototypes to try to clear from + evars contexts, object and type *) +val eterm_obligations + : env + -> Id.t + -> evar_map + -> int + -> ?status:Evar_kinds.obligation_definition_status + -> EConstr.constr + -> EConstr.types + -> obligation_info * + + (* Existential key, obl. name, type as product, location of the + original evar, associated tactic, status and dependencies as + indexes into the array *) + ((Evar.t * Id.t) list * ((Id.t -> EConstr.constr) -> EConstr.constr -> constr)) * + + (* Translations from existential identifiers to obligation + identifiers and for terms with existentials to closed terms, + given a translation from obligation identifiers to constrs, + new term, new type *) + constr * types val default_tactic : unit Proofview.tactic ref @@ -69,7 +75,7 @@ val add_mutual_definitions -> ?kind:Decls.definition_object_kind -> ?reduce:(constr -> constr) -> ?hook:DeclareDef.Hook.t -> ?opaque:bool - -> DeclareObl.notations + -> Vernacexpr.decl_notation list -> DeclareObl.fixpoint_kind -> unit val obligation diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index e676fe94db..0eb0b1b6f6 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -419,15 +419,15 @@ let string_of_theorem_kind = let open Decls in function | l -> spc() ++ hov 1 (str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")") - let pr_rec_definition ((iddecl,ro,bl,type_,def),ntn) = + let pr_rec_definition { fname; univs; rec_order; binders; rtype; body_def; notations } = let env = Global.env () in let sigma = Evd.from_env env in let pr_pure_lconstr c = Flags.without_option Flags.beautify pr_lconstr c in - let annot = pr_guard_annot (pr_lconstr_expr env sigma) bl ro in - pr_ident_decl iddecl ++ pr_binders_arg bl ++ annot - ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr env sigma c) type_ - ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_pure_lconstr env sigma def) def - ++ prlist (pr_decl_notation @@ pr_constr env sigma) ntn + let annot = pr_guard_annot (pr_lconstr_expr env sigma) binders rec_order in + pr_ident_decl (fname,univs) ++ pr_binders_arg binders ++ annot + ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr env sigma c) rtype + ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_pure_lconstr env sigma def) body_def + ++ prlist (pr_decl_notation @@ pr_constr env sigma) notations let pr_statement head (idpl,(bl,c)) = let env = Global.env () in @@ -669,8 +669,6 @@ let string_of_definition_object_kind = let open Decls in function return ( if Int.equal i 1 then keyword "Back" else keyword "Back" ++ pr_intarg i ) - | VernacBackTo i -> - return (keyword "BackTo" ++ pr_intarg i) (* State management *) | VernacWriteState s -> @@ -858,11 +856,11 @@ let string_of_definition_object_kind = let open Decls in function | DoDischarge -> keyword "Let" ++ spc () | NoDischarge -> str "" in - let pr_onecorec ((iddecl,bl,c,def),ntn) = - pr_ident_decl iddecl ++ spc() ++ pr_binders env sigma bl ++ spc() ++ str":" ++ - spc() ++ pr_lconstr_expr env sigma c ++ - pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr env sigma def) def ++ - prlist (pr_decl_notation @@ pr_constr env sigma) ntn + let pr_onecorec {fname; univs; binders; rtype; body_def; notations } = + pr_ident_decl (fname,univs) ++ spc() ++ pr_binders env sigma binders ++ spc() ++ str":" ++ + spc() ++ pr_lconstr_expr env sigma rtype ++ + pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr env sigma def) body_def ++ + prlist (pr_decl_notation @@ pr_constr env sigma) notations in return ( hov 0 (local ++ keyword "CoFixpoint" ++ spc() ++ diff --git a/vernac/ppvernac.mli b/vernac/ppvernac.mli index d4d49a09a3..9ade5afb87 100644 --- a/vernac/ppvernac.mli +++ b/vernac/ppvernac.mli @@ -14,7 +14,7 @@ val pr_set_entry_type : ('a -> Pp.t) -> 'a Extend.constr_entry_key_gen -> Pp.t (** Prints a fixpoint body *) -val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.t +val pr_rec_definition : Vernacexpr.fixpoint_expr -> Pp.t (** Prints a vernac expression without dot *) val pr_vernac_expr : Vernacexpr.vernac_expr -> Pp.t diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli index c9eb979a90..3bd252ecef 100644 --- a/vernac/pvernac.mli +++ b/vernac/pvernac.mli @@ -23,7 +23,7 @@ module Vernac_ : val command : vernac_expr Entry.t val syntax : vernac_expr Entry.t val vernac_control : vernac_control Entry.t - val rec_definition : (fixpoint_expr * decl_notation list) Entry.t + val rec_definition : fixpoint_expr Entry.t val noedit_mode : vernac_expr Entry.t val command_entry : vernac_expr Entry.t val main_entry : vernac_control option Entry.t diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 68b7462bde..9af8d8b67c 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -772,7 +772,7 @@ let vernac_inductive ~atts cum lo finite indl = let vernac_fixpoint_common ~atts discharge l = if Dumpglob.dump () then - List.iter (fun (((lid,_), _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; + List.iter (fun { fname } -> Dumpglob.dump_definition fname false "def") l; enforce_locality_exp atts.DefAttributes.locality discharge let vernac_fixpoint_interactive ~atts discharge l = @@ -793,7 +793,7 @@ let vernac_fixpoint ~atts discharge l = let vernac_cofixpoint_common ~atts discharge l = if Dumpglob.dump () then - List.iter (fun (((lid,_), _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; + List.iter (fun { fname } -> Dumpglob.dump_definition fname false "def") l; enforce_locality_exp atts.DefAttributes.locality discharge let vernac_cofixpoint_interactive ~atts discharge l = @@ -963,9 +963,10 @@ let vernac_include l = (* Sections *) -let vernac_begin_section ({v=id} as lid) = +let vernac_begin_section ~poly ({v=id} as lid) = Dumpglob.dump_definition lid true "sec"; - Lib.open_section id + Lib.open_section ~poly id; + set_bool_option_value_gen ~locality:OptLocal ["Universe"; "Polymorphism"] poly let vernac_end_section {CAst.loc} = Dumpglob.dump_reference ?loc @@ -2297,7 +2298,6 @@ let rec translate_vernac ~atts v = let open Vernacextend in match v with | VernacResetName _ | VernacResetInitial | VernacBack _ - | VernacBackTo _ | VernacAbort _ -> anomaly (str "type_vernac") (* Syntax *) @@ -2357,7 +2357,7 @@ let rec translate_vernac ~atts v = let open Vernacextend in match v with | VernacInductive (cum, priv, finite, l) -> VtDefault(fun () -> vernac_inductive ~atts cum priv finite l) | VernacFixpoint (discharge, l) -> - let opens = List.exists (fun ((_,_,_,_,p),_) -> Option.is_empty p) l in + let opens = List.exists (fun { body_def } -> Option.is_empty body_def) l in if opens then VtOpenProof (fun () -> with_def_attributes ~atts vernac_fixpoint_interactive discharge l) @@ -2365,7 +2365,7 @@ let rec translate_vernac ~atts v = let open Vernacextend in match v with VtDefault (fun () -> with_def_attributes ~atts vernac_fixpoint discharge l) | VernacCoFixpoint (discharge, l) -> - let opens = List.exists (fun ((_,_,_,p),_) -> Option.is_empty p) l in + let opens = List.exists (fun { body_def } -> Option.is_empty body_def) l in if opens then VtOpenProof(fun () -> with_def_attributes ~atts vernac_cofixpoint_interactive discharge l) else @@ -2396,8 +2396,7 @@ let rec translate_vernac ~atts v = let open Vernacextend in match v with (* Gallina extensions *) | VernacBeginSection lid -> VtNoProof(fun () -> - unsupported_attributes atts; - vernac_begin_section lid) + vernac_begin_section ~poly:(only_polymorphism atts) lid) | VernacEndSegment lid -> VtNoProof(fun () -> unsupported_attributes atts; @@ -2630,7 +2629,6 @@ and interp_expr ?proof ~atts ~st c = | VernacResetName _ -> anomaly (str "VernacResetName not handled by Stm.") | VernacResetInitial -> anomaly (str "VernacResetInitial not handled by Stm.") | VernacBack _ -> anomaly (str "VernacBack not handled by Stm.") - | VernacBackTo _ -> anomaly (str "VernacBackTo not handled by Stm.") (* This one is possible to handle here *) | VernacAbort id -> CErrors.user_err (str "Abort cannot be used through the Load command") diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index ee1f839b8d..0968632c2d 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -128,18 +128,26 @@ type definition_expr = | DefineBody of local_binder_expr list * Genredexpr.raw_red_expr option * constr_expr * constr_expr option -type fixpoint_expr = - ident_decl * recursion_order_expr option * local_binder_expr list * constr_expr * constr_expr option +type decl_notation = lstring * constr_expr * scope_name option + +type 'a fix_expr_gen = + { fname : lident + ; univs : universe_decl_expr option + ; rec_order : 'a + ; binders : local_binder_expr list + ; rtype : constr_expr + ; body_def : constr_expr option + ; notations : decl_notation list + } -type cofixpoint_expr = - ident_decl * local_binder_expr list * constr_expr * constr_expr option +type fixpoint_expr = recursion_order_expr option fix_expr_gen +type cofixpoint_expr = unit fix_expr_gen type local_decl_expr = | AssumExpr of lname * constr_expr | DefExpr of lname * constr_expr * constr_expr option type inductive_kind = Inductive_kw | CoInductive | Variant | Record | Structure | Class of bool (* true = definitional, false = inductive *) -type decl_notation = lstring * constr_expr * scope_name option type simple_binder = lident list * constr_expr type class_binder = lident * constr_expr list type 'a with_coercion = coercion_flag * 'a @@ -283,8 +291,8 @@ type nonrec vernac_expr = | VernacAssumption of (discharge * Decls.assumption_object_kind) * Declaremods.inline * (ident_decl list * constr_expr) with_coercion list | VernacInductive of vernac_cumulative option * bool (* private *) * inductive_flag * (inductive_expr * decl_notation list) list - | VernacFixpoint of discharge * (fixpoint_expr * decl_notation list) list - | VernacCoFixpoint of discharge * (cofixpoint_expr * decl_notation list) list + | VernacFixpoint of discharge * fixpoint_expr list + | VernacCoFixpoint of discharge * cofixpoint_expr list | VernacScheme of (lident option * scheme) list | VernacCombinedScheme of lident * lident list | VernacUniverse of lident list @@ -351,7 +359,6 @@ type nonrec vernac_expr = | VernacResetName of lident | VernacResetInitial | VernacBack of int - | VernacBackTo of int (* Commands *) | VernacCreateHintDb of string * bool diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml index 1dd8164ebc..747998c6cc 100644 --- a/vernac/vernacprop.ml +++ b/vernac/vernacprop.ml @@ -32,7 +32,6 @@ let rec has_Fail v = v |> CAst.with_val (function let is_navigation_vernac_expr = function | VernacResetInitial | VernacResetName _ - | VernacBackTo _ | VernacBack _ -> true | _ -> false |