diff options
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/case-repr.md | 122 | ||||
| -rw-r--r-- | dev/doc/changes.md | 5 | ||||
| -rw-r--r-- | dev/doc/release-process.md | 43 |
3 files changed, 154 insertions, 16 deletions
diff --git a/dev/doc/case-repr.md b/dev/doc/case-repr.md new file mode 100644 index 0000000000..e1a78797bd --- /dev/null +++ b/dev/doc/case-repr.md @@ -0,0 +1,122 @@ +## Case representation + +Starting from Coq 8.14, the term representation of pattern-matching uses a +so-called *compact form*. Compared to the previous representation, the major +difference is that all type and term annotations on lambda and let abstractions +that were present in branches and return clause of pattern-matchings were +removed. In order to keep the ability to construct the old expanded form out of +the new compact form, the case node also makes explicit data that was stealthily +present in the expanded return clause, namely universe instances and parameters +of the inductive type being eliminated. + +### ML Representation + +The case node now looks like +``` +Case of + case_info * + Instance.t * (* universe instances of the inductive *) + constr array * (* parameters of the inductive *) + case_return * (* erased return clause *) + case_invert * (* SProp inversion data *) + constr * (* scrutinee *) + case_branch array (* erased branches *) +``` +where +``` +type case_branch = Name.t binder_annot array * constr +type case_return = Name.t binder_annot array * types +``` + +For comparison, pre-8.14 case nodes were defined as follows. +``` +Case of + case_info * + constr * (* annotated return clause *) + case_invert * (* SProp inversion data *) + constr * (* scrutinee *) + constr array (* annotated branches *) +``` + +### Typing Rules and Invariants + +Disregarding the `case_info` cache and the SProp inversion, the typing rules for +the case node can be given as follows. + +Provided +- Γ ⊢ c : Ind@{u} pms Indices +- Inductive Ind@{i} Δ : forall Θ, Type := cᵢ : forall Ξᵢ, Ind Δ Aᵢ +- Γ, Θ@{i := u}{Δ := pms} ⊢ p : Type +- Γ, Ξᵢ@{i := u}{Δ := pms} ⊢ snd brᵢ : p{Θ := Aᵢ{Δ := pms}} + +Then Γ ⊢ Case (_, u, pms, ( _, p), _, c, br) : p{Θ := Indices} + +In particular, this implies that Γ ⊢ pms : Δ@{i := u}. Parameters are stored in +the same order as in the application node. + +The u universe instance must be a valid instance for the corresponding +inductive type, in particular their length must coincide. + +The `Name.t binder_annot array` appearing both in the return clause and +in the branches must satisfy these invariants: +- For branches, it must have the same length as the corresponding Ξᵢ context +(including let-ins) +- For the return clause, it must have the same length as the context +Θ, self : Ind@{u} pms Θ (including let-ins). The last variable appears as +the term being destructed and corresponds to the variable introduced by the +"as" clause of the user-facing syntax. +- The relevance annotations must match with the corresponding sort of the +variable from the context. + +Note that the annotated variable array is reversed w.r.t. the context, +i.e. variables appear left to right as in standard practice. + +Let-bindings can appear in Δ, Θ or Ξᵢ, since they are arbitrary +contexts. As a general rule, let bindings appear as binders but not as +instances. That is, they MUST appear in the variable array, but they MUST NOT +appear in the parameter array. + +Example: +``` +Inductive foo (X := tt) : forall (Y := X), Type := Foo : forall (Z := X), foo. + +Definition case (x : foo) : unit := match x as x₀ in foo with Foo _ z => z end +``` +The case node of the `case` function is represented as +``` +Case ( + _, + Instance.empty, + [||], + ([|(Y, Relevant); (x₀, Relevant)|], unit), (* let (Y := tt) in fun (x₀ : foo) => unit *) + NoInvert, + #1, + [| + ([|(z, Relevant)|], #1) (* let z := tt in z *) + |] +) +``` + +This choice of representation for let-bindings requires access to the +environment in some cases, e.g. to compute branch reduction. There is a +fast-path for non-let-containing inductive types though, which are the vast +majority. + +### Porting plugins + +The conversion functions from and to the expanded form are: +- `[Inductive, EConstr].expand_case` which goes from the compact to the expanded +form and cannot fail (assuming the term was well-typed) +- `[Inductive, EConstr].contract_case` which goes the other way and will +raise anomalies if the expanded forms are not fully eta-expanded. + +As such, it is always painless to convert to the old representation. Converting +the other way, you must ensure that all the terms you provide the +compatibility function with are fully eta-expanded, **including let-bindings**. +This works as expected for the common case with eta-expanded branches but will +fail for plugins that generate non-eta-expanded branches. + +Some other useful variants of these functions are: +- `Inductive.expand_case_specif` +- `EConstr.annotate_case` +- `EConstr.expand_branch` diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 5adeafaa38..26c4b01c9f 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -37,6 +37,11 @@ Dumpglob: plugins to temporarily change/pause the output of Dumpglob, and then restore it to the original setting. +Glob_term: + +- Removing useless `binding_kind` argument of `GLocalDef` in + `extended_glob_local_binder`. + ## Changes between Coq 8.11 and Coq 8.12 ### Code formatting diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md index bb766d02ea..64053a62f9 100644 --- a/dev/doc/release-process.md +++ b/dev/doc/release-process.md @@ -113,15 +113,14 @@ in time. Coq has been tagged. - [ ] Have some people test the recently auto-generated Windows and MacOS packages. -- [ ] In a PR: +- [ ] In a PR against `vX.X` (for testing): - Change the version name from alpha to beta1 (see [#7009](https://github.com/coq/coq/pull/7009/files)). - We generally do not update the magic numbers at this point. - Set `is_a_released_version` to `true` in `configure.ml`. - [ ] Put the `VX.X+beta1` tag using `git tag -s`. -- [ ] Check using `git push --tags --dry-run` that you are not - pushing anything else than the new tag. If needed, remove spurious - tags with `git tag -d`. When this is OK, proceed with `git push --tags`. +- [ ] Push the new tag with `git push upstream VX.X+beta1 --dry-run` + (remove the `--dry-run` and redo if all looks OK). - [ ] Set `is_a_released_version` to `false` in `configure.ml` (if you forget about it, you'll be reminded whenever you try to backport a PR with a changelog entry). @@ -137,29 +136,29 @@ in time. - [ ] Draft a release on GitHub. - [ ] Sign the Windows and MacOS packages and upload them on GitHub. + The Windows packages must be signed by the Inria IT security service. They - should be sent as a link to the binary together with its SHA256 hash in a - signed e-mail, via our local contact (currently `@maximedenes`). - + The MacOS packages should be signed by our own certificate, by sending them - to `@maximedenes`. A detailed step-by-step guide can be found [on the wiki](https://github.com/coq/coq/wiki/SigningReleases). + should be sent as a link to the binary (via [filesender](https://filesender.renater.fr) for example) + together with its SHA256 hash in a signed e-mail to `dsi.securite` @ `inria.fr` + putting `@maximedenes` in carbon copy. + + The MacOS packages should be signed with our own certificate. A detailed step-by-step guide can be found [on the wiki](https://github.com/coq/coq/wiki/SigningReleases). +- [ ] Upload the PDF version of the reference manual to the GitHub release. (*TODO:* automate this.) - [ ] Prepare a page of news on the website with the link to the GitHub release (see [coq/www#63](https://github.com/coq/www/pull/63)). -- [ ] Upload the new version of the reference manual to the website. - *TODO: setup some continuous deployment for this.* - [ ] Merge the website update, publish the release - and send announcement e-mails. + and send announcement e-mails, typically on + the `coq-club@inria.fr` mailing list and the discourse forum + ([posting by mail](https://github.com/coq/coq/wiki/Discourse)) - [ ] Close the milestone ## At the final release time ## - [ ] Prepare the release notes (see above) -- [ ] In a PR: +- [ ] In a PR against `vX.X` (for testing): - Change the version name from X.X.0 and the magic numbers (see [#7271](https://github.com/coq/coq/pull/7271/files)). - Set `is_a_released_version` to `true` in `configure.ml`. - [ ] Put the `VX.X.0` tag. -- [ ] Check using `git push --tags --dry-run` that you are not - pushing anything else than the new tag. If needed, remove spurious - tags with `git tag -d`. When this is OK, proceed with `git push --tags`. +- [ ] Push the new tag with `git push upstream VX.X.0 --dry-run` + (remove the `--dry-run` and redo if all looks OK). - [ ] Set `is_a_released_version` to `false` in `configure.ml` (if you forget about it, you'll be reminded whenever you try to backport a PR with a changelog entry). @@ -169,7 +168,19 @@ Repeat the generic process documented above for all releases. Ping `@Zimmi48` to: - [ ] Switch the default version of the reference manual on the website. -- [ ] Publish a new version on Zenodo. + + This is done by logging into the server (`vps697916.ovh.net`), + editing two `ProxyPass` lines (one for the refman and one for the + stdlib doc) with `sudo vim /etc/apache2/sites-available/000-coq.inria.fr.conf`, + then running `sudo systemctl reload apache2`. + + *TODO:* automate this or make it doable through the `www` git + repository. See [coq/www#111](https://github.com/coq/www/issues/111) + and [coq/www#131](https://github.com/coq/www/issues/131). + +- [ ] Publish a new version on Zenodo (only once per major version). + + *TODO:* automate this with coqbot. ## At the patch-level release time ## |