chore: add highlights for v4.19 release notes #442
Conversation
Manual/Releases/v4.19.0.lean
Outdated
| * [#7366](https://github.com/leanprover/lean4/pull/7366) adds server-side support for dedicated 'unsolved goals' and | ||
| 'goals accomplished' diagnostics that will have special support in the | ||
| Lean 4 VS Code extension. The special 'unsolved goals' diagnostic is | ||
| adapted from the 'unsolved goals' error diagnostic, while the 'goals | ||
| accomplished' diagnostic is issued when a `theorem` or `Prop`-typed | ||
| `example` has no errors or `sorry`s. The Lean 4 VS Code extension | ||
| companion PR is at [leanprover/vscode-lean4#585](https://github.com/leanprover/vscode-lean4/pull/585). |
There was a problem hiding this comment.
Maybe move this first, as the most user-visible change, and maybe even add a paragraph.
The companion change to the Lean 4 VS Code extension also adds new error and warning gutter decorations…
(See leanprover/vscode-lean4#585 for details). This deserves highlighting :-)
There was a problem hiding this comment.
Thank you! Addressed in f06e06b
| * [#7084](https://github.com/leanprover/lean4/pull/7084) enables the elaboration of theorem bodies, i.e. proofs, to | ||
| happen in parallel to each other as well as to other elaboration tasks. |
There was a problem hiding this comment.
This is also a big deal, maybe second highlight?
There was a problem hiding this comment.
Sure, added in f06e06b
|
@david-christiansen , are you ok with me merging such PRs or would you want to have a second look? |
|
Preview for this PR is ready! 🎉 (also as a proofreading version). built with commit f06e06b. |
|
Go for it. If you think something needs special attention, or you're not confident about some aspect, just let me know. |
This PR adds highlights to v4.19 release notes and reorganizes entries in the extended list.
This PR adds highlights to v4.19 release notes and reorganizes entries in the extended list.