From ca4ca9fbd0e830131512b72c9162b63e1dbd8c82 Mon Sep 17 00:00:00 2001 From: oxe-i Date: Mon, 16 Feb 2026 15:23:04 -0300 Subject: [PATCH 1/4] improve error handling by the generator --- generators/GenerateTestFile.lean | 130 ++++++++++++++++++++----------- 1 file changed, 83 insertions(+), 47 deletions(-) diff --git a/generators/GenerateTestFile.lean b/generators/GenerateTestFile.lean index 09a29d8..9516eb7 100644 --- a/generators/GenerateTestFile.lean +++ b/generators/GenerateTestFile.lean @@ -42,16 +42,32 @@ def addPracticeExercise (exercise : String) (as : List String) : IO Unit := do let _ <- child.wait def getPath (exercise : String) : IO String := do - let info ← IO.Process.run { - cmd := "bin/configlet", - args := #["info", "-o", "-v", "d"] - } - let dirPrefix := "Using cached 'problem-specifications' dir: " - let directory := info.splitOn "\n" |> - List.filter (·.startsWith dirPrefix) |> - List.map (·.stripPrefix dirPrefix) |> - List.head! - return s!"{directory}/exercises/{exercise}" + try + let info ← IO.Process.run { + cmd := "bin/configlet", + args := #["info", "-o", "-v", "d"] + } + let dirPrefix := "Using cached 'problem-specifications' dir: " + let directory := info.splitOn "\n" |> + List.filter (·.startsWith dirPrefix) |> + List.map (·.stripPrefix dirPrefix) |> + List.head! + return s!"{directory}/exercises/{exercise}" + catch _ => + let _ ← IO.Process.run { + cmd := "bin/fetch-configlet" + } + let info ← IO.Process.run { + cmd := "bin/configlet", + args := #["info", "-o", "-v", "d"] + } + let dirPrefix := "Using cached 'problem-specifications' dir: " + let directory := info.splitOn "\n" |> + List.filter (·.startsWith dirPrefix) |> + List.map (·.stripPrefix dirPrefix) |> + List.head! + return s!"{directory}/exercises/{exercise}" + def getToml (exercise : String) : IO (Except String String) := do let path := s!"exercises/practice/{exercise}/.meta/tests.toml" @@ -59,7 +75,7 @@ def getToml (exercise : String) : IO (Except String String) := do let toml <- IO.FS.readFile path return .ok toml catch _ => - return .error "No toml file." + return .error "No toml file" def readCanonicalData (exercise : String) : IO (Except String Json) := do let path <- getPath exercise @@ -67,7 +83,7 @@ def readCanonicalData (exercise : String) : IO (Except String Json) := do let json <- IO.FS.readFile (path ++ "/canonical-data.json") return Json.parse json catch _ => - return .error "No canonical data." + return .error "No canonical data" def processCanonicalCases (tests : TreeMap String String) (array : Array Json) : Except String OrderedMap := Id.run do let mut fullArray := #[] @@ -94,17 +110,25 @@ def processCanonicalCases (tests : TreeMap String String) (array : Array Json) : def getCanonicalCases (canonical : TreeMap.Raw String Json) (tests : TreeMap String String) : Except String OrderedMap := match canonical.get? "cases" with - | none => .error "No cases in canonical data." + | none => .error "No cases in canonical data" | some json => let array := getOk json.getArr? processCanonicalCases tests array -def readExtraCases (exercise : String) : IO (Except String Json) := do +def checkExtraCases (exercise : String) : IO (Except String String) := do try let json <- IO.FS.readFile (s!"exercises/practice/{exercise}/.meta/extra.json") - return Json.parse json + return .ok json catch _ => - return .error "No extra cases found." + return .error "No extra cases found" + +def readExtraCases (exercise : String) : IO (Except String Json) := do + match ← checkExtraCases exercise with + | .error msg => return .error msg + | .ok extra => + match Json.parse extra with + | .error _ => throw <| IO.userError s!"Found extra cases, but they couldn't be parsed. Is it valid JSON?" + | .ok parsed => return .ok parsed def getExtraCases (extra : Except String Json) : TreeMap.Raw String Json := match extra with @@ -186,45 +210,53 @@ def showUsage : IO Unit := def generateTestFile (exercise : String) : IO Unit := do let pascalExercise := pascalCase exercise - let maybeToml <- getToml exercise - let extra <- readExtraCases exercise + let maybeToml ← getToml exercise + let mut extra := #[] + match ← readExtraCases exercise with + | .error msg => IO.eprintln s!"{msg}. Checking canonical data." + | .ok extraCases => extra := getOk extraCases.getArr? match maybeToml with - | .error _ => - match extra with - | .error msg => throw <| IO.userError msg - | .ok json => - let array := getOk json.getArr? - match genTestFileContent pascalExercise empty array with + | .error msg => + if extra.isEmpty + then throw <| IO.userError s!"{msg} and no extra cases found." + else + IO.eprintln s!"{msg}. Trying to add extra cases." + match genTestFileContent pascalExercise empty extra with | .error msg => throw <| IO.userError msg | .ok testContent => IO.FS.writeFile s!"exercises/practice/{exercise}/{pascalExercise}Test.lean" testContent | .ok toml => let tests := getIncludes toml - let canonicalData <- readCanonicalData exercise - let data := match canonicalData with - | .error _ => Json.null - | .ok data => data - match data.getObj? with - | .error _ => - match extra with - | .error msg => throw <| IO.userError msg - | .ok json => - let array := getOk json.getArr? - match genTestFileContent pascalExercise empty array with + match ← readCanonicalData exercise with + | .error msg => + if extra.isEmpty + then throw <| IO.userError s!"{msg} and no extra cases found." + else + IO.eprintln s!"{msg}. Trying to add extra cases." + match genTestFileContent pascalExercise empty extra with | .error msg => throw <| IO.userError msg | .ok testContent => IO.FS.writeFile s!"exercises/practice/{exercise}/{pascalExercise}Test.lean" testContent - | .ok maybeMap => - match getCanonicalCases maybeMap tests with - | .error msg => throw <| IO.userError msg - | .ok cases => - match extra with - | .error _ => - match genTestFileContent pascalExercise cases #[] with + | .ok canonicalData => + match canonicalData.getObj? with + | .error _ => + if extra.isEmpty + then throw <| IO.userError "Canonical data could not be parsed and no extra cases found." + else + IO.eprintln s!"Canonical data could not be parsed. Trying to add extra cases." + match genTestFileContent pascalExercise empty extra with | .error msg => throw <| IO.userError msg - | .ok testContent => - IO.FS.writeFile s!"exercises/practice/{exercise}/{pascalExercise}Test.lean" testContent - | .ok json => - let array := getOk json.getArr? - match genTestFileContent pascalExercise cases array with + | .ok testContent => IO.FS.writeFile s!"exercises/practice/{exercise}/{pascalExercise}Test.lean" testContent + | .ok maybeMap => + match getCanonicalCases maybeMap tests with + | .error msg => + if extra.isEmpty + then throw <| IO.userError s!"{msg} and no extra cases found." + else + IO.eprintln s!"Parsing canonical data returned error: {msg}. Trying to add extra cases." + match genTestFileContent pascalExercise empty extra with + | .error msg => throw <| IO.userError msg + | .ok testContent => IO.FS.writeFile s!"exercises/practice/{exercise}/{pascalExercise}Test.lean" testContent + | .ok cases => + match genTestFileContent pascalExercise cases extra with | .error msg => throw <| IO.userError msg | .ok testContent => IO.FS.writeFile s!"exercises/practice/{exercise}/{pascalExercise}Test.lean" testContent @@ -311,10 +343,13 @@ def main (args : List String) : IO Unit := do | "-a" :: exercise :: as | "--add" :: exercise :: as => addPracticeExercise exercise as + IO.println "Exercise successfully added." generateTestFile exercise.trim + IO.println "Test cases successfully generated." | "-g" :: exercise :: _ | "--generate" :: exercise :: _ => generateTestFile exercise.trim + IO.println "Test cases successfully generated." | "-s" :: exercise :: _ | "--stub" :: exercise :: _ => generateStub exercise.trim @@ -322,5 +357,6 @@ def main (args : List String) : IO Unit := do | "--regenerate" :: _ => fetchConfiglet regenerateTestFiles + IO.println "Test cases successfully regenerated." | _ => showUsage From ba5128b8902239ff549b9f30b8cf134342c71e6d Mon Sep 17 00:00:00 2001 From: oxe-i Date: Mon, 16 Feb 2026 15:29:10 -0300 Subject: [PATCH 2/4] invalid extra cases does not interrupt generation, but an error is shown --- generators/GenerateTestFile.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/generators/GenerateTestFile.lean b/generators/GenerateTestFile.lean index 9516eb7..15dd6cf 100644 --- a/generators/GenerateTestFile.lean +++ b/generators/GenerateTestFile.lean @@ -127,7 +127,7 @@ def readExtraCases (exercise : String) : IO (Except String Json) := do | .error msg => return .error msg | .ok extra => match Json.parse extra with - | .error _ => throw <| IO.userError s!"Found extra cases, but they couldn't be parsed. Is it valid JSON?" + | .error _ => return .error "Found extra cases, but they couldn't be parsed. Is it valid JSON?" | .ok parsed => return .ok parsed def getExtraCases (extra : Except String Json) : TreeMap.Raw String Json := From 036508dae60dce1ae041f42072c8c198c49d07b0 Mon Sep 17 00:00:00 2001 From: oxe-i Date: Mon, 16 Feb 2026 15:37:08 -0300 Subject: [PATCH 3/4] adjust punctuation in extra cases errors --- generators/GenerateTestFile.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/generators/GenerateTestFile.lean b/generators/GenerateTestFile.lean index 15dd6cf..0789900 100644 --- a/generators/GenerateTestFile.lean +++ b/generators/GenerateTestFile.lean @@ -120,7 +120,7 @@ def checkExtraCases (exercise : String) : IO (Except String String) := do let json <- IO.FS.readFile (s!"exercises/practice/{exercise}/.meta/extra.json") return .ok json catch _ => - return .error "No extra cases found" + return .error "No extra cases found." def readExtraCases (exercise : String) : IO (Except String Json) := do match ← checkExtraCases exercise with @@ -213,7 +213,7 @@ def generateTestFile (exercise : String) : IO Unit := do let maybeToml ← getToml exercise let mut extra := #[] match ← readExtraCases exercise with - | .error msg => IO.eprintln s!"{msg}. Checking canonical data." + | .error msg => IO.eprintln s!"{msg} Checking canonical data." | .ok extraCases => extra := getOk extraCases.getArr? match maybeToml with | .error msg => From 6334456d76aebbb761775118802f4de1ea29753e Mon Sep 17 00:00:00 2001 From: oxe-i Date: Mon, 16 Feb 2026 15:40:11 -0300 Subject: [PATCH 4/4] reuse fetchConfiglet --- generators/GenerateTestFile.lean | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/generators/GenerateTestFile.lean b/generators/GenerateTestFile.lean index 0789900..9b51b5a 100644 --- a/generators/GenerateTestFile.lean +++ b/generators/GenerateTestFile.lean @@ -54,9 +54,7 @@ def getPath (exercise : String) : IO String := do List.head! return s!"{directory}/exercises/{exercise}" catch _ => - let _ ← IO.Process.run { - cmd := "bin/fetch-configlet" - } + fetchConfiglet let info ← IO.Process.run { cmd := "bin/configlet", args := #["info", "-o", "-v", "d"]