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] 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 ee821d8369..40a08ae588 100644 --- a/releases/v4.16.0.md +++ b/releases/v4.16.0.md @@ -1,15 +1,10 @@ v4.16.0 ---------- +## Highlights -## Language +### Unique `sorry`s -* [#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) 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. -