Fix course validation and progress tracking

.github/workflows/ci.yml

@@ -26,6 +26,9 @@ jobs:
       - name: Build
         run: lake build
 
+      - name: Run Leanlings regressions
+        run: lake env lean --run tests/LeanlingsRegression.lean
+
       # The `nng` course's solutions form a Lean library, so they are already
       # compiled (and thus verified) by `lake build` above. Here we check the
       # standalone `intro` solutions, compiled file-by-file together with each
@@ -51,3 +54,8 @@ jobs:
             exit 1
           fi
           echo "All intro solutions verified against their checks"
+
+      - name: Verify intro IO output
+        run: |
+          diff -u <(printf 'Hello, Lean!\n') <(lean --run courses/intro/solutions/15_io/io1.lean)
+          diff -u <(printf '5\n4\n3\n2\n1\n') <(lean --run courses/intro/solutions/15_io/io2.lean)

Leanlings/Config.lean

@@ -126,9 +126,11 @@ private def introExercises : Array Exercise := #[
 
   -- 15_io
   { name := "io1", dir := "15_io",
-    hint := "`s!\"text {variable} text\"` is string interpolation.\n`IO.println` prints a line to the console." },
+    hint := "`s!\"text {variable} text\"` is string interpolation.\n`IO.println` prints a line to the console.",
+    expectedOutput := some "Hello, Lean!\n" },
   { name := "io2", dir := "15_io",
-    hint := "`List.range n` gives `[0, 1, ..., n-1]`.\nUse a `for` loop to iterate over it and print." },
+    hint := "`List.range n` gives `[0, 1, ..., n-1]`.\nUse a `for` loop to iterate over it and print.",
+    expectedOutput := some "5\n4\n3\n2\n1\n" },
 
   -- 16_implicit
   { name := "implicit1", dir := "16_implicit",
@@ -573,7 +575,7 @@ private def algebraExercises : Array Exercise := #[
     hint := "Re-associate, then commute the whole product." },
   { name := "sq_expand", dir := "CommRing",
     hint := "Expand with `mul_add_mul`, then commute the `b * a` term to `a * b`." },
-  -- Field
+  -- RealField
   { name := "mul_inv_cancel", dir := "RealField",
     hint := "This is exactly the field axiom for nonzero `a`." },
   { name := "inv_mul_cancel", dir := "RealField",
@@ -764,8 +766,8 @@ private def analysisWelcome : String :=
   "You will build the rational and real numbers from the ground up — no Mathlib —\n" ++
   "and develop their theory through Cauchy sequences toward the completeness of ℝ.\n\n" ++
   "The path: construct ℚ as a quotient of fractions (proving the equivalence\n" ++
-  "relation and that the operations are well defined), develop its ordered-field\n" ++
-  "theory (order, absolute value, the Archimedean property, density), build Cauchy\n" ++
+  "relation and that the operations are well defined), develop its arithmetic\n" ++
+  "and order theory (absolute value, the Archimedean property, density), build Cauchy\n" ++
   "sequences, and assemble ℝ as their quotient.\n\n" ++
   "Two ideas recur. (1) A statement about ℚ reduces, via `mk_eq` and the\n" ++
   "computation lemmas, to one about integers that `grind`/`omega` close. (2) A\n" ++
@@ -781,8 +783,9 @@ private def analysisFinal : String :=
   "Along the way you proved:\n" ++
   "  - that cross-multiplication is an equivalence relation, and that +, ×, −, <,\n" ++
   "    ≤ respect it, so they descend to the quotient ℚ;\n" ++
-  "  - the ordered-field theory of ℚ: the field axioms, trichotomy, the triangle\n" ++
-  "    inequality, the Archimedean property, and density;\n" ++
+  "  - the arithmetic and order theory of ℚ: algebraic laws (including inverse\n" ++
+  "    cancellation), trichotomy, the triangle inequality, the Archimedean\n" ++
+  "    property, and density;\n" ++
   "  - that constant, sum, negation sequences are Cauchy and that `CauchyEquiv` is\n" ++
   "    an equivalence relation;\n" ++
   "  - the ring theory of ℝ, built as the quotient of Cauchy sequences, with ℚ\n" ++
@@ -791,11 +794,11 @@ private def analysisFinal : String :=
   "    converges, in ℝ, to the real number it represents;\n" ++
   "  - the basics of abstract metric spaces (with ℝ as the example): that a\n" ++
   "    convergent sequence is Cauchy, proven from the axioms alone;\n" ++
-  "  - that ℝ is a field — every nonzero real has a multiplicative inverse;\n" ++
+  "  - that every nonzero real satisfies the inverse law `x * x⁻¹ = 1`;\n" ++
   "  - and the summit: ℝ is Cauchy-complete — every Cauchy sequence of reals\n" ++
   "    converges — proven by rational approximation.\n\n" ++
-  "You have built the real numbers from nothing and proved they are a complete\n" ++
-  "ordered field. That is the foundation the whole of real analysis rests on.\n"
+  "You have built the real numbers from nothing as a Cauchy-complete metric\n" ++
+  "space with commutative-ring operations and inverses for nonzero elements.\n"
 
 /-- Real analysis from scratch: construct ℚ and ℝ (via Cauchy sequences) in core
 Lean, then develop their theory. -/
@@ -806,6 +809,14 @@ def analysis : Course :=
 
 def courses : Array Course := #[intro, nng, algebra, analysis]
 
+/-- Qualified exercise ids must be unique within each course; otherwise progress
+tracking would be ambiguous again. -/
+private def hasUniqueExerciseIds (course : Course) : Bool :=
+  course.exercises.all fun exercise =>
+    (course.exercises.filter (·.id == exercise.id)).size == 1
+
+#guard courses.all hasUniqueExerciseIds
+
 /-- The course used when none is selected or a stored selection is invalid. -/
 def defaultCourse : Course := intro
 

Leanlings/Course.lean

@@ -29,9 +29,27 @@ def mkCourse (id title description : String) (exercises : Array Exercise)
 
 namespace Course
 
-/-- Find an exercise within this course by name. -/
-def getExercise (c : Course) (name : String) : Option Exercise :=
-  c.exercises.find? (·.name == name)
+/-- All exercises with a given bare name. -/
+def exercisesNamed (c : Course) (name : String) : Array Exercise :=
+  c.exercises.filter (·.name == name)
+
+/-- Whether a bare exercise name needs qualification in this course. -/
+def isAmbiguousName (c : Course) (name : String) : Bool :=
+  (c.exercisesNamed name).size > 1
+
+/-- Find an exercise by its qualified `dir/name` id, or by a bare name when that
+name is unique in the course. Ambiguous bare names deliberately fail instead of
+silently selecting the first exercise. -/
+def getExercise (c : Course) (target : String) : Option Exercise :=
+  match c.exercises.find? (·.id == target) with
+  | some exercise => some exercise
+  | none =>
+    let candidates := c.exercisesNamed target
+    if candidates.size == 1 then candidates[0]? else none
+
+/-- The shortest label that still identifies this exercise in its course. -/
+def displayName (c : Course) (exercise : Exercise) : String :=
+  if c.isAmbiguousName exercise.name then exercise.id else exercise.name
 
 end Course
 end Leanlings

Leanlings/Exercise.lean

@@ -14,10 +14,18 @@ structure Exercise where
   /-- The id of the course this exercise belongs to. Stamped by `mkCourse`. -/
   course : String := ""
   hint : String := ""
+  /-- Exact stdout expected when this exercise is executed with `lean --run`.
+  Most exercises are compile-time tasks and leave this unset. -/
+  expectedOutput : Option String := none
   deriving Repr, BEq, Inhabited
 
 namespace Exercise
 
+/-- The exercise's course-local, unambiguous identifier. Bare names remain
+accepted by the CLI when they identify exactly one exercise in a course. -/
+def id (e : Exercise) : String :=
+  s!"{e.dir}/{e.name}"
+
 def path (e : Exercise) : System.FilePath :=
   s!"courses/{e.course}/exercises/{e.dir}/{e.name}.lean"
 

Leanlings/Runner.lean

@@ -20,6 +20,29 @@ private def runLean (path : System.FilePath) : IO ExerciseStatus := do
     return .compileError (output.stdout ++ output.stderr)
   return .success
 
+private def normalizeNewlines (s : String) : String :=
+  s.replace "\r\n" "\n"
+
+/-- Execute an IO exercise and compare its stdout with the contract in its
+metadata. This catches programs that merely type-check without doing the task. -/
+private def checkProgramOutput (exercise : Exercise) (expected : String) :
+    IO ExerciseStatus := do
+  let output ← IO.Process.output {
+    cmd := "lake"
+    args := #["env", "lean", "--run", exercise.path.toString]
+  }
+  if output.exitCode != 0 then
+    return .compileError
+      ("Your code compiles, but running it failed:\n" ++ output.stdout ++ output.stderr)
+  let actual := normalizeNewlines output.stdout
+  let expected := normalizeNewlines expected
+  if actual == expected then
+    return .success
+  return .compileError
+    ("Your code compiles, but it prints the wrong output.\n" ++
+     s!"Expected: {reprStr expected}\n" ++
+     s!"Actual:   {reprStr actual}")
+
 /-- Check a single exercise.
 
 Compiles via `lake env lean` so exercises that `import` a course library (e.g.
@@ -33,25 +56,30 @@ answers aren't shown to the learner. We check in two phases:
    real file with correct line numbers.
 2. If that is clean and a hidden test file exists, compile the exercise and the
    tests together. A failure here means the code type-checks but doesn't meet
-   the requirement; we say so without revealing the checks. -/
+   the requirement; we say so without revealing the checks.
+3. If the exercise declares expected output, execute it and compare stdout
+   exactly (apart from normalizing platform newline sequences). -/
 def checkExercise (exercise : Exercise) : IO ExerciseStatus := do
   match ← runLean exercise.path with
   | .success =>
     let testSrc ← (try some <$> IO.FS.readFile exercise.testPath catch _ => pure none)
     match testSrc with
-    | none => return .success
+    | none => pure ()
     | some tests =>
       let exSrc ← IO.FS.readFile exercise.path
       let tmp : System.FilePath := ".leanlings-check.lean"
       IO.FS.writeFile tmp (exSrc ++ "\n\n" ++ tests)
       let result ← runLean tmp
       try IO.FS.removeFile tmp catch _ => pure ()
       match result with
-      | .success => return .success
+      | .success => pure ()
       | _ =>
         return .compileError
           "Your code compiles, but it doesn't satisfy the exercise's checks yet.\n\
            Re-read the task — the expected behaviour is described there."
+    match exercise.expectedOutput with
+    | some expected => checkProgramOutput exercise expected
+    | none => return .success
   | other => return other
 
 /-- Display the result of checking an exercise -/

Leanlings/State.lean

@@ -5,8 +5,9 @@ namespace Leanlings
 
 /-- Persistent state tracking progress across courses.
 
-`completed` entries are namespaced as `"<courseId>/<exerciseName>"` so progress
-in one course never collides with another. `currentExercise` is a bare name
+`completed` entries are namespaced as `"<courseId>/<exerciseId>"`, where an
+exercise id is `"<dir>/<name>"`, so neither duplicate names within a course nor
+names shared by different courses collide. `currentExercise` is a qualified id
 within `currentCourse`. -/
 structure AppState where
   currentCourse : String
@@ -19,13 +20,48 @@ namespace AppState
 def stateFile : System.FilePath := ".leanlings-state"
 
 /-- The key under which an exercise's completion is recorded. -/
-def key (courseId name : String) : String := s!"{courseId}/{name}"
+def key (courseId exerciseId : String) : String := s!"{courseId}/{exerciseId}"
 
 def initial (course : Course) : AppState :=
   { currentCourse := course.id,
-    currentExercise := (course.exercises.getD 0 default).name,
+    currentExercise := (course.exercises.getD 0 default).id,
     completed := #[] }
 
+/-- Upgrade one completion key from the old `course/name` format to
+`course/dir/name`. For an old ambiguous name, selecting the first matching
+exercise is conservative: that is the only exercise the old runner could
+resolve and check. Unknown keys are retained unchanged. -/
+def migrateCompletedKey (courses : Array Course) (stored : String) : String :=
+  match courses.findSome? fun course =>
+    let coursePrefix := s!"{course.id}/"
+    if stored.startsWith coursePrefix then
+      let target := stored.drop coursePrefix.length
+      match course.exercises.find? (·.id == target) with
+      | some exercise => some (key course.id exercise.id)
+      | none =>
+        match course.exercises.find? (·.name == target) with
+        | some exercise => some (key course.id exercise.id)
+        | none => none
+    else
+      none
+  with
+  | some migrated => migrated
+  | none => stored
+
+/-- Migrate and deduplicate all stored completion keys. -/
+def normalizeCompleted (courses : Array Course) (stored : Array String) : Array String :=
+  stored.foldl (fun completed oldKey =>
+    let newKey := migrateCompletedKey courses oldKey
+    if completed.contains newKey then completed else completed.push newKey) #[]
+
+/-- Resolve either a current qualified id or a current name from an older state
+file. Legacy ambiguous names select the first exercise for the same reason as
+`migrateCompletedKey`. -/
+private def resolveStoredExercise (course : Course) (stored : String) : Option Exercise :=
+  match course.exercises.find? (·.id == stored) with
+  | some exercise => some exercise
+  | none => course.exercises.find? (·.name == stored)
+
 /-- Load state from disk, or return initial state if no (valid) state file exists.
 
 A stored course or exercise that no longer exists is repaired to a sensible
@@ -36,15 +72,17 @@ def load (courses : Array Course) (defaultCourse : Course) : IO AppState := do
     let lines := (content.splitOn "\n").filter (· != "")
     match lines with
     | course :: current :: rest =>
-      let completed := (rest.filter (· != "---")).toArray
+      let completed := normalizeCompleted courses (rest.filter (· != "---")).toArray
       let validCourse := if courses.any (·.id == course) then course else defaultCourse.id
       let activeCourse := (courses.find? (·.id == validCourse)).getD defaultCourse
       let validCurrent :=
-        if activeCourse.exercises.any (·.name == current) then current
-        else match activeCourse.exercises.findSome? (fun ex =>
-               if !completed.contains (key validCourse ex.name) then some ex.name else none) with
-             | some name => name
-             | none => (activeCourse.exercises.getD 0 default).name
+        match resolveStoredExercise activeCourse current with
+        | some exercise => exercise.id
+        | none =>
+          match activeCourse.exercises.findSome? (fun ex =>
+            if !completed.contains (key validCourse ex.id) then some ex.id else none) with
+          | some exerciseId => exerciseId
+          | none => (activeCourse.exercises.getD 0 default).id
       pure { currentCourse := validCourse, currentExercise := validCurrent, completed }
     | _ => pure (initial defaultCourse)
   catch _ =>
@@ -57,31 +95,31 @@ def save (state : AppState) : IO Unit := do
   IO.FS.writeFile stateFile content
 
 /-- Check if an exercise in the given course has been completed -/
-def isCompleted (state : AppState) (courseId name : String) : Bool :=
-  state.completed.contains (key courseId name)
+def isCompleted (state : AppState) (courseId exerciseId : String) : Bool :=
+  state.completed.contains (key courseId exerciseId)
 
 /-- Mark an exercise in the given course as completed -/
-def markCompleted (state : AppState) (courseId name : String) : AppState :=
-  let k := key courseId name
+def markCompleted (state : AppState) (courseId exerciseId : String) : AppState :=
+  let k := key courseId exerciseId
   if state.completed.contains k then state
   else { state with completed := state.completed.push k }
 
 /-- Mark an exercise as not completed (used by `reset`). -/
-def markIncomplete (state : AppState) (courseId name : String) : AppState :=
-  { state with completed := state.completed.filter (· != key courseId name) }
+def markIncomplete (state : AppState) (courseId exerciseId : String) : AppState :=
+  { state with completed := state.completed.filter (· != key courseId exerciseId) }
 
 /-- Switch the active course, moving to its first pending exercise. -/
 def switchCourse (state : AppState) (course : Course) : AppState :=
   let current := match course.exercises.findSome? (fun ex =>
-                   if !state.completed.contains (key course.id ex.name) then some ex.name else none) with
-                 | some name => name
-                 | none => (course.exercises.getD 0 default).name
+                   if !state.completed.contains (key course.id ex.id) then some ex.id else none) with
+                 | some exerciseId => exerciseId
+                 | none => (course.exercises.getD 0 default).id
   { state with currentCourse := course.id, currentExercise := current }
 
 /-- Find the next pending exercise in the given course -/
 def findNextPending (state : AppState) (course : Course) : Option String :=
   course.exercises.findSome? fun ex =>
-    if !state.completed.contains (key course.id ex.name) then some ex.name else none
+    if !state.completed.contains (key course.id ex.id) then some ex.id else none
 
 /-- Mark current exercise done and advance to next pending in the course -/
 def advance (state : AppState) (course : Course) : AppState :=
@@ -93,11 +131,11 @@ def advance (state : AppState) (course : Course) : AppState :=
 /-- Count completed exercises in the given course -/
 def countDone (state : AppState) (course : Course) : Nat :=
   course.exercises.foldl (fun n ex =>
-    if state.completed.contains (key course.id ex.name) then n + 1 else n) 0
+    if state.completed.contains (key course.id ex.id) then n + 1 else n) 0
 
 /-- Check if all exercises in the given course are done -/
 def allDone (state : AppState) (course : Course) : Bool :=
-  course.exercises.all (fun ex => state.completed.contains (key course.id ex.name))
+  course.exercises.all (fun ex => state.completed.contains (key course.id ex.id))
 
 end AppState
 end Leanlings