From a70cfd7544f8e1461aa20dbe8353d10ab0751c23 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 5 Oct 2026 03:45:06 +0000 Subject: [PATCH 1/3] feat(Linter): check import formatting in modified files --- .github/workflows/build_template.yml | 29 ++++++++++++ Mathlib/Tactic/Linter/TextBased.lean | 71 ++++++++++++++++++++++++++-- MathlibTest/Linter/TextBased.lean | 24 ++++++++++ docs/workflows.md | 2 +- scripts/README.md | 4 +- scripts/lint-style.lean | 19 ++++++-- 6 files changed, 137 insertions(+), 12 deletions(-) diff --git a/.github/workflows/build_template.yml b/.github/workflows/build_template.yml index efa405999c1ea0..0c8ace39e4f3f0 100644 --- a/.github/workflows/build_template.yml +++ b/.github/workflows/build_template.yml @@ -1022,6 +1022,35 @@ jobs: lint-bib-file: true ref: ${{ inputs.pr_branch_ref }} + # Import grouping has many pre-existing violations, so enforce it only in files changed from + # the repository's default branch. A separate cleanup PR can normalize the existing files. + - name: Check import formatting in modified Mathlib files + env: + BASE_BRANCH: ${{ github.event.repository.default_branch }} + shell: bash + run: | + base_ref="refs/remotes/origin/${BASE_BRANCH}" + refspec="+refs/heads/${BASE_BRANCH}:${base_ref}" + git fetch --no-tags origin "${refspec}" + if ! merge_base="$(git merge-base "origin/${BASE_BRANCH}" HEAD)"; then + # `lint-style-action` uses a shallow checkout. Usually fetching the base branch gives + # `merge-base` enough history; deepen only when the branch point is older. + git fetch --no-tags --unshallow origin "${refspec}" + merge_base="$(git merge-base "origin/${BASE_BRANCH}" HEAD)" + fi + + modules=() + while IFS= read -r -d '' file; do + if [[ "${file}" == Mathlib/*.lean ]]; then + module="${file%.lean}" + modules+=("${module//\//.}") + fi + done < <(git diff --name-only -z --diff-filter=ACMR "${merge_base}"...HEAD -- Mathlib) + + if (( ${#modules[@]} > 0 )); then + lake exe lint-style --imports --only "${modules[@]}" + fi + final: name: Post-CI job # ensure that this runs iff direct dependencies succeeded even if transitive dependencies were skipped diff --git a/Mathlib/Tactic/Linter/TextBased.lean b/Mathlib/Tactic/Linter/TextBased.lean index 8ca2d2e6a408b6..051b1271d75527 100644 --- a/Mathlib/Tactic/Linter/TextBased.lean +++ b/Mathlib/Tactic/Linter/TextBased.lean @@ -5,6 +5,8 @@ Authors: Michael Rothgang, Jon Eugster, Adomas Baliuka -/ module +public meta import ImportGraph.Imports.Pretty +public meta import ImportGraph.Lean.Syntax public meta import Lake.Util.Casing public import Mathlib.Data.Nat.Notation public meta import Mathlib.Tactic.Linter.TextBased.UnicodeLinter @@ -32,6 +34,7 @@ Currently, this file contains linters checking `!`, `.` or spaces. - for any code containing unicode characters not on the allowlist - for incorrect usage of unicode variant selectors +- for incorrectly grouped public and private imports This linter has a file for style exceptions (to avoid false positives in the implementation), or for downstream projects to allow a gradual adoption of this linter. @@ -62,6 +65,8 @@ inductive StyleError where * `selector` is the desired selector or `none` -/ | unicodeVariant (s : String) (selector: Option Char) + /-- Public and private imports are not grouped as prescribed by the style guide. -/ + | importFormatting deriving BEq, Inhabited /-- How to format style errors -/ @@ -115,6 +120,8 @@ def StyleError.errorMessage (err : StyleError) : String := match err with | _, _ => s!"Unexpected unicode variant selector: \"{s}\" ({oldHex}). \ Consider deleting it." + | importFormatting => + "Public imports must precede private imports, with a blank line between the two groups" /-- The error code for a given style error. Keep this in sync with `parse?_errorContext` below! -/ -- The error codes were chosen like this for historic reasons. In principle, we could also print @@ -126,6 +133,7 @@ def StyleError.errorCode (err : StyleError) : String := match err with | StyleError.semicolon => "ERR_SEM" | StyleError.unwantedUnicode _ => "ERR_UNICODE" | StyleError.unicodeVariant _ _ => "ERR_UNICODE_VARIANT" + | StyleError.importFormatting => "ERR_IMPORTS" /-- Context for a style error: the actual error, the line number in the file we're reading @@ -238,6 +246,7 @@ def parse?_errorContext (line : String) : Option ErrorContext := Id.run do let offending := removeQuotations (← errorMessage[4]?) StyleError.unicodeVariant offending none | _ => none + | "ERR_IMPORTS" => some StyleError.importFormatting | _ => none match String.toNat? lineNumber with | some n => err.map fun e ↦ (ErrorContext.mk e n path) @@ -268,6 +277,50 @@ also return the collection of all lines, changed as needed to fix the linter err abbrev TextbasedLinter := LinterOptions → Array String → Array (StyleError × ℕ) × (Option (Array String)) +/-- Check that ordinary public imports precede ordinary private imports, with a blank line between +the two groups. -/ +public register_option linter.importFormatting : Bool := { defValue := false } + +/-- Check whether ordinary `public import` and `import` declarations in a module are grouped in +that order and separated by one blank line. If not, return an automatically formatted source file. + +This deliberately leaves files containing `meta import` or `import all` alone: the style guide does +not prescribe where those less common forms belong. The formatter uses the same parsed import and +whitespace representation as `#norm_imports`, while retaining the order within each group and not +removing redundant imports. -/ +def formatImports (source fileName : String) : IO (Option (ℕ × String)) := do + let inputCtx := Lean.Parser.mkInputContext source fileName + let (header, _, log) ← Lean.Parser.parseHeader inputCtx + if log.hasErrors || (ImportGraph.Lean.getModule header).isNone then + return none + let sourceImports := ImportGraph.headerToImportRefsWithWhitespace header + if sourceImports.isEmpty || sourceImports.any fun imp ↦ imp.1.isMeta || imp.1.importAll then + return none + let publicImports := sourceImports.filter fun imp ↦ imp.1.isExported + let privateImports := sourceImports.filter fun imp ↦ !imp.1.isExported + if publicImports.isEmpty || privateImports.isEmpty then + return none + let formatGroup (imports : Array (ImportGraph.Lean.ImportRef × + ImportGraph.Lean.Import.Whitespace)) : String := + let imports := imports.map fun imp ↦ (imp.1.toImport, imp.2) + (ImportGraph.Lean.Import.prettyWithWhitespace imports .none).pretty + let formatted := s!"{formatGroup publicImports}\n\n{formatGroup privateImports}" + let importsStx := Lean.mkNullNode (sourceImports.map fun imp ↦ imp.1.stx.raw) + let some startPos := importsStx.getLeadingPos? | return none + let some stopPos := importsStx.getTrailingTailPos? | return none + let sourceSubstring : Substring.Raw := { str := source, startPos, stopPos } + let (sourceSubstring, formatted) := + if let some sourceSubstring := sourceSubstring.dropPrefix? "\n\n".toRawSubstring then + (sourceSubstring, formatted) + else + (sourceSubstring, s!"\n\n{formatted}") + if sourceSubstring.toString == formatted then + return none + let fixed := String.Pos.Raw.extract source 0 sourceSubstring.startPos ++ formatted ++ + String.Pos.Raw.extract source sourceSubstring.stopPos source.rawEndPos + let lineNumber := (inputCtx.fileMap.toPosition sourceSubstring.startPos).line + 1 + return some (lineNumber, fixed) + /-! Definitions of the actual text-based linters. -/ section @@ -454,15 +507,23 @@ def lintFile (opts : LinterOptions) (path : FilePath) (exceptions : Array ErrorC changes_made := true errors := errors.push (ErrorContext.mk StyleError.windowsLineEnding 1 path) let lines := (replaced.splitOn "\n").toArray + -- A working copy of the lines in this file, modified by applying the auto-fixes. + let mut changed := lines + + if getLinterValue linter.importFormatting opts then + if let some (lineNumber, fixed) ← formatImports replaced path.toString then + let error := ErrorContext.mk StyleError.importFormatting lineNumber path + if error.find?_comparable exceptions |>.isNone then + errors := errors.push error + changed := (fixed.splitOn "\n").toArray + changes_made := true -- We don't need to run any further checks on imports-only files. - if isImportsOnlyFile lines then - return (errors, if changes_made then some lines else none) + if isImportsOnlyFile changed then + return (errors, if changes_made then some changed else none) -- All further style errors raised in this file. let mut allOutput := #[] - -- A working copy of the lines in this file, modified by applying the auto-fixes. - let mut changed := lines for lint in allLinters do let (new_errors, changes) := lint opts changed @@ -525,7 +586,7 @@ def lintModules (opts : LinterOptions) (nolints : Array String) (moduleNames : A formatErrors allUnexpectedErrors style if allUnexpectedErrors.size > 0 then IO.eprintln s!"error: found {allUnexpectedErrors.size} new style error(s)! \ - Try `lake exe lint-style --fix` to apply automatic fixes." + Rerun this command with `--fix` to apply automatic fixes." return numberErrorFiles /-- Verify that all modules are named in `UpperCamelCase` -/ diff --git a/MathlibTest/Linter/TextBased.lean b/MathlibTest/Linter/TextBased.lean index b4373f7b4314cf..990c1efca4c2be 100644 --- a/MathlibTest/Linter/TextBased.lean +++ b/MathlibTest/Linter/TextBased.lean @@ -660,6 +660,26 @@ section unicodeLinter open Mathlib.Linter.TextBased open Mathlib.Linter.TextBased.UnicodeLinter +set_option linter.unusedTactic false in +example : True := by + run_tac do + let source := "module\n\nimport B\npublic import C\npublic import A\nimport D\n\n#check Nat\n" + let expected := + "module\n\npublic import C\npublic import A\n\nimport B\nimport D\n\n#check Nat\n" + let some (_, actual) ← formatImports source "Test.lean" + | throwError "Expected import formatting to change" + unless actual == expected do + throwError "Unexpected import formatting output:\n{actual}" + + let source := "module\n\npublic import A\n\nimport B\n\n#check Nat\n" + unless (← formatImports source "Test.lean").isNone do + throwError "Correctly grouped imports should be left unchanged" + + let source := "module\n\nimport B\npublic meta import C\npublic import A\n\n#check Nat\n" + unless (← formatImports source "Test.lean").isNone do + throwError "Import formatting should not prescribe the position of meta imports" + trivial + /- A character either does or doesn't have an abbreviation in the VSCode extension. -/ #guard withVSCodeAbbrev.toList ∩ othersInMathlib.toList = ∅ @@ -797,6 +817,10 @@ meta def ErrorContext.isValid_parse?_error_context (ec : ErrorContext) : Bool := error := .semicolon, lineNumber := 1234, path := "Mathlib/Tactic/Measurability/Init.lean"} +#guard ErrorContext.isValid_parse?_error_context { + error := .importFormatting, + lineNumber := 1234, path := "Mathlib/Tactic/Measurability/Init.lean"} + #guard ErrorContext.isValid_parse?_error_context { error := .unwantedUnicode '\u1234', lineNumber := 1234, path:="./MYFILE.lean"} diff --git a/docs/workflows.md b/docs/workflows.md index be32538ce425f5..07751b3edf7f24 100644 --- a/docs/workflows.md +++ b/docs/workflows.md @@ -36,7 +36,7 @@ This is an overview of the most important triggers used by Mathlib CI. For a com ### The main CI pipelines above all use this reusable workflow for the base logic: | File | Description | |---|---| -| [`build_template.yml`](../.github/workflows/build_template.yml) | Reusable CI workflow (`workflow_call`) that performs Lean setup, build/test/lint steps, cache/artifact handling, and reporting. | +| [`build_template.yml`](../.github/workflows/build_template.yml) | Reusable CI workflow (`workflow_call`) that performs Lean setup, build/test/lint steps, changed-file import-formatting checks, cache/artifact handling, and reporting. | ## Pull requests diff --git a/scripts/README.md b/scripts/README.md index b070aade93ecba..25d72310cc1cd2 100644 --- a/scripts/README.md +++ b/scripts/README.md @@ -227,7 +227,9 @@ to module `Foo.Bar` (no `srcDir` indirection). - `mk_all.lean` run via `lake exe mk_all`, regenerates the import-only files `Mathlib.lean`, `Mathlib/Tactic.lean`, `Archive.lean` and `Counterexamples.lean` -- `lint-style.lean`: style linters written in Lean. Run via `lake exe lint-style`. +- `lint-style.lean`: style linters written in Lean. Run via `lake exe lint-style`. Pass `--imports` + to check public/private import grouping, `--only` to avoid traversing the named modules' imports, + and `--fix` to apply available fixes. - `check_title_labels.lean` verifies that a (non-WIP, non-draft) PR has a well-formed title. In the future, it may also check that a feature PR has a topic label. - `lint-bib.sh` diff --git a/scripts/lint-style.lean b/scripts/lint-style.lean index fc6abe212be7b5..666f0a54e65ef5 100644 --- a/scripts/lint-style.lean +++ b/scripts/lint-style.lean @@ -193,6 +193,10 @@ def lintStyleCli (args : Cli.Parsed) : IO UInt32 := do toOptions := ← getLakefileLeanOptions, linterSets := linter_sets%, } + let opts := if args.hasFlag "imports" then + { opts with toOptions := opts.toOptions.setBool `linter.importFormatting true } + else + opts let style : ErrorFormat := match args.hasFlag "github" with | true => ErrorFormat.github @@ -250,11 +254,14 @@ def lintStyleCli (args : Cli.Parsed) : IO UInt32 := do let pkgs := originModules.map (·.components.head!) Lean.initSearchPath (← Lean.findSysroot) let searchPath ← Lean.getSrcSearchPath - let allModuleNames ← originModules.flatMapM fun mod => do - let some file ← searchPath.findWithExt "lean" mod - | throw <| IO.userError s!"could not find module with name {mod}" - let imports := (← file.parseImports').filterInit.imports.map (·.module) - pure <| imports.filter (·.components.head! ∈ pkgs) + let allModuleNames ← if args.hasFlag "only" then + pure originModules + else + originModules.flatMapM fun mod => do + let some file ← searchPath.findWithExt "lean" mod + | throw <| IO.userError s!"could not find module with name {mod}" + let imports := (← file.parseImports').filterInit.imports.map (·.module) + pure <| imports.filter (·.components.head! ∈ pkgs) -- Read the `nolints` file, with manual exceptions for the linter. -- NB. We pass these lints to `lintModules` explicitly to prevent cache invalidation bugs: @@ -290,6 +297,8 @@ def lintStyle : Cmd := `[Cli| github; "Print errors in a format suitable for github problem matchers\n\ otherwise, produce human-readable output" fix; "Automatically fix the style error, if possible" + imports; "Check the formatting of public and private import groups" + only; "Lint only the named modules, rather than their transitive imports" ARGS: ...modules : String; "Which modules, and their imports, will be linted.\n\ From d383ec2e64a92a383c81a6bbc14aeaf227be3d64 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 5 Oct 2026 04:11:54 +0000 Subject: [PATCH 2/3] fix(Linter): handle import modifiers and share formatting code --- .github/workflows/build_template.yml | 11 +++- Mathlib/Tactic/Linter/TextBased.lean | 78 +++++++++++++--------------- MathlibTest/Linter/TextBased.lean | 32 +++++++++--- lake-manifest.json | 2 +- 4 files changed, 73 insertions(+), 50 deletions(-) diff --git a/.github/workflows/build_template.yml b/.github/workflows/build_template.yml index 0c8ace39e4f3f0..e6bfabfc4809d1 100644 --- a/.github/workflows/build_template.yml +++ b/.github/workflows/build_template.yml @@ -1039,16 +1039,23 @@ jobs: merge_base="$(git merge-base "origin/${BASE_BRANCH}" HEAD)" fi + changed_files="${RUNNER_TEMP}/import-style-changed-files" + git diff --name-only -z --diff-filter=ACMR "${merge_base}"...HEAD -- Mathlib \ + > "${changed_files}" + modules=() while IFS= read -r -d '' file; do if [[ "${file}" == Mathlib/*.lean ]]; then module="${file%.lean}" modules+=("${module//\//.}") fi - done < <(git diff --name-only -z --diff-filter=ACMR "${merge_base}"...HEAD -- Mathlib) + done < "${changed_files}" if (( ${#modules[@]} > 0 )); then - lake exe lint-style --imports --only "${modules[@]}" + printf 'Fix with: lake exe lint-style --imports --fix --only' + printf ' %q' "${modules[@]}" + printf '\n' + lake exe lint-style --github --imports --only "${modules[@]}" fi final: diff --git a/Mathlib/Tactic/Linter/TextBased.lean b/Mathlib/Tactic/Linter/TextBased.lean index 051b1271d75527..96b2b931c97571 100644 --- a/Mathlib/Tactic/Linter/TextBased.lean +++ b/Mathlib/Tactic/Linter/TextBased.lean @@ -277,48 +277,39 @@ also return the collection of all lines, changed as needed to fix the linter err abbrev TextbasedLinter := LinterOptions → Array String → Array (StyleError × ℕ) × (Option (Array String)) -/-- Check that ordinary public imports precede ordinary private imports, with a blank line between -the two groups. -/ +/-- Check that public imports precede private imports, with a blank line between the two groups. -/ public register_option linter.importFormatting : Bool := { defValue := false } -/-- Check whether ordinary `public import` and `import` declarations in a module are grouped in -that order and separated by one blank line. If not, return an automatically formatted source file. +/-- Check whether `public import` and private `import` declarations in a module are grouped in that +order and separated by one blank line. The `meta` and `all` modifiers are ignored when determining +the group. If needed, return an automatically formatted source file when it is safe to do so. -This deliberately leaves files containing `meta import` or `import all` alone: the style guide does -not prescribe where those less common forms belong. The formatter uses the same parsed import and -whitespace representation as `#norm_imports`, while retaining the order within each group and not -removing redundant imports. -/ +The formatter uses the source-editing and parsed import/whitespace machinery behind +`#norm_imports`, while retaining the order within each group and not removing redundant imports. -/ def formatImports (source fileName : String) : IO (Option (ℕ × String)) := do let inputCtx := Lean.Parser.mkInputContext source fileName let (header, _, log) ← Lean.Parser.parseHeader inputCtx if log.hasErrors || (ImportGraph.Lean.getModule header).isNone then return none let sourceImports := ImportGraph.headerToImportRefsWithWhitespace header - if sourceImports.isEmpty || sourceImports.any fun imp ↦ imp.1.isMeta || imp.1.importAll then + if !sourceImports.any (·.1.isExported) || !sourceImports.any (!·.1.isExported) then return none - let publicImports := sourceImports.filter fun imp ↦ imp.1.isExported - let privateImports := sourceImports.filter fun imp ↦ !imp.1.isExported - if publicImports.isEmpty || privateImports.isEmpty then - return none - let formatGroup (imports : Array (ImportGraph.Lean.ImportRef × - ImportGraph.Lean.Import.Whitespace)) : String := - let imports := imports.map fun imp ↦ (imp.1.toImport, imp.2) - (ImportGraph.Lean.Import.prettyWithWhitespace imports .none).pretty - let formatted := s!"{formatGroup publicImports}\n\n{formatGroup privateImports}" - let importsStx := Lean.mkNullNode (sourceImports.map fun imp ↦ imp.1.stx.raw) - let some startPos := importsStx.getLeadingPos? | return none - let some stopPos := importsStx.getTrailingTailPos? | return none - let sourceSubstring : Substring.Raw := { str := source, startPos, stopPos } - let (sourceSubstring, formatted) := - if let some sourceSubstring := sourceSubstring.dropPrefix? "\n\n".toRawSubstring then - (sourceSubstring, formatted) - else - (sourceSubstring, s!"\n\n{formatted}") - if sourceSubstring.toString == formatted then - return none - let fixed := String.Pos.Raw.extract source 0 sourceSubstring.startPos ++ formatted ++ - String.Pos.Raw.extract source sourceSubstring.stopPos source.rawEndPos - let lineNumber := (inputCtx.fileMap.toPosition sourceSubstring.startPos).line + 1 + let imports := sourceImports.map fun imp ↦ (imp.1.toImport, imp.2) + let formatted := ImportGraph.Lean.Import.prettyWithWhitespaceGroupedByVisibility imports + let some edit := ImportGraph.Lean.Import.mkImportBlockEdit source sourceImports formatted + | return none + let fixed := edit.apply source + let lineNumber := (inputCtx.fileMap.toPosition edit.startPos).line + -- Refuse unsafe automatic edits, for example when a multi-line block comment cannot be carried + -- with its import by the whitespace representation. Returning the original source still makes + -- the linter report the violation. + let (fixedHeader, _, fixedLog) ← Lean.Parser.parseHeader <| + Lean.Parser.mkInputContext fixed fileName + let expectedImports := (sourceImports.filter (·.1.isExported) ++ + sourceImports.filter (!·.1.isExported)).map (·.1.toImport) + let actualImports := (ImportGraph.Lean.headerToImportRefs fixedHeader).map (·.toImport) + if fixedLog.hasErrors || actualImports != expectedImports then + return some (lineNumber, source) return some (lineNumber, fixed) /-! Definitions of the actual text-based linters. -/ @@ -510,14 +501,6 @@ def lintFile (opts : LinterOptions) (path : FilePath) (exceptions : Array ErrorC -- A working copy of the lines in this file, modified by applying the auto-fixes. let mut changed := lines - if getLinterValue linter.importFormatting opts then - if let some (lineNumber, fixed) ← formatImports replaced path.toString then - let error := ErrorContext.mk StyleError.importFormatting lineNumber path - if error.find?_comparable exceptions |>.isNone then - errors := errors.push error - changed := (fixed.splitOn "\n").toArray - changes_made := true - -- We don't need to run any further checks on imports-only files. if isImportsOnlyFile changed then return (errors, if changes_made then some changed else none) @@ -555,6 +538,19 @@ def lintFile (opts : LinterOptions) (path : FilePath) (exceptions : Array ErrorC -- Filter exceptions. Note: This list is not sorted. For github, this is fine. errors := errors.append (allOutput.flatten.filter (fun e ↦ (e.find?_comparable exceptions).isNone)) + + -- Apply import formatting after the line-based linters. This keeps their reported line numbers + -- tied to the source on disk even when regrouping imports adds or removes blank lines. + if getLinterValue linter.importFormatting opts then + let changedSource := "\n".intercalate changed.toList + if let some (lineNumber, fixed) ← formatImports changedSource path.toString then + let error := ErrorContext.mk StyleError.importFormatting lineNumber path + if error.find?_comparable exceptions |>.isNone then + errors := errors.push error + let fixedLines := (fixed.splitOn "\n").toArray + if fixedLines != changed then + changed := fixedLines + changes_made := true return (errors, if changes_made then some changed else none) /-- Lint a collection of modules for style violations. @@ -586,7 +582,7 @@ def lintModules (opts : LinterOptions) (nolints : Array String) (moduleNames : A formatErrors allUnexpectedErrors style if allUnexpectedErrors.size > 0 then IO.eprintln s!"error: found {allUnexpectedErrors.size} new style error(s)! \ - Rerun this command with `--fix` to apply automatic fixes." + Rerun `lake exe lint-style` with `--fix` to apply automatic fixes." return numberErrorFiles /-- Verify that all modules are named in `UpperCamelCase` -/ diff --git a/MathlibTest/Linter/TextBased.lean b/MathlibTest/Linter/TextBased.lean index 990c1efca4c2be..9df718ab2a82de 100644 --- a/MathlibTest/Linter/TextBased.lean +++ b/MathlibTest/Linter/TextBased.lean @@ -655,10 +655,10 @@ end showLinter /-! Tests for linters defined in `TextBased.lean`. -/ section textBased -section unicodeLinter open Mathlib.Linter.TextBased -open Mathlib.Linter.TextBased.UnicodeLinter + +section importFormatting set_option linter.unusedTactic false in example : True := by @@ -666,8 +666,10 @@ example : True := by let source := "module\n\nimport B\npublic import C\npublic import A\nimport D\n\n#check Nat\n" let expected := "module\n\npublic import C\npublic import A\n\nimport B\nimport D\n\n#check Nat\n" - let some (_, actual) ← formatImports source "Test.lean" + let some (lineNumber, actual) ← formatImports source "Test.lean" | throwError "Expected import formatting to change" + unless lineNumber == 3 do + throwError "Expected the import error on line 3, got line {lineNumber}" unless actual == expected do throwError "Unexpected import formatting output:\n{actual}" @@ -675,11 +677,29 @@ example : True := by unless (← formatImports source "Test.lean").isNone do throwError "Correctly grouped imports should be left unchanged" - let source := "module\n\nimport B\npublic meta import C\npublic import A\n\n#check Nat\n" - unless (← formatImports source "Test.lean").isNone do - throwError "Import formatting should not prescribe the position of meta imports" + let source := "module\n\nimport B\npublic meta import C\nimport all D\n" ++ + "public import A\n\n#check Nat\n" + let expected := "module\n\npublic meta import C\npublic import A\n\nimport B\n" ++ + "import all D\n\n#check Nat\n" + let some (_, actual) ← formatImports source "Test.lean" + | throwError "Expected meta and all imports to be grouped by visibility" + unless actual == expected do + throwError "Unexpected formatting with meta and all imports:\n{actual}" + + let source := "module\n\nimport B /- trailing\ncontinued -/\n" ++ + "public import A\n\n#check Nat\n" + let some (_, actual) ← formatImports source "Test.lean" + | throwError "Expected unsafe import formatting to still be reported" + unless actual == source do + throwError "Unsafe import formatting should be reported without an automatic fix" trivial +end importFormatting + +section unicodeLinter + +open Mathlib.Linter.TextBased.UnicodeLinter + /- A character either does or doesn't have an abbreviation in the VSCode extension. -/ #guard withVSCodeAbbrev.toList ∩ othersInMathlib.toList = ∅ diff --git a/lake-manifest.json b/lake-manifest.json index b9f0149ca488ea..5f4b5c21a3d218 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "7ad9f2e325aa6cec3dacaa97c2653a98032750eb", + "rev": "8d28ba6feadfe3f695379ea0125aa560eafe3c7b", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", From 7316203f16a2762d5c37e0d542ca1f5c6e769d83 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 5 Oct 2026 07:37:34 +0000 Subject: [PATCH 3/3] chore: include merged ImportGraph sorting fix --- lake-manifest.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lake-manifest.json b/lake-manifest.json index 5f4b5c21a3d218..acff4415844ab2 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "8d28ba6feadfe3f695379ea0125aa560eafe3c7b", + "rev": "7d55631b042cb7d24f67f83a8a4b7c7b588a4e9b", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main",