diff options
| -rw-r--r-- | .github/PULL_REQUEST_TEMPLATE.md | 2 | ||||
| -rw-r--r-- | .gitlab-ci.yml | 13 | ||||
| -rw-r--r-- | .mailmap | 15 | ||||
| -rw-r--r-- | CHANGES.md (renamed from CHANGES) | 100 | ||||
| -rw-r--r-- | INSTALL | 4 | ||||
| -rw-r--r-- | README.md | 2 | ||||
| -rw-r--r-- | coq.opam | 6 | ||||
| -rwxr-xr-x | dev/build/windows/makecoq_mingw.sh | 2 | ||||
| -rw-r--r-- | dev/ci/README.md | 2 | ||||
| -rwxr-xr-x | dev/ci/ci-basic-overlay.sh | 5 | ||||
| -rwxr-xr-x | dev/ci/ci-iris-lambda-rust.sh | 4 | ||||
| -rw-r--r-- | dev/ci/docker/bionic_coq/Dockerfile | 4 | ||||
| -rw-r--r-- | dev/doc/MERGING.md | 4 | ||||
| -rw-r--r-- | dev/doc/changes.md | 70 | ||||
| -rw-r--r-- | doc/sphinx/credits-contents.rst | 4 | ||||
| -rw-r--r-- | ide/coqide.opam | 12 | ||||
| -rw-r--r-- | ide/dune-workspace | 6 | ||||
| -rw-r--r-- | interp/constrexpr_ops.ml | 8 | ||||
| -rw-r--r-- | interp/constrexpr_ops.mli | 24 | ||||
| -rw-r--r-- | parsing/g_constr.mlg | 10 | ||||
| -rw-r--r-- | vernac/comAssumption.ml | 5 | ||||
| -rw-r--r-- | vernac/g_vernac.mlg | 16 |
22 files changed, 184 insertions, 134 deletions
diff --git a/.github/PULL_REQUEST_TEMPLATE.md b/.github/PULL_REQUEST_TEMPLATE.md index 4a8606a38a..73b61ee0d9 100644 --- a/.github/PULL_REQUEST_TEMPLATE.md +++ b/.github/PULL_REQUEST_TEMPLATE.md @@ -16,4 +16,4 @@ Fixes / closes #???? <!-- If this is a feature pull request / breaks compatibility: --> <!-- (Otherwise, remove these lines.) --> - [ ] Corresponding documentation was added / updated (including any warning and error messages added / removed / modified). -- [ ] Entry added in CHANGES. +- [ ] Entry added in CHANGES.md. diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 34deeb3f18..da90ebaa98 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -9,7 +9,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: "bionic_coq-V2018-09-25-V1" + CACHEKEY: "bionic_coq-V2018-10-04-V1" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" @@ -234,12 +234,17 @@ windows32: except: - /^pr-.*$/ -pkg:dune-release: - <<: *dune-template +pkg:opam: stage: test + # OPAM will build out-of-tree so no point in importing artifacts + dependencies: [] + script: + - set -e + - opam pin add coq . + - opam pin add coqide ide + - set +e variables: OPAM_SWITCH: edge - DUNE_TARGET: release pkg:nix: image: nixorg/nix:latest # Minimal NixOS image which doesn't even contain git @@ -18,6 +18,7 @@ Yves Bertot <yves.bertot@inria.fr> bertot <bertot@85f007b7-540e- Yves Bertot <yves.bertot@inria.fr> Yves Bertot <bertot@inria.fr> Yves Bertot <yves.bertot@inria.fr> Yves Bertot <Yves.Bertot@inria.fr> Frédéric Besson <frederic.besson@inria.fr> fbesson <fbesson@85f007b7-540e-0410-9357-904b9bb8a0f7> +Siddharth Bhat <siddu.druid@gmail.com> Siddharth <siddu.druid@gmail.com> Pierre Boutillier <pierre.boutillier@ens-lyon.org> pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> Pierre Boutillier <pierre.boutillier@ens-lyon.org> Pierre <pierre.boutillier@ens-lyon.org> Pierre Boutillier <pierre.boutillier@ens-lyon.org> Pierre Boutillier <pierre.boutillier@pps.univ-paris-diderot.fr> @@ -31,6 +32,8 @@ Maxime Dénès <mail@maximedenes.fr> mdenes <mdenes@85f007b7-540 Maxime Dénès <mail@maximedenes.fr> Maxime Denes <maximedenes@gillespie.inria.fr> Olivier Desmettre <desmettr@gforge> desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> Damien Doligez <doligez@gforge> doligez <doligez@85f007b7-540e-0410-9357-904b9bb8a0f7> +Andres Erbsen <andreser@mit.edu> Andres Erbsen <andres@kevix.co> +Jim Fehrle <jfehrle@sbcglobal.net> Jim <jfehrle@sbcglobal.net> Jean-Christophe Filliâtre <Jean-Christophe.Filliatre@lri.fr> filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> Jean-Christophe Filliâtre <Jean-Christophe.Filliatre@lri.fr> Jean-Christophe Filliatre <Jean-Christophe.Filliatre@lri.fr> Julien Forest <julien.forest@ensiie.fr> jforest <jforest@85f007b7-540e-0410-9357-904b9bb8a0f7> @@ -43,6 +46,7 @@ Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> <gaetan.gilbert@ens-lyon.fr> Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> <gaetan.gilbert@skyskimmer.net> Stéphane Glondu <steph@glondu.net> glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> Stéphane Glondu <steph@glondu.net> Stephane Glondu <steph@glondu.net> +Matěj Grabovský <mgrabovsky@yahoo.com> Matěj G <mgrabovsky@users.noreply.github.com> Benjamin Grégoire <benjamin.gregoire@inria.fr> Benjamin Gregoire <Benjamin.Gregoire@inria.fr> Benjamin Grégoire <benjamin.gregoire@inria.fr> bgregoir <bgregoir@85f007b7-540e-0410-9357-904b9bb8a0f7> Benjamin Grégoire <benjamin.gregoire@inria.fr> gregoire <gregoire@85f007b7-540e-0410-9357-904b9bb8a0f7> @@ -51,6 +55,7 @@ Jason Gross <jgross@mit.edu> Jason Gross <jasongross9@gmai Vincent Gross <vgross@gforge> vgross <vgross@85f007b7-540e-0410-9357-904b9bb8a0f7> Huang Guan-Shieng <huang@gforge> huang <huang@85f007b7-540e-0410-9357-904b9bb8a0f7> Hugo Herbelin <Hugo.Herbelin@inria.fr> herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> +Jasper Hugunin <jasperh@cs.washington.edu> Jasper Hugunin <jasper@hashplex.com> Tom Hutchinson <thutchin@gforge> thutchin <thutchin@85f007b7-540e-0410-9357-904b9bb8a0f7> Cezary Kaliszyk <cek@gforge> cek <cek@85f007b7-540e-0410-9357-904b9bb8a0f7> Florent Kirchner <fkirchne@gforge> fkirchne <fkirchne@85f007b7-540e-0410-9357-904b9bb8a0f7> @@ -58,6 +63,7 @@ Florent Kirchner <fkirchne@gforge> kirchner <kirchner@85f007b7-5 Johannes Kloos <jkloos@mpi-sws.org> jkloos <jkloos@mpi-sws.org> Matej Košík <matej.kosik@inria.fr> Matej Kosik <m4tej.kosik@gmail.com> Matej Košík <matej.kosik@inria.fr> Matej Kosik <matej.kosik@inria.fr> +Vincent Laporte <Vincent.Laporte@fondation-inria.fr> Vincent Laporte <Vincent.Laporte@gmail.com> Marc Lasson <marc.lasson@gmail.com> mlasson <marc.lasson@gmail.com> William Lawvere <mundungus.corleone@gmail.com> william-lawvere <mundungus.corleone@gmail.com> Pierre Letouzey <pierre.letouzey@inria.fr> letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> @@ -70,6 +76,7 @@ Lionel Elie Mamane <lmamane@gforge> lmamane <lmamane@85f007b7-540 Claude Marché <marche@gforge> marche <marche@85f007b7-540e-0410-9357-904b9bb8a0f7> Micaela Mayero <mayero@gforge> mayero <mayero@85f007b7-540e-0410-9357-904b9bb8a0f7> Guillaume Melquiond <guillaume.melquiond@inria.fr> gmelquio <gmelquio@85f007b7-540e-0410-9357-904b9bb8a0f7> +Guillaume Melquiond <guillaume.melquiond@inria.fr> Guillaume Melquiond <guillaume.melquiond@gmail.com> Alexandre Miquel <miquel@gforge> miquel <miquel@85f007b7-540e-0410-9357-904b9bb8a0f7> Benjamin Monate <monate@gforge> monate <monate@85f007b7-540e-0410-9357-904b9bb8a0f7> Julien Narboux <jnarboux@gforge> jnarboux <jnarboux@85f007b7-540e-0410-9357-904b9bb8a0f7> @@ -81,6 +88,7 @@ Russell O'Connor <roconnor@blockstream.io> roconnor-blockstream <roconno Christine Paulin <cpaulin@gforge> cpaulin <cpaulin@85f007b7-540e-0410-9357-904b9bb8a0f7> Christine Paulin <cpaulin@gforge> mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> +Clément Pit-Claudel <clement.pitclaudel@live.com> Clément Pit--Claudel <clement.pitclaudel@live.com> Loïc Pottier <pottier@gforge> pottier <pottier@85f007b7-540e-0410-9357-904b9bb8a0f7> Matthias Puech <puech@gforge> puech <puech@85f007b7-540e-0410-9357-904b9bb8a0f7> Lars Rasmusson <lars.rasmusson@sics.se> larsr <Lars.Rasmusson@sics.se> @@ -91,16 +99,23 @@ Yann Régis-Gianas <yrg@pps.univ-paris-diderot.fr> regisgia <regisgia@85f007b7- Yann Régis-Gianas <yrg@pps.univ-paris-diderot.fr> Regis-Gianas <yrg@pps.univ-paris-diderot.fr> Clément Renard <clrenard@gforge> clrenard <clrenard@85f007b7-540e-0410-9357-904b9bb8a0f7> Claudio Sacerdoti Coen <sacerdot@gforge> sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> +Kazuhiko Sakaguchi <pi8027@gmail.com> Kazuhiko Sakaguchi <sakaguchi@coins.tsukuba.ac.jp> Vincent Siles <vsiles@gforge> vsiles <vsiles@85f007b7-540e-0410-9357-904b9bb8a0f7> +Michael Soegtrop <michael.soegtrop@intel.com> Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> Elie Soubiran <soubiran@gforge> soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7> Matthieu Sozeau <mattam@mattam.org> msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> Matthieu Sozeau <mattam@mattam.org> Matthieu Sozeau <matthieu.sozeau@inria.fr> +Matthieu Sozeau <mattam@mattam.org> Matthieu Sozeau <mattam@eduroam-prg-sg-1-46-137.net.univ-paris-diderot.fr> Arnaud Spiwack <arnaud@spiwack.net> aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> +Paul Steckler <steck@stecksoft.com> Paul Steckler <psteck@mit.edu> Enrico Tassi <Enrico.Tassi@inria.fr> gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> Enrico Tassi <Enrico.Tassi@inria.fr> Enrico Tassi <enrico.tassi@inria.fr> Enrico Tassi <Enrico.Tassi@inria.fr> Enrico Tassi <gares@fettunta.org> +Enrico Tassi <Enrico.Tassi@inria.fr> Enrico <gares@fettunta.org> Laurent Théry <laurent.thery@inria.fr> thery <thery@85f007b7-540e-0410-9357-904b9bb8a0f7> Laurent Théry <laurent.thery@inria.fr> thery <thery@sophia.inria.fr> +Laurent Théry <laurent.thery@inria.fr> Laurent Théry <thery@sophia.inria.fr> +Anton Trunov <anton.a.trunov@gmail.com> Anton Trunov <anton.trunov@imdea.org> Benjamin Werner <werner@gforge> werner <werner@85f007b7-540e-0410-9357-904b9bb8a0f7> Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> Theo Zimmermann <theo.zimmermann@ens.fr> Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> Théo Zimmermann <theo.zimmi@gmail.com> @@ -18,7 +18,7 @@ Tactics - Removed the deprecated `romega` tactics. - Tactic names are no longer allowed to clash, even if they are not defined in the same section. For example, the following is no longer accepted: - `Ltac foo := idtac. Section S. Ltac foo := fail. End S.` + `Ltac foo := idtac. Section S. Ltac foo := fail. End S.` Changes from 8.8.2 to 8.9+beta1 =============================== @@ -32,34 +32,34 @@ Notations - New support for autonomous grammars of terms, called "custom entries" (see chapter "Syntax extensions" of the reference manual). -- New command "Declare Scope" to explicitly declare a scope name +- New command `Declare Scope` to explicitly declare a scope name before any use of it. Implicit declaration of a scope at the time of - "Bind Scope", "Delimit Scope", "Undelimit Scope", or "Notation" is + `Bind Scope`, `Delimit Scope`, `Undelimit Scope`, or `Notation` is deprecated. Tactics -- Added toplevel goal selector ! which expects a single focused goal. - Use with Set Default Goal Selector to force focusing before tactics +- Added toplevel goal selector `!` which expects a single focused goal. + Use with `Set Default Goal Selector` to force focusing before tactics are called. - The undocumented "nameless" forms `fix N`, `cofix` that were - deprecated in 8.8 have been removed from LTAC's syntax; please use + deprecated in 8.8 have been removed from Ltac's syntax; please use `fix ident N/cofix ident` to explicitly name the (co)fixpoint hypothesis to be introduced. -- Introduction tactics "intro"/"intros" on a goal which is an +- Introduction tactics `intro`/`intros` on a goal that is an existential variable now force a refinement of the goal into a dependent product rather than failing. -- Support for fix/cofix added in Ltac "match" and "lazymatch". +- Support for `fix`/`cofix` added in Ltac `match` and `lazymatch`. - Ltac backtraces now include trace information about tactics called by OCaml-defined tactics. -- Option "Ltac Debug" now applies also to terms built using Ltac functions. +- Option `Ltac Debug` now applies also to terms built using Ltac functions. -- Deprecated the Implicit Tactic family of commands. +- Deprecated the `Implicit Tactic` family of commands. - The default program obligation tactic uses a bounded proof search instead of an unbounded and potentially non-terminating one now @@ -82,7 +82,7 @@ Tactics - The `romega` tactics have been deprecated; please use `lia` instead. - Names of existential variables occurring in Ltac functions - (e.g. "?[n]" or "?n" in terms - not in patterns) are now interpreted + (e.g. `?[n]` or `?n` in terms - not in patterns) are now interpreted the same way as other variable names occurring in Ltac functions. Focusing @@ -95,24 +95,24 @@ Specification language, type inference - A fix to unification (which was sensitive to the ascii name of variables) may occasionally change type inference in incompatible - ways, especially regarding the inference of the return clause of "match". + ways, especially regarding the inference of the return clause of `match`. - Fixing a missing check in interpreting instances of existential - variables which are bound to local definitions might exceptionally + variables that are bound to local definitions might exceptionally induce an overhead if the cost of checking the conversion of the corresponding definitions is additionally high (PR #8215). -- A few improvements in inference of the return clause of "match" can +- A few improvements in inference of the return clause of `match` can exceptionally introduce incompatibilities (PR #262). This can be - solved by writing an explicit "return" clause, sometimes even simply - an explicit "return _" clause. + solved by writing an explicit `return` clause, sometimes even simply + an explicit `return _` clause. Standard Library - Added `Ascii.eqb` and `String.eqb` and the `=?` notation for them, and proved some lemmas about them. Note that this might cause - incompatibilities if you have, e.g., string_scope and Z_scope both - open with string_scope on top, and expect `=?` to refer to `Z.eqb`. + incompatibilities if you have, e.g., `string_scope` and `Z_scope` both + open with `string_scope` on top, and expect `=?` to refer to `Z.eqb`. Solution: wrap `_ =? _` in `(_ =? _)%Z` (or whichever scope you want). @@ -152,35 +152,34 @@ Standard Library Tools - Coq_makefile lets one override or extend the following variables from - the command line: COQFLAGS, COQCHKFLAGS, COQDOCFLAGS. - COQFLAGS is now entirely separate from COQLIBS, so in custom Makefiles - $(COQFLAGS) should be replaced by $(COQFLAGS) $(COQLIBS). + the command line: `COQFLAGS`, `COQCHKFLAGS`, `COQDOCFLAGS`. + `COQFLAGS` is now entirely separate from `COQLIBS`, so in custom Makefiles + `$(COQFLAGS)` should be replaced by `$(COQFLAGS) $(COQLIBS)`. -- Removed the gallina utility (extracts specification from Coq vernacular files). +- Removed the `gallina` utility (extracts specification from Coq vernacular files). If you would like to maintain this tool externally, please contact us. - Removed the Emacs modes distributed with Coq. You are advised to - use Proof-General <https://proofgeneral.github.io/> (and optionally - Company-Coq <https://github.com/cpitclaudel/company-coq>) instead. + use [Proof-General](https://proofgeneral.github.io/) (and optionally + [Company-Coq](https://github.com/cpitclaudel/company-coq)) instead. If your use case is not covered by these alternative Emacs modes, please open an issue. We can help set up external maintenance as part of Proof-General, or independently as part of coq-community. - Vernacular Commands -- Removed deprecated commands Arguments Scope and Implicit Arguments - (not the option). Use the Arguments command instead. +- Removed deprecated commands `Arguments Scope` and `Implicit Arguments` + (not the option). Use the `Arguments` command instead. - Nested proofs may be enabled through the option `Nested Proofs Allowed`. By default, they are disabled and produce an error. The deprecation warning which used to occur when using nested proofs has been removed. -- Added option Uniform Inductive Parameters which abstracts over parameters +- Added option `Uniform Inductive Parameters` which abstracts over parameters before typechecking constructors, allowing to write for example `Inductive list (A : Type) := nil : list | cons : A -> list -> list.` -- New Set Hint Variables/Constants Opaque/Transparent commands for setting +- New `Set Hint Variables/Constants Opaque/Transparent` commands for setting globally the opacity flag of variables and constants in hint databases, overwritting the opacity set of the hint database. -- Added generic syntax for “attributes”, as in: +- Added generic syntax for "attributes", as in: `#[local] Lemma foo : bar.` - Added the `Numeral Notation` command for registering decimal numeral notations for custom types @@ -188,8 +187,8 @@ Vernacular Commands scope. If you want the previous behavior, use `Global Set SsrHave NoTCResolution`. - Multiple sections with the same name are allowed. -- Combined Scheme can now work when inductive schemes are generated in sort - Type. It used to be limited to sort Prop. +- `Combined Scheme` can now work when inductive schemes are generated in sort + `Type`. It used to be limited to sort `Prop`. Coq binaries and process model @@ -207,40 +206,41 @@ SSReflect - The implementation of delayed clear switches in intro patterns is now simpler to explain: - 1. The immediate effect of a clear switch like {x} is to rename the - variable x to _x_ (i.e. a reserved identifier that cannot be mentioned + 1. The immediate effect of a clear switch like `{x}` is to rename the + variable `x` to `_x_` (i.e. a reserved identifier that cannot be mentioned explicitly) - 2. The delayed effect of {x} is that _x_ is cleared at the end of the intro + 2. The delayed effect of `{x}` is that `_x_` is cleared at the end of the intro pattern - 3. A clear switch immediately before a view application like {x}/v is - translated to /v{x}. - In particular rule 3 lets one write {x}/v even if v uses the variable x: + 3. A clear switch immediately before a view application like `{x}/v` is + translated to `/v{x}`. + + In particular, the third rule lets one write `{x}/v` even if `v` uses the variable `x`: indeed the view is executed before the renaming. - An empty clear switch is now accepted in intro patterns before a view application whenever the view is a variable. - One can now write {}/v to mean {v}/v. Remark that {}/x is very similar - to the idiom {}e for the rewrite tactic (the equation e is used for + One can now write `{}/v` to mean `{v}/v`. Remark that `{}/x` is very similar + to the idiom `{}e` for the rewrite tactic (the equation `e` is used for rewriting and then discarded). Standard Library -- There are now conversions between [string] and [positive], [Z], - [nat], and [N] in binary, octal, and hex. +- There are now conversions between `string` and `positive`, `Z`, + `nat`, and `N` in binary, octal, and hex. Display diffs between proof steps -- coqtop and coqide can now highlight the differences between proof steps +- `coqtop` and `coqide` can now highlight the differences between proof steps in color. This can be enabled from the command line or the - `Set Diffs "on"|"off"|"removed"` command. Please see the documentation for + `Set Diffs "on"/"off"/"removed"` command. Please see the documentation for details. Showing diffs in Proof General requires small changes to PG (under discussion). Notations - Added `++` infix for `VectorDef.append`. - Note that this might cause incompatibilities if you have, e.g., list_scope - and vector_scope both open with vector_scope on top, and expect `++` to + Note that this might cause incompatibilities if you have, e.g., `list_scope` + and `vector_scope` both open with `vector_scope` on top, and expect `++` to refer to `app`. Solution: wrap `_ ++ _` in `(_ ++ _)%list` (or whichever scope you want). @@ -266,7 +266,7 @@ Kernel Windows installer - The Windows installer now includes many more external packages that can be -individually selected for installation. + individually selected for installation. Many other bug fixes and lots of documentation improvements (for details, see the 8.8.2 milestone at https://github.com/coq/coq/milestone/15?closed=1). @@ -276,10 +276,10 @@ Changes from 8.8.0 to 8.8.1 Kernel -- Fix a critical bug with cofixpoints and vm_compute/native_compute (#7333). +- Fix a critical bug with cofixpoints and `vm_compute`/`native_compute` (#7333). - Fix a critical bug with modules and algebraic universes (#7695) - Fix a critical bug with inlining of polymorphic constants (#7615). -- Fix a critical bug with universe polymorphism and vm_compute (#7723). Was +- Fix a critical bug with universe polymorphism and `vm_compute` (#7723). Was present since 8.5. Notations @@ -303,7 +303,7 @@ Changes from 8.8+beta1 to 8.8.0 Tools - Asynchronous proof delegation policy was fixed. Since version 8.7 - Coq was ignoring previous runs and the -async-proofs-delegation-threshold + Coq was ignoring previous runs and the `-async-proofs-delegation-threshold` option did not have the expected behavior. Tactic language @@ -39,14 +39,14 @@ WHAT DO YOU NEED ? - Findlib (version >= 1.4.1) (available at http://projects.camlcity.org/projects/findlib.html) - - Camlp5 (version >= 7.01) + - Camlp5 (version >= 7.03) (available at https://camlp5.github.io/) - GNU Make version 3.81 or later - a C compiler - - for CoqIDE, the lablgtk development files (version >= 2.18.3), + - for CoqIDE, the lablgtk development files (version >= 2.18.5), and the GTK 2.x libraries including gtksourceview2. Note that num, camlp5 and lablgtk should be properly registered with @@ -27,7 +27,7 @@ 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`](CHANGES) that explains the differences and the +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. @@ -6,13 +6,13 @@ bug-reports: "https://github.com/coq/coq/issues" dev-repo: "https://github.com/coq/coq.git" license: "LGPL-2.1" -available: [ ocaml-version >= "4.02.3" ] +available: [ ocaml-version >= "4.05.0" ] depends: [ - "dune" { build } + "dune" { build & >= "1.2.0" } "ocamlfind" { build } "num" - "camlp5" + "camlp5" { >= "7.03" } ] build-env: [ diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 5f07aa8fca..b8bea755e0 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1374,7 +1374,7 @@ function copy_coq_license { # FIXME: this is not the micromega license # It only applies to code that was copied into one single file! install -D README.md "$PREFIXCOQ/license_readme/coq/ReadMe.md" - install -D CHANGES "$PREFIXCOQ/license_readme/coq/Changes.txt" + install -D CHANGES.md "$PREFIXCOQ/license_readme/coq/Changes.md" install -D INSTALL "$PREFIXCOQ/license_readme/coq/Install.txt" install -D doc/README.md "$PREFIXCOQ/license_readme/coq/ReadMeDoc.md" || true fi diff --git a/dev/ci/README.md b/dev/ci/README.md index 24952eb5b7..7870cbb51d 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -126,7 +126,7 @@ patch (or ask someone to prepare a patch) to fix the project: developer who merges the PR on Coq. There are plans to improve this, cf. [#6724](https://github.com/coq/coq/issues/6724). -Moreover your PR must absolutely update the [`CHANGES`](../../CHANGES) file. +Moreover your PR must absolutely update the [`CHANGES.md`](../../CHANGES.md) file. Advanced GitLab CI information ------------------------------ diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 1b1aeafa0d..511eaaba9c 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -49,11 +49,12 @@ ######################################################################## # Iris ######################################################################## -: "${stdpp_CI_REF:=master}" + +# NB: stdpp and Iris refs are gotten from the opam files in the Iris +# and lambdaRust repos respectively. : "${stdpp_CI_GITURL:=https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp}" : "${stdpp_CI_ARCHIVEURL:=${stdpp_CI_GITURL}/-/archive}" -: "${Iris_CI_REF:=master}" : "${Iris_CI_GITURL:=https://gitlab.mpi-sws.org/FP/iris-coq}" : "${Iris_CI_ARCHIVEURL:=${Iris_CI_GITURL}/-/archive}" diff --git a/dev/ci/ci-iris-lambda-rust.sh b/dev/ci/ci-iris-lambda-rust.sh index 6960a8b98a..95f143bb95 100755 --- a/dev/ci/ci-iris-lambda-rust.sh +++ b/dev/ci/ci-iris-lambda-rust.sh @@ -9,13 +9,13 @@ install_ssreflect git_download lambdaRust # Extract required version of Iris -Iris_REF=$(grep -F coq-iris < "${CI_BUILD_DIR}/lambdaRust/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/') +Iris_CI_REF=$(grep -F coq-iris < "${CI_BUILD_DIR}/lambdaRust/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/') # Setup Iris git_download Iris # Extract required version of std++ -stdpp_REF=$(grep -F coq-stdpp < "${CI_BUILD_DIR}/Iris/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/') +stdpp_CI_REF=$(grep -F coq-stdpp < "${CI_BUILD_DIR}/Iris/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/') # Setup std++ git_download stdpp diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index fcfa591ce1..f257c62dd3 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2018-09-25-V1" +# CACHEKEY: "bionic_coq-V2018-10-04-V2" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -41,7 +41,7 @@ ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.2.1 ounit.2.0.8 odoc.1.2.0" \ CI_OPAM="menhir.20180530 elpi.1.1.0 ocamlgraph.1.8.8" # BASE switch; CI_OPAM contains Coq's CI dependencies. -ENV CAMLP5_VER="7.01" \ +ENV CAMLP5_VER="7.03" \ COQIDE_OPAM="lablgtk.2.18.5 conf-gtksourceview.2" # base switch diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md index c0cd9c8cdd..000f21c254 100644 --- a/dev/doc/MERGING.md +++ b/dev/doc/MERGING.md @@ -54,7 +54,7 @@ those external projects should have been prepared (cf. the relevant sub-section in the [CI README](../ci/README.md#Breaking-changes) and the PR can be tested with these fixes thanks to ["overlays"](../ci/user-overlays/README.md). -Moreover the PR must absolutely update the [`CHANGES`](../../CHANGES) file. +Moreover the PR must absolutely update the [`CHANGES.md`](../../CHANGES.md) file. If overlays are missing, ask the author to prepare them and label the PR with the [needs: overlay](https://github.com/coq/coq/labels/needs%3A%20overlay) label. @@ -93,7 +93,7 @@ When the PR has conflicts, the assignee can either: In both cases, CI should be run again. -In some rare cases (e.g. the conflicts are in the CHANGES file), it is ok to fix +In some rare cases (e.g. the conflicts are in the `CHANGES.md` file), it is ok to fix the conflicts in the merge commit (following the same steps as below), and push to `master` directly. Don't use the GitHub interface to fix these conflicts. diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 5371d84a06..d6d296f012 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -2,11 +2,6 @@ ### ML API -Termops: - -- Internal printing functions have been placed under the - `Termops.Internal` namespace. - Names - Kernel names no longer contain a section path. They now have only two @@ -27,8 +22,8 @@ Names - In `Libnames`, the type `reference` and its two constructors `Qualid` and `Ident` have been removed in favor of `qualid`. `Qualid` is now the identity, `Ident` can be replaced by `qualid_of_ident`. Matching over `reference` can be - replaced by a test using `qualid_is_ident`. Extracting the ident part of a - qualid can be done using `qualid_basename`. + replaced by a test using `qualid_is_ident`. Extracting the `ident` part of a + `qualid` can be done using `qualid_basename`. Misctypes @@ -62,20 +57,20 @@ Proof engine ML Libraries used by Coq -- Introduction of a "Smart" module for collecting "smart*" functions, e.g. - Array.Smart.map. -- Uniformization of some names, e.g. Array.Smart.fold_left_map instead - of Array.smartfoldmap. +- Introduction of a `Smart` module for collecting `smart*` functions, e.g. + `Array.Smart.map`. +- Uniformization of some names, e.g. `Array.Smart.fold_left_map` instead + of `Array.smartfoldmap`. Printer.ml API -- The mechanism in Printer that allowed dynamically overriding pr_subgoals, - pr_subgoal and pr_goal was removed to simplify the code. It was - earlierly used by PCoq. +- The mechanism in `Printer` that allowed dynamically overriding `pr_subgoals`, + `pr_subgoal` and `pr_goal` was removed to simplify the code. It was + earlier used by PCoq. Kernel - The following renamings happened: +- The following renamings happened: - `Context.Rel.t` into `Constr.rel_context` - `Context.Named.t` into `Constr.named_context` - `Context.Compacted.t` into `Constr.compacted_context` @@ -104,19 +99,24 @@ Vernacular commands Primitive number parsers -- For better modularity, the primitive parsers for positive, N and Z - have been split over three files (plugins/syntax/positive_syntax.ml, - plugins/syntax/n_syntax.ml, plugins/syntax/z_syntax.ml). +- For better modularity, the primitive parsers for `positive`, `N` and `Z` + have been split over three files (`plugins/syntax/positive_syntax.ml`, + `plugins/syntax/n_syntax.ml`, `plugins/syntax/z_syntax.ml`). Parsing -- Manual uses of the Pcoq.Gram module have been deprecated. Wrapper modules - Pcoq.Entry and Pcoq.Parsable were introduced to replace it. +- Manual uses of the `Pcoq.Gram` module have been deprecated. Wrapper modules + `Pcoq.Entry` and `Pcoq.Parsable` were introduced to replace it. + +Termops + +- Internal printing functions have been placed under the + `Termops.Internal` namespace. ### Unit testing - The test suite now allows writing unit tests against OCaml code in the Coq - code base. Those unit tests create a dependency on the OUnit test framework. +The test suite now allows writing unit tests against OCaml code in the Coq +code base. Those unit tests create a dependency on the OUnit test framework. ### Transitioning away from Camlp5 @@ -151,7 +151,7 @@ let myval = 0 Steps to perform: - replace the brackets enclosing OCaml code in actions with braces -- if not there yet, add a leading `|̀ to the first rule +- if not there yet, add a leading `|` to the first rule For instance, code of the form: ``` @@ -182,8 +182,8 @@ Most plugin writers do not need this low-level interface, but for the sake of completeness we document it. Steps to perform are: -- replace GEXTEND with GRAMMAR EXTEND -- wrap every occurrence of OCaml code in actions into braces { } +- replace `GEXTEND` with `GRAMMAR EXTEND` +- wrap every occurrence of OCaml code in actions into braces `{ }` For instance, code of the form ``` @@ -233,7 +233,7 @@ All the other bugs kept their number. General deprecation -- All functions marked [@@ocaml.deprecated] in 8.7 have been +- All functions marked `[@@ocaml.deprecated]` in 8.7 have been removed. Please, make sure your plugin is warning-free in 8.7 before trying to port it over 8.8. @@ -261,8 +261,8 @@ We changed the type of the following functions: - `Global.body_of_constant`: same as above. -- `Constrinterp.*` generally, many functions that used to take an - `evar_map ref` have been now switched to functions that will work in +- `Constrinterp.*`: generally, many functions that used to take an + `evar_map ref` have now been switched to functions that will work in a functional way. The old style of passing `evar_map`s as references is not supported anymore. @@ -280,16 +280,16 @@ We have changed the representation of the following types: Some tactics and related functions now support static configurability, e.g.: -- injectable, dEq, etc. takes an argument ~keep_proofs which, - - if None, tells to behave as told with the flag Keep Proof Equalities - - if Some b, tells to keep proof equalities iff b is true +- `injectable`, `dEq`, etc. take an argument `~keep_proofs` which, + - if `None`, tells to behave as told with the flag `Keep Proof Equalities` + - if `Some b`, tells to keep proof equalities iff `b` is true Declaration of printers for arguments used only in vernac command -- It should now use "declare_extra_vernac_genarg_pprule" rather than - "declare_extra_genarg_pprule", otherwise, a failure at runtime might +- It should now use `declare_extra_vernac_genarg_pprule` rather than + `declare_extra_genarg_pprule`, otherwise, a failure at runtime might happen. An alternative is to register the corresponding argument as - a value, using "Geninterp.register_val0 wit None". + a value, using `Geninterp.register_val0 wit None`. Types Alias deprecation and type relocation. @@ -332,7 +332,7 @@ functions when some given constants are traversed: * `declare_reduction_effect`: to declare a hook to be applied when some constant are visited during the execution of some reduction functions - (primarily cbv). + (primarily `cbv`). * `set_reduction_effect`: to declare a constant on which a given effect hook should be called. diff --git a/doc/sphinx/credits-contents.rst b/doc/sphinx/credits-contents.rst index 212f0a65b0..d1df0657aa 100644 --- a/doc/sphinx/credits-contents.rst +++ b/doc/sphinx/credits-contents.rst @@ -1238,7 +1238,7 @@ of integers and real constants are now represented using `IZR` (work by Guillaume Melquiond). Standard library additions and improvements by Jason Gross, Pierre Letouzey and -others, documented in the `CHANGES` file. +others, documented in the ``CHANGES.md`` file. The mathematical proof language/declarative mode plugin was removed from the archive. @@ -1352,7 +1352,7 @@ version. Version 8.8 also comes with a bunch of smaller-scale changes and improvements regarding the different components of the system. -Most important ones are documented in the ``CHANGES`` file. +Most important ones are documented in the ``CHANGES.md`` file. The efficiency of the whole system has seen improvements thanks to contributions from Gaëtan Gilbert, Pierre-Marie Pédrot, Maxime Dénès and diff --git a/ide/coqide.opam b/ide/coqide.opam index ba05b9edcf..897177b283 100644 --- a/ide/coqide.opam +++ b/ide/coqide.opam @@ -6,14 +6,16 @@ bug-reports: "https://github.com/coq/coq/issues" dev-repo: "https://github.com/coq/coq.git" license: "LGPL-2.1" -available: [ocaml-version >= "4.02.3"] +available: [ocaml-version >= "4.05.0"] depends: [ - "dune" { build } - "ocamlfind" { build } - "num" - "camlp5" + "dune" { build & >= "1.2.0" } "coq" + "conf-gtksourceview" + "lablgtk" { >= "2.18.5" } ] +build-env: [ + [ COQ_CONFIGURE_PREFIX = "%{prefix}" ] +] build: [ [ "dune" "build" "-p" name "-j" jobs ] ] diff --git a/ide/dune-workspace b/ide/dune-workspace new file mode 100644 index 0000000000..38875eac2c --- /dev/null +++ b/ide/dune-workspace @@ -0,0 +1,6 @@ +(lang dune 1.2) + +; Add custom flags here. Default developer profile is `dev` +(env + (dev (flags :standard -rectypes -w -9-27-50+60)) + (release (flags :standard -rectypes))) diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 23d0536df8..d5f0b7bff6 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -526,6 +526,14 @@ let mkAppC (f,l) = | CApp (g,l') -> CAst.make @@ CApp (g, l' @ l) | _ -> CAst.make @@ CApp ((None, f), l) +let mkProdCN ?loc bll c = + if bll = [] then c else + CAst.make ?loc @@ CProdN (bll,c) + +let mkLambdaCN ?loc bll c = + if bll = [] then c else + CAst.make ?loc @@ CLambdaN (bll,c) + let mkCProdN ?loc bll c = CAst.make ?loc @@ CProdN (bll,c) diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index 61e8aa1b51..9e83bde8b2 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -38,22 +38,36 @@ val constr_loc : constr_expr -> Loc.t option val cases_pattern_expr_loc : cases_pattern_expr -> Loc.t option val local_binders_loc : local_binder_expr list -> Loc.t option -(** {6 Constructors}*) +(** {6 Constructors} *) + +(** {7 Term constructors} *) + +(** Basic form of the corresponding constructors *) val mkIdentC : Id.t -> constr_expr val mkRefC : qualid -> constr_expr -val mkAppC : constr_expr * constr_expr list -> constr_expr val mkCastC : constr_expr * constr_expr Glob_term.cast_type -> constr_expr val mkLambdaC : lname list * binder_kind * constr_expr * constr_expr -> constr_expr val mkLetInC : lname * constr_expr * constr_expr option * constr_expr -> constr_expr val mkProdC : lname list * binder_kind * constr_expr * constr_expr -> constr_expr -val mkCLambdaN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_expr -(** Same as [abstract_constr_expr], with location *) +val mkAppC : constr_expr * constr_expr list -> constr_expr +(** Basic form of application, collapsing nested applications *) +(** Optimized constructors: does not add a constructor for an empty binder list *) + +val mkLambdaCN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_expr +val mkProdCN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_expr + +(** Aliases for the corresponding constructors; generally [mkLambdaCN] and + [mkProdCN] should be preferred *) + +val mkCLambdaN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_expr val mkCProdN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_expr -(** Same as [prod_constr_expr], with location *) +(** {7 Pattern constructors} *) + +(** Interpretation of a list of patterns as a disjunctive pattern (optimized) *) val mkCPatOr : ?loc:Loc.t -> cases_pattern_expr list -> cases_pattern_expr val mkAppPattern : ?loc:Loc.t -> cases_pattern_expr -> cases_pattern_expr list -> cases_pattern_expr diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index 7cb5af787b..e25f7aa54f 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -249,20 +249,20 @@ GRAMMAR EXTEND Gram record_field_declaration: [ [ id = global; bl = binders; ":="; c = lconstr -> - { (id, if bl = [] then c else mkCLambdaN ~loc bl c) } ] ] + { (id, mkLambdaCN ~loc bl c) } ] ] ; binder_constr: [ [ "forall"; bl = open_binders; ","; c = operconstr LEVEL "200" -> - { mkCProdN ~loc bl c } + { mkProdCN ~loc bl c } | "fun"; bl = open_binders; "=>"; c = operconstr LEVEL "200" -> - { mkCLambdaN ~loc bl c } + { mkLambdaCN ~loc bl c } | "let"; id=name; bl = binders; ty = type_cstr; ":="; c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> { let ty,c1 = match ty, c1 with | (_,None), { CAst.v = CCast(c, CastConv t) } -> (Loc.tag ?loc:(constr_loc t) @@ Some t), c (* Tolerance, see G_vernac.def_body *) | _, _ -> ty, c1 in - CAst.make ~loc @@ CLetIn(id,mkCLambdaN ?loc:(constr_loc c1) bl c1, - Option.map (mkCProdN ?loc:(fst ty) bl) (snd ty), c2) } + CAst.make ~loc @@ CLetIn(id,mkLambdaCN ?loc:(constr_loc c1) bl c1, + Option.map (mkProdCN ?loc:(fst ty) bl) (snd ty), c2) } | "let"; fx = single_fix; "in"; c = operconstr LEVEL "200" -> { let fixp = mk_single_fix fx in let { CAst.loc = li; v = id } = match fixp.CAst.v with diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 750ed35cbc..9497f2fb03 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -84,8 +84,7 @@ match local with in (gr,inst,Lib.is_modtype_strict ()) -let interp_assumption sigma env impls bl c = - let c = mkCProdN ?loc:(local_binders_loc bl) bl c in +let interp_assumption sigma env impls c = let sigma, (ty, impls) = interp_type_evars_impls env sigma ~impls c in sigma, (ty, impls) @@ -148,7 +147,7 @@ let do_assumptions kind nl l = in (* We intepret all declarations in the same evar_map, i.e. as a telescope. *) let (sigma,_,_),l = List.fold_left_map (fun (sigma,env,ienv) (is_coe,(idl,c)) -> - let sigma,(t,imps) = interp_assumption sigma env ienv [] c in + let sigma,(t,imps) = interp_assumption sigma env ienv c in let env = EConstr.push_named_context (List.map (fun {CAst.v=id} -> LocalAssum (id,t)) idl) env in let ienv = List.fold_right (fun {CAst.v=id} ienv -> diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index cf69a84b8b..895737b538 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -296,7 +296,7 @@ GRAMMAR EXTEND Gram { if List.exists (function CLocalPattern _ -> true | _ -> false) bl then (* FIXME: "red" will be applied to types in bl and Cast with remain *) - let c = mkCLambdaN ~loc bl c in + let c = mkLambdaCN ~loc bl c in DefineBody ([], red, c, None) else (match c with @@ -308,7 +308,7 @@ GRAMMAR EXTEND Gram then (* FIXME: "red" will be applied to types in bl and Cast with remain *) let c = CAst.make ~loc @@ CCast (c, CastConv t) in - (([],mkCLambdaN ~loc bl c), None) + (([],mkLambdaCN ~loc bl c), None) else ((bl, c), Some t) in DefineBody (bl, red, c, tyo) } @@ -419,16 +419,16 @@ GRAMMAR EXTEND Gram ; record_binder_body: [ [ l = binders; oc = of_type_with_opt_coercion; - t = lconstr -> { fun id -> (oc,AssumExpr (id,mkCProdN ~loc l t)) } + t = lconstr -> { fun id -> (oc,AssumExpr (id,mkProdCN ~loc l t)) } | l = binders; oc = of_type_with_opt_coercion; t = lconstr; ":="; b = lconstr -> { fun id -> - (oc,DefExpr (id,mkCLambdaN ~loc l b,Some (mkCProdN ~loc l t))) } + (oc,DefExpr (id,mkLambdaCN ~loc l b,Some (mkProdCN ~loc l t))) } | l = binders; ":="; b = lconstr -> { fun id -> match b.CAst.v with | CCast(b', (CastConv t|CastVM t|CastNative t)) -> - (None,DefExpr(id,mkCLambdaN ~loc l b',Some (mkCProdN ~loc l t))) + (None,DefExpr(id,mkLambdaCN ~loc l b',Some (mkProdCN ~loc l t))) | _ -> - (None,DefExpr(id,mkCLambdaN ~loc l b,None)) } ] ] + (None,DefExpr(id,mkLambdaCN ~loc l b,None)) } ] ] ; record_binder: [ [ id = name -> { (None,AssumExpr(id, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))) } @@ -448,9 +448,9 @@ GRAMMAR EXTEND Gram constructor_type: [[ l = binders; t= [ coe = of_type_with_opt_coercion; c = lconstr -> - { fun l id -> (not (Option.is_empty coe),(id,mkCProdN ~loc l c)) } + { fun l id -> (not (Option.is_empty coe),(id,mkProdCN ~loc l c)) } | -> - { fun l id -> (false,(id,mkCProdN ~loc l (CAst.make ~loc @@ CHole (None, IntroAnonymous, None)))) } ] + { fun l id -> (false,(id,mkProdCN ~loc l (CAst.make ~loc @@ CHole (None, IntroAnonymous, None)))) } ] -> { t l } ]] ; |