diff options
78 files changed, 1400 insertions, 797 deletions
diff --git a/.gitignore b/.gitignore index c30fd850a1..4e02e7617c 100644 --- a/.gitignore +++ b/.gitignore @@ -145,7 +145,9 @@ plugins/ssr/ssrvernac.ml # other auto-generated files +kernel/byterun/coq_instruct.h kernel/byterun/coq_jumptbl.h +kernel/genOpcodeFiles.exe kernel/copcodes.ml kernel/uint63.ml ide/index_urls.txt diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index a1da9be20b..c5038d3bb0 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -209,6 +209,17 @@ after_script: variables: - $WINDOWS =~ /enabled/ +.deploy-template: &deploy-template + stage: deploy + before_script: + - which ssh-agent || ( apt-get update -y && apt-get install openssh-client -y ) + - eval $(ssh-agent -s) + - mkdir -p ~/.ssh + - chmod 700 ~/.ssh + - ssh-keyscan -t rsa github.com >> ~/.ssh/known_hosts + - git config --global user.name "coqbot" + - git config --global user.email "coqbot@users.noreply.github.com" + build:base: <<: *build-template variables: @@ -325,6 +336,21 @@ pkg:nix:deploy: - master - /^v.*\..*$/ +pkg:nix:deploy:channel: + <<: *deploy-template + environment: + name: cachix + url: https://coq.cachix.org + only: + variables: + - $CACHIX_DEPLOYMENT_KEY + dependencies: + - pkg:nix:deploy + script: + - echo "$CACHIX_DEPLOYMENT_KEY" | tr -d '\r' | ssh-add - > /dev/null + - git fetch --unshallow + - git push git@github.com:coq/coq-on-cachix "${CI_COMMIT_REF_NAME}" + pkg:nix: <<: *nix-template except: @@ -357,7 +383,7 @@ doc:stdlib:dune: - _build/default/doc/stdlib/html doc:refman:deploy: - stage: deploy + <<: *deploy-template environment: name: deployment url: https://coq.github.io/ @@ -368,14 +394,6 @@ doc:refman:deploy: - doc:ml-api:odoc - doc:refman:dune - doc:stdlib:dune - before_script: - - which ssh-agent || ( apt-get update -y && apt-get install openssh-client -y ) - - eval $(ssh-agent -s) - - mkdir -p ~/.ssh - - chmod 700 ~/.ssh - - ssh-keyscan -t rsa github.com >> ~/.ssh/known_hosts - - git config --global user.name "coqbot" - - git config --global user.email "coqbot@users.noreply.github.com" script: - echo "$DOCUMENTATION_DEPLOY_KEY" | tr -d '\r' | ssh-add - > /dev/null - git clone git@github.com:coq/doc.git _deploy @@ -566,6 +584,9 @@ library:ci-math-comp: library:ci-sf: <<: *ci-template +library:ci-stdlib2: + <<: *ci-template-flambda + library:ci-unimath: <<: *ci-template-flambda diff --git a/CHANGES.md b/CHANGES.md index af2b7991dd..59cc17c233 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -97,6 +97,9 @@ Tactics - Ltac backtraces can be turned on using the "Ltac Backtrace" option. +- The syntax of the `autoapply` tactic was fixed to conform with preexisting + documentation: it now takes a `with` clause instead of a `using` clause. + Vernacular commands - `Combined Scheme` can now work when inductive schemes are generated in sort diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index bb0e388cdd..31fa3d2c4a 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -1,34 +1,72 @@ # Contributing to Coq -Thank you for your interest in contributing to Coq! There are many ways to contribute, and we appreciate all of them. +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). ## Bug Reports -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](https://github.com/coq/coq/issues) (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](https://github.com/coq/coq/issues). 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. - -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 necessary to minimize your bug or identify precisely where the issue is, 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). +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: + +- 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 writting a bug report + +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 +necessary to minimize your bug or identify precisely where the issue is, +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. +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)). -For further help with the Coq sources, feel free to join -the [Coq Gitter chat](https://gitter.im/coq/coq) and ask questions. Please make pull requests against the `master` branch. @@ -41,10 +79,10 @@ 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 developments, on every pull request, but these results +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.md`](dev/ci/README.md#information-for-developers) for more +[`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 @@ -53,19 +91,30 @@ 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. 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. +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`. +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`. -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. +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`. - This label will be automatically added if you open or synchronize your PR and - it is not up-to-date with the base branch. So please, do not forget to rebase - your branch every time you update it. + 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] indicate the PR needs testing beyond what the test suite can handle. @@ -76,45 +125,86 @@ Here are a few tags Coq developers may add to your PR and what they mean. In gen To learn more about the merging process, you can read the [merging documentation for Coq maintainers](dev/doc/MERGING.md). -## Documentation - -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. +[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 -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. +[jenkins-doc]: https://github.com/coq/coq/wiki/Jenkins-(automated-benchmarking) -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/). +## Documentation -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. +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. -## Following the development +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. -If you want to follow the development activity around Coq, you are encouraged -to subscribe to the [Coqdev mailing list](https://sympa.inria.fr/sympa/info/coqdev). -This mailing list has reasonably low traffic. +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 may also choose to use GitHub feature to -["watch" this repository](https://github.com/coq/coq/subscription), but be -advised that this means receiving a very large number of notifications. -GitHub gives [some advice](https://blog.github.com/2017-07-18-managing-large-numbers-of-github-notifications/#prioritize-the-notifications-you-receive) -on how to configure your e-mail client to filter these notifications. -A possible alternative is to deactivate e-mail notifications and manage your -GitHub web notifications using a tool such as [Octobox](http://octobox.io/). +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 outside this repository +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. -There are many useful ways to contribute to the Coq ecosystem that don't involve the Coq repository. +## Where to get help (with the Coq source code, or anything else) -Tutorials to teach Coq, and especially to teach particular advanced features, would be 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. +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. +People are generally happy to help and very reactive. -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.md`](/dev/ci/README.md) for more information. +[Coq development category]: https://coq.discourse.group/c/coq-development -Ask and answer questions on [Stack Exchange](https://stackexchange.com/filters/299857/questions-tagged-coq-on-stackexchange-sites) which has a helpful community of Coq users. +## Watching the repository -Hang out on the Coq IRC channel, `irc://irc.freenode.net/#coq`, and help answer questions. +["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 [confifure 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/). -[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 +## Contributing outside this repository -[jenkins-doc]: https://github.com/coq/coq/wiki/Jenkins-(automated-benchmarking) +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 @@ -75,16 +75,22 @@ endef ## Files in the source tree +# instead of using "export FOO" do "COQ_EXPORTED += FOO" +# this makes it possible to clean up the environment in the subcall +COQ_EXPORTED := COQ_EXPORTED + LEXFILES := $(call find, '*.mll') YACCFILES := $(call find, '*.mly') -export MLLIBFILES := $(call find, '*.mllib') -export MLPACKFILES := $(call find, '*.mlpack') -export MLGFILES := $(call find, '*.mlg') -export CFILES := $(call findindir, 'kernel/byterun', '*.c') +MLLIBFILES := $(call find, '*.mllib') +MLPACKFILES := $(call find, '*.mlpack') +MLGFILES := $(call find, '*.mlg') +CFILES := $(call findindir, 'kernel/byterun', '*.c') +COQ_EXPORTED +=MLLIBFILES MLPACKFILES MLGFILES CFILES # NB our find wrapper ignores the test suite MERLININFILES := $(call find, '.merlin.in') test-suite/unit-tests/.merlin.in -export MERLINFILES := $(MERLININFILES:.in=) +MERLINFILES := $(MERLININFILES:.in=) +COQ_EXPORTED += MERLINFILES # NB: The lists of currently existing .ml and .mli files will change # before and after a build or a make clean. Hence we do not export @@ -97,17 +103,21 @@ EXISTINGMLI := $(call find, '*.mli') GENMLGFILES:= $(MLGFILES:.mlg=.ml) # GRAMFILES must be in linking order -export GRAMFILES=$(addprefix gramlib/.pack/gramlib__,Ploc Plexing Gramext Grammar) -export GRAMMLFILES := $(addsuffix .ml, $(GRAMFILES)) $(addsuffix .mli, $(GRAMFILES)) -export GENGRAMFILES := $(GRAMMLFILES) gramlib/.pack/gramlib.ml -export GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) ide/coqide_os_specific.ml kernel/copcodes.ml kernel/uint63.ml -export GENHFILES:=kernel/byterun/coq_jumptbl.h -export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) +GRAMFILES=$(addprefix gramlib/.pack/gramlib__,Ploc Plexing Gramext Grammar) +GRAMMLFILES := $(addsuffix .ml, $(GRAMFILES)) $(addsuffix .mli, $(GRAMFILES)) +GENGRAMFILES := $(GRAMMLFILES) gramlib/.pack/gramlib.ml +GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) ide/coqide_os_specific.ml kernel/copcodes.ml kernel/uint63.ml +GENHFILES:=kernel/byterun/coq_instruct.h kernel/byterun/coq_jumptbl.h +GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) +COQ_EXPORTED += GRAMFILES GRAMMLFILES GENGRAMFILES GENMLFILES GENHFILES GENFILES ## More complex file lists -export MLSTATICFILES := $(filter-out $(GENMLFILES), $(EXISTINGML)) -export MLIFILES := $(sort $(GENMLIFILES) $(EXISTINGMLI)) +MLSTATICFILES := $(filter-out $(GENMLFILES), $(EXISTINGML)) +MLIFILES := $(sort $(GENMLIFILES) $(EXISTINGMLI)) +COQ_EXPORTED += MLSTATICFILES MLIFILES + +export $(COQ_EXPORTED) include Makefile.common diff --git a/Makefile.build b/Makefile.build index ea356d5f8e..8b989f161a 100644 --- a/Makefile.build +++ b/Makefile.build @@ -11,6 +11,9 @@ # This makefile is normally called by the main Makefile after setting # some variables. +# Cleanup environment (avoids filling it up) +unexport $(COQ_EXPORTED) + ########################################################################### # User-customizable variables ########################################################################### @@ -316,11 +319,21 @@ $(LIBCOQRUN): kernel/byterun/coq_jumptbl.h $(BYTERUN) cd $(dir $(LIBCOQRUN)) && \ $(OCAMLFIND) ocamlmklib -oc $(COQRUN) $(notdir $(BYTERUN)) -kernel/byterun/coq_jumptbl.h : kernel/byterun/coq_instruct.h kernel/byterun/make_jumptbl.sh - kernel/byterun/make_jumptbl.sh $< $@ +kernel/genOpcodeFiles.exe: kernel/genOpcodeFiles.ml + $(SHOW)'OCAMLC $<' + $(HIDE)$(OCAMLC) -o $@ $< + +kernel/byterun/coq_instruct.h: kernel/genOpcodeFiles.exe + $(SHOW)'WRITE $@' + $(HIDE)$< enum > $@ -kernel/copcodes.ml: kernel/byterun/coq_instruct.h kernel/make_opcodes.sh kernel/make-opcodes - kernel/make_opcodes.sh $< $@ +kernel/byterun/coq_jumptbl.h: kernel/genOpcodeFiles.exe + $(SHOW)'WRITE $@' + $(HIDE)$< jump > $@ + +kernel/copcodes.ml: kernel/genOpcodeFiles.exe + $(SHOW)'WRITE $@' + $(HIDE)$< copml > $@ %.o: %.c $(SHOW)'OCAMLC $<' @@ -849,6 +862,18 @@ $(VDFILE).d: $(D_DEPEND_BEFORE_SRC) $(VFILES) $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT ########################################################################### + +# Useful to check that the exported variables are within the win32 limits + +printenv-real: + @env + @echo + @echo -n "Maxsize (win32 limit is 8k) : " + @env | wc -L + @echo -n "Total (win32 limit is 32k) : " + @env | wc -m + + # To speed-up things a bit, let's dissuade make to attempt rebuilding makefiles Makefile $(wildcard Makefile.*) config/Makefile : ; @@ -863,5 +888,5 @@ Makefile $(wildcard Makefile.*) config/Makefile : ; # For emacs: # Local Variables: -# mode: makefile +# mode: makefile-gmake # End: diff --git a/Makefile.ci b/Makefile.ci index 0307d39d54..9180d51bee 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -40,6 +40,7 @@ CI_TARGETS= \ ci-relation-algebra \ ci-sf \ ci-simple-io \ + ci-stdlib2 \ ci-tlc \ ci-unimath \ ci-verdi-raft \ diff --git a/Makefile.dune b/Makefile.dune index da4c59af75..4609c563d9 100644 --- a/Makefile.dune +++ b/Makefile.dune @@ -3,7 +3,7 @@ .PHONY: help voboot states world watch check # Main developer targets .PHONY: coq coqide coqide-server # Package targets -.PHONY: quickbyte quickopt # Partial / quick developer targets +.PHONY: quickbyte quickopt quickide # Partial / quick developer targets .PHONY: refman-html stdlib-html apidoc # Documentation targets .PHONY: test-suite release # Accesory targets .PHONY: ocheck trunk ireport clean # Maintenance targets @@ -27,6 +27,7 @@ help: @echo "" @echo " - quickbyte: build main ML files [coqtop + plugins + ide + printers] using the bytecode compiler" @echo " - quickopt: build main ML files [coqtop + plugins + ide + printers] using the optimizing compiler" + @echo " - quickide: build main IDE files [client + server + prelude] using the optimizing compiler" @echo "" @echo " - test-suite: run Coq's test suite" @echo " - refman-html: build Coq's reference manual [HTML version]" @@ -40,12 +41,14 @@ help: @echo " - clean: remove build directory and autogenerated files" @echo " - help: show this message" +# We need to bootstrap with a dummy coq.plugins.ltac so install targets do work. voboot: + @echo "(library (name ltac_plugin) (public_name coq.plugins.ltac) (modules_without_implementation extraargs extratactics))" > plugins/ltac/dune dune build $(DUNEOPT) @vodeps dune exec ./tools/coq_dune.exe $(BUILD_CONTEXT)/.vfiles.d states: voboot - dune build $(DUNEOPT) theories/Init/Prelude.vo + dune build --display=short $(DUNEOPT) dev/shim/coqtop-prelude world: voboot dune build $(DUNEOPT) @install @@ -77,6 +80,9 @@ quickbyte: voboot quickopt: voboot dune build $(DUNEOPT) $(QUICKOPT_TARGETS) +quickide: states + dune build $(DUNEOPT) dev/shim/coqide-prelude + test-suite: voboot dune runtest --no-buffer $(DUNEOPT) @@ -68,25 +68,25 @@ and the [Coq FAQ](https://github.com/coq/coq/wiki/The-Coq-FAQ), for additional user-contributed documentation. ## Changes + There is a file named [`CHANGES.md`](CHANGES.md) that explains the differences and the incompatibilities since last versions. If you upgrade Coq, please read it carefully. -## The Coq Club -The Coq Club moderated mailing list is meant to be a standard way -to discuss questions about the Coq system and related topics. The -subscription link can be found at [coq.inria.fr/community](http://coq.inria.fr/community). +## Questions and discussion + +We have a number of channels to reach the user community and the +development team: -The topics to be discussed in the club should include: +- Our [Discourse forum](https://coq.discourse.group). +- Our mailing list, the [Coq-Club](https://sympa.inria.fr/sympa/info/coq-club). +- Our [Gitter channel][gitter-link], which is a good way to reach + developers for quick chat and development questions. -* technical problems; -* questions about proof developments; -* suggestions and questions about the implementation; -* announcements of proofs; -* theoretical questions about typed lambda-calculi which are - closely related to Coq. +See also [coq.inria.fr/community](https://coq.inria.fr/community.html). ## Bugs report + Please report any bug / feature request in [our issue tracker](https://github.com/coq/coq/issues). To be effective, bug reports should mention the OCaml version used diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml index 4329b2d743..b681fb876e 100644 --- a/checker/checkInductive.ml +++ b/checker/checkInductive.ml @@ -89,6 +89,9 @@ let eq_recarg a1 a2 = match a1, a2 with let eq_reloc_tbl = Array.equal (fun x y -> Int.equal (fst x) (fst y) && Int.equal (snd x) (snd y)) +let eq_in_context (ctx1, t1) (ctx2, t2) = + Context.Rel.equal Constr.equal ctx1 ctx2 && Constr.equal t1 t2 + let check_packet env mind ind { mind_typename; mind_arity_ctxt; mind_arity; mind_consnames; mind_user_lc; mind_nrealargs; mind_nrealdecls; mind_kelim; mind_nf_lc; @@ -105,7 +108,7 @@ let check_packet env mind ind check "mind_nrealdecls" Int.(equal ind.mind_nrealdecls mind_nrealdecls); check "mind_kelim" (check_kelim ind.mind_kelim mind_kelim); - check "mind_nf_lc" (Array.equal Constr.equal ind.mind_nf_lc mind_nf_lc); + check "mind_nf_lc" (Array.equal eq_in_context ind.mind_nf_lc mind_nf_lc); (* NB: here syntactic equality is not just an optimisation, we also care about the shape of the terms *) diff --git a/checker/values.ml b/checker/values.ml index 66467fa8f5..bcac3014be 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -261,7 +261,7 @@ let v_one_ind = v_tuple "one_inductive_body" Int; Int; List v_sortfam; - Array v_constr; + Array (v_pair v_rctxt v_constr); Array Int; Array Int; v_wfp; diff --git a/clib/cMap.ml b/clib/cMap.ml index e4ce6c7c02..016d8bdeca 100644 --- a/clib/cMap.ml +++ b/clib/cMap.ml @@ -36,6 +36,7 @@ sig val fold_right : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b val height : 'a t -> int val filter_range : (key -> int) -> 'a t -> 'a t + val update: key -> ('a option -> 'a option) -> 'a t -> 'a t module Smart : sig val map : ('a -> 'a) -> 'a t -> 'a t @@ -64,6 +65,7 @@ sig val fold_right : (M.t -> 'a -> 'b -> 'b) -> 'a map -> 'b -> 'b val height : 'a map -> int val filter_range : (M.t -> int) -> 'a map -> 'a map + val update: M.t -> ('a option -> 'a option) -> 'a map -> 'a map module Smart : sig val map : ('a -> 'a) -> 'a map -> 'a map @@ -94,8 +96,8 @@ struct type set = S.t type 'a _map = - | MEmpty - | MNode of 'a map * M.t * 'a * 'a map * int + | MEmpty + | MNode of {l:'a map; v:F.key; d:'a; r:'a map; h:int} type _set = | SEmpty @@ -108,41 +110,41 @@ struct let rec set k v (s : 'a map) : 'a map = match map_prj s with | MEmpty -> raise Not_found - | MNode (l, k', v', r, h) -> + | MNode {l; v=k'; d=v'; r; h} -> let c = M.compare k k' in if c < 0 then let l' = set k v l in if l == l' then s - else map_inj (MNode (l', k', v', r, h)) + else map_inj (MNode {l=l'; v=k'; d=v'; r; h}) else if c = 0 then if v' == v then s - else map_inj (MNode (l, k', v, r, h)) + else map_inj (MNode {l; v=k'; d=v; r; h}) else let r' = set k v r in if r == r' then s - else map_inj (MNode (l, k', v', r', h)) + else map_inj (MNode {l; v=k'; d=v'; r=r'; h}) let rec modify k f (s : 'a map) : 'a map = match map_prj s with | MEmpty -> raise Not_found - | MNode (l, k', v, r, h) -> - let c = M.compare k k' in + | MNode {l; v; d; r; h} -> + let c = M.compare k v in if c < 0 then let l' = modify k f l in if l == l' then s - else map_inj (MNode (l', k', v, r, h)) + else map_inj (MNode {l=l'; v; d; r; h}) else if c = 0 then - let v' = f k' v in - if v' == v then s - else map_inj (MNode (l, k', v', r, h)) + let d' = f v d in + if d' == d then s + else map_inj (MNode {l; v; d=d'; r; h}) else let r' = modify k f r in if r == r' then s - else map_inj (MNode (l, k', v, r', h)) + else map_inj (MNode {l; v; d; r=r'; h}) let rec domain (s : 'a map) : set = match map_prj s with | MEmpty -> set_inj SEmpty - | MNode (l, k, _, r, h) -> - set_inj (SNode (domain l, k, domain r, h)) + | MNode {l; v; r; h; _} -> + set_inj (SNode (domain l, v, domain r, h)) (** This function is essentially identity, but OCaml current stdlib does not take advantage of the similarity of the two structures, so we introduce this unsafe loophole. *) @@ -150,31 +152,31 @@ struct let rec bind f (s : set) : 'a map = match set_prj s with | SEmpty -> map_inj MEmpty | SNode (l, k, r, h) -> - map_inj (MNode (bind f l, k, f k, bind f r, h)) + map_inj (MNode { l=bind f l; v=k; d=f k; r=bind f r; h}) (** Dual operation of [domain]. *) let rec fold_left f (s : 'a map) accu = match map_prj s with | MEmpty -> accu - | MNode (l, k, v, r, h) -> + | MNode {l; v=k; d=v; r; h} -> let accu = f k v (fold_left f l accu) in fold_left f r accu let rec fold_right f (s : 'a map) accu = match map_prj s with | MEmpty -> accu - | MNode (l, k, v, r, h) -> + | MNode {l; v=k; d=v; r; h} -> let accu = f k v (fold_right f r accu) in fold_right f l accu let height s = match map_prj s with | MEmpty -> 0 - | MNode (_, _, _, _, h) -> h + | MNode {h;_} -> h (* Filter based on a range *) let filter_range in_range m = let rec aux m = function | MEmpty -> m - | MNode (l, k, v, r, _) -> - let vr = in_range k in + | MNode {l; v; d; r; _} -> + let vr = in_range v in (* the range is below the current value *) if vr < 0 then aux m (map_prj l) (* the range is above the current value *) @@ -183,29 +185,102 @@ struct else let m = aux m (map_prj l) in let m = aux m (map_prj r) in - F.add k v m + F.add v d m in aux F.empty (map_prj m) + (* Imported from OCaml upstream until we can bump the version *) + let create l x d r = + let hl = height l and hr = height r in + map_inj @@ MNode{l; v=x; d; r; h=(if hl >= hr then hl + 1 else hr + 1)} + + let bal l x d r = + let hl = match map_prj l with MEmpty -> 0 | MNode {h} -> h in + let hr = match map_prj r with MEmpty -> 0 | MNode {h} -> h in + if hl > hr + 2 then begin + match map_prj l with + | MEmpty -> invalid_arg "Map.bal" + | MNode{l=ll; v=lv; d=ld; r=lr} -> + if height ll >= height lr then + create ll lv ld (create lr x d r) + else begin + match map_prj lr with + | MEmpty -> invalid_arg "Map.bal" + | MNode{l=lrl; v=lrv; d=lrd; r=lrr}-> + create (create ll lv ld lrl) lrv lrd (create lrr x d r) + end + end else if hr > hl + 2 then begin + match map_prj r with + | MEmpty -> invalid_arg "Map.bal" + | MNode{l=rl; v=rv; d=rd; r=rr} -> + if height rr >= height rl then + create (create l x d rl) rv rd rr + else begin + match map_prj rl with + | MEmpty -> invalid_arg "Map.bal" + | MNode{l=rll; v=rlv; d=rld; r=rlr} -> + create (create l x d rll) rlv rld (create rlr rv rd rr) + end + end else + map_inj @@ MNode{l; v=x; d; r; h=(if hl >= hr then hl + 1 else hr + 1)} + + let rec remove_min_binding m = match map_prj m with + | MEmpty -> invalid_arg "Map.remove_min_elt" + | MNode {l;v;d;r;_} -> + match map_prj l with + | MEmpty -> r + | _ -> bal (remove_min_binding l) v d r + + let merge t1 t2 = + match (map_prj t1, map_prj t2) with + (MEmpty, t) -> map_inj t + | (t, MEmpty) -> map_inj t + | (_, _) -> + let (x, d) = F.min_binding t2 in + bal t1 x d (remove_min_binding t2) + + let rec update x f m = match map_prj m with + | MEmpty -> + begin match f None with + | None -> map_inj MEmpty + | Some data -> map_inj @@ MNode{l=map_inj MEmpty; v=x; d=data; r=map_inj MEmpty; h=1} + end + | MNode {l; v; d; r; h} as m -> + let c = M.compare x v in + if c = 0 then begin + match f (Some d) with + | None -> merge l r + | Some data -> + if d == data then map_inj m else + map_inj @@ MNode{l; v=x; d=data; r; h} + end else if c < 0 then + let ll = update x f l in + if l == ll then map_inj m else bal ll v d r + else + let rr = update x f r in + if r == rr then map_inj m else bal l v d rr + + (* End of Imported OCaml *) + module Smart = struct let rec map f (s : 'a map) = match map_prj s with | MEmpty -> map_inj MEmpty - | MNode (l, k, v, r, h) -> + | MNode {l; v=k; d=v; r; h} -> let l' = map f l in let r' = map f r in let v' = f v in if l == l' && r == r' && v == v' then s - else map_inj (MNode (l', k, v', r', h)) + else map_inj (MNode {l=l'; v=k; d=v'; r=r'; h}) let rec mapi f (s : 'a map) = match map_prj s with | MEmpty -> map_inj MEmpty - | MNode (l, k, v, r, h) -> + | MNode {l; v=k; d=v; r; h} -> let l' = mapi f l in let r' = mapi f r in let v' = f k v in if l == l' && r == r' && v == v' then s - else map_inj (MNode (l', k, v', r', h)) + else map_inj (MNode {l=l'; v=k; d=v'; r=r'; h}) end @@ -214,9 +289,9 @@ struct let rec map f (s : 'a map) : 'b map = match map_prj s with | MEmpty -> map_inj MEmpty - | MNode (l, k, v, r, h) -> + | MNode {l; v=k; d=v; r; h} -> let (k, v) = f k v in - map_inj (MNode (map f l, k, v, map f r, h)) + map_inj (MNode {l=map f l; v=k; d=v; r=map f r; h}) end @@ -227,14 +302,14 @@ struct let rec fold_left f s accu = match map_prj s with | MEmpty -> return accu - | MNode (l, k, v, r, h) -> + | MNode {l; v=k; d=v; r; h} -> fold_left f l accu >>= fun accu -> f k v accu >>= fun accu -> fold_left f r accu let rec fold_right f s accu = match map_prj s with | MEmpty -> return accu - | MNode (l, k, v, r, h) -> + | MNode {l; v=k; d=v; r; h} -> fold_right f r accu >>= fun accu -> f k v accu >>= fun accu -> fold_right f l accu diff --git a/clib/cMap.mli b/clib/cMap.mli index ca6ddb2f4e..9bbb8d50dd 100644 --- a/clib/cMap.mli +++ b/clib/cMap.mli @@ -66,6 +66,18 @@ sig [filter_range] returns the submap of [m] whose keys are in range. Note that [in_range] has to define a continouous range. *) + val update: key -> ('a option -> 'a option) -> 'a t -> 'a t + (** [update x f m] returns a map containing the same bindings as + [m], except for the binding of [x]. Depending on the value of + [y] where [y] is [f (find_opt x m)], the binding of [x] is + added, removed or updated. If [y] is [None], the binding is + removed if it exists; otherwise, if [y] is [Some z] then [x] + is associated to [z] in the resulting map. If [x] was already + bound in [m] to a value that is physically equal to [z], [m] + is returned unchanged (the result of the function is then + physically equal to [m]). + *) + module Smart : sig val map : ('a -> 'a) -> 'a t -> 'a t diff --git a/clib/hMap.ml b/clib/hMap.ml index 5d634b7af0..09ffb39c21 100644 --- a/clib/hMap.ml +++ b/clib/hMap.ml @@ -408,6 +408,18 @@ struct let filter_range f s = filter (fun x _ -> f x = 0) s + let update k f m = + let aux = function + | None -> (match f None with + | None -> None + | Some v -> Some (Map.singleton k v)) + | Some m -> + let m = Map.update k f m in + if Map.is_empty m then None + else Some m + in + Int.Map.update (M.hash k) aux m + module Unsafe = struct let map f s = diff --git a/default.nix b/default.nix index b65d736d79..3290f5dee8 100644 --- a/default.nix +++ b/default.nix @@ -78,7 +78,6 @@ stdenv.mkDerivation rec { !elem (baseNameOf path) [".git" "result" "bin" "_build" "_build_ci"]) ./.; preConfigure = '' - patchShebangs kernel/ patchShebangs dev/tools/ ''; diff --git a/dev/README.md b/dev/README.md index d9fdd230d3..9761f7b96f 100644 --- a/dev/README.md +++ b/dev/README.md @@ -25,7 +25,6 @@ | [`dev/doc/universes.txt`](doc/universes.txt) | Help for debugging universes | | [`dev/doc/extensions.txt`](doc/extensions.txt) | Some help about TACTIC EXTEND | | [`dev/doc/perf-analysis`](doc/perf-analysis)| Analysis of perfs measured on the compilation of user contribs | -| [`dev/doc/cic.dtd`](doc/cic.dtd) | Official dtd of the calc. of ind. constr. for im/ex-portation | | [`dev/doc/econstr.md`](doc/econstr.md) | Describes `Econstr`, implementation of treatment of `evar` in the engine | | [`dev/doc/primproj.md`](doc/primproj.md) | Describes primitive projections | | [`dev/doc/proof-engine.md`](doc/proof-engine.md) | Tutorial on new proof engine | diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat index 8489bcfc3a..c8cfcf60c8 100755 --- a/dev/build/windows/MakeCoq_MinGW.bat +++ b/dev/build/windows/MakeCoq_MinGW.bat @@ -373,7 +373,8 @@ IF "%RUNSETUP%"=="Y" ( -P make,unzip ^
-P gdb,liblzma5 ^
-P patch,automake1.14 ^
- -P mingw64-%ARCH%-binutils,mingw64-%ARCH%-gcc-core,mingw64-%ARCH%-gcc-g++,mingw64-%ARCH%-pkg-config,mingw64-%ARCH%-windows_default_manifest ^
+ -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 libiconv-devel,libunistring-devel,libncurses-devel ^
-P gettext-devel,libgettextpo-devel ^
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 2e934ff0c0..43f44a80b4 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1202,7 +1202,7 @@ function make_lablgtk { make_gtk_sourceview2 if build_prep https://forge.ocamlcore.org/frs/download.php/1726 lablgtk-2.18.6 tar.gz 1 ; then # configure should be fixed to search for $TARGET_ARCH-pkg-config.exe - cp "/bin/$TARGET_ARCH-pkg-config.exe" bin_special/pkg-config.exe + cp "/bin/$TARGET_ARCH-pkg-config" bin_special/pkg-config logn configure ./configure --build="$BUILD" --host="$HOST" --target="$TARGET" --prefix="$PREFIXOCAML" # lablgtk shows occasional errors with -j, so don't pass $MAKE_OPT diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 74e8d3bbaa..deeec3942d 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -289,3 +289,10 @@ : "${verdi_raft_CI_REF:=master}" : "${verdi_raft_CI_GITURL:=https://github.com/uwplse/verdi-raft}" : "${verdi_raft_CI_ARCHIVEURL:=${verdi_raft_CI_GITURL}/archive}" + +######################################################################## +# stdlib2 +######################################################################## +: "${stdlib2_CI_REF:=master}" +: "${stdlib2_CI_GITURL:=https://github.com/coq/stdlib2}" +: "${stdlib2_CI_ARCHIVEURL:=${stdlib2_CI_GITURL}/archive}" diff --git a/dev/ci/ci-stdlib2.sh b/dev/ci/ci-stdlib2.sh new file mode 100755 index 0000000000..ec1c180d7d --- /dev/null +++ b/dev/ci/ci-stdlib2.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download stdlib2 + +( cd "${CI_BUILD_DIR}/stdlib2/src" && ./bootstrap && make && make install) diff --git a/dev/ci/user-overlays/09476-ppedrot-context-constructor.sh b/dev/ci/user-overlays/09476-ppedrot-context-constructor.sh new file mode 100644 index 0000000000..1af8b5430d --- /dev/null +++ b/dev/ci/user-overlays/09476-ppedrot-context-constructor.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "9476" ] || [ "$CI_BRANCH" = "context-constructor" ]; then + + quickchick_CI_REF=context-constructor + quickchick_CI_GITURL=https://github.com/ppedrot/QuickChick + + equations_CI_REF=context-constructor + equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations + +fi diff --git a/dev/doc/README-V1-V5.asciidoc b/dev/doc/README-V1-V5.asciidoc deleted file mode 100644 index 631fb92c97..0000000000 --- a/dev/doc/README-V1-V5.asciidoc +++ /dev/null @@ -1,378 +0,0 @@ -Notes on the prehistory of Coq -============================== -:author: Thierry Coquand, Gérard Huet & Christine Paulin-Mohring -:revdate: September 2015 -:toc: -:toc-placement: preamble -:toclevels: 1 -:showtitle: - - -This document is a copy within the Coq archive of a document written -in September 2015 by Gérard Huet, Thierry Coquand and Christine Paulin -to accompany their public release of the archive of versions 1.10 to 6.2 -of Coq and of its CONSTR ancestor. CONSTR, then Coq, was designed and -implemented in the Formel team, joint between the INRIA Rocquencourt -laboratory and the Ecole Normale Supérieure of Paris, from 1984 -onwards. - -Version 1 ---------- - -This software is a prototype type-checker for a higher-order logical -formalism known as the Theory of Constructions, presented in his PhD -thesis by Thierry Coquand, with influences from Girard's system F and -de Bruijn's Automath. The metamathematical analysis of the system is -the PhD work of Thierry Coquand. The software is mostly the work of -Gérard Huet. Most of the mathematical examples verified with the -software are due to Thierry Coquand. - -The programming language of the CONSTR software (as it was called at -the time) was a version of ML adapted from the Edinburgh LCF system -and running on a LISP backend. The main improvements from the original -LCF ML were that ML was compiled rather than interpreted (Gérard Huet -building on the original translator by Lockwood Morris), and that it -was enriched by recursively defined types (work of Guy -Cousineau). This ancestor of CAML was used and improved by Larry -Paulson for his implementation of Cambridge LCF. - -Software developments of this prototype occurred from late 1983 to -early 1985. - -Version 1.10 was frozen on December 22nd 1984. It is the version used -for the examples in Thierry Coquand's thesis, defended on January 31st -1985. There was a unique binding operator, used both for universal -quantification (dependent product) at the level of types and -functional abstraction (λ) at the level of terms/proofs, in the manner -of Automath. Substitution (λ-reduction) was implemented using de -Bruijn's indexes. - -Version 1.11 was frozen on February 19th, 1985. It is the version used -for the examples in the paper: Th. Coquand, G. Huet. __Constructions: A -Higher Order Proof System for Mechanizing Mathematics__ <<CH85>>. - -Christine Paulin joined the team at this point, for her DEA research -internship. In her DEA memoir (August 1985) she presents developments -for the _lambo_ function – _lambo(f)(n)_ computes the minimal _m_ such -that _f(m)_ is greater than _n_, for _f_ an increasing integer -function, a challenge for constructive mathematics. She also encoded -the majority voting algorithm of Boyer and Moore. - -Version 2 ---------- - -The formal system, now renamed as the _Calculus of Constructions_, was -presented with a proof of consistency and comparisons with proof -systems of Per Martin Löf, Girard, and the Automath family of N. de -Bruijn, in the paper: T. Coquand and G. Huet. __The Calculus of -Constructions__ <<CH88>>. - -An abstraction of the software design, in the form of an abstract -machine for proof checking, and a fuller sequence of mathematical -developments was presented in: Th. Coquand, G. Huet. __Concepts -Mathématiques et Informatiques Formalisés dans le Calcul des -Constructions__<<CH87>>. - -Version 2.8 was frozen on December 16th, 1985, and served for -developing the exemples in the above papers. - -This calculus was then enriched in version 2.9 with a cumulative -hierarchy of universes. Universe levels were initially explicit -natural numbers. Another improvement was the possibility of automatic -synthesis of implicit type arguments, relieving the user of tedious -redundant declarations. - -Christine Paulin wrote an article __Algorithm development in the -Calculus of Constructions__ <<P86>>. Besides _lambo_ and _majority_, -she presents quicksort and a text formatting algorithm. - -Version 2.13 of the Calculus of Constructions with universes was -frozen on June 25th, 1986. - -A synthetic presentation of type theory along constructive lines with -ML algorithms was given by Gérard Huet in his May 1986 CMU course -notes _Formal Structures for Computation and Deduction_. Its chapter -_Induction and Recursion in the Theory of Constructions_ was presented -as an invited paper at the Joint Conference on Theory and Practice of -Software Development TAPSOFT’87 at Pise in March 1987, and published -as __Induction Principles Formalized in the Calculus of -Constructions__ <<H88>>. - -Version 3 ---------- - -This version saw the beginning of proof automation, with a search -algorithm inspired from PROLOG and the applicative logic programming -programs of the course notes _Formal structures for computation and -deduction_. The search algorithm was implemented in ML by Thierry -Coquand. The proof system could thus be used in two modes: proof -verification and proof synthesis, with tactics such as `AUTO`. - -The implementation language was now called CAML, for Categorical -Abstract Machine Language. It used as backend the LLM3 virtual machine -of Le Lisp by Jérôme Chailloux. The main developers of CAML were -Michel Mauny, Ascander Suarez and Pierre Weis. - -V3.1 was started in the summer of 1986, V3.2 was frozen at the end of -November 1986. V3.4 was developed in the first half of 1987. - -Thierry Coquand held a post-doctoral position in Cambrige University -in 1986-87, where he developed a variant implementation in SML, with -which he wrote some developments on fixpoints in Scott's domains. - -Version 4 ---------- - -This version saw the beginning of program extraction from proofs, with -two varieties of the type `Prop` of propositions, indicating -constructive intent. The proof extraction algorithms were implemented -by Christine Paulin-Mohring. - -V4.1 was frozen on July 24th, 1987. It had a first identified library -of mathematical developments (directory exemples), with libraries -Logic (containing impredicative encodings of intuitionistic logic and -algebraic primitives for booleans, natural numbers and list), `Peano` -developing second-order Peano arithmetic, `Arith` defining addition, -multiplication, euclidean division and factorial. Typical developments -were the Knaster-Tarski theorem and Newman's lemma from rewriting -theory. - -V4.2 was a joint development of a team consisting of Thierry Coquand, -Gérard Huet and Christine Paulin-Mohring. A file V4.2.log records the -log of changes. It was frozen on September 1987 as the last version -implemented in CAML 2.3, and V4.3 followed on CAML 2.5, a more stable -development system. - -V4.3 saw the first top-level of the system. Instead of evaluating -explicit quotations, the user could develop his mathematics in a -high-level language called the mathematical vernacular (following -Automath terminology). The user could develop files in the vernacular -notation (with .v extension) which were now separate from the `ml` -sources of the implementation. Gilles Dowek joined the team to -develop the vernacular language as his DEA internship research. - -A notion of sticky constant was introduced, in order to keep names of -lemmas when local hypotheses of proofs were discharged. This gave a -notion of global mathematical environment with local sections. - -Another significant practical change was that the system, originally -developped on the VAX central computer of our lab, was transferred on -SUN personal workstations, allowing a level of distributed -development. The extraction algorithm was modified, with three -annotations `Pos`, `Null` and `Typ` decorating the sorts `Prop` and -`Type`. - -Version 4.3 was frozen at the end of November 1987, and was -distributed to an early community of users (among those were Hugo -Herbelin and Loic Colson). - -V4.4 saw the first version of (encoded) inductive types. Now natural -numbers could be defined as: - -[source, coq] -Inductive NAT : Prop = O : NAT | Succ : NAT->NAT. - -These inductive types were encoded impredicatively in the calculus, -using a subsystem _rec_ due to Christine Paulin. V4.4 was frozen on -March 6th 1988. - -Version 4.5 was the first one to support inductive types and program -extraction. Its banner was _Calcul des Constructions avec -Réalisations et Synthèse_. The vernacular language was enriched to -accommodate extraction commands. - -The verification engine design was presented as: G. Huet. _The -Constructive Engine_. Version 4.5. Invited Conference, 2nd European -Symposium on Programming, Nancy, March 88. The final paper, -describing the V4.9 implementation, appeared in: A perspective in -Theoretical Computer Science, Commemorative Volume in memory of Gift -Siromoney, Ed. R. Narasimhan, World Scientific Publishing, 1989. - -Version 4.5 was demonstrated in June 1988 at the YoP Institute on -Logical Foundations of Functional Programming organized by Gérard Huet -at Austin, Texas. - -Version 4.6 was started during the summer of 1988. Its main -improvement was the complete rehaul of the proof synthesis engine by -Thierry Coquand, with a tree structure of goals. - -Its source code was communicated to Randy Pollack on September 2nd -1988. It evolved progressively into LEGO, proof system for Luo's -formalism of Extended Calculus of Constructions. - -The discharge tactic was modified by Gérard Huet to allow for -inter-dependencies in discharged lemmas. Christine Paulin improved the -inductive definition scheme in order to accommodate predicates of any -arity. - -Version 4.7 was started on September 6th, 1988. - -This version starts exploiting the CAML notion of module in order to -improve the modularity of the implementation. Now the term verifier is -identified as a proper module Machine, which the structure of its -internal data structures being hidden and thus accessible only through -the legitimate operations. This machine (the constructive engine) was -the trusted core of the implementation. The proof synthesis mechanism -was a separate proof term generator. Once a complete proof term was -synthesized with the help of tactics, it was entirely re-checked by -the engine. Thus there was no need to certify the tactics, and the -system took advantage of this fact by having tactics ignore the -universe levels, universe consistency check being relegated to the -final type-checking pass. This induced a certain puzzlement in early -users who saw, after a successful proof search, their `QED` followed -by silence, followed by a failure message due to a universe -inconsistency… - -The set of examples comprise set theory experiments by Hugo Herbelin, -and notably the Schroeder-Bernstein theorem. - -Version 4.8, started on October 8th, 1988, saw a major -re-implementation of the abstract syntax type `constr`, separating -variables of the formalism and metavariables denoting incomplete terms -managed by the search mechanism. A notion of level (with three values -`TYPE`, `OBJECT` and `PROOF`) is made explicit and a type judgement -clarifies the constructions, whose implementation is now fully -explicit. Structural equality is speeded up by using pointer equality, -yielding spectacular improvements. Thierry Coquand adapts the proof -synthesis to the new representation, and simplifies pattern matching -to first-order predicate calculus matching, with important performance -gain. - -A new representation of the universe hierarchy is then defined by -Gérard Huet. Universe levels are now implemented implicitly, through -a hidden graph of abstract levels constrained with an order relation. -Checking acyclicity of the graph insures well-foundedness of the -ordering, and thus consistency. This was documented in a memo _Adding -Type:Type to the Calculus of Constructions_ which was never published. - -The development version is released as a stable 4.8 at the end of -1988. - -Version 4.9 is released on March 1st 1989, with the new ``elastic'' -universe hierarchy. - -The spring of 1989 saw the first attempt at documenting the system -usage, with a number of papers describing the formalism: - -- _Metamathematical Investigations of a Calculus of Constructions_, by - Thierry Coquand <<C90>>, -- _Inductive definitions in the Calculus of Constructions_, by - Christine Paulin-Mohrin, -- _Extracting Fω's programs from proofs in the Calculus of - Constructions_, by Christine Paulin-Mohring <<P89>>, -- _The Constructive Engine_, by Gérard Huet <<H89>>, - -as well as a number of user guides: - -- _A short user's guide for the Constructions_ Version 4.10, by Gérard Huet -- _A Vernacular Syllabus_, by Gilles Dowek. -- _The Tactics Theorem Prover, User's guide_, Version 4.10, by Thierry - Coquand. - -Stable V4.10, released on May 1st, 1989, was then a mature system, -distributed with CAML V2.6. - -In the mean time, Thierry Coquand and Christine Paulin-Mohring had -been investigating how to add native inductive types to the Calculus -of Constructions, in the manner of Per Martin-Löf's Intuitionistic -Type Theory. The impredicative encoding had already been presented in: -F. Pfenning and C. Paulin-Mohring. __Inductively defined types in the -Calculus of Constructions__ <<PP90>>. An extension of the calculus -with primitive inductive types appeared in: Th. Coquand and -C. Paulin-Mohring. __Inductively defined types__ <<CP90>>. - -This led to the Calculus of Inductive Constructions, logical formalism -implemented in Versions 5 upward of the system, and documented in: -C. Paulin-Mohring. __Inductive Definitions in the System Coq - Rules -and Properties__ <<P93>>. - -The last version of CONSTR is Version 4.11, which was last distributed -in the spring of 1990. It was demonstrated at the first workshop of -the European Basic Research Action Logical Frameworks In Sophia -Antipolis in May 1990. - -At the end of 1989, Version 5.1 was started, and renamed as the system -Coq for the Calculus of Inductive Constructions. It was then ported to -the new stand-alone implementation of ML called Caml-light. - -In 1990 many changes occurred. Thierry Coquand left for Chalmers -University in Göteborg. Christine Paulin-Mohring took a CNRS -researcher position at the LIP laboratory of École Normale Supérieure -de Lyon. Project Formel was terminated, and gave rise to two teams: -Cristal at INRIA-Roquencourt, that continued developments in -functional programming with Caml-light then Ocaml, and Coq, continuing -the type theory research, with a joint team headed by Gérard Huet at -INRIA-Rocquencourt and Christine Paulin-Mohring at the LIP laboratory -of CNRS-ENS Lyon. - -Chetan Murthy joined the team in 1991 and became the main software -architect of Version 5. He completely rehauled the implementation for -efficiency. Versions 5.6 and 5.8 were major distributed versions, -with complete documentation and a library of users' developements. The -use of the RCS revision control system, and systematic ChangeLog -files, allow a more precise tracking of the software developments. - -Developments from Version 6 upwards are documented in the credits -section of Coq's Reference Manual. - -==== -September 2015 + -Thierry Coquand, Gérard Huet and Christine Paulin-Mohring. -==== - -[bibliography] -.Bibliographic references - -- [[[CH85]]] Th. Coquand, G. Huet. _Constructions: A Higher Order - Proof System for Mechanizing Mathematics_. Invited paper, EUROCAL85, - April 1985, Linz, Austria. Springer Verlag LNCS 203, pp. 151-184. - -- [[[CH88]]] T. Coquand and G. Huet. _The Calculus of Constructions_. - Submitted on June 30th 1985, accepted on December 5th, 1985, - Information and Computation. Preprint as Rapport de Recherche Inria - n°530, Mai 1986. Final version in Information and Computation - 76,2/3, Feb. 88. - -- [[[CH87]]] Th. Coquand, G. Huet. _Concepts Mathématiques et - Informatiques Formalisés dans le Calcul des Constructions_. Invited - paper, European Logic Colloquium, Orsay, July 1985. Preprint as - Rapport de recherche INRIA n°463, Dec. 85. Published in Logic - Colloquium 1985, North-Holland, 1987. - -- [[[P86]]] C. Paulin. _Algorithm development in the Calculus of - Constructions_, preprint as Rapport de recherche INRIA n°497, - March 86. Final version in Proceedings Symposium on Logic in Computer - Science, Cambridge, MA, 1986 (IEEE Computer Society Press). - -- [[[H88]]] G. Huet. _Induction Principles Formalized in the Calculus - of Constructions_ in Programming of Future Generation Computers, - Ed. K. Fuchi and M. Nivat, North-Holland, 1988. - -- [[[C90]]] Th. Coquand. _Metamathematical Investigations of a - Calculus of Constructions_, by INRIA Research Report N°1088, - Sept. 1989, published in Logic and Computer Science, - ed. P.G. Odifreddi, Academic Press, 1990. - -- [[[P89]]] C. Paulin. _Extracting F ω's programs from proofs in the - calculus of constructions_. 16th Annual ACM Symposium on Principles - of Programming Languages, Austin. 1989. - -- [[[H89]]] G. Huet. _The constructive engine_. A perspective in - Theoretical Computer Science. Commemorative Volume for Gift - Siromoney. World Scientific Publishing (1989). - -- [[[PP90]]] F. Pfenning and C. Paulin-Mohring. _Inductively defined - types in the Calculus of Constructions_. Preprint technical report - CMU-CS-89-209, final version in Proceedings of Mathematical - Foundations of Programming Semantics, volume 442, Lecture Notes in - Computer Science. Springer-Verlag, 1990 - -- [[[CP90]]] Th. Coquand and C. Paulin-Mohring. _Inductively defined - types_. In P. Martin-Löf and G. Mints, editors, Proceedings of - Colog'88, volume 417, Lecture Notes in Computer Science. - Springer-Verlag, 1990. - -- [[[P93]]] C. Paulin-Mohring. _Inductive Definitions in the System - Coq - Rules and Properties_. In M. Bezem and J.-F. Groote, editors, - Proceedings of the conference Typed Lambda Calculi and Applications, - volume 664, Lecture Notes in Computer Science, 1993. diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index da91c85856..a31ab1c511 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -44,6 +44,24 @@ Dune will read the file `~/.config/dune/config`; see `man dune-config`. Among others, you can set in this file the custom number of build threads `(jobs N)` and display options `(display _mode_)`. +## Running binaries [coqtop / coqide] + +There are two special targets `states` and `quickide` that will +generate "shims" for running `coqtop` and `coqide` in a fast build. In +order to use them, do: + +``` +$ make -f Makefile.dune voboot # Only once per session +$ dune exec dev/shim/coqtop-prelude +``` + +or `quickide` / `dev/shim/coqide-prelude` for CoqIDE. These targets +enjoy quick incremental compilation thanks to `-opaque` so they tend +to be very fast while developing. + +Note that for a fast developer build of ML files, the `check` target +will be faster. + ## Targets The default dune target is `dune build` (or `dune build @install`), diff --git a/dev/shim/dune b/dev/shim/dune new file mode 100644 index 0000000000..85a0d205da --- /dev/null +++ b/dev/shim/dune @@ -0,0 +1,27 @@ +(rule + (targets coqtop-prelude) + (deps + %{bin:coqtop} + %{project_root}/theories/Init/Prelude.vo) + (action + (with-outputs-to coqtop-prelude + (progn + (echo "#!/usr/bin/env bash\n") + (bash "echo \"$(pwd)/%{bin:coqtop} -coqlib $(pwd)/%{project_root}\" \"$@\"") + (run chmod +x %{targets}))))) + +(rule + (targets coqide-prelude) + (deps + %{bin:coqqueryworker.opt} + %{bin:coqtacticworker.opt} + %{bin:coqproofworker.opt} + %{project_root}/theories/Init/Prelude.vo + %{project_root}/coqide-server.install + %{project_root}/coqide.install) + (action + (with-outputs-to coqide-prelude + (progn + (echo "#!/usr/bin/env bash\n") + (bash "echo \"$(pwd)/%{bin:coqide} -coqlib $(pwd)/%{project_root}\" \"$@\"") + (run chmod +x %{targets}))))) diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el index ec72f96509..c6687b9731 100644 --- a/dev/tools/coqdev.el +++ b/dev/tools/coqdev.el @@ -80,9 +80,8 @@ Note that this function is executed before _Coqproject is read if it exists." (when dir (unless coq-prog-args (setq coq-prog-args - `("-coqlib" ,dir "-R" ,(concat dir "plugins") - "Coq" "-R" ,(concat dir "theories") - "Coq"))) + `("-coqlib" ,dir + "-topfile" ,buffer-file-name))) (setq-local coq-prog-name (concat dir "bin/coqtop"))))) (add-hook 'hack-local-variables-hook #'coqdev-setup-proofgeneral) diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index fac0035de1..881f7a310d 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -234,7 +234,8 @@ In addition to the objects above, the ``coqrst`` Sphinx plugin defines the follo - Behavior options - ``reset``: Send a ``Reset Initial`` command before running this block - - ``fail``: Don't die if a command fails + - ``fail``: Don't die if a command fails, implies ``warn`` (so no need to put both) + - ``warn``: Don't die if a command emits a warning - ``restart``: Send a ``Restart`` command before running this block (only works in proof mode) - ``abort``: Send an ``Abort All`` command after running this block (leaves all pending proofs if any) diff --git a/doc/sphinx/addendum/canonical-structures.rst b/doc/sphinx/addendum/canonical-structures.rst index 3e414a714c..a9d894cab5 100644 --- a/doc/sphinx/addendum/canonical-structures.rst +++ b/doc/sphinx/addendum/canonical-structures.rst @@ -313,7 +313,9 @@ constructor ``*``. It also tests that they work as expected. Unfortunately, these declarations are very verbose. In the following subsection we show how to make them more compact. -.. coqtop:: all +.. FIXME shouldn't warn + +.. coqtop:: all warn Module Add_instance_attempt. @@ -418,7 +420,9 @@ the reader can refer to :cite:`CSwcu`. The declaration of canonical instances can now be way more compact: -.. coqtop:: all +.. FIXME should not warn + +.. coqtop:: all warn Canonical Structure nat_LEQty := Eval hnf in Pack nat nat_LEQmx. diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib index d9eaa2c6c6..0467852b19 100644 --- a/doc/sphinx/biblio.bib +++ b/doc/sphinx/biblio.bib @@ -45,6 +45,58 @@ s}, year = {1972} } +@inproceedings{CH85, + title={Constructions: a higher order proof system for mechanizing mathematics}, + author={Coquand, Thierry and Huet, Gérard}, + booktitle={European Conference on Computer Algebra}, + pages={151--184}, + year={1985}, + issn = {1611-3349}, + doi = {10.1007/3-540-15983-5_13}, + url = {http://dx.doi.org/10.1007/3-540-15983-5_13}, + isbn = 9783540396840, + publisher = {Springer Berlin Heidelberg} +} + +@techreport{CH88 + TITLE = {{The calculus of constructions}}, + AUTHOR = {Coquand, T. and Huet, G{\'e}rard}, + URL = {https://hal.inria.fr/inria-00076024}, + NUMBER = {RR-0530}, + INSTITUTION = {{INRIA}}, + YEAR = {1986}, + MONTH = May, + PDF = {https://hal.inria.fr/inria-00076024/file/RR-0530.pdf}, + HAL_ID = {inria-00076024}, + HAL_VERSION = {v1}, +} + +@techreport{CH87, + TITLE = {{Concepts mathematiques et informatiques formalises dans le calcul des constructions}}, + AUTHOR = {Coquand, T. and Huet, G{\'e}rard}, + URL = {https://hal.inria.fr/inria-00076039}, + NUMBER = {RR-0515}, + INSTITUTION = {{INRIA}}, + YEAR = {1986}, + MONTH = Apr, + PDF = {https://hal.inria.fr/inria-00076039/file/RR-0515.pdf}, + HAL_ID = {inria-00076039}, + HAL_VERSION = {v1}, +} + +@techreport{C90, + TITLE = {{Metamathematical investigations of a calculus of constructions}}, + AUTHOR = {Coquand, T.}, + URL = {https://hal.inria.fr/inria-00075471}, + NUMBER = {RR-1088}, + INSTITUTION = {{INRIA}}, + YEAR = {1989}, + MONTH = Sep, + PDF = {https://hal.inria.fr/inria-00075471/file/RR-1088.pdf}, + HAL_ID = {inria-00075471}, + HAL_VERSION = {v1}, +} + @PhDThesis{Coq85, author = {Th. Coquand}, month = jan, @@ -80,6 +132,19 @@ s}, bibsource = {DBLP, http://dblp.uni-trier.de} } +@inproceedings{CP90, + title={Inductively defined types}, + author={Coquand, Thierry and Paulin, Christine}, + booktitle={COLOG-88}, + pages={50--66}, + year={1990}, + issn = {1611-3349}, + doi = {10.1007/3-540-52335-9_47}, + url = {http://dx.doi.org/10.1007/3-540-52335-9_47}, + isbn = 9783540469636, + publisher = {Springer Berlin Heidelberg} +} + @Book{Cur58, author = {Haskell B. Curry and Robert Feys and William Craig}, title = {Combinatory Logic}, @@ -216,7 +281,19 @@ s}, year = {1980} } -@InProceedings{Hue88, +@inproceedings{H88, + title={Induction principles formalized in the Calculus of Constructions}, + author={Huet, G{\'e}rard}, + booktitle={Programming of Future Generation Computers. Elsevier Science}, + year={1988}, + issn = {1611-3349}, + doi = {10.1007/3-540-17660-8_62}, + url = {http://dx.doi.org/10.1007/3-540-17660-8_62}, + isbn = 9783540477464, + publisher = {Springer Berlin Heidelberg} +} + +@InProceedings{H89, author = {G. Huet}, booktitle = {A perspective in Theoretical Computer Science. Commemorative Volume for Gift Siromoney}, editor = {R. Narasimhan}, @@ -305,6 +382,50 @@ s}, url = {http://www.xmailserver.org/diff2.pdf} } +@inproceedings{P86, + title={Algorithm development in the calculus of constructions}, + author={Mohring, Christine}, + booktitle={LICS}, + pages={84--91}, + year={1986} +} + +@inproceedings{P89, + title={Extracting $\Omega$'s programs from proofs in the calculus of constructions}, + author={Paulin-Mohring, Christine}, + booktitle={Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages}, + pages={89--104}, + year={1989}, + doi = {10.1145/75277.75285}, + url = {http://dx.doi.org/10.1145/75277.75285}, + isbn = 0897912942, + organization = {ACM Press} +} + +@inproceedings{P93, + title={Inductive definitions in the system coq rules and properties}, + author={Paulin-Mohring, Christine}, + booktitle={International Conference on Typed Lambda Calculi and Applications}, + pages={328--345}, + year={1993}, + doi = {10.1007/bfb0037116}, + url = {http://dx.doi.org/10.1007/bfb0037116}, + isbn = 3540565175, + organization = {Springer-Verlag} +} + +@inproceedings{PP90, + title={Inductively defined types in the Calculus of Constructions}, + author={Pfenning, Frank and Paulin-Mohring, Christine}, + booktitle={International Conference on Mathematical Foundations of Programming Semantics}, + pages={209--228}, + year={1989}, + doi = {10.1007/bfb0040259}, + url = {http://dx.doi.org/10.1007/bfb0040259}, + isbn = 0387973753, + organization = {Springer-Verlag} +} + @InProceedings{Parent95b, author = {C. Parent}, booktitle = {{Mathematics of Program Construction'95}}, diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits.rst index 909af6e2f2..5873096523 100644 --- a/doc/sphinx/credits.rst +++ b/doc/sphinx/credits.rst @@ -2,10 +2,13 @@ Credits ------- +Historical roots +---------------- + Coq is a proof assistant for higher-order logic, allowing the development of computer programs consistent with their formal -specification. It is the result of about ten years of research of the -Coq project. We shall briefly survey here three main aspects: the +specification. It is the result of about ten years [#years]_ of research +of the Coq project. We shall briefly survey here three main aspects: the *logical language* in which we write our axiomatizations and specifications, the *proof assistant* which allows the development of verified mathematical proofs, and the *program extractor* which @@ -21,8 +24,8 @@ prompted Russell to restrict predicate calculus with a stratification of *types*. This effort culminated with *Principia Mathematica*, the first systematic attempt at a formal foundation of mathematics. A simplification of this system along the lines of simply typed -:math:`\lambda`-calculus occurred with Church’s *Simple Theory of -Types*. The :math:`\lambda`-calculus notation, originally used for +λ-calculus occurred with Church’s *Simple Theory of +Types*. The λ-calculus notation, originally used for expressing functionality, could also be used as an encoding of natural deduction proofs. This Curry-Howard isomorphism was used by N. de Bruijn in the *Automath* project, the first full-scale attempt to develop and @@ -32,7 +35,7 @@ Exploiting this Curry-Howard isomorphism, notable achievements in proof theory saw the emergence of two type-theoretic frameworks; the first one, Martin-Löf’s *Intuitionistic Theory of Types*, attempts a new foundation of mathematics on constructive principles. The second one, -Girard’s polymorphic :math:`\lambda`-calculus :math:`F_\omega`, is a +Girard’s polymorphic λ-calculus :math:`F_\omega`, is a very strong functional system in which we may represent higher-order logic proof structures. Combining both systems in a higher-order extension of the Automath language, T. Coquand presented in 1985 the @@ -107,15 +110,27 @@ advantage of special hardware, debuggers, and the like. We hope that |Coq| can be of use to researchers interested in experimenting with this new methodology. +.. [#years] At the time of writting, i.e. 1995. + +Brief summary of the versions up to 5.10 +---------------------------------------- + +.. note:: + This summary was written in 1995 together with the previous + section and formed the initial version of the Credits chapter + (that has since then been appended to, at each new release). + A more comprehensive description of these early versions is + available in the next few sections, which were written in 2015. + A first implementation of CoC was started in 1984 by G. Huet and T. Coquand. Its implementation language was CAML, a functional programming language from the ML family designed at INRIA in Rocquencourt. The core of this system was a proof-checker for CoC seen as a typed -:math:`\lambda`-calculus, called the *Constructive Engine*. This engine +λ-calculus, called the *Constructive Engine*. This engine was operated through a high-level notation permitting the declaration of axioms and parameters, the definition of mathematical types and objects, and the explicit construction of proof objects encoded as -:math:`\lambda`-terms. A section mechanism, designed and implemented by +λ-terms. A section mechanism, designed and implemented by G. Dowek, allowed hierarchical developments of mathematical theories. This high-level language was called the *Mathematical Vernacular*. Furthermore, an interactive *Theorem Prover* permitted the incremental @@ -189,8 +204,324 @@ definitions of “inversion predicates”. | Gérard Huet | -Credits: addendum for version 6.1 ---------------------------------- +Version 1 +--------- + +.. note:: + + These additional notes come from a document written + in September 2015 by Gérard Huet, Thierry Coquand and Christine Paulin + to accompany their public release of the archive of versions 1.10 to 6.2 + of Coq and of its CONSTR ancestor. CONSTR, then Coq, was designed and + implemented in the Formel team, joint between the INRIA Rocquencourt + laboratory and the Ecole Normale Supérieure of Paris, from 1984 + onwards. + +This software is a prototype type-checker for a higher-order logical +formalism known as the Theory of Constructions, presented in his PhD +thesis by Thierry Coquand, with influences from Girard's system F and +de Bruijn's Automath. The metamathematical analysis of the system is +the PhD work of Thierry Coquand. The software is mostly the work of +Gérard Huet. Most of the mathematical examples verified with the +software are due to Thierry Coquand. + +The programming language of the CONSTR software (as it was called at +the time) was a version of ML adapted from the Edinburgh LCF system +and running on a LISP backend. The main improvements from the original +LCF ML were that ML was compiled rather than interpreted (Gérard Huet +building on the original translator by Lockwood Morris), and that it +was enriched by recursively defined types (work of Guy +Cousineau). This ancestor of CAML was used and improved by Larry +Paulson for his implementation of Cambridge LCF. + +Software developments of this prototype occurred from late 1983 to +early 1985. + +Version 1.10 was frozen on December 22nd 1984. It is the version used +for the examples in Thierry Coquand's thesis, defended on January 31st +1985. There was a unique binding operator, used both for universal +quantification (dependent product) at the level of types and +functional abstraction (λ) at the level of terms/proofs, in the manner +of Automath. Substitution (λ-reduction) was implemented using de +Bruijn's indexes. + +Version 1.11 was frozen on February 19th, 1985. It is the version used +for the examples in the paper: T. Coquand, G. Huet. *Constructions: A +Higher Order Proof System for Mechanizing Mathematics* :cite:`CH85`. + +Christine Paulin joined the team at this point, for her DEA research +internship. In her DEA memoir (August 1985) she presents developments +for the *lambo* function – :math:`\text{lambo}(f)(n)` computes the minimal +:math:`m` such that :math:`f(m)` is greater than :math:`n`, for :math:`f` +an increasing integer function, a challenge for constructive mathematics. +She also encoded the majority voting algorithm of Boyer and Moore. + +Version 2 +--------- + +The formal system, now renamed as the *Calculus of Constructions*, was +presented with a proof of consistency and comparisons with proof +systems of Per Martin Löf, Girard, and the Automath family of N. de +Bruijn, in the paper: T. Coquand and G. Huet. *The Calculus of +Constructions* :cite:`CH88`. + +An abstraction of the software design, in the form of an abstract +machine for proof checking, and a fuller sequence of mathematical +developments was presented in: T. Coquand, G. Huet. *Concepts +Mathématiques et Informatiques Formalisés dans le Calcul des +Constructions* :cite:`CH87`. + +Version 2.8 was frozen on December 16th, 1985, and served for +developing the examples in the above papers. + +This calculus was then enriched in version 2.9 with a cumulative +hierarchy of universes. Universe levels were initially explicit +natural numbers. Another improvement was the possibility of automatic +synthesis of implicit type arguments, relieving the user of tedious +redundant declarations. + +Christine Paulin wrote an article *Algorithm development in the +Calculus of Constructions* :cite:`P86`. Besides *lambo* and *majority*, +she presents *quicksort* and a text formatting algorithm. + +Version 2.13 of the Calculus of Constructions with universes was +frozen on June 25th, 1986. + +A synthetic presentation of type theory along constructive lines with +ML algorithms was given by Gérard Huet in his May 1986 CMU course +notes *Formal Structures for Computation and Deduction*. Its chapter +*Induction and Recursion in the Theory of Constructions* was presented +as an invited paper at the Joint Conference on Theory and Practice of +Software Development TAPSOFT’87 at Pise in March 1987, and published +as *Induction Principles Formalized in the Calculus of +Constructions* :cite:`H88`. + +Version 3 +--------- + +This version saw the beginning of proof automation, with a search +algorithm inspired from PROLOG and the applicative logic programming +programs of the course notes *Formal structures for computation and +deduction*. The search algorithm was implemented in ML by Thierry +Coquand. The proof system could thus be used in two modes: proof +verification and proof synthesis, with tactics such as ``AUTO``. + +The implementation language was now called CAML, for Categorical +Abstract Machine Language. It used as backend the LLM3 virtual machine +of Le Lisp by Jérôme Chailloux. The main developers of CAML were +Michel Mauny, Ascander Suarez and Pierre Weis. + +V3.1 was started in the summer of 1986, V3.2 was frozen at the end of +November 1986. V3.4 was developed in the first half of 1987. + +Thierry Coquand held a post-doctoral position in Cambrige University +in 1986-87, where he developed a variant implementation in SML, with +which he wrote some developments on fixpoints in Scott's domains. + +Version 4 +--------- + +This version saw the beginning of program extraction from proofs, with +two varieties of the type ``Prop`` of propositions, indicating +constructive intent. The proof extraction algorithms were implemented +by Christine Paulin-Mohring. + +V4.1 was frozen on July 24th, 1987. It had a first identified library +of mathematical developments (directory ``exemples``), with libraries +``Logic`` (containing impredicative encodings of intuitionistic logic and +algebraic primitives for booleans, natural numbers and list), ``Peano`` +developing second-order Peano arithmetic, ``Arith`` defining addition, +multiplication, euclidean division and factorial. Typical developments +were the Knaster-Tarski theorem and Newman's lemma from rewriting +theory. + +V4.2 was a joint development of a team consisting of Thierry Coquand, +Gérard Huet and Christine Paulin-Mohring. A file V4.2.log records the +log of changes. It was frozen on September 1987 as the last version +implemented in CAML 2.3, and V4.3 followed on CAML 2.5, a more stable +development system. + +V4.3 saw the first top-level of the system. Instead of evaluating +explicit quotations, the user could develop his mathematics in a +high-level language called the mathematical vernacular (following +Automath terminology). The user could develop files in the vernacular +notation (with ``.v`` extension) which were now separate from the ``ml`` +sources of the implementation. Gilles Dowek joined the team to +develop the vernacular language as his DEA internship research. + +A notion of sticky constant was introduced, in order to keep names of +lemmas when local hypotheses of proofs were discharged. This gave a +notion of global mathematical environment with local sections. + +Another significant practical change was that the system, originally +developped on the VAX central computer of our lab, was transferred on +SUN personal workstations, allowing a level of distributed +development. The extraction algorithm was modified, with three +annotations ``Pos``, ``Null`` and ``Typ`` decorating the sorts ``Prop`` +and ``Type``. + +Version 4.3 was frozen at the end of November 1987, and was +distributed to an early community of users (among those were Hugo +Herbelin and Loic Colson). + +V4.4 saw the first version of (encoded) inductive types. Now natural +numbers could be defined as:: + + [source, coq] + Inductive NAT : Prop = O : NAT | Succ : NAT->NAT. + +These inductive types were encoded impredicatively in the calculus, +using a subsystem *rec* due to Christine Paulin. V4.4 was frozen on +March 6th 1988. + +Version 4.5 was the first one to support inductive types and program +extraction. Its banner was *Calcul des Constructions avec +Réalisations et Synthèse*. The vernacular language was enriched to +accommodate extraction commands. + +The verification engine design was presented as: G. Huet. *The +Constructive Engine*. Version 4.5. Invited Conference, 2nd European +Symposium on Programming, Nancy, March 88. The final paper, +describing the V4.9 implementation, appeared in: A perspective in +Theoretical Computer Science, Commemorative Volume in memory of Gift +Siromoney, Ed. R. Narasimhan, World Scientific Publishing, 1989. + +Version 4.5 was demonstrated in June 1988 at the YoP Institute on +Logical Foundations of Functional Programming organized by Gérard Huet +at Austin, Texas. + +Version 4.6 was started during the summer of 1988. Its main +improvement was the complete rehaul of the proof synthesis engine by +Thierry Coquand, with a tree structure of goals. + +Its source code was communicated to Randy Pollack on September 2nd +1988. It evolved progressively into LEGO, proof system for Luo's +formalism of Extended Calculus of Constructions. + +The discharge tactic was modified by Gérard Huet to allow for +inter-dependencies in discharged lemmas. Christine Paulin improved the +inductive definition scheme in order to accommodate predicates of any +arity. + +Version 4.7 was started on September 6th, 1988. + +This version starts exploiting the CAML notion of module in order to +improve the modularity of the implementation. Now the term verifier is +identified as a proper module Machine, which the structure of its +internal data structures being hidden and thus accessible only through +the legitimate operations. This machine (the constructive engine) was +the trusted core of the implementation. The proof synthesis mechanism +was a separate proof term generator. Once a complete proof term was +synthesized with the help of tactics, it was entirely re-checked by +the engine. Thus there was no need to certify the tactics, and the +system took advantage of this fact by having tactics ignore the +universe levels, universe consistency check being relegated to the +final type-checking pass. This induced a certain puzzlement in early +users who saw, after a successful proof search, their ``QED`` followed +by silence, followed by a failure message due to a universe +inconsistency… + +The set of examples comprise set theory experiments by Hugo Herbelin, +and notably the Schroeder-Bernstein theorem. + +Version 4.8, started on October 8th, 1988, saw a major +re-implementation of the abstract syntax type ``constr``, separating +variables of the formalism and metavariables denoting incomplete terms +managed by the search mechanism. A notion of level (with three values +``TYPE``, ``OBJECT`` and ``PROOF``) is made explicit and a type judgement +clarifies the constructions, whose implementation is now fully +explicit. Structural equality is speeded up by using pointer equality, +yielding spectacular improvements. Thierry Coquand adapts the proof +synthesis to the new representation, and simplifies pattern matching +to first-order predicate calculus matching, with important performance +gain. + +A new representation of the universe hierarchy is then defined by +Gérard Huet. Universe levels are now implemented implicitly, through +a hidden graph of abstract levels constrained with an order relation. +Checking acyclicity of the graph insures well-foundedness of the +ordering, and thus consistency. This was documented in a memo *Adding +Type:Type to the Calculus of Constructions* which was never published. + +The development version is released as a stable 4.8 at the end of +1988. + +Version 4.9 is released on March 1st 1989, with the new "elastic" +universe hierarchy. + +The spring of 1989 saw the first attempt at documenting the system +usage, with a number of papers describing the formalism: + +- *Metamathematical Investigations of a Calculus of Constructions*, by + Thierry Coquand :cite:`C90`, + +- *Inductive definitions in the Calculus of Constructions*, by + Christine Paulin-Mohrin, + +- *Extracting Fω's programs from proofs in the Calculus of + Constructions*, by Christine Paulin-Mohring* :cite:`P89`, + +- *The Constructive Engine*, by Gérard Huet :cite:`H89`, + +as well as a number of user guides: + +- *A short user's guide for the Constructions*, Version 4.10, by Gérard Huet +- *A Vernacular Syllabus*, by Gilles Dowek. +- *The Tactics Theorem Prover, User's guide*, Version 4.10, by Thierry + Coquand. + +Stable V4.10, released on May 1st, 1989, was then a mature system, +distributed with CAML V2.6. + +In the mean time, Thierry Coquand and Christine Paulin-Mohring had +been investigating how to add native inductive types to the Calculus +of Constructions, in the manner of Per Martin-Löf's Intuitionistic +Type Theory. The impredicative encoding had already been presented in: +F. Pfenning and C. Paulin-Mohring. *Inductively defined types in the +Calculus of Constructions* :cite:`PP90`. An extension of the calculus +with primitive inductive types appeared in: T. Coquand and +C. Paulin-Mohring. *Inductively defined types* :cite:`CP90`. + +This led to the Calculus of Inductive Constructions, logical formalism +implemented in Versions 5 upward of the system, and documented in: +C. Paulin-Mohring. *Inductive Definitions in the System Coq - Rules +and Properties* :cite:`P93`. + +The last version of CONSTR is Version 4.11, which was last distributed +in the spring of 1990. It was demonstrated at the first workshop of +the European Basic Research Action Logical Frameworks In Sophia +Antipolis in May 1990. + +Version 5 +--------- + +At the end of 1989, Version 5.1 was started, and renamed as the system +Coq for the Calculus of Inductive Constructions. It was then ported to +the new stand-alone implementation of ML called Caml-light. + +In 1990 many changes occurred. Thierry Coquand left for Chalmers +University in Göteborg. Christine Paulin-Mohring took a CNRS +researcher position at the LIP laboratory of École Normale Supérieure +de Lyon. Project Formel was terminated, and gave rise to two teams: +Cristal at INRIA-Roquencourt, that continued developments in +functional programming with Caml-light then OCaml, and Coq, continuing +the type theory research, with a joint team headed by Gérard Huet at +INRIA-Rocquencourt and Christine Paulin-Mohring at the LIP laboratory +of CNRS-ENS Lyon. + +Chetan Murthy joined the team in 1991 and became the main software +architect of Version 5. He completely rehauled the implementation for +efficiency. Versions 5.6 and 5.8 were major distributed versions, +with complete documentation and a library of users' developements. The +use of the RCS revision control system, and systematic ChangeLog +files, allow a more precise tracking of the software developments. + +| September 2015 + +| Thierry Coquand, Gérard Huet and Christine Paulin-Mohring. +| + +Version 6.1 +----------- The present version 6.1 of |Coq| is based on the V5.10 architecture. It was ported to the new language Objective Caml by Bruno Barras. The @@ -226,8 +557,8 @@ Barras. | Christine Paulin | -Credits: addendum for version 6.2 ---------------------------------- +Version 6.2 +----------- In version 6.2 of |Coq|, the parsing is done using camlp4, a preprocessor and pretty-printer for CAML designed by Daniel de Rauglaudre at INRIA. @@ -271,8 +602,8 @@ Loiseleur. | Christine Paulin | -Credits: addendum for version 6.3 ---------------------------------- +Version 6.3 +----------- The main changes in version V6.3 were the introduction of a few new tactics and the extension of the guard condition for fixpoint @@ -304,8 +635,8 @@ Monin from CNET Lannion. | Christine Paulin | -Credits: versions 7 -------------------- +Versions 7 +---------- The version V7 is a new implementation started in September 1999 by Jean-Christophe Filliâtre. This is a major revision with respect to the @@ -393,8 +724,8 @@ J.-F. Monin from France Telecom R & D. | Hugo Herbelin & Christine Paulin | -Credits: version 8.0 --------------------- +Version 8.0 +----------- Coq version 8 is a major revision of the |Coq| proof assistant. First, the underlying logic is slightly different. The so-called *impredicativity* @@ -495,8 +826,8 @@ under the responsibility of Christine Paulin. | (updated Apr. 2006) | -Credits: version 8.1 --------------------- +Version 8.1 +----------- Coq version 8.1 adds various new functionalities. @@ -574,8 +905,8 @@ and Yale University. | Hugo Herbelin | -Credits: version 8.2 --------------------- +Version 8.2 +----------- Coq version 8.2 adds new features, new libraries and improves on many various aspects. @@ -668,8 +999,8 @@ the Coq-Club mailing list. | Hugo Herbelin | -Credits: version 8.3 --------------------- +Version 8.3 +----------- Coq version 8.3 is before all a transition version with refinements or extensions of the existing features and libraries and a new tactic nsatz @@ -742,8 +1073,8 @@ Pierce for the excellent teaching materials they provided. | Hugo Herbelin | -Credits: version 8.4 --------------------- +Version 8.4 +----------- Coq version 8.4 contains the result of three long-term projects: a new modular library of arithmetic by Pierre Letouzey, a new proof engine by @@ -898,8 +1229,8 @@ Eelis van der Weegen. | Hugo Herbelin | -Credits: version 8.5 --------------------- +Version 8.5 +----------- Coq version 8.5 contains the result of five specific long-term projects: @@ -916,7 +1247,7 @@ Coq version 8.5 contains the result of five specific long-term projects: Matthieu Sozeau. - An implementation of primitive projections with - :math:`\eta`-conversion bringing significant performance improvements + :math:`\eta`\-conversion bringing significant performance improvements when using records by Matthieu Sozeau. The full integration of the proof engine, by Arnaud Spiwack and @@ -967,10 +1298,10 @@ messages in case of inconsistencies and allowing higher-level algorithms like unification to be entirely type safe. The internal representation of universes has been modified but this is invisible to the user. -The underlying logic has been extended with :math:`\eta`-conversion for +The underlying logic has been extended with :math:`\eta`\-conversion for records defined with primitive projections by Matthieu Sozeau. This -additional form of :math:`\eta`-conversion is justified using the same -principle than the previously added :math:`\eta`-conversion for function +additional form of :math:`\eta`\-conversion is justified using the same +principle than the previously added :math:`\eta`\-conversion for function types, based on formulations of the Calculus of Inductive Constructions with typed equality. Primitive projections, which do not carry the parameters of the record and are rigid names (not defined as a @@ -1052,8 +1383,8 @@ Tankink. Maxime Dénès coordinated the release process. | Hugo Herbelin, Matthieu Sozeau and the |Coq| development team | -Credits: version 8.6 --------------------- +Version 8.6 +----------- Coq version 8.6 contains the result of refinements, stabilization of 8.5’s features and cleanups of the internals of the system. Over the @@ -1192,8 +1523,8 @@ Dénès to put together a |Coq| consortium. | Matthieu Sozeau and the |Coq| development team | -Credits: version 8.7 --------------------- +Version 8.7 +----------- |Coq| version 8.7 contains the result of refinements, stabilization of features and cleanups of the internals of the system along with a few new features. The @@ -1298,8 +1629,8 @@ system, is now upcoming and will rely on Inria’s newly created Foundation. | Matthieu Sozeau and the |Coq| development team | -Credits: version 8.8 --------------------- +Version 8.8 +----------- |Coq| version 8.8 contains the result of refinements and stabilization of features and deprecations, cleanups of the internals of the system along @@ -1405,8 +1736,8 @@ The contacts of the Coq Consortium are Yves Bertot and Maxime Dénès. | Matthieu Sozeau for the |Coq| development team | -Credits: version 8.9 --------------------- +Version 8.9 +----------- |Coq| version 8.9 contains the result of refinements and stabilization of features and deprecations or removals of deprecated features, diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index c1eab8a970..d1b95e6203 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -606,7 +606,10 @@ Finally, it gives the definition of the usual orderings ``le``, single: ge (term) single: gt (term) -.. coqtop:: in +.. This emits a notation already used warning but it won't be shown to + the user. + +.. coqtop:: in warn Inductive le (n:nat) : nat -> Prop := | le_n : le n n diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 9ab3f905e6..9bd41d79b7 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -1023,7 +1023,7 @@ Mutually defined inductive types .. coqtop:: in - Variables A B : Set. + Parameters A B : Set. Inductive tree : Set := node : A -> forest -> tree @@ -1533,7 +1533,7 @@ the following attributes names are recognized: .. example:: - .. coqtop:: all reset + .. coqtop:: all reset warn From Coq Require Program. #[program] Definition one : nat := S _. diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst index 63d6a229ed..b629d15b11 100644 --- a/doc/sphinx/proof-engine/detailed-tactic-examples.rst +++ b/doc/sphinx/proof-engine/detailed-tactic-examples.rst @@ -33,7 +33,7 @@ example, revisiting the first example of the inversion documentation: | LeO : forall n:nat, Le 0 n | LeS : forall n m:nat, Le n m -> Le (S n) (S m). - Variable P : nat -> nat -> Prop. + Parameter P : nat -> nat -> Prop. Goal forall n m:nat, Le (S n) m -> P n m. @@ -69,7 +69,7 @@ as well in this case, e.g.: .. coqtop:: in - Variable Q : forall (n m : nat), Le n m -> Prop. + Parameter Q : forall (n m : nat), Le n m -> Prop. Goal forall n m (p : Le (S n) m), Q (S n) m p. .. coqtop:: all @@ -124,7 +124,7 @@ the following example on vectors: .. coqtop:: in - Variable A : Set. + Parameter A : Set. .. coqtop:: in @@ -329,7 +329,7 @@ the optional tactic of the ``Hint Rewrite`` command. .. coqtop:: in - Variable Ack : nat -> nat -> nat. + Parameter Ack : nat -> nat -> nat. .. coqtop:: in @@ -357,7 +357,7 @@ the optional tactic of the ``Hint Rewrite`` command. .. coqtop:: in - Variable g : nat -> nat -> nat. + Parameter g : nat -> nat -> nat. .. coqtop:: in diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 3e87e8acd8..52e3029b8f 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -200,7 +200,7 @@ following form: :name: [> ... | ... | ... ] (dispatch) The expressions :n:`@expr__i` are evaluated to :n:`v__i`, for - i = 0, ..., n and all have to be tactics. The :n:`v__i` is applied to the + i = 1, ..., n and all have to be tactics. The :n:`v__i` is applied to the i-th goal, for i = 1, ..., n. It fails if the number of focused goals is not exactly n. diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 2300a317f1..27360f02d3 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -30,7 +30,7 @@ When a proof is completed, the message ``Proof completed`` is displayed. One can then register this proof as a defined constant in the environment. Because there exists a correspondence between proofs and terms of λ-calculus, known as the *Curry-Howard isomorphism* -:cite:`How80,Bar81,Gir89,Hue88`, |Coq| stores proofs as terms of |Cic|. Those +:cite:`How80,Bar81,Gir89,H89`, |Coq| stores proofs as terms of |Cic|. Those terms are called *proof terms*. diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index b81830f06b..b240cef40c 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -2902,6 +2902,7 @@ pattern will be used to process its instance. Axiom P : nat -> Prop. Axioms eqn leqn : nat -> nat -> bool. + Declare Scope this_scope. Notation "a != b" := (eqn a b) (at level 70) : this_scope. Notation "a <= b" := (leqn a b) (at level 70) : this_scope. Open Scope this_scope. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index b5e9a902c6..7b395900e9 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -378,7 +378,7 @@ Examples: .. coqtop:: reset none - Variables (A : Prop) (B: nat -> Prop) (C: Prop). + Parameters (A : Prop) (B: nat -> Prop) (C: Prop). .. coqtop:: out @@ -730,15 +730,15 @@ Applying theorems .. coqtop:: reset in - Variable R : nat -> nat -> Prop. + Parameter R : nat -> nat -> Prop. - Hypothesis Rtrans : forall x y z:nat, R x y -> R y z -> R x z. + Axiom Rtrans : forall x y z:nat, R x y -> R y z -> R x z. - Variables n m p : nat. + Parameters n m p : nat. - Hypothesis Rnm : R n m. + Axiom Rnm : R n m. - Hypothesis Rmp : R m p. + Axiom Rmp : R m p. Consider the goal ``(R n p)`` provable using the transitivity of ``R``: @@ -3683,11 +3683,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is Local is useless since hints do not survive anyway to the closure of sections. - .. cmdv:: Local Hint @hint_definition - - Idem for the core database. - - .. cmdv:: Hint Resolve @term {? | {? @num} {? @pattern}} + .. cmdv:: Hint Resolve @term {? | {? @num} {? @pattern}} : @ident :name: Hint Resolve This command adds :n:`simple apply @term` to the hint list with the head @@ -3706,16 +3702,16 @@ The general command to add a hint to some databases :n:`{+ @ident}` is typical example of a hint that is used only by :tacn:`eauto` is a transitivity lemma. - .. exn:: @term cannot be used as a hint + .. exn:: @term cannot be used as a hint - The head symbol of the type of :n:`@term` is a bound variable such that - this tactic cannot be associated to a constant. + The head symbol of the type of :n:`@term` is a bound variable + such that this tactic cannot be associated to a constant. - .. cmdv:: Hint Resolve {+ @term} + .. cmdv:: Hint Resolve {+ @term} : @ident Adds each :n:`Hint Resolve @term`. - .. cmdv:: Hint Resolve -> @term + .. cmdv:: Hint Resolve -> @term : @ident Adds the left-to-right implication of an equivalence as a hint (informally the hint will be used as :n:`apply <- @term`, although as mentionned @@ -3726,7 +3722,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is Adds the right-to-left implication of an equivalence as a hint. - .. cmdv:: Hint Immediate @term + .. cmdv:: Hint Immediate @term : @ident :name: Hint Immediate This command adds :n:`simple apply @term; trivial` to the hint list associated @@ -3742,37 +3738,37 @@ The general command to add a hint to some databases :n:`{+ @ident}` is .. exn:: @term cannot be used as a hint :undocumented: - .. cmdv:: Immediate {+ @term} + .. cmdv:: Immediate {+ @term} : @ident Adds each :n:`Hint Immediate @term`. - .. cmdv:: Hint Constructors @ident + .. cmdv:: Hint Constructors @qualid : @ident :name: Hint Constructors - If :n:`@ident` is an inductive type, this command adds all its constructors as + If :token:`qualid` is an inductive type, this command adds all its constructors as hints of type ``Resolve``. Then, when the conclusion of current goal has the form - :n:`(@ident ...)`, :tacn:`auto` will try to apply each constructor. + :n:`(@qualid ...)`, :tacn:`auto` will try to apply each constructor. - .. exn:: @ident is not an inductive type - :undocumented: + .. exn:: @qualid is not an inductive type + :undocumented: - .. cmdv:: Hint Constructors {+ @ident} + .. cmdv:: Hint Constructors {+ @qualid} : @ident - Adds each :n:`Hint Constructors @ident`. + Extends the previous command for several inductive types. - .. cmdv:: Hint Unfold @qualid + .. cmdv:: Hint Unfold @qualid : @ident :name: Hint Unfold This adds the tactic :n:`unfold @qualid` to the hint list that will only be - used when the head constant of the goal is :n:`@ident`. + used when the head constant of the goal is :token:`qualid`. Its cost is 4. - .. cmdv:: Hint Unfold {+ @ident} + .. cmdv:: Hint Unfold {+ @qualid} - Adds each :n:`Hint Unfold @ident`. + Extends the previous command for several defined constants. - .. cmdv:: Hint Transparent {+ @qualid} - Hint Opaque {+ @qualid} + .. cmdv:: Hint Transparent {+ @qualid} : @ident + Hint Opaque {+ @qualid} : @ident :name: Hint Transparent; Hint Opaque This adds transparency hints to the database, making :n:`@qualid` @@ -3781,8 +3777,8 @@ The general command to add a hint to some databases :n:`{+ @ident}` is discrimination network to relax or constrain it in the case of discriminated databases. - .. cmdv:: Hint Variables %( Transparent %| Opaque %) - Hint Constants %( Transparent %| Opaque %) + .. cmdv:: Hint Variables %( Transparent %| Opaque %) : @ident + Hint Constants %( Transparent %| Opaque %) : @ident :name: Hint Variables; Hint Constants This sets the transparency flag used during unification of @@ -3790,7 +3786,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is overwritting the existing settings of opacity. It is advised to use this just after a :cmd:`Create HintDb` command. - .. cmdv:: Hint Extern @num {? @pattern} => @tactic + .. cmdv:: Hint Extern @num {? @pattern} => @tactic : @ident :name: Hint Extern This hint type is to extend :tacn:`auto` with tactics other than :tacn:`apply` and @@ -3801,7 +3797,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is .. coqtop:: in - Hint Extern 4 (~(_ = _)) => discriminate. + Hint Extern 4 (~(_ = _)) => discriminate : core. Now, when the head of the goal is a disequality, ``auto`` will try discriminate if it does not manage to solve the goal with hints with a @@ -3820,7 +3816,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is Goal forall a b:list (nat * nat), {a = b} + {a <> b}. Info 1 auto with eqdec. - .. cmdv:: Hint Cut @regexp + .. cmdv:: Hint Cut @regexp : @ident :name: Hint Cut .. warning:: @@ -3854,7 +3850,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is semantics of ``Hint Cut e`` is to set the cut expression to ``c | e``, the initial cut expression being `emp`. - .. cmdv:: Hint Mode @qualid {* (+ | ! | -)} + .. cmdv:: Hint Mode @qualid {* (+ | ! | -)} : @ident :name: Hint Mode This sets an optional mode of use of the identifier :n:`@qualid`. When diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 4f46a80dcf..e5eb7eb4f5 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1115,6 +1115,8 @@ Binding arguments of a constant to an interpretation scope .. coqtop:: all Parameter g : bool -> bool. + Declare Scope mybool_scope. + Notation "@@" := true (only parsing) : bool_scope. Notation "@@" := false (only parsing): mybool_scope. @@ -1151,6 +1153,7 @@ Binding types of arguments to an interpretation scope .. coqtop:: in reset Parameter U : Set. + Declare Scope U_scope. Bind Scope U_scope with U. Parameter Uplus : U -> U -> U. Parameter P : forall T:Set, T -> U -> Prop. @@ -1575,7 +1578,7 @@ Numeral notations For example - .. coqtop:: all + .. coqtop:: all warn Check 90000. diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 8df0f2be97..eaf1b2c2ad 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -580,7 +580,8 @@ class CoqtopDirective(Directive): - Behavior options - ``reset``: Send a ``Reset Initial`` command before running this block - - ``fail``: Don't die if a command fails + - ``fail``: Don't die if a command fails, implies ``warn`` (so no need to put both) + - ``warn``: Don't die if a command emits a warning - ``restart``: Send a ``Restart`` command before running this block (only works in proof mode) - ``abort``: Send an ``Abort All`` command after running this block (leaves all pending proofs if any) @@ -835,11 +836,12 @@ class CoqtopBlocksTransform(Transform): # Behavior options opt_reset = 'reset' in options opt_fail = 'fail' in options + opt_warn = 'warn' in options opt_restart = 'restart' in options opt_abort = 'abort' in options - options = options - set(('reset', 'fail', 'restart', 'abort')) + options = options - {'reset', 'fail', 'warn', 'restart', 'abort'} - unexpected_options = list(options - set(('all', 'none', 'in', 'out'))) + unexpected_options = list(options - {'all', 'none', 'in', 'out'}) if unexpected_options: loc = get_node_location(node) raise ExtensionError("{}: Unexpected options for .. coqtop:: {}".format(loc,unexpected_options)) @@ -857,6 +859,9 @@ class CoqtopBlocksTransform(Transform): return { 'reset': opt_reset, 'fail': opt_fail, + # if errors are allowed, then warnings too + # and they should be displayed as warnings, not errors + 'warn': opt_warn or opt_fail, 'restart': opt_restart, 'abort': opt_abort, 'input': opt_input or opt_all, @@ -891,18 +896,22 @@ class CoqtopBlocksTransform(Transform): pairs = [] if options['restart']: - repl.sendone("Restart.") + repl.sendone('Restart.') if options['reset']: - repl.sendone("Reset Initial.") - repl.sendone("Set Coqtop Exit On Error.") + repl.sendone('Reset Initial.') + repl.send_initial_options() if options['fail']: - repl.sendone("Unset Coqtop Exit On Error.") + repl.sendone('Unset Coqtop Exit On Error.') + if options['warn']: + repl.sendone('Set Warnings "default".') for sentence in self.split_sentences(node.rawsource): pairs.append((sentence, repl.sendone(sentence))) if options['abort']: - repl.sendone("Abort All.") + repl.sendone('Abort All.') if options['fail']: - repl.sendone("Set Coqtop Exit On Error.") + repl.sendone('Set Coqtop Exit On Error.') + if options['warn']: + repl.sendone('Set Warnings "+default".') dli = nodes.definition_list_item() for sentence, output in pairs: @@ -923,7 +932,7 @@ class CoqtopBlocksTransform(Transform): Finds nodes to process using is_coqtop_block.""" with CoqTop(color=True) as repl: - repl.sendone("Set Coqtop Exit On Error.") + repl.send_initial_options() for node in self.document.traverse(CoqtopBlocksTransform.is_coqtop_block): try: self.add_coq_output_1(repl, node) diff --git a/doc/tools/coqrst/repl/coqtop.py b/doc/tools/coqrst/repl/coqtop.py index ddba2edd4a..26f6255069 100644 --- a/doc/tools/coqrst/repl/coqtop.py +++ b/doc/tools/coqrst/repl/coqtop.py @@ -87,6 +87,11 @@ class CoqTop: raise CoqTopError(err, sentence, self.coqtop.before) return output + def send_initial_options(self): + """Options to send when starting the toplevel and after a Reset Initial.""" + self.sendone('Set Coqtop Exit On Error.') + self.sendone('Set Warnings "+default".') + def sendmany(*sentences): """A small demo: send each sentence in sentences and print the output""" with CoqTop() as coqtop: diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 24894fc9f5..7f1dc70d95 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1188,7 +1188,6 @@ let check_constructor_length env loc cstr len_pl pl0 = (error_wrong_numarg_constructor ?loc env cstr (Inductiveops.constructor_nrealargs cstr))) -open Term open Declarations (* Similar to Cases.adjust_local_defs but on RCPat *) @@ -1197,16 +1196,15 @@ let insert_local_defs_in_pattern (ind,j) l = if mip.mind_consnrealdecls.(j-1) = mip.mind_consnrealargs.(j-1) then (* Optimisation *) l else - let typi = mip.mind_nf_lc.(j-1) in - let (_,typi) = decompose_prod_n_assum (Context.Rel.length mib.mind_params_ctxt) typi in - let (decls,_) = decompose_prod_assum typi in + let (ctx, _) = mip.mind_nf_lc.(j-1) in + let decls = List.skipn (Context.Rel.length mib.mind_params_ctxt) (List.rev ctx) in let rec aux decls args = match decls, args with | Context.Rel.Declaration.LocalDef _ :: decls, args -> (DAst.make @@ RCPatAtom None) :: aux decls args | _, [] -> [] (* In particular, if there were trailing local defs, they have been inserted *) | Context.Rel.Declaration.LocalAssum _ :: decls, a :: args -> a :: aux decls args | _ -> assert false in - aux (List.rev decls) l + aux decls l let add_local_defs_and_check_length loc env g pl args = match g with | ConstructRef cstr -> diff --git a/interp/impargs.ml b/interp/impargs.ml index 6fd52d98dd..2c281af2d2 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -452,9 +452,10 @@ let compute_mib_implicits flags kn = let ind = (kn,i) in let ar, _ = Typeops.type_of_global_in_context env (IndRef ind) in ((IndRef ind,compute_semi_auto_implicits env sigma flags (of_constr ar)), - Array.mapi (fun j c -> + Array.mapi (fun j (ctx, cty) -> + let c = of_constr (Term.it_mkProd_or_LetIn cty ctx) in (ConstructRef (ind,j+1),compute_semi_auto_implicits env_ar sigma flags c)) - (Array.map of_constr mip.mind_nf_lc)) + mip.mind_nf_lc) in Array.mapi imps_one_inductive mib.mind_packets diff --git a/kernel/byterun/coq_instruct.h b/kernel/byterun/coq_instruct.h deleted file mode 100644 index c7abedaed6..0000000000 --- a/kernel/byterun/coq_instruct.h +++ /dev/null @@ -1,67 +0,0 @@ -/***********************************************************************/ -/* */ -/* Coq Compiler */ -/* */ -/* Benjamin Gregoire, projets Logical and Cristal */ -/* INRIA Rocquencourt */ -/* */ -/* */ -/***********************************************************************/ - -#ifndef _COQ_INSTRUCT_ -#define _COQ_INSTRUCT_ - -/* Nota: this list of instructions is parsed to produce derived files */ -/* coq_jumptbl.h and copcodes.ml. Instructions should be uppercase */ -/* and alone on lines starting by two spaces. */ -/* If adding an instruction, DON'T FORGET TO UPDATE coq_fix_code.c */ -/* with the arity of the instruction and maybe coq_tcode_of_code. */ - -enum instructions { - ACC0, ACC1, ACC2, ACC3, ACC4, ACC5, ACC6, ACC7, ACC, - PUSH, - PUSHACC0, PUSHACC1, PUSHACC2, PUSHACC3, PUSHACC4, - PUSHACC5, PUSHACC6, PUSHACC7, PUSHACC, - POP, - ENVACC1, ENVACC2, ENVACC3, ENVACC4, ENVACC, - PUSHENVACC1, PUSHENVACC2, PUSHENVACC3, PUSHENVACC4, PUSHENVACC, - PUSH_RETADDR, - APPLY, APPLY1, APPLY2, APPLY3, APPLY4, - APPTERM, APPTERM1, APPTERM2, APPTERM3, - RETURN, RESTART, GRAB, GRABREC, - CLOSURE, CLOSUREREC, CLOSURECOFIX, - OFFSETCLOSUREM2, OFFSETCLOSURE0, OFFSETCLOSURE2, OFFSETCLOSURE, - PUSHOFFSETCLOSUREM2, PUSHOFFSETCLOSURE0, PUSHOFFSETCLOSURE2, - PUSHOFFSETCLOSURE, - GETGLOBAL, PUSHGETGLOBAL, - MAKEBLOCK, MAKEBLOCK1, MAKEBLOCK2, MAKEBLOCK3, MAKEBLOCK4, - SWITCH, PUSHFIELDS, - GETFIELD0, GETFIELD1, GETFIELD, - SETFIELD0, SETFIELD1, SETFIELD, - PROJ, - ENSURESTACKCAPACITY, - CONST0, CONST1, CONST2, CONST3, CONSTINT, - PUSHCONST0, PUSHCONST1, PUSHCONST2, PUSHCONST3, PUSHCONSTINT, - ACCUMULATE, - MAKESWITCHBLOCK, MAKEACCU, MAKEPROD, -/* spiwack: */ - BRANCH, - CHECKADDINT63, ADDINT63, CHECKADDCINT63, CHECKADDCARRYCINT63, - CHECKSUBINT63, SUBINT63, CHECKSUBCINT63, CHECKSUBCARRYCINT63, - CHECKMULINT63, CHECKMULCINT63, - CHECKDIVINT63, CHECKMODINT63, CHECKDIVEUCLINT63, CHECKDIV21INT63, - CHECKLXORINT63, CHECKLORINT63, CHECKLANDINT63, - CHECKLSLINT63, CHECKLSRINT63, CHECKADDMULDIVINT63, - CHECKLSLINT63CONST1, CHECKLSRINT63CONST1, - - CHECKEQINT63, CHECKLTINT63, LTINT63, CHECKLEINT63, LEINT63, - CHECKCOMPAREINT63, - - CHECKHEAD0INT63, CHECKTAIL0INT63, - - ISINT, AREINT2, - - STOP -}; - -#endif /* _COQ_INSTRUCT_ */ diff --git a/kernel/byterun/dune b/kernel/byterun/dune index c3c44670be..20bdf28e54 100644 --- a/kernel/byterun/dune +++ b/kernel/byterun/dune @@ -5,6 +5,9 @@ (c_names coq_fix_code coq_memory coq_values coq_interp)) (rule + (targets coq_instruct.h) + (action (with-stdout-to %{targets} (run ../genOpcodeFiles.exe enum)))) + +(rule (targets coq_jumptbl.h) - (deps (:h-file coq_instruct.h) make_jumptbl.sh) - (action (bash "./make_jumptbl.sh %{h-file} %{targets}"))) + (action (with-stdout-to %{targets} (run ../genOpcodeFiles.exe jump)))) diff --git a/kernel/byterun/make_jumptbl.sh b/kernel/byterun/make_jumptbl.sh deleted file mode 100755 index eacd4daac8..0000000000 --- a/kernel/byterun/make_jumptbl.sh +++ /dev/null @@ -1,3 +0,0 @@ -#!/usr/bin/env bash - -sed -n -e '/^ /s/ \([A-Z]\)/ \&\&coq_lbl_\1/gp' -e '/^}/q' ${1} > ${2} diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 6777e0c223..567850645e 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -166,7 +166,7 @@ type one_inductive_body = { mind_kelim : Sorts.family list; (** List of allowed elimination sorts *) - mind_nf_lc : types array; (** Head normalized constructor types so that their conclusion exposes the inductive type *) + mind_nf_lc : (rel_context * types) array; (** Head normalized constructor types so that their conclusion exposes the inductive type *) mind_consnrealargs : int array; (** Number of expected proper arguments of the constructors (w/o params) *) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 9e0230c3ba..d56502a095 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -214,7 +214,7 @@ let subst_mind_packet sub mbp = mind_consnrealdecls = mbp.mind_consnrealdecls; mind_consnrealargs = mbp.mind_consnrealargs; mind_typename = mbp.mind_typename; - mind_nf_lc = Array.Smart.map (subst_mps sub) mbp.mind_nf_lc; + mind_nf_lc = Array.Smart.map (fun (ctx, c) -> Context.Rel.map (subst_mps sub) ctx, subst_mps sub c) mbp.mind_nf_lc; mind_arity_ctxt = subst_rel_context sub mbp.mind_arity_ctxt; mind_arity = subst_ind_arity sub mbp.mind_arity; mind_user_lc = Array.Smart.map (subst_mps sub) mbp.mind_user_lc; @@ -299,9 +299,8 @@ let hcons_ind_arity = let hcons_mind_packet oib = let user = Array.Smart.map Constr.hcons oib.mind_user_lc in - let nf = Array.Smart.map Constr.hcons oib.mind_nf_lc in - (* Special optim : merge [mind_user_lc] and [mind_nf_lc] if possible *) - let nf = if Array.equal (==) user nf then user else nf in + let map (ctx, c) = Context.Rel.map Constr.hcons ctx, Constr.hcons c in + let nf = Array.Smart.map map oib.mind_nf_lc in { oib with mind_typename = Names.Id.hcons oib.mind_typename; mind_arity_ctxt = hcons_rel_context oib.mind_arity_ctxt; diff --git a/kernel/dune b/kernel/dune index 1f2d696a36..a8a87a3e95 100644 --- a/kernel/dune +++ b/kernel/dune @@ -3,13 +3,16 @@ (synopsis "The Coq Kernel") (public_name coq.kernel) (wrapped false) - (modules (:standard \ uint63_x86 uint63_amd64 write_uint63)) + (modules (:standard \ genOpcodeFiles uint63_x86 uint63_amd64 write_uint63)) (libraries lib byterun)) +(executable + (name genOpcodeFiles) + (modules genOpcodeFiles)) + (rule (targets copcodes.ml) - (deps (:h-file byterun/coq_instruct.h) make-opcodes make_opcodes.sh) - (action (bash "./make_opcodes.sh %{h-file} %{targets}"))) + (action (with-stdout-to %{targets} (run ./genOpcodeFiles.exe copml)))) (executable (name write_uint63) diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml new file mode 100644 index 0000000000..6564954dfd --- /dev/null +++ b/kernel/genOpcodeFiles.ml @@ -0,0 +1,193 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <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) *) +(************************************************************************) + +(** List of opcodes. + + It is used to generate the [coq_instruct.h], [coq_jumptbl.h] and + [copcodes.ml] files. + + If adding an instruction, DON'T FORGET TO UPDATE coq_fix_code.c + with the arity of the instruction and maybe coq_tcode_of_code. +*) +let opcodes = + [| + "ACC0"; + "ACC1"; + "ACC2"; + "ACC3"; + "ACC4"; + "ACC5"; + "ACC6"; + "ACC7"; + "ACC"; + "PUSH"; + "PUSHACC0"; + "PUSHACC1"; + "PUSHACC2"; + "PUSHACC3"; + "PUSHACC4"; + "PUSHACC5"; + "PUSHACC6"; + "PUSHACC7"; + "PUSHACC"; + "POP"; + "ENVACC1"; + "ENVACC2"; + "ENVACC3"; + "ENVACC4"; + "ENVACC"; + "PUSHENVACC1"; + "PUSHENVACC2"; + "PUSHENVACC3"; + "PUSHENVACC4"; + "PUSHENVACC"; + "PUSH_RETADDR"; + "APPLY"; + "APPLY1"; + "APPLY2"; + "APPLY3"; + "APPLY4"; + "APPTERM"; + "APPTERM1"; + "APPTERM2"; + "APPTERM3"; + "RETURN"; + "RESTART"; + "GRAB"; + "GRABREC"; + "CLOSURE"; + "CLOSUREREC"; + "CLOSURECOFIX"; + "OFFSETCLOSUREM2"; + "OFFSETCLOSURE0"; + "OFFSETCLOSURE2"; + "OFFSETCLOSURE"; + "PUSHOFFSETCLOSUREM2"; + "PUSHOFFSETCLOSURE0"; + "PUSHOFFSETCLOSURE2"; + "PUSHOFFSETCLOSURE"; + "GETGLOBAL"; + "PUSHGETGLOBAL"; + "MAKEBLOCK"; + "MAKEBLOCK1"; + "MAKEBLOCK2"; + "MAKEBLOCK3"; + "MAKEBLOCK4"; + "SWITCH"; + "PUSHFIELDS"; + "GETFIELD0"; + "GETFIELD1"; + "GETFIELD"; + "SETFIELD0"; + "SETFIELD1"; + "SETFIELD"; + "PROJ"; + "ENSURESTACKCAPACITY"; + "CONST0"; + "CONST1"; + "CONST2"; + "CONST3"; + "CONSTINT"; + "PUSHCONST0"; + "PUSHCONST1"; + "PUSHCONST2"; + "PUSHCONST3"; + "PUSHCONSTINT"; + "ACCUMULATE"; + "MAKESWITCHBLOCK"; + "MAKEACCU"; + "MAKEPROD"; + "BRANCH"; + "CHECKADDINT63"; + "ADDINT63"; + "CHECKADDCINT63"; + "CHECKADDCARRYCINT63"; + "CHECKSUBINT63"; + "SUBINT63"; + "CHECKSUBCINT63"; + "CHECKSUBCARRYCINT63"; + "CHECKMULINT63"; + "CHECKMULCINT63"; + "CHECKDIVINT63"; + "CHECKMODINT63"; + "CHECKDIVEUCLINT63"; + "CHECKDIV21INT63"; + "CHECKLXORINT63"; + "CHECKLORINT63"; + "CHECKLANDINT63"; + "CHECKLSLINT63"; + "CHECKLSRINT63"; + "CHECKADDMULDIVINT63"; + "CHECKLSLINT63CONST1"; + "CHECKLSRINT63CONST1"; + "CHECKEQINT63"; + "CHECKLTINT63"; + "LTINT63"; + "CHECKLEINT63"; + "LEINT63"; + "CHECKCOMPAREINT63"; + "CHECKHEAD0INT63"; + "CHECKTAIL0INT63"; + "ISINT"; + "AREINT2"; + "STOP" + |] + +let pp_c_comment fmt = + Format.fprintf fmt "/* %a */" + +let pp_ocaml_comment fmt = + Format.fprintf fmt "(* %a *)" + +let pp_header isOcaml fmt = + Format.fprintf fmt "%a" + (fun fmt -> + (if isOcaml then pp_ocaml_comment else pp_c_comment) fmt + Format.pp_print_string) + "DO NOT EDIT: automatically generated by kernel/genOpcodeFiles.ml" + +let pp_with_commas fmt k = + Array.iteri (fun n s -> + Format.fprintf fmt " %a%s@." + k s + (if n + 1 < Array.length opcodes + then "," else "") + ) opcodes + +let pp_coq_instruct_h fmt = + let line = Format.fprintf fmt "%s@." in + pp_header false fmt; + line "#pragma once"; + line "enum instructions {"; + pp_with_commas fmt Format.pp_print_string; + line "};" + +let pp_coq_jumptbl_h fmt = + pp_with_commas fmt (fun fmt -> Format.fprintf fmt "&&coq_lbl_%s") + +let pp_copcodes_ml fmt = + pp_header true fmt; + Array.iteri (fun n s -> + Format.fprintf fmt "let op%s = %d@.@." s n + ) opcodes + +let usage () = + Format.eprintf "usage: %s [enum|jump|copml]@." Sys.argv.(0); + exit 1 + +let main () = + match Sys.argv.(1) with + | "enum" -> pp_coq_instruct_h Format.std_formatter + | "jump" -> pp_coq_jumptbl_h Format.std_formatter + | "copml" -> pp_copcodes_ml Format.std_formatter + | _ -> usage () + | exception Invalid_argument _ -> usage () + +let () = main () diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 8f06e1e4b8..457c17907e 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -416,7 +416,9 @@ let compute_projections (kn, i as ind) mib = let pkt = mib.mind_packets.(i) in let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in let subst = List.init mib.mind_ntypes (fun i -> mkIndU ((kn, mib.mind_ntypes - i - 1), u)) in - let rctx, _ = decompose_prod_assum (substl subst pkt.mind_nf_lc.(0)) in + let (ctx, cty) = pkt.mind_nf_lc.(0) in + let cty = it_mkProd_or_LetIn cty ctx in + let rctx, _ = decompose_prod_assum (substl subst cty) in let ctx, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in (** We build a substitution smashing the lets in the record parameters so that typechecking projections requires just a substitution and not @@ -475,7 +477,7 @@ let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite (* Check one inductive *) let build_one_packet (id,cnames) ((arity,lc),(indices,splayed_lc),kelim) recarg = (* Type of constructors in normal form *) - let nf_lc = Array.map (fun (d,b) -> it_mkProd_or_LetIn b (d@paramsctxt)) splayed_lc in + let nf_lc = Array.map (fun (d, b) -> (d@paramsctxt, b)) splayed_lc in let consnrealdecls = Array.map (fun (d,_) -> Context.Rel.length d) splayed_lc in diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 848ae65c51..f4c2483c14 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -251,7 +251,11 @@ let constrained_type_of_constructor (_cstr,u as cstru) (mib,_mip as ind) = let arities_of_specif (kn,u) (mib,mip) = let specif = mip.mind_nf_lc in - Array.map (constructor_instantiate kn u mib) specif + let map (ctx, c) = + let cty = Term.it_mkProd_or_LetIn c ctx in + constructor_instantiate kn u mib cty + in + Array.map map specif let arities_of_constructors ind specif = arities_of_specif (fst (fst ind), snd ind) specif @@ -342,7 +346,8 @@ let is_correct_arity env c pj ind specif params = (* [p] is the predicate, [i] is the constructor number (starting from 0), and [cty] is the type of the constructor (params not instantiated) *) let build_branches_type (ind,u) (_,mip as specif) params p = - let build_one_branch i cty = + let build_one_branch i (ctx, c) = + let cty = Term.it_mkProd_or_LetIn c ctx in let typi = full_constructor_instantiate (ind,u,specif,params) cty in let (cstrsign,ccl) = Term.decompose_prod_assum typi in let nargs = Context.Rel.length cstrsign in @@ -597,6 +602,7 @@ let lambda_implicit_lift n a = (* This removes global parameters of the inductive types in lc (for nested inductive types only ) *) let abstract_mind_lc ntyps npars lc = + let lc = Array.map (fun (ctx, c) -> Term.it_mkProd_or_LetIn c ctx) lc in if Int.equal npars 0 then lc else diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 3c1464c6c9..ad35c16c22 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -139,4 +139,4 @@ val subterm_specif : guard_env -> stack_element list -> constr -> subterm_spec val lambda_implicit_lift : int -> constr -> constr -val abstract_mind_lc : int -> Int.t -> constr array -> constr array +val abstract_mind_lc : int -> Int.t -> (rel_context * constr) array -> constr array diff --git a/kernel/make-opcodes b/kernel/make-opcodes deleted file mode 100644 index e1371b3d0c..0000000000 --- a/kernel/make-opcodes +++ /dev/null @@ -1,3 +0,0 @@ -$1=="enum" {n=0; next; } - {printf("(* THIS FILE IS GENERATED. DON'T EDIT. *)\n\n"); - for (i = 1; i <= NF; i++) {printf("let op%s = %d\n", $i, n++);}} diff --git a/kernel/make_opcodes.sh b/kernel/make_opcodes.sh deleted file mode 100755 index bb8aba2f07..0000000000 --- a/kernel/make_opcodes.sh +++ /dev/null @@ -1,4 +0,0 @@ -#!/usr/bin/env bash - -script_dir="$(dirname "$0")" -tr -d "\r" < "${1}" | sed -n -e '/^enum/p' -e 's/,//g' -e '/^ /p' | awk -f "$script_dir"/make-opcodes > "${2}" diff --git a/kernel/write_uint63.ml b/kernel/write_uint63.ml index 0fcaf4f10a..beb59ce205 100644 --- a/kernel/write_uint63.ml +++ b/kernel/write_uint63.ml @@ -1,10 +1,18 @@ -(** Equivalent of rm -f *) +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <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) *) +(************************************************************************) +(** Equivalent of rm -f *) let safe_remove f = try Unix.chmod f 0o644; Sys.remove f with _ -> () (** * Generate an implementation of 63-bit arithmetic *) - let ml_file_copy input output = safe_remove output; let i = open_in input in diff --git a/lib/flags.ml b/lib/flags.ml index 1195b8caf1..6718e7a954 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -43,8 +43,6 @@ let with_options ol f x = let record_aux_file = ref false -let test_mode = ref false - let async_proofs_worker_id = ref "master" let async_proofs_is_worker () = !async_proofs_worker_id <> "master" diff --git a/lib/flags.mli b/lib/flags.mli index 2b4446a1db..bf8846417b 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -35,10 +35,6 @@ be eventually removed by cleanups such as PR#1103 *) val record_aux_file : bool ref -(* Flag set when the test-suite is called. Its only effect to display - verbose information for `Fail` *) -val test_mode : bool ref - (** Async-related flags *) val async_proofs_worker_id : string ref val async_proofs_is_worker : unit -> bool diff --git a/lib/future.ml b/lib/future.ml index b372bedc5d..6e7c6fd9e3 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -33,7 +33,7 @@ let _ = CErrors.register_handler (function | _ -> raise CErrors.Unhandled) type fix_exn = Exninfo.iexn -> Exninfo.iexn -let id x = prerr_endline "Future: no fix_exn.\nYou have probably created a Future.computation from a value without passing the ~fix_exn argument. You probably want to chain with an already existing future instead."; x +let id x = x module UUID = struct type t = int diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 204f889f90..ef6c07bff2 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -1044,7 +1044,9 @@ let fake_match_projection env p = let indu = mkIndU (ind,u) in let ctx, paramslet = let subst = List.init mib.mind_ntypes (fun i -> mkIndU ((fst ind, mib.mind_ntypes - i - 1), u)) in - let rctx, _ = decompose_prod_assum (Vars.substl subst mip.mind_nf_lc.(0)) in + let (ctx, cty) = mip.mind_nf_lc.(0) in + let cty = Term.it_mkProd_or_LetIn cty ctx in + let rctx, _ = decompose_prod_assum (Vars.substl subst cty) in List.chop mip.mind_consnrealdecls.(0) rctx in let ci_pp_info = { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index a60a966cec..56b3dc97cf 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -13,7 +13,6 @@ open Names open Constr open EConstr open Vars -open Termops open Util open Declarations open Globnames @@ -100,9 +99,8 @@ let kind_of_formula env sigma term = else let has_realargs=(n>0) in let is_trivial= - let is_constant c = - Int.equal (nb_prod sigma (EConstr.of_constr c)) mib.mind_nparams in - Array.exists is_constant mip.mind_nf_lc in + let is_constant n = Int.equal n 0 in + Array.exists is_constant mip.mind_consnrealargs in if Inductiveops.mis_is_recursive (ind,mib,mip) || (has_realargs && not is_trivial) then diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg index 9ecc36bdf3..3f2fabeeee 100644 --- a/plugins/ltac/g_class.mlg +++ b/plugins/ltac/g_class.mlg @@ -99,8 +99,19 @@ TACTIC EXTEND is_ground | [ "is_ground" constr(ty) ] -> { is_ground ty } END +{ +let deprecated_autoapply_using = + CWarnings.create + ~name:"autoapply-using" ~category:"deprecated" + (fun () -> Pp.str "The syntax [autoapply ... using] is deprecated. Use [autoapply ... with] instead.") +} + TACTIC EXTEND autoapply -| [ "autoapply" constr(c) "using" preident(i) ] -> { autoapply c i } +| [ "autoapply" constr(c) "using" preident(i) ] -> { + deprecated_autoapply_using (); + autoapply c i + } +| [ "autoapply" constr(c) "with" preident(i) ] -> { autoapply c i } END { diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index a0b1d784f1..7216849948 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -209,7 +209,8 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = let mind,indb = Inductive.lookup_mind_specif env (kn,i) in let tys = indb.Declarations.mind_nf_lc in let renamed_tys = - Array.mapi (fun j t -> + Array.mapi (fun j (ctx, cty) -> + let t = Term.it_mkProd_or_LetIn cty ctx in ppdebug(lazy Pp.(str "Search" ++ Printer.pr_constr_env env (project gl) t)); let t = Arguments_renaming.rename_type t (GlobRef.ConstructRef((kn,i),j+1)) in diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 68626597fc..affed5389f 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -514,12 +514,11 @@ let rec cases_pattern_of_glob_constr na c = ) c open Declarations -open Term open Context (* Keep only patterns which are not bound to a local definitions *) -let drop_local_defs typi args = - let (decls,_) = decompose_prod_assum typi in +let drop_local_defs params decls args = + let decls = List.skipn (Rel.length params) (List.rev decls) in let rec aux decls args = match decls, args with | [], [] -> [] @@ -531,7 +530,7 @@ let drop_local_defs typi args = end | Rel.Declaration.LocalAssum _ :: decls, a :: args -> a :: aux decls args | _ -> assert false in - aux (List.rev decls) args + aux decls args let add_patterns_for_params_remove_local_defs (ind,j) l = let (mib,mip) = Global.lookup_inductive ind in @@ -540,9 +539,8 @@ let add_patterns_for_params_remove_local_defs (ind,j) l = if mip.mind_consnrealdecls.(j-1) = mip.mind_consnrealargs.(j-1) then (* Optimisation *) l else - let typi = mip.mind_nf_lc.(j-1) in - let (_,typi) = decompose_prod_n_assum (Rel.length mib.mind_params_ctxt) typi in - drop_local_defs typi l in + let (ctx, _) = mip.mind_nf_lc.(j - 1) in + drop_local_defs mib.mind_params_ctxt ctx l in Util.List.addn nparams (DAst.make @@ PatVar Anonymous) l let add_alias ?loc na c = diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 4c02dc0f09..d937456bcb 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -101,7 +101,8 @@ let mis_nf_constructor_type ((ind,u),mib,mip) j = and nconstr = Array.length mip.mind_consnames in let make_Ik k = mkIndU (((fst ind),ntypes-k-1),u) in if j > nconstr then user_err Pp.(str "Not enough constructors in the type."); - substl (List.init ntypes make_Ik) (subst_instance_constr u specif.(j-1)) + let (ctx, cty) = specif.(j - 1) in + substl (List.init ntypes make_Ik) (subst_instance_constr u (Term.it_mkProd_or_LetIn cty ctx)) (* Number of constructors *) @@ -280,8 +281,7 @@ let make_case_info env ind style = let ind_tags = Context.Rel.to_tags (List.firstn mip.mind_nrealdecls mip.mind_arity_ctxt) in let cstr_tags = - Array.map2 (fun c n -> - let d,_ = decompose_prod_assum c in + Array.map2 (fun (d, _) n -> Context.Rel.to_tags (List.firstn n d)) mip.mind_nf_lc mip.mind_consnrealdecls in let print_info = { ind_tags; cstr_tags; style } in @@ -462,7 +462,8 @@ let compute_projections env (kn, i as ind) = let pkt = mib.mind_packets.(i) in let { mind_nparams = nparamargs; mind_params_ctxt = params } = mib in let subst = List.init mib.mind_ntypes (fun i -> mkIndU ((kn, mib.mind_ntypes - i - 1), u)) in - let rctx, _ = decompose_prod_assum (substl subst pkt.mind_nf_lc.(0)) in + let ctx, cty = pkt.mind_nf_lc.(0) in + let rctx, _ = decompose_prod_assum (substl subst (Term.it_mkProd_or_LetIn cty ctx)) in let ctx, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in (* We build a substitution smashing the lets in the record parameters so that typechecking projections requires just a substitution and not @@ -622,9 +623,7 @@ let set_pattern_names env sigma ind brv = let (mib,mip) = Inductive.lookup_mind_specif env ind in let arities = Array.map - (fun c -> - Context.Rel.length ((prod_assum c)) - - mib.mind_nparams) + (fun (d, _) -> List.length d - mib.mind_nparams) mip.mind_nf_lc in Array.map2 (set_names env sigma) arities brv diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index b7090e69da..77ae09ee6f 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -107,7 +107,8 @@ let find_rectype_a env c = (* Instantiate inductives and parameters in constructor type *) -let type_constructor mind mib u typ params = +let type_constructor mind mib u (ctx, typ) params = + let typ = it_mkProd_or_LetIn typ ctx in let s = ind_subst mind mib u in let ctyp = substl s typ in let nparams = Array.length params in diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 083661a64b..ff528bd2cf 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -61,7 +61,8 @@ let find_rectype_a env c = (* Instantiate inductives and parameters in constructor type *) -let type_constructor mind mib u typ params = +let type_constructor mind mib u (ctx, typ) params = + let typ = it_mkProd_or_LetIn typ ctx in let s = ind_subst mind mib u in let ctyp = substl s typ in let ctyp = subst_instance_constr u ctyp in diff --git a/stm/stm.ml b/stm/stm.ml index 8af1a2ebd2..ab388977a5 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -3205,10 +3205,9 @@ let edit_at ~doc id = let vcs = VCS.backup () in let on_cur_branch id = let rec aux cur = - if id = cur then true - else match VCS.visit cur with + match VCS.visit cur with | { step = `Fork _ } -> false - | { next } -> aux next in + | { next } -> if id = cur then true else aux next in aux (VCS.get_branch_pos (VCS.current_branch ())) in let rec is_pure_aux id = let view = VCS.visit id in diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index b12018cd66..3c1115d056 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -138,7 +138,7 @@ let get_sym_eq_data env (ind,u) = let realsign,_ = List.chop mip.mind_nrealdecls arityctxt in if List.exists is_local_def realsign then error "Inductive equalities with local definitions in arity not supported."; - let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in + let constrsign,ccl = mip.mind_nf_lc.(0) in let _,constrargs = decompose_app ccl in if not (Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt)) then error "Constructor must have no arguments"; (* This can be relaxed... *) @@ -173,7 +173,7 @@ let get_non_sym_eq_data env (ind,u) = let realsign,_ = List.chop mip.mind_nrealdecls arityctxt in if List.exists is_local_def realsign then error "Inductive equalities with local definitions in arity not supported"; - let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in + let constrsign,ccl = mip.mind_nf_lc.(0) in let _,constrargs = decompose_app ccl in if not (Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt)) then error "Constructor must have no arguments"; @@ -776,7 +776,7 @@ let build_congr env (eq,refl,ctx) ind = error "Inductive equalities with local definitions in arity not supported."; let env_with_arity = push_rel_context arityctxt env in let ty = RelDecl.get_type (lookup_rel (mip.mind_nrealargs - i + 1) env_with_arity) in - let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in + let constrsign,ccl = mip.mind_nf_lc.(0) in let _,constrargs = decompose_app ccl in if not (Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt)) then error "Constructor must have no arguments"; diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 708412720a..395b4928ce 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -106,22 +106,24 @@ let match_with_one_constructor sigma style onlybinary allow_rec t = && (Int.equal mip.mind_nrealargs 0) then if is_strict_conjunction style (* strict conjunction *) then - let ctx = - (prod_assum sigma (snd - (decompose_prod_n_assum sigma mib.mind_nparams (EConstr.of_constr mip.mind_nf_lc.(0))))) in + let (ctx, _) = mip.mind_nf_lc.(0) in + let ctx = List.skipn (Context.Rel.length mib.mind_params_ctxt) (List.rev ctx) in if + (* Constructor has a type of the form + c : forall (a_0 ... a_n : Type) (x_0 : A_0) ... (x_n : A_n). T **) List.for_all (fun decl -> let c = RelDecl.get_type decl in is_local_assum decl && - isRel sigma c && - Int.equal (destRel sigma c) mib.mind_nparams) ctx + Constr.isRel c && + Int.equal (Constr.destRel c) mib.mind_nparams) ctx then Some (hdapp,args) else None else + let ctx, cty = mip.mind_nf_lc.(0) in + let cty = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in let ctyp = whd_beta_prod sigma - (Termops.prod_applist_assum sigma (Context.Rel.length mib.mind_params_ctxt) - (EConstr.of_constr mip.mind_nf_lc.(0)) args) in + (Termops.prod_applist_assum sigma (Context.Rel.length mib.mind_params_ctxt) cty args) in let cargs = List.map RelDecl.get_type (prod_assum sigma ctyp) in if not (is_lax_conjunction style) || has_nodep_prod sigma ctyp then (* Record or non strict conjunction *) @@ -165,12 +167,13 @@ let is_tuple sigma t = it is strict if it has the form "Inductive I A1 ... An := C1 (_:A1) | ... | Cn : (_:An)" *) -let test_strict_disjunction n lc = - let open Term in - Array.for_all_i (fun i c -> - match (prod_assum (snd (decompose_prod_n_assum n c))) with - | [LocalAssum (_,c)] -> Constr.isRel c && Int.equal (Constr.destRel c) (n - i) - | _ -> false) 0 lc +let test_strict_disjunction (mib, mip) = + let n = List.length mib.mind_params_ctxt in + let check i (ctx, _) = match List.skipn n (List.rev ctx) with + | [LocalAssum (_, c)] -> Constr.isRel c && Int.equal (Constr.destRel c) (n - i) + | _ -> false + in + Array.for_all_i check 0 mip.mind_nf_lc let match_with_disjunction ?(strict=false) ?(onlybinary=false) sigma t = let (hdapp,args) = decompose_app sigma t in @@ -183,14 +186,16 @@ let match_with_disjunction ?(strict=false) ?(onlybinary=false) sigma t = && (Int.equal mip.mind_nrealargs 0) then if strict then - if test_strict_disjunction mib.mind_nparams mip.mind_nf_lc then + if test_strict_disjunction (mib, mip) then Some (hdapp,args) else None else - let cargs = - Array.map (fun ar -> pi2 (destProd sigma (prod_applist sigma (EConstr.of_constr ar) args))) - mip.mind_nf_lc in + let map (ctx, cty) = + let ar = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in + pi2 (destProd sigma (prod_applist sigma ar args)) + in + let cargs = Array.map map mip.mind_nf_lc in Some (hdapp,Array.to_list cargs) else None @@ -225,10 +230,8 @@ let match_with_unit_or_eq_type sigma t = match EConstr.kind sigma hdapp with | Ind (ind , _) -> let (mib,mip) = Global.lookup_inductive ind in - let constr_types = mip.mind_nf_lc in let nconstr = Array.length mip.mind_consnames in - let zero_args c = Int.equal (nb_prod sigma (EConstr.of_constr c)) mib.mind_nparams in - if Int.equal nconstr 1 && zero_args constr_types.(0) then + if Int.equal nconstr 1 && Int.equal mip.mind_consnrealargs.(0) 0 then Some hdapp else None @@ -308,11 +311,13 @@ let match_with_equation env sigma t = let constr_types = mip.mind_nf_lc in let nconstr = Array.length mip.mind_consnames in if Int.equal nconstr 1 then - if is_matching env sigma coq_refl_leibniz1_pattern (EConstr.of_constr constr_types.(0)) then + let (ctx, cty) = constr_types.(0) in + let cty = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in + if is_matching env sigma coq_refl_leibniz1_pattern cty then None, hdapp, MonomorphicLeibnizEq(args.(0),args.(1)) - else if is_matching env sigma coq_refl_leibniz2_pattern (EConstr.of_constr constr_types.(0)) then + else if is_matching env sigma coq_refl_leibniz2_pattern cty then None, hdapp, PolymorphicLeibnizEq(args.(0),args.(1),args.(2)) - else if is_matching env sigma coq_refl_jm_pattern (EConstr.of_constr constr_types.(0)) then + else if is_matching env sigma coq_refl_jm_pattern cty then None, hdapp, HeterogenousEq(args.(0),args.(1),args.(2),args.(3)) else raise NoEquationFound else raise NoEquationFound @@ -378,8 +383,9 @@ let match_with_nodep_ind sigma t = | Ind (ind, _) -> let (mib,mip) = Global.lookup_inductive ind in if Array.length (mib.mind_packets)>1 then None else - let nodep_constr c = - has_nodep_prod_after (Context.Rel.length mib.mind_params_ctxt) sigma (EConstr.of_constr c) in + let nodep_constr (ctx, cty) = + let c = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in + has_nodep_prod_after (Context.Rel.length mib.mind_params_ctxt) sigma c in if Array.for_all nodep_constr mip.mind_nf_lc then let params= if Int.equal mip.mind_nrealargs 0 then args else @@ -400,7 +406,7 @@ let match_with_sigma_type sigma t = && (Int.equal mip.mind_nrealargs 0) && (Int.equal (Array.length mip.mind_consnames)1) && has_nodep_prod_after (Context.Rel.length mib.mind_params_ctxt + 1) sigma - (EConstr.of_constr mip.mind_nf_lc.(0)) + (let (ctx, cty) = mip.mind_nf_lc.(0) in EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx)) then (*allowing only 1 existential*) Some (hdapp,args) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index bfbce8f6eb..ec8d4d0e14 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -20,6 +20,7 @@ open Tacmach open Clenv open Tactypes +module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration (************************************************************************) @@ -223,8 +224,8 @@ let compute_induction_names = compute_induction_names_gen true (* Compute the let-in signature of case analysis or standard induction scheme *) let compute_constructor_signatures ~rec_flag ((_,k as ity),u) = let rec analrec c recargs = - match Constr.kind c, recargs with - | Prod (_,_,c), recarg::rest -> + match c, recargs with + | RelDecl.LocalAssum _ :: c, recarg::rest -> let rest = analrec c rest in begin match Declareops.dest_recarg recarg with | Norec | Imbr _ -> true :: rest @@ -232,14 +233,13 @@ let compute_constructor_signatures ~rec_flag ((_,k as ity),u) = if rec_flag && Int.equal j k then true :: true :: rest else true :: rest end - | LetIn (_,_,_,c), rest -> false :: analrec c rest - | _, [] -> [] + | RelDecl.LocalDef _ :: c, rest -> false :: analrec c rest + | [], [] -> [] | _ -> anomaly (Pp.str "compute_constructor_signatures.") in let (mib,mip) = Global.lookup_inductive ity in - let n = mib.mind_nparams in - let lc = - Array.map (fun c -> snd (Term.decompose_prod_n_assum n c)) mip.mind_nf_lc in + let map (ctx, _) = List.skipn (Context.Rel.length mib.mind_params_ctxt) (List.rev ctx) in + let lc = Array.map map mip.mind_nf_lc in let lrecargs = Declareops.dest_subterms mip.mind_recargs in Array.map2 analrec lc lrecargs diff --git a/test-suite/Makefile b/test-suite/Makefile index 5582503d89..6efd47afc2 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -38,9 +38,9 @@ include ../Makefile.common BIN := $(shell cd ..; pwd)/bin/ COQFLAGS?= +COQLIB?= ifeq ($(COQLIB),) - # This method of setting `pwd` won't work on win32 OCaml - COQLIB := $(shell cd ..; pwd) + COQLIB := $(shell ocaml ocaml_pwd.ml ..) endif export COQLIB diff --git a/test-suite/dune b/test-suite/dune index 9efc1e2dc1..c430400ba5 100644 --- a/test-suite/dune +++ b/test-suite/dune @@ -6,7 +6,7 @@ (rule (targets libpath.inc) - (action (with-stdout-to %{targets} (run ./ocaml_pwd.exe ../../install/%{context_name}/lib/coq/ )))) + (action (with-stdout-to %{targets} (run ./ocaml_pwd.exe -quoted ../../install/%{context_name}/lib/coq/ )))) (rule (targets summary.log) diff --git a/test-suite/ide/reopen1.fake b/test-suite/ide/reopen1.fake new file mode 100644 index 0000000000..2c4f13de86 --- /dev/null +++ b/test-suite/ide/reopen1.fake @@ -0,0 +1,22 @@ +# Script simulating a dialog between coqide and coqtop -ideslave +# Run it via fake_ide +# +# jumping outside the focused zone should signal an unfocus. + +# first proof +ADD here { Goal True. } +ADD here1 { Proof. } +ADD { Qed. } +WAIT +EDIT_AT here1 +EDIT_AT here +# fwd again +ADD here2 { Proof. } +ADD here3 { Qed. } +WAIT +EDIT_AT here2 +# Fixing the proof +ADD { Proof. } +ADD { trivial. } +ADD { Qed. } +JOIN diff --git a/test-suite/ocaml_pwd.ml b/test-suite/ocaml_pwd.ml index 10ca52a4a9..afa3deea3a 100644 --- a/test-suite/ocaml_pwd.ml +++ b/test-suite/ocaml_pwd.ml @@ -1,7 +1,7 @@ let _ = - let ch_dir = Sys.argv.(1) in + let quoted = Sys.argv.(1) = "-quoted" in + let ch_dir = Sys.argv.(if quoted then 2 else 1) in Sys.chdir ch_dir; let dir = Sys.getcwd () in - (* Needed for windows *) - let dir = Filename.quote dir in + let dir = if quoted then Filename.quote dir else dir in Format.printf "%s%!" dir diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v index 8a04206bb2..8732305953 100644 --- a/theories/Classes/Init.v +++ b/theories/Classes/Init.v @@ -23,7 +23,7 @@ Typeclasses Opaque id const flip compose arrow impl iff not all. (** Apply using the same opacity information as typeclass proof search. *) -Ltac class_apply c := autoapply c using typeclass_instances. +Ltac class_apply c := autoapply c with typeclass_instances. (** The unconvertible typeclass, to test that two objects of the same type are actually different. *) diff --git a/topbin/dune b/topbin/dune index f42e4d6fc2..e35a3de54b 100644 --- a/topbin/dune +++ b/topbin/dune @@ -36,3 +36,8 @@ (modules :standard \ coqtop_byte_bin coqtop_bin coqc_bin) (libraries coq.toplevel) (link_flags -linkall)) + +; Workers installed targets +(alias + (name topworkers) + (deps %{bin:coqqueryworker.opt} %{bin:coqtacticworker.opt} %{bin:coqproofworker.opt})) diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index abfda07426..bbccae8edb 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -457,7 +457,7 @@ let parse_args ~help ~init arglist : t * string list = |"-batch" -> Flags.quiet := true; { oval with batch = true } - |"-test-mode" -> Flags.test_mode := true; oval + |"-test-mode" -> Vernacentries.test_mode := true; oval |"-beautify" -> Flags.beautify := true; oval |"-boot" -> warn_deprecated_boot (); diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 11b64a5247..0d31992e98 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -16,7 +16,6 @@ open CAst open Util open Names open Nameops -open Term open Tacmach open Constrintern open Prettyp @@ -32,6 +31,7 @@ open Lemmas open Locality open Attributes +module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration (** TODO: make this function independent of Ltac *) @@ -133,22 +133,23 @@ let show_intro all = *) let make_cases_aux glob_ref = + let open Declarations in match glob_ref with | Globnames.IndRef ind -> - let {Declarations.mind_nparams = np} , {Declarations.mind_nf_lc = tarr} = Global.lookup_inductive ind in + let mib, mip = Global.lookup_inductive ind in Util.Array.fold_right_i - (fun i typ l -> - let al = List.rev (fst (decompose_prod typ)) in - let al = Util.List.skipn np al in + (fun i (ctx, _) l -> + let al = Util.List.skipn (List.length mib.mind_params_ctxt) (List.rev ctx) in let rec rename avoid = function | [] -> [] - | (n,_)::l -> + | RelDecl.LocalDef _ :: l -> "_" :: rename avoid l + | RelDecl.LocalAssum (n, _)::l -> let n' = Namegen.next_name_away_with_default (Id.to_string Namegen.default_dependent_ident) n avoid in Id.to_string n' :: rename (Id.Set.add n' avoid) l in let al' = rename Id.Set.empty al in let consref = ConstructRef (ith_constructor_of_inductive ind (i + 1)) in (Libnames.string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty consref) :: al') :: l) - tarr [] + mip.mind_nf_lc [] | _ -> raise Not_found let make_cases s = @@ -2377,6 +2378,8 @@ let locate_if_not_already ?loc (e, info) = exception HasNotFailed exception HasFailed of Pp.t +let test_mode = ref false + (* XXX STATE: this type hints that restoring the state should be the caller's responsibility *) let with_fail st b f = @@ -2402,7 +2405,7 @@ let with_fail st b f = | HasNotFailed -> user_err ~hdr:"Fail" (str "The command has not failed!") | HasFailed msg -> - if not !Flags.quiet || !Flags.test_mode then Feedback.msg_info + if not !Flags.quiet || !test_mode then Feedback.msg_info (str "The command has indeed failed with message:" ++ fnl () ++ msg) | _ -> assert false end diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index 4fbd3849b0..f43cec48e9 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -41,3 +41,7 @@ val command_focus : unit Proof.focus_kind val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr -> Evd.evar_map * Redexpr.red_expr) Hook.t + +(* Flag set when the test-suite is called. Its only effect to display + verbose information for `Fail` *) +val test_mode : bool ref |