diff --git a/CLAUDE.md b/CLAUDE.md new file mode 100644 index 0000000..587fa2a --- /dev/null +++ b/CLAUDE.md @@ -0,0 +1,71 @@ +# CLAUDE.md + +This file provides guidance to Claude Code (claude.ai/code) when working with code in this repository. + +## Was das Repository ist + +Kursnotizen „Algebra in Lean“ zur Vorlesung *Algebra und Zahlentheorie* +(Stefan Kebekus, Universität Freiburg). Ausgewählte Beweise des Skripts werden +*Satz für Satz* nach Lean 4 / Mathlib übersetzt: der deutsche Originalsatz +steht als Zitat bzw. Kommentar direkt über dem Lean-Code. Jedes Kapitel endet +mit einer Übungsaufgabe, deren `sorry` die Studierenden ersetzen sollen. + +**Die Prosa ist deutsch.** Kommentare, Aufgabentexte und Kapitelnamen auf +Deutsch schreiben; Lemma- und Theoremnamen ebenfalls deutsch +(`neutral_eindeutig`, `gradformel`). + +## Befehle + +```bash +lake exe cache get # Mathlib-Cache holen (vor dem ersten Build!) +lake build # Übungsdateien + Buch elaborieren +lake exe algebrainlean --output _out # Buch nach _out/html-multi rendern +python3 -m http.server 8000 -d _out/html-multi +./deploy.sh # baut und rsynct nach cplx.vm.uni-freiburg.de +``` + +Einzelne Datei prüfen: `lake build AlgebraInLean.Degrees` bzw. `lake build Book.Degrees`. +Es gibt keine Testsuite — „Test“ heißt: `lake build` läuft ohne Fehler durch. +Fehlende Beweise sind absichtliche `sorry`s (Warnung, kein Fehler). + +## Doppelstruktur: `AlgebraInLean/` ↔ `Book/` + +Jedes Kapitel existiert **zweimal**, mit demselben Dateinamen: + +* `AlgebraInLean/X.lean` — die Übungsdatei, die Studierende in VS Code öffnen. + `import Mathlib` (bequem), `namespace AlgebraInLean`, Prosa in `/-! … -/`. +* `Book/X.lean` — dasselbe Material als [Verso](https://github.com/leanprover/verso)-Kapitel. + Prosa als Verso-Markup, Lean-Code in ```` ```lean ````-Blöcken, die beim Build + **mitelaboriert** werden — die gerenderten Beweise kompilieren also garantiert. + +Wer Mathematik ändert, muss **beide Seiten anfassen**; sie driften sonst +auseinander. Neue Kapitel zusätzlich in `AlgebraInLean.lean` (Import) und +`Book.lean` (Import + `{include 0 Book.X}`) eintragen, und die Tabelle in +`README.md` ergänzen (dort fehlen derzeit `Elements` und `Transitivity`). + +Konventionen in `Book/`: + +* Kopf jeder Datei: `import VersoManual`, `import Manual.Meta`, dann + **Minimal-Imports** von Mathlib (mit `#min_imports` ermittelt) statt + `import Mathlib` — das hält den Buch-Build erträglich schnell. +* `set_option pp.rawOnError true` und `set_option verso.docstring.allowMissing true`. +* `#doc (Manual) "Titel" =>` mit `%%%`-Block: `htmlSplit := .never`, + `tag`/`file` als deutscher URL-Slug (`gradformel`, `reziprozitaet`, …). + `file` bestimmt den Pfad in `_out/html-multi/`; Slugs nicht nachträglich + ändern, sonst brechen Links auf dem Server. +* Mathe im Verso-Dialekt: `$`…`` inline, `` $$`…` `` abgesetzt. + +## Build-Setup + +* Toolchain in `lean-toolchain` ist verbindlich (`v4.33.0-rc2`). +* `lakefile.lean`: Reihenfolge der `require`s ist bewusst — `verso-manual` + (aus dem Lean-Reference-Manual-Repo, das seinerseits die passende + Verso-Nightly pinnt) **vor** Mathlib, damit Mathlibs Pins der geteilten + Abhängigkeiten gewinnen; sonst verweigert `lake exe cache get` den Dienst. + Verso wird nicht direkt required. +* `Main.lean` konfiguriert die Ausgabe: nur Multi-Page-HTML, kein TeX, eigene + CSS/JS aus `static/` (Theme folgt Pfaffelhubers *leancourse*). KaTeX bringt + Verso selbst mit — keine zweite Kopie einbinden, sonst wird jede Formel + doppelt gerendert. +* `.lake/`, `_out/` und `public/` sind nicht versioniert; `public/` ist die + ausgelieferte Kopie der Build-Ausgabe.