release-highlights

name	release-highlights
description	Write the Highlights section for Lean 4 release notes. Use when asked to write, draft, or update release highlights for a Lean version.
allowed-tools	Bash, Read, Glob, Grep, Edit, Write, WebFetch, WebSearch

Write Release Highlights for Lean

You are writing the "Highlights" section for a Lean 4 release. This section goes at the top of the release notes (after the statistics paragraph) and summarizes the most important changes for users.

Input

You will be given the release notes file for a Lean version (e.g. v4.30.0). This file is a .lean file in the leanprover/reference-manual repository under Manual/Releases/, containing embedded markdown.

Reference manual repo path: Before starting, check whether you know the local path to the leanprover/reference-manual repository clone. If you don't know it, ask the user for the path. Do not guess or assume a path — the user may have it checked out anywhere.

Version: Ask the user which version to write highlights for. Do not assume a version — the user must specify it explicitly (e.g. v4.30.0).

Release candidates are normal. The release notes file is typically a release candidate (its title may read e.g. Lean 4.31.0-rc2 and it may contain a :::warn ... release candidate ...::: admonition). This is expected — write the highlights as usual against the rc content. Do not treat the rc warning as a blocker, and leave that admonition in place.

The release notes file already contains:

• A statistics paragraph ("For this release, N changes landed...")
• Detailed per-category sections (Language, Library, Tactics, Lake, etc.) with one bullet per PR

Your job is to write a # Highlights section to insert between the statistics paragraph and the detailed sections.

Process

Step 1: Gather context

1. Read the full release notes file carefully.

2. Fetch and read ALL PR descriptions for every PR mentioned in the release notes for the current release — no exceptions, no sampling, no "I already have enough to write the highlights." This is a MANDATORY, NON-NEGOTIABLE step: even if you believe you have identified the flagship features after reading a subset, you MUST still fetch every remaining PR before writing, because a terse one-line entry is often the only surface signal for a change whose PR description reveals it to be highlight-worthy. Skipping any PR is a process failure even if the final highlights happen to come out fine.

   Mechanize the sweep so you cannot miss any. First extract the complete, deduplicated list of PR numbers from the current release notes file (e.g. grep -oE 'pull/[0-9]+' Manual/Releases/vX_Y_Z.lean | grep -oE '[0-9]+' | sort -un), count them, then fetch every one of them in batches with gh pr view NNNNN --repo leanprover/lean4 --json title,body. After fetching, confirm the number of PRs you actually read equals the count from the file. Only read the current release's notes file — do NOT also read or fetch PRs from previous releases' notes files. Batch these calls in parallel where possible (a shell for loop over the extracted numbers is the simplest way to guarantee coverage). This is essential because:

   • PR descriptions often contain examples, motivation, and context not present in the one-line release note entry.
   • Long, human-written PR descriptions are a strong signal that the change is important and highlight-worthy.
   • Caveat: If a PR description appears to be AI-generated (signed by Claude, or recognizable AI style with generic phrasing), do NOT treat length as a signal of importance. AI writes detailed descriptions even for minor fixes.
   • Watch for milestones hiding in terse entries. Sometimes a single line like "The old compiler has been replaced by the new compiler" or "grind tactic is now available" represents a huge milestone that deserves top billing. Don't let a short release note entry cause you to overlook it.

3. Look at the previous release's highlights to understand the current trajectory of features (e.g., was grind highlighted last time? Is the module system still experimental?).

Step 2: Select highlights

What to highlight:

• User-facing UX improvements (editor features, error messages, "try this" improvements, go-to-definition) — these should come first, as they affect the most users
• Major new language features (new commands, new syntax, new elaboration capabilities)
• Significant new tactic capabilities (grind, simp, bv_decide, etc.)
• Monadic verification / mvcgen features — these are a key research direction and should be highlighted when present
• Notable performance improvements
• Important breaking changes that users need to know about (migration guidance is valuable)
• New Lake features
• Major library redesigns or new APIs (String overhaul, iterator API, async primitives, new types)

What NOT to highlight:

• Individual bug fixes (unless they fix a very prominent issue)
• Internal refactors
• Individual lemma additions
• Small performance tweaks
• Internal API changes
• Features that are still WIP/preparational for future releases (check with context if unsure)
• Changes where the PR description is the only signal of importance and it's AI-generated

Signals of highlight-worthiness (in rough priority order):

1. Changes that affect how users write Lean code day-to-day (new syntax, new tactics, editor UX)
2. Long, human-written PR descriptions with examples — the author thought it was important
3. Multiple related PRs addressing the same feature — indicates sustained effort worth showcasing
4. Explicit "breaking change" labels — collect these in a dedicated subsection
5. Features with demo videos or playground links

Calibrating depth for different feature types:

• Flagship features (e.g., a major tactic getting new capabilities like grind): Give these generous space. Use sub-headings (###) for each major new capability, include code examples from PR descriptions. The reader should understand what's new and be able to try it. When a feature like grind has multiple distinct new capabilities in one release, each deserves its own sub-section with examples. However, if a feature is being introduced for the first time, a brief announcement with a link to its documentation may be better than a deep dive — the reference manual is the right place for comprehensive docs, not the release notes.
• Code examples are essential. For any feature that can be demonstrated with code, include an example. Pull examples from PR descriptions — authors often include well-crafted demonstrations. A highlight without a code example is much less useful to the reader.
• Themed groups of PRs (e.g., "error messages improved", "performance gains"): A brief thematic summary + a list of PR links is sufficient. Do NOT elaborate on each PR individually — just convey the theme and let the reader follow the links if interested.
• Related breaking changes should be unified into a single narrative. When multiple PRs address the same underlying issue (e.g., transparency handling changes touching isDefEq, @[implicit_reducible], simp +instances, and inferInstanceAs), present them as one coherent story with a migration guide, NOT as separate highlights. The reader needs to understand the whole picture, not piece it together from fragments.
• Migration guides are high-value content. When a breaking change is disruptive, include practical migration advice: set_option workarounds, lakefile.toml configuration examples, available porting scripts, and step-by-step guidance. Check PR descriptions thoroughly for migration instructions — they often contain lakefile.toml snippets, helper scripts, and diagnostic commands that are extremely valuable to include verbatim. This is often the most useful part of the highlights for affected users.
• Experimental features can be highlighted but should be clearly labeled with "Experimental:" in the heading (e.g., ## Experimental: Module System). This signals to users that the feature is available for experimentation but not yet stable. Do NOT give experimental features the same prominence as stable features.
• Policy/process changes (e.g., backward compatibility options policy): Brief mention, 1-2 sentences.
• Internal infrastructure (e.g., symbol clash prevention, try? parallelism, compiler pass migrations): Usually not highlight-worthy unless the user impact is direct and significant (e.g., measurable startup time improvement).

What NOT to highlight (continued):

• Internal milestones (e.g., removing old compiler backend) unless they have direct user impact
• Incremental improvements to a feature that was already highlighted in a previous release, unless there's a qualitative leap (e.g., don't re-highlight grind every release just because it got faster; DO highlight when grind gets a fundamentally new capability like interactive mode)
• Many small improvements to the same subsystem — summarize them in the intro paragraph instead of giving them their own section

How many highlights?

• The number of highlights should reflect the release. Feature-rich releases (v4.18, v4.22, v4.25) may have 7-13 topics. Consolidation releases (v4.23, v4.24) may have just 2-5 topics.
• Err on the side of fewer highlights. A highlight section that's too long fails its purpose — it becomes just another copy of the detailed list. It is better to have 3 really well-written highlights than 10 mediocre ones.
• If the release is light on big features, say so in the intro paragraph (e.g., "brings significant performance improvements, better error messages, and a plethora of bug fixes and consolidations") and only highlight the 2-3 things that are genuinely new to users.
• If nearly everything seems highlight-worthy, you are probably not being selective enough. Step back and ask: "Would a Lean user who skims only this section get the right picture of this release?"
• Breaking changes should be collected into a dedicated ## Breaking Changes subsection at the end of the highlights section. This is more useful to users than scattering breaking changes across feature descriptions. When a breaking change is directly related to a highlighted feature (e.g., String.Slice overhaul), mention it briefly in the feature highlight AND include it with migration details in the Breaking Changes section.

Step 3: Write the highlights

Structure:

# Highlights

[Optional 1-3 sentence overview of the release's themes]

## [Descriptive Feature Name]

[#NNNNN](https://github.com/leanprover/lean4/pull/NNNNN) [prose description
of the change, what it does, why it matters].

[Code example if available and illuminating]

## [Flagship Feature with Sub-items] (e.g., "New Features in Grind")

### [Sub-capability 1]

[#NNNNN](...) [description with code example]

### [Sub-capability 2]

[#NNNNN](...) [description with code example]

### Other New Features in [Feature]

- [brief bullet list of smaller items with PR links]

## [Themed Group] (e.g., "Error Messages", "Performance Gains")

[1-2 sentence thematic summary]

PRs: [#N1](...), [#N2](...), [#N3](...).

## Library Highlights

[Thematic summary of library changes, not an exhaustive list.]

## Breaking Changes

- [#NNNNN](...) [description + migration guidance]
- [#NNNNN](...) [description + migration guidance]

Writing style:

• Technical but accessible. Assume the reader uses Lean but may not follow development closely.
• Third person, declarative: "[#NNNNN] adds support for...", "[#NNNNN] implements..."
• Show excitement about genuine progress — these notes should "show off the hard work that went into the release" — but don't be breathless or use marketing language.
• Include code examples when they help illustrate a feature. Pull good examples from PR descriptions or linked issues.
• For breaking changes, always include migration guidance when available.
• Keep individual highlight entries concise (1-3 paragraphs typically). For major features, more detail is fine.

Formatting rules:

• PR links are always full markdown links: [#NNNNN](https://github.com/leanprover/lean4/pull/NNNNN)
• Issue links similarly: [#NNNN](https://github.com/leanprover/lean4/issues/NNNN)
• Use ## for each major highlight topic heading
• Use ### for sub-topics within a highlight (e.g., multiple grind features under ## New Features in Grind)
• Code blocks use triple backticks. Use lean language tag when appropriate for Verso-native files, plain triple backticks for markdown-block files.
• Breaking changes are marked with *Breaking change:* or *Breaking Changes:* in italic
• When consolidating multiple PRs into one highlight, list all PR links

Regarding the detailed sections below the highlights:

• Do NOT reorder or restructure the detailed per-category sections
• If a PR was moved to highlights with extended description, optionally add a brief note in the detailed section: "see highlights for details"
• All PRs should remain in the detailed list even if highlighted above

Step 4: Library highlights

Library changes deserve a ## Library Highlights subsection only when there are genuinely notable library changes (new types, API redesigns, new frameworks). The approach:

• Do NOT try to list every library change — that would just duplicate the detailed list
• Summarize thematically: "expanded lemmas for Array/Vector/List", "better support for bitwise operations"
• Highlight genuinely new types, major API redesigns, or new frameworks (e.g., async primitives, iterator API)
• Call out breaking library changes explicitly
• If library changes are mostly incremental lemma additions and minor fixes, omit this subsection entirely or mention them in the intro paragraph

Step 5: Review

Before finalizing, check:

• Is the highlights section between the statistics paragraph and the first detailed section?
• Are all PR links correctly formatted?
• Does each highlight actually add value over the one-line entry in the detailed list?
• Are breaking changes clearly called out with migration guidance?
• Is the length appropriate? (Not so long it's just a copy of the detailed list, not so short it misses important things)
• Does it sound exciting and professional without being over-the-top?
• Are WIP/preparational features excluded (or marked as experimental/preview)?

Step 6: Post-processing — Link to the reference manual

After writing the highlights, do a post-processing pass to add cross-references to the Lean reference manual where relevant. This requires using Verso-native format (not markdown blocks).

Use Verso cross-reference syntax:

• {tactic}\grind`` — links to a tactic's documentation
• {name}\String.Slice`` — links to a declaration's documentation
• {option}\backward.do.legacy`` — links to an option's documentation
• {ref "section-slug"}[display text] — links to a named section
• {keywordOf Lean.Parser.Command.grind_pattern}\grind_pattern`` — links to a keyword

Examples of where to add these:

• When mentioning a tactic by name, use {tactic}\tacticName``
• When mentioning a type or definition, use {name}\Fully.Qualified.Name``
• When mentioning an option, use {option}\option.name``
• When referring to a documented section of the reference manual, use {ref "slug"}[text]

To find valid section slugs, search the reference manual source for tag := or section headings. Do not guess slugs — only use ones you can verify exist.

This step does not affect highlight selection or phrasing — it just enriches the output with useful navigation links.

Format details

Always use Verso-native format: markdown is written directly in the #doc block. Use # Highlights as the heading level, ## for topics, ### for sub-topics.

Code blocks within Verso-native files use ```lean (with language tag) when the code should be checked by Lean, or plain ``` when it should not be checked (e.g., illustrative goal states, pseudo-code).