From 8364c3e17800deb6c6eff0219d80880d9c6790ff Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 12 Aug 2024 10:33:05 +1000 Subject: [PATCH] chore: begin development cycle for v4.12.0 (#4986) --- RELEASES.md | 6 ++- doc/dev/release_checklist.md | 4 +- releases_drafts/mutualStructural.md | 65 ----------------------------- src/CMakeLists.txt | 2 +- 4 files changed, 9 insertions(+), 68 deletions(-) delete mode 100644 releases_drafts/mutualStructural.md diff --git a/RELEASES.md b/RELEASES.md index 6e610a987f..7d8a0c41b1 100644 --- a/RELEASES.md +++ b/RELEASES.md @@ -8,10 +8,14 @@ This file contains work-in-progress notes for the upcoming release, as well as p Please check the [releases](https://github.com/leanprover/lean4/releases) page for the current status of each version. -v4.11.0 +v4.12.0 ---------- Development in progress. +v4.11.0 +---------- +Release candidate, release notes will be copied from the branch `releases/v4.11.0` once completed. + v4.10.0 ---------- diff --git a/doc/dev/release_checklist.md b/doc/dev/release_checklist.md index e095f3d067..27e039499b 100644 --- a/doc/dev/release_checklist.md +++ b/doc/dev/release_checklist.md @@ -192,7 +192,7 @@ We'll use `v4.7.0-rc1` as the intended release version in this example. finalized release notes from the `releases/v4.6.0` branch. - Replaces the "development in progress" in the `v4.7.0` section of `RELEASES.md` with ``` - Release candidate, release notes will be copied from `branch releases/v4.7.0` once completed. + Release candidate, release notes will be copied from the branch `releases/v4.7.0` once completed. ``` and inserts the following section before that section: ``` @@ -201,6 +201,8 @@ We'll use `v4.7.0-rc1` as the intended release version in this example. Development in progress. ``` - Removes all the entries from the `./releases_drafts/` folder. + - Titled "chore: begin development cycle for v4.8.0" + ## Time estimates: Slightly longer than the corresponding steps for a stable release. diff --git a/releases_drafts/mutualStructural.md b/releases_drafts/mutualStructural.md deleted file mode 100644 index a1efee9f5d..0000000000 --- a/releases_drafts/mutualStructural.md +++ /dev/null @@ -1,65 +0,0 @@ -* Structural recursion can now be explicitly requested using - ``` - termination_by structural x - ``` - in analogy to the existing `termination_by x` syntax that causes well-founded recursion to be used. - (#4542) - -* The `termination_by?` syntax no longer forces the use of well-founded recursion, and when structural - recursion is inferred, will print the result using the `termination_by` syntax. - -* Mutual structural recursion is supported now. This supports both mutual recursion over a non-mutual - data type, as well as recursion over mutual or nested data types: - - ```lean - mutual - def Even : Nat → Prop - | 0 => True - | n+1 => Odd n - - def Odd : Nat → Prop - | 0 => False - | n+1 => Even n - end - - mutual - inductive A - | other : B → A - | empty - inductive B - | other : A → B - | empty - end - - mutual - def A.size : A → Nat - | .other b => b.size + 1 - | .empty => 0 - - def B.size : B → Nat - | .other a => a.size + 1 - | .empty => 0 - end - - inductive Tree where | node : List Tree → Tree - - mutual - def Tree.size : Tree → Nat - | node ts => Tree.list_size ts - - def Tree.list_size : List Tree → Nat - | [] => 0 - | t::ts => Tree.size t + Tree.list_size ts - end - ``` - - Functional induction principles are generated for these functions as well (`A.size.induct`, `A.size.mutual_induct`). - - Nested structural recursion is still not supported. - - PRs #4639, #4715, #4642, #4656, #4684, #4715, #4728, #4575, #4731, #4658, #4734, #4738, #4718, - #4733, #4787, #4788, #4789, #4807, #4772 - -* A bugfix in the structural recursion code may in some cases break existing code, when a parameter - of the type of the recursive argument is bound behind indices of that type. This can usually be - fixed by reordering the parameters of the function (PR #4672) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 0699177388..ad4df96ea2 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -10,7 +10,7 @@ endif() include(ExternalProject) project(LEAN CXX C) set(LEAN_VERSION_MAJOR 4) -set(LEAN_VERSION_MINOR 11) +set(LEAN_VERSION_MINOR 12) set(LEAN_VERSION_PATCH 0) set(LEAN_VERSION_IS_RELEASE 0) # This number is 1 in the release revision, and 0 otherwise. set(LEAN_SPECIAL_VERSION_DESC "" CACHE STRING "Additional version description like 'nightly-2018-03-11'")