update LeanTest to prepare for a v3 test-runner

bin/update-from-templates

@@ -18,7 +18,7 @@ vendor_hash=$(hash_dir templates/vendor)
 toolchain_hash=$(md5sum templates/lean-toolchain | cut -d' ' -f1)
 
 num_updated=0
-for exercise_dir in exercises/practice/*; do
+for exercise_dir in exercises/{practice,concept}/*; do
     [[ -d "${exercise_dir}" ]] || continue
 
     # Update lean-toolchain

exercises/practice/acronym/vendor/LeanTest/LeanTest/Json.lean

@@ -0,0 +1,57 @@
+/-
+Minimal, dependency-free JSON string building.
+-/
+
+namespace LeanTest.Json
+
+private def hexDigit (n : Nat) : Char :=
+  if n < 10 then Char.ofNat (n + 48) else Char.ofNat (n - 10 + 97)
+
+private def toHex4 (n : Nat) : String :=
+  let d0 := hexDigit ((n / 4096) % 16)
+  let d1 := hexDigit ((n / 256) % 16)
+  let d2 := hexDigit ((n / 16) % 16)
+  let d3 := hexDigit (n % 16)
+  String.ofList [d0, d1, d2, d3]
+
+private def escapeChar (c : Char) : String :=
+  match c with
+  | '"' => "\\\""
+  | '\\' => "\\\\"
+  | '\n' => "\\n"
+  | '\r' => "\\r"
+  | '\t' => "\\t"
+  | c => if c.toNat < 0x20 then "\\u" ++ toHex4 c.toNat else String.ofList [c]
+
+/-- Escape a string's contents for embedding between JSON double-quotes. -/
+def escape (s : String) : String :=
+  String.join (s.toList.map escapeChar)
+
+/-- A JSON string literal, including the surrounding quotes. -/
+def str (s : String) : String :=
+  "\"" ++ escape s ++ "\""
+
+/-- A JSON string literal, or `null` when absent. -/
+def strOrNull : Option String → String
+  | none => "null"
+  | some s => str s
+
+/-- A JSON number, or `null` when absent. -/
+def natOrNull : Option Nat → String
+  | none => "null"
+  | some n => toString n
+
+/-- Truncate `s` to at most `maxLen` characters. -/
+def truncate (s : String) (maxLen : Nat) : String :=
+  if s.length <= maxLen then s
+  else String.ofList (s.toList.take (maxLen - 1)) ++ "…"
+
+/-- Build a JSON object from a list of already-encoded `"key": value` pairs. -/
+def object (fields : List String) : String :=
+  "{" ++ String.intercalate ", " fields ++ "}"
+
+/-- Build a JSON array from a list of already-encoded elements. -/
+def array (elems : List String) : String :=
+  "[" ++ String.intercalate ", " elems ++ "]"
+
+end LeanTest.Json

exercises/practice/acronym/vendor/LeanTest/LeanTest/SourceParser.lean

@@ -0,0 +1,84 @@
+/-
+Extracts the literal source text of each `.addTest "<name>" (...)` call.
+-/
+
+namespace LeanTest.SourceParser
+
+private def listStartsWith : List Char → List Char → Bool
+  | _, [] => true
+  | [], _ :: _ => false
+  | x :: xs, p :: ps => x == p && listStartsWith xs ps
+
+private def isSpace (c : Char) : Bool :=
+  c == ' ' || c == '\t' || c == '\n' || c == '\r'
+
+/-- Trim leading/trailing whitespace. -/
+private def trimStr (s : String) : String :=
+  let chars := s.toList.dropWhile isSpace
+  String.ofList (chars.reverse.dropWhile isSpace).reverse
+
+/-- Return the remainder of the list after `marker`, or `none` if it doesn't occur. -/
+private partial def findMarker (xs : List Char) (marker : List Char) : Option (List Char) :=
+  match xs with
+  | [] => none
+  | _ :: rest =>
+    if listStartsWith xs marker then some (xs.drop marker.length)
+    else findMarker rest marker
+
+private partial def readStringLiteral (xs : List Char) : String × List Char :=
+  go xs #[]
+where
+  go (xs : List Char) (acc : Array Char) : String × List Char :=
+    match xs with
+    | [] => (String.ofList acc.toList, [])
+    | '\\' :: c :: rest => go rest (acc.push '\\' |>.push c)
+    | '"' :: rest => (String.ofList acc.toList, rest)
+    | c :: rest => go rest (acc.push c)
+
+private partial def readParenBody (xs : List Char) : String × List Char :=
+  match xs with
+  | '(' :: rest => go rest 0 #[] false
+  | _ => ("", xs)
+where
+  go (xs : List Char) (depth : Nat) (acc : Array Char) (inString : Bool) : String × List Char :=
+    match xs with
+    | [] => (String.ofList acc.toList, [])
+    | '\\' :: c :: rest =>
+      if inString then go rest depth (acc.push '\\' |>.push c) inString
+      else go (c :: rest) depth (acc.push '\\') inString
+    | '"' :: rest => go rest depth (acc.push '"') (!inString)
+    | '(' :: rest =>
+      if inString then go rest depth (acc.push '(') inString
+      else go rest (depth + 1) (acc.push '(') inString
+    | ')' :: rest =>
+      if inString then go rest depth (acc.push ')') inString
+      else if depth == 0 then (String.ofList acc.toList, rest)
+      else go rest (depth - 1) (acc.push ')') inString
+    | c :: rest => go rest depth (acc.push c) inString
+
+/-- Extract `(test name, source body)` pairs for each `.addTest "<name>" (...)` in `source`. -/
+partial def extractTestBodies (source : String) : List (String × String) :=
+  go source.toList #[]
+where
+  marker := ".addTest \"".toList
+  go (xs : List Char) (acc : Array (String × String)) : List (String × String) :=
+    match findMarker xs marker with
+    | none => acc.toList
+    | some afterMarker =>
+      let (name, afterName) := readStringLiteral afterMarker
+      let afterWs := afterName.dropWhile isSpace
+      let (body, rest) := readParenBody afterWs
+      let trimmed := (trimStr body).toList
+      let trimmed :=
+        if listStartsWith trimmed ['d', 'o'] then
+          (trimStr (String.ofList (trimmed.drop 2))).toList
+        else trimmed
+      go rest (acc.push (name, String.ofList trimmed))
+
+/-- Look up the captured source for `name`, or `""` if extraction found nothing. -/
+def lookup (name : String) (bodies : List (String × String)) : String :=
+  match bodies.find? (fun p => p.1 == name) with
+  | some (_, code) => code
+  | none => ""
+
+end LeanTest.SourceParser

exercises/practice/acronym/vendor/LeanTest/LeanTest/Test.lean

@@ -3,21 +3,18 @@ Test case and test suite management.
 -/
 
 import LeanTest.Assertions
+import LeanTest.Json
+import LeanTest.SourceParser
 
 namespace LeanTest
 
 /-- A single test case -/
 structure TestCase where
   description : String
   test : IO AssertionResult
+  taskId : Option Nat := none -- set for concept exercises
   deriving Inhabited
 
-/-- Result of running a test -/
-structure TestResult where
-  description : String
-  result : AssertionResult
-  deriving Repr
-
 /-- A collection of tests (test suite) -/
 structure TestSuite where
   name : String
@@ -31,28 +28,49 @@ def empty (name : String) : TestSuite :=
   { name := name, tests := [] }
 
 /-- Add a test to the suite -/
-def addTest (suite : TestSuite) (description : String) (test : IO AssertionResult) : TestSuite :=
-  { suite with tests := suite.tests ++ [{ description := description, test := test }] }
+def addTest (suite : TestSuite) (description : String) (test : IO AssertionResult)
+    (taskId : Option Nat := none) : TestSuite :=
+  { suite with tests := suite.tests ++ [{ description := description, test := test, taskId := taskId }] }
 
 end TestSuite
 
+/-- Per-test outcome, matching the v3 interface's `pass` / `fail` / `error`. -/
+inductive TestStatus where
+  | pass
+  | fail
+  | error
+  deriving Repr, BEq
+
+def TestStatus.toReportString : TestStatus → String
+  | .pass => "pass"
+  | .fail => "fail"
+  | .error => "error"
+
+/-- Result of running a test -/
+structure TestResult where
+  description : String
+  status : TestStatus
+  message : Option String -- `none` when `status = .pass`
+  taskId : Option Nat
+  deriving Repr
+
 /-- Test statistics -/
 structure TestStats where
-  total : Nat
-  passed : Nat
-  failed : Nat
-  deriving Repr
+  total : Nat := 0
+  passed : Nat := 0
+  failed : Nat := 0
+  errored : Nat := 0
 
 namespace TestStats
 
-def empty : TestStats :=
-  { total := 0, passed := 0, failed := 0 }
+def empty : TestStats := {}
 
-def addResult (stats : TestStats) (result : AssertionResult) : TestStats :=
-  { total := stats.total + 1
-  , passed := if result.isSuccess then stats.passed + 1 else stats.passed
-  , failed := if result.isSuccess then stats.failed else stats.failed + 1
-  }
+def addResult (stats : TestStats) (status : TestStatus) : TestStats :=
+  { stats with
+    total := stats.total + 1
+    passed := stats.passed + (if status == .pass then 1 else 0)
+    failed := stats.failed + (if status == .fail then 1 else 0)
+    errored := stats.errored + (if status == .error then 1 else 0) }
 
 end TestStats
 
@@ -63,27 +81,33 @@ def yellowColor : String := "\x1b[33m"
 def resetColor : String := "\x1b[0m"
 def boldColor : String := "\x1b[1m"
 
-/-- Run a single test and print the result -/
+/-- Run a single test, printing a colored result line, and returning a structured `TestResult`.
+    Exceptions are caught and returned as a per-test `error`. -/
 def runTest (testCase : TestCase) : IO TestResult := do
-  let result ← testCase.test
-  match result with
-  | .success =>
-    IO.println s!"  {greenColor}✓{resetColor} {testCase.description}"
-  | .failure msg =>
+  try
+    let result ← testCase.test
+    match result with
+    | .success =>
+      IO.println s!"  {greenColor}✓{resetColor} {testCase.description}"
+      return { description := testCase.description, status := .pass, message := none, taskId := testCase.taskId }
+    | .failure msg =>
+      IO.println s!"  {redColor}✗{resetColor} {testCase.description}"
+      IO.println s!"    {redColor}{msg}{resetColor}"
+      return { description := testCase.description, status := .fail, message := some msg, taskId := testCase.taskId }
+  catch e =>
+    let msg := toString e
     IO.println s!"  {redColor}✗{resetColor} {testCase.description}"
     IO.println s!"    {redColor}{msg}{resetColor}"
-  return { description := testCase.description, result := result }
+    return { description := testCase.description, status := .error, message := some msg, taskId := testCase.taskId }
 
 /-- Run all tests in a test suite -/
-def runTestSuite (suite : TestSuite) : IO TestStats := do
+def runTestSuite (suite : TestSuite) : IO (List TestResult) := do
   IO.println s!"\n{boldColor}{suite.name}{resetColor}"
-  let mut stats := TestStats.empty
-
+  let mut results : List TestResult := []
   for testCase in suite.tests do
     let result ← runTest testCase
-    stats := stats.addResult result.result
-
-  return stats
+    results := results ++ [result]
+  return results
 
 /-- Print test summary -/
 def printSummary (stats : TestStats) : IO Unit := do
@@ -94,37 +118,81 @@ def printSummary (stats : TestStats) : IO Unit := do
 
   if stats.failed > 0 then
     IO.println s!"  {redColor}Failed: {stats.failed}{resetColor}"
+  if stats.errored > 0 then
+    IO.println s!"  {redColor}Errored: {stats.errored}{resetColor}"
+
+  if stats.failed > 0 || stats.errored > 0 then
     IO.println s!"\n{redColor}FAILED{resetColor}"
   else
     IO.println s!"\n{greenColor}ALL TESTS PASSED{resetColor}"
 
-/-- Run multiple test suites -/
-def runTestSuites (suites : List TestSuite) : IO Unit := do
-  let mut totalStats := TestStats.empty
-
+/-- Build the v3 `results.json` payload for a full run's `TestResult`s.
+    `testCode` maps each test's description to its captured source.
+    `results` may be empty if an exercise is compile-time only (theorem proving, etc.). -/
+def buildResultsJson (results : List TestResult) (testCode : List (String × String)) : String :=
+  open Json in
+  let overall : TestStatus :=
+    if results.all (fun t => t.status == .pass) then .pass
+    else if !results.isEmpty && results.all (fun t => t.status == .error) then .error
+    else .fail
+  let testJson (t : TestResult) : String :=
+    let code := SourceParser.lookup t.description testCode
+    let fields :=
+      [ s!"\"name\": {str t.description}"
+      , s!"\"status\": {str t.status.toReportString}"
+      , s!"\"message\": {strOrNull t.message}"
+      , s!"\"test_code\": {str code}"
+      ] ++ (match t.taskId with
+            | none => []
+            | some n => [s!"\"task_id\": {n}"])
+    object fields
+  let topMessage : Option String :=
+    match overall with
+    | .error =>
+      let firstMsg := results.head?.bind (·.message)
+      some (truncate (firstMsg.getD "All tests failed with an error.") 65535)
+    | _ => none
+  object [
+    s!"\"version\": 3",
+    s!"\"status\": {str overall.toReportString}",
+    s!"\"message\": {strOrNull topMessage}",
+    s!"\"tests\": {array (results.map testJson)}"
+  ]
+
+/-- If the runner set `EXERCISM_OUTPUT_DIR`, write `results.json` there.
+    Reads `EXERCISM_TEST_FILE` (if set) to source `test_code` from the test file.
+    Silently does nothing when `EXERCISM_OUTPUT_DIR` is unset. -/
+def writeResultsIfRequested (results : List TestResult) : IO Unit := do
+  match (← IO.getEnv "EXERCISM_OUTPUT_DIR") with
+  | none => pure ()
+  | some outputDir =>
+    let testCode ←
+      match (← IO.getEnv "EXERCISM_TEST_FILE") with
+      | none => pure []
+      | some path =>
+        try
+          let source ← IO.FS.readFile path
+          pure (SourceParser.extractTestBodies source)
+        catch _ => pure []
+    IO.FS.createDirAll outputDir
+    IO.FS.writeFile s!"{outputDir}/results.json" (buildResultsJson results testCode)
+
+/-- Run multiple test suites, print a summary.
+    If the proper env vars are set, write `results.json`. -/
+def runTestSuites (suites : List TestSuite) : IO (List TestResult) := do
+  let mut allResults : List TestResult := []
   for suite in suites do
-    let stats ← runTestSuite suite
-    totalStats := {
-      total := totalStats.total + stats.total,
-      passed := totalStats.passed + stats.passed,
-      failed := totalStats.failed + stats.failed
-    }
+    let results ← runTestSuite suite
+    allResults := allResults ++ results
 
-  printSummary totalStats
+  let stats := allResults.foldl (fun s r => s.addResult r.status) TestStats.empty
+  printSummary stats
+  writeResultsIfRequested allResults
+  return allResults
 
-/-- Run multiple test suites and return exit code (0 = all passed, 1 = some failed) -/
+/-- Run multiple test suites and return exit code (0 = all passed, 1 = some failed/errored) -/
 def runTestSuitesWithExitCode (suites : List TestSuite) : IO UInt32 := do
-  let mut totalStats := TestStats.empty
-
-  for suite in suites do
-    let stats ← runTestSuite suite
-    totalStats := {
-      total := totalStats.total + stats.total,
-      passed := totalStats.passed + stats.passed,
-      failed := totalStats.failed + stats.failed
-    }
-
-  printSummary totalStats
-  return if totalStats.failed > 0 then 1 else 0
+  let results ← runTestSuites suites
+  return if results.any (fun r => r.status != .pass) then 1 else 0
 
 end LeanTest