chore: merge main and update to nightly-2026-06-22#870
Merged
Conversation
Adds prioritization to search results, slightly boosting searches for names and tactic names while down-prioritizing release notes. Relies on leanprover/verso#844.
The previous phrasing "[that they performed this check](https://github.com/leanprover/reference-manual/blob/main/Manual/ValidatingProofs.lean#L67C188-L67C207)" was ambiguous. The new phrasing explicitly states who should do what check. Closes #848
Reorder the four reducibility levels in the section on reducibility so the list now reads irreducible → semireducible → implicit reducible → reducible (most restrictive to least), which matches how the levels are usually introduced and aligns with the unfolding hierarchy. 🤖 Prepared with Claude Code Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Was "we use malicious to describe code _to go_ out of its way", corrected to "we use malicious to describe code that _goes out_ of its way" (emphasis highlights edit)
Changes for the v4.30.0 highlights on top of #836 . --------- Co-authored-by: Joscha <joscha@plugh.de> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
This PR adds Netlify header rules that cause the content-addressed parts of the search index to be permanently cached, so clients don't need to do an HTTP round-trip after having downloaded them. A profile in Chrome showed a significant improvement.
Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
Adapts to leanprover/verso#862 After that gets merged, this PR should be updated to point back at `main` before merging.
Co-authored-by: github-actions[bot] <github-actions[bot]@users.noreply.github.com> Co-authored-by: David Thrane Christiansen <david@lean-fro.org> Co-authored-by: jcreedcmu <jcreed@gmail.com> Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk> Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com> Co-authored-by: Sebastian Graf <sgraf1337@gmail.com> Co-authored-by: Robert J. Simmons <442315+robsimmons@users.noreply.github.com> Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com> Co-authored-by: Pim Otte <otte.pim@gmail.com> Co-authored-by: Phil Nguyen <pcn@cs.umd.edu> Co-authored-by: Violetta Sim <38787503+eyihluyc@users.noreply.github.com> Co-authored-by: Markus Himmel <markus@himmel-villmar.de> Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com> Co-authored-by: euprunin <178733547+euprunin@users.noreply.github.com> Co-authored-by: u <u@h> Co-authored-by: Pablo Graubner <2234137+pgraubner@users.noreply.github.com> Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: Marc Huisinga <mhuisi@protonmail.com> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: jrr6 <7482866+jrr6@users.noreply.github.com> Co-authored-by: Leonardo de Moura <leomoura@amazon.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Violetta Sim <38787503+viol37@users.noreply.github.com> Co-authored-by: Rob Simmons <rob@lean-fro.org> Co-authored-by: leanprover-bot <leanprover-bot@lean-fro.org> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Wojciech Różowski <wojciech@lean-fro.org> Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com> Co-authored-by: Richard Davison <richard.neil.davison@gmail.com> Co-authored-by: Chris Su <102528557+chrissuu@users.noreply.github.com> Co-authored-by: ericrbg-harmonic <eric@harmonic.fun> Co-authored-by: Mac Malone <tydeu@hatpress.net>
This was somehow committed by the automation and needs to be removed.
I forgot to link them, and there were some tiny tweaks to the release notes themselves.
Bumps dependencies to fix two bugs in tutorial header permalink widgets: 1. They were absolute, rather than relative, URLs, so they ignored `<base>` 2. They had doubled components in their HTML IDs
Co-authored-by: Sebastian Graf <sgraf1337@gmail.com>
This PR expands the "Test and Lint Drivers" chapter in the Lake reference to make `lake test` and `lake lint` substantially easier to follow on a first read. The previous text was a single short paragraph that mentioned `@[test_driver]` once without an example. The new section covers: * what a test or lint driver actually is — a target (executable, script, or library) that Lake invokes; Lake itself is not a test framework, * exit-code semantics for executable and script drivers, and the elaboration-error contract for library drivers, * a verified `lakefile.toml` example for both `testDriver` and `lintDriver`, * prose instructions for the equivalent `lakefile.lean` configuration (without a code example, since the surrounding chapter is currently in a `:::TODO` because importing Lake's attributes crashes the compiler), * the single-driver constraint and the conflict between the attribute and the configuration field, * the `<pkg>/<name>` syntax for drivers defined in dependency packages, * how `testDriverArgs` and `lintDriverArgs` compose with arguments passed after `--` on the command line, * the restriction that library test drivers do not accept arguments, * notes on `lake check-test` and `lake check-lint`. Motivated by a recent Zulip thread asking for better documentation: https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Using.20.60lake.20test.60.20effectively/near/598083186 🤖 Prepared with Claude Code --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com> Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
Changes for the v4.31.0 highlights --------- Co-authored-by: Joscha <joscha@plugh.de>
Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
Addresses both #13679 and more general compiler freedom --------- Co-authored-by: David Thrane Christiansen <david@lean-fro.org> Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
Contributor
|
Preview for this PR is ready! 🎉 (also as a proofreading version). built with commit 311cfa5. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
7 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This updates to nightly-2026-06-22 and adds a discussion of the new Float model and the instance/implicit reducibility split.