From a40bcee14f5d496aedc9d191bc9494dae7e0da2c Mon Sep 17 00:00:00 2001 From: Violetta Sim <38787503+eyihluyc@users.noreply.github.com> Date: Mon, 3 Feb 2025 16:18:08 -0700 Subject: [PATCH 1/4] doc: add highlights section to v4.16.0 release notes (#6925) This PR adds the highlights section to v4.16.0 release notes. --------- Co-authored-by: Joachim Breitner Co-authored-by: David Thrane Christiansen Co-authored-by: Kim Morrison --- releases/v4.16.0.md | 110 ++++++++++++++++++++++---------------------- 1 file changed, 56 insertions(+), 54 deletions(-) diff --git a/releases/v4.16.0.md b/releases/v4.16.0.md index ee821d83697b..40a08ae58854 100644 --- a/releases/v4.16.0.md +++ b/releases/v4.16.0.md @@ -1,15 +1,10 @@ v4.16.0 ---------- +## Highlights -## Language - -* [#3696](https://github.com/leanprover/lean4/pull/3696) makes all message constructors handle pretty printer errors. - -* [#4460](https://github.com/leanprover/lean4/pull/4460) runs all linters for a single command (together) on a separate -thread from further elaboration, making a first step towards -parallelizing the elaborator. +### Unique `sorry`s -* [#5757](https://github.com/leanprover/lean4/pull/5757) makes it harder to create "fake" theorems about definitions that +[#5757](https://github.com/leanprover/lean4/pull/5757) makes it harder to create "fake" theorems about definitions that are stubbed-out with `sorry` by ensuring that each `sorry` is not definitionally equal to any other. For example, this now fails: ```lean @@ -34,10 +29,9 @@ definition" on `sorry` in the Infoview, which brings you to its origin. The option `set_option pp.sorrySource true` causes the pretty printer to show source position information on sorries. -* [#6123](https://github.com/leanprover/lean4/pull/6123) ensures that the configuration in `Simp.Config` is used when -reducing terms and checking definitional equality in `simp`. +### Separators in numeric literals -* [#6204](https://github.com/leanprover/lean4/pull/6204) lets `_` be used in numeric literals as a separator. For +[#6204](https://github.com/leanprover/lean4/pull/6204) lets `_` be used in numeric literals as a separator. For example, `1_000_000`, `0xff_ff` or `0b_10_11_01_00`. New lexical syntax: ```text numeral10 : [0-9]+ ("_"+ [0-9]+)* @@ -47,6 +41,50 @@ numeral16 : "0" [xX] ("_"* hex_char+)+ float : numeral10 "." numeral10? [eE[+-]numeral10] ``` +### Additional new featues + +* [#6300](https://github.com/leanprover/lean4/pull/6300) adds the `debug.proofAsSorry` option. When enabled, the proofs +of theorems are ignored and replaced with `sorry`. + +* [#6362](https://github.com/leanprover/lean4/pull/6362) adds the `--error=kind` option (shorthand: `-Ekind`) to the +`lean` CLI. When set, messages of `kind` (e.g., +`linter.unusedVariables`) will be reported as errors. This setting does +nothing in interactive contexts (e.g., the server). + +* [#6366](https://github.com/leanprover/lean4/pull/6366) adds support for `Float32` and fixes a bug in the runtime. + +### Library updates + +The Lean 4 library saw many changes that improve arithmetic reasoning, enhance data structure APIs, +and refine library organization. Key changes include better support for bitwise operations, shifts, +and conversions, expanded lemmas for `Array`, `Vector`, and `List`, and improved ordering definitions. +Some modules have been reorganized for clarity, and internal refinements ensure greater consistency and correctness. + +### Breaking changes + +[#6330](https://github.com/leanprover/lean4/pull/6330) removes unnecessary parameters from the functional induction +principles. This is a breaking change; broken code can typically be adjusted +simply by passing fewer parameters. + +_This highlights section was contributed by Violetta Sim._ + +For this release, 201 changes landed. In addition to the 74 feature additions and 44 fixes listed below there were 7 refactoring changes, 5 documentation improvements and 62 chores. + +## Language + +* [#3696](https://github.com/leanprover/lean4/pull/3696) makes all message constructors handle pretty printer errors. + +* [#4460](https://github.com/leanprover/lean4/pull/4460) runs all linters for a single command (together) on a separate +thread from further elaboration, making a first step towards +parallelizing the elaborator. + +* [#5757](https://github.com/leanprover/lean4/pull/5757), see the highlights section above for details. + +* [#6123](https://github.com/leanprover/lean4/pull/6123) ensures that the configuration in `Simp.Config` is used when +reducing terms and checking definitional equality in `simp`. + +* [#6204](https://github.com/leanprover/lean4/pull/6204), see the highlights section above for details. + * [#6270](https://github.com/leanprover/lean4/pull/6270) fixes a bug that could cause the `injectivity` tactic to fail in reducible mode, which could cause unfolding lemma generation to fail (used by tactics such as `unfold`). In particular, @@ -70,23 +108,13 @@ speedups on problems with lots of variables. * [#6295](https://github.com/leanprover/lean4/pull/6295) sets up simprocs for all the remaining operations defined in `Init.Data.Fin.Basic` -* [#6300](https://github.com/leanprover/lean4/pull/6300) adds the `debug.proofAsSorry` option. When enabled, the proofs -of theorems are ignored and replaced with `sorry`. +* [#6300](https://github.com/leanprover/lean4/pull/6300), see the highlights section above for details. -* [#6330](https://github.com/leanprover/lean4/pull/6330) removes unnecessary parameters from the funcion induction -principles. This is a breaking change; broken code can typically be adjusted -simply by passing fewer parameters. +* [#6330](https://github.com/leanprover/lean4/pull/6330), see the highlights section above for details. -* [#6330](https://github.com/leanprover/lean4/pull/6330) removes unnecessary parameters from the funcion induction -principles. This is a breaking change; broken code can typically be adjusted -simply by passing fewer parameters. +* [#6362](https://github.com/leanprover/lean4/pull/6362), see the highlights section above for details. -* [#6362](https://github.com/leanprover/lean4/pull/6362) adds the `--error=kind` option (shorthand: `-Ekind`) to the -`lean` CLI. When set, messages of `kind` (e.g., -`linter.unusedVariables`) will be reported as errors. This setting does -nothing in interactive contexts (e.g., the server). - -* [#6366](https://github.com/leanprover/lean4/pull/6366) adds support for `Float32` and fixes a bug in the runtime. +* [#6366](https://github.com/leanprover/lean4/pull/6366), see the highlights section above for details. * [#6375](https://github.com/leanprover/lean4/pull/6375) fixes a bug in the simplifier. It was producing terms with loose bound variables when eliminating unused `let_fun` expressions. @@ -280,8 +308,7 @@ tactic. * [#6490](https://github.com/leanprover/lean4/pull/6490) adds basic configuration options for the `grind` tactic. * [#6492](https://github.com/leanprover/lean4/pull/6492) fixes a bug in the theorem instantiation procedure in the (WIP) -`grind` tactic. For example, it was missing the following instance in -one of the tests: +`grind` tactic. * [#6497](https://github.com/leanprover/lean4/pull/6497) fixes another theorem instantiation bug in the `grind` tactic. It also moves new instances to be processed to `Goal`. @@ -298,8 +325,7 @@ test. `grind` tactic. * [#6503](https://github.com/leanprover/lean4/pull/6503) adds a simple strategy to the (WIP) `grind` tactic. It just -keeps internalizing new theorem instances found by E-matching. The -simple strategy can solve examples such as: +keeps internalizing new theorem instances found by E-matching. * [#6506](https://github.com/leanprover/lean4/pull/6506) adds the `monotonicity` tactic, intended to be used inside the `partial_fixpoint` feature. @@ -477,30 +503,7 @@ make use of all `export`s when pretty printing, but now it only uses "horizontal exports" that put the names into an unrelated namespace, which the dot notation feature in #6189 now incentivizes. -* [#5757](https://github.com/leanprover/lean4/pull/5757) makes it harder to create "fake" theorems about definitions that -are stubbed-out with `sorry` by ensuring that each `sorry` is not -definitionally equal to any other. For example, this now fails: -```lean -example : (sorry : Nat) = sorry := rfl -- fails -``` -However, this still succeeds, since the `sorry` is a single -indeterminate `Nat`: -```lean -def f (n : Nat) : Nat := sorry -example : f 0 = f 1 := rfl -- succeeds -``` -One can be more careful by putting parameters to the right of the colon: -```lean -def f : (n : Nat) → Nat := sorry -example : f 0 = f 1 := rfl -- fails -``` -Most sources of synthetic sorries (recall: a sorry that originates from -the elaborator) are now unique, except for elaboration errors, since -making these unique tends to cause a confusing cascade of errors. In -general, however, such sorries are labeled. This enables "go to -definition" on `sorry` in the Infoview, which brings you to its origin. -The option `set_option pp.sorrySource true` causes the pretty printer to -show source position information on sorries. +* [#5757](https://github.com/leanprover/lean4/pull/5757), aside from introducing labeled sorries, fixes the bug that the metadata attached to the pretty-printed representation of arguments with a borrow annotation (for example, the second argument of `String.append`), is inconsistent with the metadata attached to the regular arguments. ## Documentation @@ -560,4 +563,3 @@ the universe parameter. * [#6363](https://github.com/leanprover/lean4/pull/6363) fixes errors at load time in the comparison mode of the Firefox profiler. - From 800c60d77a387908ab914a51f2b10772db35fa30 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 4 Feb 2025 10:24:33 +1100 Subject: [PATCH 2/4] chore: report total commits by category in release notes (#6931) This PR reports a sentence like: ```quote For this release, 201 changes landed. In addition to the 74 feature additions and 44 fixes listed below there were 7 refactoring changes, 5 documentation improvements and 62 chores. ``` in the automatically generated release notes. --- script/release_notes.py | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) diff --git a/script/release_notes.py b/script/release_notes.py index 8c97a0395daa..f55ba87de129 100755 --- a/script/release_notes.py +++ b/script/release_notes.py @@ -65,6 +65,24 @@ def format_markdown_description(pr_number, description): link = f"[#{pr_number}](https://github.com/leanprover/lean4/pull/{pr_number})" return f"{link} {description}" +def count_commit_types(commits): + counts = { + 'total': len(commits), + 'feat': 0, + 'fix': 0, + 'refactor': 0, + 'doc': 0, + 'chore': 0 + } + + for _, first_line, _ in commits: + for commit_type in ['feat:', 'fix:', 'refactor:', 'doc:', 'chore:']: + if first_line.startswith(commit_type): + counts[commit_type.rstrip(':')] += 1 + break + + return counts + def main(): parser = argparse.ArgumentParser(description='Generate release notes from Git commits') parser.add_argument('--since', required=True, help='Git tag to generate release notes since') @@ -132,6 +150,13 @@ def main(): for label in changelog_labels: changelog[label].append((pr_number, markdown_description)) + # Add commit type counting + counts = count_commit_types(commits) + print(f"For this release, {counts['total']} changes landed. " + f"In addition to the {counts['feat']} feature additions and {counts['fix']} fixes listed below " + f"there were {counts['refactor']} refactoring changes, {counts['doc']} documentation improvements " + f"and {counts['chore']} chores.\n") + section_order = sort_sections_order() sorted_changelog = sorted(changelog.items(), key=lambda item: section_order.index(format_section_title(item[0])) if format_section_title(item[0]) in section_order else len(section_order)) From 838dcc496f518e9572bb4908b133bf31bfb5f6e7 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 4 Feb 2025 10:26:46 +1100 Subject: [PATCH 3/4] chore: release notes use more paragraphs when needed (#6932) Often PR descriptions end with a colon, followed by a new paragraph containing a code block. Currently in the release notes these get dropped. This PR attempts to include them. It's not particularly robust, but I'll review during the next release. --- script/release_notes.py | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/script/release_notes.py b/script/release_notes.py index f55ba87de129..7f9e74ba803b 100755 --- a/script/release_notes.py +++ b/script/release_notes.py @@ -117,7 +117,11 @@ def main(): body = full_message[len(first_line):].strip() paragraphs = body.split('\n\n') - second_paragraph = paragraphs[0] if len(paragraphs) > 0 else "" + description = paragraphs[0] if len(paragraphs) > 0 else "" + + # If there's a third paragraph and second ends with colon, include it + if len(paragraphs) > 1 and description.endswith(':'): + description = description + '\n\n' + paragraphs[1] labels = fetch_pr_labels(pr_number) @@ -127,7 +131,7 @@ def main(): report_errors = first_line.startswith("feat:") or first_line.startswith("fix:") - if not second_paragraph.startswith("This PR "): + if not description.startswith("This PR "): if report_errors: sys.stderr.write(f"No PR description found in commit:\n{commit_hash}\n{first_line}\n{body}\n\n") fallback_description = re.sub(r":$", "", first_line.split(" ", 1)[1]).rsplit(" (#", 1)[0] @@ -135,7 +139,7 @@ def main(): else: continue else: - markdown_description = format_markdown_description(pr_number, second_paragraph.replace("This PR ", "")) + markdown_description = format_markdown_description(pr_number, description.replace("This PR ", "")) changelog_labels = [label for label in labels if label.startswith("changelog-")] if len(changelog_labels) > 1: From 99f514dc5ef5f0cbad9eb89808681acae65df735 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 4 Feb 2025 10:46:26 +1100 Subject: [PATCH 4/4] chore: release_checklist.py checks for bump/v4.X.0 branches (#6933) Some downstream repositories require a `bump/v4.X.0` branch to exist for their integration CI. This PR updates `release_checklist.py` to check for the existence of these branches, when needed. --- doc/dev/release_checklist.md | 2 +- script/release_checklist.py | 26 ++++++++++++++++++++++---- script/release_repos.yml | 2 ++ 3 files changed, 25 insertions(+), 5 deletions(-) diff --git a/doc/dev/release_checklist.md b/doc/dev/release_checklist.md index 80c40ba5d601..7680d0c10a2e 100644 --- a/doc/dev/release_checklist.md +++ b/doc/dev/release_checklist.md @@ -199,7 +199,7 @@ We'll use `v4.7.0-rc1` as the intended release version in this example. - We do this for the same list of repositories as for stable releases, see above. As above, there are dependencies between these, and so the process above is iterative. It greatly helps if you can merge the `bump/v4.7.0` PRs yourself! - It is essential for Mathlib CI that you then create the next `bump/v4.8.0` branch + - It is essential for Mathlib and Batteries CI that you then create the next `bump/v4.8.0` branch for the next development cycle. Set the `lean-toolchain` file on this branch to same `nightly` you used for this release. - (Note: we're currently uncertain if we really want to do this step. Check with Kim Morrison if you're unsure.) diff --git a/script/release_checklist.py b/script/release_checklist.py index 3968a77ff49e..d716d97d4026 100755 --- a/script/release_checklist.py +++ b/script/release_checklist.py @@ -142,6 +142,14 @@ def extract_org_repo_from_url(repo_url): return repo_url.replace("https://github.com/", "").rstrip("/") return repo_url +def get_next_version(version): + """Calculate the next version number, ignoring RC suffix.""" + # Strip v prefix and RC suffix if present + base_version = strip_rc_suffix(version.lstrip('v')) + major, minor, patch = map(int, base_version.split('.')) + # Next version is always .0 + return f"v{major}.{minor + 1}.0" + def main(): github_token = get_github_token() @@ -201,6 +209,7 @@ def main(): branch = repo["branch"] check_stable = repo["stable-branch"] check_tag = repo.get("toolchain-tag", True) + check_bump = repo.get("bump-branch", False) print(f"\nRepository: {name}") @@ -220,15 +229,24 @@ def main(): if check_tag: if not tag_exists(url, toolchain, github_token): print(f" ❌ Tag {toolchain} does not exist. Run `script/push_repo_release_tag.py {extract_org_repo_from_url(url)} {branch} {toolchain}`.") - continue - print(f" ✅ Tag {toolchain} exists") + else: + print(f" ✅ Tag {toolchain} exists") # Only check merging into stable if stable-branch is true and not a release candidate if check_stable and not is_release_candidate(toolchain): if not is_merged_into_stable(url, toolchain, "stable", github_token): print(f" ❌ Tag {toolchain} is not merged into stable") - continue - print(f" ✅ Tag {toolchain} is merged into stable") + else: + print(f" ✅ Tag {toolchain} is merged into stable") + + # Check for bump branch if configured + if check_bump: + next_version = get_next_version(toolchain) + bump_branch = f"bump/{next_version}" + if branch_exists(url, bump_branch, github_token): + print(f" ✅ Bump branch {bump_branch} exists") + else: + print(f" ❌ Bump branch {bump_branch} does not exist") if __name__ == "__main__": main() diff --git a/script/release_repos.yml b/script/release_repos.yml index 4246f1c36a45..e59f05e4492f 100644 --- a/script/release_repos.yml +++ b/script/release_repos.yml @@ -4,6 +4,7 @@ repositories: toolchain-tag: true stable-branch: true branch: main + bump-branch: true dependencies: [] - name: lean4checker @@ -76,6 +77,7 @@ repositories: toolchain-tag: true stable-branch: true branch: master + bump-branch: true dependencies: - Aesop - ProofWidgets4