|
| 1 | +/- |
| 2 | +Copyright (c) 2025 Lean FRO LLC. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Author: Jason Reed |
| 5 | +-/ |
| 6 | +import Lean.Util.Diff |
| 7 | + |
| 8 | +namespace Verso.Integration |
| 9 | + |
| 10 | +/-- Configuration for the test runner -/ |
| 11 | +structure Config where |
| 12 | + /-- Where are expected files located? We expect a subdirectory |
| 13 | + `expected` and `runTest` should produce files into a subdirectory |
| 14 | + `output`. -/ |
| 15 | + testDir : System.FilePath |
| 16 | + /-- Should the expected output be replaced with the actual output? -/ |
| 17 | + updateExpected : Bool := false |
| 18 | + /-- How to run the test -/ |
| 19 | + runTest : IO Unit |
| 20 | + |
| 21 | +/-- |
| 22 | +Returns all non-directory filepaths that are children of `root`, which |
| 23 | +must be a directory. Returns these as paths relative to `root`. |
| 24 | +
|
| 25 | +This differs from `System.FilePath.walkRoot`, in that the latter returns |
| 26 | +absolute paths, and includes subdirectories. |
| 27 | +-/ |
| 28 | +partial def filesBelow (root : System.FilePath) : |
| 29 | + IO (Array System.FilePath) := Prod.snd <$> StateT.run (go ".") #[] |
| 30 | +where |
| 31 | + go (p : System.FilePath) := do |
| 32 | + for d in (← (root / p).readDir) do |
| 33 | + if ← d.path.isDir then |
| 34 | + go (p / d.fileName) |
| 35 | + else |
| 36 | + modify (·.push (p / d.fileName)) |
| 37 | + |
| 38 | +/-- |
| 39 | +Given an array of pairs `(src, tgt)` of absolute paths, copy every |
| 40 | +`src` to every `tgt`, creating directories as necessary. |
| 41 | +-/ |
| 42 | +partial def copyFiles (pairs : Array (System.FilePath × System.FilePath)) : |
| 43 | + IO Unit := do |
| 44 | + for (src, tgt) in pairs do |
| 45 | + if let .some parent := tgt.parent then |
| 46 | + IO.FS.createDirAll parent |
| 47 | + IO.FS.writeBinFile tgt (← IO.FS.readBinFile src) |
| 48 | + |
| 49 | +/-- Main test runner -/ |
| 50 | +def runTests (config : Config) : IO Unit := do |
| 51 | + unless ← System.FilePath.pathExists config.testDir do |
| 52 | + throw <| .userError s!"Test directory not found: {config.testDir}" |
| 53 | + |
| 54 | + let outputRoot := config.testDir / "output" |
| 55 | + let expectedRoot := config.testDir / "expected" |
| 56 | + |
| 57 | + if config.updateExpected then |
| 58 | + let outputFiles := (← filesBelow outputRoot) |
| 59 | + IO.println s!"Updating expected outputs in {config.testDir}..." |
| 60 | + if ← System.FilePath.pathExists expectedRoot then do |
| 61 | + IO.FS.removeDirAll expectedRoot |
| 62 | + copyFiles (outputFiles.map (fun p => (outputRoot / p, expectedRoot / p))) |
| 63 | + else |
| 64 | + unless ← System.FilePath.pathExists expectedRoot do |
| 65 | + throw <| .userError s!"Expected output directory not found: {expectedRoot}" |
| 66 | + let expectedFiles := (← filesBelow expectedRoot) |
| 67 | + |
| 68 | + IO.println s!"Running test in {config.testDir}..." |
| 69 | + if ← outputRoot.pathExists then |
| 70 | + IO.FS.removeDirAll outputRoot |
| 71 | + config.runTest |
| 72 | + let outputFiles := (← filesBelow outputRoot) |
| 73 | + |
| 74 | + if expectedFiles != outputFiles then |
| 75 | + IO.println s!"✗ Expected files differ from actual files" |
| 76 | + IO.println s!"Expected files in {expectedRoot}:\n {expectedFiles}" |
| 77 | + IO.println s!"Actual files in {outputRoot}:\n {outputFiles}" |
| 78 | + throw <| .userError s!"Test in {config.testDir} failed" |
| 79 | + |
| 80 | + for file in expectedFiles do |
| 81 | + let expected ← IO.FS.readFile (expectedRoot / file) |
| 82 | + let actual ← IO.FS.readFile (outputRoot / file) |
| 83 | + if expected != actual then |
| 84 | + let d := Lean.Diff.diff (expected.split (· == '\n') |>.toArray) (actual.split (· == '\n') |>.toArray) |
| 85 | + IO.println s!"✗ In test {config.testDir}, output file {file}" |
| 86 | + IO.println s!" Expected output differs from actual output" |
| 87 | + IO.println (Lean.Diff.linesToString d) |
| 88 | + throw <| .userError s!"Test in {config.testDir} failed" |
| 89 | + |
| 90 | + return |
0 commit comments