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

.github/workflows/ci.yml

@@ -54,6 +54,9 @@ jobs:
       - name: Drive the UI against a real Lean server
         if: runner.os != 'Windows'
         run: dotnet tools/LeanStudio.Snapshot/bin/Release/net10.0/LeanStudio.Snapshot.dll . snapshots
+      - name: Run the Lean menu's text and Git commands in the window
+        if: runner.os != 'Windows'
+        run: dotnet tools/LeanStudio.Snapshot/bin/Release/net10.0/LeanStudio.Snapshot.dll --commands
       - uses: actions/upload-artifact@v6
         if: always() && runner.os != 'Windows'
         with:

CHANGELOG.md

@@ -1,6 +1,6 @@
 # Changelog
 
-## Unreleased
+## 0.11.0
 
 **What VS Code had and Lean Studio didn't**:
 - **An integrated terminal** (⌃`, *View ▸ Terminal*): your shell in the bottom panel, in the project's folder, with `lake` and `lean` on its path. A real pseudo-terminal and xterm's emulator, so colours, full-screen programs and resizing work; a 5,000-line scrollback; copy and paste. *Open in Terminal* in Files now opens it there (*Open in External Terminal* is the old one).
@@ -14,6 +14,24 @@
 - **Dev containers and WSL**: *Remote: Use the Dev Container* runs a project's Lean in its dev container (found running, or started with `devcontainer up`), which mounts the folder, so no sshfs is needed. On Windows, a folder in WSL runs its Lean inside WSL by itself.
 - Each file came back scrolled to the top after switching to another and back: AvaloniaEdit's `ScrollToVerticalOffset` does nothing in the version used. It now keeps its place.
 
+**New**:
+- **Sort Imports** (*Lean ▸ Sort Imports*, and in the command palette): puts each run of `import` lines in the file's header in order by module name and drops repeats, as Mathlib's style asks. Blank lines and comments between runs stay, so a deliberate grouping is kept; nothing below the header moves. One undoable edit that touches only the lines that changed.
+- **Tidy Whitespace and Check Style** (*Lean ▸ Tidy Whitespace and Check Style*): holds the file to the text rules of Mathlib's style linter. Trailing whitespace, tabs, Windows line endings and a missing or doubled final newline are fixed as one undoable edit; lines over 100 characters are listed in Output for you to break.
+- **Tidy File** (*Lean ▸ Tidy File*) does both in one undoable edit: sorts the imports, fixes the whitespace, and lists what is left (long lines and, in a project that uses Mathlib, the file conventions).
+- **Mathlib's file conventions**: the copyright header, a module docstring, and theorem names that start with a capital are reported by *Tidy File* in a Mathlib project and by `style_check` over MCP (`mathlib=true` forces it). **Add Mathlib Copyright Header** puts the header on a file that has none, for this year and the name git is set up with.
+- **Remove Deprecations Older Than Six Months** (*Lean ▸ Remove Deprecations Older Than Six Months*): Mathlib deletes a deprecated alias some months after the rename. Reads each `(since := "…")`, and deletes those past the age, with their doc comments, as one undoable edit; each is named in Output. The counterpart of the deprecated alias *Rename* writes. `stale_deprecations` does the same over MCP, with `months` and `apply`.
+- **Doc comments on definitions**: in a Mathlib project, Tidy File and `style_check` also list each public `def`, `abbrev`, `structure`, `class` and `inductive` with no doc comment, as Mathlib's `docBlame` linter asks, read from the text, so nothing has to be built first.
+- **Wrap Long Comment Lines** (*Lean ▸ Wrap Long Comment Lines*): breaks the `--` comment and docstring lines over 100 characters at a space, which Tidy cannot do for you, as one undoable edit. Code, code fences, indented code in a docstring and words longer than the limit (a URL) are never touched. `style_check` takes `wrap=true` with `apply`.
+- Structure, class and inductive names that start with a lowercase letter are now reported by the Mathlib conventions check.
+- **Copy as a Zulip Message** (*File ▸ Copy as a Zulip Message*, and under Share in the palette): the active file in a `lean` fence and, in a quote below it, what Lean says about it, errors first, ready to paste into the Lean Zulip chat. The fences grow when the code has backticks of its own.
+- **Suggest a Name for This Theorem** (*Lean ▸ Suggest a Name for This Theorem*): reads the statement of the theorem at the cursor and gives the name Mathlib's scheme would: the conclusion read left to right with each operation and relation as a word, then `_of_` before each assumption. `a + b = b + a` is `add_comm`, `0 + a = a` is `zero_add`, `a ≤ b → b < c → a < c` is `lt_of_le_of_lt`. It says whether the theorem's own name matches; *Rename Symbol* applies it. A starting point for statements about operations and relations, not an oracle. `suggest_name` does the same over MCP.
+- **Merge Consecutive rw / intro Steps** (*Lean ▸ Merge Consecutive rw / intro Steps*): `rw [a]` then `rw [b]` become `rw [a, b]` (also `simp_rw`, and for the same `at` location), and two `intro` lines become one, as one undoable edit. Only whole lines that do nothing else are merged, so the proof means exactly what it did. `merge_tactics` does the same over MCP.
+- **Find Duplicate Theorem Statements** (*Lean ▸ Find Duplicate Theorem Statements*): looks through the project's Lean files for theorems that state the same thing under different names, with the names of the variables they bind and the spacing left out (`(a b : ℕ) : a + b = b + a` is `(x y : ℕ) : x + y = y + x`), and lists each group in Output with its files and lines. Mathlib asks that a result is stated once. Statements are compared as text, so two that are equal only by unfolding are not found. `duplicate_statements` does the same over MCP.
+- **Project Health Summary** (*Lean ▸ Project Health Summary*): the project's state at a glance, counted from its Lean files without building anything: files, lines, theorems and definitions; `sorry` and TODO counts; the share of definitions with a doc comment; deprecated declarations and how many are old enough to delete; style problems; and the five files with the most still to do. `project_health` does the same over MCP, as Markdown.
+- **Sorry Burndown** (*Lean ▸ Sorry Burndown*): how a formalization is coming along. The number of `sorry`s the project had at each of its last 30 commits, as a sparkline (`▇▅▃▁`) and the commits that moved the count (`2026-09-02  2222222  −3  Prove a`). Read with `git grep` on each commit, so nothing is checked out or built and a long history takes seconds. `sorry_history` does the same over MCP, with `commits`.
+- **What This Branch Changed Mathematically** (*Lean ▸ What This Branch Changed Mathematically*): the theorems the current branch adds, removes and restates since it left `main`, the way a reviewer reads a pull request, with the proofs ignored. A theorem proved differently, or with renamed variables, is no change; one whose statement differs is listed with its before and after. Markdown in Output, ready to paste into the pull request. `statement_changes` does the same over MCP, between any two refs.
+- **Over MCP**, `sort_imports` and `style_check` do the same for assistants, each with `apply` to write the file.
+
 **Fixes**:
 - `verify` over MCP kept returning the declarations of the build it first read after the project was built again outside it (`lake build` in a terminal), until the server restarted ([#2](https://github.com/keithadler/leanstudio/issues/2)). Tenet now notes the build it opened (each `.olean`'s size and time, the manifest and the toolchain) and reads the new one when it has changed; the window's Verify, Why?, the project map and the blueprint check do the same.
 - A request to Lean left waiting when its server stopped could surface later as an error no one caught; the error now also names the request.

CONTRIBUTING.md

@@ -74,7 +74,14 @@ desktop session. It opens a real window, and checks that Lean's infoview renders
 dotnet tools/LeanStudio.Snapshot/bin/Release/net10.0/LeanStudio.Snapshot.dll --native-infoview . snapshots
 ```
 
-CI runs the build and tests on Linux, macOS and Windows, and runs the snapshot on Linux and macOS. Please make sure
+The text, Mathlib and Git commands of the Lean menu (Sort Imports, Tidy File, Sorry Burndown…) are run in the real
+window on real documents by a check that needs git but not Lean:
+
+```bash
+dotnet tools/LeanStudio.Snapshot/bin/Release/net10.0/LeanStudio.Snapshot.dll --commands
+```
+
+CI runs the build and tests on Linux, macOS and Windows, and runs the snapshot and that command check on Linux and macOS. Please make sure
 they pass locally first.
 
 ## What a good change looks like

Directory.Build.props

@@ -11,7 +11,7 @@
     <Product>Lean Studio</Product>
     <Copyright>Copyright (c) 2026 Keith Adler (@keithadler)</Copyright>
     <PackageLicenseExpression>MIT</PackageLicenseExpression>
-    <VersionPrefix>0.10.0</VersionPrefix>
+    <VersionPrefix>0.11.0</VersionPrefix>
   </PropertyGroup>
   <PropertyGroup>
     <AvaloniaVersion>12.1.3</AvaloniaVersion>

README.md

@@ -94,6 +94,8 @@ Most people write Lean in VS Code with the official lean4 extension, and it's ve
 | Why a theorem isn't fully proved, and a map of what rests on `sorry` | | ✓ |
 | A profiler: live as you edit, flame graphs, cost per tactic line, heartbeats, simp and instance counters, and a heartbeat regression check for CI | | ✓ |
 | Search Mathlib in plain English, and Loogle, built in | | ✓ |
+| Sorry Burndown: the project's `sorry` count over its last commits, from Git, and a branch's added, removed and restated theorems with proofs ignored, as Markdown for the pull request | | ✓ |
+| Mathlib housekeeping: sort imports, tidy whitespace, wrap long comments, add the copyright header, delete old deprecations, a Mathlib-style name for a theorem, theorems that state the same thing, a project health summary | | ✓ |
 | Proof walkthroughs as web pages; share links to the web editor | | ✓ |
 | A tutorial, goals read in English, errors explained, for people new to Lean | | ✓ |
 | C FFI: `@[extern]` checked against the C code, stubs, clangd | | ✓ |
@@ -328,6 +330,18 @@ The infoview shares Lean Studio's Lean server, so nothing starts twice. "Try thi
 What CI and reviewers check, before you push:
 
 - **Remove Unused Imports** (*Lean ▸ Remove Unused Imports*) takes out the imports a file doesn't need, as one undoable edit, and says why for each: nothing uses it, or another import already brings it in. Lean elaborates the file, and every constant, tactic, macro and notation it uses is traced to its module, so an import needed only for `ring` or a notation stays. It works on any file, not only `module` files like `lake shake`. It takes seconds on Mathlib files.
+- **Sort Imports** (*Lean ▸ Sort Imports*) puts each run of `import` lines in the header in order by module name and drops repeats, as Mathlib's style asks, leaving comments, blank-line groups and the body alone.
+- **Tidy Whitespace and Check Style** (*Lean ▸ Tidy Whitespace and Check Style*) holds a file to Mathlib's text rules: trailing whitespace, tabs, CRLF and the final newline are fixed in one undoable edit, and lines over 100 characters are listed for you to break.
+- **Tidy File** does Sort Imports and the whitespace fixes in one edit; in a Mathlib project it also reports a missing copyright header or module docstring and theorem names that start with a capital, and **Add Mathlib Copyright Header** writes the header for you.
+- **What This Branch Changed Mathematically** lists the theorems a branch adds, removes and restates since `main`, with proofs ignored, as Markdown for the pull request: what a reviewer reads first.
+- **Sorry Burndown** draws the project's `sorry` count over its last 30 commits as a sparkline and names the commits that moved it, straight from Git, with nothing built.
+- **Project Health Summary** counts the project's files into a report: size, sorries and TODOs, doc-comment coverage, deprecations and style problems, and where the most is left to do.
+- **Find Duplicate Theorem Statements** lists theorems of the project that state the same thing under different names, with each one's file and line.
+- **Merge Consecutive rw / intro Steps** turns `rw [a]` then `rw [b]` (or `simp_rw`, or two `intro`s) into one line, where that cannot change the proof.
+- **Suggest a Name for This Theorem** works out the name Mathlib's scheme would give a theorem from its statement (`a + b = b + a` is `add_comm`; `a ≤ b → b < c → a < c` is `lt_of_le_of_lt`) and says whether yours matches.
+- **Copy as a Zulip Message** (*File ▸ Copy as a Zulip Message*) puts the file in a `lean` fence with Lean's errors and warnings in a quote under it, ready to paste into the Lean Zulip chat.
+- **Wrap Long Comment Lines** breaks over-long `--` comments and docstring prose at a space, the one style problem Tidy leaves to you; code is never touched.
+- **Remove Deprecations Older Than Six Months** deletes the deprecated aliases whose `(since := "…")` is old enough, with their doc comments, in one undoable edit; Tidy File in a Mathlib project also lists public definitions with no doc comment.
 - **Lint File** runs the linters CI runs and lists what they find in Problems. In a Mathlib project that's Mathlib's standard set, its style linters among them. Wherever Batteries is available it also runs Batteries' environment linters: missing docstrings, `simp` normal form, unused arguments. Elsewhere it runs every linter Lean has.
 - **Renames keep the old name working.** After Rename Symbol on a declaration, Lean Studio offers to add `@[deprecated (since := "…")] alias old := new` after it, as Mathlib asks. Without Batteries it writes the core Lean equivalent.
 - **The library root stays complete.** A new file is added to its library's root file when that imports every module (as `Mathlib.lean` does), and a deleted one is taken out. *Import Every Module in the Library Root* adds any that are missing, like `lake exe mk_all`.
@@ -652,7 +666,7 @@ The build generates XML documentation for every project in `src/`, and a public
 
 ## Status
 
-Lean Studio is at **0.10**, and the [changelog](CHANGELOG.md) lists what's new since then. The whole workflow works end to end and is tested against real Lean 4.34. It has been used by hand on macOS; on Windows and Linux it is built and tested by CI. Known gaps:
+Lean Studio is at **0.11**, and the [changelog](CHANGELOG.md) lists what's new since then. The whole workflow works end to end and is tested against real Lean 4.34. It has been used by hand on macOS; on Windows and Linux it is built and tested by CI. Known gaps:
 
 - User widgets render in the Infoview tab, not in the Tactic State panel, which shows Lean's interactive text. On Linux the tab needs WebKitGTK; without it, widgets open in the browser.
 - Tenet's badges describe the last build. After you edit a file, rebuild to refresh them.