diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 91fd941..664de17 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -25,14 +25,27 @@ jobs: build-args: --wfail test: false lint: false - - name: Run tests + - name: Build tests + run: lake build testSuite --wfail + - name: Run core 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 \ + 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 92f1c31..93e7ad8 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) @@ -13292,7 +13287,8 @@ def assertCliSkipsHiddenPathsByDefault : IO Unit := ] do assertTrue s!"CLI --include-hidden discovers {file}" (includedFiles.contains file) -def assertCliLoadsImportedSyntax : 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" @@ -13303,18 +13299,14 @@ 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 + 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" @@ -14761,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 @@ -14829,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 @@ -16213,7 +16202,7 @@ def runCliAndArchitectureTests (env projectSyntaxEnv : Lean.Environment) : IO Un assertCliFormatsDirectory env loader assertCliFormatsDirectoryRecursively env loader assertCliSkipsHiddenPathsByDefault - assertCliLoadsImportedSyntax + assertFormatsImportedSyntaxWithProjectEnvironment projectSyntaxEnv assertFmtExecutableConfigured assertRendererTraceIncludesPathAndState env assertCliFixtureUpdate env @@ -16229,7 +16218,7 @@ def runCliAndArchitectureTests (env projectSyntaxEnv : Lean.Environment) : IO Un assertQqApplicationArgumentUsesStructuralBoundary projectSyntaxEnv assertLakeDslFormatting assertMathlibLowRiskSyntaxKindsHaveRules - assertMissingRuleCheckUsesDispatch env loader + assertMissingRuleCheckUsesDispatch env projectSyntaxEnv assertCheckCommandHasRule env assertGuardMsgsCommandUsesCommandInLayout env assertBinderTacticProofBodyHasNoMissingRules env @@ -16251,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 := @@ -16265,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