Mathlib-contributor tools, new editor commands, and version 0.11.0

[keithadler]

What this changes

Adds a set of commands (menu, command palette and MCP tools) for people who write Lean and contribute to Mathlib, tests for each, and bumps the version to 0.11.0.

• Sort Imports, Tidy Whitespace and Check Style, Tidy File, Wrap Long Comment Lines: Mathlib's text rules (trailing whitespace, tabs, CRLF, final newline, 100-character lines) and import order, each as one undoable edit.
• Mathlib conventions: copyright header, module docstring, theorem and type naming, doc comments on public definitions; Add Mathlib Copyright Header.
• Remove Deprecations Older Than Six Months: finds deprecated aliases by their (since := "…") and deletes the old ones with their doc comments.
• Suggest a Name for This Theorem: a Mathlib-style name from a statement (a + b = b + a is add_comm).
• Merge Consecutive rw / intro Steps: merges rw [a] then rw [b] (also simp_rw, and two intros) where that cannot change the proof.
• Find Duplicate Theorem Statements: theorems that state the same thing under different names.
• Copy as a Zulip Message: the file in a lean fence with Lean's messages in a quote.
• MCP tools: sort_imports, style_check, stale_deprecations, suggest_name, merge_tactics, duplicate_statements.
• Version 0.11.0 in Directory.Build.props; the CHANGELOG's Unreleased section is now 0.11.0; the README's Status says 0.11.

New tests are in tests/LeanStudio.Tests/PickerAndConflictTests.cs.

Checklist

• The solution builds with no warnings (warnings are errors here); the new test classes and the existing MCP tests pass locally. The full suite and the Lean-backed tests have not been run locally; CI will run them.
• Snapshot run: not run; the new menu items have not been clicked through in the running app.
• The new commands work on text and need no running Lean, so none of the new tests starts Lean.
• Public types and members have /// doc comments
• CHANGELOG.md has entries for each change

Not done here: no v0.11.0 tag, and the Homebrew and winget manifests under packaging/ still say 0.10.0. They are updated after a release is published.

🤖 Generated with Claude Code

https://claude.ai/code/session_01FF5AYRpU9TWeWY3CFh2ETw

---

Generated by Claude Code

[keithadler]

CI has been red intermittently on this PR. Here is what failed, what I fixed, and what I did not touch. (Updated after run 90.)

Fixed in this PR, in my own code: SorryHistoryTests.ReadsARealRepository failed on macOS in runs 87–89. Sorry Burndown passed git grep -E '\b(sorry|admit)\b', and macOS's regex library has no \b, so it found nothing. Fixed in 0575df7 with git grep -w -e sorry -e admit. It no longer fails in run 90.

Fixed in this PR, in code the PR does not otherwise touch (its own commit, easy to drop or cherry-pick out): two of the intermittent failures had one root cause in JsonRpcConnection.RequestAsync. When the other side died while a request was still waiting to be written, the reader failed the request with the named (while waiting for …) error, and then the request's own write failed too. The caller got the raw Pipe is broken., and the reader's error, which nobody awaited, surfaced later as an unobserved task exception. That is:

• Windows, StressTests.WhenTheOtherSideDiesEveryWaitingRequestFailsPromptly (Pipe is broken.): runs 86 and 88.
• The Snapshot step's "no error was caught and logged behind the scenes" check, from textDocument/documentHighlight (macOS, run 86) and textDocument/documentSymbol (Linux, runs 89 and 90).

The new test ARequestWhoseWriteFailsAfterTheReaderSawTheCloseNamesItAndLeavesNothingUnobserved reproduces it deterministically with gated streams. Before the fix it fails with the same message as CI; after, it passes, as do all 20 Stress tests and the rest of the local suite (352 passed, 91 skipped for lack of Lean, 0 failed). The change makes a failed write report the request by name, wrapping the original error, and observes the reader's error.

Not touched (still intermittent, not this change): RemoteLeanTests.LeansServerRunsRemotelyAndTheEditorSeesLocalPaths failed on macOS in run 90 with an empty collection of diagnostics. The test treats "file progress done" as the end and then reads the last diagnostics it saw, so it races the two messages. It runs Lean over a stand-in SSH script; the diff does not touch it.

I'd like the rest of the fixes judged on a clean run rather than my say-so, so I'll check the next one.

---

Generated by Claude Code