Multi-course support, Natural Number Game course, and intro-course fixes

.github/workflows/ci.yml

@@ -26,17 +26,28 @@ jobs:
       - name: Build
         run: lake build
 
-      - name: Verify all solutions
+      # 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
+      # exercise's hidden correctness checks (courses/intro/tests/), so the
+      # reference answers are verified to actually satisfy the `#guard`s.
+      - name: Verify intro solutions
         run: |
           failed=0
-          for f in .solutions/**/*.lean; do
-            if ! lean "$f" 2>&1; then
+          for f in $(find courses/intro/solutions -path '*/*.lean' | sort); do
+            rel=${f#courses/intro/solutions/}
+            test="courses/intro/tests/$rel"
+            tmp=$(mktemp /tmp/leanlings-XXXXXX.lean)
+            cat "$f" > "$tmp"
+            if [ -f "$test" ]; then printf '\n\n' >> "$tmp"; cat "$test" >> "$tmp"; fi
+            if ! lean "$tmp" 2>&1; then
               echo "FAIL: $f"
               failed=$((failed + 1))
             fi
+            rm -f "$tmp"
           done
           if [ $failed -gt 0 ]; then
             echo "$failed solution(s) failed"
             exit 1
           fi
-          echo "All solutions verified"
+          echo "All intro solutions verified against their checks"

.gitignore

@@ -1,2 +1,3 @@
 .lake/
 .leanlings-state
+.leanlings-check.lean

Leanlings.lean

@@ -1,4 +1,5 @@
 import Leanlings.Exercise
+import Leanlings.Course
 import Leanlings.UI
 import Leanlings.Runner
 import Leanlings.State

Leanlings/Course.lean

@@ -0,0 +1,37 @@
+import Leanlings.Exercise
+
+namespace Leanlings
+
+/-- A single course: a named, ordered collection of exercises that lives under
+`courses/<id>/`. Multiple courses can coexist; the active one is tracked in
+`AppState`. -/
+structure Course where
+  /-- Slug used both as the `courses/<id>/` directory name and the CLI selector. -/
+  id : String
+  /-- Human-readable title shown in listings. -/
+  title : String
+  /-- One-line summary shown in `courses`. -/
+  description : String
+  exercises : Array Exercise
+  /-- Shown when starting a course (progress at 0). -/
+  welcome : String := ""
+  /-- Shown when every exercise in the course is complete. -/
+  final : String := ""
+  deriving Inhabited
+
+/-- Build a course, stamping its `id` onto every exercise so each exercise can
+resolve its own file path without the caller threading the course through. -/
+def mkCourse (id title description : String) (exercises : Array Exercise)
+    (welcome : String := "") (final : String := "") : Course :=
+  { id, title, description,
+    exercises := exercises.map (fun e => { e with course := id }),
+    welcome, final }
+
+namespace Course
+
+/-- Find an exercise within this course by name. -/
+def getExercise (c : Course) (name : String) : Option Exercise :=
+  c.exercises.find? (·.name == name)
+
+end Course
+end Leanlings

Leanlings/Exercise.lean

@@ -11,16 +11,23 @@ inductive ExerciseStatus where
 structure Exercise where
   name : String := ""
   dir : String := ""
+  /-- The id of the course this exercise belongs to. Stamped by `mkCourse`. -/
+  course : String := ""
   hint : String := ""
   deriving Repr, BEq, Inhabited
 
 namespace Exercise
 
 def path (e : Exercise) : System.FilePath :=
-  s!"exercises/{e.dir}/{e.name}.lean"
+  s!"courses/{e.course}/exercises/{e.dir}/{e.name}.lean"
 
 def solutionPath (e : Exercise) : System.FilePath :=
-  s!".solutions/{e.dir}/{e.name}.lean"
+  s!"courses/{e.course}/solutions/{e.dir}/{e.name}.lean"
+
+/-- Hidden correctness checks (`#guard`s) for an exercise, kept out of the file
+the learner edits so the expected answers aren't given away. May not exist. -/
+def testPath (e : Exercise) : System.FilePath :=
+  s!"courses/{e.course}/tests/{e.dir}/{e.name}.lean"
 
 end Exercise
 end Leanlings

Leanlings/Runner.lean

@@ -6,22 +6,53 @@ namespace Leanlings.Runner
 private def containsSubstr (s sub : String) : Bool :=
   (s.splitOn sub).length > 1
 
-/-- Check a single exercise by running `lean` on it -/
-def checkExercise (exercise : Exercise) : IO ExerciseStatus := do
-  let output ← IO.Process.output {
-    cmd := "lean"
-    args := #[exercise.path.toString]
-  }
+/-- Run `lean` on a file via `lake env lean` (so course-library imports resolve)
+and classify the result. -/
+private def runLean (path : System.FilePath) : IO ExerciseStatus := do
+  let output ← IO.Process.output { cmd := "lake", args := #["env", "lean", path.toString] }
   -- Check for sorry first — if sorry is present, that's the primary issue
-  -- (test failures caused by sorry are noise the user doesn't need to see)
+  -- (test failures caused by sorry are noise the user doesn't need to see).
   if containsSubstr output.stderr "declaration uses `sorry`" ||
      containsSubstr output.stdout "declaration uses `sorry`" then
     return .hasSorry
-  -- No sorry — check for compilation or test errors
   if output.exitCode != 0 then
     return .compileError output.stderr
   return .success
 
+/-- Check a single exercise.
+
+Compiles via `lake env lean` so exercises that `import` a course library (e.g.
+the `nng` course's `MyNat` development) resolve against the built package; the
+`intro` course imports nothing and is unaffected. Requires `lake build` first.
+
+Correctness checks (`#guard`s) are kept in a hidden test file so the expected
+answers aren't shown to the learner. We check in two phases:
+
+1. Compile the exercise alone, so `sorry`/type errors are reported against the
+   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. -/
+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
+    | 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
+      | _ =>
+        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."
+  | other => return other
+
 /-- Display the result of checking an exercise -/
 def displayResult (exercise : Exercise) (status : ExerciseStatus) : IO Unit := do
   match status with

Leanlings/State.lean

@@ -1,9 +1,15 @@
 import Leanlings.Exercise
+import Leanlings.Course
 
 namespace Leanlings
 
-/-- Persistent state tracking exercise progress -/
+/-- 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
+within `currentCourse`. -/
 structure AppState where
+  currentCourse : String
   currentExercise : String
   completed : Array String
   deriving Repr
@@ -12,61 +18,82 @@ namespace AppState
 
 def stateFile : System.FilePath := ".leanlings-state"
 
-def initial (exercises : Array Exercise) : AppState :=
-  { currentExercise := (exercises.getD 0 default).name, completed := #[] }
+/-- The key under which an exercise's completion is recorded. -/
+def key (courseId name : String) : String := s!"{courseId}/{name}"
+
+def initial (course : Course) : AppState :=
+  { currentCourse := course.id,
+    currentExercise := (course.exercises.getD 0 default).name,
+    completed := #[] }
 
-/-- Load state from disk, or return initial state if no state file exists -/
-def load (exercises : Array Exercise) : IO AppState := do
+/-- 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
+default rather than failing. -/
+def load (courses : Array Course) (defaultCourse : Course) : IO AppState := do
   try
     let content ← IO.FS.readFile stateFile
     let lines := (content.splitOn "\n").filter (· != "")
     match lines with
-    | current :: rest =>
+    | course :: current :: rest =>
       let completed := (rest.filter (· != "---")).toArray
-      let validCompleted := completed.filter (fun name => exercises.any (·.name == name))
-      let validCurrent := if exercises.any (·.name == current) then current
-                          else match exercises.findSome? (fun ex => if !validCompleted.contains ex.name then some ex.name else none) with
-                               | some name => name
-                               | none => (exercises.getD 0 default).name
-      pure { currentExercise := validCurrent, completed := validCompleted }
-    | [] => pure (initial exercises)
+      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
+      pure { currentCourse := validCourse, currentExercise := validCurrent, completed }
+    | _ => pure (initial defaultCourse)
   catch _ =>
-    pure (initial exercises)
+    pure (initial defaultCourse)
 
 /-- Save state to disk -/
 def save (state : AppState) : IO Unit := do
   let completedStr := state.completed.foldl (fun acc s => acc ++ s ++ "\n") ""
-  let content := s!"{state.currentExercise}\n---\n{completedStr}"
+  let content := s!"{state.currentCourse}\n{state.currentExercise}\n---\n{completedStr}"
   IO.FS.writeFile stateFile content
 
-/-- Check if an exercise has been completed -/
-def isCompleted (state : AppState) (name : String) : Bool :=
-  state.completed.contains name
+/-- 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)
+
+/-- Mark an exercise in the given course as completed -/
+def markCompleted (state : AppState) (courseId name : String) : AppState :=
+  let k := key courseId name
+  if state.completed.contains k then state
+  else { state with completed := state.completed.push k }
 
-/-- Mark an exercise as completed -/
-def markCompleted (state : AppState) (name : String) : AppState :=
-  if state.completed.contains name then state
-  else { state with completed := state.completed.push name }
+/-- 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
+  { state with currentCourse := course.id, currentExercise := current }
 
-/-- Find the next pending exercise -/
-def findNextPending (state : AppState) (exercises : Array Exercise) : Option String :=
-  exercises.findSome? fun ex =>
-    if !state.completed.contains ex.name then some ex.name else none
+/-- 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
 
-/-- Mark current exercise done and advance to next pending -/
-def advance (state : AppState) (exercises : Array Exercise) : AppState :=
-  let state := state.markCompleted state.currentExercise
-  match state.findNextPending exercises with
+/-- Mark current exercise done and advance to next pending in the course -/
+def advance (state : AppState) (course : Course) : AppState :=
+  let state := state.markCompleted course.id state.currentExercise
+  match state.findNextPending course with
   | some next => { state with currentExercise := next }
   | none => state
 
-/-- Count completed exercises -/
-def countDone (state : AppState) : Nat :=
-  state.completed.size
+/-- 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
 
-/-- Check if all exercises are done -/
-def allDone (state : AppState) (exercises : Array Exercise) : Bool :=
-  exercises.all (fun ex => state.completed.contains ex.name)
+/-- 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))
 
 end AppState
 end Leanlings