Multi-course support, Natural Number Game course, and intro-course fixes - #12
Merged
Conversation
Restructure leanlings around courses so more than one progression can
coexist. The exercise/solution files move under courses/intro/, and the
tooling is taught the new layout.
- Exercise gains a `course` field; path/solutionPath resolve to
courses/<course>/{exercises,solutions}/...
- New Course abstraction (Leanlings/Course.lean) with a mkCourse smart
constructor that stamps the course id onto each exercise.
- Config wraps the 70 exercises as the `intro` course and exposes
courses/defaultCourse/getCourse.
- AppState is course-aware: tracks currentCourse and namespaces completed
entries as "<course>/<name>" so per-course progress never collides.
- Main threads the active course through every command and adds
`courses` (list) and `course <id>` (switch); reset hint now points at
the real solution path.
- CI verifies solutions via courses/*/solutions/*/*.lean.
- README documents the course layout and new commands.
Bump from v4.28.0 to the latest stable release. leanlings has no dependencies (no Mathlib), so the upgrade is self-contained: the tool builds clean and all 70 exercise solutions still compile under v4.30.0.
…low-up) Port the Natural Number Game (leanprover-community/NNG4, Apache-2.0) into leanlings as a second course, with no Mathlib or GameServer dependency. Foundation (courses/nng/solutions/MyNatLib/, pure core Lean): - MyNat: an axiomatic Peano development of ℕ — type, opaque +/*/^ with their recursion-equation axioms, order (≤/<), and the Peano API (succ_inj, pred, zero_ne_succ), plus DecidableEq. - Core-only reimplementations of the tactic conveniences the levels need: lean3-style `induction … with d hd` and `cases … with` (via rec'/casesOn', handling dependent hypotheses), `use`, `apply … at` (a unifying elaborator), `nth_rewrite`, and `symm at`. Content: all 78 live levels across 9 worlds (Tutorial → Algorithm), each converted from the GameServer DSL into a leanlings exercise (the level's Introduction preserved as a comment) plus a reference solution. The solutions form one import-chain compiled as a Lean library, so `lake build` verifies every one. A handful of proofs that used Mathlib-only tactics (tauto/contrapose/decide) were rewritten in core Lean. The joke "FLT" level (solved by a sorry-cheat) is omitted. Tooling: - lakefile: the nng solutions are a `lean_lib` (default target). - Runner now checks exercises via `lake env lean` so course-library imports resolve. The intro course (no imports) is unaffected. - Config registers the `nng` course alongside `intro`. - CI verifies nng solutions via `lake build`; the file-by-file loop now covers only the standalone intro solutions. Licensing: courses/nng/ vendors NNG's Apache-2.0 LICENSE and adds a NOTICE stating the modifications; every ported file carries a provenance header.
#7 Hide the answers: move every exercise's `#guard` correctness checks out of the file the learner edits into a hidden courses/intro/tests/ tree (39 files). The Runner now checks in two phases — compile the exercise alone (so sorry/type errors report against the real file with correct line numbers), then, if clean, compile it together with the hidden checks, reporting a friendly "doesn't satisfy the checks yet" message instead of revealing them. CI now compiles each intro solution together with its hidden checks, so reference answers are verified to actually satisfy the guards (they weren't before — this caught two latent bugs, fixed below). #9 exists1: the instructions told learners to use `use`, which isn't in core Lean (it's a Mathlib tactic). Teach the core anonymous constructor `exact ⟨w, p⟩` / `refine ⟨w, ?_⟩` instead, and note where `use` comes from. #8 tactics3: `rewrite_back` was solvable with a forward `rw [h]`. Redesigned so the goal is about `b` while the extra fact is about `a`, forcing `rw [← h]`. #5 have1: the `double_neg_intro` solution didn't use `have` despite the instructions. It now names the contradiction with `have contra : False := hn hp`, and the exercise gives a step-by-step hint. #6 intro3: the first Bool exercise now tells the learner the Bool values are `true` and `false` (they hadn't been introduced yet). Latent bugs surfaced by verifying solutions against their checks: - 13_quiz/quiz1: solution carried a duplicate copy of the test fixtures; removed (the hidden test file owns them now). - 14_do_notation/do2: the guards compared `Except String Int` with `==` but no `BEq` instance existed (previously masked by `sorry`); the test now provides one.
# Conflicts: # courses/intro/exercises/14_do_notation/do2.lean
This was referenced Jun 2, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This branch turns leanlings into a multi-course tool, adds a second course (a Mathlib-free port of the Natural Number Game), upgrades the Lean toolchain, and resolves the outstanding intro-course feedback.
Closes #3, #5, #6, #7, #8, #9.
Commits
courses/<id>/; aCourseabstraction, per-course progress, andcourses/course <id>CLI commands.introis the default.nngcourse — all 78 live levels across 9 worlds, ported from NNG4 (Apache-2.0).MyNatis a from-scratch axiomatic Peano development in pure core Lean; the tactics NNG borrows from Mathlib (induction … with,cases … with,use,apply … at,nth_rewrite,symm at) are reimplemented in core. Solutions form one Lean library, solake buildverifies every one.double_neg_introin21_cases_have/have1.leandoes not usehave#5–Onexists1:usedoesn't work. #9) — see below.Issues addressed
nngadded as a second course.exists1:usedoesn't work. #9usedoesn't work in exists1 —useisn't core Lean (it's Mathlib); exists1 now teaches the core anonymous constructor⟨w, p⟩/refine ⟨w, ?_⟩.tactics3, you don't need to use backwards rewriting for the third solution #8 tactics3 backward rewrite not forced —rewrite_backredesigned sorw [← h]is genuinely required.double_neg_introin21_cases_have/have1.leandoes not usehave#5 have1 solution doesn't usehave— solution now names the contradiction withhave contra : False := hn hp.true/false.#guardblock moved out of exercise files into a hiddencourses/intro/tests/tree; the Runner checks in two phases and reports a friendly message on a failed hidden check instead of revealing it. CI now verifies each solution against its hidden checks (it didn't before — this caught two latent bugs, both fixed).Verification
lake buildclean (tool + thenngsolution library = all 78 nng solutions verified).sorrywith no errors.courses,course,run,solution).Notes / caveats
courses/nng/vendors NNG's Apache-2.0LICENSEand aNOTICEstating the modifications; every ported file carries a provenance header.nnghints still reference tactics that were substituted away (contrapose!,simp_add) — cosmetic, since each exercise's full intro comment is the real guidance.