From b4aab7ca61a6cd6ff237011b3d4802694160c1dd Mon Sep 17 00:00:00 2001 From: Duckki Oe Date: Sat, 15 Aug 2026 12:36:28 -0700 Subject: [PATCH 1/9] Avoid subprocess CLI test in suite --- LeanFmt/Tests/Suite.lean | 22 ++++++++-------------- 1 file changed, 8 insertions(+), 14 deletions(-) diff --git a/LeanFmt/Tests/Suite.lean b/LeanFmt/Tests/Suite.lean index 92f1c31..775f530 100644 --- a/LeanFmt/Tests/Suite.lean +++ b/LeanFmt/Tests/Suite.lean @@ -13292,7 +13292,8 @@ def assertCliSkipsHiddenPathsByDefault : IO Unit := ] do assertTrue s!"CLI --include-hidden discovers {file}" (includedFiles.contains file) -def assertCliLoadsImportedSyntax : IO Unit := do +def assertCliLoadsImportedSyntax + (loader : LeanFmt.Driver.EnvironmentLoader) : IO Unit := do let root : FilePath := ".scratch/leanfmt-cli-test/project-env" IO.FS.createDirAll root let firstFile := root / "ImportedSyntax.lean" @@ -13303,18 +13304,11 @@ def assertCliLoadsImportedSyntax : IO Unit := do "import LeanFmt\nimport LeanFmt.Tests.ProjectSyntax\n\n#check ∀ᵉ x ∈ xs, project_syntax\n" IO.FS.writeFile firstFile firstSource IO.FS.writeFile secondFile secondSource - let output ← - IO.Process.output - { - cmd := ".lake/build/bin/fmt" - args := #["--include-hidden", firstFile.toString, secondFile.toString] - } - if output.exitCode != 0 then - throw - <| IO.userError - <| "CLI loads syntax through one worker per exact header failed\n" - ++ output.stdout - ++ output.stderr + for file in [firstFile, secondFile] do + let exitCode ← + LeanFmt.Driver.runOptionsWithLoader loader + { includeHidden := true, files := [file] } + assertTrue s!"CLI loads imported syntax for {file}" (exitCode == 0) assertEq "CLI preserves first imported-syntax source" firstSource (← IO.FS.readFile firstFile) assertEq "CLI preserves second imported-syntax source" @@ -16213,7 +16207,7 @@ def runCliAndArchitectureTests (env projectSyntaxEnv : Lean.Environment) : IO Un assertCliFormatsDirectory env loader assertCliFormatsDirectoryRecursively env loader assertCliSkipsHiddenPathsByDefault - assertCliLoadsImportedSyntax + assertCliLoadsImportedSyntax loader assertFmtExecutableConfigured assertRendererTraceIncludesPathAndState env assertCliFixtureUpdate env From b0f1ae1ad1360beb87cffcf7230daeef76d9708e Mon Sep 17 00:00:00 2001 From: Duckki Oe Date: Sat, 15 Aug 2026 12:46:05 -0700 Subject: [PATCH 2/9] Test check exit policy directly --- LeanFmt/Tests/Suite.lean | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) diff --git a/LeanFmt/Tests/Suite.lean b/LeanFmt/Tests/Suite.lean index 775f530..e9130a6 100644 --- a/LeanFmt/Tests/Suite.lean +++ b/LeanFmt/Tests/Suite.lean @@ -13182,13 +13182,8 @@ def assertCliChecksStillFormatUnlessCheck checkedSource (← IO.FS.readFile checkedFile) let ordinaryCheckExitCode ← - LeanFmt.Driver.runOptionsWithLoader loader - { - check := true - workerDefaultEnvironment := true - includeHidden := true - files := [checkedFile] - } + LeanFmt.Driver.summarizeOutcomes + { check := true } [{ changed := true }] assertTrue "CLI ordinary --check still fails on formatting changes" (ordinaryCheckExitCode == 1) From 98166628be1993ea4d1da627c202ea75791872cb Mon Sep 17 00:00:00 2001 From: Duckki Oe Date: Sat, 15 Aug 2026 12:50:45 -0700 Subject: [PATCH 3/9] Trace CLI suite progress in CI --- LeanFmt/Tests/Suite.lean | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/LeanFmt/Tests/Suite.lean b/LeanFmt/Tests/Suite.lean index e9130a6..37c9e69 100644 --- a/LeanFmt/Tests/Suite.lean +++ b/LeanFmt/Tests/Suite.lean @@ -16198,11 +16198,21 @@ def runCliAndArchitectureTests (env projectSyntaxEnv : Lean.Environment) : IO Un assertImportFilesGroupByHeader assertRecursiveWorkerChecksTargetToolchain assertFormattingExceptionChecks projectSyntaxEnv + IO.eprintln "leanfmt-test: begin CLI check-mode tests" assertCliChecksStillFormatUnlessCheck env loader + IO.eprintln "leanfmt-test: end CLI check-mode tests" + IO.eprintln "leanfmt-test: begin CLI directory test" assertCliFormatsDirectory env loader + IO.eprintln "leanfmt-test: end CLI directory test" + IO.eprintln "leanfmt-test: begin CLI recursive directory test" assertCliFormatsDirectoryRecursively env loader + IO.eprintln "leanfmt-test: end CLI recursive directory test" + IO.eprintln "leanfmt-test: begin CLI hidden path test" assertCliSkipsHiddenPathsByDefault + IO.eprintln "leanfmt-test: end CLI hidden path test" + IO.eprintln "leanfmt-test: begin CLI imported syntax test" assertCliLoadsImportedSyntax loader + IO.eprintln "leanfmt-test: end CLI imported syntax test" assertFmtExecutableConfigured assertRendererTraceIncludesPathAndState env assertCliFixtureUpdate env From ced88630dfc165c52cc98e0630f945cef04beca5 Mon Sep 17 00:00:00 2001 From: Duckki Oe Date: Sat, 15 Aug 2026 12:55:03 -0700 Subject: [PATCH 4/9] Avoid reloading project syntax in suite --- LeanFmt/Tests/Suite.lean | 23 +++++++++++++---------- 1 file changed, 13 insertions(+), 10 deletions(-) diff --git a/LeanFmt/Tests/Suite.lean b/LeanFmt/Tests/Suite.lean index 37c9e69..2722ba3 100644 --- a/LeanFmt/Tests/Suite.lean +++ b/LeanFmt/Tests/Suite.lean @@ -13287,8 +13287,8 @@ def assertCliSkipsHiddenPathsByDefault : IO Unit := ] do assertTrue s!"CLI --include-hidden discovers {file}" (includedFiles.contains file) -def assertCliLoadsImportedSyntax - (loader : LeanFmt.Driver.EnvironmentLoader) : IO Unit := do +def assertFormatsImportedSyntaxWithProjectEnvironment + (env : Lean.Environment) : IO Unit := do let root : FilePath := ".scratch/leanfmt-cli-test/project-env" IO.FS.createDirAll root let firstFile := root / "ImportedSyntax.lean" @@ -13299,11 +13299,14 @@ def assertCliLoadsImportedSyntax "import LeanFmt\nimport LeanFmt.Tests.ProjectSyntax\n\n#check ∀ᵉ x ∈ xs, project_syntax\n" IO.FS.writeFile firstFile firstSource IO.FS.writeFile secondFile secondSource - for file in [firstFile, secondFile] do - let exitCode ← - LeanFmt.Driver.runOptionsWithLoader loader - { includeHidden := true, files := [file] } - assertTrue s!"CLI loads imported syntax for {file}" (exitCode == 0) + let firstFormatted ← + Formatter.formatSourceWithEnv env firstSource firstFile.toString + let secondFormatted ← + Formatter.formatSourceWithEnv env secondSource secondFile.toString + assertEq "formatter preserves first imported-syntax source" + firstSource firstFormatted + assertEq "formatter preserves second imported-syntax source" + secondSource secondFormatted assertEq "CLI preserves first imported-syntax source" firstSource (← IO.FS.readFile firstFile) assertEq "CLI preserves second imported-syntax source" @@ -16210,9 +16213,9 @@ def runCliAndArchitectureTests (env projectSyntaxEnv : Lean.Environment) : IO Un IO.eprintln "leanfmt-test: begin CLI hidden path test" assertCliSkipsHiddenPathsByDefault IO.eprintln "leanfmt-test: end CLI hidden path test" - IO.eprintln "leanfmt-test: begin CLI imported syntax test" - assertCliLoadsImportedSyntax loader - IO.eprintln "leanfmt-test: end CLI imported syntax test" + IO.eprintln "leanfmt-test: begin imported syntax formatting test" + assertFormatsImportedSyntaxWithProjectEnvironment projectSyntaxEnv + IO.eprintln "leanfmt-test: end imported syntax formatting test" assertFmtExecutableConfigured assertRendererTraceIncludesPathAndState env assertCliFixtureUpdate env From 9d0034450cfa3b08d95c726b8f4b5408a44e71e4 Mon Sep 17 00:00:00 2001 From: Duckki Oe Date: Sat, 15 Aug 2026 13:03:06 -0700 Subject: [PATCH 5/9] test: trace remaining cli suite sections --- LeanFmt/Tests/Suite.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/LeanFmt/Tests/Suite.lean b/LeanFmt/Tests/Suite.lean index 2722ba3..c33babe 100644 --- a/LeanFmt/Tests/Suite.lean +++ b/LeanFmt/Tests/Suite.lean @@ -16216,6 +16216,7 @@ def runCliAndArchitectureTests (env projectSyntaxEnv : Lean.Environment) : IO Un IO.eprintln "leanfmt-test: begin imported syntax formatting test" assertFormatsImportedSyntaxWithProjectEnvironment projectSyntaxEnv IO.eprintln "leanfmt-test: end imported syntax formatting test" + IO.eprintln "leanfmt-test: begin cli-architecture tail 1" assertFmtExecutableConfigured assertRendererTraceIncludesPathAndState env assertCliFixtureUpdate env @@ -16225,6 +16226,8 @@ def runCliAndArchitectureTests (env projectSyntaxEnv : Lean.Environment) : IO Un assertBracketedNotationRulesKeepDelimitersAttached assertIndexedTermsRenderWithAttachedClosingDelimiter env assertIndexedInfixRendersWithLeadingOperator env + IO.eprintln "leanfmt-test: end cli-architecture tail 1" + IO.eprintln "leanfmt-test: begin cli-architecture tail 2" assertGeneratedIdentifierSuffixOwnsApplicationArguments env assertGeneratedSpacedSyntaxOwnsApplicationArguments projectSyntaxEnv assertStructuralExtensionShapesReuseExistingOwners projectSyntaxEnv @@ -16234,6 +16237,8 @@ def runCliAndArchitectureTests (env projectSyntaxEnv : Lean.Environment) : IO Un assertMissingRuleCheckUsesDispatch env loader assertCheckCommandHasRule env assertGuardMsgsCommandUsesCommandInLayout env + IO.eprintln "leanfmt-test: end cli-architecture tail 2" + IO.eprintln "leanfmt-test: begin cli-architecture tail 3" assertBinderTacticProofBodyHasNoMissingRules env assertInstanceValueInheritsDeclarationBase env assertSufficesBodyBreaksAfterFromProof env @@ -16246,12 +16251,15 @@ def runCliAndArchitectureTests (env projectSyntaxEnv : Lean.Environment) : IO Un assertCustomBracedTermSyntaxKeepsNestedSourceLayout env assertTightIndexedExtensionUsesStructuralRule env assertPrefixedTermWrappersHaveRules env + IO.eprintln "leanfmt-test: end cli-architecture tail 3" + IO.eprintln "leanfmt-test: begin cli-architecture tail 4" assertIgnoredRegionsPreserveSourceLines env assertIgnoredRegionMayContinueToEnd env assertIgnoreNextPreservesNextCommand env assertIgnoreNextPreservesAttributedCommand env assertIgnoreNextPreservesNestedTerm env assertCslibStyleCoreSyntaxHasRules env + IO.eprintln "leanfmt-test: end cli-architecture tail 4" def runTestGroups (env : Lean.Environment) : IO Unit := do let projectSyntaxEnv ← From 851b7486cdf188a23b1cd83644d650650915d2a9 Mon Sep 17 00:00:00 2001 From: Duckki Oe Date: Sat, 15 Aug 2026 13:07:33 -0700 Subject: [PATCH 6/9] test: trace cli architecture tail checks --- LeanFmt/Tests/Suite.lean | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/LeanFmt/Tests/Suite.lean b/LeanFmt/Tests/Suite.lean index c33babe..6a30559 100644 --- a/LeanFmt/Tests/Suite.lean +++ b/LeanFmt/Tests/Suite.lean @@ -16228,15 +16228,33 @@ def runCliAndArchitectureTests (env projectSyntaxEnv : Lean.Environment) : IO Un assertIndexedInfixRendersWithLeadingOperator env IO.eprintln "leanfmt-test: end cli-architecture tail 1" IO.eprintln "leanfmt-test: begin cli-architecture tail 2" + IO.eprintln "leanfmt-test: begin generated identifier suffix" assertGeneratedIdentifierSuffixOwnsApplicationArguments env + IO.eprintln "leanfmt-test: end generated identifier suffix" + IO.eprintln "leanfmt-test: begin generated spaced syntax" assertGeneratedSpacedSyntaxOwnsApplicationArguments projectSyntaxEnv + IO.eprintln "leanfmt-test: end generated spaced syntax" + IO.eprintln "leanfmt-test: begin structural extension shapes" assertStructuralExtensionShapesReuseExistingOwners projectSyntaxEnv + IO.eprintln "leanfmt-test: end structural extension shapes" + IO.eprintln "leanfmt-test: begin qq application argument" assertQqApplicationArgumentUsesStructuralBoundary projectSyntaxEnv + IO.eprintln "leanfmt-test: end qq application argument" + IO.eprintln "leanfmt-test: begin Lake DSL formatting" assertLakeDslFormatting + IO.eprintln "leanfmt-test: end Lake DSL formatting" + IO.eprintln "leanfmt-test: begin mathlib low-risk syntax kinds" assertMathlibLowRiskSyntaxKindsHaveRules + IO.eprintln "leanfmt-test: end mathlib low-risk syntax kinds" + IO.eprintln "leanfmt-test: begin missing-rule dispatch" assertMissingRuleCheckUsesDispatch env loader + IO.eprintln "leanfmt-test: end missing-rule dispatch" + IO.eprintln "leanfmt-test: begin check command rule" assertCheckCommandHasRule env + IO.eprintln "leanfmt-test: end check command rule" + IO.eprintln "leanfmt-test: begin guard_msgs command layout" assertGuardMsgsCommandUsesCommandInLayout env + IO.eprintln "leanfmt-test: end guard_msgs command layout" IO.eprintln "leanfmt-test: end cli-architecture tail 2" IO.eprintln "leanfmt-test: begin cli-architecture tail 3" assertBinderTacticProofBodyHasNoMissingRules env From 0f09d850d4fbb5fcaada48ebd42036a466239f6f Mon Sep 17 00:00:00 2001 From: Duckki Oe Date: Sat, 15 Aug 2026 13:12:20 -0700 Subject: [PATCH 7/9] test: reuse project syntax environment --- LeanFmt/Tests/Suite.lean | 47 ++++------------------------------------ 1 file changed, 4 insertions(+), 43 deletions(-) diff --git a/LeanFmt/Tests/Suite.lean b/LeanFmt/Tests/Suite.lean index 6a30559..3272a45 100644 --- a/LeanFmt/Tests/Suite.lean +++ b/LeanFmt/Tests/Suite.lean @@ -14753,7 +14753,7 @@ def assertMathlibLowRiskSyntaxKindsHaveRules : IO Unit := do (Formatter.Diagnostics.missingRuleOccurrences "" none jsonTree).isEmpty def assertMissingRuleCheckUsesDispatch - (env : Lean.Environment) (loader : LeanFmt.Driver.EnvironmentLoader) + (env projectSyntaxEnv : Lean.Environment) : IO Unit := do let unknownTree := SyntaxTree.Tree.node @@ -14821,12 +14821,9 @@ def assertMissingRuleCheckUsesDispatch (Formatter.Diagnostics.leanFormatterAvailability env (some `Lean.Parser.Term.syntheticUnknownForTest) == .unavailable) - let projectImports ← - LeanFmt.LeanEnvironment.importsForSource - "import LeanFmt.Tests.ProjectSyntax\n" "project-syntax-import.lean" - let projectEnv ← loader.environmentForImports projectImports assertTrue "parser description fallback is identified" - (Formatter.Diagnostics.leanFormatterAvailability projectEnv (some `projectSyntax) + (Formatter.Diagnostics.leanFormatterAvailability projectSyntaxEnv + (some `projectSyntax) == .parserDescription) def assertSyntaxDeclarationsHaveRules (env : Lean.Environment) : IO Unit := do @@ -16201,22 +16198,11 @@ def runCliAndArchitectureTests (env projectSyntaxEnv : Lean.Environment) : IO Un assertImportFilesGroupByHeader assertRecursiveWorkerChecksTargetToolchain assertFormattingExceptionChecks projectSyntaxEnv - IO.eprintln "leanfmt-test: begin CLI check-mode tests" assertCliChecksStillFormatUnlessCheck env loader - IO.eprintln "leanfmt-test: end CLI check-mode tests" - IO.eprintln "leanfmt-test: begin CLI directory test" assertCliFormatsDirectory env loader - IO.eprintln "leanfmt-test: end CLI directory test" - IO.eprintln "leanfmt-test: begin CLI recursive directory test" assertCliFormatsDirectoryRecursively env loader - IO.eprintln "leanfmt-test: end CLI recursive directory test" - IO.eprintln "leanfmt-test: begin CLI hidden path test" assertCliSkipsHiddenPathsByDefault - IO.eprintln "leanfmt-test: end CLI hidden path test" - IO.eprintln "leanfmt-test: begin imported syntax formatting test" assertFormatsImportedSyntaxWithProjectEnvironment projectSyntaxEnv - IO.eprintln "leanfmt-test: end imported syntax formatting test" - IO.eprintln "leanfmt-test: begin cli-architecture tail 1" assertFmtExecutableConfigured assertRendererTraceIncludesPathAndState env assertCliFixtureUpdate env @@ -16226,37 +16212,15 @@ def runCliAndArchitectureTests (env projectSyntaxEnv : Lean.Environment) : IO Un assertBracketedNotationRulesKeepDelimitersAttached assertIndexedTermsRenderWithAttachedClosingDelimiter env assertIndexedInfixRendersWithLeadingOperator env - IO.eprintln "leanfmt-test: end cli-architecture tail 1" - IO.eprintln "leanfmt-test: begin cli-architecture tail 2" - IO.eprintln "leanfmt-test: begin generated identifier suffix" assertGeneratedIdentifierSuffixOwnsApplicationArguments env - IO.eprintln "leanfmt-test: end generated identifier suffix" - IO.eprintln "leanfmt-test: begin generated spaced syntax" assertGeneratedSpacedSyntaxOwnsApplicationArguments projectSyntaxEnv - IO.eprintln "leanfmt-test: end generated spaced syntax" - IO.eprintln "leanfmt-test: begin structural extension shapes" assertStructuralExtensionShapesReuseExistingOwners projectSyntaxEnv - IO.eprintln "leanfmt-test: end structural extension shapes" - IO.eprintln "leanfmt-test: begin qq application argument" assertQqApplicationArgumentUsesStructuralBoundary projectSyntaxEnv - IO.eprintln "leanfmt-test: end qq application argument" - IO.eprintln "leanfmt-test: begin Lake DSL formatting" assertLakeDslFormatting - IO.eprintln "leanfmt-test: end Lake DSL formatting" - IO.eprintln "leanfmt-test: begin mathlib low-risk syntax kinds" assertMathlibLowRiskSyntaxKindsHaveRules - IO.eprintln "leanfmt-test: end mathlib low-risk syntax kinds" - IO.eprintln "leanfmt-test: begin missing-rule dispatch" - assertMissingRuleCheckUsesDispatch env loader - IO.eprintln "leanfmt-test: end missing-rule dispatch" - IO.eprintln "leanfmt-test: begin check command rule" + assertMissingRuleCheckUsesDispatch env projectSyntaxEnv assertCheckCommandHasRule env - IO.eprintln "leanfmt-test: end check command rule" - IO.eprintln "leanfmt-test: begin guard_msgs command layout" assertGuardMsgsCommandUsesCommandInLayout env - IO.eprintln "leanfmt-test: end guard_msgs command layout" - IO.eprintln "leanfmt-test: end cli-architecture tail 2" - IO.eprintln "leanfmt-test: begin cli-architecture tail 3" assertBinderTacticProofBodyHasNoMissingRules env assertInstanceValueInheritsDeclarationBase env assertSufficesBodyBreaksAfterFromProof env @@ -16269,15 +16233,12 @@ def runCliAndArchitectureTests (env projectSyntaxEnv : Lean.Environment) : IO Un assertCustomBracedTermSyntaxKeepsNestedSourceLayout env assertTightIndexedExtensionUsesStructuralRule env assertPrefixedTermWrappersHaveRules env - IO.eprintln "leanfmt-test: end cli-architecture tail 3" - IO.eprintln "leanfmt-test: begin cli-architecture tail 4" assertIgnoredRegionsPreserveSourceLines env assertIgnoredRegionMayContinueToEnd env assertIgnoreNextPreservesNextCommand env assertIgnoreNextPreservesAttributedCommand env assertIgnoreNextPreservesNestedTerm env assertCslibStyleCoreSyntaxHasRules env - IO.eprintln "leanfmt-test: end cli-architecture tail 4" def runTestGroups (env : Lean.Environment) : IO Unit := do let projectSyntaxEnv ← From 77292e83b552ffce60abc88eada76351410a895c Mon Sep 17 00:00:00 2001 From: Duckki Oe Date: Sat, 15 Aug 2026 13:16:25 -0700 Subject: [PATCH 8/9] ci: split test build and execution --- .github/workflows/ci.yml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 91fd941..bee81e1 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -25,14 +25,16 @@ jobs: build-args: --wfail test: false lint: false + - name: Build tests + run: lake build testSuite --wfail - name: Run tests run: | while sleep 20; do - echo "lake test still running..." + echo "testSuite still running..." done & heartbeat=$! trap 'kill "$heartbeat" 2>/dev/null || true' EXIT - lake test --wfail + lake exe testSuite - name: Run local environment linters run: lake -d tools/linter exe runLinter - name: Check fixtures and formatter invariants From d9b7da7c8b0b7798f572dbd4bd821b37b881cf21 Mon Sep 17 00:00:00 2001 From: Duckki Oe Date: Sat, 15 Aug 2026 13:20:32 -0700 Subject: [PATCH 9/9] ci: split test suite groups --- .github/workflows/ci.yml | 15 +++++++++++++-- LeanFmt/Tests/Run.lean | 4 ++-- LeanFmt/Tests/Suite.lean | 10 +++++++--- 3 files changed, 22 insertions(+), 7 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index bee81e1..664de17 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -27,14 +27,25 @@ jobs: lint: false - name: Build tests run: lake build testSuite --wfail - - name: Run tests + - name: Run core tests run: | while sleep 20; do echo "testSuite still running..." done & heartbeat=$! trap 'kill "$heartbeat" 2>/dev/null || true' EXIT - lake exe testSuite + lake exe testSuite \ + syntax-tree documented-examples layout-architecture \ + basic-formatting expression-renderer control-flow \ + collection-declaration + - name: Run CLI and architecture tests + run: | + while sleep 20; do + echo "testSuite cli-architecture still running..." + done & + heartbeat=$! + trap 'kill "$heartbeat" 2>/dev/null || true' EXIT + lake exe testSuite cli-architecture - name: Run local environment linters run: lake -d tools/linter exe runLinter - name: Check fixtures and formatter invariants diff --git a/LeanFmt/Tests/Run.lean b/LeanFmt/Tests/Run.lean index ac6a076..60a4201 100644 --- a/LeanFmt/Tests/Run.lean +++ b/LeanFmt/Tests/Run.lean @@ -1,7 +1,7 @@ import LeanFmt.Tests.Suite -def main (_args : List String) : IO UInt32 := do +def main (args : List String) : IO UInt32 := do Lean.initSearchPath (← Lean.findSysroot) let env ← LeanFmt.Formatter.defaultEnvironment - LeanFmt.Tests.runTestGroups env + LeanFmt.Tests.runTestGroups env args pure 0 diff --git a/LeanFmt/Tests/Suite.lean b/LeanFmt/Tests/Suite.lean index 3272a45..93e7ad8 100644 --- a/LeanFmt/Tests/Suite.lean +++ b/LeanFmt/Tests/Suite.lean @@ -16240,7 +16240,7 @@ def runCliAndArchitectureTests (env projectSyntaxEnv : Lean.Environment) : IO Un assertIgnoreNextPreservesNestedTerm env assertCslibStyleCoreSyntaxHasRules env -def runTestGroups (env : Lean.Environment) : IO Unit := do +def runTestGroups (env : Lean.Environment) (selected : List String := []) : IO Unit := do let projectSyntaxEnv ← SyntaxTree.importEnvironment #[{ module := `LeanFmt.Tests.ProjectSyntax }] let groups := @@ -16254,7 +16254,11 @@ def runTestGroups (env : Lean.Environment) : IO Unit := do ("collection-declaration", runCollectionAndDeclarationTests env), ("cli-architecture", runCliAndArchitectureTests env projectSyntaxEnv) ] - for (_name, group) in groups do - group + for name in selected do + unless groups.any (fun (groupName, _) => groupName == name) do + throw <| IO.userError s!"unknown test group: {name}" + for (name, group) in groups do + if selected.isEmpty || selected.contains name then + group end LeanFmt.Tests