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/CHANGELOG.md b/CHANGELOG.md index ce6ce70..5e4265a 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). @@ -14,6 +14,24 @@ - **Dev containers and WSL**: *Remote: Use the Dev Container* runs a project's Lean in its dev container (found running, or started with `devcontainer up`), which mounts the folder, so no sshfs is needed. On Windows, a folder in WSL runs its Lean inside WSL by itself. - Each file came back scrolled to the top after switching to another and back: AvaloniaEdit's `ScrollToVerticalOffset` does nothing in the version used. It now keeps its place. +**New**: +- **Sort Imports** (*Lean ▸ Sort Imports*, and in the command palette): puts each run of `import` lines in the file's header in order by module name and drops repeats, as Mathlib's style asks. Blank lines and comments between runs stay, so a deliberate grouping is kept; nothing below the header moves. One undoable edit that touches only the lines that changed. +- **Tidy Whitespace and Check Style** (*Lean ▸ Tidy Whitespace and Check Style*): holds the file to the text rules of Mathlib's style linter. Trailing whitespace, tabs, Windows line endings and a missing or doubled final newline are fixed as one undoable edit; lines over 100 characters are listed in Output for you to break. +- **Tidy File** (*Lean ▸ Tidy File*) does both in one undoable edit: sorts the imports, fixes the whitespace, and lists what is left (long lines and, in a project that uses Mathlib, the file conventions). +- **Mathlib's file conventions**: the copyright header, a module docstring, and theorem names that start with a capital are reported by *Tidy File* in a Mathlib project and by `style_check` over MCP (`mathlib=true` forces it). **Add Mathlib Copyright Header** puts the header on a file that has none, for this year and the name git is set up with. +- **Remove Deprecations Older Than Six Months** (*Lean ▸ Remove Deprecations Older Than Six Months*): Mathlib deletes a deprecated alias some months after the rename. Reads each `(since := "…")`, and deletes those past the age, with their doc comments, as one undoable edit; each is named in Output. The counterpart of the deprecated alias *Rename* writes. `stale_deprecations` does the same over MCP, with `months` and `apply`. +- **Doc comments on definitions**: in a Mathlib project, Tidy File and `style_check` also list each public `def`, `abbrev`, `structure`, `class` and `inductive` with no doc comment, as Mathlib's `docBlame` linter asks, read from the text, so nothing has to be built first. +- **Wrap Long Comment Lines** (*Lean ▸ Wrap Long Comment Lines*): breaks the `--` comment and docstring lines over 100 characters at a space, which Tidy cannot do for you, as one undoable edit. Code, code fences, indented code in a docstring and words longer than the limit (a URL) are never touched. `style_check` takes `wrap=true` with `apply`. +- Structure, class and inductive names that start with a lowercase letter are now reported by the Mathlib conventions check. +- **Copy as a Zulip Message** (*File ▸ Copy as a Zulip Message*, and under Share in the palette): the active file in a `lean` fence and, in a quote below it, what Lean says about it, errors first, ready to paste into the Lean Zulip chat. The fences grow when the code has backticks of its own. +- **Suggest a Name for This Theorem** (*Lean ▸ Suggest a Name for This Theorem*): reads the statement of the theorem at the cursor and gives the name Mathlib's scheme would: the conclusion read left to right with each operation and relation as a word, then `_of_` before each assumption. `a + b = b + a` is `add_comm`, `0 + a = a` is `zero_add`, `a ≤ b → b < c → a < c` is `lt_of_le_of_lt`. It says whether the theorem's own name matches; *Rename Symbol* applies it. A starting point for statements about operations and relations, not an oracle. `suggest_name` does the same over MCP. +- **Merge Consecutive rw / intro Steps** (*Lean ▸ Merge Consecutive rw / intro Steps*): `rw [a]` then `rw [b]` become `rw [a, b]` (also `simp_rw`, and for the same `at` location), and two `intro` lines become one, as one undoable edit. Only whole lines that do nothing else are merged, so the proof means exactly what it did. `merge_tactics` does the same over MCP. +- **Find Duplicate Theorem Statements** (*Lean ▸ Find Duplicate Theorem Statements*): looks through the project's Lean files for theorems that state the same thing under different names, with the names of the variables they bind and the spacing left out (`(a b : ℕ) : a + b = b + a` is `(x y : ℕ) : x + y = y + x`), and lists each group in Output with its files and lines. Mathlib asks that a result is stated once. Statements are compared as text, so two that are equal only by unfolding are not found. `duplicate_statements` does the same over MCP. +- **Project Health Summary** (*Lean ▸ Project Health Summary*): the project's state at a glance, counted from its Lean files without building anything: files, lines, theorems and definitions; `sorry` and TODO counts; the share of definitions with a doc comment; deprecated declarations and how many are old enough to delete; style problems; and the five files with the most still to do. `project_health` does the same over MCP, as Markdown. +- **Sorry Burndown** (*Lean ▸ Sorry Burndown*): how a formalization is coming along. The number of `sorry`s the project had at each of its last 30 commits, as a sparkline (`▇▅▃▁`) and the commits that moved the count (`2026-09-02 2222222 −3 Prove a`). Read with `git grep` on each commit, so nothing is checked out or built and a long history takes seconds. `sorry_history` does the same over MCP, with `commits`. +- **What This Branch Changed Mathematically** (*Lean ▸ What This Branch Changed Mathematically*): the theorems the current branch adds, removes and restates since it left `main`, the way a reviewer reads a pull request, with the proofs ignored. A theorem proved differently, or with renamed variables, is no change; one whose statement differs is listed with its before and after. Markdown in Output, ready to paste into the pull request. `statement_changes` does the same over MCP, between any two refs. +- **Over MCP**, `sort_imports` and `style_check` do the same for assistants, each with `apply` to write the file. + **Fixes**: - `verify` over MCP kept returning the declarations of the build it first read after the project was built again outside it (`lake build` in a terminal), until the server restarted ([#2](https://github.com/keithadler/leanstudio/issues/2)). Tenet now notes the build it opened (each `.olean`'s size and time, the manifest and the toolchain) and reads the new one when it has changed; the window's Verify, Why?, the project map and the blueprint check do the same. - A request to Lean left waiting when its server stopped could surface later as an error no one caught; the error now also names the request. 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/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 ec3554d..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 | | ✓ | @@ -328,6 +330,18 @@ The infoview shares Lean Studio's Lean server, so nothing starts twice. "Try thi What CI and reviewers check, before you push: - **Remove Unused Imports** (*Lean ▸ Remove Unused Imports*) takes out the imports a file doesn't need, as one undoable edit, and says why for each: nothing uses it, or another import already brings it in. Lean elaborates the file, and every constant, tactic, macro and notation it uses is traced to its module, so an import needed only for `ring` or a notation stays. It works on any file, not only `module` files like `lake shake`. It takes seconds on Mathlib files. +- **Sort Imports** (*Lean ▸ Sort Imports*) puts each run of `import` lines in the header in order by module name and drops repeats, as Mathlib's style asks, leaving comments, blank-line groups and the body alone. +- **Tidy Whitespace and Check Style** (*Lean ▸ Tidy Whitespace and Check Style*) holds a file to Mathlib's text rules: trailing whitespace, tabs, CRLF and the final newline are fixed in one undoable edit, and lines over 100 characters are listed for you to break. +- **Tidy File** does Sort Imports and the whitespace fixes in one edit; in a Mathlib project it also reports a missing copyright header or module docstring and theorem names that start with a capital, and **Add Mathlib Copyright Header** writes the header for you. +- **What This Branch Changed Mathematically** lists the theorems a branch adds, removes and restates since `main`, with proofs ignored, as Markdown for the pull request: what a reviewer reads first. +- **Sorry Burndown** draws the project's `sorry` count over its last 30 commits as a sparkline and names the commits that moved it, straight from Git, with nothing built. +- **Project Health Summary** counts the project's files into a report: size, sorries and TODOs, doc-comment coverage, deprecations and style problems, and where the most is left to do. +- **Find Duplicate Theorem Statements** lists theorems of the project that state the same thing under different names, with each one's file and line. +- **Merge Consecutive rw / intro Steps** turns `rw [a]` then `rw [b]` (or `simp_rw`, or two `intro`s) into one line, where that cannot change the proof. +- **Suggest a Name for This Theorem** works out the name Mathlib's scheme would give a theorem from its statement (`a + b = b + a` is `add_comm`; `a ≤ b → b < c → a < c` is `lt_of_le_of_lt`) and says whether yours matches. +- **Copy as a Zulip Message** (*File ▸ Copy as a Zulip Message*) puts the file in a `lean` fence with Lean's errors and warnings in a quote under it, ready to paste into the Lean Zulip chat. +- **Wrap Long Comment Lines** breaks over-long `--` comments and docstring prose at a space, the one style problem Tidy leaves to you; code is never touched. +- **Remove Deprecations Older Than Six Months** deletes the deprecated aliases whose `(since := "…")` is old enough, with their doc comments, in one undoable edit; Tidy File in a Mathlib project also lists public definitions with no doc comment. - **Lint File** runs the linters CI runs and lists what they find in Problems. In a Mathlib project that's Mathlib's standard set, its style linters among them. Wherever Batteries is available it also runs Batteries' environment linters: missing docstrings, `simp` normal form, unused arguments. Elsewhere it runs every linter Lean has. - **Renames keep the old name working.** After Rename Symbol on a declaration, Lean Studio offers to add `@[deprecated (since := "…")] alias old := new` after it, as Mathlib asks. Without Batteries it writes the core Lean equivalent. - **The library root stays complete.** A new file is added to its library's root file when that imports every module (as `Mathlib.lean` does), and a deleted one is taken out. *Import Every Module in the Library Root* adds any that are missing, like `lake exe mk_all`. @@ -652,7 +666,7 @@ The build generates XML documentation for every project in `src/`, and a public ## Status -Lean Studio is at **0.10**, and the [changelog](CHANGELOG.md) lists what's new since then. The whole workflow works end to end and is tested against real Lean 4.34. It has been used by hand on macOS; on Windows and Linux it is built and tested by CI. Known gaps: +Lean Studio is at **0.11**, and the [changelog](CHANGELOG.md) lists what's new since then. The whole workflow works end to end and is tested against real Lean 4.34. It has been used by hand on macOS; on Windows and Linux it is built and tested by CI. Known gaps: - User widgets render in the Infoview tab, not in the Tactic State panel, which shows Lean's interactive text. On Linux the tab needs WebKitGTK; without it, widgets open in the browser. - Tenet's badges describe the last build. After you edit a file, rebuild to refresh them. diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index ca5c4c6..d6df8b1 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -126,11 +126,11 @@ 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), `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. | +| [`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), `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`, `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.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/ViewModels/MainViewModel.Pro.cs b/src/LeanStudio.App/ViewModels/MainViewModel.Pro.cs index d749570..c5e5261 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; @@ -412,6 +413,356 @@ 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."); + } + + /// + /// 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."); + } + + /// + /// 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); + } + 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}"); + } + 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."); + } + + /// + /// 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."); + } + + /// + /// 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.")); + } + + /// + /// 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."); + } + + /// + /// 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."); + } + + /// + /// 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 = ""; + } + } + + /// + /// 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 = ""; + } + } + + /// + /// 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 = ""; + } + } + + /// + /// 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 0e8527e..fcf1579 100644 --- a/src/LeanStudio.App/Views/MainWindow.axaml +++ b/src/LeanStudio.App/Views/MainWindow.axaml @@ -56,6 +56,7 @@ + @@ -122,6 +123,8 @@ + + @@ -129,6 +132,16 @@ + + + + + + + + + + diff --git a/src/LeanStudio.App/Views/MainWindow.axaml.cs b/src/LeanStudio.App/Views/MainWindow.axaml.cs index c57c3a6..802e76f 100644 --- a/src/LeanStudio.App/Views/MainWindow.axaml.cs +++ b/src/LeanStudio.App/Views/MainWindow.axaml.cs @@ -1079,6 +1079,18 @@ 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: 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)); + 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)); 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)); @@ -1176,6 +1188,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/Git/SorryHistory.cs b/src/LeanStudio.Core/Git/SorryHistory.cs new file mode 100644 index 0000000..0c28393 --- /dev/null +++ b/src/LeanStudio.Core/Git/SorryHistory.cs @@ -0,0 +1,104 @@ +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(); + // -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", "-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; + } + + /// 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.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.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.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/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.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/src/LeanStudio.Core/Workflow/MathlibConventions.cs b/src/LeanStudio.Core/Workflow/MathlibConventions.cs new file mode 100644 index 0000000..9da913e --- /dev/null +++ b/src/LeanStudio.Core/Workflow/MathlibConventions.cs @@ -0,0 +1,73 @@ +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) 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. + 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 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) + { + 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.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.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.Core/Workflow/StyleCheck.cs b/src/LeanStudio.Core/Workflow/StyleCheck.cs new file mode 100644 index 0000000..a3290dc --- /dev/null +++ b/src/LeanStudio.Core/Workflow/StyleCheck.cs @@ -0,0 +1,158 @@ +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"; + } + + /// + /// 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.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.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/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/src/LeanStudio.Mcp/LeanTools.cs b/src/LeanStudio.Mcp/LeanTools.cs index 48c6492..788e03a 100644 --- a/src/LeanStudio.Mcp/LeanTools.cs +++ b/src/LeanStudio.Mcp/LeanTools.cs @@ -695,6 +695,188 @@ 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. 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), + ("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); + string text = await File.ReadAllTextAsync(path, ct); + bool conventions = OptBool(a, "mathlib") ?? bench.ProjectFor(path).DependsOnMathlib; + 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"; + } + 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) + { + 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"); + } + 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("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("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("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("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("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("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 new file mode 100644 index 0000000..169f9a6 --- /dev/null +++ b/tests/LeanStudio.Tests/PickerAndConflictTests.cs @@ -0,0 +1,726 @@ +using LeanStudio.Core.Editing; +using LeanStudio.Core.Git; +using LeanStudio.Core.Proofs; +using LeanStudio.Core.Workflow; + +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))); + } +} + +/// 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("")); + } +} + +/// 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(); + } + + 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()); + 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); + 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 + + 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 })); + 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, "-- " + 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); + await Call("stale_deprecations", new() { ["path"] = file, ["apply"] = true }); + Assert.Equal("def new := 1\n", await File.ReadAllTextAsync(file, TestContext.Current.CancellationToken)); + } + finally + { + Directory.Delete(dir, true); + } + } +} + +/// 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 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() + { + 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")); + } +} + +/// 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)); + } +} + +/// 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"); + } +} + +/// 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); + } +} + +/// 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")); + } +} + +/// 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")); + } +} + +/// 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); + } + } +} + +/// 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); + } + } +} + +/// 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); + } + } +} + +/// 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); + } + } +} 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() { 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"