Lean 4.5.0 (2024-02-01)🔗

Modify the lexical syntax of string literals to have string gaps, which are escape sequences of the form "\" newline whitespace*. These have the interpretation of an empty string and allow a string to flow across multiple lines without introducing additional whitespace. The following is equivalent to "this is a string".
```
"this is \
   a string"
```
PR #2821 and RFC #2838.
Add raw string literal syntax. For example, r"\n" is equivalent to "\\n", with no escape processing. To include double quote characters in a raw string one can add sufficiently many # characters before and after the bounding "s, as in r#"the "the" is in quotes"# for "the \"the\" is in quotes". PR #2929 and issue #1422.
The low-level termination_by' clause is no longer supported.

Migration guide: Use termination_by instead, e.g.:
```
-termination_by' measure (fun ⟨i, _⟩ => as.size - i)
+termination_by i _ => as.size - i
```
If the well-founded relation you want to use is not the one that the WellFoundedRelation type class would infer for your termination argument, you can use WellFounded.wrap from the std library to explicitly give one:
```
-termination_by' ⟨r, hwf⟩
+termination_by x => hwf.wrap x
```
Support snippet edits in LSP TextEdits. See Lean.Lsp.SnippetString for more details.
Deprecations and changes in the widget API.
- Widget.UserWidgetDefinition is deprecated in favour of Widget.Module. The annotation @[widget] is deprecated in favour of @[widget_module]. To migrate a definition of type UserWidgetDefinition, remove the name field and replace the type with Widget.Module. Removing the name results in a title bar no longer being drawn above your panel widget. To add it back, draw it as part of the component using <details open=true><summary class='mv2 pointer'>{name}</summary>{rest_of_widget}</details>. See an example migration here.
- The new command show_panel_widgets allows displaying always-on and locally-on panel widgets.
- RpcEncodable widget props can now be stored in the infotree.
- See RFC 2963 for more details and motivation.
If no usable lexicographic order can be found automatically for a termination proof, explain why. See feat: GuessLex: if no measure is found, explain why.
Option to print inferred termination argument. With set_option showInferredTerminationBy true you will get messages like
```
Inferred termination argument:
termination_by
ackermann n m => (sizeOf n, sizeOf m)
```
for automatically generated termination_by clauses.
More detailed error messages for invalid mutual blocks.
Multiple improvements to the output of simp? and simp_all?.
Tactics with withLocation * no longer fail if they close the main goal.
Implementation of a test_extern command for writing tests for @[extern] and @[implemented_by] functions. Usage is
```
import Lean.Util.TestExtern

test_extern Nat.add 17 37
```
The head symbol must be the constant with the @[extern] or @[implemented_by] attribute. The return type must have a DecidableEq instance.

Bug fixes for #2853, #2953, #2966, #2971, #2990, #3094.

Bug fix for eager evaluation of default value in Option.getD. Avoid panic in leanPosToLspPos when file source is unavailable. Improve short-circuiting behavior for List.all and List.any.

Several Lake bug fixes: #3036, #3064, #3069.