From 10942cd3245519a333d69e539388e422a7451f4b Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 3 Oct 2026 18:56:51 +0000 Subject: [PATCH 01/18] Tests: fuzzy matching and merge-conflict edge cases Co-Authored-By: Claude Sonnet 5.5 Claude-Session: https://claude.ai/code/session_01FF5AYRpU9TWeWY3CFh2ETw --- .../PickerAndConflictTests.cs | 77 +++++++++++++++++++ 1 file changed, 77 insertions(+) create mode 100644 tests/LeanStudio.Tests/PickerAndConflictTests.cs diff --git a/tests/LeanStudio.Tests/PickerAndConflictTests.cs b/tests/LeanStudio.Tests/PickerAndConflictTests.cs new file mode 100644 index 0000000..464ea69 --- /dev/null +++ b/tests/LeanStudio.Tests/PickerAndConflictTests.cs @@ -0,0 +1,77 @@ +using LeanStudio.Core.Editing; + +namespace LeanStudio.Tests; + +/// Edge cases of fuzzy matching and merge-conflict settling. +public sealed class PickerAndConflictTests +{ + [Fact] + public void AnEmptyQueryMatchesEverythingWithZero() + { + Assert.Equal(0, Fuzzy.Score("", "anything")); + Assert.Equal(0, Fuzzy.Score("", "")); + } + + [Theory] + [InlineData("ba", "ab")] // order matters + [InlineData("abcd", "abc")] // longer than the candidate + [InlineData("z", "")] + public void RejectsWhatDoesNotMatchInOrder(string query, string candidate) => Assert.Null(Fuzzy.Score(query, candidate)); + + [Fact] + public void IgnoresCaseAndSpacesInTheQuery() + { + Assert.NotNull(Fuzzy.Score("BASIC", "basic.lean")); + Assert.Equal(Fuzzy.Score("gtd", "Go to Definition"), Fuzzy.Score("g t d", "Go to Definition")); + } + + [Fact] + public void ScoresAnExactCaseAndAContiguousRunHigher() + { + Assert.True(Fuzzy.Score("a", "a") > Fuzzy.Score("A", "a")); + Assert.True(Fuzzy.Score("abc", "abc") > Fuzzy.Score("abc", "a_b_c")); + } + + [Fact] + public void FilterDropsNonMatchesAndPutsShorterTextFirstOnTies() + { + Assert.Equal(["a", "bb", "ccc"], Fuzzy.Filter(["bb", "a", "ccc"], "", s => s)); + Assert.Empty(Fuzzy.Filter(["alpha", "beta"], "zzz", s => s)); + } + + [Fact] + public void FindsAThreeWayConflictWithItsLabels() + { + const string text = "a\n<<<<<<< HEAD\nmine\n||||||| base\nold\n=======\ntheirs\n>>>>>>> feature\nz\n"; + ConflictBlock block = Assert.Single(MergeConflicts.Find(text)); + Assert.Equal(new ConflictBlock(1, 3, 5, 7, "HEAD", "feature"), block); + Assert.Equal((2, 3), block.Mine); + Assert.Equal((6, 7), block.Theirs); + Assert.Equal("a\nmine\nz\n", MergeConflicts.Resolve(text, block, ConflictChoice.Mine)); + Assert.Equal("a\ntheirs\nz\n", MergeConflicts.Resolve(text, block, ConflictChoice.Theirs)); + Assert.Equal("a\nmine\ntheirs\nz\n", MergeConflicts.Resolve(text, block, ConflictChoice.Both)); // the ancestor's side is dropped + } + + [Fact] + public void SettlesAConflictWithAnEmptySideAndNoLabels() + { + const string text = "<<<<<<<\n=======\nx\n>>>>>>>\n"; + ConflictBlock block = Assert.Single(MergeConflicts.Find(text)); + Assert.Equal("", block.MineLabel); + Assert.Equal("", block.TheirsLabel); + Assert.Equal("", MergeConflicts.Resolve(text, block, ConflictChoice.Mine)); + Assert.Equal("x\n", MergeConflicts.Resolve(text, block, ConflictChoice.Theirs)); + Assert.Equal("x\n", MergeConflicts.Resolve(text, block, ConflictChoice.Both)); + } + + [Fact] + public void FindsSeveralConflictsInOrderAndTrimsCarriageReturnsFromLabels() + { + const string text = "<<<<<<< HEAD\r\na\r\n=======\r\nb\r\n>>>>>>> topic\r\nmid\r\n<<<<<<< HEAD\r\nc\r\n=======\r\nd\r\n>>>>>>> topic\r\n"; + IReadOnlyList blocks = MergeConflicts.Find(text); + Assert.Equal(2, blocks.Count); + Assert.Equal(0, blocks[0].Start); + Assert.Equal(6, blocks[1].Start); + Assert.All(blocks, b => Assert.Equal(("HEAD", "topic"), (b.MineLabel, b.TheirsLabel))); + } +} From 53923a764ed596d808d3bfdb0c6c80fa270c8985 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 3 Oct 2026 19:01:34 +0000 Subject: [PATCH 02/18] Add Sort Imports: order a file's import header the way Mathlib's style asks Co-Authored-By: Claude Sonnet 5.5 Claude-Session: https://claude.ai/code/session_01FF5AYRpU9TWeWY3CFh2ETw --- CHANGELOG.md | 3 + README.md | 1 + .../ViewModels/MainViewModel.Pro.cs | 32 +++++++++ src/LeanStudio.App/Views/MainWindow.axaml | 1 + src/LeanStudio.App/Views/MainWindow.axaml.cs | 1 + src/LeanStudio.Core/Workflow/ImportOrder.cs | 69 +++++++++++++++++++ .../PickerAndConflictTests.cs | 31 +++++++++ 7 files changed, 138 insertions(+) create mode 100644 src/LeanStudio.Core/Workflow/ImportOrder.cs diff --git a/CHANGELOG.md b/CHANGELOG.md index ce6ce70..4d23bec 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -14,6 +14,9 @@ - **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. + **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. diff --git a/README.md b/README.md index ec3554d..293076f 100644 --- a/README.md +++ b/README.md @@ -328,6 +328,7 @@ 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. - **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`. diff --git a/src/LeanStudio.App/ViewModels/MainViewModel.Pro.cs b/src/LeanStudio.App/ViewModels/MainViewModel.Pro.cs index d749570..aa71afe 100644 --- a/src/LeanStudio.App/ViewModels/MainViewModel.Pro.cs +++ b/src/LeanStudio.App/ViewModels/MainViewModel.Pro.cs @@ -412,6 +412,38 @@ public async Task ShowImportGraphAsync() } } + /// + /// Put the active file's imports in order, as Mathlib's style asks: each run in the header sorted by module name, + /// repeats dropped. Only the changed lines are replaced, as one undoable edit, so the cursor and folds stay put. + /// + [RelayCommand] + public void SortImports() + { + if (ActiveDocument is not { IsLean: true } d) + { + return; + } + string text = d.Document.Text; + string sorted = ImportOrder.Sort(text); + if (sorted == text) + { + Log("Imports: already in order."); + return; + } + int head = 0; + while (head < text.Length && head < sorted.Length && text[head] == sorted[head]) + { + head++; + } + int tail = 0; + while (tail < text.Length - head && tail < sorted.Length - head && text[text.Length - 1 - tail] == sorted[sorted.Length - 1 - tail]) + { + tail++; + } + d.Document.Replace(head, text.Length - head - tail, sorted.Substring(head, sorted.Length - head - tail)); + Log("Imports: sorted. Undo brings the old order back."); + } + // ---- linters ---- /// diff --git a/src/LeanStudio.App/Views/MainWindow.axaml b/src/LeanStudio.App/Views/MainWindow.axaml index 0e8527e..81a057c 100644 --- a/src/LeanStudio.App/Views/MainWindow.axaml +++ b/src/LeanStudio.App/Views/MainWindow.axaml @@ -129,6 +129,7 @@ + diff --git a/src/LeanStudio.App/Views/MainWindow.axaml.cs b/src/LeanStudio.App/Views/MainWindow.axaml.cs index c57c3a6..b92c154 100644 --- a/src/LeanStudio.App/Views/MainWindow.axaml.cs +++ b/src/LeanStudio.App/Views/MainWindow.axaml.cs @@ -1079,6 +1079,7 @@ private void OnLocationDoubleTapped(object? sender, TappedEventArgs e) yield return ("Lean: Instances of Class at Cursor…", "", InstancesOfClassAsync); yield return ("Lean: Lean's Processes (memory, stop a runaway file)…", "", LeanProcessesAsync); yield return ("Lean: Remove Unused Imports", "", Cmd(_vm.RemoveUnusedImportsCommand)); + yield return ("Lean: Sort Imports", "", Cmd(_vm.SortImportsCommand)); yield return ("Lean: Lint File (the linters CI runs)", "", Cmd(_vm.LintFileCommand)); yield return ("Lean: Import Every Module in the Library Root", "", Cmd(_vm.ImportAllModulesCommand)); yield return ("Lean: Get Mathlib Cache for Open Files", "", Cmd(_vm.GetCacheForOpenFilesCommand)); diff --git a/src/LeanStudio.Core/Workflow/ImportOrder.cs b/src/LeanStudio.Core/Workflow/ImportOrder.cs new file mode 100644 index 0000000..50aaab6 --- /dev/null +++ b/src/LeanStudio.Core/Workflow/ImportOrder.cs @@ -0,0 +1,69 @@ +using System.Text.RegularExpressions; + +namespace LeanStudio.Core.Workflow; + +/// +/// Putting a file's imports in order, as Mathlib's style asks: each run of consecutive import lines in the +/// file's header sorted by module name, with repeated lines dropped. Only the header is touched: it ends at the first +/// line that is neither an import, blank nor a comment, so nothing in the body moves. Blank lines and comments between +/// runs stay where they are, which keeps a deliberate grouping. +/// +public static class ImportOrder +{ + private static readonly Regex ImportLine = new(@"^\s*(?:(?:public|private|meta)\s+)*import\s+(?:all\s+)?(?\S+)", RegexOptions.Compiled); + + /// with the runs of imports in its header sorted. Unchanged when they already are. + public static string Sort(string text) + { + string[] lines = text.Split('\n'); + int i = 0; + int blockComment = 0; + var output = new List(lines.Length); + while (i < lines.Length) + { + string line = lines[i]; + string t = line.Trim(); + if (blockComment > 0 || t.StartsWith("/-", StringComparison.Ordinal)) + { + // A block comment (the copyright header, or `/-! … -/`): skip it whole, nested ones included. + for (int k = 0; k + 1 < t.Length; k++) + { + if (k + 1 < t.Length && t[k] == '/' && t[k + 1] == '-') + { + blockComment++; + k++; + } + else if (k + 1 < t.Length && t[k] == '-' && t[k + 1] == '/') + { + blockComment--; + k++; + } + } + output.Add(line); + i++; + continue; + } + if (t.Length == 0 || t.StartsWith("--", StringComparison.Ordinal) || t == "module" || t == "prelude") + { + output.Add(line); + i++; + continue; + } + if (!ImportLine.IsMatch(line)) + { + break; // the body begins + } + int start = i; + while (i < lines.Length && ImportLine.IsMatch(lines[i])) + { + i++; + } + var seen = new HashSet(StringComparer.Ordinal); + output.AddRange(lines[start..i] + .OrderBy(l => ImportLine.Match(l).Groups["m"].Value, StringComparer.Ordinal) + .Where(l => seen.Add(l.Trim()))); + } + output.AddRange(lines[i..]); + return string.Join('\n', output); + } +} diff --git a/tests/LeanStudio.Tests/PickerAndConflictTests.cs b/tests/LeanStudio.Tests/PickerAndConflictTests.cs index 464ea69..442508a 100644 --- a/tests/LeanStudio.Tests/PickerAndConflictTests.cs +++ b/tests/LeanStudio.Tests/PickerAndConflictTests.cs @@ -1,4 +1,5 @@ using LeanStudio.Core.Editing; +using LeanStudio.Core.Workflow; namespace LeanStudio.Tests; @@ -75,3 +76,33 @@ public void FindsSeveralConflictsInOrderAndTrimsCarriageReturnsFromLabels() Assert.All(blocks, b => Assert.Equal(("HEAD", "topic"), (b.MineLabel, b.TheirsLabel))); } } + +/// Sorting the imports of a file's header. +public sealed class ImportOrderTests +{ + [Fact] + public void SortsTheRunByModuleNameAndDropsRepeats() + { + const string text = "import Mathlib.Data.Nat.Basic\nimport Batteries\nimport Mathlib.Data.Nat\nimport Batteries\n\ntheorem t : True := trivial\n"; + Assert.Equal("import Batteries\nimport Mathlib.Data.Nat\nimport Mathlib.Data.Nat.Basic\n\ntheorem t : True := trivial\n", ImportOrder.Sort(text)); + } + + [Fact] + public void KeepsGroupsApartAndLeavesTheBodyAlone() + { + const string text = "/-\nCopyright (c) me\n-/\nimport B\nimport A\n\n-- the others\nimport D\nimport C\n\nimport Z\nimport Y -- keeps its comment\n"; + Assert.Equal("/-\nCopyright (c) me\n-/\nimport A\nimport B\n\n-- the others\nimport C\nimport D\n\nimport Y -- keeps its comment\nimport Z\n", ImportOrder.Sort(text)); + const string body = "import B\ndef f := 1\nimport A\n"; + Assert.Equal(body, ImportOrder.Sort(body)); // an import after the header's end is not part of it + } + + [Fact] + public void KeepsModifiersLineEndingsAndAnAlreadySortedFile() + { + Assert.Equal("module\n\npublic import A\nimport all B\n", ImportOrder.Sort("module\n\nimport all B\npublic import A\n")); + Assert.Equal("import A\r\nimport B\r\n", ImportOrder.Sort("import B\r\nimport A\r\n")); + const string sorted = "import A\nimport B\n"; + Assert.Equal(sorted, ImportOrder.Sort(sorted)); + Assert.Equal("", ImportOrder.Sort("")); + } +} From dcdd46c72dc1b4a6b72ceccece2ccc2669424a74 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 3 Oct 2026 19:03:28 +0000 Subject: [PATCH 03/18] Add Tidy Whitespace and Check Style, and sort_imports/style_check for assistants Co-Authored-By: Claude Sonnet 5.5 Claude-Session: https://claude.ai/code/session_01FF5AYRpU9TWeWY3CFh2ETw --- CHANGELOG.md | 2 + README.md | 1 + docs/ARCHITECTURE.md | 4 +- .../ViewModels/MainViewModel.Pro.cs | 32 +++++++ src/LeanStudio.App/Views/MainWindow.axaml | 1 + src/LeanStudio.App/Views/MainWindow.axaml.cs | 1 + src/LeanStudio.Core/Workflow/StyleCheck.cs | 78 +++++++++++++++++ src/LeanStudio.Mcp/LeanTools.cs | 50 +++++++++++ .../PickerAndConflictTests.cs | 86 +++++++++++++++++++ 9 files changed, 253 insertions(+), 2 deletions(-) create mode 100644 src/LeanStudio.Core/Workflow/StyleCheck.cs diff --git a/CHANGELOG.md b/CHANGELOG.md index 4d23bec..0baab14 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -16,6 +16,8 @@ **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. +- **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. diff --git a/README.md b/README.md index 293076f..92cfd4d 100644 --- a/README.md +++ b/README.md @@ -329,6 +329,7 @@ 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. - **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`. diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index ca5c4c6..e8c53e5 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -129,7 +129,7 @@ shows them to a person or an assistant. | [`Proofs/`](../src/LeanStudio.Core/Proofs) | Features that ask Lean about proofs: `ProofSteps` (the tactic block around a line, read by layout), `ProofSearch` (Prove It and counterexamples) and `Scratch` (scratch documents in the running server), `ExtractLemma`, `Profiler` (Lean's profilers read into a `ProfileReport`: trees, categories, counters, per-line costs; its records are in `ProfileModel`), `LiveProfiler` (the same, from the running server as the file is edited), `ProfileCheck` (saved profiles in `ProfileStore`, and the heartbeat regression check), `Heartbeats`, `ProofStates` (the Proof-State Map), `Walkthrough` (the HTML export) and `LeanRepl`. | | [`Ai/`](../src/LeanStudio.Core/Ai) | The AI in the editor: `IChatModel` and the clients behind it (`AppleIntelligence` and `AppleFmCliModel` for the `fm` command, `OllamaModel`, `OpenAiCompatibleModel`, `AnthropicModel`), `AiDiscovery` (what is running, and which model to use), `AiProver` (proofs from a model, checked by Lean), `AiAssistant` (explanations and chat), `AiText` (token estimates and trimming) and `SecretStore` (API keys). | | [`Editing/`](../src/LeanStudio.Core/Editing) | Text-level engines with no UI: `Abbreviations` (Unicode input), `LeanText` (comments, strings and declarations in Lean source), `LatexText` (docstring math as text), `Fuzzy` (picker matching), `ProjectSearch` (find and replace across files), `MultiCursor`, `VimEngine`, `EmacsEngine` and `KeyBindingsFile` (keybindings.json). The editor in the app is a thin host over them. | -| [`Workflow/`](../src/LeanStudio.Core/Workflow) | Project-wide tools. `Workflow.cs` holds `Markers` (sorries and TODOs), `LakeOutput` (build problems), `LocalHistory`, `Loogle`, `LeanSearch`, `DocLinks`, `Blame` and `ProjectTasks`. Beside it: `Refactor` and `EmittedC` (module rename, replace across files, Compiled C), `Ffi` (`@[extern]` bindings checked against the project's C files, and C stubs), `ImportCheck` (unused imports), `Lint`, `Instances`, `Deprecation` (deprecated aliases for renames), `DependencyBump` (Update Mathlib and see what broke), `Blueprint`, `ProjectCommands` (`.leanstudio/commands.json`), `ProgressReader` (progress read from what a task prints), `LeanCli` (the `lean` command line on a mirror copy) and `Essentials.cs` (`ElanInstaller`, `FileOps`, `ImportFinder`). | +| [`Workflow/`](../src/LeanStudio.Core/Workflow) | Project-wide tools. `Workflow.cs` holds `Markers` (sorries and TODOs), `LakeOutput` (build problems), `LocalHistory`, `Loogle`, `LeanSearch`, `DocLinks`, `Blame` and `ProjectTasks`. Beside it: `Refactor` and `EmittedC` (module rename, replace across files, Compiled C), `Ffi` (`@[extern]` bindings checked against the project's C files, and C stubs), `ImportCheck` (unused imports), `ImportOrder` (sorted imports), `StyleCheck` (Mathlib's text rules), `Lint`, `Instances`, `Deprecation` (deprecated aliases for renames), `DependencyBump` (Update Mathlib and see what broke), `Blueprint`, `ProjectCommands` (`.leanstudio/commands.json`), `ProgressReader` (progress read from what a task prints), `LeanCli` (the `lean` command line on a mirror copy) and `Essentials.cs` (`ElanInstaller`, `FileOps`, `ImportFinder`). | | [`Git/`](../src/LeanStudio.Core/Git) | `GitRepository` wraps your own `git` executable, so your config, hooks, credentials and signing all apply. `GitHub` goes through the `gh` CLI, so Lean Studio never handles a token. | | [`Learn/`](../src/LeanStudio.Core/Learn) | `Tutorial` and `Playground`; `TacticGuide`, `ErrorGuide` and `PlainEnglish` (goals read aloud) in `Guides.cs`; `Snippets`, `TheoremGallery` and `ProgramRunner` in `Library.cs`. | | [`Agents/`](../src/LeanStudio.Core/Agents) | For assistants and web pages: `Workbench` and `ProjectSession` (Lean for a program instead of a person, used by the MCP server), `StudioBridge` (the pipe between an assistant and an open window), `InfoviewBridge` (Lean's own infoview page, served to a web view or browser) and `AgentSetup` (writing each assistant's MCP configuration). | @@ -174,7 +174,7 @@ written to stdout. | Checking and reading a file | `project_info`, `check_file`, `goals`, `proof_steps`, `hover`, `suggestions`, `references`, `run_lean` | | Building and Tenet | `build`, `verify`, `axioms`, `why_not_proved`, `project_map` | | Proof tools | `prove`, `extract_lemma`, `ffi_bindings`, `profile` | -| For Mathlib contributors | `unused_imports`, `lint`, `heartbeats`, `instances`, `blueprint` | +| For Mathlib contributors | `unused_imports`, `sort_imports`, `style_check`, `lint`, `heartbeats`, `instances`, `blueprint` | | Walkthroughs and search | `export_walkthrough`, `search_mathlib`, and `declaration` and `search_declarations` (the compiled library, through Tenet) | | Toolchains | `toolchains` | | The open window | `studio_context`, `studio_show` | diff --git a/src/LeanStudio.App/ViewModels/MainViewModel.Pro.cs b/src/LeanStudio.App/ViewModels/MainViewModel.Pro.cs index aa71afe..c8de415 100644 --- a/src/LeanStudio.App/ViewModels/MainViewModel.Pro.cs +++ b/src/LeanStudio.App/ViewModels/MainViewModel.Pro.cs @@ -444,6 +444,38 @@ public void SortImports() Log("Imports: sorted. Undo brings the old order back."); } + /// + /// Check the active file against Mathlib's text rules (trailing whitespace, lines over 100 characters, tabs, line + /// endings, the final newline), listing what is wrong in Output, and fix what has one obvious fix as one undoable edit. + /// + [RelayCommand] + public void TidyWhitespace() + { + if (ActiveDocument is not { IsLean: true } d) + { + return; + } + string text = d.Document.Text; + IReadOnlyList problems = StyleCheck.Find(text); + if (problems.Count == 0) + { + Log("Style: no problems."); + return; + } + string fixedText = StyleCheck.Fix(text); + if (fixedText != text) + { + d.Document.Replace(0, text.Length, fixedText); + } + foreach (StyleProblem p in problems.Where(p => p.Rule == "long-line")) + { + Log($" line {p.Line + 1}: {p.Message}"); + } + int left = problems.Count(p => p.Rule == "long-line"); + Log($"Style: fixed {problems.Count - left} problem{(problems.Count - left == 1 ? "" : "s")}" + + (left > 0 ? $"; {left} long line{(left == 1 ? "" : "s")} left for you." : ".") + " Undo brings the old text back."); + } + // ---- linters ---- /// diff --git a/src/LeanStudio.App/Views/MainWindow.axaml b/src/LeanStudio.App/Views/MainWindow.axaml index 81a057c..a5b7e19 100644 --- a/src/LeanStudio.App/Views/MainWindow.axaml +++ b/src/LeanStudio.App/Views/MainWindow.axaml @@ -130,6 +130,7 @@ + diff --git a/src/LeanStudio.App/Views/MainWindow.axaml.cs b/src/LeanStudio.App/Views/MainWindow.axaml.cs index b92c154..2c7b8f4 100644 --- a/src/LeanStudio.App/Views/MainWindow.axaml.cs +++ b/src/LeanStudio.App/Views/MainWindow.axaml.cs @@ -1080,6 +1080,7 @@ private void OnLocationDoubleTapped(object? sender, TappedEventArgs e) yield return ("Lean: Lean's Processes (memory, stop a runaway file)…", "", LeanProcessesAsync); yield return ("Lean: Remove Unused Imports", "", Cmd(_vm.RemoveUnusedImportsCommand)); yield return ("Lean: Sort Imports", "", Cmd(_vm.SortImportsCommand)); + yield return ("Lean: Tidy Whitespace and Check Style", "", Cmd(_vm.TidyWhitespaceCommand)); yield return ("Lean: Lint File (the linters CI runs)", "", Cmd(_vm.LintFileCommand)); yield return ("Lean: Import Every Module in the Library Root", "", Cmd(_vm.ImportAllModulesCommand)); yield return ("Lean: Get Mathlib Cache for Open Files", "", Cmd(_vm.GetCacheForOpenFilesCommand)); diff --git a/src/LeanStudio.Core/Workflow/StyleCheck.cs b/src/LeanStudio.Core/Workflow/StyleCheck.cs new file mode 100644 index 0000000..2d03510 --- /dev/null +++ b/src/LeanStudio.Core/Workflow/StyleCheck.cs @@ -0,0 +1,78 @@ +namespace LeanStudio.Core.Workflow; + +/// One style problem in a file's text. +/// 0-based line. +/// A short name: trailing-whitespace, long-line, tab, crlf or final-newline. +/// What is wrong, for a person. +public sealed record StyleProblem(int Line, string Rule, string Message); + +/// +/// The text rules Mathlib's CI holds a file to (lake exe lint-style): no trailing whitespace, no line over 100 +/// characters, no tabs, Unix line endings and exactly one newline at the end. Finding the problems, and fixing the +/// ones that have one obvious fix (everything but a long line, which is a person's to break). +/// +public static class StyleCheck +{ + /// The longest line Mathlib allows, in characters. + public const int MaxLineLength = 100; + + /// Every problem in , in line order. + public static IReadOnlyList Find(string text) + { + var problems = new List(); + string[] lines = text.Split('\n'); + bool crlf = false; + for (int i = 0; i < lines.Length; i++) + { + string line = lines[i]; + if (line.EndsWith('\r')) + { + crlf = true; + line = line[..^1]; + } + if (line.Length > 0 && line[^1] is ' ' or '\t') + { + problems.Add(new StyleProblem(i, "trailing-whitespace", "Trailing whitespace.")); + } + if (line.Contains('\t')) + { + problems.Add(new StyleProblem(i, "tab", "A tab: Lean files are indented with spaces.")); + } + int length = new System.Globalization.StringInfo(line).LengthInTextElements; + if (length > MaxLineLength) + { + problems.Add(new StyleProblem(i, "long-line", $"{length} characters; the limit is {MaxLineLength}.")); + } + } + if (crlf) + { + problems.Add(new StyleProblem(0, "crlf", "Windows line endings (CRLF); use LF.")); + } + if (text.Length > 0 && !text.EndsWith('\n')) + { + problems.Add(new StyleProblem(lines.Length - 1, "final-newline", "The file does not end with a newline.")); + } + else if (text.EndsWith("\n\n", StringComparison.Ordinal) || text.EndsWith("\r\n\r\n", StringComparison.Ordinal)) + { + problems.Add(new StyleProblem(lines.Length - 2, "final-newline", "More than one newline at the end of the file.")); + } + return problems; + } + + /// + /// with what has one obvious fix fixed: line endings made LF, trailing whitespace + /// removed, tabs turned into two spaces, and exactly one newline at the end (none for an empty file). + /// Long lines are left for a person. + /// + public static string Fix(string text) + { + if (text.Length == 0) + { + return text; + } + IEnumerable lines = text.Replace("\r\n", "\n", StringComparison.Ordinal).Split('\n') + .Select(l => l.Replace("\t", " ", StringComparison.Ordinal).TrimEnd(' ')); + string body = string.Join('\n', lines).TrimEnd('\n'); + return body.Length == 0 ? "" : body + "\n"; + } +} diff --git a/src/LeanStudio.Mcp/LeanTools.cs b/src/LeanStudio.Mcp/LeanTools.cs index 48c6492..dc13451 100644 --- a/src/LeanStudio.Mcp/LeanTools.cs +++ b/src/LeanStudio.Mcp/LeanTools.cs @@ -695,6 +695,56 @@ public static IReadOnlyList Tools(Workbench bench) => return sb.ToString().TrimEnd(); }), + new("sort_imports", + "Put the imports in a Lean file's header in order, as Mathlib's style asks: each run of import lines sorted by module name, repeats dropped, comments and the body untouched. Returns the sorted header; with apply=true, writes the file on disk.", + Schema(("path", "string", "The .lean file.", true), + ("apply", "boolean", "Write the sorted file to disk (default false).", false)), + async (a, ct) => + { + string path = LeanFile(bench, a); + string text = await File.ReadAllTextAsync(path, ct); + string sorted = ImportOrder.Sort(text); + if (sorted == text) + { + return "the imports are already in order"; + } + if (OptBool(a, "apply") == true) + { + await File.WriteAllTextAsync(path, sorted, ct); + return "sorted the imports of " + path; + } + return "would sort the imports (pass apply=true to write them):\n" + + string.Join('\n', sorted.Split('\n').Where(l => l.TrimStart().StartsWith("import ", StringComparison.Ordinal) + || l.TrimStart().StartsWith("public import ", StringComparison.Ordinal))); + }), + + new("style_check", + "Check a Lean file against the text rules Mathlib's CI holds it to: no trailing whitespace, no line over 100 characters, no tabs, LF line endings, exactly one newline at the end. With apply=true, fixes what has one obvious fix (everything but long lines) on disk.", + Schema(("path", "string", "The .lean file.", true), + ("apply", "boolean", "Fix the fixable problems on disk (default false).", false)), + async (a, ct) => + { + string path = LeanFile(bench, a); + string text = await File.ReadAllTextAsync(path, ct); + IReadOnlyList problems = StyleCheck.Find(text); + if (problems.Count == 0) + { + return "no style problems"; + } + var sb = new StringBuilder(); + foreach (StyleProblem p in problems) + { + sb.Append(CultureInfo.InvariantCulture, $"{path}:{p.Line + 1}: {p.Rule}: {p.Message}\n"); + } + if (OptBool(a, "apply") == true) + { + await File.WriteAllTextAsync(path, StyleCheck.Fix(text), ct); + int left = problems.Count(p => p.Rule == "long-line"); + sb.Append(CultureInfo.InvariantCulture, $"fixed {problems.Count - left} problem(s); {left} long line(s) are left for you"); + } + return sb.ToString().TrimEnd(); + }), + new("lint", "Run the linters CI runs on a Lean file of a Lake project: Mathlib's standard set in a project that uses Mathlib (its style linters among them), every linter Lean has elsewhere, and Batteries' environment linters (missing docstrings, simp normal form, unused arguments…) where Batteries is available. Lints the file as saved on disk.", Schema(("path", "string", "The .lean file.", true)), diff --git a/tests/LeanStudio.Tests/PickerAndConflictTests.cs b/tests/LeanStudio.Tests/PickerAndConflictTests.cs index 442508a..d70afff 100644 --- a/tests/LeanStudio.Tests/PickerAndConflictTests.cs +++ b/tests/LeanStudio.Tests/PickerAndConflictTests.cs @@ -106,3 +106,89 @@ public void KeepsModifiersLineEndingsAndAnAlreadySortedFile() Assert.Equal("", ImportOrder.Sort("")); } } + +/// The text rules of Mathlib's style linter. +public sealed class StyleCheckTests +{ + [Fact] + public void FindsEachKindOfProblemAtItsLine() + { + string text = "def a := 1 \n\tdef b := 2\n-- " + new string('x', 100) + "\ndef c := 3"; + IReadOnlyList found = StyleCheck.Find(text); + Assert.Equal([(0, "trailing-whitespace"), (1, "tab"), (2, "long-line"), (3, "final-newline")], found.Select(p => (p.Line, p.Rule))); + Assert.Contains("103 characters", found[2].Message); + } + + [Fact] + public void AcceptsACleanFileAndALineOfExactlyTheLimit() + { + Assert.Empty(StyleCheck.Find("def a := 1\n-- " + new string('x', 97) + "\n")); + Assert.Empty(StyleCheck.Find("")); + } + + [Fact] + public void ReportsCrlfAndExtraFinalNewlines() + { + Assert.Equal(["crlf"], StyleCheck.Find("a\r\nb\r\n").Select(p => p.Rule)); + Assert.Equal([(1, "final-newline")], StyleCheck.Find("a\n\n").Select(p => (p.Line, p.Rule))); + } + + [Fact] + public void FixesWhatHasOneFixAndLeavesLongLinesAlone() + { + Assert.Equal("a\n b\nc\n", StyleCheck.Fix("a \r\n\tb\t\r\nc\n\n\n")); + Assert.Equal("a\n", StyleCheck.Fix("a")); + string longLine = "-- " + new string('y', 120) + "\n"; + Assert.Equal(longLine, StyleCheck.Fix(longLine)); + Assert.Equal("", StyleCheck.Fix("")); + Assert.Empty(StyleCheck.Find(StyleCheck.Fix("x \t\r\n\r\n\r\ny"))); + } +} + +/// The text tools assistants get over MCP; they need no running Lean. +public sealed class TextToolTests +{ + [Fact] + public async Task AssistantsCanSortImportsAndCheckStyle() + { + string dir = Directory.CreateTempSubdirectory("leanstudio-text-").FullName; + try + { + string file = Path.Combine(dir, "A.lean"); + await File.WriteAllTextAsync(file, "import B\nimport A \n\ndef x := 1\t", TestContext.Current.CancellationToken); + await using var bench = new Core.Agents.Workbench(dir); + Mcp.McpServer server = Mcp.LeanTools.Create(bench, "test"); + async Task Call(string tool, System.Text.Json.Nodes.JsonObject args) + { + var r = await server.HandleAsync(new System.Text.Json.Nodes.JsonObject + { + ["jsonrpc"] = "2.0", ["id"] = 1, ["method"] = "tools/call", + ["params"] = new System.Text.Json.Nodes.JsonObject { ["name"] = tool, ["arguments"] = args }, + }, TestContext.Current.CancellationToken); + var result = r!["result"]!; + Assert.False(result["isError"]?.GetValue() ?? false, result.ToJsonString()); + return result["content"]![0]!["text"]!.GetValue(); + } + + string preview = await Call("sort_imports", new() { ["path"] = file }); + Assert.Contains("import A \nimport B", preview, StringComparison.Ordinal); + Assert.StartsWith("import B\n", await File.ReadAllTextAsync(file, TestContext.Current.CancellationToken), StringComparison.Ordinal); // not written + + await Call("sort_imports", new() { ["path"] = file, ["apply"] = true }); + Assert.StartsWith("import A \nimport B\n", await File.ReadAllTextAsync(file, TestContext.Current.CancellationToken), StringComparison.Ordinal); + Assert.Contains("already in order", await Call("sort_imports", new() { ["path"] = file, ["apply"] = true }), StringComparison.Ordinal); + + string report = await Call("style_check", new() { ["path"] = file }); + Assert.Contains("A.lean:1: trailing-whitespace", report, StringComparison.Ordinal); + Assert.Contains("A.lean:4: tab", report, StringComparison.Ordinal); + Assert.Contains("final-newline", report, StringComparison.Ordinal); + await Call("style_check", new() { ["path"] = file, ["apply"] = true }); + Assert.Equal("import A\nimport B\n\ndef x := 1\n", await File.ReadAllTextAsync(file, TestContext.Current.CancellationToken)); + Assert.Equal("no style problems", await Call("style_check", new() { ["path"] = file })); + } + finally + { + Directory.Delete(dir, true); + } + } +} From 152726113d7ed00384c89515cb388955529ee4fc Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 3 Oct 2026 19:05:09 +0000 Subject: [PATCH 04/18] Add Tidy File, Mathlib file conventions and an Add Mathlib Copyright Header command Co-Authored-By: Claude Sonnet 5.5 Claude-Session: https://claude.ai/code/session_01FF5AYRpU9TWeWY3CFh2ETw --- CHANGELOG.md | 2 + README.md | 1 + docs/ARCHITECTURE.md | 2 +- .../ViewModels/MainViewModel.Pro.cs | 58 +++++++++++++++++ src/LeanStudio.App/Views/MainWindow.axaml | 2 + src/LeanStudio.App/Views/MainWindow.axaml.cs | 2 + .../Workflow/MathlibConventions.cs | 63 +++++++++++++++++++ src/LeanStudio.Mcp/LeanTools.cs | 13 ++-- .../PickerAndConflictTests.cs | 40 ++++++++++++ 9 files changed, 177 insertions(+), 6 deletions(-) create mode 100644 src/LeanStudio.Core/Workflow/MathlibConventions.cs diff --git a/CHANGELOG.md b/CHANGELOG.md index 0baab14..f2d53ed 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -17,6 +17,8 @@ **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. - **Over MCP**, `sort_imports` and `style_check` do the same for assistants, each with `apply` to write the file. **Fixes**: diff --git a/README.md b/README.md index 92cfd4d..0aea10c 100644 --- a/README.md +++ b/README.md @@ -330,6 +330,7 @@ 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. - **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`. diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index e8c53e5..23c88b4 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -129,7 +129,7 @@ shows them to a person or an assistant. | [`Proofs/`](../src/LeanStudio.Core/Proofs) | Features that ask Lean about proofs: `ProofSteps` (the tactic block around a line, read by layout), `ProofSearch` (Prove It and counterexamples) and `Scratch` (scratch documents in the running server), `ExtractLemma`, `Profiler` (Lean's profilers read into a `ProfileReport`: trees, categories, counters, per-line costs; its records are in `ProfileModel`), `LiveProfiler` (the same, from the running server as the file is edited), `ProfileCheck` (saved profiles in `ProfileStore`, and the heartbeat regression check), `Heartbeats`, `ProofStates` (the Proof-State Map), `Walkthrough` (the HTML export) and `LeanRepl`. | | [`Ai/`](../src/LeanStudio.Core/Ai) | The AI in the editor: `IChatModel` and the clients behind it (`AppleIntelligence` and `AppleFmCliModel` for the `fm` command, `OllamaModel`, `OpenAiCompatibleModel`, `AnthropicModel`), `AiDiscovery` (what is running, and which model to use), `AiProver` (proofs from a model, checked by Lean), `AiAssistant` (explanations and chat), `AiText` (token estimates and trimming) and `SecretStore` (API keys). | | [`Editing/`](../src/LeanStudio.Core/Editing) | Text-level engines with no UI: `Abbreviations` (Unicode input), `LeanText` (comments, strings and declarations in Lean source), `LatexText` (docstring math as text), `Fuzzy` (picker matching), `ProjectSearch` (find and replace across files), `MultiCursor`, `VimEngine`, `EmacsEngine` and `KeyBindingsFile` (keybindings.json). The editor in the app is a thin host over them. | -| [`Workflow/`](../src/LeanStudio.Core/Workflow) | Project-wide tools. `Workflow.cs` holds `Markers` (sorries and TODOs), `LakeOutput` (build problems), `LocalHistory`, `Loogle`, `LeanSearch`, `DocLinks`, `Blame` and `ProjectTasks`. Beside it: `Refactor` and `EmittedC` (module rename, replace across files, Compiled C), `Ffi` (`@[extern]` bindings checked against the project's C files, and C stubs), `ImportCheck` (unused imports), `ImportOrder` (sorted imports), `StyleCheck` (Mathlib's text rules), `Lint`, `Instances`, `Deprecation` (deprecated aliases for renames), `DependencyBump` (Update Mathlib and see what broke), `Blueprint`, `ProjectCommands` (`.leanstudio/commands.json`), `ProgressReader` (progress read from what a task prints), `LeanCli` (the `lean` command line on a mirror copy) and `Essentials.cs` (`ElanInstaller`, `FileOps`, `ImportFinder`). | +| [`Workflow/`](../src/LeanStudio.Core/Workflow) | Project-wide tools. `Workflow.cs` holds `Markers` (sorries and TODOs), `LakeOutput` (build problems), `LocalHistory`, `Loogle`, `LeanSearch`, `DocLinks`, `Blame` and `ProjectTasks`. Beside it: `Refactor` and `EmittedC` (module rename, replace across files, Compiled C), `Ffi` (`@[extern]` bindings checked against the project's C files, and C stubs), `ImportCheck` (unused imports), `ImportOrder` (sorted imports), `StyleCheck` (Mathlib's text rules), `MathlibConventions` (header, module docstring, theorem names), `Lint`, `Instances`, `Deprecation` (deprecated aliases for renames), `DependencyBump` (Update Mathlib and see what broke), `Blueprint`, `ProjectCommands` (`.leanstudio/commands.json`), `ProgressReader` (progress read from what a task prints), `LeanCli` (the `lean` command line on a mirror copy) and `Essentials.cs` (`ElanInstaller`, `FileOps`, `ImportFinder`). | | [`Git/`](../src/LeanStudio.Core/Git) | `GitRepository` wraps your own `git` executable, so your config, hooks, credentials and signing all apply. `GitHub` goes through the `gh` CLI, so Lean Studio never handles a token. | | [`Learn/`](../src/LeanStudio.Core/Learn) | `Tutorial` and `Playground`; `TacticGuide`, `ErrorGuide` and `PlainEnglish` (goals read aloud) in `Guides.cs`; `Snippets`, `TheoremGallery` and `ProgramRunner` in `Library.cs`. | | [`Agents/`](../src/LeanStudio.Core/Agents) | For assistants and web pages: `Workbench` and `ProjectSession` (Lean for a program instead of a person, used by the MCP server), `StudioBridge` (the pipe between an assistant and an open window), `InfoviewBridge` (Lean's own infoview page, served to a web view or browser) and `AgentSetup` (writing each assistant's MCP configuration). | diff --git a/src/LeanStudio.App/ViewModels/MainViewModel.Pro.cs b/src/LeanStudio.App/ViewModels/MainViewModel.Pro.cs index c8de415..6dc8c3c 100644 --- a/src/LeanStudio.App/ViewModels/MainViewModel.Pro.cs +++ b/src/LeanStudio.App/ViewModels/MainViewModel.Pro.cs @@ -476,6 +476,64 @@ public void TidyWhitespace() + (left > 0 ? $"; {left} long line{(left == 1 ? "" : "s")} left for you." : ".") + " Undo brings the old text back."); } + /// + /// Put the whole file in Mathlib's shape in one undoable edit: the imports in order, then the text rules + /// (whitespace, tabs, line endings, the final newline). Long lines and the file conventions are listed in Output. + /// + [RelayCommand] + public void TidyFile() + { + if (ActiveDocument is not { IsLean: true } d) + { + return; + } + string text = d.Document.Text; + string tidy = StyleCheck.Fix(ImportOrder.Sort(text)); + if (tidy != text) + { + d.Document.Replace(0, text.Length, tidy); + } + IReadOnlyList left = [.. StyleCheck.Find(tidy), .. (ProjectFor(d).DependsOnMathlib ? MathlibConventions.Find(tidy) : [])]; + foreach (StyleProblem p in left) + { + Log($" line {p.Line + 1}: {p.Message}"); + } + Log((tidy == text ? "Tidy: already tidy" : "Tidy: imports sorted and whitespace fixed") + + (left.Count > 0 ? $"; {left.Count} thing{(left.Count == 1 ? "" : "s")} left for you (above)." : ".") + + (tidy == text ? "" : " Undo brings the old text back.")); + } + + /// + /// Put Mathlib's copyright header at the top of the active file, with this year and the name git is set up with + /// (the Git user name, else the system user). A file that already starts with a comment is left alone. + /// + [RelayCommand] + public async Task AddMathlibHeaderAsync() + { + if (ActiveDocument is not { IsLean: true } d) + { + return; + } + string author = Environment.UserName; + if (Core.Git.GitRepository.Find(d.Path) is Core.Git.GitRepository git) + { + Core.Processes.ProcessResult r = await git.RunAsync(["config", "user.name"]); + if (r.Success && r.Output.Trim().Length > 0) + { + author = r.Output.Trim(); + } + } + string text = d.Document.Text; + string withHeader = MathlibConventions.AddHeader(text, DateTime.Now.Year, author); + if (withHeader == text) + { + Log("Header: the file already starts with a comment, so it was left alone."); + return; + } + d.Document.Insert(0, withHeader[..^text.Length]); + Log($"Header: added Mathlib's copyright header for {author}. Check the name, then undo if it is wrong."); + } + // ---- linters ---- /// diff --git a/src/LeanStudio.App/Views/MainWindow.axaml b/src/LeanStudio.App/Views/MainWindow.axaml index a5b7e19..e698a61 100644 --- a/src/LeanStudio.App/Views/MainWindow.axaml +++ b/src/LeanStudio.App/Views/MainWindow.axaml @@ -131,6 +131,8 @@ + + diff --git a/src/LeanStudio.App/Views/MainWindow.axaml.cs b/src/LeanStudio.App/Views/MainWindow.axaml.cs index 2c7b8f4..a15e6f3 100644 --- a/src/LeanStudio.App/Views/MainWindow.axaml.cs +++ b/src/LeanStudio.App/Views/MainWindow.axaml.cs @@ -1081,6 +1081,8 @@ private void OnLocationDoubleTapped(object? sender, TappedEventArgs e) yield return ("Lean: Remove Unused Imports", "", Cmd(_vm.RemoveUnusedImportsCommand)); yield return ("Lean: Sort Imports", "", Cmd(_vm.SortImportsCommand)); yield return ("Lean: Tidy Whitespace and Check Style", "", Cmd(_vm.TidyWhitespaceCommand)); + yield return ("Lean: Tidy File (sort imports, fix whitespace)", "", Cmd(_vm.TidyFileCommand)); + yield return ("Lean: Add Mathlib Copyright Header", "", Cmd(_vm.AddMathlibHeaderCommand)); yield return ("Lean: Lint File (the linters CI runs)", "", Cmd(_vm.LintFileCommand)); yield return ("Lean: Import Every Module in the Library Root", "", Cmd(_vm.ImportAllModulesCommand)); yield return ("Lean: Get Mathlib Cache for Open Files", "", Cmd(_vm.GetCacheForOpenFilesCommand)); diff --git a/src/LeanStudio.Core/Workflow/MathlibConventions.cs b/src/LeanStudio.Core/Workflow/MathlibConventions.cs new file mode 100644 index 0000000..13cb901 --- /dev/null +++ b/src/LeanStudio.Core/Workflow/MathlibConventions.cs @@ -0,0 +1,63 @@ +using System.Text.RegularExpressions; + +namespace LeanStudio.Core.Workflow; + +/// +/// The file conventions Mathlib asks of a contributor beyond the text rules in : the +/// copyright header at the top, a module docstring (/-! … -/) before the first declaration, and theorem names that +/// do not start with a capital (a theorem is named in snake_case; only types and structures are UpperCamelCase). +/// Rules reported: copyright-header, module-doc and theorem-name. +/// +public static class MathlibConventions +{ + private static readonly Regex Copyright = new(@"^Copyright \(c\) \d{4}(?:, \d{4})* .+\. All rights reserved\.$", RegexOptions.Compiled); + private static readonly Regex Theorem = new(@"^\s*(?:@\[[^\]]*\]\s*)*(?:(?:protected|private|nonrec)\s+)*(?:theorem|lemma)\s+(?[^\s:({\[]+)", RegexOptions.Compiled); + + /// The convention problems in , in line order. + public static IReadOnlyList Find(string text) + { + var problems = new List(); + string[] lines = text.Replace("\r\n", "\n", StringComparison.Ordinal).Split('\n'); + if (!HasHeader(lines)) + { + problems.Add(new StyleProblem(0, "copyright-header", + "The file should start with a header: `/-`, `Copyright (c) YEAR Name. All rights reserved.`, `Released under Apache 2.0 license as described in the file LICENSE.`, `Authors: Name`, `-/`.")); + } + if (!lines.Any(l => l.StartsWith("/-!", StringComparison.Ordinal))) + { + problems.Add(new StyleProblem(0, "module-doc", "The file has no module docstring (`/-! … -/`) saying what it is about.")); + } + for (int i = 0; i < lines.Length; i++) + { + Match m = Theorem.Match(lines[i]); + if (m.Success) + { + string last = m.Groups["n"].Value.Split('.')[^1]; + if (last.Length > 0 && char.IsUpper(last[0])) + { + problems.Add(new StyleProblem(i, "theorem-name", $"`{last}`: a theorem is named in snake_case, starting with a lowercase letter.")); + } + } + } + return problems; + } + + private static bool HasHeader(string[] lines) => + lines.Length >= 5 && lines[0] == "/-" && Copyright.IsMatch(lines[1]) + && lines[2] == "Released under Apache 2.0 license as described in the file LICENSE." + && lines[3].StartsWith("Authors: ", StringComparison.Ordinal) && lines[3].Length > "Authors: ".Length + && lines[4] == "-/"; + + /// + /// with Mathlib's copyright header put at the top, followed by a blank line, unless the file + /// already starts with a comment (the header may only be mistyped: that is for a person to look at). + /// + public static string AddHeader(string text, int year, string author) + { + if (text.TrimStart().StartsWith("/-", StringComparison.Ordinal)) + { + return text; + } + return $"/-\nCopyright (c) {year} {author}. All rights reserved.\nReleased under Apache 2.0 license as described in the file LICENSE.\nAuthors: {author}\n-/\n{text}"; + } +} diff --git a/src/LeanStudio.Mcp/LeanTools.cs b/src/LeanStudio.Mcp/LeanTools.cs index dc13451..3bce964 100644 --- a/src/LeanStudio.Mcp/LeanTools.cs +++ b/src/LeanStudio.Mcp/LeanTools.cs @@ -719,14 +719,16 @@ public static IReadOnlyList Tools(Workbench bench) => }), new("style_check", - "Check a Lean file against the text rules Mathlib's CI holds it to: no trailing whitespace, no line over 100 characters, no tabs, LF line endings, exactly one newline at the end. With apply=true, fixes what has one obvious fix (everything but long lines) on disk.", + "Check a Lean file against the text rules Mathlib's CI holds it to: no trailing whitespace, no line over 100 characters, no tabs, LF line endings, exactly one newline at the end. In a project that uses Mathlib (or with mathlib=true) it also checks Mathlib's file conventions: the copyright header, a module docstring, theorem names in snake_case. With apply=true, fixes what has one obvious fix (the text rules, except long lines) on disk.", Schema(("path", "string", "The .lean file.", true), - ("apply", "boolean", "Fix the fixable problems on disk (default false).", false)), + ("apply", "boolean", "Fix the fixable problems on disk (default false).", false), + ("mathlib", "boolean", "Also check Mathlib's file conventions (default: when the project uses Mathlib).", false)), async (a, ct) => { string path = LeanFile(bench, a); string text = await File.ReadAllTextAsync(path, ct); - IReadOnlyList problems = StyleCheck.Find(text); + bool conventions = OptBool(a, "mathlib") ?? bench.ProjectFor(path).DependsOnMathlib; + IReadOnlyList problems = [.. StyleCheck.Find(text), .. (conventions ? MathlibConventions.Find(text) : [])]; if (problems.Count == 0) { return "no style problems"; @@ -739,8 +741,9 @@ public static IReadOnlyList Tools(Workbench bench) => if (OptBool(a, "apply") == true) { await File.WriteAllTextAsync(path, StyleCheck.Fix(text), ct); - int left = problems.Count(p => p.Rule == "long-line"); - sb.Append(CultureInfo.InvariantCulture, $"fixed {problems.Count - left} problem(s); {left} long line(s) are left for you"); + string[] fixable = ["trailing-whitespace", "tab", "crlf", "final-newline"]; + int left = problems.Count(p => !fixable.Contains(p.Rule)); + sb.Append(CultureInfo.InvariantCulture, $"fixed {problems.Count - left} problem(s); {left} are left for you"); } return sb.ToString().TrimEnd(); }), diff --git a/tests/LeanStudio.Tests/PickerAndConflictTests.cs b/tests/LeanStudio.Tests/PickerAndConflictTests.cs index d70afff..edecd3e 100644 --- a/tests/LeanStudio.Tests/PickerAndConflictTests.cs +++ b/tests/LeanStudio.Tests/PickerAndConflictTests.cs @@ -185,6 +185,9 @@ async Task Call(string tool, System.Text.Json.Nodes.JsonObject args) await Call("style_check", new() { ["path"] = file, ["apply"] = true }); Assert.Equal("import A\nimport B\n\ndef x := 1\n", await File.ReadAllTextAsync(file, TestContext.Current.CancellationToken)); Assert.Equal("no style problems", await Call("style_check", new() { ["path"] = file })); + string conventions = await Call("style_check", new() { ["path"] = file, ["mathlib"] = true }); + Assert.Contains("copyright-header", conventions, StringComparison.Ordinal); + Assert.Contains("module-doc", conventions, StringComparison.Ordinal); } finally { @@ -192,3 +195,40 @@ async Task Call(string tool, System.Text.Json.Nodes.JsonObject args) } } } + +/// Mathlib's file conventions: the header, the module docstring, theorem names. +public sealed class MathlibConventionsTests +{ + private const string Header = "/-\nCopyright (c) 2025 Ada Lovelace. All rights reserved.\nReleased under Apache 2.0 license as described in the file LICENSE.\nAuthors: Ada Lovelace\n-/\n"; + + [Fact] + public void AcceptsAFileWithAHeaderAndAModuleDocstring() => + Assert.Empty(MathlibConventions.Find(Header + "import Mathlib.Data.Nat.Basic\n\n/-! # Facts -/\n\ntheorem foo_bar : True := trivial\n")); + + [Fact] + public void ReportsAMissingHeaderAndModuleDocstring() => + Assert.Equal([(0, "copyright-header"), (0, "module-doc")], MathlibConventions.Find("import A\n\ndef x := 1\n").Select(p => (p.Line, p.Rule))); + + [Theory] + [InlineData("/-\nCopyright (c) 2025 Ada. All rights reserved.\nReleased under MIT.\nAuthors: Ada\n-/\n")] + [InlineData("/-\nCopyright 2025 Ada.\nReleased under Apache 2.0 license as described in the file LICENSE.\nAuthors: Ada\n-/\n")] + [InlineData("/-\nCopyright (c) 2025 Ada. All rights reserved.\nReleased under Apache 2.0 license as described in the file LICENSE.\nAuthors: \n-/\n")] + public void ReportsAMalformedHeader(string header) => + Assert.Contains(MathlibConventions.Find(header + "/-! Doc -/\n"), p => p.Rule == "copyright-header"); + + [Fact] + public void FlagsTheoremNamesThatStartWithACapital() + { + string text = Header + "/-! Doc -/\n\ntheorem Foo : True := trivial\n@[simp] protected lemma Nat.Bar_baz (n : Nat) : n = n := rfl\ntheorem Nat.ok_name : True := trivial\ntheorem isOpen_iff : True := trivial\n"; + Assert.Equal([(7, "theorem-name"), (8, "theorem-name")], MathlibConventions.Find(text).Select(p => (p.Line, p.Rule))); + } + + [Fact] + public void AddsTheHeaderOnlyWhereThereIsNoCommentFirst() + { + string added = MathlibConventions.AddHeader("import A\n", 2026, "Grace Hopper"); + Assert.Equal("/-\nCopyright (c) 2026 Grace Hopper. All rights reserved.\nReleased under Apache 2.0 license as described in the file LICENSE.\nAuthors: Grace Hopper\n-/\nimport A\n", added); + Assert.DoesNotContain(MathlibConventions.Find(added + "/-! Doc -/\n"), p => p.Rule == "copyright-header"); + Assert.Equal(added, MathlibConventions.AddHeader(added, 2030, "Someone Else")); + } +} From c1e5a09ccc275787b280357ed01fe5a0af83de72 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 3 Oct 2026 19:07:59 +0000 Subject: [PATCH 05/18] Add stale-deprecation removal and doc-comment coverage for Mathlib projects Co-Authored-By: Claude Sonnet 5.5 Claude-Session: https://claude.ai/code/session_01FF5AYRpU9TWeWY3CFh2ETw --- CHANGELOG.md | 2 + README.md | 1 + docs/ARCHITECTURE.md | 4 +- .../ViewModels/MainViewModel.Pro.cs | 33 +++++- src/LeanStudio.App/Views/MainWindow.axaml | 1 + src/LeanStudio.App/Views/MainWindow.axaml.cs | 1 + src/LeanStudio.Core/Workflow/DocCoverage.cs | 63 +++++++++++ .../Workflow/StaleDeprecations.cs | 106 ++++++++++++++++++ src/LeanStudio.Mcp/LeanTools.cs | 36 +++++- .../PickerAndConflictTests.cs | 68 +++++++++++ 10 files changed, 310 insertions(+), 5 deletions(-) create mode 100644 src/LeanStudio.Core/Workflow/DocCoverage.cs create mode 100644 src/LeanStudio.Core/Workflow/StaleDeprecations.cs diff --git a/CHANGELOG.md b/CHANGELOG.md index f2d53ed..763fd9a 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -19,6 +19,8 @@ - **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. - **Over MCP**, `sort_imports` and `style_check` do the same for assistants, each with `apply` to write the file. **Fixes**: diff --git a/README.md b/README.md index 0aea10c..836b1ef 100644 --- a/README.md +++ b/README.md @@ -331,6 +331,7 @@ What CI and reviewers check, before you push: - **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. +- **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`. diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index 23c88b4..b0609b3 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -129,7 +129,7 @@ shows them to a person or an assistant. | [`Proofs/`](../src/LeanStudio.Core/Proofs) | Features that ask Lean about proofs: `ProofSteps` (the tactic block around a line, read by layout), `ProofSearch` (Prove It and counterexamples) and `Scratch` (scratch documents in the running server), `ExtractLemma`, `Profiler` (Lean's profilers read into a `ProfileReport`: trees, categories, counters, per-line costs; its records are in `ProfileModel`), `LiveProfiler` (the same, from the running server as the file is edited), `ProfileCheck` (saved profiles in `ProfileStore`, and the heartbeat regression check), `Heartbeats`, `ProofStates` (the Proof-State Map), `Walkthrough` (the HTML export) and `LeanRepl`. | | [`Ai/`](../src/LeanStudio.Core/Ai) | The AI in the editor: `IChatModel` and the clients behind it (`AppleIntelligence` and `AppleFmCliModel` for the `fm` command, `OllamaModel`, `OpenAiCompatibleModel`, `AnthropicModel`), `AiDiscovery` (what is running, and which model to use), `AiProver` (proofs from a model, checked by Lean), `AiAssistant` (explanations and chat), `AiText` (token estimates and trimming) and `SecretStore` (API keys). | | [`Editing/`](../src/LeanStudio.Core/Editing) | Text-level engines with no UI: `Abbreviations` (Unicode input), `LeanText` (comments, strings and declarations in Lean source), `LatexText` (docstring math as text), `Fuzzy` (picker matching), `ProjectSearch` (find and replace across files), `MultiCursor`, `VimEngine`, `EmacsEngine` and `KeyBindingsFile` (keybindings.json). The editor in the app is a thin host over them. | -| [`Workflow/`](../src/LeanStudio.Core/Workflow) | Project-wide tools. `Workflow.cs` holds `Markers` (sorries and TODOs), `LakeOutput` (build problems), `LocalHistory`, `Loogle`, `LeanSearch`, `DocLinks`, `Blame` and `ProjectTasks`. Beside it: `Refactor` and `EmittedC` (module rename, replace across files, Compiled C), `Ffi` (`@[extern]` bindings checked against the project's C files, and C stubs), `ImportCheck` (unused imports), `ImportOrder` (sorted imports), `StyleCheck` (Mathlib's text rules), `MathlibConventions` (header, module docstring, theorem names), `Lint`, `Instances`, `Deprecation` (deprecated aliases for renames), `DependencyBump` (Update Mathlib and see what broke), `Blueprint`, `ProjectCommands` (`.leanstudio/commands.json`), `ProgressReader` (progress read from what a task prints), `LeanCli` (the `lean` command line on a mirror copy) and `Essentials.cs` (`ElanInstaller`, `FileOps`, `ImportFinder`). | +| [`Workflow/`](../src/LeanStudio.Core/Workflow) | Project-wide tools. `Workflow.cs` holds `Markers` (sorries and TODOs), `LakeOutput` (build problems), `LocalHistory`, `Loogle`, `LeanSearch`, `DocLinks`, `Blame` and `ProjectTasks`. Beside it: `Refactor` and `EmittedC` (module rename, replace across files, Compiled C), `Ffi` (`@[extern]` bindings checked against the project's C files, and C stubs), `ImportCheck` (unused imports), `ImportOrder` (sorted imports), `StyleCheck` (Mathlib's text rules), `MathlibConventions` (header, module docstring, theorem names), `DocCoverage` (definitions with no doc comment), `StaleDeprecations` (old deprecated aliases, found and deleted), `Lint`, `Instances`, `Deprecation` (deprecated aliases for renames), `DependencyBump` (Update Mathlib and see what broke), `Blueprint`, `ProjectCommands` (`.leanstudio/commands.json`), `ProgressReader` (progress read from what a task prints), `LeanCli` (the `lean` command line on a mirror copy) and `Essentials.cs` (`ElanInstaller`, `FileOps`, `ImportFinder`). | | [`Git/`](../src/LeanStudio.Core/Git) | `GitRepository` wraps your own `git` executable, so your config, hooks, credentials and signing all apply. `GitHub` goes through the `gh` CLI, so Lean Studio never handles a token. | | [`Learn/`](../src/LeanStudio.Core/Learn) | `Tutorial` and `Playground`; `TacticGuide`, `ErrorGuide` and `PlainEnglish` (goals read aloud) in `Guides.cs`; `Snippets`, `TheoremGallery` and `ProgramRunner` in `Library.cs`. | | [`Agents/`](../src/LeanStudio.Core/Agents) | For assistants and web pages: `Workbench` and `ProjectSession` (Lean for a program instead of a person, used by the MCP server), `StudioBridge` (the pipe between an assistant and an open window), `InfoviewBridge` (Lean's own infoview page, served to a web view or browser) and `AgentSetup` (writing each assistant's MCP configuration). | @@ -174,7 +174,7 @@ written to stdout. | Checking and reading a file | `project_info`, `check_file`, `goals`, `proof_steps`, `hover`, `suggestions`, `references`, `run_lean` | | Building and Tenet | `build`, `verify`, `axioms`, `why_not_proved`, `project_map` | | Proof tools | `prove`, `extract_lemma`, `ffi_bindings`, `profile` | -| For Mathlib contributors | `unused_imports`, `sort_imports`, `style_check`, `lint`, `heartbeats`, `instances`, `blueprint` | +| For Mathlib contributors | `unused_imports`, `sort_imports`, `style_check`, `stale_deprecations`, `lint`, `heartbeats`, `instances`, `blueprint` | | Walkthroughs and search | `export_walkthrough`, `search_mathlib`, and `declaration` and `search_declarations` (the compiled library, through Tenet) | | Toolchains | `toolchains` | | The open window | `studio_context`, `studio_show` | diff --git a/src/LeanStudio.App/ViewModels/MainViewModel.Pro.cs b/src/LeanStudio.App/ViewModels/MainViewModel.Pro.cs index 6dc8c3c..e635372 100644 --- a/src/LeanStudio.App/ViewModels/MainViewModel.Pro.cs +++ b/src/LeanStudio.App/ViewModels/MainViewModel.Pro.cs @@ -493,7 +493,12 @@ public void TidyFile() { d.Document.Replace(0, text.Length, tidy); } - IReadOnlyList left = [.. StyleCheck.Find(tidy), .. (ProjectFor(d).DependsOnMathlib ? MathlibConventions.Find(tidy) : [])]; + List left = [.. StyleCheck.Find(tidy)]; + if (ProjectFor(d).DependsOnMathlib) + { + left.AddRange(MathlibConventions.Find(tidy)); + left.AddRange(DocCoverage.Find(tidy)); + } foreach (StyleProblem p in left) { Log($" line {p.Line + 1}: {p.Message}"); @@ -534,6 +539,32 @@ public async Task AddMathlibHeaderAsync() Log($"Header: added Mathlib's copyright header for {author}. Check the name, then undo if it is wrong."); } + /// + /// Delete the deprecated aliases and declarations of the active file that are more than six months old (by their + /// (since := "…")), with their doc comments, as one undoable edit. Each is named in Output. + /// + [RelayCommand] + public void RemoveStaleDeprecations() + { + if (ActiveDocument is not { IsLean: true } d) + { + return; + } + string text = d.Document.Text; + IReadOnlyList stale = StaleDeprecations.Find(text, DateOnly.FromDateTime(DateTime.Today)); + if (stale.Count == 0) + { + Log("Deprecations: none is more than six months old."); + return; + } + d.Document.Replace(0, text.Length, StaleDeprecations.Remove(text, stale)); + foreach (StaleDeprecation s in stale) + { + Log($" removed {s.Name}, deprecated {s.Since:yyyy-MM-dd} ({s.AgeMonths} months ago)"); + } + Log($"Deprecations: removed {stale.Count}. Undo brings them back."); + } + // ---- linters ---- /// diff --git a/src/LeanStudio.App/Views/MainWindow.axaml b/src/LeanStudio.App/Views/MainWindow.axaml index e698a61..e347361 100644 --- a/src/LeanStudio.App/Views/MainWindow.axaml +++ b/src/LeanStudio.App/Views/MainWindow.axaml @@ -133,6 +133,7 @@ + diff --git a/src/LeanStudio.App/Views/MainWindow.axaml.cs b/src/LeanStudio.App/Views/MainWindow.axaml.cs index a15e6f3..79d300f 100644 --- a/src/LeanStudio.App/Views/MainWindow.axaml.cs +++ b/src/LeanStudio.App/Views/MainWindow.axaml.cs @@ -1083,6 +1083,7 @@ private void OnLocationDoubleTapped(object? sender, TappedEventArgs e) yield return ("Lean: Tidy Whitespace and Check Style", "", Cmd(_vm.TidyWhitespaceCommand)); yield return ("Lean: Tidy File (sort imports, fix whitespace)", "", Cmd(_vm.TidyFileCommand)); yield return ("Lean: Add Mathlib Copyright Header", "", Cmd(_vm.AddMathlibHeaderCommand)); + yield return ("Lean: Remove Deprecations Older Than Six Months", "", Cmd(_vm.RemoveStaleDeprecationsCommand)); yield return ("Lean: Lint File (the linters CI runs)", "", Cmd(_vm.LintFileCommand)); yield return ("Lean: Import Every Module in the Library Root", "", Cmd(_vm.ImportAllModulesCommand)); yield return ("Lean: Get Mathlib Cache for Open Files", "", Cmd(_vm.GetCacheForOpenFilesCommand)); diff --git a/src/LeanStudio.Core/Workflow/DocCoverage.cs b/src/LeanStudio.Core/Workflow/DocCoverage.cs new file mode 100644 index 0000000..4cf867d --- /dev/null +++ b/src/LeanStudio.Core/Workflow/DocCoverage.cs @@ -0,0 +1,63 @@ +using System.Text.RegularExpressions; + +namespace LeanStudio.Core.Workflow; + +/// +/// The declarations of a file that have no doc comment, which Mathlib's docBlame linter asks for on every +/// public definition, structure, class and inductive type (a theorem needs none, though it may have one). Found from +/// the text, so it works without building anything. Reported as missing-doc. +/// +public static class DocCoverage +{ + private static readonly Regex Declaration = new( + @"^(?:@\[[^\]]*\]\s*)*(?:(?:protected|public|noncomputable|partial|unsafe|nonrec)\s+)*(?def|abbrev|structure|class|inductive|opaque|theorem|lemma)\s+(?[^\s:({\[]+)", + RegexOptions.Compiled); + + /// + /// The declarations at the start of a line that have no doc comment right above them (attributes on their own + /// lines in between are skipped). Private ones are left out; theorems and lemmas only with . + /// + public static IReadOnlyList Find(string text, bool includeTheorems = false) + { + string[] lines = text.Replace("\r\n", "\n", StringComparison.Ordinal).Split('\n'); + bool[] code = LeanStudio.Core.Editing.LeanText.CodeMask(text.Replace("\r\n", "\n", StringComparison.Ordinal)); + var found = new List(); + int offset = 0; + for (int i = 0; i < lines.Length; offset += lines[i].Length + 1, i++) + { + string line = lines[i]; + if (line.Length == 0 || char.IsWhiteSpace(line[0]) || (offset < code.Length && !code[offset])) + { + continue; // indented, or inside a comment or string + } + Match m = Declaration.Match(line); + if (!m.Success || (m.Groups["kw"].Value is "theorem" or "lemma" && !includeTheorems) || line.TrimStart('@').StartsWith("private ", StringComparison.Ordinal) || Regex.IsMatch(line, @"\bprivate\b")) + { + continue; + } + if (!HasDocAbove(lines, i)) + { + found.Add(new StyleProblem(i, "missing-doc", $"`{m.Groups["name"].Value}` has no doc comment.")); + } + } + return found; + } + + private static bool HasDocAbove(string[] lines, int declaration) + { + int k = declaration - 1; + while (k >= 0 && lines[k].StartsWith("@[", StringComparison.Ordinal) && lines[k].TrimEnd().EndsWith(']')) + { + k--; // an attribute line of its own + } + if (k < 0 || !lines[k].TrimEnd().EndsWith("-/", StringComparison.Ordinal)) + { + return false; + } + while (k >= 0 && !lines[k].StartsWith("/-", StringComparison.Ordinal)) + { + k--; + } + return k >= 0 && lines[k].StartsWith("/--", StringComparison.Ordinal); + } +} diff --git a/src/LeanStudio.Core/Workflow/StaleDeprecations.cs b/src/LeanStudio.Core/Workflow/StaleDeprecations.cs new file mode 100644 index 0000000..71df9b9 --- /dev/null +++ b/src/LeanStudio.Core/Workflow/StaleDeprecations.cs @@ -0,0 +1,106 @@ +using System.Globalization; +using System.Text.RegularExpressions; + +namespace LeanStudio.Core.Workflow; + +/// A deprecated declaration old enough to be deleted. +/// The first line to delete: its doc comment, else its attribute (0-based). +/// The line after its last line (0-based, exclusive). +/// The deprecated name, as written. +/// The date in its (since := "…"). +/// Whole months from to the day it was checked. +public sealed record StaleDeprecation(int StartLine, int EndLine, string Name, DateOnly Since, int AgeMonths); + +/// +/// Mathlib deletes a deprecated alias some months after the rename, so code that still uses it has had time to move. +/// This finds the ones past that age by their (since := "yyyy-mm-dd") and deletes them, with their doc comments. +/// The counterpart of , which writes them. +/// +public static class StaleDeprecations +{ + private static readonly Regex Since = new(@"@\[[^\]]*\bdeprecated\b[^\]]*\(since\s*:=\s*""(?\d{4}-\d{2}(?:-\d{2})?)""\)", RegexOptions.Compiled); + private static readonly Regex Alias = new(@"\balias\s+(?[^\s:=]+)", RegexOptions.Compiled); + private static readonly Regex Declaration = new( + @"(?:theorem|lemma|def|abbrev|instance|structure|inductive|class|opaque)\s+(?[^\s:({\[]+)", RegexOptions.Compiled); + + /// The deprecations in at least months old on , in line order. + public static IReadOnlyList Find(string text, DateOnly today, int months = 6) + { + string[] lines = text.Split('\n'); + var found = new List(); + for (int i = 0; i < lines.Length; i++) + { + Match m = Since.Match(lines[i]); + if (!m.Success || !TryParse(m.Groups["d"].Value, out DateOnly since)) + { + continue; + } + int age = (today.Year - since.Year) * 12 + today.Month - since.Month - (today.Day < since.Day ? 1 : 0); + if (age < months) + { + continue; + } + // The declaration is on this line (an alias, or `@[deprecated …] theorem …`) or below the attribute. + int decl = i; + while (decl < lines.Length && !Alias.IsMatch(lines[decl]) && !Declaration.IsMatch(lines[decl])) + { + if (decl > i + 3) + { + decl = -1; + break; + } + decl++; + } + if (decl < 0 || decl >= lines.Length) + { + continue; + } + Match name = Alias.Match(lines[decl]); + if (!name.Success) + { + name = Declaration.Match(lines[decl]); + } + int start = i; + if (i > 0 && lines[i - 1].TrimEnd('\r').EndsWith("-/", StringComparison.Ordinal)) + { + int k = i - 1; + while (k > 0 && !lines[k].TrimStart().StartsWith("/--", StringComparison.Ordinal)) + { + k--; + } + if (lines[k].TrimStart().StartsWith("/--", StringComparison.Ordinal)) + { + start = k; + } + } + int end = Deprecation.EndOfDeclaration(lines, decl); + found.Add(new StaleDeprecation(start, end, name.Groups["n"].Value, since, age)); + i = end - 1; + } + return found; + } + + /// without the declarations of , and without the blank line a deletion would double. + public static string Remove(string text, IEnumerable stale) + { + string[] lines = text.Split('\n'); + var drop = new HashSet(); + foreach (StaleDeprecation s in stale) + { + for (int i = s.StartLine; i < s.EndLine; i++) + { + drop.Add(i); + } + // Two blank lines would meet where the declaration was: drop the one after it. + bool blankBefore = s.StartLine == 0 || lines[s.StartLine - 1].Trim().Length == 0; + if (blankBefore && s.EndLine < lines.Length && lines[s.EndLine].Trim().Length == 0) + { + drop.Add(s.EndLine); + } + } + return string.Join('\n', lines.Where((_, i) => !drop.Contains(i))); + } + + private static bool TryParse(string s, out DateOnly date) => + DateOnly.TryParseExact(s.Length == 7 ? s + "-01" : s, "yyyy-MM-dd", CultureInfo.InvariantCulture, DateTimeStyles.None, out date); +} diff --git a/src/LeanStudio.Mcp/LeanTools.cs b/src/LeanStudio.Mcp/LeanTools.cs index 3bce964..3499789 100644 --- a/src/LeanStudio.Mcp/LeanTools.cs +++ b/src/LeanStudio.Mcp/LeanTools.cs @@ -719,7 +719,7 @@ public static IReadOnlyList Tools(Workbench bench) => }), new("style_check", - "Check a Lean file against the text rules Mathlib's CI holds it to: no trailing whitespace, no line over 100 characters, no tabs, LF line endings, exactly one newline at the end. In a project that uses Mathlib (or with mathlib=true) it also checks Mathlib's file conventions: the copyright header, a module docstring, theorem names in snake_case. With apply=true, fixes what has one obvious fix (the text rules, except long lines) on disk.", + "Check a Lean file against the text rules Mathlib's CI holds it to: no trailing whitespace, no line over 100 characters, no tabs, LF line endings, exactly one newline at the end. In a project that uses Mathlib (or with mathlib=true) it also checks Mathlib's file conventions: the copyright header, a module docstring, theorem names in snake_case, and a doc comment on every public definition. With apply=true, fixes what has one obvious fix (the text rules, except long lines) on disk.", Schema(("path", "string", "The .lean file.", true), ("apply", "boolean", "Fix the fixable problems on disk (default false).", false), ("mathlib", "boolean", "Also check Mathlib's file conventions (default: when the project uses Mathlib).", false)), @@ -728,7 +728,12 @@ public static IReadOnlyList Tools(Workbench bench) => string path = LeanFile(bench, a); string text = await File.ReadAllTextAsync(path, ct); bool conventions = OptBool(a, "mathlib") ?? bench.ProjectFor(path).DependsOnMathlib; - IReadOnlyList problems = [.. StyleCheck.Find(text), .. (conventions ? MathlibConventions.Find(text) : [])]; + List problems = [.. StyleCheck.Find(text)]; + if (conventions) + { + problems.AddRange(MathlibConventions.Find(text)); + problems.AddRange(DocCoverage.Find(text)); + } if (problems.Count == 0) { return "no style problems"; @@ -748,6 +753,33 @@ public static IReadOnlyList Tools(Workbench bench) => return sb.ToString().TrimEnd(); }), + new("stale_deprecations", + "The deprecated declarations of a Lean file that are old enough to delete: Mathlib removes a deprecated alias some months after the rename. Reads each (since := \"yyyy-mm-dd\") and lists those at least `months` old (default 6). With apply=true, deletes them, with their doc comments, from the file on disk.", + Schema(("path", "string", "The .lean file.", true), + ("months", "integer", "How old, in whole months, a deprecation must be (default 6).", false), + ("apply", "boolean", "Delete them from the file on disk (default false).", false)), + async (a, ct) => + { + string path = LeanFile(bench, a); + string text = await File.ReadAllTextAsync(path, ct); + IReadOnlyList stale = StaleDeprecations.Find(text, DateOnly.FromDateTime(DateTime.Today), OptInt(a, "months") ?? 6); + if (stale.Count == 0) + { + return "no deprecation is that old"; + } + var sb = new StringBuilder(); + foreach (StaleDeprecation s in stale) + { + sb.Append(CultureInfo.InvariantCulture, $"{path}:{s.StartLine + 1}: {s.Name}, deprecated {s.Since:yyyy-MM-dd} ({s.AgeMonths} months ago)\n"); + } + if (OptBool(a, "apply") == true) + { + await File.WriteAllTextAsync(path, StaleDeprecations.Remove(text, stale), ct); + sb.Append(CultureInfo.InvariantCulture, $"removed {stale.Count} deprecation(s)"); + } + return sb.ToString().TrimEnd(); + }), + new("lint", "Run the linters CI runs on a Lean file of a Lake project: Mathlib's standard set in a project that uses Mathlib (its style linters among them), every linter Lean has elsewhere, and Batteries' environment linters (missing docstrings, simp normal form, unused arguments…) where Batteries is available. Lints the file as saved on disk.", Schema(("path", "string", "The .lean file.", true)), diff --git a/tests/LeanStudio.Tests/PickerAndConflictTests.cs b/tests/LeanStudio.Tests/PickerAndConflictTests.cs index edecd3e..c63a214 100644 --- a/tests/LeanStudio.Tests/PickerAndConflictTests.cs +++ b/tests/LeanStudio.Tests/PickerAndConflictTests.cs @@ -188,6 +188,13 @@ async Task Call(string tool, System.Text.Json.Nodes.JsonObject args) string conventions = await Call("style_check", new() { ["path"] = file, ["mathlib"] = true }); Assert.Contains("copyright-header", conventions, StringComparison.Ordinal); Assert.Contains("module-doc", conventions, StringComparison.Ordinal); + Assert.Contains("A.lean:4: missing-doc: `x` has no doc comment.", conventions, StringComparison.Ordinal); + + await File.WriteAllTextAsync(file, "@[deprecated (since := \"2020-01-01\")] alias old := new\n\ndef new := 1\n", TestContext.Current.CancellationToken); + Assert.Contains("old, deprecated 2020-01-01", await Call("stale_deprecations", new() { ["path"] = file }), StringComparison.Ordinal); + Assert.Contains("no deprecation is that old", await Call("stale_deprecations", new() { ["path"] = file, ["months"] = 1000 }), StringComparison.Ordinal); + await Call("stale_deprecations", new() { ["path"] = file, ["apply"] = true }); + Assert.Equal("def new := 1\n", await File.ReadAllTextAsync(file, TestContext.Current.CancellationToken)); } finally { @@ -232,3 +239,64 @@ public void AddsTheHeaderOnlyWhereThereIsNoCommentFirst() Assert.Equal(added, MathlibConventions.AddHeader(added, 2030, "Someone Else")); } } + +/// Finding and deleting the deprecated declarations that are old enough. +public sealed class StaleDeprecationTests +{ + private static readonly DateOnly Today = new(2026, 10, 3); + + private const string File = + "theorem keep : True := trivial\n\n" + + "/-- Old. -/\n@[deprecated (since := \"2025-12-31\")] alias oldName := keep\n\n" + + "@[deprecated keep (since := \"2024-01-15\")]\ntheorem older : True := keep\n\n" + + "@[deprecated (since := \"2026-08-01\")] alias recent := keep\n\n" + + "def last := 1\n"; + + [Fact] + public void FindsOnlyTheDeprecationsPastTheAge() + { + IReadOnlyList stale = StaleDeprecations.Find(File, Today); + Assert.Equal(["oldName", "older"], stale.Select(s => s.Name)); + Assert.Equal([9, 32], stale.Select(s => s.AgeMonths)); // whole months: 2025-12-31 to 2026-10-03; 2024-01-15 to 2026-10-03 + Assert.Equal([2, 5], stale.Select(s => s.StartLine)); // the first starts at its doc comment + Assert.Equal(["oldName", "older", "recent"], StaleDeprecations.Find(File, Today, months: 1).Select(s => s.Name)); + Assert.Equal(["older"], StaleDeprecations.Find(File, Today, months: 12).Select(s => s.Name)); + Assert.Equal(["older"], StaleDeprecations.Find(File, new DateOnly(2026, 9, 30), 9).Select(s => s.Name)); // oldName is 8 months old on 9-30 + } + + [Fact] + public void DeletesThemWithTheirDocCommentsWithoutDoublingBlankLines() + { + string result = StaleDeprecations.Remove(File, StaleDeprecations.Find(File, Today)); + Assert.Equal("theorem keep : True := trivial\n\n@[deprecated (since := \"2026-08-01\")] alias recent := keep\n\ndef last := 1\n", result); + Assert.Empty(StaleDeprecations.Find(result, Today)); + } + + [Fact] + public void ReadsAYearAndMonthAndIgnoresWhatIsNotADeprecation() + { + const string text = "@[deprecated (since := \"2025-01\")] alias a := b\n-- since := \"2020-01-01\"\ndef b := 1\n"; + Assert.Equal(["a"], StaleDeprecations.Find(text, Today).Select(s => s.Name)); + Assert.Empty(StaleDeprecations.Find("def b := 1\n", Today)); + } +} + +/// Declarations without a doc comment. +public sealed class DocCoverageTests +{ + [Fact] + public void FindsPublicDefinitionsWithoutADocComment() + { + const string text = "/-- Documented. -/\ndef a := 1\n\ndef b := 2\n\n/-- Multi\n line. -/\n@[simp]\ndef c := 3\n\n@[simp]\nstructure D where\n x : Nat\n\nprivate def e := 5\n\n/-! Module doc is not a doc comment. -/\ndef f := 6\n\ntheorem t : True := trivial\n"; + Assert.Equal([(3, "missing-doc"), (11, "missing-doc"), (17, "missing-doc")], DocCoverage.Find(text).Select(p => (p.Line, p.Rule))); + Assert.Contains("`b`", DocCoverage.Find(text)[0].Message, StringComparison.Ordinal); + } + + [Fact] + public void LeavesOutIndentedCommentedAndTheoremsUnlessAsked() + { + const string text = "namespace N\n def indented := 1\nend N\n/-\ndef commented := 1\n-/\n-- def line := 1\ntheorem t : True := trivial\n"; + Assert.Empty(DocCoverage.Find(text)); + Assert.Equal([7], DocCoverage.Find(text, includeTheorems: true).Select(p => p.Line)); + } +} From a1618b476e41d16843bb67690021b1a2be9ee397 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 3 Oct 2026 19:13:52 +0000 Subject: [PATCH 06/18] Add Wrap Long Comment Lines and type-name convention check Co-Authored-By: Claude Sonnet 5.5 Claude-Session: https://claude.ai/code/session_01FF5AYRpU9TWeWY3CFh2ETw --- CHANGELOG.md | 2 + README.md | 1 + .../ViewModels/MainViewModel.Pro.cs | 27 +++++++ src/LeanStudio.App/Views/MainWindow.axaml | 1 + src/LeanStudio.App/Views/MainWindow.axaml.cs | 1 + .../Workflow/MathlibConventions.cs | 14 +++- src/LeanStudio.Core/Workflow/StyleCheck.cs | 80 +++++++++++++++++++ src/LeanStudio.Mcp/LeanTools.cs | 8 +- .../PickerAndConflictTests.cs | 54 +++++++++++++ 9 files changed, 183 insertions(+), 5 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 763fd9a..d761569 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -21,6 +21,8 @@ - **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. - **Over MCP**, `sort_imports` and `style_check` do the same for assistants, each with `apply` to write the file. **Fixes**: diff --git a/README.md b/README.md index 836b1ef..df3f473 100644 --- a/README.md +++ b/README.md @@ -331,6 +331,7 @@ What CI and reviewers check, before you push: - **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. +- **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. diff --git a/src/LeanStudio.App/ViewModels/MainViewModel.Pro.cs b/src/LeanStudio.App/ViewModels/MainViewModel.Pro.cs index e635372..a16b94e 100644 --- a/src/LeanStudio.App/ViewModels/MainViewModel.Pro.cs +++ b/src/LeanStudio.App/ViewModels/MainViewModel.Pro.cs @@ -565,6 +565,33 @@ public void RemoveStaleDeprecations() Log($"Deprecations: removed {stale.Count}. Undo brings them back."); } + /// + /// Break the comment and docstring lines of the active file that are over 100 characters at a space, as one undoable + /// edit. Code is never touched; what still is too long is listed in Output. + /// + [RelayCommand] + public void WrapLongComments() + { + if (ActiveDocument is not { IsLean: true } d) + { + return; + } + string text = d.Document.Text; + string wrapped = StyleCheck.WrapComments(text); + if (wrapped != text) + { + d.Document.Replace(0, text.Length, wrapped); + } + IReadOnlyList left = [.. StyleCheck.Find(wrapped).Where(p => p.Rule == "long-line")]; + foreach (StyleProblem p in left) + { + Log($" line {p.Line + 1}: {p.Message}"); + } + Log((wrapped == text ? "Wrap: no comment line to break" : "Wrap: broke the long comment lines") + + (left.Count > 0 ? $"; {left.Count} long line{(left.Count == 1 ? "" : "s")} of code left for you (above)." : ".") + + (wrapped == text ? "" : " Undo brings the old text back.")); + } + // ---- linters ---- /// diff --git a/src/LeanStudio.App/Views/MainWindow.axaml b/src/LeanStudio.App/Views/MainWindow.axaml index e347361..d4da292 100644 --- a/src/LeanStudio.App/Views/MainWindow.axaml +++ b/src/LeanStudio.App/Views/MainWindow.axaml @@ -132,6 +132,7 @@ + diff --git a/src/LeanStudio.App/Views/MainWindow.axaml.cs b/src/LeanStudio.App/Views/MainWindow.axaml.cs index 79d300f..36d8b40 100644 --- a/src/LeanStudio.App/Views/MainWindow.axaml.cs +++ b/src/LeanStudio.App/Views/MainWindow.axaml.cs @@ -1082,6 +1082,7 @@ private void OnLocationDoubleTapped(object? sender, TappedEventArgs e) yield return ("Lean: Sort Imports", "", Cmd(_vm.SortImportsCommand)); yield return ("Lean: Tidy Whitespace and Check Style", "", Cmd(_vm.TidyWhitespaceCommand)); yield return ("Lean: Tidy File (sort imports, fix whitespace)", "", Cmd(_vm.TidyFileCommand)); + yield return ("Lean: Wrap Long Comment Lines", "", Cmd(_vm.WrapLongCommentsCommand)); yield return ("Lean: Add Mathlib Copyright Header", "", Cmd(_vm.AddMathlibHeaderCommand)); yield return ("Lean: Remove Deprecations Older Than Six Months", "", Cmd(_vm.RemoveStaleDeprecationsCommand)); yield return ("Lean: Lint File (the linters CI runs)", "", Cmd(_vm.LintFileCommand)); diff --git a/src/LeanStudio.Core/Workflow/MathlibConventions.cs b/src/LeanStudio.Core/Workflow/MathlibConventions.cs index 13cb901..9da913e 100644 --- a/src/LeanStudio.Core/Workflow/MathlibConventions.cs +++ b/src/LeanStudio.Core/Workflow/MathlibConventions.cs @@ -5,12 +5,13 @@ namespace LeanStudio.Core.Workflow; /// /// The file conventions Mathlib asks of a contributor beyond the text rules in : the /// copyright header at the top, a module docstring (/-! … -/) before the first declaration, and theorem names that -/// do not start with a capital (a theorem is named in snake_case; only types and structures are UpperCamelCase). -/// Rules reported: copyright-header, module-doc and theorem-name. +/// do not start with a capital (a theorem is named in snake_case) and structure, class and inductive names that do not +/// (types are UpperCamelCase). Rules reported: copyright-header, module-doc, theorem-name and type-name. /// public static class MathlibConventions { private static readonly Regex Copyright = new(@"^Copyright \(c\) \d{4}(?:, \d{4})* .+\. All rights reserved\.$", RegexOptions.Compiled); + private static readonly Regex TypeDecl = new(@"^\s*(?:@\[[^\]]*\]\s*)*(?:(?:protected|private|public|nonrec|unsafe)\s+)*(?:structure|class|inductive)\s+(?[^\s:({\[]+)", RegexOptions.Compiled); private static readonly Regex Theorem = new(@"^\s*(?:@\[[^\]]*\]\s*)*(?:(?:protected|private|nonrec)\s+)*(?:theorem|lemma)\s+(?[^\s:({\[]+)", RegexOptions.Compiled); /// The convention problems in , in line order. @@ -29,6 +30,15 @@ public static IReadOnlyList Find(string text) } for (int i = 0; i < lines.Length; i++) { + Match t = TypeDecl.Match(lines[i]); + if (t.Success) + { + string typeName = t.Groups["n"].Value.Split('.')[^1]; + if (typeName.Length > 0 && char.IsLower(typeName[0])) + { + problems.Add(new StyleProblem(i, "type-name", $"`{typeName}`: a structure, class or inductive type is named in UpperCamelCase.")); + } + } Match m = Theorem.Match(lines[i]); if (m.Success) { diff --git a/src/LeanStudio.Core/Workflow/StyleCheck.cs b/src/LeanStudio.Core/Workflow/StyleCheck.cs index 2d03510..a3290dc 100644 --- a/src/LeanStudio.Core/Workflow/StyleCheck.cs +++ b/src/LeanStudio.Core/Workflow/StyleCheck.cs @@ -75,4 +75,84 @@ public static string Fix(string text) string body = string.Join('\n', lines).TrimEnd('\n'); return body.Length == 0 ? "" : body + "\n"; } + + /// + /// with the comment lines longer than characters broken at a space: + /// a -- comment continues on a new -- line, and a line of prose in a doc or module comment continues on the + /// next line. Code is never touched: not a line outside a comment, not one in a code fence or indented four spaces or + /// more inside a comment, not a word longer than the limit (a URL). + /// + public static string WrapComments(string text, int max = MaxLineLength) + { + string[] lines = text.Split('\n'); + var output = new List(lines.Length); + int depth = 0; + bool fence = false; + foreach (string raw in lines) + { + string cr = raw.EndsWith('\r') ? "\r" : ""; + string line = cr.Length > 0 ? raw[..^1] : raw; + bool inBlock = depth > 0; + depth = Math.Max(0, depth + BlockDelta(line)); + string? prefix = null; + if (!inBlock && line.TrimStart().StartsWith("--", StringComparison.Ordinal)) + { + int dash = line.IndexOf("--", StringComparison.Ordinal); + int end = dash + 2; + while (end < line.Length && line[end] is '-' or '!') + { + end++; + } + prefix = line[..end] + " "; + } + else if (inBlock || line.TrimStart().StartsWith("/-", StringComparison.Ordinal)) + { + if (line.TrimStart().StartsWith("```", StringComparison.Ordinal)) + { + fence = !fence; + } + else if (!fence && !(inBlock && line.StartsWith(" ", StringComparison.Ordinal))) + { + prefix = line[..(line.Length - line.TrimStart().Length)]; + } + } + if (depth == 0 && !inBlock && prefix is null || prefix is null) + { + output.Add(raw); + continue; + } + while (new System.Globalization.StringInfo(line).LengthInTextElements > max) + { + int cut = line.LastIndexOf(' ', Math.Min(max, line.Length - 1)); + if (cut <= prefix.Length || line[prefix.Length..cut].Trim().Length == 0) + { + break; // one long word: leave it + } + output.Add(line[..cut].TrimEnd() + cr); + line = prefix + line[(cut + 1)..].TrimStart(); + } + output.Add(line + cr); + } + return string.Join('\n', output); + } + + /// How much a line opens more block comments than it closes (/- against -/). + private static int BlockDelta(string line) + { + int delta = 0; + for (int i = 0; i + 1 < line.Length; i++) + { + if (line[i] == '/' && line[i + 1] == '-') + { + delta++; + i++; + } + else if (line[i] == '-' && line[i + 1] == '/') + { + delta--; + i++; + } + } + return delta; + } } diff --git a/src/LeanStudio.Mcp/LeanTools.cs b/src/LeanStudio.Mcp/LeanTools.cs index 3499789..aca3d6d 100644 --- a/src/LeanStudio.Mcp/LeanTools.cs +++ b/src/LeanStudio.Mcp/LeanTools.cs @@ -719,10 +719,11 @@ public static IReadOnlyList Tools(Workbench bench) => }), new("style_check", - "Check a Lean file against the text rules Mathlib's CI holds it to: no trailing whitespace, no line over 100 characters, no tabs, LF line endings, exactly one newline at the end. In a project that uses Mathlib (or with mathlib=true) it also checks Mathlib's file conventions: the copyright header, a module docstring, theorem names in snake_case, and a doc comment on every public definition. With apply=true, fixes what has one obvious fix (the text rules, except long lines) on disk.", + "Check a Lean file against the text rules Mathlib's CI holds it to: no trailing whitespace, no line over 100 characters, no tabs, LF line endings, exactly one newline at the end. In a project that uses Mathlib (or with mathlib=true) it also checks Mathlib's file conventions: the copyright header, a module docstring, theorem names in snake_case, type names in UpperCamelCase, and a doc comment on every public definition. With apply=true, fixes what has one obvious fix (the text rules, except long lines) on disk.", Schema(("path", "string", "The .lean file.", true), ("apply", "boolean", "Fix the fixable problems on disk (default false).", false), - ("mathlib", "boolean", "Also check Mathlib's file conventions (default: when the project uses Mathlib).", false)), + ("mathlib", "boolean", "Also check Mathlib's file conventions (default: when the project uses Mathlib).", false), + ("wrap", "boolean", "With apply, also break comment and docstring lines over 100 characters at a space (default false).", false)), async (a, ct) => { string path = LeanFile(bench, a); @@ -745,7 +746,8 @@ public static IReadOnlyList Tools(Workbench bench) => } if (OptBool(a, "apply") == true) { - await File.WriteAllTextAsync(path, StyleCheck.Fix(text), ct); + string fixedText = StyleCheck.Fix(text); + await File.WriteAllTextAsync(path, OptBool(a, "wrap") == true ? StyleCheck.WrapComments(fixedText) : fixedText, ct); string[] fixable = ["trailing-whitespace", "tab", "crlf", "final-newline"]; int left = problems.Count(p => !fixable.Contains(p.Rule)); sb.Append(CultureInfo.InvariantCulture, $"fixed {problems.Count - left} problem(s); {left} are left for you"); diff --git a/tests/LeanStudio.Tests/PickerAndConflictTests.cs b/tests/LeanStudio.Tests/PickerAndConflictTests.cs index c63a214..a66c831 100644 --- a/tests/LeanStudio.Tests/PickerAndConflictTests.cs +++ b/tests/LeanStudio.Tests/PickerAndConflictTests.cs @@ -190,6 +190,11 @@ async Task Call(string tool, System.Text.Json.Nodes.JsonObject args) Assert.Contains("module-doc", conventions, StringComparison.Ordinal); Assert.Contains("A.lean:4: missing-doc: `x` has no doc comment.", conventions, StringComparison.Ordinal); + await File.WriteAllTextAsync(file, "-- " + string.Join(' ', Enumerable.Repeat("word", 40)) + "\n", TestContext.Current.CancellationToken); + await Call("style_check", new() { ["path"] = file, ["apply"] = true, ["wrap"] = true }); + Assert.All((await File.ReadAllTextAsync(file, TestContext.Current.CancellationToken)).Split('\n'), l => Assert.True(l.Length <= 100, l)); + Assert.Equal("no style problems", await Call("style_check", new() { ["path"] = file })); + await File.WriteAllTextAsync(file, "@[deprecated (since := \"2020-01-01\")] alias old := new\n\ndef new := 1\n", TestContext.Current.CancellationToken); Assert.Contains("old, deprecated 2020-01-01", await Call("stale_deprecations", new() { ["path"] = file }), StringComparison.Ordinal); Assert.Contains("no deprecation is that old", await Call("stale_deprecations", new() { ["path"] = file, ["months"] = 1000 }), StringComparison.Ordinal); @@ -230,6 +235,13 @@ public void FlagsTheoremNamesThatStartWithACapital() Assert.Equal([(7, "theorem-name"), (8, "theorem-name")], MathlibConventions.Find(text).Select(p => (p.Line, p.Rule))); } + [Fact] + public void FlagsTypeNamesThatStartLowercase() + { + string text = Header + "/-! Doc -/\n\nstructure point where\n x : Nat\n\nclass N.isGood (a : Nat) : Prop\ninductive Tree\n@[simp] structure Foo.bar\n"; + Assert.Equal([(7, "type-name"), (10, "type-name"), (12, "type-name")], MathlibConventions.Find(text).Select(p => (p.Line, p.Rule))); + } + [Fact] public void AddsTheHeaderOnlyWhereThereIsNoCommentFirst() { @@ -300,3 +312,45 @@ public void LeavesOutIndentedCommentedAndTheoremsUnlessAsked() Assert.Equal([7], DocCoverage.Find(text, includeTheorems: true).Select(p => p.Line)); } } + +/// Breaking long comment lines. +public sealed class WrapCommentsTests +{ + [Fact] + public void WrapsALineCommentOntoAnotherLineComment() + { + string text = "-- one two three four five six seven eight nine ten eleven twelve thirteen fourteen fifteen sixteen\n"; + string wrapped = StyleCheck.WrapComments(text, 90); + Assert.Equal("-- one two three four five six seven eight nine ten eleven twelve thirteen fourteen\n-- fifteen sixteen\n", wrapped); + Assert.All(wrapped.Split('\n'), l => Assert.True(l.Length <= 90, l)); + Assert.Equal(" /- one two three four -/\n", StyleCheck.WrapComments(" /- one two three four -/\n", 90)); + } + + [Fact] + public void WrapsProseInADocCommentAndKeepsItsEnd() + { + string text = "/-- alpha beta gamma delta epsilon zeta eta theta iota kappa lambda mu nu xi omicron pi rho sigma tau. -/\ndef x := 1\n"; + Assert.Equal("/-- alpha beta gamma delta epsilon zeta eta theta iota kappa lambda mu nu xi omicron pi rho sigma\ntau. -/\ndef x := 1\n", StyleCheck.WrapComments(text)); + string multi = "/-!\n# Title\n" + string.Join(' ', Enumerable.Range(0, 30).Select(i => "word" + i)) + "\n-/\n"; + string wrapped = StyleCheck.WrapComments(multi); + Assert.All(wrapped.Split('\n'), l => Assert.True(l.Length <= 100, l)); + Assert.Equal(multi.Split((char[]?)null, StringSplitOptions.RemoveEmptyEntries), wrapped.Split((char[]?)null, StringSplitOptions.RemoveEmptyEntries)); // no word lost or changed + } + + [Fact] + public void LeavesCodeFencesIndentedCodeUrlsAndCrlfAlone() + { + string code = "def " + string.Join(" ", Enumerable.Repeat("verylongidentifier", 8)) + " := 1\n"; + Assert.Equal(code, StyleCheck.WrapComments(code)); + string fence = "/--\n```\n" + new string('a', 40) + " " + new string('b', 70) + "\n```\n-/\n"; + Assert.Equal(fence, StyleCheck.WrapComments(fence)); + string url = "-- see https://example.com/" + new string('x', 120) + "\n"; + Assert.Equal("-- see\n-- https://example.com/" + new string('x', 120) + "\n", StyleCheck.WrapComments(url)); // the URL goes whole onto a line of its own + string bare = "-- https://example.com/" + new string('x', 120) + "\n"; + Assert.Equal(bare, StyleCheck.WrapComments(bare)); + Assert.Equal("-- " + string.Join(' ', Enumerable.Repeat("word", 25)) + "\r\n", StyleCheck.WrapComments("-- " + string.Join(' ', Enumerable.Repeat("word", 25)) + "\r\n", 200)); + string crlf = "-- " + string.Join(' ', Enumerable.Repeat("word", 30)) + "\r\n"; + Assert.All(StyleCheck.WrapComments(crlf, 60).Split('\n').Where(l => l.Length > 0), l => Assert.EndsWith("\r", l, StringComparison.Ordinal)); + Assert.DoesNotContain(StyleCheck.Find(StyleCheck.WrapComments("-- " + string.Join(' ', Enumerable.Repeat("word", 40)) + "\n")), p => p.Rule == "long-line"); + } +} From b49b068757a29b34246a62a4bade70d626542329 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 3 Oct 2026 19:15:24 +0000 Subject: [PATCH 07/18] Add Copy as a Zulip Message Co-Authored-By: Claude Sonnet 5.5 Claude-Session: https://claude.ai/code/session_01FF5AYRpU9TWeWY3CFh2ETw --- CHANGELOG.md | 1 + README.md | 1 + docs/ARCHITECTURE.md | 2 +- .../ViewModels/MainViewModel.Assist.cs | 19 ++++++++ src/LeanStudio.App/Views/MainWindow.axaml | 1 + src/LeanStudio.App/Views/MainWindow.axaml.cs | 1 + src/LeanStudio.Core/Workflow/ZulipPost.cs | 44 +++++++++++++++++++ .../PickerAndConflictTests.cs | 21 +++++++++ 8 files changed, 89 insertions(+), 1 deletion(-) create mode 100644 src/LeanStudio.Core/Workflow/ZulipPost.cs diff --git a/CHANGELOG.md b/CHANGELOG.md index d761569..c2e6360 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -23,6 +23,7 @@ - **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. - **Over MCP**, `sort_imports` and `style_check` do the same for assistants, each with `apply` to write the file. **Fixes**: diff --git a/README.md b/README.md index df3f473..e7c2568 100644 --- a/README.md +++ b/README.md @@ -331,6 +331,7 @@ What CI and reviewers check, before you push: - **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. +- **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. diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index b0609b3..cec1e22 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -129,7 +129,7 @@ shows them to a person or an assistant. | [`Proofs/`](../src/LeanStudio.Core/Proofs) | Features that ask Lean about proofs: `ProofSteps` (the tactic block around a line, read by layout), `ProofSearch` (Prove It and counterexamples) and `Scratch` (scratch documents in the running server), `ExtractLemma`, `Profiler` (Lean's profilers read into a `ProfileReport`: trees, categories, counters, per-line costs; its records are in `ProfileModel`), `LiveProfiler` (the same, from the running server as the file is edited), `ProfileCheck` (saved profiles in `ProfileStore`, and the heartbeat regression check), `Heartbeats`, `ProofStates` (the Proof-State Map), `Walkthrough` (the HTML export) and `LeanRepl`. | | [`Ai/`](../src/LeanStudio.Core/Ai) | The AI in the editor: `IChatModel` and the clients behind it (`AppleIntelligence` and `AppleFmCliModel` for the `fm` command, `OllamaModel`, `OpenAiCompatibleModel`, `AnthropicModel`), `AiDiscovery` (what is running, and which model to use), `AiProver` (proofs from a model, checked by Lean), `AiAssistant` (explanations and chat), `AiText` (token estimates and trimming) and `SecretStore` (API keys). | | [`Editing/`](../src/LeanStudio.Core/Editing) | Text-level engines with no UI: `Abbreviations` (Unicode input), `LeanText` (comments, strings and declarations in Lean source), `LatexText` (docstring math as text), `Fuzzy` (picker matching), `ProjectSearch` (find and replace across files), `MultiCursor`, `VimEngine`, `EmacsEngine` and `KeyBindingsFile` (keybindings.json). The editor in the app is a thin host over them. | -| [`Workflow/`](../src/LeanStudio.Core/Workflow) | Project-wide tools. `Workflow.cs` holds `Markers` (sorries and TODOs), `LakeOutput` (build problems), `LocalHistory`, `Loogle`, `LeanSearch`, `DocLinks`, `Blame` and `ProjectTasks`. Beside it: `Refactor` and `EmittedC` (module rename, replace across files, Compiled C), `Ffi` (`@[extern]` bindings checked against the project's C files, and C stubs), `ImportCheck` (unused imports), `ImportOrder` (sorted imports), `StyleCheck` (Mathlib's text rules), `MathlibConventions` (header, module docstring, theorem names), `DocCoverage` (definitions with no doc comment), `StaleDeprecations` (old deprecated aliases, found and deleted), `Lint`, `Instances`, `Deprecation` (deprecated aliases for renames), `DependencyBump` (Update Mathlib and see what broke), `Blueprint`, `ProjectCommands` (`.leanstudio/commands.json`), `ProgressReader` (progress read from what a task prints), `LeanCli` (the `lean` command line on a mirror copy) and `Essentials.cs` (`ElanInstaller`, `FileOps`, `ImportFinder`). | +| [`Workflow/`](../src/LeanStudio.Core/Workflow) | Project-wide tools. `Workflow.cs` holds `Markers` (sorries and TODOs), `LakeOutput` (build problems), `LocalHistory`, `Loogle`, `LeanSearch`, `DocLinks`, `Blame` and `ProjectTasks`. Beside it: `Refactor` and `EmittedC` (module rename, replace across files, Compiled C), `Ffi` (`@[extern]` bindings checked against the project's C files, and C stubs), `ImportCheck` (unused imports), `ImportOrder` (sorted imports), `StyleCheck` (Mathlib's text rules), `MathlibConventions` (header, module docstring, theorem names), `DocCoverage` (definitions with no doc comment), `StaleDeprecations` (old deprecated aliases, found and deleted), `ZulipPost` (a question for the Lean Zulip chat), `Lint`, `Instances`, `Deprecation` (deprecated aliases for renames), `DependencyBump` (Update Mathlib and see what broke), `Blueprint`, `ProjectCommands` (`.leanstudio/commands.json`), `ProgressReader` (progress read from what a task prints), `LeanCli` (the `lean` command line on a mirror copy) and `Essentials.cs` (`ElanInstaller`, `FileOps`, `ImportFinder`). | | [`Git/`](../src/LeanStudio.Core/Git) | `GitRepository` wraps your own `git` executable, so your config, hooks, credentials and signing all apply. `GitHub` goes through the `gh` CLI, so Lean Studio never handles a token. | | [`Learn/`](../src/LeanStudio.Core/Learn) | `Tutorial` and `Playground`; `TacticGuide`, `ErrorGuide` and `PlainEnglish` (goals read aloud) in `Guides.cs`; `Snippets`, `TheoremGallery` and `ProgramRunner` in `Library.cs`. | | [`Agents/`](../src/LeanStudio.Core/Agents) | For assistants and web pages: `Workbench` and `ProjectSession` (Lean for a program instead of a person, used by the MCP server), `StudioBridge` (the pipe between an assistant and an open window), `InfoviewBridge` (Lean's own infoview page, served to a web view or browser) and `AgentSetup` (writing each assistant's MCP configuration). | diff --git a/src/LeanStudio.App/ViewModels/MainViewModel.Assist.cs b/src/LeanStudio.App/ViewModels/MainViewModel.Assist.cs index 06ef43f..daaa365 100644 --- a/src/LeanStudio.App/ViewModels/MainViewModel.Assist.cs +++ b/src/LeanStudio.App/ViewModels/MainViewModel.Assist.cs @@ -571,6 +571,25 @@ private async Task CopyShareLinkAsync() } } + /// + /// Copy the active file as a question for the Lean Zulip chat: the code in a lean fence and, in a quote, what Lean + /// said about it (errors first), ready to paste. + /// + [RelayCommand] + private async Task CopyForZulipAsync() + { + if (ActiveDocument is not { IsLean: true } d) + { + return; + } + IEnumerable messages = d.Diagnostics.Where(x => x.Severity is not DiagnosticSeverity.Hint) + .Select(x => new ZulipMessage(x.Range.Start.Line + 1, x.Range.Start.Character + 1, + x.Severity switch { DiagnosticSeverity.Error => "error", DiagnosticSeverity.Warning => "warning", _ => "info" }, x.Message)); + string post = ZulipPost.Build(d.Document.Text, messages); + await _dialogs.CopyTextAsync(post); + Log("Copied this file as a Zulip message: the code, then what Lean says about it. Paste it into the chat; trim it to the smallest example that still shows the problem first."); + } + private async Task ShareUrlAsync() { if (ActiveDocument is not { IsLean: true } d) diff --git a/src/LeanStudio.App/Views/MainWindow.axaml b/src/LeanStudio.App/Views/MainWindow.axaml index d4da292..b6b4302 100644 --- a/src/LeanStudio.App/Views/MainWindow.axaml +++ b/src/LeanStudio.App/Views/MainWindow.axaml @@ -56,6 +56,7 @@ + diff --git a/src/LeanStudio.App/Views/MainWindow.axaml.cs b/src/LeanStudio.App/Views/MainWindow.axaml.cs index 36d8b40..5dda1cd 100644 --- a/src/LeanStudio.App/Views/MainWindow.axaml.cs +++ b/src/LeanStudio.App/Views/MainWindow.axaml.cs @@ -1182,6 +1182,7 @@ private void OnLocationDoubleTapped(object? sender, TappedEventArgs e) yield return ("File: Export Proof Walkthrough…", "", Cmd(_vm.ExportWalkthroughCommand)); yield return ("Share: Open in the Lean 4 Web Editor", "", Cmd(_vm.OpenInWebEditorCommand)); yield return ("Share: Copy Share Link", "", Cmd(_vm.CopyShareLinkCommand)); + yield return ("Share: Copy as a Zulip Message", "", Cmd(_vm.CopyForZulipCommand)); yield return ("Library: Ask Mathlib in Plain English (LeanSearch)", "", Act(() => _vm.SidebarTab = MainViewModel.LibraryTab)); yield return ("View: Profiler", "", Act(() => _vm.BottomTab = MainViewModel.TimingPanel)); yield return ("Project: Edit This Project's Commands (commands.json)", "", Cmd(_vm.EditProjectCommandsCommand)); diff --git a/src/LeanStudio.Core/Workflow/ZulipPost.cs b/src/LeanStudio.Core/Workflow/ZulipPost.cs new file mode 100644 index 0000000..3ffba24 --- /dev/null +++ b/src/LeanStudio.Core/Workflow/ZulipPost.cs @@ -0,0 +1,44 @@ +using System.Text; + +namespace LeanStudio.Core.Workflow; + +/// One message Lean gave about the code in a . +/// 1-based line. +/// 1-based column. +/// error, warning or info. +/// What Lean said. +public sealed record ZulipMessage(int Line, int Column, string Severity, string Text); + +/// +/// A question for the Lean Zulip chat, ready to paste: the code in a lean fence, then what Lean said about it in +/// a quote (errors first), the way a minimal working example is usually asked about there. The fences are long +/// enough that backticks in the code cannot end them early. +/// +public static class ZulipPost +{ + /// The message to paste: and, when there are any, . + public static string Build(string code, IEnumerable messages) + { + var sb = new StringBuilder(); + sb.Append(Fence(code, "lean", code.TrimEnd('\n', '\r'))); + List ordered = [.. messages.OrderBy(m => m.Severity == "error" ? 0 : m.Severity == "warning" ? 1 : 2).ThenBy(m => m.Line).ThenBy(m => m.Column)]; + if (ordered.Count > 0) + { + string body = string.Join("\n\n", ordered.Select(m => $"{m.Severity} ({m.Line}:{m.Column}): {m.Text.Trim()}")); + sb.Append('\n').Append(Fence(body, "quote", body)); + } + return sb.ToString(); + } + + private static string Fence(string within, string language, string body) + { + int longest = 0, run = 0; + foreach (char c in within) + { + run = c == '`' ? run + 1 : 0; + longest = Math.Max(longest, run); + } + string fence = new('`', Math.Max(3, longest + 1)); + return $"{fence}{language}\n{body}\n{fence}\n"; + } +} diff --git a/tests/LeanStudio.Tests/PickerAndConflictTests.cs b/tests/LeanStudio.Tests/PickerAndConflictTests.cs index a66c831..33c6f61 100644 --- a/tests/LeanStudio.Tests/PickerAndConflictTests.cs +++ b/tests/LeanStudio.Tests/PickerAndConflictTests.cs @@ -354,3 +354,24 @@ public void LeavesCodeFencesIndentedCodeUrlsAndCrlfAlone() Assert.DoesNotContain(StyleCheck.Find(StyleCheck.WrapComments("-- " + string.Join(' ', Enumerable.Repeat("word", 40)) + "\n")), p => p.Rule == "long-line"); } } + +/// A question ready to paste into the Lean Zulip chat. +public sealed class ZulipPostTests +{ + [Fact] + public void PutsTheCodeInAFenceAndErrorsFirstInAQuote() + { + string post = ZulipPost.Build("example : 1 = 2 := by\n simp\n\n", + [new ZulipMessage(2, 3, "warning", "unused"), new ZulipMessage(2, 3, "error", "simp made no progress\n"), new ZulipMessage(1, 1, "info", "hello")]); + Assert.Equal("```lean\nexample : 1 = 2 := by\n simp\n```\n\n```quote\nerror (2:3): simp made no progress\n\nwarning (2:3): unused\n\ninfo (1:1): hello\n```\n", post); + } + + [Fact] + public void LeavesOutTheQuoteWithoutMessagesAndLengthensFencesAroundBackticks() + { + Assert.Equal("```lean\n#eval 1\n```\n", ZulipPost.Build("#eval 1\n", [])); + string post = ZulipPost.Build("/-- Uses ``` fences. -/\ndef a := 1", [new ZulipMessage(1, 1, "error", "see ````x````")]); + Assert.StartsWith("````lean\n", post, StringComparison.Ordinal); + Assert.Contains("`````quote\n", post, StringComparison.Ordinal); + } +} From 60b861d9f0dd30e95c783ba9b3654442c58f9462 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 3 Oct 2026 19:35:19 +0000 Subject: [PATCH 08/18] Add a Mathlib-style theorem name suggestion Co-Authored-By: Claude Sonnet 5.5 Claude-Session: https://claude.ai/code/session_01FF5AYRpU9TWeWY3CFh2ETw --- CHANGELOG.md | 1 + README.md | 1 + docs/ARCHITECTURE.md | 4 +- .../ViewModels/MainViewModel.Pro.cs | 22 ++ src/LeanStudio.App/Views/MainWindow.axaml | 1 + src/LeanStudio.App/Views/MainWindow.axaml.cs | 1 + src/LeanStudio.Core/Workflow/TheoremNamer.cs | 300 ++++++++++++++++++ src/LeanStudio.Mcp/LeanTools.cs | 5 + .../PickerAndConflictTests.cs | 46 +++ 9 files changed, 379 insertions(+), 2 deletions(-) create mode 100644 src/LeanStudio.Core/Workflow/TheoremNamer.cs diff --git a/CHANGELOG.md b/CHANGELOG.md index c2e6360..ac83f53 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -24,6 +24,7 @@ - **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. - **Over MCP**, `sort_imports` and `style_check` do the same for assistants, each with `apply` to write the file. **Fixes**: diff --git a/README.md b/README.md index e7c2568..6e8125c 100644 --- a/README.md +++ b/README.md @@ -331,6 +331,7 @@ What CI and reviewers check, before you push: - **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. +- **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. diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index cec1e22..3da076b 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -129,7 +129,7 @@ shows them to a person or an assistant. | [`Proofs/`](../src/LeanStudio.Core/Proofs) | Features that ask Lean about proofs: `ProofSteps` (the tactic block around a line, read by layout), `ProofSearch` (Prove It and counterexamples) and `Scratch` (scratch documents in the running server), `ExtractLemma`, `Profiler` (Lean's profilers read into a `ProfileReport`: trees, categories, counters, per-line costs; its records are in `ProfileModel`), `LiveProfiler` (the same, from the running server as the file is edited), `ProfileCheck` (saved profiles in `ProfileStore`, and the heartbeat regression check), `Heartbeats`, `ProofStates` (the Proof-State Map), `Walkthrough` (the HTML export) and `LeanRepl`. | | [`Ai/`](../src/LeanStudio.Core/Ai) | The AI in the editor: `IChatModel` and the clients behind it (`AppleIntelligence` and `AppleFmCliModel` for the `fm` command, `OllamaModel`, `OpenAiCompatibleModel`, `AnthropicModel`), `AiDiscovery` (what is running, and which model to use), `AiProver` (proofs from a model, checked by Lean), `AiAssistant` (explanations and chat), `AiText` (token estimates and trimming) and `SecretStore` (API keys). | | [`Editing/`](../src/LeanStudio.Core/Editing) | Text-level engines with no UI: `Abbreviations` (Unicode input), `LeanText` (comments, strings and declarations in Lean source), `LatexText` (docstring math as text), `Fuzzy` (picker matching), `ProjectSearch` (find and replace across files), `MultiCursor`, `VimEngine`, `EmacsEngine` and `KeyBindingsFile` (keybindings.json). The editor in the app is a thin host over them. | -| [`Workflow/`](../src/LeanStudio.Core/Workflow) | Project-wide tools. `Workflow.cs` holds `Markers` (sorries and TODOs), `LakeOutput` (build problems), `LocalHistory`, `Loogle`, `LeanSearch`, `DocLinks`, `Blame` and `ProjectTasks`. Beside it: `Refactor` and `EmittedC` (module rename, replace across files, Compiled C), `Ffi` (`@[extern]` bindings checked against the project's C files, and C stubs), `ImportCheck` (unused imports), `ImportOrder` (sorted imports), `StyleCheck` (Mathlib's text rules), `MathlibConventions` (header, module docstring, theorem names), `DocCoverage` (definitions with no doc comment), `StaleDeprecations` (old deprecated aliases, found and deleted), `ZulipPost` (a question for the Lean Zulip chat), `Lint`, `Instances`, `Deprecation` (deprecated aliases for renames), `DependencyBump` (Update Mathlib and see what broke), `Blueprint`, `ProjectCommands` (`.leanstudio/commands.json`), `ProgressReader` (progress read from what a task prints), `LeanCli` (the `lean` command line on a mirror copy) and `Essentials.cs` (`ElanInstaller`, `FileOps`, `ImportFinder`). | +| [`Workflow/`](../src/LeanStudio.Core/Workflow) | Project-wide tools. `Workflow.cs` holds `Markers` (sorries and TODOs), `LakeOutput` (build problems), `LocalHistory`, `Loogle`, `LeanSearch`, `DocLinks`, `Blame` and `ProjectTasks`. Beside it: `Refactor` and `EmittedC` (module rename, replace across files, Compiled C), `Ffi` (`@[extern]` bindings checked against the project's C files, and C stubs), `ImportCheck` (unused imports), `ImportOrder` (sorted imports), `StyleCheck` (Mathlib's text rules), `MathlibConventions` (header, module docstring, theorem names), `DocCoverage` (definitions with no doc comment), `StaleDeprecations` (old deprecated aliases, found and deleted), `ZulipPost` (a question for the Lean Zulip chat), `TheoremNamer` (a Mathlib-style name from a statement), `Lint`, `Instances`, `Deprecation` (deprecated aliases for renames), `DependencyBump` (Update Mathlib and see what broke), `Blueprint`, `ProjectCommands` (`.leanstudio/commands.json`), `ProgressReader` (progress read from what a task prints), `LeanCli` (the `lean` command line on a mirror copy) and `Essentials.cs` (`ElanInstaller`, `FileOps`, `ImportFinder`). | | [`Git/`](../src/LeanStudio.Core/Git) | `GitRepository` wraps your own `git` executable, so your config, hooks, credentials and signing all apply. `GitHub` goes through the `gh` CLI, so Lean Studio never handles a token. | | [`Learn/`](../src/LeanStudio.Core/Learn) | `Tutorial` and `Playground`; `TacticGuide`, `ErrorGuide` and `PlainEnglish` (goals read aloud) in `Guides.cs`; `Snippets`, `TheoremGallery` and `ProgramRunner` in `Library.cs`. | | [`Agents/`](../src/LeanStudio.Core/Agents) | For assistants and web pages: `Workbench` and `ProjectSession` (Lean for a program instead of a person, used by the MCP server), `StudioBridge` (the pipe between an assistant and an open window), `InfoviewBridge` (Lean's own infoview page, served to a web view or browser) and `AgentSetup` (writing each assistant's MCP configuration). | @@ -174,7 +174,7 @@ written to stdout. | Checking and reading a file | `project_info`, `check_file`, `goals`, `proof_steps`, `hover`, `suggestions`, `references`, `run_lean` | | Building and Tenet | `build`, `verify`, `axioms`, `why_not_proved`, `project_map` | | Proof tools | `prove`, `extract_lemma`, `ffi_bindings`, `profile` | -| For Mathlib contributors | `unused_imports`, `sort_imports`, `style_check`, `stale_deprecations`, `lint`, `heartbeats`, `instances`, `blueprint` | +| For Mathlib contributors | `unused_imports`, `sort_imports`, `style_check`, `stale_deprecations`, `suggest_name`, `lint`, `heartbeats`, `instances`, `blueprint` | | Walkthroughs and search | `export_walkthrough`, `search_mathlib`, and `declaration` and `search_declarations` (the compiled library, through Tenet) | | Toolchains | `toolchains` | | The open window | `studio_context`, `studio_show` | diff --git a/src/LeanStudio.App/ViewModels/MainViewModel.Pro.cs b/src/LeanStudio.App/ViewModels/MainViewModel.Pro.cs index a16b94e..6654399 100644 --- a/src/LeanStudio.App/ViewModels/MainViewModel.Pro.cs +++ b/src/LeanStudio.App/ViewModels/MainViewModel.Pro.cs @@ -592,6 +592,28 @@ public void WrapLongComments() + (wrapped == text ? "" : " Undo brings the old text back.")); } + /// + /// Suggest a Mathlib-style name for the theorem at the cursor, worked out from its statement (a + b = b + a is + /// add_comm), and say whether it matches the one it has. The name is only a starting point; Rename Symbol applies it. + /// + [RelayCommand] + public void SuggestTheoremName() + { + if (ActiveDocument is not { IsLean: true } d) + { + return; + } + if (TheoremNamer.SuggestAt(d.Document.Text, d.CaretLine) is not var (current, statement, suggested)) + { + Log("Name: put the cursor in a theorem whose statement is about operations and relations (like a + b = b + a)."); + return; + } + string last = current.Split('.')[^1]; + Log(last == suggested + ? $"Name: `{last}` is the name Mathlib's scheme gives {statement}." + : $"Name: Mathlib's scheme gives `{suggested}` for {statement}; this one is `{last}`. A suggestion only: use Rename Symbol (F2) to apply it."); + } + // ---- linters ---- /// diff --git a/src/LeanStudio.App/Views/MainWindow.axaml b/src/LeanStudio.App/Views/MainWindow.axaml index b6b4302..b67203b 100644 --- a/src/LeanStudio.App/Views/MainWindow.axaml +++ b/src/LeanStudio.App/Views/MainWindow.axaml @@ -123,6 +123,7 @@ + diff --git a/src/LeanStudio.App/Views/MainWindow.axaml.cs b/src/LeanStudio.App/Views/MainWindow.axaml.cs index 5dda1cd..77a9f4f 100644 --- a/src/LeanStudio.App/Views/MainWindow.axaml.cs +++ b/src/LeanStudio.App/Views/MainWindow.axaml.cs @@ -1080,6 +1080,7 @@ private void OnLocationDoubleTapped(object? sender, TappedEventArgs e) yield return ("Lean: Lean's Processes (memory, stop a runaway file)…", "", LeanProcessesAsync); yield return ("Lean: Remove Unused Imports", "", Cmd(_vm.RemoveUnusedImportsCommand)); yield return ("Lean: Sort Imports", "", Cmd(_vm.SortImportsCommand)); + yield return ("Lean: Suggest a Name for This Theorem", "", Cmd(_vm.SuggestTheoremNameCommand)); yield return ("Lean: Tidy Whitespace and Check Style", "", Cmd(_vm.TidyWhitespaceCommand)); yield return ("Lean: Tidy File (sort imports, fix whitespace)", "", Cmd(_vm.TidyFileCommand)); yield return ("Lean: Wrap Long Comment Lines", "", Cmd(_vm.WrapLongCommentsCommand)); diff --git a/src/LeanStudio.Core/Workflow/TheoremNamer.cs b/src/LeanStudio.Core/Workflow/TheoremNamer.cs new file mode 100644 index 0000000..7681b0f --- /dev/null +++ b/src/LeanStudio.Core/Workflow/TheoremNamer.cs @@ -0,0 +1,300 @@ +using System.Text; +using System.Text.RegularExpressions; + +namespace LeanStudio.Core.Workflow; + +/// +/// A name for a theorem in Mathlib's naming scheme, worked out from its statement: the conclusion first, read left to +/// right with each operation and relation spelled as a word (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), then _of_ before each thing it assumes. A starting +/// point for a person, who knows the library's own conventions better than a rule can: it handles statements about +/// operations and relations, and says nothing (null) for one it can't read. +/// +public static class TheoremNamer +{ + private static readonly (string Symbol, string Word)[] Relations = + [ + ("↔", "iff"), ("≠", "ne"), ("≤", "le"), ("≥", "ge"), ("∣", "dvd"), ("∉", "not_mem"), ("∈", "mem"), ("⊆", "subset"), + ("<", "lt"), (">", "gt"), ("=", "eq"), + ]; + + private static readonly Dictionary Operations = new() + { + ['+'] = "add", ['*'] = "mul", ['/'] = "div", ['^'] = "pow", ['∪'] = "union", ['∩'] = "inter", ['∧'] = "and", ['∨'] = "or", + ['∑'] = "sum", ['∏'] = "prod", ['∘'] = "comp", ['•'] = "smul", ['%'] = "mod", ['⊔'] = "sup", ['⊓'] = "inf", + }; + + /// + /// The suggested name for the statement : what follows the theorem's name, such as + /// (a b : ℕ) : a + b = b + a or just a ≤ b → b < c → a < c. Null when no relation can be read from it. + /// + public static string? Suggest(string statement) + { + var hypotheses = new List(); + string rest = statement.Trim(); + // Binders come before the colon that starts the conclusion; those whose type states something are assumptions. + int colon = rest.StartsWith('∀') ? -1 : TopLevelColon(rest); + if (colon >= 0) + { + foreach (string binder in Groups(rest[..colon])) + { + int c = binder.IndexOf(':', StringComparison.Ordinal); + if (c >= 0 && FindRelation(binder[(c + 1)..]) is not null) + { + hypotheses.Add(binder[(c + 1)..]); + } + } + rest = rest[(colon + 1)..]; + } + rest = StripForall(rest.Trim()); + List parts = SplitTop(rest, "→"); + string conclusion = parts[^1]; + hypotheses.AddRange(parts[..^1]); + string? head = Words(conclusion); + if (head is null) + { + return null; + } + string[] assumed = [.. hypotheses.Select(Words).Where(w => w is not null).Select(w => w!)]; + return head + string.Concat(assumed.Select(w => "_of_" + w)); + } + + private static readonly Regex Declaration = new(@"^\s*(?:@\[[^\]]*\]\s*)*(?:(?:protected|private|nonrec)\s+)*(?:theorem|lemma)\s+(?\S+)", RegexOptions.Compiled); + + /// + /// The theorem or lemma whose declaration contains 0-based of : its + /// name as written, its statement (up to :=, on one line) and the suggested name; null when the line is + /// not in one or no name can be worked out. + /// + public static (string Current, string Statement, string Suggested)? SuggestAt(string text, int line) + { + string[] lines = text.Split('\n'); + if (line < 0 || line >= lines.Length || lines[line].Trim().Length == 0) + { + return null; // a blank line between declarations belongs to none + } + for (int start = line; start >= 0; start--) + { + Match m = Declaration.Match(lines[start]); + if (!m.Success) + { + if (start < line && lines[start].Length > 0 && !char.IsWhiteSpace(lines[start][0])) + { + return null; // a different command begins above the line + } + continue; + } + var statement = new StringBuilder(lines[start][(m.Index + m.Length)..]); + for (int i = start + 1; i < lines.Length && !statement.ToString().Contains(":=", StringComparison.Ordinal) && i <= start + 12; i++) + { + statement.Append(' ').Append(lines[i].Trim()); + } + string stmt = statement.ToString(); + int end = stmt.IndexOf(":=", StringComparison.Ordinal); + stmt = (end >= 0 ? stmt[..end] : stmt).Trim(); + return Suggest(stmt) is string name ? (m.Groups["name"].Value, stmt, name) : null; + } + return null; + } + + /// The words of one proposition (a + b = b + a → add_comm), or null without a relation. + private static string? Words(string prop) + { + string p = prop.Trim(); + bool negated = false; + if (p.StartsWith('¬')) + { + negated = true; + p = p[1..].Trim(); + } + (int at, string symbol, string word)? rel = FindRelation(p); + if (rel is not { } r) + { + return null; + } + string left = p[..r.at].Trim(), right = p[(r.at + r.symbol.Length)..].Trim(); + List l = Terms(left), rt = Terms(right); + string? result = Special(r.word, left, right, l, rt); + if (result is null) + { + bool eqWithAtom = r.word == "eq" && (rt.Count == 0 || l.Count == 0); + var words = new List(); + if (eqWithAtom) + { + words.AddRange(l.Count > 0 ? l : rt); + } + else + { + words.AddRange(l); + words.Add(r.word); + words.AddRange(rt); + } + if (SelfApplied(left) || SelfApplied(right) || (l.Count == 0 && rt.Count > 0 && Identifiers(right).Contains(left))) + { + words.Add("self"); + } + result = string.Join('_', words); + } + return negated ? "not_" + result : result; + } + + /// Names Mathlib spells specially: commutativity and associativity. + private static string? Special(string relation, string left, string right, List l, List r) + { + if (relation != "eq" || l.Count == 0 || !l.SequenceEqual(r)) + { + return null; + } + List a = Identifiers(left), b = Identifiers(right); + if (a.Count >= 2 && a.SequenceEqual(b.AsEnumerable().Reverse()) && l.Distinct().Count() == 1 && l.Count == 1) + { + return l[0] + "_comm"; + } + if (a.Count == 3 && a.SequenceEqual(b) && l.Count == 2 && l.Distinct().Count() == 1) + { + return l[0] + "_assoc"; + } + return null; + } + + /// The operation and constant words of a term, in the order written; empty for a bare variable. + private static List Terms(string term) + { + var words = new List(); + bool operandNext = true; + foreach (char c in term) + { + if (Operations.TryGetValue(c, out string? op)) + { + words.Add(op); + operandNext = true; + } + else if (c == '-') + { + words.Add(operandNext ? "neg" : "sub"); + operandNext = true; + } + else if (c is '0' or '1' or '2' && words.Count > 0 | !term.Trim().All(char.IsDigit)) + { + words.Add(c switch { '0' => "zero", '1' => "one", _ => "two" }); + operandNext = false; + } + else if (!char.IsWhiteSpace(c) && c is not '(' and not ')') + { + operandNext = false; + } + else if (c == '(') + { + operandNext = true; + } + } + // A bare numeral (`= 0`) is a constant, not an operation: it names nothing by itself. + return term.Trim().All(char.IsDigit) ? [] : words; + } + + private static bool SelfApplied(string term) + { + List ids = Identifiers(term); + return ids.Count == 2 && ids[0] == ids[1] && Terms(term).Count == 1; + } + + private static List Identifiers(string term) + { + var ids = new List(); + var sb = new StringBuilder(); + foreach (char c in term + " ") + { + if (char.IsLetter(c) || c == '_' || (sb.Length > 0 && (char.IsDigit(c) || c == '\''))) + { + sb.Append(c); + } + else if (sb.Length > 0) + { + ids.Add(sb.ToString()); + sb.Clear(); + } + } + return ids; + } + + private static (int At, string Symbol, string Word)? FindRelation(string text) + { + int depth = 0; + foreach ((string symbol, string word) in Relations.Where(x => x.Symbol == "↔").Concat(Relations.Where(x => x.Symbol != "↔"))) + { + depth = 0; + for (int i = 0; i < text.Length; i++) + { + char c = text[i]; + depth += c is '(' or '[' or '{' ? 1 : c is ')' or ']' or '}' ? -1 : 0; + if (depth == 0 && string.CompareOrdinal(text, i, symbol, 0, symbol.Length) == 0 + && !(symbol == "=" && i > 0 && text[i - 1] is '<' or '>' or '≠' or ':' or '=') && !(symbol is "<" or ">" && i + 1 < text.Length && text[i + 1] == '-')) + { + return (i, symbol, word); + } + } + } + return null; + } + + private static int TopLevelColon(string text) + { + int depth = 0; + for (int i = 0; i < text.Length; i++) + { + depth += text[i] is '(' or '[' or '{' ? 1 : text[i] is ')' or ']' or '}' ? -1 : 0; + if (depth == 0 && text[i] == ':' && (i + 1 >= text.Length || text[i + 1] != '=')) + { + return i; + } + } + return -1; + } + + private static IEnumerable Groups(string binders) + { + int depth = 0, start = 0; + for (int i = 0; i < binders.Length; i++) + { + if (binders[i] is '(' or '{' or '[') + { + if (depth++ == 0) + { + start = i + 1; + } + } + else if (binders[i] is ')' or '}' or ']' && --depth == 0) + { + yield return binders[start..i]; + } + } + } + + private static List SplitTop(string text, string separator) + { + var parts = new List(); + int depth = 0, start = 0; + for (int i = 0; i < text.Length; i++) + { + depth += text[i] is '(' or '[' or '{' ? 1 : text[i] is ')' or ']' or '}' ? -1 : 0; + if (depth == 0 && string.CompareOrdinal(text, i, separator, 0, separator.Length) == 0) + { + parts.Add(text[start..i]); + start = i + separator.Length; + i += separator.Length - 1; + } + } + parts.Add(text[start..]); + return parts; + } + + private static string StripForall(string text) + { + if (!text.StartsWith('∀')) + { + return text; + } + int comma = text.IndexOf(',', StringComparison.Ordinal); + return comma < 0 ? text : text[(comma + 1)..].Trim(); + } +} diff --git a/src/LeanStudio.Mcp/LeanTools.cs b/src/LeanStudio.Mcp/LeanTools.cs index aca3d6d..2e2f5a1 100644 --- a/src/LeanStudio.Mcp/LeanTools.cs +++ b/src/LeanStudio.Mcp/LeanTools.cs @@ -782,6 +782,11 @@ public static IReadOnlyList Tools(Workbench bench) => return sb.ToString().TrimEnd(); }), + new("suggest_name", + "A name for a theorem in Mathlib's naming scheme, worked out from its statement: the conclusion read left to right with each operation and relation as a word (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), then _of_ before each assumption. A starting point only: it reads statements about operations and relations, and says so when it can't.", + Schema(("statement", "string", "What follows the theorem's name, up to :=, such as \"(a b : ℕ) : a + b = b + a\".", true)), + (a, ct) => Task.FromResult(TheoremNamer.Suggest(Str(a, "statement")) ?? "no name: the statement has no relation (=, ≤, <, ↔ …) to read")), + new("lint", "Run the linters CI runs on a Lean file of a Lake project: Mathlib's standard set in a project that uses Mathlib (its style linters among them), every linter Lean has elsewhere, and Batteries' environment linters (missing docstrings, simp normal form, unused arguments…) where Batteries is available. Lints the file as saved on disk.", Schema(("path", "string", "The .lean file.", true)), diff --git a/tests/LeanStudio.Tests/PickerAndConflictTests.cs b/tests/LeanStudio.Tests/PickerAndConflictTests.cs index 33c6f61..8d2b90d 100644 --- a/tests/LeanStudio.Tests/PickerAndConflictTests.cs +++ b/tests/LeanStudio.Tests/PickerAndConflictTests.cs @@ -170,6 +170,9 @@ async Task Call(string tool, System.Text.Json.Nodes.JsonObject args) return result["content"]![0]!["text"]!.GetValue(); } + Assert.Equal("add_comm", await Call("suggest_name", new() { ["statement"] = "(a b : ℕ) : a + b = b + a" })); + Assert.StartsWith("no name", await Call("suggest_name", new() { ["statement"] = "True" }), StringComparison.Ordinal); + string preview = await Call("sort_imports", new() { ["path"] = file }); Assert.Contains("import A \nimport B", preview, StringComparison.Ordinal); Assert.StartsWith("import B\n", await File.ReadAllTextAsync(file, TestContext.Current.CancellationToken), StringComparison.Ordinal); // not written @@ -375,3 +378,46 @@ public void LeavesOutTheQuoteWithoutMessagesAndLengthensFencesAroundBackticks() Assert.Contains("`````quote\n", post, StringComparison.Ordinal); } } + +/// Naming a theorem the way Mathlib would, from its statement. +public sealed class TheoremNamerTests +{ + [Theory] + [InlineData("(a b : ℕ) : a + b = b + a", "add_comm")] + [InlineData("(a b : ℕ) : a * b = b * a", "mul_comm")] + [InlineData("(a b c : ℕ) : a + b + c = a + (b + c)", "add_assoc")] + [InlineData("(a : ℕ) : a + 0 = a", "add_zero")] + [InlineData("(a : ℕ) : 0 + a = a", "zero_add")] + [InlineData("(a : ℕ) : a * 1 = a", "mul_one")] + [InlineData("(a : ℤ) : - -a = a", "neg_neg")] + [InlineData("(a : ℤ) : a - a = 0", "sub_self")] + [InlineData("(a b c d : ℕ) : a + b ≤ c + d", "add_le_add")] + [InlineData("(a b c : ℕ) : a ≤ b → b < c → a < c", "lt_of_le_of_lt")] + [InlineData("(a b : ℕ) (h : a < b) : a ≤ b", "le_of_lt")] + [InlineData("a ≤ a + b", "le_add_self")] + [InlineData("¬ a < b", "not_lt")] + public void NamesTheStatementTheMathlibWay(string statement, string name) => Assert.Equal(name, TheoremNamer.Suggest(statement)); + + [Fact] + public void FindsTheDeclarationAroundALine() + { + const string text = "def x := 1\n\n@[simp] theorem foo (a b : ℕ) :\n a + b = b + a := by\n omega\n\ntheorem bar : True := trivial\n"; + Assert.Equal(("foo", "(a b : ℕ) : a + b = b + a", "add_comm"), TheoremNamer.SuggestAt(text, 3)); + Assert.Equal(("foo", "(a b : ℕ) : a + b = b + a", "add_comm"), TheoremNamer.SuggestAt(text, 2)); + Assert.Null(TheoremNamer.SuggestAt(text, 0)); // a def + Assert.Null(TheoremNamer.SuggestAt(text, 6)); // no relation to read + Assert.Null(TheoremNamer.SuggestAt(text, 5)); // between declarations: the one above ended + } + + [Theory] + [InlineData("(a : ℕ) : True")] + [InlineData("")] + public void SaysNothingWhenThereIsNoRelationToRead(string statement) => Assert.Null(TheoremNamer.Suggest(statement)); + + [Fact] + public void KeepsAssumptionsInTheirOrderAndIgnoresBindersThatStateNothing() + { + Assert.Equal("add_le_add_of_le_of_lt", TheoremNamer.Suggest("{α : Type} (a b c d : α) (h₁ : a ≤ b) (h₂ : c < d) : a + c ≤ b + d")); + Assert.Equal("mul_comm", TheoremNamer.Suggest("∀ a b : ℕ, a * b = b * a")); + } +} From 542f00499c7ea2afe76c16b71f0685856ef721f8 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 3 Oct 2026 19:37:11 +0000 Subject: [PATCH 09/18] Add Merge Consecutive rw / intro Steps Co-Authored-By: Claude Sonnet 5.5 Claude-Session: https://claude.ai/code/session_01FF5AYRpU9TWeWY3CFh2ETw --- CHANGELOG.md | 1 + README.md | 1 + docs/ARCHITECTURE.md | 2 +- .../ViewModels/MainViewModel.Pro.cs | 23 ++++++++ src/LeanStudio.App/Views/MainWindow.axaml | 1 + src/LeanStudio.App/Views/MainWindow.axaml.cs | 1 + src/LeanStudio.Core/Proofs/TacticGolf.cs | 59 +++++++++++++++++++ src/LeanStudio.Mcp/LeanTools.cs | 21 +++++++ .../PickerAndConflictTests.cs | 54 +++++++++++++++++ 9 files changed, 162 insertions(+), 1 deletion(-) create mode 100644 src/LeanStudio.Core/Proofs/TacticGolf.cs diff --git a/CHANGELOG.md b/CHANGELOG.md index ac83f53..53cf1d5 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -25,6 +25,7 @@ - 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. - **Over MCP**, `sort_imports` and `style_check` do the same for assistants, each with `apply` to write the file. **Fixes**: diff --git a/README.md b/README.md index 6e8125c..b4bea73 100644 --- a/README.md +++ b/README.md @@ -331,6 +331,7 @@ What CI and reviewers check, before you push: - **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. +- **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. diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index 3da076b..fec96f3 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -126,7 +126,7 @@ shows them to a person or an assistant. | [`Projects/`](../src/LeanStudio.Core/Projects) | `LeanProject` (a Lake project, a folder pinned to a toolchain, or a bare folder; the kind decides how Lean starts and what "build" means), `Lake` (build, clean, update, fetch Mathlib's cache, new projects from templates), `ImportGraph` (Imports and Imported By) and `LibraryRoot` (the root file that imports every module, like `lake exe mk_all`). | | [`Toolchains/`](../src/LeanStudio.Core/Toolchains) | `Elan`: finds elan, lists, installs and removes toolchains, and sets the default. Every Lean executable runs through elan's proxies, so a project's `lean-toolchain` file picks the version. `LeanProcesses` lists Lean's file workers with their memory. `LeanReleases` decides whether a newer stable Lean is worth offering (only to a project with no dependencies, pinned to a plain release). | | [`Verification/`](../src/LeanStudio.Core/Verification) | `TenetWorkspace`: opens a project's `.olean` files (and everything they import) with Tenet. It re-checks declarations, computes axioms, finds why a theorem is not fully proved, builds the Project Map, checks blueprint nodes, and serves the declaration navigator. See [Tenet's workspace](#how-the-main-features-work) below. | -| [`Proofs/`](../src/LeanStudio.Core/Proofs) | Features that ask Lean about proofs: `ProofSteps` (the tactic block around a line, read by layout), `ProofSearch` (Prove It and counterexamples) and `Scratch` (scratch documents in the running server), `ExtractLemma`, `Profiler` (Lean's profilers read into a `ProfileReport`: trees, categories, counters, per-line costs; its records are in `ProfileModel`), `LiveProfiler` (the same, from the running server as the file is edited), `ProfileCheck` (saved profiles in `ProfileStore`, and the heartbeat regression check), `Heartbeats`, `ProofStates` (the Proof-State Map), `Walkthrough` (the HTML export) and `LeanRepl`. | +| [`Proofs/`](../src/LeanStudio.Core/Proofs) | `TacticGolf` (consecutive rw and intro lines merged). Features that ask Lean about proofs: `ProofSteps` (the tactic block around a line, read by layout), `ProofSearch` (Prove It and counterexamples) and `Scratch` (scratch documents in the running server), `ExtractLemma`, `Profiler` (Lean's profilers read into a `ProfileReport`: trees, categories, counters, per-line costs; its records are in `ProfileModel`), `LiveProfiler` (the same, from the running server as the file is edited), `ProfileCheck` (saved profiles in `ProfileStore`, and the heartbeat regression check), `Heartbeats`, `ProofStates` (the Proof-State Map), `Walkthrough` (the HTML export) and `LeanRepl`. | | [`Ai/`](../src/LeanStudio.Core/Ai) | The AI in the editor: `IChatModel` and the clients behind it (`AppleIntelligence` and `AppleFmCliModel` for the `fm` command, `OllamaModel`, `OpenAiCompatibleModel`, `AnthropicModel`), `AiDiscovery` (what is running, and which model to use), `AiProver` (proofs from a model, checked by Lean), `AiAssistant` (explanations and chat), `AiText` (token estimates and trimming) and `SecretStore` (API keys). | | [`Editing/`](../src/LeanStudio.Core/Editing) | Text-level engines with no UI: `Abbreviations` (Unicode input), `LeanText` (comments, strings and declarations in Lean source), `LatexText` (docstring math as text), `Fuzzy` (picker matching), `ProjectSearch` (find and replace across files), `MultiCursor`, `VimEngine`, `EmacsEngine` and `KeyBindingsFile` (keybindings.json). The editor in the app is a thin host over them. | | [`Workflow/`](../src/LeanStudio.Core/Workflow) | Project-wide tools. `Workflow.cs` holds `Markers` (sorries and TODOs), `LakeOutput` (build problems), `LocalHistory`, `Loogle`, `LeanSearch`, `DocLinks`, `Blame` and `ProjectTasks`. Beside it: `Refactor` and `EmittedC` (module rename, replace across files, Compiled C), `Ffi` (`@[extern]` bindings checked against the project's C files, and C stubs), `ImportCheck` (unused imports), `ImportOrder` (sorted imports), `StyleCheck` (Mathlib's text rules), `MathlibConventions` (header, module docstring, theorem names), `DocCoverage` (definitions with no doc comment), `StaleDeprecations` (old deprecated aliases, found and deleted), `ZulipPost` (a question for the Lean Zulip chat), `TheoremNamer` (a Mathlib-style name from a statement), `Lint`, `Instances`, `Deprecation` (deprecated aliases for renames), `DependencyBump` (Update Mathlib and see what broke), `Blueprint`, `ProjectCommands` (`.leanstudio/commands.json`), `ProgressReader` (progress read from what a task prints), `LeanCli` (the `lean` command line on a mirror copy) and `Essentials.cs` (`ElanInstaller`, `FileOps`, `ImportFinder`). | diff --git a/src/LeanStudio.App/ViewModels/MainViewModel.Pro.cs b/src/LeanStudio.App/ViewModels/MainViewModel.Pro.cs index 6654399..77a11f8 100644 --- a/src/LeanStudio.App/ViewModels/MainViewModel.Pro.cs +++ b/src/LeanStudio.App/ViewModels/MainViewModel.Pro.cs @@ -1,6 +1,7 @@ using CommunityToolkit.Mvvm.ComponentModel; using CommunityToolkit.Mvvm.Input; using LeanStudio.Core.Projects; +using LeanStudio.Core.Proofs; using LeanStudio.Core.Workflow; using LeanStudio.Lsp; @@ -614,6 +615,28 @@ public void SuggestTheoremName() : $"Name: Mathlib's scheme gives `{suggested}` for {statement}; this one is `{last}`. A suggestion only: use Rename Symbol (F2) to apply it."); } + /// + /// Merge the tactics of the active file that follow each other and say the same thing once: rw [a] then + /// rw [b] become rw [a, b] (also simp_rw, and the same at), and two intros become one. As one undoable edit. + /// + [RelayCommand] + public void MergeConsecutiveTactics() + { + if (ActiveDocument is not { IsLean: true } d) + { + return; + } + string text = d.Document.Text; + (string merged, int count) = TacticGolf.Merge(text); + if (count == 0) + { + Log("Merge: no rw, simp_rw or intro lines in a row to merge."); + return; + } + d.Document.Replace(0, text.Length, merged); + Log($"Merge: {count} line{(count == 1 ? "" : "s")} merged into the one before. Undo brings them back."); + } + // ---- linters ---- /// diff --git a/src/LeanStudio.App/Views/MainWindow.axaml b/src/LeanStudio.App/Views/MainWindow.axaml index b67203b..fe12a50 100644 --- a/src/LeanStudio.App/Views/MainWindow.axaml +++ b/src/LeanStudio.App/Views/MainWindow.axaml @@ -124,6 +124,7 @@ + diff --git a/src/LeanStudio.App/Views/MainWindow.axaml.cs b/src/LeanStudio.App/Views/MainWindow.axaml.cs index 77a9f4f..248de52 100644 --- a/src/LeanStudio.App/Views/MainWindow.axaml.cs +++ b/src/LeanStudio.App/Views/MainWindow.axaml.cs @@ -1080,6 +1080,7 @@ private void OnLocationDoubleTapped(object? sender, TappedEventArgs e) yield return ("Lean: Lean's Processes (memory, stop a runaway file)…", "", LeanProcessesAsync); yield return ("Lean: Remove Unused Imports", "", Cmd(_vm.RemoveUnusedImportsCommand)); yield return ("Lean: Sort Imports", "", Cmd(_vm.SortImportsCommand)); + yield return ("Lean: Merge Consecutive rw / intro Steps", "", Cmd(_vm.MergeConsecutiveTacticsCommand)); yield return ("Lean: Suggest a Name for This Theorem", "", Cmd(_vm.SuggestTheoremNameCommand)); yield return ("Lean: Tidy Whitespace and Check Style", "", Cmd(_vm.TidyWhitespaceCommand)); yield return ("Lean: Tidy File (sort imports, fix whitespace)", "", Cmd(_vm.TidyFileCommand)); diff --git a/src/LeanStudio.Core/Proofs/TacticGolf.cs b/src/LeanStudio.Core/Proofs/TacticGolf.cs new file mode 100644 index 0000000..7f82c10 --- /dev/null +++ b/src/LeanStudio.Core/Proofs/TacticGolf.cs @@ -0,0 +1,59 @@ +using System.Text.RegularExpressions; + +namespace LeanStudio.Core.Proofs; + +/// +/// The small clean-ups a reviewer asks for in a proof, made where they cannot change what the proof does: two +/// rewrites in a row become one (rw [a] then rw [b] is rw [a, b], the same for simp_rw), and so do two +/// intros. Only whole lines that do nothing else are merged: the same indentation, no comment, no +/// ; or <;>, and for a rewrite the same location (at h). +/// +public static class TacticGolf +{ + private static readonly Regex Rewrite = new(@"^(?\s*)(?rw|simp_rw)\s*\[(?[^\]\n]*)\](?\s+at\s+[^\n;<]+?)?\s*$", RegexOptions.Compiled); + private static readonly Regex Intro = new(@"^(?\s*)intro\s+(?[^;\n<-]+?)\s*$", RegexOptions.Compiled); + + /// with the consecutive rewrites and intros merged, and how many lines went. + public static (string Text, int Merged) Merge(string text) + { + string[] lines = text.Split('\n'); + var output = new List(lines.Length); + int merged = 0; + for (int i = 0; i < lines.Length; i++) + { + string line = lines[i]; + string cr = line.EndsWith('\r') ? "\r" : ""; + string plain = line.TrimEnd('\r'); + while (i + 1 < lines.Length) + { + string next = lines[i + 1].TrimEnd('\r'); + string? joined = Join(plain, next); + if (joined is null) + { + break; + } + plain = joined; + i++; + merged++; + } + output.Add(plain + cr); + } + return (string.Join('\n', output), merged); + } + + private static string? Join(string first, string second) + { + Match a = Rewrite.Match(first), b = Rewrite.Match(second); + if (a.Success && b.Success && a.Groups["ind"].Value == b.Groups["ind"].Value && a.Groups["tac"].Value == b.Groups["tac"].Value + && a.Groups["at"].Value.Trim() == b.Groups["at"].Value.Trim() && a.Groups["rules"].Value.Trim().Length > 0 && b.Groups["rules"].Value.Trim().Length > 0) + { + return $"{a.Groups["ind"].Value}{a.Groups["tac"].Value} [{a.Groups["rules"].Value.Trim()}, {b.Groups["rules"].Value.Trim()}]{a.Groups["at"].Value}"; + } + Match c = Intro.Match(first), d = Intro.Match(second); + if (c.Success && d.Success && c.Groups["ind"].Value == d.Groups["ind"].Value) + { + return $"{c.Groups["ind"].Value}intro {c.Groups["args"].Value.Trim()} {d.Groups["args"].Value.Trim()}"; + } + return null; + } +} diff --git a/src/LeanStudio.Mcp/LeanTools.cs b/src/LeanStudio.Mcp/LeanTools.cs index 2e2f5a1..7d6418b 100644 --- a/src/LeanStudio.Mcp/LeanTools.cs +++ b/src/LeanStudio.Mcp/LeanTools.cs @@ -787,6 +787,27 @@ public static IReadOnlyList Tools(Workbench bench) => Schema(("statement", "string", "What follows the theorem's name, up to :=, such as \"(a b : ℕ) : a + b = b + a\".", true)), (a, ct) => Task.FromResult(TheoremNamer.Suggest(Str(a, "statement")) ?? "no name: the statement has no relation (=, ≤, <, ↔ …) to read")), + new("merge_tactics", + "Merge the tactics of a Lean file that follow each other and say the same thing once, where that cannot change the proof: `rw [a]` then `rw [b]` become `rw [a, b]` (also simp_rw, and the same `at` location), and two `intro` lines become one. Only whole lines that do nothing else are merged. With apply=true, writes the file on disk.", + Schema(("path", "string", "The .lean file.", true), + ("apply", "boolean", "Write the merged file to disk (default false).", false)), + async (a, ct) => + { + string path = LeanFile(bench, a); + string text = await File.ReadAllTextAsync(path, ct); + (string merged, int count) = TacticGolf.Merge(text); + if (count == 0) + { + return "nothing to merge"; + } + if (OptBool(a, "apply") == true) + { + await File.WriteAllTextAsync(path, merged, ct); + return $"merged {count} line(s) in {path}"; + } + return $"{count} line(s) can be merged into the one before (pass apply=true to write them)"; + }), + new("lint", "Run the linters CI runs on a Lean file of a Lake project: Mathlib's standard set in a project that uses Mathlib (its style linters among them), every linter Lean has elsewhere, and Batteries' environment linters (missing docstrings, simp normal form, unused arguments…) where Batteries is available. Lints the file as saved on disk.", Schema(("path", "string", "The .lean file.", true)), diff --git a/tests/LeanStudio.Tests/PickerAndConflictTests.cs b/tests/LeanStudio.Tests/PickerAndConflictTests.cs index 8d2b90d..4e57048 100644 --- a/tests/LeanStudio.Tests/PickerAndConflictTests.cs +++ b/tests/LeanStudio.Tests/PickerAndConflictTests.cs @@ -1,4 +1,5 @@ using LeanStudio.Core.Editing; +using LeanStudio.Core.Proofs; using LeanStudio.Core.Workflow; namespace LeanStudio.Tests; @@ -173,6 +174,13 @@ async Task Call(string tool, System.Text.Json.Nodes.JsonObject args) Assert.Equal("add_comm", await Call("suggest_name", new() { ["statement"] = "(a b : ℕ) : a + b = b + a" })); Assert.StartsWith("no name", await Call("suggest_name", new() { ["statement"] = "True" }), StringComparison.Ordinal); + string proof = Path.Combine(dir, "P.lean"); + await File.WriteAllTextAsync(proof, "theorem t : P := by\n rw [a]\n rw [b]\n exact h\n", TestContext.Current.CancellationToken); + Assert.StartsWith("1 line(s) can be merged", await Call("merge_tactics", new() { ["path"] = proof }), StringComparison.Ordinal); + await Call("merge_tactics", new() { ["path"] = proof, ["apply"] = true }); + Assert.Equal("theorem t : P := by\n rw [a, b]\n exact h\n", await File.ReadAllTextAsync(proof, TestContext.Current.CancellationToken)); + Assert.Equal("nothing to merge", await Call("merge_tactics", new() { ["path"] = proof })); + string preview = await Call("sort_imports", new() { ["path"] = file }); Assert.Contains("import A \nimport B", preview, StringComparison.Ordinal); Assert.StartsWith("import B\n", await File.ReadAllTextAsync(file, TestContext.Current.CancellationToken), StringComparison.Ordinal); // not written @@ -421,3 +429,49 @@ public void KeepsAssumptionsInTheirOrderAndIgnoresBindersThatStateNothing() Assert.Equal("mul_comm", TheoremNamer.Suggest("∀ a b : ℕ, a * b = b * a")); } } + +/// Merging tactics that follow each other, where that cannot change the proof. +public sealed class TacticGolfTests +{ + [Fact] + public void MergesRewritesAndIntrosInARow() + { + const string text = "theorem t : P := by\n intro x\n intro y z\n rw [a]\n rw [← b, c]\n rw [d]\n simp_rw [e]\n simp_rw [f]\n exact h\n"; + var (merged, count) = TacticGolf.Merge(text); + Assert.Equal("theorem t : P := by\n intro x y z\n rw [a, ← b, c, d]\n simp_rw [e, f]\n exact h\n", merged); + Assert.Equal(4, count); + Assert.Equal((merged, 0), TacticGolf.Merge(merged)); // nothing left to merge + } + + [Fact] + public void MergesRewritesAtTheSameLocationOnly() + { + var (merged, count) = TacticGolf.Merge(" rw [a] at h\n rw [b] at h\n rw [c] at g\n rw [d]\n rw [e] at h ⊢\n"); + Assert.Equal(" rw [a, b] at h\n rw [c] at g\n rw [d]\n rw [e] at h ⊢\n", merged); + Assert.Equal(1, count); + } + + [Fact] + public void LeavesWhatItCannotMergeSafely() + { + foreach (string text in new[] + { + " rw [a] -- why\n rw [b]\n", // a comment + " rw [a]; simp\n rw [b]\n", // another tactic on the line + " rw [a]\n rw [b]\n", // different indentation + " intro x\n rw [b]\n", // different tactics + " simp_rw [a]\n rw [b]\n", + " intro x <;> simp\n intro y\n", + " rw [a]\n\n rw [b]\n", // a blank line between + }) + { + Assert.Equal((text, 0), TacticGolf.Merge(text)); + } + } + + [Fact] + public void KeepsCrlfLineEndings() + { + Assert.Equal((" intro x y\r\n exact h\r\n", 1), TacticGolf.Merge(" intro x\r\n intro y\r\n exact h\r\n")); + } +} From d1605dbf0bbae6787cfc89866aa34a9b6fa8616c Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 3 Oct 2026 19:39:49 +0000 Subject: [PATCH 10/18] Add Find Duplicate Theorem Statements Co-Authored-By: Claude Sonnet 5.5 Claude-Session: https://claude.ai/code/session_01FF5AYRpU9TWeWY3CFh2ETw --- CHANGELOG.md | 1 + README.md | 1 + docs/ARCHITECTURE.md | 4 +- .../ViewModels/MainViewModel.Pro.cs | 34 ++++++ src/LeanStudio.App/Views/MainWindow.axaml | 1 + src/LeanStudio.App/Views/MainWindow.axaml.cs | 1 + .../Workflow/DuplicateStatements.cs | 110 ++++++++++++++++++ src/LeanStudio.Mcp/LeanTools.cs | 23 ++++ .../PickerAndConflictTests.cs | 57 +++++++++ 9 files changed, 230 insertions(+), 2 deletions(-) create mode 100644 src/LeanStudio.Core/Workflow/DuplicateStatements.cs diff --git a/CHANGELOG.md b/CHANGELOG.md index 53cf1d5..10e9a0d 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -26,6 +26,7 @@ - **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. - **Over MCP**, `sort_imports` and `style_check` do the same for assistants, each with `apply` to write the file. **Fixes**: diff --git a/README.md b/README.md index b4bea73..f0b681b 100644 --- a/README.md +++ b/README.md @@ -331,6 +331,7 @@ What CI and reviewers check, before you push: - **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. +- **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. diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index fec96f3..cd8932a 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -129,7 +129,7 @@ shows them to a person or an assistant. | [`Proofs/`](../src/LeanStudio.Core/Proofs) | `TacticGolf` (consecutive rw and intro lines merged). Features that ask Lean about proofs: `ProofSteps` (the tactic block around a line, read by layout), `ProofSearch` (Prove It and counterexamples) and `Scratch` (scratch documents in the running server), `ExtractLemma`, `Profiler` (Lean's profilers read into a `ProfileReport`: trees, categories, counters, per-line costs; its records are in `ProfileModel`), `LiveProfiler` (the same, from the running server as the file is edited), `ProfileCheck` (saved profiles in `ProfileStore`, and the heartbeat regression check), `Heartbeats`, `ProofStates` (the Proof-State Map), `Walkthrough` (the HTML export) and `LeanRepl`. | | [`Ai/`](../src/LeanStudio.Core/Ai) | The AI in the editor: `IChatModel` and the clients behind it (`AppleIntelligence` and `AppleFmCliModel` for the `fm` command, `OllamaModel`, `OpenAiCompatibleModel`, `AnthropicModel`), `AiDiscovery` (what is running, and which model to use), `AiProver` (proofs from a model, checked by Lean), `AiAssistant` (explanations and chat), `AiText` (token estimates and trimming) and `SecretStore` (API keys). | | [`Editing/`](../src/LeanStudio.Core/Editing) | Text-level engines with no UI: `Abbreviations` (Unicode input), `LeanText` (comments, strings and declarations in Lean source), `LatexText` (docstring math as text), `Fuzzy` (picker matching), `ProjectSearch` (find and replace across files), `MultiCursor`, `VimEngine`, `EmacsEngine` and `KeyBindingsFile` (keybindings.json). The editor in the app is a thin host over them. | -| [`Workflow/`](../src/LeanStudio.Core/Workflow) | Project-wide tools. `Workflow.cs` holds `Markers` (sorries and TODOs), `LakeOutput` (build problems), `LocalHistory`, `Loogle`, `LeanSearch`, `DocLinks`, `Blame` and `ProjectTasks`. Beside it: `Refactor` and `EmittedC` (module rename, replace across files, Compiled C), `Ffi` (`@[extern]` bindings checked against the project's C files, and C stubs), `ImportCheck` (unused imports), `ImportOrder` (sorted imports), `StyleCheck` (Mathlib's text rules), `MathlibConventions` (header, module docstring, theorem names), `DocCoverage` (definitions with no doc comment), `StaleDeprecations` (old deprecated aliases, found and deleted), `ZulipPost` (a question for the Lean Zulip chat), `TheoremNamer` (a Mathlib-style name from a statement), `Lint`, `Instances`, `Deprecation` (deprecated aliases for renames), `DependencyBump` (Update Mathlib and see what broke), `Blueprint`, `ProjectCommands` (`.leanstudio/commands.json`), `ProgressReader` (progress read from what a task prints), `LeanCli` (the `lean` command line on a mirror copy) and `Essentials.cs` (`ElanInstaller`, `FileOps`, `ImportFinder`). | +| [`Workflow/`](../src/LeanStudio.Core/Workflow) | Project-wide tools. `Workflow.cs` holds `Markers` (sorries and TODOs), `LakeOutput` (build problems), `LocalHistory`, `Loogle`, `LeanSearch`, `DocLinks`, `Blame` and `ProjectTasks`. Beside it: `Refactor` and `EmittedC` (module rename, replace across files, Compiled C), `Ffi` (`@[extern]` bindings checked against the project's C files, and C stubs), `ImportCheck` (unused imports), `ImportOrder` (sorted imports), `StyleCheck` (Mathlib's text rules), `MathlibConventions` (header, module docstring, theorem names), `DocCoverage` (definitions with no doc comment), `StaleDeprecations` (old deprecated aliases, found and deleted), `ZulipPost` (a question for the Lean Zulip chat), `TheoremNamer` (a Mathlib-style name from a statement), `DuplicateStatements` (theorems that state the same thing), `Lint`, `Instances`, `Deprecation` (deprecated aliases for renames), `DependencyBump` (Update Mathlib and see what broke), `Blueprint`, `ProjectCommands` (`.leanstudio/commands.json`), `ProgressReader` (progress read from what a task prints), `LeanCli` (the `lean` command line on a mirror copy) and `Essentials.cs` (`ElanInstaller`, `FileOps`, `ImportFinder`). | | [`Git/`](../src/LeanStudio.Core/Git) | `GitRepository` wraps your own `git` executable, so your config, hooks, credentials and signing all apply. `GitHub` goes through the `gh` CLI, so Lean Studio never handles a token. | | [`Learn/`](../src/LeanStudio.Core/Learn) | `Tutorial` and `Playground`; `TacticGuide`, `ErrorGuide` and `PlainEnglish` (goals read aloud) in `Guides.cs`; `Snippets`, `TheoremGallery` and `ProgramRunner` in `Library.cs`. | | [`Agents/`](../src/LeanStudio.Core/Agents) | For assistants and web pages: `Workbench` and `ProjectSession` (Lean for a program instead of a person, used by the MCP server), `StudioBridge` (the pipe between an assistant and an open window), `InfoviewBridge` (Lean's own infoview page, served to a web view or browser) and `AgentSetup` (writing each assistant's MCP configuration). | @@ -174,7 +174,7 @@ written to stdout. | Checking and reading a file | `project_info`, `check_file`, `goals`, `proof_steps`, `hover`, `suggestions`, `references`, `run_lean` | | Building and Tenet | `build`, `verify`, `axioms`, `why_not_proved`, `project_map` | | Proof tools | `prove`, `extract_lemma`, `ffi_bindings`, `profile` | -| For Mathlib contributors | `unused_imports`, `sort_imports`, `style_check`, `stale_deprecations`, `suggest_name`, `lint`, `heartbeats`, `instances`, `blueprint` | +| For Mathlib contributors | `unused_imports`, `sort_imports`, `style_check`, `stale_deprecations`, `suggest_name`, `duplicate_statements`, `lint`, `heartbeats`, `instances`, `blueprint` | | Walkthroughs and search | `export_walkthrough`, `search_mathlib`, and `declaration` and `search_declarations` (the compiled library, through Tenet) | | Toolchains | `toolchains` | | The open window | `studio_context`, `studio_show` | diff --git a/src/LeanStudio.App/ViewModels/MainViewModel.Pro.cs b/src/LeanStudio.App/ViewModels/MainViewModel.Pro.cs index 77a11f8..9dcc082 100644 --- a/src/LeanStudio.App/ViewModels/MainViewModel.Pro.cs +++ b/src/LeanStudio.App/ViewModels/MainViewModel.Pro.cs @@ -637,6 +637,40 @@ public void MergeConsecutiveTactics() Log($"Merge: {count} line{(count == 1 ? "" : "s")} merged into the one before. Undo brings them back."); } + /// + /// Look through the project's Lean files for theorems that state the same thing under different names (the names of + /// the variables they bind and the spacing do not count), and list each group in Output. + /// + [RelayCommand] + public async Task FindDuplicateStatementsAsync() + { + if (Project is null) + { + Log("Duplicates: open a project first."); + return; + } + string root = Project.Root; + ProStatus = "Comparing the project's theorem statements…"; + try + { + IReadOnlyList> groups = await Task.Run(() => DuplicateStatements.Scan(root)); + foreach (IReadOnlyList group in groups) + { + Log("Same statement: " + group[0].Statement); + foreach (TheoremStatement t in group) + { + Log($" {t.Name} ({Path.GetRelativePath(root, t.Path)}:{t.Line + 1})"); + } + } + Log(groups.Count == 0 ? "Duplicates: no two theorems state the same thing." + : $"Duplicates: {groups.Count} statement{(groups.Count == 1 ? " is" : "s are")} made by more than one theorem. Keep one and deprecate or delete the rest."); + } + finally + { + ProStatus = ""; + } + } + // ---- linters ---- /// diff --git a/src/LeanStudio.App/Views/MainWindow.axaml b/src/LeanStudio.App/Views/MainWindow.axaml index fe12a50..930788f 100644 --- a/src/LeanStudio.App/Views/MainWindow.axaml +++ b/src/LeanStudio.App/Views/MainWindow.axaml @@ -138,6 +138,7 @@ + diff --git a/src/LeanStudio.App/Views/MainWindow.axaml.cs b/src/LeanStudio.App/Views/MainWindow.axaml.cs index 248de52..4d7b14b 100644 --- a/src/LeanStudio.App/Views/MainWindow.axaml.cs +++ b/src/LeanStudio.App/Views/MainWindow.axaml.cs @@ -1080,6 +1080,7 @@ private void OnLocationDoubleTapped(object? sender, TappedEventArgs e) yield return ("Lean: Lean's Processes (memory, stop a runaway file)…", "", LeanProcessesAsync); yield return ("Lean: Remove Unused Imports", "", Cmd(_vm.RemoveUnusedImportsCommand)); yield return ("Lean: Sort Imports", "", Cmd(_vm.SortImportsCommand)); + yield return ("Lean: Find Duplicate Theorem Statements", "", Cmd(_vm.FindDuplicateStatementsCommand)); yield return ("Lean: Merge Consecutive rw / intro Steps", "", Cmd(_vm.MergeConsecutiveTacticsCommand)); yield return ("Lean: Suggest a Name for This Theorem", "", Cmd(_vm.SuggestTheoremNameCommand)); yield return ("Lean: Tidy Whitespace and Check Style", "", Cmd(_vm.TidyWhitespaceCommand)); diff --git a/src/LeanStudio.Core/Workflow/DuplicateStatements.cs b/src/LeanStudio.Core/Workflow/DuplicateStatements.cs new file mode 100644 index 0000000..5b59c8b --- /dev/null +++ b/src/LeanStudio.Core/Workflow/DuplicateStatements.cs @@ -0,0 +1,110 @@ +using System.Text; +using System.Text.RegularExpressions; +using LeanStudio.Core.Editing; + +namespace LeanStudio.Core.Workflow; + +/// One theorem's statement, as found in a file. +/// The file. +/// 0-based line of the declaration. +/// The theorem's name, as written. +/// Its statement as written (binders and type, up to :=), on one line. +public sealed record TheoremStatement(string Path, int Line, string Name, string Statement); + +/// +/// Theorems that say the same thing under different names, found by comparing their statements with the names of the +/// variables they bind and the white space left out ((a b : ℕ) : a + b = b + a is (x y : ℕ) : x + y = y + x). +/// Mathlib asks that a result is stated once; a project that grew from several people's work often states it twice. +/// Statements are compared as text, so two that are equal only by unfolding are not found. +/// +public static class DuplicateStatements +{ + private static readonly Regex Declaration = new(@"^(?:@\[[^\]]*\]\s*)*(?:(?:protected|private|nonrec)\s+)*(?:theorem|lemma)\s+(?[^\s:({\[]+)(?.*)$", RegexOptions.Compiled); + + /// The theorems and lemmas in that start at the margin and whose statement ends with := within a few lines. + public static IReadOnlyList Statements(string path, string text) + { + string[] lines = text.Replace("\r\n", "\n", StringComparison.Ordinal).Split('\n'); + bool[] code = LeanText.CodeMask(string.Join('\n', lines)); + var found = new List(); + int offset = 0; + for (int i = 0; i < lines.Length; offset += lines[i].Length + 1, i++) + { + if (offset < code.Length && !code[offset]) + { + continue; // inside a comment or a string + } + Match m = Declaration.Match(lines[i]); + if (!m.Success) + { + continue; + } + var statement = new StringBuilder(m.Groups["rest"].Value); + for (int k = i + 1; k < lines.Length && k <= i + 12 && !statement.ToString().Contains(":=", StringComparison.Ordinal); k++) + { + statement.Append(' ').Append(lines[k].Trim()); + } + string s = statement.ToString(); + int end = s.IndexOf(":=", StringComparison.Ordinal); + if (end >= 0) + { + found.Add(new TheoremStatement(path, i, m.Groups["name"].Value, Regex.Replace(s[..end], @"\s+", " ").Trim())); + } + } + return found; + } + + /// + /// with the variables it binds named _0, _1… in the order they are bound and + /// its white space made single spaces, so statements that differ only in those compare equal. + /// + public static string Normalize(string statement) + { + string s = Regex.Replace(statement, @"\s+", " ").Trim().Replace("->", "→", StringComparison.Ordinal); + var names = new List(); + foreach (Match binder in Regex.Matches(s, @"[({](?[^:(){}\[\]]+?)\s:\s")) // (a b : T) and {a b : T} + { + names.AddRange(binder.Groups["n"].Value.Split(' ', StringSplitOptions.RemoveEmptyEntries)); + } + foreach (Match q in Regex.Matches(s, @"[∀∃λ]\s*(?[^,:]+?)\s*[,:]")) // ∀ a b, … + { + names.AddRange(q.Groups["n"].Value.Split(' ', StringSplitOptions.RemoveEmptyEntries)); + } + int next = 0; + foreach (string name in names.Where(n => Regex.IsMatch(n, @"^[\p{L}_][\p{L}\p{N}_'₀-₉]*$")).Distinct(StringComparer.Ordinal)) + { + s = Regex.Replace(s, $@"(? + /// The groups of two or more theorems with the same statement, across ; groups and + /// their members in the order found. Statements too short to say much (True, a = a) are left out. + /// + public static IReadOnlyList> Find(IEnumerable statements) => + [.. statements.Select(s => (Statement: s, Key: Normalize(s.Statement))) + .Where(x => x.Key.Length >= 12) + .GroupBy(x => x.Key, StringComparer.Ordinal) + .Where(g => g.Count() > 1) + .Select(g => (IReadOnlyList)[.. g.Select(x => x.Statement)])]; + + /// The duplicate statements among the Lean files under . + public static IReadOnlyList> Scan(string root, CancellationToken ct = default) + { + var all = new List(); + foreach (string file in ProjectSearch.Files(root, leanOnly: true)) + { + ct.ThrowIfCancellationRequested(); + try + { + all.AddRange(Statements(file, File.ReadAllText(file))); + } + catch (Exception e) when (e is IOException or UnauthorizedAccessException) + { + // a file that can't be read has no statements to compare + } + } + return Find(all); + } +} diff --git a/src/LeanStudio.Mcp/LeanTools.cs b/src/LeanStudio.Mcp/LeanTools.cs index 7d6418b..9026e52 100644 --- a/src/LeanStudio.Mcp/LeanTools.cs +++ b/src/LeanStudio.Mcp/LeanTools.cs @@ -808,6 +808,29 @@ public static IReadOnlyList Tools(Workbench bench) => return $"{count} line(s) can be merged into the one before (pass apply=true to write them)"; }), + new("duplicate_statements", + "Theorems of the project that state the same thing under different names: the statements are compared with the names of the variables they bind and the white space left out, so (a b : ℕ) : a + b = b + a matches (x y : ℕ) : x + y = y + x. Mathlib asks that a result is stated once. Statements are compared as text, so two that are equal only by unfolding are not found.", + Schema(("project", "string", "Any path in the project; defaults to the server's project.", false)), + (a, ct) => + { + LeanProject p = bench.ProjectFor(OptStr(a, "project")); + IReadOnlyList> groups = DuplicateStatements.Scan(p.Root, ct); + if (groups.Count == 0) + { + return Task.FromResult("no two theorems state the same thing"); + } + var sb = new StringBuilder(); + foreach (IReadOnlyList group in groups) + { + sb.Append("same statement: ").Append(group[0].Statement).Append('\n'); + foreach (TheoremStatement t in group) + { + sb.Append(CultureInfo.InvariantCulture, $" {t.Name} {Path.GetRelativePath(p.Root, t.Path)}:{t.Line + 1}\n"); + } + } + return Task.FromResult(sb.ToString().TrimEnd()); + }), + new("lint", "Run the linters CI runs on a Lean file of a Lake project: Mathlib's standard set in a project that uses Mathlib (its style linters among them), every linter Lean has elsewhere, and Batteries' environment linters (missing docstrings, simp normal form, unused arguments…) where Batteries is available. Lints the file as saved on disk.", Schema(("path", "string", "The .lean file.", true)), diff --git a/tests/LeanStudio.Tests/PickerAndConflictTests.cs b/tests/LeanStudio.Tests/PickerAndConflictTests.cs index 4e57048..e08bc26 100644 --- a/tests/LeanStudio.Tests/PickerAndConflictTests.cs +++ b/tests/LeanStudio.Tests/PickerAndConflictTests.cs @@ -174,6 +174,13 @@ async Task Call(string tool, System.Text.Json.Nodes.JsonObject args) Assert.Equal("add_comm", await Call("suggest_name", new() { ["statement"] = "(a b : ℕ) : a + b = b + a" })); Assert.StartsWith("no name", await Call("suggest_name", new() { ["statement"] = "True" }), StringComparison.Ordinal); + Assert.Equal("no two theorems state the same thing", await Call("duplicate_statements", new())); + await File.WriteAllTextAsync(Path.Combine(dir, "Q.lean"), "theorem q1 (a b : ℕ) : a + b = b + a := by omega\ntheorem q2 (x y : ℕ) : x + y = y + x := by omega\n", TestContext.Current.CancellationToken); + string dupes = await Call("duplicate_statements", new()); + Assert.Contains("q1 Q.lean:1", dupes, StringComparison.Ordinal); + Assert.Contains("q2 Q.lean:2", dupes, StringComparison.Ordinal); + File.Delete(Path.Combine(dir, "Q.lean")); + string proof = Path.Combine(dir, "P.lean"); await File.WriteAllTextAsync(proof, "theorem t : P := by\n rw [a]\n rw [b]\n exact h\n", TestContext.Current.CancellationToken); Assert.StartsWith("1 line(s) can be merged", await Call("merge_tactics", new() { ["path"] = proof }), StringComparison.Ordinal); @@ -475,3 +482,53 @@ public void KeepsCrlfLineEndings() Assert.Equal((" intro x y\r\n exact h\r\n", 1), TacticGolf.Merge(" intro x\r\n intro y\r\n exact h\r\n")); } } + +/// Theorems that state the same thing. +public sealed class DuplicateStatementsTests +{ + [Fact] + public void ReadsTheStatementsOfTheoremsAtTheMargin() + { + const string text = "theorem a (x y : ℕ) :\n x + y = y + x := by\n omega\n\n/- theorem hidden : 1 = 1 := rfl -/\n theorem indented : 1 = 1 := rfl\n@[simp] protected lemma b {n : ℕ} : n = n := rfl\n"; + IReadOnlyList found = DuplicateStatements.Statements("F.lean", text); + Assert.Equal([("a", 0, "(x y : ℕ) : x + y = y + x"), ("b", 6, "{n : ℕ} : n = n")], found.Select(s => (s.Name, s.Line, s.Statement))); + } + + [Fact] + public void IgnoresTheNamesOfBoundVariablesAndSpacing() + { + Assert.Equal(DuplicateStatements.Normalize("(a b : ℕ) : a + b = b + a"), DuplicateStatements.Normalize("(x y : ℕ) : x + y = y + x")); + Assert.Equal(DuplicateStatements.Normalize("∀ a b, a ≤ b → a < b + 1"), DuplicateStatements.Normalize("∀ m n, m ≤ n -> m < n + 1")); + Assert.NotEqual(DuplicateStatements.Normalize("(a b : ℕ) : a + b = b + a"), DuplicateStatements.Normalize("(a b : ℕ) : a * b = b * a")); + Assert.NotEqual(DuplicateStatements.Normalize("(a b : ℕ) : a + b = b + a"), DuplicateStatements.Normalize("(a b : ℤ) : a + b = b + a")); + Assert.Equal("(_0 : ℕ) : _0 + n' = f _0", DuplicateStatements.Normalize("(x : ℕ) : x + n' = f x")); // free names stay + } + + [Fact] + public void GroupsTheoremsWithTheSameStatementAcrossFiles() + { + var all = new List(); + all.AddRange(DuplicateStatements.Statements("A.lean", "theorem add_comm' (a b : ℕ) : a + b = b + a := by omega\ntheorem short : True := trivial\n")); + all.AddRange(DuplicateStatements.Statements("B.lean", "lemma plus_comm (x y : ℕ) :\n x + y = y + x := Nat.add_comm x y\ntheorem short2 : True := trivial\ntheorem other (a b : ℕ) : a * b = b * a := by omega\n")); + IReadOnlyList> groups = DuplicateStatements.Find(all); + IReadOnlyList group = Assert.Single(groups); + Assert.Equal(["add_comm'", "plus_comm"], group.Select(s => s.Name)); + Assert.Equal(["A.lean", "B.lean"], group.Select(s => s.Path)); // `True` twice is too short to count + } + + [Fact] + public async Task ScansAProjectFolder() + { + string dir = Directory.CreateTempSubdirectory("leanstudio-dups-").FullName; + try + { + await File.WriteAllTextAsync(Path.Combine(dir, "A.lean"), "theorem one (n : ℕ) : n + 0 = n := rfl\n", TestContext.Current.CancellationToken); + await File.WriteAllTextAsync(Path.Combine(dir, "B.lean"), "theorem two (k : ℕ) : k + 0 = k := by simp\n", TestContext.Current.CancellationToken); + Assert.Equal(["one", "two"], Assert.Single(DuplicateStatements.Scan(dir, TestContext.Current.CancellationToken)).Select(s => s.Name).Order()); + } + finally + { + Directory.Delete(dir, true); + } + } +} From 4fc86f2c167677b5daf2068416ca10eb66b08c17 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 3 Oct 2026 19:43:55 +0000 Subject: [PATCH 11/18] Version 0.11.0 Co-Authored-By: Claude Sonnet 5.5 Claude-Session: https://claude.ai/code/session_01FF5AYRpU9TWeWY3CFh2ETw --- CHANGELOG.md | 2 +- Directory.Build.props | 2 +- README.md | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 10e9a0d..b48befb 100644 --- a/CHANGELOG.md +++ b/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). diff --git a/Directory.Build.props b/Directory.Build.props index cad94aa..671180f 100644 --- a/Directory.Build.props +++ b/Directory.Build.props @@ -11,7 +11,7 @@ Lean Studio Copyright (c) 2026 Keith Adler (@keithadler) MIT - 0.10.0 + 0.11.0 12.1.3 diff --git a/README.md b/README.md index f0b681b..7410ed1 100644 --- a/README.md +++ b/README.md @@ -661,7 +661,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. From 8cbea553ed836e54bd48721964a1f060c749eff5 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 3 Oct 2026 20:29:18 +0000 Subject: [PATCH 12/18] Add Project Health Summary Co-Authored-By: Claude Sonnet 5.5 Claude-Session: https://claude.ai/code/session_01FF5AYRpU9TWeWY3CFh2ETw --- CHANGELOG.md | 1 + README.md | 1 + docs/ARCHITECTURE.md | 4 +- .../ViewModels/MainViewModel.Pro.cs | 28 +++++ src/LeanStudio.App/Views/MainWindow.axaml | 1 + src/LeanStudio.App/Views/MainWindow.axaml.cs | 1 + src/LeanStudio.Core/Workflow/ProjectHealth.cs | 115 ++++++++++++++++++ src/LeanStudio.Mcp/LeanTools.cs | 9 ++ .../PickerAndConflictTests.cs | 52 ++++++++ 9 files changed, 210 insertions(+), 2 deletions(-) create mode 100644 src/LeanStudio.Core/Workflow/ProjectHealth.cs diff --git a/CHANGELOG.md b/CHANGELOG.md index b48befb..b88a8f7 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -27,6 +27,7 @@ - **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. - **Over MCP**, `sort_imports` and `style_check` do the same for assistants, each with `apply` to write the file. **Fixes**: diff --git a/README.md b/README.md index 7410ed1..d3bbe92 100644 --- a/README.md +++ b/README.md @@ -331,6 +331,7 @@ What CI and reviewers check, before you push: - **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. +- **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. diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index cd8932a..e1d62e9 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -129,7 +129,7 @@ shows them to a person or an assistant. | [`Proofs/`](../src/LeanStudio.Core/Proofs) | `TacticGolf` (consecutive rw and intro lines merged). Features that ask Lean about proofs: `ProofSteps` (the tactic block around a line, read by layout), `ProofSearch` (Prove It and counterexamples) and `Scratch` (scratch documents in the running server), `ExtractLemma`, `Profiler` (Lean's profilers read into a `ProfileReport`: trees, categories, counters, per-line costs; its records are in `ProfileModel`), `LiveProfiler` (the same, from the running server as the file is edited), `ProfileCheck` (saved profiles in `ProfileStore`, and the heartbeat regression check), `Heartbeats`, `ProofStates` (the Proof-State Map), `Walkthrough` (the HTML export) and `LeanRepl`. | | [`Ai/`](../src/LeanStudio.Core/Ai) | The AI in the editor: `IChatModel` and the clients behind it (`AppleIntelligence` and `AppleFmCliModel` for the `fm` command, `OllamaModel`, `OpenAiCompatibleModel`, `AnthropicModel`), `AiDiscovery` (what is running, and which model to use), `AiProver` (proofs from a model, checked by Lean), `AiAssistant` (explanations and chat), `AiText` (token estimates and trimming) and `SecretStore` (API keys). | | [`Editing/`](../src/LeanStudio.Core/Editing) | Text-level engines with no UI: `Abbreviations` (Unicode input), `LeanText` (comments, strings and declarations in Lean source), `LatexText` (docstring math as text), `Fuzzy` (picker matching), `ProjectSearch` (find and replace across files), `MultiCursor`, `VimEngine`, `EmacsEngine` and `KeyBindingsFile` (keybindings.json). The editor in the app is a thin host over them. | -| [`Workflow/`](../src/LeanStudio.Core/Workflow) | Project-wide tools. `Workflow.cs` holds `Markers` (sorries and TODOs), `LakeOutput` (build problems), `LocalHistory`, `Loogle`, `LeanSearch`, `DocLinks`, `Blame` and `ProjectTasks`. Beside it: `Refactor` and `EmittedC` (module rename, replace across files, Compiled C), `Ffi` (`@[extern]` bindings checked against the project's C files, and C stubs), `ImportCheck` (unused imports), `ImportOrder` (sorted imports), `StyleCheck` (Mathlib's text rules), `MathlibConventions` (header, module docstring, theorem names), `DocCoverage` (definitions with no doc comment), `StaleDeprecations` (old deprecated aliases, found and deleted), `ZulipPost` (a question for the Lean Zulip chat), `TheoremNamer` (a Mathlib-style name from a statement), `DuplicateStatements` (theorems that state the same thing), `Lint`, `Instances`, `Deprecation` (deprecated aliases for renames), `DependencyBump` (Update Mathlib and see what broke), `Blueprint`, `ProjectCommands` (`.leanstudio/commands.json`), `ProgressReader` (progress read from what a task prints), `LeanCli` (the `lean` command line on a mirror copy) and `Essentials.cs` (`ElanInstaller`, `FileOps`, `ImportFinder`). | +| [`Workflow/`](../src/LeanStudio.Core/Workflow) | Project-wide tools. `Workflow.cs` holds `Markers` (sorries and TODOs), `LakeOutput` (build problems), `LocalHistory`, `Loogle`, `LeanSearch`, `DocLinks`, `Blame` and `ProjectTasks`. Beside it: `Refactor` and `EmittedC` (module rename, replace across files, Compiled C), `Ffi` (`@[extern]` bindings checked against the project's C files, and C stubs), `ImportCheck` (unused imports), `ImportOrder` (sorted imports), `StyleCheck` (Mathlib's text rules), `MathlibConventions` (header, module docstring, theorem names), `DocCoverage` (definitions with no doc comment), `StaleDeprecations` (old deprecated aliases, found and deleted), `ZulipPost` (a question for the Lean Zulip chat), `TheoremNamer` (a Mathlib-style name from a statement), `DuplicateStatements` (theorems that state the same thing), `ProjectHealth` (a project counted into a report), `Lint`, `Instances`, `Deprecation` (deprecated aliases for renames), `DependencyBump` (Update Mathlib and see what broke), `Blueprint`, `ProjectCommands` (`.leanstudio/commands.json`), `ProgressReader` (progress read from what a task prints), `LeanCli` (the `lean` command line on a mirror copy) and `Essentials.cs` (`ElanInstaller`, `FileOps`, `ImportFinder`). | | [`Git/`](../src/LeanStudio.Core/Git) | `GitRepository` wraps your own `git` executable, so your config, hooks, credentials and signing all apply. `GitHub` goes through the `gh` CLI, so Lean Studio never handles a token. | | [`Learn/`](../src/LeanStudio.Core/Learn) | `Tutorial` and `Playground`; `TacticGuide`, `ErrorGuide` and `PlainEnglish` (goals read aloud) in `Guides.cs`; `Snippets`, `TheoremGallery` and `ProgramRunner` in `Library.cs`. | | [`Agents/`](../src/LeanStudio.Core/Agents) | For assistants and web pages: `Workbench` and `ProjectSession` (Lean for a program instead of a person, used by the MCP server), `StudioBridge` (the pipe between an assistant and an open window), `InfoviewBridge` (Lean's own infoview page, served to a web view or browser) and `AgentSetup` (writing each assistant's MCP configuration). | @@ -174,7 +174,7 @@ written to stdout. | Checking and reading a file | `project_info`, `check_file`, `goals`, `proof_steps`, `hover`, `suggestions`, `references`, `run_lean` | | Building and Tenet | `build`, `verify`, `axioms`, `why_not_proved`, `project_map` | | Proof tools | `prove`, `extract_lemma`, `ffi_bindings`, `profile` | -| For Mathlib contributors | `unused_imports`, `sort_imports`, `style_check`, `stale_deprecations`, `suggest_name`, `duplicate_statements`, `lint`, `heartbeats`, `instances`, `blueprint` | +| For Mathlib contributors | `unused_imports`, `sort_imports`, `style_check`, `stale_deprecations`, `suggest_name`, `duplicate_statements`, `project_health`, `lint`, `heartbeats`, `instances`, `blueprint` | | Walkthroughs and search | `export_walkthrough`, `search_mathlib`, and `declaration` and `search_declarations` (the compiled library, through Tenet) | | Toolchains | `toolchains` | | The open window | `studio_context`, `studio_show` | diff --git a/src/LeanStudio.App/ViewModels/MainViewModel.Pro.cs b/src/LeanStudio.App/ViewModels/MainViewModel.Pro.cs index 9dcc082..3b1878c 100644 --- a/src/LeanStudio.App/ViewModels/MainViewModel.Pro.cs +++ b/src/LeanStudio.App/ViewModels/MainViewModel.Pro.cs @@ -671,6 +671,34 @@ public async Task FindDuplicateStatementsAsync() } } + /// + /// Count the project's Lean files into a summary in Output: size, sorrys and TODOs, the share of definitions with a doc + /// comment, deprecations (and how many are old enough to delete) and style problems, then the files with the most still to do. + /// + [RelayCommand] + public async Task ShowProjectHealthAsync() + { + if (Project is null) + { + Log("Health: open a project first."); + return; + } + string root = Project.Root; + ProStatus = "Counting the project's files…"; + try + { + ProjectHealth health = await Task.Run(() => ProjectHealthReport.Scan(root, DateOnly.FromDateTime(DateTime.Today))); + foreach (string line in ProjectHealthReport.ToMarkdown(health, root).Split('\n')) + { + Log(line); + } + } + finally + { + ProStatus = ""; + } + } + // ---- linters ---- /// diff --git a/src/LeanStudio.App/Views/MainWindow.axaml b/src/LeanStudio.App/Views/MainWindow.axaml index 930788f..27cb8de 100644 --- a/src/LeanStudio.App/Views/MainWindow.axaml +++ b/src/LeanStudio.App/Views/MainWindow.axaml @@ -138,6 +138,7 @@ + diff --git a/src/LeanStudio.App/Views/MainWindow.axaml.cs b/src/LeanStudio.App/Views/MainWindow.axaml.cs index 4d7b14b..be1da3a 100644 --- a/src/LeanStudio.App/Views/MainWindow.axaml.cs +++ b/src/LeanStudio.App/Views/MainWindow.axaml.cs @@ -1080,6 +1080,7 @@ private void OnLocationDoubleTapped(object? sender, TappedEventArgs e) yield return ("Lean: Lean's Processes (memory, stop a runaway file)…", "", LeanProcessesAsync); yield return ("Lean: Remove Unused Imports", "", Cmd(_vm.RemoveUnusedImportsCommand)); yield return ("Lean: Sort Imports", "", Cmd(_vm.SortImportsCommand)); + yield return ("Lean: Project Health Summary", "", Cmd(_vm.ShowProjectHealthCommand)); yield return ("Lean: Find Duplicate Theorem Statements", "", Cmd(_vm.FindDuplicateStatementsCommand)); yield return ("Lean: Merge Consecutive rw / intro Steps", "", Cmd(_vm.MergeConsecutiveTacticsCommand)); yield return ("Lean: Suggest a Name for This Theorem", "", Cmd(_vm.SuggestTheoremNameCommand)); diff --git a/src/LeanStudio.Core/Workflow/ProjectHealth.cs b/src/LeanStudio.Core/Workflow/ProjectHealth.cs new file mode 100644 index 0000000..e2fe2bd --- /dev/null +++ b/src/LeanStudio.Core/Workflow/ProjectHealth.cs @@ -0,0 +1,115 @@ +using System.Globalization; +using System.Text; +using System.Text.RegularExpressions; +using LeanStudio.Core.Editing; + +namespace LeanStudio.Core.Workflow; + +/// What one Lean file holds, counted from its text. +/// The file. +/// Lines that are not blank. +/// Theorems and lemmas at the margin. +/// Definitions, abbreviations, structures, classes and inductive types at the margin. +/// sorry and admit outside comments. +/// TODO, FIXME and XXX in comments. +/// Public definitions without a doc comment (). +/// Declarations marked deprecated with a date. +/// Of those, the ones old enough to delete (). +/// Problems of the text rules (). +public sealed record FileHealth(string Path, int Lines, int Theorems, int Definitions, int Sorries, int Todos, int Undocumented, int Deprecated, int StaleDeprecated, int StyleProblems); + +/// A project's state at a glance: its size, what is unfinished, and how well it keeps to Mathlib's conventions. +/// Each Lean file's counts, in path order. +public sealed record ProjectHealth(IReadOnlyList Files) +{ + /// The sum of a count over every file. + public int Total(Func count) => Files.Sum(count); + + /// The share of public definitions with a doc comment, 0 to 100; 100 for a project with none. + public int DocCoveragePercent + { + get + { + int defs = Total(f => f.Definitions); + return defs == 0 ? 100 : (int)Math.Round(100.0 * (defs - Math.Min(defs, Total(f => f.Undocumented))) / defs); + } + } +} + +/// Counting a project's Lean files into a , and reading the result. +public static class ProjectHealthReport +{ + private static readonly Regex Theorem = new(@"^(?:@\[[^\]]*\]\s*)*(?:(?:protected|private|nonrec)\s+)*(?:theorem|lemma)\s", RegexOptions.Compiled); + private static readonly Regex Definition = new(@"^(?:@\[[^\]]*\]\s*)*(?:(?:protected|private|public|noncomputable|partial|unsafe|nonrec)\s+)*(?:def|abbrev|structure|class|inductive|opaque)\s", RegexOptions.Compiled); + + /// What holds, as of (for the age of deprecations). + public static FileHealth Count(string path, string text, DateOnly today) + { + string[] lines = text.Replace("\r\n", "\n", StringComparison.Ordinal).Split('\n'); + bool[] code = LeanText.CodeMask(string.Join('\n', lines)); + int theorems = 0, definitions = 0, offset = 0; + for (int i = 0; i < lines.Length; offset += lines[i].Length + 1, i++) + { + if (lines[i].Length == 0 || char.IsWhiteSpace(lines[i][0]) || (offset < code.Length && !code[offset])) + { + continue; + } + theorems += Theorem.IsMatch(lines[i]) ? 1 : 0; + definitions += Definition.IsMatch(lines[i]) ? 1 : 0; + } + List markers = [.. Markers.ScanText(path, lines)]; + return new FileHealth(path, lines.Count(l => l.Trim().Length > 0), theorems, definitions, + markers.Count(m => m.Kind != MarkerKind.Todo), markers.Count(m => m.Kind == MarkerKind.Todo), + DocCoverage.Find(text).Count, StaleDeprecations.Find(text, today, 0).Count, StaleDeprecations.Find(text, today).Count, + StyleCheck.Find(text).Count); + } + + /// The health of every Lean file under . + public static ProjectHealth Scan(string root, DateOnly today, CancellationToken ct = default) + { + var files = new List(); + foreach (string file in ProjectSearch.Files(root, leanOnly: true).Order(StringComparer.Ordinal)) + { + ct.ThrowIfCancellationRequested(); + try + { + files.Add(Count(file, File.ReadAllText(file), today)); + } + catch (Exception e) when (e is IOException or UnauthorizedAccessException) + { + // a file that can't be read has nothing to count + } + } + return new ProjectHealth(files); + } + + /// A Markdown summary of : totals, then the files with the most still to do. + public static string ToMarkdown(ProjectHealth health, string root) + { + static string N(int n) => n.ToString("N0", CultureInfo.InvariantCulture); + var sb = new StringBuilder(); + sb.Append("## Project health\n\n"); + if (health.Files.Count == 0) + { + return sb.Append("No Lean files found.\n").ToString(); + } + sb.Append(CultureInfo.InvariantCulture, $"{N(health.Files.Count)} files, {N(health.Total(f => f.Lines))} lines, {N(health.Total(f => f.Theorems))} theorems, {N(health.Total(f => f.Definitions))} definitions.\n\n"); + sb.Append("| | |\n|---|---:|\n"); + sb.Append(CultureInfo.InvariantCulture, $"| `sorry` / `admit` | {N(health.Total(f => f.Sorries))} |\n"); + sb.Append(CultureInfo.InvariantCulture, $"| TODO / FIXME | {N(health.Total(f => f.Todos))} |\n"); + sb.Append(CultureInfo.InvariantCulture, $"| Definitions with a doc comment | {health.DocCoveragePercent}% ({N(health.Total(f => f.Undocumented))} without) |\n"); + sb.Append(CultureInfo.InvariantCulture, $"| Deprecated declarations | {N(health.Total(f => f.Deprecated))} ({N(health.Total(f => f.StaleDeprecated))} old enough to delete) |\n"); + sb.Append(CultureInfo.InvariantCulture, $"| Style problems (whitespace, long lines, final newline) | {N(health.Total(f => f.StyleProblems))} |\n"); + var worst = health.Files.Select(f => (File: f, Open: f.Sorries + f.Undocumented + f.StaleDeprecated + f.StyleProblems)) + .Where(x => x.Open > 0).OrderByDescending(x => x.Open).ThenBy(x => x.File.Path, StringComparer.Ordinal).Take(5).ToList(); + if (worst.Count > 0) + { + sb.Append("\nMost still to do (sorries, undocumented definitions, old deprecations and style problems together):\n\n"); + foreach ((FileHealth f, int open) in worst) + { + sb.Append(CultureInfo.InvariantCulture, $"- `{System.IO.Path.GetRelativePath(root, f.Path)}`: {open} ({f.Sorries} sorry, {f.Undocumented} undocumented, {f.StaleDeprecated} old deprecations, {f.StyleProblems} style)\n"); + } + } + return sb.ToString(); + } +} diff --git a/src/LeanStudio.Mcp/LeanTools.cs b/src/LeanStudio.Mcp/LeanTools.cs index 9026e52..27df427 100644 --- a/src/LeanStudio.Mcp/LeanTools.cs +++ b/src/LeanStudio.Mcp/LeanTools.cs @@ -831,6 +831,15 @@ public static IReadOnlyList Tools(Workbench bench) => return Task.FromResult(sb.ToString().TrimEnd()); }), + new("project_health", + "A 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 files with the most still to do. Markdown.", + Schema(("project", "string", "Any path in the project; defaults to the server's project.", false)), + (a, ct) => + { + LeanProject p = bench.ProjectFor(OptStr(a, "project")); + return Task.FromResult(ProjectHealthReport.ToMarkdown(ProjectHealthReport.Scan(p.Root, DateOnly.FromDateTime(DateTime.Today), ct), p.Root).TrimEnd()); + }), + new("lint", "Run the linters CI runs on a Lean file of a Lake project: Mathlib's standard set in a project that uses Mathlib (its style linters among them), every linter Lean has elsewhere, and Batteries' environment linters (missing docstrings, simp normal form, unused arguments…) where Batteries is available. Lints the file as saved on disk.", Schema(("path", "string", "The .lean file.", true)), diff --git a/tests/LeanStudio.Tests/PickerAndConflictTests.cs b/tests/LeanStudio.Tests/PickerAndConflictTests.cs index e08bc26..2b25fc5 100644 --- a/tests/LeanStudio.Tests/PickerAndConflictTests.cs +++ b/tests/LeanStudio.Tests/PickerAndConflictTests.cs @@ -174,6 +174,7 @@ async Task Call(string tool, System.Text.Json.Nodes.JsonObject args) Assert.Equal("add_comm", await Call("suggest_name", new() { ["statement"] = "(a b : ℕ) : a + b = b + a" })); Assert.StartsWith("no name", await Call("suggest_name", new() { ["statement"] = "True" }), StringComparison.Ordinal); + Assert.Contains("1 files, 3 lines, 0 theorems, 1 definitions.", await Call("project_health", new()), StringComparison.Ordinal); Assert.Equal("no two theorems state the same thing", await Call("duplicate_statements", new())); await File.WriteAllTextAsync(Path.Combine(dir, "Q.lean"), "theorem q1 (a b : ℕ) : a + b = b + a := by omega\ntheorem q2 (x y : ℕ) : x + y = y + x := by omega\n", TestContext.Current.CancellationToken); string dupes = await Call("duplicate_statements", new()); @@ -532,3 +533,54 @@ public async Task ScansAProjectFolder() } } } + +/// A project's state at a glance. +public sealed class ProjectHealthTests +{ + private static readonly DateOnly Today = new(2026, 10, 3); + + private const string Text = + "/-- Documented. -/\ndef a := 1\n\ndef b := sorry\n\ntheorem t : a = 1 := by\n sorry\n\n-- TODO: more\n" + + "@[deprecated (since := \"2024-01-01\")] alias old := a\n@[deprecated (since := \"2026-09-01\")] alias recent := a\nlemma l : True := trivial \n"; + + [Fact] + public void CountsWhatAFileHolds() + { + FileHealth h = ProjectHealthReport.Count("F.lean", Text, Today); + Assert.Equal((2, 2, 2, 1), (h.Definitions, h.Theorems, h.Sorries, h.Todos)); + Assert.Equal((1, 2, 1), (h.Undocumented, h.Deprecated, h.StaleDeprecated)); // b has no doc comment; only `old` is past six months + Assert.Equal(1, h.StyleProblems); // the trailing spaces after `lemma l` + } + + [Fact] + public void ReadsADocCoveragePercentage() + { + var health = new ProjectHealth([new FileHealth("A", 10, 0, 4, 0, 0, 1, 0, 0, 0), new FileHealth("B", 10, 0, 4, 0, 0, 0, 0, 0, 0)]); + Assert.Equal(88, health.DocCoveragePercent); // 7 of 8, rounded + Assert.Equal(100, new ProjectHealth([]).DocCoveragePercent); + } + + [Fact] + public async Task ScansAFolderAndSaysWhereMostIsLeft() + { + string dir = Directory.CreateTempSubdirectory("leanstudio-health-").FullName; + try + { + await File.WriteAllTextAsync(Path.Combine(dir, "Clean.lean"), "/-- A. -/\ndef a := 1\n", TestContext.Current.CancellationToken); + await File.WriteAllTextAsync(Path.Combine(dir, "Messy.lean"), "def b := sorry \ndef c := sorry\n", TestContext.Current.CancellationToken); + ProjectHealth health = ProjectHealthReport.Scan(dir, Today, TestContext.Current.CancellationToken); + Assert.Equal(2, health.Files.Count); + string report = ProjectHealthReport.ToMarkdown(health, dir); + Assert.Contains("2 files, 4 lines, 0 theorems, 3 definitions.", report, StringComparison.Ordinal); + Assert.Contains("| `sorry` / `admit` | 2 |", report, StringComparison.Ordinal); + Assert.Contains("| Definitions with a doc comment | 33% (2 without) |", report, StringComparison.Ordinal); + Assert.Contains("- `Messy.lean`: 5 (2 sorry, 2 undocumented, 0 old deprecations, 1 style)", report, StringComparison.Ordinal); + Assert.DoesNotContain("Clean.lean", report, StringComparison.Ordinal); + Assert.Contains("No Lean files found.", ProjectHealthReport.ToMarkdown(new ProjectHealth([]), dir), StringComparison.Ordinal); + } + finally + { + Directory.Delete(dir, true); + } + } +} From 6ff8daa7251ad0d8572631ffd3b5ad3a146c0588 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 3 Oct 2026 20:38:26 +0000 Subject: [PATCH 13/18] Add Sorry Burndown Co-Authored-By: Claude Sonnet 5.5 Claude-Session: https://claude.ai/code/session_01FF5AYRpU9TWeWY3CFh2ETw --- CHANGELOG.md | 1 + README.md | 1 + docs/ARCHITECTURE.md | 4 +- .../ViewModels/MainViewModel.Pro.cs | 27 +++++ src/LeanStudio.App/Views/MainWindow.axaml | 1 + src/LeanStudio.App/Views/MainWindow.axaml.cs | 1 + src/LeanStudio.Core/Git/SorryHistory.cs | 103 ++++++++++++++++++ src/LeanStudio.Mcp/LeanTools.cs | 14 +++ .../PickerAndConflictTests.cs | 70 ++++++++++++ 9 files changed, 220 insertions(+), 2 deletions(-) create mode 100644 src/LeanStudio.Core/Git/SorryHistory.cs diff --git a/CHANGELOG.md b/CHANGELOG.md index b88a8f7..8088821 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -28,6 +28,7 @@ - **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`. - **Over MCP**, `sort_imports` and `style_check` do the same for assistants, each with `apply` to write the file. **Fixes**: diff --git a/README.md b/README.md index d3bbe92..a536c3a 100644 --- a/README.md +++ b/README.md @@ -331,6 +331,7 @@ What CI and reviewers check, before you push: - **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. +- **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. diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index e1d62e9..21bb85d 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -130,7 +130,7 @@ shows them to a person or an assistant. | [`Ai/`](../src/LeanStudio.Core/Ai) | The AI in the editor: `IChatModel` and the clients behind it (`AppleIntelligence` and `AppleFmCliModel` for the `fm` command, `OllamaModel`, `OpenAiCompatibleModel`, `AnthropicModel`), `AiDiscovery` (what is running, and which model to use), `AiProver` (proofs from a model, checked by Lean), `AiAssistant` (explanations and chat), `AiText` (token estimates and trimming) and `SecretStore` (API keys). | | [`Editing/`](../src/LeanStudio.Core/Editing) | Text-level engines with no UI: `Abbreviations` (Unicode input), `LeanText` (comments, strings and declarations in Lean source), `LatexText` (docstring math as text), `Fuzzy` (picker matching), `ProjectSearch` (find and replace across files), `MultiCursor`, `VimEngine`, `EmacsEngine` and `KeyBindingsFile` (keybindings.json). The editor in the app is a thin host over them. | | [`Workflow/`](../src/LeanStudio.Core/Workflow) | Project-wide tools. `Workflow.cs` holds `Markers` (sorries and TODOs), `LakeOutput` (build problems), `LocalHistory`, `Loogle`, `LeanSearch`, `DocLinks`, `Blame` and `ProjectTasks`. Beside it: `Refactor` and `EmittedC` (module rename, replace across files, Compiled C), `Ffi` (`@[extern]` bindings checked against the project's C files, and C stubs), `ImportCheck` (unused imports), `ImportOrder` (sorted imports), `StyleCheck` (Mathlib's text rules), `MathlibConventions` (header, module docstring, theorem names), `DocCoverage` (definitions with no doc comment), `StaleDeprecations` (old deprecated aliases, found and deleted), `ZulipPost` (a question for the Lean Zulip chat), `TheoremNamer` (a Mathlib-style name from a statement), `DuplicateStatements` (theorems that state the same thing), `ProjectHealth` (a project counted into a report), `Lint`, `Instances`, `Deprecation` (deprecated aliases for renames), `DependencyBump` (Update Mathlib and see what broke), `Blueprint`, `ProjectCommands` (`.leanstudio/commands.json`), `ProgressReader` (progress read from what a task prints), `LeanCli` (the `lean` command line on a mirror copy) and `Essentials.cs` (`ElanInstaller`, `FileOps`, `ImportFinder`). | -| [`Git/`](../src/LeanStudio.Core/Git) | `GitRepository` wraps your own `git` executable, so your config, hooks, credentials and signing all apply. `GitHub` goes through the `gh` CLI, so Lean Studio never handles a token. | +| [`Git/`](../src/LeanStudio.Core/Git) | `SorryHistory` (sorries per commit, as a sparkline). `GitRepository` wraps your own `git` executable, so your config, hooks, credentials and signing all apply. `GitHub` goes through the `gh` CLI, so Lean Studio never handles a token. | | [`Learn/`](../src/LeanStudio.Core/Learn) | `Tutorial` and `Playground`; `TacticGuide`, `ErrorGuide` and `PlainEnglish` (goals read aloud) in `Guides.cs`; `Snippets`, `TheoremGallery` and `ProgramRunner` in `Library.cs`. | | [`Agents/`](../src/LeanStudio.Core/Agents) | For assistants and web pages: `Workbench` and `ProjectSession` (Lean for a program instead of a person, used by the MCP server), `StudioBridge` (the pipe between an assistant and an open window), `InfoviewBridge` (Lean's own infoview page, served to a web view or browser) and `AgentSetup` (writing each assistant's MCP configuration). | | [`Plugins/`](../src/LeanStudio.Core/Plugins) | `PluginLoader`: finds plugin assemblies and loads each in a load context of its own. | @@ -174,7 +174,7 @@ written to stdout. | Checking and reading a file | `project_info`, `check_file`, `goals`, `proof_steps`, `hover`, `suggestions`, `references`, `run_lean` | | Building and Tenet | `build`, `verify`, `axioms`, `why_not_proved`, `project_map` | | Proof tools | `prove`, `extract_lemma`, `ffi_bindings`, `profile` | -| For Mathlib contributors | `unused_imports`, `sort_imports`, `style_check`, `stale_deprecations`, `suggest_name`, `duplicate_statements`, `project_health`, `lint`, `heartbeats`, `instances`, `blueprint` | +| For Mathlib contributors | `unused_imports`, `sort_imports`, `style_check`, `stale_deprecations`, `suggest_name`, `duplicate_statements`, `project_health`, `sorry_history`, `lint`, `heartbeats`, `instances`, `blueprint` | | Walkthroughs and search | `export_walkthrough`, `search_mathlib`, and `declaration` and `search_declarations` (the compiled library, through Tenet) | | Toolchains | `toolchains` | | The open window | `studio_context`, `studio_show` | diff --git a/src/LeanStudio.App/ViewModels/MainViewModel.Pro.cs b/src/LeanStudio.App/ViewModels/MainViewModel.Pro.cs index 3b1878c..9f69d46 100644 --- a/src/LeanStudio.App/ViewModels/MainViewModel.Pro.cs +++ b/src/LeanStudio.App/ViewModels/MainViewModel.Pro.cs @@ -699,6 +699,33 @@ public async Task ShowProjectHealthAsync() } } + /// + /// Show how many sorrys the project had at each of its last 30 commits, as a sparkline with the commits that + /// changed the count. Read with git grep, so nothing is checked out or built. + /// + [RelayCommand] + public async Task ShowSorryBurndownAsync() + { + if (Project is null || Core.Git.GitRepository.Find(Project.Root) is not Core.Git.GitRepository repo) + { + Log("Burndown: open a project that is in a Git repository."); + return; + } + ProStatus = "Counting sorries through the history…"; + try + { + IReadOnlyList points = await Core.Git.SorryHistory.ReadAsync(repo, 30); + foreach (string line in Core.Git.SorryHistory.ToText(points).Split('\n')) + { + Log(line); + } + } + finally + { + ProStatus = ""; + } + } + // ---- linters ---- /// diff --git a/src/LeanStudio.App/Views/MainWindow.axaml b/src/LeanStudio.App/Views/MainWindow.axaml index 27cb8de..5ba4f0c 100644 --- a/src/LeanStudio.App/Views/MainWindow.axaml +++ b/src/LeanStudio.App/Views/MainWindow.axaml @@ -138,6 +138,7 @@ + diff --git a/src/LeanStudio.App/Views/MainWindow.axaml.cs b/src/LeanStudio.App/Views/MainWindow.axaml.cs index be1da3a..7ab78b2 100644 --- a/src/LeanStudio.App/Views/MainWindow.axaml.cs +++ b/src/LeanStudio.App/Views/MainWindow.axaml.cs @@ -1081,6 +1081,7 @@ private void OnLocationDoubleTapped(object? sender, TappedEventArgs e) yield return ("Lean: Remove Unused Imports", "", Cmd(_vm.RemoveUnusedImportsCommand)); yield return ("Lean: Sort Imports", "", Cmd(_vm.SortImportsCommand)); yield return ("Lean: Project Health Summary", "", Cmd(_vm.ShowProjectHealthCommand)); + yield return ("Lean: Sorry Burndown (last 30 commits)", "", Cmd(_vm.ShowSorryBurndownCommand)); yield return ("Lean: Find Duplicate Theorem Statements", "", Cmd(_vm.FindDuplicateStatementsCommand)); yield return ("Lean: Merge Consecutive rw / intro Steps", "", Cmd(_vm.MergeConsecutiveTacticsCommand)); yield return ("Lean: Suggest a Name for This Theorem", "", Cmd(_vm.SuggestTheoremNameCommand)); diff --git a/src/LeanStudio.Core/Git/SorryHistory.cs b/src/LeanStudio.Core/Git/SorryHistory.cs new file mode 100644 index 0000000..292ff34 --- /dev/null +++ b/src/LeanStudio.Core/Git/SorryHistory.cs @@ -0,0 +1,103 @@ +using System.Globalization; +using System.Text; +using System.Text.RegularExpressions; + +namespace LeanStudio.Core.Git; + +/// One commit and how many sorrys the project had in it. +/// The commit's hash. +/// Its author date, yyyy-MM-dd. +/// Its first line. +/// The sorry and admit words in its Lean files, outside -- comments. +public sealed record SorryPoint(string Hash, string Date, string Subject, int Sorries); + +/// +/// How a formalization is coming along, read from Git: the number of sorrys the project had at each of its latest +/// commits, oldest first, drawn as a sparkline. Counted with git grep on each commit, so nothing is checked out or +/// built and a long history takes seconds. A sorry inside a block comment still counts; one after -- does not. +/// +public static class SorryHistory +{ + private static readonly Regex Word = new(@"\b(?:sorry|admit)\b", RegexOptions.Compiled); + + /// The sorries in , the lines git grep -n printed (commit:path:line:text). + public static int Count(string grepOutput) + { + int count = 0; + foreach (string line in grepOutput.Split('\n')) + { + string[] parts = line.TrimEnd('\r').Split(':', 4); + if (parts.Length < 4) + { + continue; + } + string text = parts[3]; + int comment = text.IndexOf("--", StringComparison.Ordinal); + count += Word.Matches(comment >= 0 ? text[..comment] : text).Count; + } + return count; + } + + /// The commits git log --format=%H%x09%as%x09%s printed, newest first, as (hash, date, subject). + public static IReadOnlyList<(string Hash, string Date, string Subject)> ParseLog(string log) => + [.. log.Split('\n').Select(l => l.TrimEnd('\r').Split('\t', 3)).Where(p => p.Length == 3 && p[0].Length >= 7).Select(p => (p[0], p[1], p[2]))]; + + /// + /// The sorries at each of the latest commits of , + /// oldest first. Empty when it has no history. + /// + public static async Task> ReadAsync(GitRepository repo, int commits = 30, CancellationToken ct = default) + { + Processes.ProcessResult log = await repo.RunAsync(["log", $"-n{Math.Clamp(commits, 1, 500)}", "--format=%H%x09%as%x09%s"], ct: ct).ConfigureAwait(false); + if (!log.Success) + { + return []; + } + var points = new List(); + foreach ((string hash, string date, string subject) in ParseLog(log.Output).Reverse()) + { + ct.ThrowIfCancellationRequested(); + // Exit code 1 means no match: the commit has no sorry (or no Lean file), which is a count of 0. + Processes.ProcessResult grep = await repo.RunAsync(["grep", "-n", "-I", "-E", @"\b(sorry|admit)\b", hash, "--", "*.lean"], ct: ct).ConfigureAwait(false); + points.Add(new SorryPoint(hash, date, subject, grep.ExitCode is 0 or 1 ? Count(grep.Output) : 0)); + } + return points; + } + + /// The counts as one character each, ▁ for the lowest to █ for the highest; all ▁ when they are equal. + public static string Sparkline(IEnumerable counts) + { + const string Bars = "▁▂▃▄▅▆▇█"; + List list = [.. counts]; + if (list.Count == 0) + { + return ""; + } + int min = list.Min(), max = list.Max(); + return string.Concat(list.Select(c => max == min ? Bars[0] : Bars[(int)Math.Round((c - min) * (Bars.Length - 1.0) / (max - min))])); + } + + /// A plain-text summary: the sparkline, the first and the latest count, and a line for each commit that changed it. + public static string ToText(IReadOnlyList points) + { + if (points.Count == 0) + { + return "No commits to read."; + } + var sb = new StringBuilder(); + SorryPoint first = points[0], last = points[^1]; + sb.Append(CultureInfo.InvariantCulture, $"Sorries over the last {points.Count} commit{(points.Count == 1 ? "" : "s")}: {Sparkline(points.Select(p => p.Sorries))} {first.Sorries} → {last.Sorries}"); + int change = last.Sorries - first.Sorries; + sb.Append(change == 0 ? " (no change)\n" : string.Create(CultureInfo.InvariantCulture, $" ({(change > 0 ? "+" : "−")}{Math.Abs(change)})\n")); + int previous = first.Sorries; + foreach (SorryPoint p in points.Skip(1)) + { + if (p.Sorries != previous) + { + sb.Append(CultureInfo.InvariantCulture, $" {p.Date} {p.Hash[..7]} {(p.Sorries > previous ? "+" : "−")}{Math.Abs(p.Sorries - previous)} {p.Subject}\n"); + } + previous = p.Sorries; + } + return sb.ToString().TrimEnd(); + } +} diff --git a/src/LeanStudio.Mcp/LeanTools.cs b/src/LeanStudio.Mcp/LeanTools.cs index 27df427..34353a4 100644 --- a/src/LeanStudio.Mcp/LeanTools.cs +++ b/src/LeanStudio.Mcp/LeanTools.cs @@ -840,6 +840,20 @@ public static IReadOnlyList Tools(Workbench bench) => return Task.FromResult(ProjectHealthReport.ToMarkdown(ProjectHealthReport.Scan(p.Root, DateOnly.FromDateTime(DateTime.Today), ct), p.Root).TrimEnd()); }), + new("sorry_history", + "How a formalization is coming along: the number of sorry (and admit) words in the project's Lean files at each of its latest commits, oldest first, as a sparkline with the commits that changed the count. Read with git grep, so nothing is checked out or built; a sorry in a block comment still counts, one after -- does not.", + Schema(("project", "string", "Any path in the project; defaults to the server's project.", false), + ("commits", "integer", "How many of the latest commits to read (default 30, at most 500).", false)), + async (a, ct) => + { + LeanProject p = bench.ProjectFor(OptStr(a, "project")); + if (Core.Git.GitRepository.Find(p.Root) is not Core.Git.GitRepository repo) + { + throw new ToolException($"{p.Root} is not in a Git repository, so there is no history to read"); + } + return Core.Git.SorryHistory.ToText(await Core.Git.SorryHistory.ReadAsync(repo, OptInt(a, "commits") ?? 30, ct)); + }), + new("lint", "Run the linters CI runs on a Lean file of a Lake project: Mathlib's standard set in a project that uses Mathlib (its style linters among them), every linter Lean has elsewhere, and Batteries' environment linters (missing docstrings, simp normal form, unused arguments…) where Batteries is available. Lints the file as saved on disk.", Schema(("path", "string", "The .lean file.", true)), diff --git a/tests/LeanStudio.Tests/PickerAndConflictTests.cs b/tests/LeanStudio.Tests/PickerAndConflictTests.cs index 2b25fc5..3a51017 100644 --- a/tests/LeanStudio.Tests/PickerAndConflictTests.cs +++ b/tests/LeanStudio.Tests/PickerAndConflictTests.cs @@ -1,4 +1,5 @@ using LeanStudio.Core.Editing; +using LeanStudio.Core.Git; using LeanStudio.Core.Proofs; using LeanStudio.Core.Workflow; @@ -584,3 +585,72 @@ public async Task ScansAFolderAndSaysWhereMostIsLeft() } } } + +/// How many sorries a project had at each commit. +public sealed class SorryHistoryTests +{ + [Fact] + public void CountsSorriesOutsideLineComments() + { + const string grep = "abc:A.lean:3: sorry\nabc:A.lean:7: exact foo -- a sorry here is a comment\nabc:B.lean:2:theorem t : P := by sorry\nabc:B.lean:9: admit; sorry\nabc:B.lean:12:def sorryNot := 1\n"; + Assert.Equal(4, SorryHistory.Count(grep)); + Assert.Equal(0, SorryHistory.Count("")); + Assert.Equal(1, SorryHistory.Count("abc:A.lean:3: have : x := by sorry -- and: colons: here\r\n")); + } + + [Fact] + public void ReadsTheLogAndDrawsASparkline() + { + Assert.Equal([("aaaaaaa1", "2026-10-02", "Add b"), ("bbbbbbb2", "2026-10-01", "Start")], SorryHistory.ParseLog("aaaaaaa1\t2026-10-02\tAdd b\nbbbbbbb2\t2026-10-01\tStart\n\nnot a commit\n")); + Assert.Equal("█▅▁", SorryHistory.Sparkline([10, 6, 2])); + Assert.Equal("▁▁▁", SorryHistory.Sparkline([4, 4, 4])); + Assert.Equal("", SorryHistory.Sparkline([])); + Assert.Equal("▁█", SorryHistory.Sparkline([0, 7])); + } + + [Fact] + public void SummarizesWhatChanged() + { + SorryPoint[] points = + [ + new("1111111aaa", "2026-09-01", "Start", 8), new("2222222bbb", "2026-09-02", "Prove a", 5), + new("3333333ccc", "2026-09-03", "Docs", 5), new("4444444ddd", "2026-09-04", "State c", 6), + ]; + Assert.Equal("Sorries over the last 4 commits: █▁▁▃ 8 → 6 (−2)\n 2026-09-02 2222222 −3 Prove a\n 2026-09-04 4444444 +1 State c", SorryHistory.ToText(points)); + Assert.Equal("No commits to read.", SorryHistory.ToText([])); + Assert.EndsWith("(no change)", SorryHistory.ToText([new("1111111aaa", "2026-09-01", "Only", 3)]), StringComparison.Ordinal); + } + + [Fact] + public async Task ReadsARealRepository() + { + string dir = Directory.CreateTempSubdirectory("leanstudio-sorry-").FullName; + try + { + CancellationToken ct = TestContext.Current.CancellationToken; + Assert.NotNull((await Core.Git.GitRepository.InitAsync(dir, ct)).Path); + var repo = Core.Git.GitRepository.Find(dir)!; + async Task Commit(string lean, string message) + { + await File.WriteAllTextAsync(Path.Combine(dir, "A.lean"), lean, ct); + Assert.True((await repo.RunAsync(["add", "-A"], ct: ct)).Success); + Assert.True((await repo.RunAsync(["-c", "user.name=t", "-c", "user.email=t@t", "-c", "commit.gpgsign=false", "commit", "-m", message], ct: ct)).Success); + } + await Commit("theorem a : P := by sorry\ntheorem b : Q := by sorry\n", "Two sorries"); + await Commit("theorem a : P := by simp\ntheorem b : Q := by sorry\n", "Prove a"); + await Commit("theorem a : P := by simp\ntheorem b : Q := by simp\n", "Prove b"); + IReadOnlyList points = await SorryHistory.ReadAsync(repo, 10, ct); + Assert.Equal([2, 1, 0], points.Select(p => p.Sorries)); + Assert.Equal(["Two sorries", "Prove a", "Prove b"], points.Select(p => p.Subject)); + Assert.Equal(["Prove a", "Prove b"], (await SorryHistory.ReadAsync(repo, 2, ct)).Select(p => p.Subject)); + } + finally + { + foreach (string f in Directory.EnumerateFiles(dir, "*", SearchOption.AllDirectories)) + { + File.SetAttributes(f, FileAttributes.Normal); + } + Directory.Delete(dir, true); + } + } +} From 96c72b28b8341aaacb3cf65728741f64a4df5eb9 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 3 Oct 2026 20:39:32 +0000 Subject: [PATCH 14/18] Add What This Branch Changed Mathematically Co-Authored-By: Claude Sonnet 5.5 Claude-Session: https://claude.ai/code/session_01FF5AYRpU9TWeWY3CFh2ETw --- CHANGELOG.md | 1 + README.md | 1 + docs/ARCHITECTURE.md | 4 +- .../ViewModels/MainViewModel.Pro.cs | 37 +++++ src/LeanStudio.App/Views/MainWindow.axaml | 1 + src/LeanStudio.App/Views/MainWindow.axaml.cs | 1 + src/LeanStudio.Core/Git/StatementDiff.cs | 141 ++++++++++++++++++ src/LeanStudio.Mcp/LeanTools.cs | 23 +++ .../PickerAndConflictTests.cs | 70 +++++++++ 9 files changed, 277 insertions(+), 2 deletions(-) create mode 100644 src/LeanStudio.Core/Git/StatementDiff.cs diff --git a/CHANGELOG.md b/CHANGELOG.md index 8088821..5e4265a 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -29,6 +29,7 @@ - **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**: diff --git a/README.md b/README.md index a536c3a..155b79f 100644 --- a/README.md +++ b/README.md @@ -331,6 +331,7 @@ What CI and reviewers check, before you push: - **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. diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index 21bb85d..d6df8b1 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -130,7 +130,7 @@ shows them to a person or an assistant. | [`Ai/`](../src/LeanStudio.Core/Ai) | The AI in the editor: `IChatModel` and the clients behind it (`AppleIntelligence` and `AppleFmCliModel` for the `fm` command, `OllamaModel`, `OpenAiCompatibleModel`, `AnthropicModel`), `AiDiscovery` (what is running, and which model to use), `AiProver` (proofs from a model, checked by Lean), `AiAssistant` (explanations and chat), `AiText` (token estimates and trimming) and `SecretStore` (API keys). | | [`Editing/`](../src/LeanStudio.Core/Editing) | Text-level engines with no UI: `Abbreviations` (Unicode input), `LeanText` (comments, strings and declarations in Lean source), `LatexText` (docstring math as text), `Fuzzy` (picker matching), `ProjectSearch` (find and replace across files), `MultiCursor`, `VimEngine`, `EmacsEngine` and `KeyBindingsFile` (keybindings.json). The editor in the app is a thin host over them. | | [`Workflow/`](../src/LeanStudio.Core/Workflow) | Project-wide tools. `Workflow.cs` holds `Markers` (sorries and TODOs), `LakeOutput` (build problems), `LocalHistory`, `Loogle`, `LeanSearch`, `DocLinks`, `Blame` and `ProjectTasks`. Beside it: `Refactor` and `EmittedC` (module rename, replace across files, Compiled C), `Ffi` (`@[extern]` bindings checked against the project's C files, and C stubs), `ImportCheck` (unused imports), `ImportOrder` (sorted imports), `StyleCheck` (Mathlib's text rules), `MathlibConventions` (header, module docstring, theorem names), `DocCoverage` (definitions with no doc comment), `StaleDeprecations` (old deprecated aliases, found and deleted), `ZulipPost` (a question for the Lean Zulip chat), `TheoremNamer` (a Mathlib-style name from a statement), `DuplicateStatements` (theorems that state the same thing), `ProjectHealth` (a project counted into a report), `Lint`, `Instances`, `Deprecation` (deprecated aliases for renames), `DependencyBump` (Update Mathlib and see what broke), `Blueprint`, `ProjectCommands` (`.leanstudio/commands.json`), `ProgressReader` (progress read from what a task prints), `LeanCli` (the `lean` command line on a mirror copy) and `Essentials.cs` (`ElanInstaller`, `FileOps`, `ImportFinder`). | -| [`Git/`](../src/LeanStudio.Core/Git) | `SorryHistory` (sorries per commit, as a sparkline). `GitRepository` wraps your own `git` executable, so your config, hooks, credentials and signing all apply. `GitHub` goes through the `gh` CLI, so Lean Studio never handles a token. | +| [`Git/`](../src/LeanStudio.Core/Git) | `SorryHistory` (sorries per commit, as a sparkline), `StatementDiff` (the theorems a branch adds, removes and restates). `GitRepository` wraps your own `git` executable, so your config, hooks, credentials and signing all apply. `GitHub` goes through the `gh` CLI, so Lean Studio never handles a token. | | [`Learn/`](../src/LeanStudio.Core/Learn) | `Tutorial` and `Playground`; `TacticGuide`, `ErrorGuide` and `PlainEnglish` (goals read aloud) in `Guides.cs`; `Snippets`, `TheoremGallery` and `ProgramRunner` in `Library.cs`. | | [`Agents/`](../src/LeanStudio.Core/Agents) | For assistants and web pages: `Workbench` and `ProjectSession` (Lean for a program instead of a person, used by the MCP server), `StudioBridge` (the pipe between an assistant and an open window), `InfoviewBridge` (Lean's own infoview page, served to a web view or browser) and `AgentSetup` (writing each assistant's MCP configuration). | | [`Plugins/`](../src/LeanStudio.Core/Plugins) | `PluginLoader`: finds plugin assemblies and loads each in a load context of its own. | @@ -174,7 +174,7 @@ written to stdout. | Checking and reading a file | `project_info`, `check_file`, `goals`, `proof_steps`, `hover`, `suggestions`, `references`, `run_lean` | | Building and Tenet | `build`, `verify`, `axioms`, `why_not_proved`, `project_map` | | Proof tools | `prove`, `extract_lemma`, `ffi_bindings`, `profile` | -| For Mathlib contributors | `unused_imports`, `sort_imports`, `style_check`, `stale_deprecations`, `suggest_name`, `duplicate_statements`, `project_health`, `sorry_history`, `lint`, `heartbeats`, `instances`, `blueprint` | +| For Mathlib contributors | `unused_imports`, `sort_imports`, `style_check`, `stale_deprecations`, `suggest_name`, `duplicate_statements`, `project_health`, `sorry_history`, `statement_changes`, `lint`, `heartbeats`, `instances`, `blueprint` | | Walkthroughs and search | `export_walkthrough`, `search_mathlib`, and `declaration` and `search_declarations` (the compiled library, through Tenet) | | Toolchains | `toolchains` | | The open window | `studio_context`, `studio_show` | diff --git a/src/LeanStudio.App/ViewModels/MainViewModel.Pro.cs b/src/LeanStudio.App/ViewModels/MainViewModel.Pro.cs index 9f69d46..c5e5261 100644 --- a/src/LeanStudio.App/ViewModels/MainViewModel.Pro.cs +++ b/src/LeanStudio.App/ViewModels/MainViewModel.Pro.cs @@ -726,6 +726,43 @@ public async Task ShowSorryBurndownAsync() } } + /// + /// Say what the current branch changed mathematically, as a pull request would be read: the theorems it adds, removes + /// and restates since it left main, with proofs ignored. Written to Output as Markdown to paste into the pull request. + /// + [RelayCommand] + public async Task ShowStatementChangesAsync() + { + if (Project is null || Core.Git.GitRepository.Find(Project.Root) is not Core.Git.GitRepository repo) + { + Log("Statements: open a project that is in a Git repository."); + return; + } + ProStatus = "Comparing theorem statements with main…"; + try + { + if (await Core.Git.StatementDiff.DefaultBaseAsync(repo) is not string baseRef) + { + Log("Statements: this branch has no commits of its own since main, so there is nothing to compare."); + return; + } + Core.Git.StatementChanges? changes = await Core.Git.StatementDiff.ReadAsync(repo, baseRef, "HEAD"); + if (changes is null) + { + Log("Statements: git could not compare the branch with main."); + return; + } + foreach (string line in Core.Git.StatementDiff.ToMarkdown(changes, baseRef[..Math.Min(7, baseRef.Length)], "HEAD").Split('\n')) + { + Log(line); + } + } + finally + { + ProStatus = ""; + } + } + // ---- linters ---- /// diff --git a/src/LeanStudio.App/Views/MainWindow.axaml b/src/LeanStudio.App/Views/MainWindow.axaml index 5ba4f0c..fcf1579 100644 --- a/src/LeanStudio.App/Views/MainWindow.axaml +++ b/src/LeanStudio.App/Views/MainWindow.axaml @@ -138,6 +138,7 @@ + diff --git a/src/LeanStudio.App/Views/MainWindow.axaml.cs b/src/LeanStudio.App/Views/MainWindow.axaml.cs index 7ab78b2..802e76f 100644 --- a/src/LeanStudio.App/Views/MainWindow.axaml.cs +++ b/src/LeanStudio.App/Views/MainWindow.axaml.cs @@ -1082,6 +1082,7 @@ private void OnLocationDoubleTapped(object? sender, TappedEventArgs e) yield return ("Lean: Sort Imports", "", Cmd(_vm.SortImportsCommand)); yield return ("Lean: Project Health Summary", "", Cmd(_vm.ShowProjectHealthCommand)); yield return ("Lean: Sorry Burndown (last 30 commits)", "", Cmd(_vm.ShowSorryBurndownCommand)); + yield return ("Lean: What This Branch Changed Mathematically", "", Cmd(_vm.ShowStatementChangesCommand)); yield return ("Lean: Find Duplicate Theorem Statements", "", Cmd(_vm.FindDuplicateStatementsCommand)); yield return ("Lean: Merge Consecutive rw / intro Steps", "", Cmd(_vm.MergeConsecutiveTacticsCommand)); yield return ("Lean: Suggest a Name for This Theorem", "", Cmd(_vm.SuggestTheoremNameCommand)); diff --git a/src/LeanStudio.Core/Git/StatementDiff.cs b/src/LeanStudio.Core/Git/StatementDiff.cs new file mode 100644 index 0000000..7fce824 --- /dev/null +++ b/src/LeanStudio.Core/Git/StatementDiff.cs @@ -0,0 +1,141 @@ +using System.Globalization; +using System.Text; +using LeanStudio.Core.Workflow; + +namespace LeanStudio.Core.Git; + +/// A theorem whose statement is not the one it had. +/// The theorem's name. +/// Its statement before. +/// Its statement after. +public sealed record ChangedStatement(string Name, string Before, string After); + +/// What a change did to the theorems a project states, leaving out how they are proved. +/// Theorems that were not there before. +/// Theorems that are gone. +/// Theorems of the same name whose statement differs by more than white space and the names of bound variables. +public sealed record StatementChanges(IReadOnlyList Added, IReadOnlyList Removed, IReadOnlyList Changed) +{ + /// Nothing was added, removed or restated. + public bool IsEmpty => Added.Count == 0 && Removed.Count == 0 && Changed.Count == 0; +} + +/// +/// What a change means mathematically: the theorems it adds, removes and restates, found by comparing statements +/// (not proofs) before and after. A reviewer of a pull request reads these first. Theorems are matched by name, so +/// moving one to another file is no change, and renaming one is a removal and an addition. +/// +public static class StatementDiff +{ + /// Compare the statements and , each sorted by name. + public static StatementChanges Compare(IEnumerable before, IEnumerable after) + { + Dictionary was = Index(before), now = Index(after); + return new StatementChanges( + [.. now.Values.Where(t => !was.ContainsKey(t.Name)).OrderBy(t => t.Name, StringComparer.Ordinal)], + [.. was.Values.Where(t => !now.ContainsKey(t.Name)).OrderBy(t => t.Name, StringComparer.Ordinal)], + [.. now.Values.Where(t => was.TryGetValue(t.Name, out TheoremStatement? old) + && DuplicateStatements.Normalize(old.Statement) != DuplicateStatements.Normalize(t.Statement)) + .OrderBy(t => t.Name, StringComparer.Ordinal).Select(t => new ChangedStatement(t.Name, was[t.Name].Statement, t.Statement))]); + } + + private static Dictionary Index(IEnumerable statements) + { + var index = new Dictionary(StringComparer.Ordinal); + foreach (TheoremStatement t in statements) + { + index.TryAdd(t.Name, t); + } + return index; + } + + /// + /// The statement changes of the Lean files that differ between and + /// in (git diff over them, the way a pull request compares), or null when git cannot compare them. + /// + public static async Task ReadAsync(GitRepository repo, string baseRef, string headRef, CancellationToken ct = default) + { + Processes.ProcessResult names = await repo.RunAsync(["diff", "--name-only", "--no-renames", baseRef, headRef, "--", "*.lean"], ct: ct).ConfigureAwait(false); + if (!names.Success) + { + return null; + } + var before = new List(); + var after = new List(); + foreach (string file in names.Output.Split('\n').Select(l => l.Trim()).Where(l => l.Length > 0)) + { + ct.ThrowIfCancellationRequested(); + Processes.ProcessResult was = await repo.RunAsync(["show", $"{baseRef}:{file}"], ct: ct).ConfigureAwait(false); + Processes.ProcessResult now = await repo.RunAsync(["show", $"{headRef}:{file}"], ct: ct).ConfigureAwait(false); + if (was.Success) + { + before.AddRange(DuplicateStatements.Statements(file, was.Output)); + } + if (now.Success) + { + after.AddRange(DuplicateStatements.Statements(file, now.Output)); + } + } + return Compare(before, after); + } + + /// + /// Where the current branch left the project's main line: the merge base of HEAD with the first of + /// origin/main, main, origin/master and master that exists, or null when there is none (or + /// the branch is that line, and so has nothing of its own). + /// + public static async Task DefaultBaseAsync(GitRepository repo, CancellationToken ct = default) + { + foreach (string candidate in new[] { "origin/main", "main", "origin/master", "master" }) + { + Processes.ProcessResult exists = await repo.RunAsync(["rev-parse", "--verify", "--quiet", candidate + "^{commit}"], ct: ct).ConfigureAwait(false); + if (!exists.Success) + { + continue; + } + Processes.ProcessResult mergeBase = await repo.RunAsync(["merge-base", candidate, "HEAD"], ct: ct).ConfigureAwait(false); + Processes.ProcessResult head = await repo.RunAsync(["rev-parse", "HEAD"], ct: ct).ConfigureAwait(false); + string hash = mergeBase.Output.Trim(); + return mergeBase.Success && hash.Length > 0 && hash != head.Output.Trim() ? hash : null; + } + return null; + } + + /// The changes as Markdown, to paste into a pull request: what is new, what is gone and what is restated. + public static string ToMarkdown(StatementChanges changes, string baseRef, string headRef) + { + var sb = new StringBuilder(); + sb.Append(CultureInfo.InvariantCulture, $"## Statements changed between `{baseRef}` and `{headRef}`\n\n"); + if (changes.IsEmpty) + { + return sb.Append("No theorem was added, removed or restated. Only proofs and other code changed.\n").ToString(); + } + if (changes.Added.Count > 0) + { + sb.Append(CultureInfo.InvariantCulture, $"**Added ({changes.Added.Count})**\n\n"); + foreach (TheoremStatement t in changes.Added) + { + sb.Append(CultureInfo.InvariantCulture, $"- `{t.Name}` {t.Statement}\n"); + } + sb.Append('\n'); + } + if (changes.Changed.Count > 0) + { + sb.Append(CultureInfo.InvariantCulture, $"**Restated ({changes.Changed.Count})**\n\n"); + foreach (ChangedStatement c in changes.Changed) + { + sb.Append(CultureInfo.InvariantCulture, $"- `{c.Name}`\n - before: {c.Before}\n - after: {c.After}\n"); + } + sb.Append('\n'); + } + if (changes.Removed.Count > 0) + { + sb.Append(CultureInfo.InvariantCulture, $"**Removed ({changes.Removed.Count})**\n\n"); + foreach (TheoremStatement t in changes.Removed) + { + sb.Append(CultureInfo.InvariantCulture, $"- `{t.Name}` {t.Statement}\n"); + } + } + return sb.ToString().TrimEnd() + "\n"; + } +} diff --git a/src/LeanStudio.Mcp/LeanTools.cs b/src/LeanStudio.Mcp/LeanTools.cs index 34353a4..788e03a 100644 --- a/src/LeanStudio.Mcp/LeanTools.cs +++ b/src/LeanStudio.Mcp/LeanTools.cs @@ -854,6 +854,29 @@ public static IReadOnlyList Tools(Workbench bench) => return Core.Git.SorryHistory.ToText(await Core.Git.SorryHistory.ReadAsync(repo, OptInt(a, "commits") ?? 30, ct)); }), + new("statement_changes", + "What a change means mathematically, the way a pull request is read: the theorems it adds, removes and restates, with proofs ignored (the names of bound variables and spacing do not count as a restatement). Compares two git refs of the project's Lean files; by default the current branch against where it left main. Markdown, ready to paste into a pull request.", + Schema(("project", "string", "Any path in the project; defaults to the server's project.", false), + ("base", "string", "The ref to compare from (default: where the current branch left main).", false), + ("head", "string", "The ref to compare to (default HEAD).", false)), + async (a, ct) => + { + LeanProject p = bench.ProjectFor(OptStr(a, "project")); + if (Core.Git.GitRepository.Find(p.Root) is not Core.Git.GitRepository repo) + { + throw new ToolException($"{p.Root} is not in a Git repository"); + } + string head = OptStr(a, "head") ?? "HEAD"; + string? baseRef = OptStr(a, "base") ?? await Core.Git.StatementDiff.DefaultBaseAsync(repo, ct); + if (baseRef is null) + { + return "this branch has no commits of its own since main, so there is nothing to compare (pass base)"; + } + Core.Git.StatementChanges changes = await Core.Git.StatementDiff.ReadAsync(repo, baseRef, head, ct) + ?? throw new ToolException($"git could not compare {baseRef} with {head}"); + return Core.Git.StatementDiff.ToMarkdown(changes, baseRef.Length >= 40 ? baseRef[..7] : baseRef, head).TrimEnd(); + }), + new("lint", "Run the linters CI runs on a Lean file of a Lake project: Mathlib's standard set in a project that uses Mathlib (its style linters among them), every linter Lean has elsewhere, and Batteries' environment linters (missing docstrings, simp normal form, unused arguments…) where Batteries is available. Lints the file as saved on disk.", Schema(("path", "string", "The .lean file.", true)), diff --git a/tests/LeanStudio.Tests/PickerAndConflictTests.cs b/tests/LeanStudio.Tests/PickerAndConflictTests.cs index 3a51017..169f9a6 100644 --- a/tests/LeanStudio.Tests/PickerAndConflictTests.cs +++ b/tests/LeanStudio.Tests/PickerAndConflictTests.cs @@ -654,3 +654,73 @@ async Task Commit(string lean, string message) } } } + +/// What a change did to the theorems a project states. +public sealed class StatementDiffTests +{ + private static TheoremStatement T(string name, string statement) => new("F.lean", 0, name, statement); + + [Fact] + public void FindsAddedRemovedAndRestatedTheorems() + { + StatementChanges changes = StatementDiff.Compare( + [T("keep", "(a : ℕ) : a = a"), T("gone", "True"), T("weaker", "(a : ℕ) : a ≤ a + 1"), T("renamed_var", "(a b : ℕ) : a + b = b + a")], + [T("keep", "(a : ℕ) : a = a"), T("fresh", "(n : ℕ) : n + 0 = n"), T("weaker", "(a : ℕ) : a < a + 1"), T("renamed_var", "(x y : ℕ) : x + y = y + x")]); + Assert.Equal(["fresh"], changes.Added.Select(t => t.Name)); + Assert.Equal(["gone"], changes.Removed.Select(t => t.Name)); + ChangedStatement c = Assert.Single(changes.Changed); // the renamed variables and the spacing are no change + Assert.Equal(("weaker", "(a : ℕ) : a ≤ a + 1", "(a : ℕ) : a < a + 1"), (c.Name, c.Before, c.After)); + Assert.False(changes.IsEmpty); + Assert.True(StatementDiff.Compare([T("a", "True")], [T("a", "True")]).IsEmpty); + } + + [Fact] + public void WritesMarkdownForAPullRequest() + { + StatementChanges changes = new([T("fresh", "(n : ℕ) : n + 0 = n")], [T("gone", "True")], [new ChangedStatement("weaker", "a ≤ b", "a < b")]); + Assert.Equal("## Statements changed between `main` and `topic`\n\n**Added (1)**\n\n- `fresh` (n : ℕ) : n + 0 = n\n\n**Restated (1)**\n\n- `weaker`\n - before: a ≤ b\n - after: a < b\n\n**Removed (1)**\n\n- `gone` True\n", + StatementDiff.ToMarkdown(changes, "main", "topic")); + Assert.Contains("Only proofs and other code changed.", StatementDiff.ToMarkdown(new StatementChanges([], [], []), "a", "b"), StringComparison.Ordinal); + } + + [Fact] + public async Task ComparesTwoRefsOfARealRepositoryAndIgnoresProofs() + { + string dir = Directory.CreateTempSubdirectory("leanstudio-stmt-").FullName; + try + { + CancellationToken ct = TestContext.Current.CancellationToken; + Assert.NotNull((await GitRepository.InitAsync(dir, ct)).Path); + var repo = GitRepository.Find(dir)!; + async Task Commit(string lean, string message) + { + await File.WriteAllTextAsync(Path.Combine(dir, "A.lean"), lean, ct); + Assert.True((await repo.RunAsync(["add", "-A"], ct: ct)).Success); + Assert.True((await repo.RunAsync(["-c", "user.name=t", "-c", "user.email=t@t", "-c", "commit.gpgsign=false", "commit", "-m", message], ct: ct)).Success); + } + await Commit("theorem a (n : ℕ) : n + 0 = n := by sorry\ntheorem b : 1 = 1 := rfl\n", "Start"); + await Commit("theorem a (m : ℕ) : m + 0 = m := by simp\ntheorem c (n : ℕ) : 0 + n = n := by simp\n", "Prove a, drop b, add c"); + StatementChanges? changes = await StatementDiff.ReadAsync(repo, "HEAD~1", "HEAD", ct); + Assert.NotNull(changes); + Assert.Equal(["c"], changes.Added.Select(t => t.Name)); + Assert.Equal(["b"], changes.Removed.Select(t => t.Name)); + Assert.Empty(changes.Changed); // `a` has a new proof and a renamed variable, the same statement + Assert.Null(await StatementDiff.ReadAsync(repo, "no-such-ref", "HEAD", ct)); + + Assert.Null(await StatementDiff.DefaultBaseAsync(repo, ct)); // on main itself there is nothing of its own + string mainTip = (await repo.RunAsync(["rev-parse", "HEAD"], ct: ct)).Output.Trim(); + Assert.True((await repo.RunAsync(["checkout", "-q", "-b", "topic"], ct: ct)).Success); + await Commit("theorem a (m : ℕ) : m + 0 = m := by simp\ntheorem c (n : ℕ) : 0 + n = n := by simp\ntheorem d : True := trivial\n", "Add d"); + Assert.Equal(mainTip, await StatementDiff.DefaultBaseAsync(repo, ct)); + Assert.Equal(["d"], (await StatementDiff.ReadAsync(repo, mainTip, "HEAD", ct))!.Added.Select(t => t.Name)); + } + finally + { + foreach (string f in Directory.EnumerateFiles(dir, "*", SearchOption.AllDirectories)) + { + File.SetAttributes(f, FileAttributes.Normal); + } + Directory.Delete(dir, true); + } + } +} From a101f9f7764cef911abe0158d8160a077e79762d Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 3 Oct 2026 20:41:32 +0000 Subject: [PATCH 15/18] Run the new Lean-menu commands in the real headless window, and in CI Co-Authored-By: Claude Sonnet 5.5 Claude-Session: https://claude.ai/code/session_01FF5AYRpU9TWeWY3CFh2ETw --- .github/workflows/ci.yml | 3 + CONTRIBUTING.md | 9 +- tools/LeanStudio.Snapshot/CommandChecks.cs | 161 +++++++++++++++++++++ tools/LeanStudio.Snapshot/Program.cs | 2 + 4 files changed, 174 insertions(+), 1 deletion(-) create mode 100644 tools/LeanStudio.Snapshot/CommandChecks.cs diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 061b742..5721bbd 100644 --- a/.github/workflows/ci.yml +++ b/.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: diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index e72ad99..c16212f 100644 --- a/CONTRIBUTING.md +++ b/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 diff --git a/tools/LeanStudio.Snapshot/CommandChecks.cs b/tools/LeanStudio.Snapshot/CommandChecks.cs new file mode 100644 index 0000000..dfdf234 --- /dev/null +++ b/tools/LeanStudio.Snapshot/CommandChecks.cs @@ -0,0 +1,161 @@ +using CommunityToolkit.Mvvm.Input; +using LeanStudio.App.Services; +using LeanStudio.App.ViewModels; +using LeanStudio.App.Views; + +namespace LeanStudio.Snapshot; + +/// +/// The text, Mathlib and Git commands of the Lean menu, run in the real (headless) window on real documents: +/// LeanStudio.Snapshot --commands. Needs git but not Lean, so it runs anywhere the app builds. +/// +internal static class CommandChecks +{ + private static int _failures; + + private static void Check(bool ok, string what) + { + Console.WriteLine((ok ? " ok " : " FAIL ") + what); + if (!ok) + { + _failures++; + } + } + + public static async Task RunAsync() + { + string dir = Directory.CreateTempSubdirectory("leanstudio-commands-").FullName; + try + { + await Git(dir, "init", "-q", "-b", "main"); + string path = Path.Combine(dir, "A.lean"); + await File.WriteAllTextAsync(path, "theorem a (n : Nat) : n + 0 = n := by sorry\ntheorem b (n : Nat) : n = n := by sorry\n"); + await Git(dir, "add", "-A"); + await Git(dir, "-c", "user.name=Ada Lovelace", "-c", "user.email=a@l", "-c", "commit.gpgsign=false", "commit", "-q", "-m", "Two sorries"); + await File.WriteAllTextAsync(path, "theorem a (n : Nat) : n + 0 = n := by simp\ntheorem b (n : Nat) : n = n := by sorry\n"); + await Git(dir, "-c", "user.name=Ada Lovelace", "-c", "user.email=a@l", "-c", "commit.gpgsign=false", "commit", "-q", "-am", "Prove a"); + await Git(dir, "config", "user.name", "Ada Lovelace"); + + var window = new MainWindow(new Settings()) { Width = 1200, Height = 800 }; + window.Taskbar.UseNative = false; + window.OpenOnStartup = dir; + window.Show(); + MainViewModel vm = window.ViewModel; + Check(await WaitFor(() => vm.Project is not null, 30), "the project opens"); + DocumentViewModel? doc = await vm.OpenFileAsync(path); + Check(doc is not null, "a Lean file opens"); + if (doc is null) + { + return 1; + } + + string Text() => doc.Document.Text; + void Set(string text) => doc.Document.Text = text; + string Output() => vm.Output.Text; + async Task Run(IRelayCommand command) + { + if (command is IAsyncRelayCommand async) + { + await async.ExecuteAsync(null); + } + else + { + command.Execute(null); + } + } + + Console.WriteLine("sort imports"); + Set("import B\nimport A\nimport B\n\ndef x := 1\n"); + await Run(vm.SortImportsCommand); + Check(Text() == "import A\nimport B\n\ndef x := 1\n", "Sort Imports orders and de-duplicates the header"); + doc.Document.UndoStack.Undo(); + Check(Text() == "import B\nimport A\nimport B\n\ndef x := 1\n", "and one undo brings the old order back"); + + Console.WriteLine("whitespace and style"); + Set("def a := 1 \r\n\tdef b := 2\r\n\r\n\r\n"); + await Run(vm.TidyWhitespaceCommand); + Check(Text() == "def a := 1\n def b := 2\n", "Tidy Whitespace fixes trailing spaces, tabs, CRLF and the final newlines"); + Set("import B\nimport A \n\ndef x := 1\t"); + await Run(vm.TidyFileCommand); + Check(Text() == "import A\nimport B\n\ndef x := 1\n", "Tidy File sorts the imports and fixes the whitespace in one edit"); + Set("-- " + string.Join(' ', Enumerable.Repeat("word", 40)) + "\n"); + await Run(vm.WrapLongCommentsCommand); + Check(Text().Split('\n').All(l => l.Length <= 100) && Text().Contains("\n-- word", StringComparison.Ordinal), "Wrap Long Comment Lines breaks a long comment"); + + Console.WriteLine("proof clean-ups"); + Set("theorem t : P := by\n intro x\n intro y\n rw [a]\n rw [b]\n exact h\n"); + await Run(vm.MergeConsecutiveTacticsCommand); + Check(Text() == "theorem t : P := by\n intro x y\n rw [a, b]\n exact h\n", "Merge Consecutive rw / intro Steps merges them"); + Set("@[deprecated (since := \"2020-01-01\")] alias old := new\n\ndef new := 1\n"); + await Run(vm.RemoveStaleDeprecationsCommand); + Check(Text() == "def new := 1\n", "Remove Deprecations Older Than Six Months deletes the old alias"); + + Console.WriteLine("Mathlib conventions"); + Set("import A\n"); + await Run(vm.AddMathlibHeaderCommand); + Check(Text().StartsWith("/-\nCopyright (c) ", StringComparison.Ordinal) && Text().Contains(" Ada Lovelace. All rights reserved.\n", StringComparison.Ordinal) + && Text().EndsWith("-/\nimport A\n", StringComparison.Ordinal), "Add Mathlib Copyright Header writes the header with the git user's name"); + string before = Text(); + await Run(vm.AddMathlibHeaderCommand); + Check(Text() == before, "and leaves a file that starts with a comment alone"); + Set("theorem a (a b : ℕ) :\n a + b = b + a := by omega\n"); + doc.Reveal(1, 0); + await Run(vm.SuggestTheoremNameCommand); + Check(Output().Contains("`add_comm`", StringComparison.Ordinal), "Suggest a Name for This Theorem says add_comm"); + + Console.WriteLine("project and Git"); + await File.WriteAllTextAsync(Path.Combine(dir, "B.lean"), "theorem b2 (n : Nat) : n = n := by simp\n"); + await File.WriteAllTextAsync(Path.Combine(dir, "C.lean"), "theorem c2 (k : Nat) : k = k := by simp\ndef undocumented := 1\n"); + await Run(vm.ShowProjectHealthCommand); + Check(Output().Contains("## Project health", StringComparison.Ordinal) && Output().Contains("sorry", StringComparison.Ordinal), "Project Health Summary reports into Output"); + await Run(vm.FindDuplicateStatementsCommand); + Check(Output().Contains("Same statement:", StringComparison.Ordinal) && Output().Contains("b2", StringComparison.Ordinal) && Output().Contains("c2", StringComparison.Ordinal), + "Find Duplicate Theorem Statements finds b2 and c2 stating the same thing"); + await Run(vm.ShowSorryBurndownCommand); + Check(Output().Contains("Sorries over the last 2 commits: █▁ 2 → 1 (−1)", StringComparison.Ordinal) || Output().Contains("2 → 1", StringComparison.Ordinal), "Sorry Burndown draws 2 → 1 from the history"); + await Run(vm.ShowStatementChangesCommand); + Check(Output().Contains("nothing to compare", StringComparison.Ordinal), "What This Branch Changed Mathematically says there is nothing to compare on main itself"); + await Git(dir, "checkout", "-q", "-b", "topic"); + await File.WriteAllTextAsync(path, "theorem a (n : Nat) : n + 0 = n := by simp\ntheorem b (n : Nat) : n = n := by sorry\ntheorem fresh : True := trivial\n"); + await Git(dir, "-c", "user.name=t", "-c", "user.email=t@t", "-c", "commit.gpgsign=false", "commit", "-q", "-am", "Add fresh"); + await Run(vm.ShowStatementChangesCommand); + Check(Output().Contains("**Added (1)**", StringComparison.Ordinal) && Output().Contains("`fresh` : True", StringComparison.Ordinal), "and on a branch lists the theorem it added"); + + Console.WriteLine("share"); + await Run(vm.CopyForZulipCommand); + Check(Output().Contains("Copied this file as a Zulip message", StringComparison.Ordinal), "Copy as a Zulip Message copies the file"); + } + finally + { + foreach (string f in Directory.EnumerateFiles(dir, "*", SearchOption.AllDirectories)) + { + File.SetAttributes(f, FileAttributes.Normal); + } + Directory.Delete(dir, true); + } + return _failures; + } + + private static async Task Git(string dir, params string[] args) + { + var result = await LeanStudio.Core.Processes.ProcessRunner.RunAsync("git", args, dir); + if (!result.Success) + { + throw new InvalidOperationException("git " + string.Join(' ', args) + ": " + result.Output); + } + } + + private static async Task WaitFor(Func condition, double seconds) + { + var sw = System.Diagnostics.Stopwatch.StartNew(); + while (!condition()) + { + if (sw.Elapsed.TotalSeconds > seconds) + { + return false; + } + await Task.Delay(50); + } + return true; + } +} diff --git a/tools/LeanStudio.Snapshot/Program.cs b/tools/LeanStudio.Snapshot/Program.cs index 113fc03..63cf1de 100644 --- a/tools/LeanStudio.Snapshot/Program.cs +++ b/tools/LeanStudio.Snapshot/Program.cs @@ -52,6 +52,8 @@ { failures = args.Length > 2 && args[0] == "--validate" ? await Validate.RunAsync(Path.GetFullPath(args[1]), Path.GetFullPath(args[2]), args[3..]) + : args.Length > 0 && args[0] == "--commands" + ? await LeanStudio.Snapshot.CommandChecks.RunAsync() : args.Length > 1 && args[0] == "--leak" ? await LeanStudio.Snapshot.Leak.RunAsync(Path.GetFullPath(args[1])) : args.Length > 3 && args[0] == "--scale-profiler" From 5ca17a7f76debea2f85502ce7f2949b7d8d9f70f Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 3 Oct 2026 20:41:40 +0000 Subject: [PATCH 16/18] README: the new commands in the comparison with VS Code Co-Authored-By: Claude Sonnet 5.5 Claude-Session: https://claude.ai/code/session_01FF5AYRpU9TWeWY3CFh2ETw --- README.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/README.md b/README.md index 155b79f..2dd622f 100644 --- a/README.md +++ b/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 | | ✓ | From 0575df781044c36be04e566c459a40bce1b1de15 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 3 Oct 2026 20:47:36 +0000 Subject: [PATCH 17/18] Sorry Burndown: match sorry with git grep -w, as macOS's regex has no \b SorryHistoryTests.ReadsARealRepository found no sorries on macOS CI: the \b in the pattern given to git grep -E is not supported there. Co-Authored-By: Claude Sonnet 5.5 Claude-Session: https://claude.ai/code/session_01FF5AYRpU9TWeWY3CFh2ETw --- src/LeanStudio.Core/Git/SorryHistory.cs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/LeanStudio.Core/Git/SorryHistory.cs b/src/LeanStudio.Core/Git/SorryHistory.cs index 292ff34..0c28393 100644 --- a/src/LeanStudio.Core/Git/SorryHistory.cs +++ b/src/LeanStudio.Core/Git/SorryHistory.cs @@ -57,8 +57,9 @@ public static async Task> ReadAsync(GitRepository repo foreach ((string hash, string date, string subject) in ParseLog(log.Output).Reverse()) { ct.ThrowIfCancellationRequested(); + // -w, not a \b pattern: macOS's regular expressions have no \b, so there it matches nothing. // Exit code 1 means no match: the commit has no sorry (or no Lean file), which is a count of 0. - Processes.ProcessResult grep = await repo.RunAsync(["grep", "-n", "-I", "-E", @"\b(sorry|admit)\b", hash, "--", "*.lean"], ct: ct).ConfigureAwait(false); + Processes.ProcessResult grep = await repo.RunAsync(["grep", "-n", "-I", "-w", "-e", "sorry", "-e", "admit", hash, "--", "*.lean"], ct: ct).ConfigureAwait(false); points.Add(new SorryPoint(hash, date, subject, grep.ExitCode is 0 or 1 ? Count(grep.Output) : 0)); } return points; From fb800262c8f10ead7b5125259af8f0a53042352e Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 3 Oct 2026 20:56:17 +0000 Subject: [PATCH 18/18] Name a request whose write failed as the connection closed, and observe the reader's error When the other side died while a request still waited to be written, the reader failed it (naming it) and then its 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 the intermittent Windows failure of StressTests.WhenTheOtherSideDiesEveryWaitingRequestFailsPromptly and the Snapshot run's 'no error was caught behind the scenes' check (textDocument/documentSymbol, documentHighlight). A new test reproduces it deterministically with gated streams. Co-Authored-By: Claude Sonnet 5.5 Claude-Session: https://claude.ai/code/session_01FF5AYRpU9TWeWY3CFh2ETw --- src/LeanStudio.Lsp/JsonRpcConnection.cs | 20 ++++- tests/LeanStudio.Tests/StressTests.cs | 98 +++++++++++++++++++++++++ 2 files changed, 117 insertions(+), 1 deletion(-) diff --git a/src/LeanStudio.Lsp/JsonRpcConnection.cs b/src/LeanStudio.Lsp/JsonRpcConnection.cs index a1008c2..fc3ac7d 100644 --- a/src/LeanStudio.Lsp/JsonRpcConnection.cs +++ b/src/LeanStudio.Lsp/JsonRpcConnection.cs @@ -133,9 +133,16 @@ public async Task RequestAsync(string method, object? parameters, C { await WriteAsync(msg).ConfigureAwait(false); } + catch (IOException e) + { + Abandon(id, tcs); + // The other side may have died while this request waited to be written: the reader has then failed it + // already, naming it. The caller is told the same, not just that a pipe broke. + throw new IOException($"the language server connection closed (while waiting for {method})", e); + } catch { - _pending.TryRemove(id, out _); + Abandon(id, tcs); throw; } try @@ -220,6 +227,17 @@ private async Task WriteAsync(JsonObject msg) private volatile bool _disposed; + /// + /// Stop waiting for request because it could not be written. If the reader failed it first + /// (the connection closed meanwhile), that error is observed here: nobody else will await it. + /// + private void Abandon(long id, TaskCompletionSource tcs) + { + _pending.TryRemove(id, out _); + _pendingMethods.TryRemove(id, out _); + Forget(tcs.Task); + } + /// Let a message go without waiting for it; if it fails (the connection closed), that is not an error. private static void Forget(Task t) => t.ContinueWith(static x => _ = x.Exception, TaskContinuationOptions.OnlyOnFaulted | TaskContinuationOptions.ExecuteSynchronously); diff --git a/tests/LeanStudio.Tests/StressTests.cs b/tests/LeanStudio.Tests/StressTests.cs index 63d3ee9..1e79ea3 100644 --- a/tests/LeanStudio.Tests/StressTests.cs +++ b/tests/LeanStudio.Tests/StressTests.cs @@ -141,6 +141,104 @@ public async Task AfterClosingEveryCallFailsTheWayCallersExpect() await wire.DisposeAsync(); } + /// An input that gives no byte until it is told to end. + private sealed class EndsOnCommand(Task end) : Stream + { + public override bool CanRead => true; + public override bool CanSeek => false; + public override bool CanWrite => false; + public override long Length => throw new NotSupportedException(); + public override long Position { get => throw new NotSupportedException(); set => throw new NotSupportedException(); } + public override void Flush() { } + public override int Read(byte[] buffer, int offset, int count) => throw new NotSupportedException(); + public override long Seek(long offset, SeekOrigin origin) => throw new NotSupportedException(); + public override void SetLength(long value) => throw new NotSupportedException(); + public override void Write(byte[] buffer, int offset, int count) => throw new NotSupportedException(); + + public override async ValueTask ReadAsync(Memory buffer, CancellationToken cancellationToken = default) + { + await end.WaitAsync(cancellationToken); + return 0; // the other side has gone + } + } + + /// An output whose first write waits to be released, and then fails as a pipe whose reader has died does. + private sealed class BreaksOnCommand(Task release, TaskCompletionSource entered) : Stream + { + public override bool CanRead => false; + public override bool CanSeek => false; + public override bool CanWrite => true; + public override long Length => throw new NotSupportedException(); + public override long Position { get => throw new NotSupportedException(); set => throw new NotSupportedException(); } + public override void Flush() { } + public override Task FlushAsync(CancellationToken cancellationToken) => Task.CompletedTask; + public override int Read(byte[] buffer, int offset, int count) => throw new NotSupportedException(); + public override long Seek(long offset, SeekOrigin origin) => throw new NotSupportedException(); + public override void SetLength(long value) => throw new NotSupportedException(); + public override void Write(byte[] buffer, int offset, int count) => throw new NotSupportedException(); + + public override async ValueTask WriteAsync(ReadOnlyMemory buffer, CancellationToken cancellationToken = default) + { + entered.TrySetResult(); + await release.WaitAsync(cancellationToken); + throw new IOException("Pipe is broken."); + } + } + + [Fact] + public async Task ARequestWhoseWriteFailsAfterTheReaderSawTheCloseNamesItAndLeavesNothingUnobserved() + { + // The other side dies while a request is still waiting to be written: the reader fails it (naming it), and + // then its write fails too. The caller must be told which request it was, as for any other, and the error the + // reader gave must not be left for the finalizer to report. + var unobserved = new List(); + void OnUnobserved(object? sender, UnobservedTaskExceptionEventArgs e) + { + lock (unobserved) + { + unobserved.Add(e.Exception); + } + } + TaskScheduler.UnobservedTaskException += OnUnobserved; + try + { + IOException failure = await FailARequestAsync(TestContext.Current.CancellationToken); + Assert.Contains("(while waiting for hang)", failure.Message, StringComparison.Ordinal); + Assert.Equal("Pipe is broken.", failure.InnerException?.Message); + for (int i = 0; i < 3; i++) + { + GC.Collect(); + GC.WaitForPendingFinalizers(); + } + lock (unobserved) + { + Assert.Empty(unobserved); + } + } + finally + { + TaskScheduler.UnobservedTaskException -= OnUnobserved; + } + } + + [System.Runtime.CompilerServices.MethodImpl(System.Runtime.CompilerServices.MethodImplOptions.NoInlining)] + private static async Task FailARequestAsync(CancellationToken ct) + { + var end = new TaskCompletionSource(TaskCreationOptions.RunContinuationsAsynchronously); + var release = new TaskCompletionSource(TaskCreationOptions.RunContinuationsAsynchronously); + var entered = new TaskCompletionSource(TaskCreationOptions.RunContinuationsAsynchronously); + var closed = new TaskCompletionSource(TaskCreationOptions.RunContinuationsAsynchronously); + await using var connection = new JsonRpcConnection(new EndsOnCommand(end.Task), new BreaksOnCommand(release.Task, entered)); + connection.Closed += _ => closed.TrySetResult(); + connection.Start(); + Task request = connection.RequestAsync("hang", null, ct); + await entered.Task.WaitAsync(TimeSpan.FromSeconds(10), ct); // its write is under way and waiting + end.SetResult(); // the other side goes: the reader fails the request that is waiting + await closed.Task.WaitAsync(TimeSpan.FromSeconds(10), ct); + release.SetResult(); // and now its write fails too + return await Assert.ThrowsAsync(() => request.WaitAsync(TimeSpan.FromSeconds(10), ct)); + } + [Fact] public async Task GarbageJsonIsSkippedAndTheConversationGoesOn() {