Skip to content

Commit

Permalink
merge master
Browse files Browse the repository at this point in the history
  • Loading branch information
@kim-em
kim-em committed Feb 4, 2025
2 parents 01e8f42 + 99f514d commit 5c5ccf5
Show file tree
Hide file tree
Showing 2 changed files with 88 additions and 57 deletions.
110 changes: 56 additions & 54 deletions releases/v4.16.0.md
View file
Original file line number Diff line number Diff line change
@@ -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
Expand All @@ -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]+)*
Expand All @@ -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,
Expand All @@ -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.
Expand Down Expand Up @@ -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`.
Expand All @@ -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.
Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -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.

35 changes: 32 additions & 3 deletions script/release_notes.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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')
Expand Down Expand Up @@ -99,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)

Expand All @@ -109,15 +131,15 @@ 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]
markdown_description = format_markdown_description(pr_number, fallback_description)
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:
Expand All @@ -132,6 +154,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))

Expand Down

0 comments on commit 5c5ccf5

Please sign in to comment.