docs: style guides, contributor guide, and a student README

CLAUDE.md

@@ -64,11 +64,20 @@ AI-usage disclosure paragraph at the end of commit messages is important wheneve
 When migrating material, AI should try to translate (English to Portuguese) but not rewrite or invent new text. Only humans should deviate from the original CSwFP texts.
 
 
-# Pedagogical decisions
-
-We will avoid fragmented presentation of material. That is why we will largely reorder CSwFP.
-
-We should avoid presenting definitions that will be rephrased later, with the same name that in another chapter would have a new definition. Eventually, namespaces would avoid conflicts, but students may get confused. But exceptions can occur.
-
-We will never discuss `haskell vs Lean` decisions in the book. The reader does not necessarily know Haskell and should not worry about it. We also do not expect the reader to have read the original CSwFP. This book is self-contained. As a result, we never mention CSwFP sections, pages, etc.
+# Style guides
+
+The normative conventions live in two files, which are to be read in addition
+to this one. **Read both in full before creating or editing any file that ends
+up in the book**; everything you write must conform to them.
+
+- `STYLE-CODE.md` — Lean code and Verso markup: the ledger of which Lean
+  feature is first used in which chapter (the book's hard constraint is that
+  nothing is used before it is presented), the directive vocabulary, the build
+  variants, and naming.
+- `STYLE-WRITING.md` — prose: the project's pedagogical decisions, writing
+  advice, and the Portuguese conventions including the term list.
+
+`CONTRIBUTING.md` covers workflow. `DEVIATIONS.md` records what departs from
+CSwFP and why. In case of conflict, the style guides win on style and this
+file wins on project scope.
 

CONTRIBUTING.md

@@ -0,0 +1,107 @@
+# Contributing to CSwL
+
+This file covers workflow and mechanics. For conventions, read `STYLE-CODE.md`
+(Lean and Verso) and `STYLE-WRITING.md` (prose and Portuguese) — both are
+normative, and both should be read before you edit anything that reaches the
+book.
+
+Everything about the project is in English: this file, identifiers, code
+comments, commit messages, issues. Only the book's prose is in Portuguese.
+
+## Who decides what
+
+The book's content and its structure — what a chapter says, what order the
+material comes in, which exercises exist, how chapters are divided — are the
+author's. Contributions are welcome on everything else, and are most valuable
+where a task is objective:
+
+- reporting anything that does not build, or builds with an unexpected warning;
+- reporting prose that is wrong, unclear, or badly translated;
+- working the exercises and reporting those that are unsolvable, ambiguous, or
+  mis-rated;
+- checking that a chapter uses no Lean feature the book has not yet presented
+  (`STYLE-CODE.md` has the ledger);
+- fixes to typos, markup slips, and broken references.
+
+A change that reorganizes material, adds or removes an exercise, or introduces
+a Lean feature earlier than the ledger records is a proposal, not a fix: open
+an issue and let the author decide.
+
+## Getting set up
+
+Install Lean via [elan](https://lean-lang.org/install), then clone the
+repository and fetch the prebuilt Mathlib — without this, `lake build`
+compiles all of Mathlib from scratch:
+
+```sh
+lake exe cache get
+lake build
+```
+
+Use VS Code with the Lean 4 extension. Opening any file under `CSwL/` will
+prompt to install the toolchain the book pins.
+
+To build and read the book locally:
+
+```sh
+make serve   # http://127.0.0.1:8000/
+```
+
+`make all` generates all four variants under `_out/`. See `STYLE-CODE.md` for
+what each variant is.
+
+## Issues
+
+Pending work is tracked in [GitHub
+issues](https://github.com/cslib-community/CSwL/issues). Anything you find that
+you are not fixing yourself belongs there.
+
+For a comment that is local to one passage and only makes sense with that
+section in view, use a `:::dev` note in the Lean file itself rather than an
+issue. Those render as editorial notes and never reach the student.
+
+## Branches and pull requests
+
+- `main` must always build.
+- Do not commit to `main`; work on a branch and open a pull request.
+- Keep a pull request to one coherent piece of work. Smaller and sooner beats
+  bigger and later.
+- Before opening it, check that what you touched still builds — `lake build
+  CSwL.Sets` for a single chapter, `make all` if you changed the
+  infrastructure or anything that affects the generated variants.
+- Delete the branch once it is merged.
+
+Commit messages follow [Conventional
+Commits](https://www.conventionalcommits.org/): `feat:`, `fix:`, `docs:`,
+`refactor:`, with an optional scope — `docs(readme): …`, `fix(logic): …`.
+
+## Editing the right file
+
+The book's sources are the Lean files under `CSwL/`. Everything under `_out/`
+is generated and is overwritten by the next `make` — never edit there.
+
+That includes the generated projects' `README.md`, which comes from
+`readmeTemplate` in `CSwLMeta/Save/Project.lean`.
+
+## AI usage
+
+AI may be used in this project, under conditions that differ from the ones
+some related projects adopt. The rules:
+
+- **AI never writes prose on its own initiative.** It produces text only when
+  explicitly asked, and what it produces is a draft for a human to revise.
+- **When migrating material, AI translates.** English to Portuguese, as
+  literally as the target language allows. It does not rewrite, expand,
+  restructure, or invent. Deviating from the source is a human decision.
+- **AI-generated commentary is marked as such**, and belongs in `:::dev`
+  blocks, which never reach the student.
+- **Infrastructure is different.** Code under `CSwLMeta/` and the scripts
+  around the build are not book content, and AI may write them — but a file
+  that is mostly AI-written says so at the top, because it will typically be
+  less carefully considered than hand-written code.
+- **Commit messages** that describe AI-assisted work carry a disclosure
+  paragraph in English, added only after a human approves it. Never
+  `Co-Authored-By: Claude`.
+
+`CLAUDE.md` holds the instructions Claude Code reads at the start of a
+session; it points at this file and the two style guides.

CSwL/Logic/FOL.lean

@@ -5,6 +5,8 @@ import Mathlib.Tactic.Use
 open Verso.Genre Manual
 open CSwLMeta
 
+set_option verso.code.warnLineLength 100
+
 #doc (Manual) "Lógica de predicados" =>
 %%%
 tag := "FOL"
@@ -57,8 +59,8 @@ arbitrário e prove que vale para ele. É a mesma `intro` agora sobre um objeto
 
 ```lean
 example (h : ∀ x, P x) : ∀ y, P y := by
-  intro y
-  exact h y
+  intro n
+  exact h n
 ```
 
 A introdução de `∃` exige exibir a testemunha. A tática `use` substitui a variável quantificada pelo objeto passado, e deixa como objetivo o que falta provar sobre ele.

CSwL/Logic/PL.lean

@@ -19,9 +19,9 @@ namespace PL
 
 # Introdução
 
-A lógica proposicional (LP, ou cálculo sentencial) trata de fórmulas construídas a partir de variáveis proposicionais usando os conectivos `¬`, `∧`, `∨`, `→` e `↔`. Intuitivamente, uma variável proposicional `p` representa uma sentença ou proposição que pode ser verdadeira ou falsa. Queremos usar lógica proposicional para fugir das impressões das línguas naturais. Formalizar proposições e provas quando podemos concluir uma proposição a partir de outras proposições tomadas como premissas.
+A lógica proposicional (PL, "Propositional Logic") trata de fórmulas construídas a partir de variáveis proposicionais usando os conectivos `¬`, `∧`, `∨`, `→` e `↔`. Intuitivamente, uma variável proposicional `p` representa uma sentença ou proposição que pode ser verdadeira ou falsa. Podemos usar lógica proposicional para fugir das impressões das línguas naturais. Queremos tornar precisa a noção de que uma proposição `α` decorre de outra proposição `β`.
 
-Como primeiro exemplo, adaptado de {citet Bib.enderton2001}[], a sentença "traços de potássio foram observados" pode ser traduzida para a linguagem formal como o símbolo `K`. Já para a sentença fortemente relacionada "traços de potássio não foram observados", podemos usar `¬ K`. Aqui `¬` é o nosso símbolo de negação, lido como "não". Poderíamos também pensar em traduzir "traços de potássio não foram observados" por algum símbolo novo `J`, mas preferimos decompor sentenças em suas partes atômicas tanto quanto possível. Para uma sentença não relacionada, "a amostra continha cloro" escolhemos o símbolo `C`. Assim, as seguintes sentenças compostas podem ser formalizadas.
+Como primeiro exemplo, adaptado de {citet Bib.enderton2001}[], a sentença "traços de potássio foram observados" pode ser traduzida para a linguagem formal como o símbolo `K`. Já para a sentença relacionada "traços de potássio não foram observados", podemos usar `¬ K`. Aqui `¬` é o nosso símbolo de negação, lido como "não". Poderíamos também pensar em traduzir "traços de potássio não foram observados" por algum símbolo novo `J`, mas preferimos decompor sentenças em suas partes atômicas tanto quanto possível. Para uma sentença não relacionada, "a amostra continha cloro" escolhemos o símbolo `C`. Assim, as seguintes sentenças compostas podem ser formalizadas.
 
 - A sentença "Se traços de potássio foram observados, então a amostra não continha cloro." é formalizada como `(K → (¬C))` com símbolo `→` significando "se ... então ...".
 - A sentença "A amostra continha cloro, e traços de potássio foram observados." é formalizada como `(C ∧ K)` com símbolo `∧` significando a conjunção "e".

CSwL/Sets.lean

@@ -583,6 +583,10 @@ modelo a um fragmento — um domínio de entidades e, para cada verbo, a
 relação que ele denota — e à qual o tratamento de verbos de mais de dois
 lugares, e do escopo entre eles, volta mais tarde.
 
+:::dev "Alexandre (arademaker)"
+Estamos apresentando conceitos dentro do enunciado de um exercício. Talvez seja melhor evitar isso.
+:::
+
 ::::exercise (rating := 2) (name := "cartesian-square")
 
 Tome `A` como o conjunto `{Kasparov, Karpov, Anand}`. Encontre `A × A`.

CSwLMeta/Comment.lean

@@ -77,10 +77,13 @@ def decodeDevData? (data : Json) : Option (Option String × Option String × Opt
     some (str? a, str? u, nat? y)
   | _ => none
 
-/-- Should a dev note surface in reader-facing outputs (the HTML book and the
-generated `.lean` files)?  Only *actionable* notes are shown: those with urgency
-`NOW` or `BeforeNextRelease`, or with no urgency at all.  `PotentialImprovement`
-notes remain suppressed. -/
+/-- Should a dev note be rendered at all, in the variants that keep it (every
+one but `student`)?  Only *actionable* notes are: those with urgency `NOW` or
+`BeforeNextRelease`, or with no urgency at all.  `PotentialImprovement` notes
+remain suppressed.
+
+This is the second of two filters and is about urgency alone; which variants
+keep a note is decided in `Block.devcomment`'s `traverse`. -/
 def devNoteShown (urgency : Option String) : Bool :=
   match urgency with
   | none => true
@@ -98,26 +101,39 @@ def devUrgencyText (urgency : String) : String :=
 /-- Label for a rendered dev note —
 `Nota editorial (Alexandre Rademaker, before next release, 2026)` — with
 absent fields omitted.  The heading names the note without naming the source
-this book adapts: `CSwL` is self-contained, and a rendered note reaches every
-variant, the student one included. -/
+this book adapts, since `CSwL` is self-contained: the note does not reach the
+student build, but it does reach the `terse` one the instructor opens in
+class. -/
 def devNoteLabel (author urgency : Option String) (year : Option Nat)
     (heading : String := "Nota editorial") : String :=
   let fields := author.toList ++ (urgency.map devUrgencyText).toList ++ (year.map toString).toList
   if fields.isEmpty then heading
   else s!"{heading} ({String.intercalate ", " fields})"
 
 /-! `Block.devcomment` carries the note body as its children and records its
-author/urgency metadata in `data`. All notes survive traversal (the CSwL has
-no student/solutions split on this block — every variant is a "reader" of the
-book). Among the surviving blocks, a note is rendered only when its urgency
-passes `devNoteShown` (`NOW`, `BeforeNextRelease`, or none): highlighted in the
-HTML book, and passed through as a labelled comment in generated `.lean` files
-by `CSwLMeta.Save.Extract.walkBlock`.  `PotentialImprovement` notes render
+author/urgency metadata in `data`.
+
+A dev note is addressed to the book's authors, so **no note survives traversal
+in the `student` variant** — neither the HTML nor the generated `.lean`, since
+both are produced from the per-variant traversed tree. The other three
+variants keep every note: `solutions` and `grading` are the authors' own, and
+`terse` is the instructor's, where a note on screen during a class is
+harmless.
+
+Among the surviving blocks, a note is rendered only when its urgency passes
+`devNoteShown` (`NOW`, `BeforeNextRelease`, or none): highlighted in the HTML
+book, and passed through as a labelled comment in generated `.lean` files by
+`CSwLMeta.Save.Extract.walkBlock`.  `PotentialImprovement` notes render
 nothing. -/
 block_extension Block.devcomment (author : Option String)
     (urgency : Option String) (year : Option Nat) where
   data := Json.arr #[toJson author, toJson urgency, toJson year]
-  traverse _ _ _ := return none
+  traverse _ _ _ := do
+    if (← getCurrVariant).isStudent then
+      -- Dev notes are for the authors; the student build gets none of them.
+      return some (.concat #[])
+    else
+      return none
   toHtml :=
     open Verso.Output.Html in
     some fun _ goB _ data contents => do

CSwLMeta/Save/Project.lean

@@ -112,15 +112,49 @@ private def lakefileTemplate (vol : String) (v : Variant)
   "name = \"" ++ vol ++ "\"\n" ++
   libs
 
+/-- The `student` variant is the one the students receive, so its README is the
+  whole set-up guide: how to build, how to work an exercise, how to report a
+  problem. The `solutions` and `terse` variants are read by the instructor, who
+  has the repository itself, and get only the note saying where they came from.
+  The `grading` variant gets additional instructions for its private autograder
+  below. Written in English, like every other document about the project; only
+  the book's prose is in Portuguese. -/
 private def readmeTemplate (vol : String) (v : Variant) : String :=
-  s!"# {vol} — variante `{v}`\n\n" ++
-  "Gerado a partir do livro (Verso, gênero `Manual`) por " ++
-  s!"`lake exe cswl-book {v}` — **não edite aqui**: a fonte é o `CSwL`.\n\n" ++
-  (if v.isGrading then
-    "Esta variante traz as provas completas e os atributos " ++
-    "`[autogradedProof …]`. Para corrigir uma entrega:\n\n" ++
-    "    lake exe autograder --local <entrega> <arquivo deste projeto>\n\n" ++
-    "Ela nunca sai do repositório privado.\n"
+  s!"# {vol} — `{v}` variant\n\n" ++
+  "Generated from the book (Verso, `Manual` genre) by " ++
+  s!"`lake exe cswl-book {v}` — **do not edit here**: the source is `{vol}`, " ++
+  "and the next build overwrites this directory.\n\n" ++
+  (if v.isStudent then
+    "## Setting up\n\n" ++
+    "Install Lean with [elan](https://lean-lang.org/install). Then, in this\n" ++
+    "directory, fetch the prebuilt Mathlib and build:\n\n" ++
+    "    lake exe cache get\n" ++
+    "    lake build\n\n" ++
+    "`lake exe cache get` matters: without it, `lake build` compiles all of\n" ++
+    "Mathlib from scratch.\n\n" ++
+    "Use VS Code with the Lean 4 extension, and open **this directory** as\n" ++
+    "the folder — not a file inside it, or the extension will not find the\n" ++
+    "project.\n\n" ++
+    "## Working the exercises\n\n" ++
+    "Each exercise is a `sorry` to replace. Lean checks your answer as you\n" ++
+    "type: while a `sorry` remains, the file reports a warning, and when the\n" ++
+    "proof or definition is complete the warning disappears. The InfoView\n" ++
+    "panel shows the goal at the cursor.\n\n" ++
+    "The exercises are in the same order as the book, and each one sits in\n" ++
+    "the chapter section that discusses it. Read the corresponding section\n" ++
+    "of the book alongside the code.\n\n" ++
+    "Keep your own copy of anything you want to survive: this directory is\n" ++
+    "regenerated from the book, and a rebuild overwrites whatever is here.\n\n" ++
+    "## Reporting a problem\n\n" ++
+    "If something does not build, a statement is ambiguous, or the prose is\n" ++
+    "wrong, open an issue at\n" ++
+    "<https://github.com/cslib-community/CSwL/issues>. Say which chapter and\n" ++
+    "which exercise, and paste the message Lean gave you.\n"
+   else if v.isGrading then
+    "This variant carries the complete proofs and the `[autogradedProof …]`\n" ++
+    "attributes. To grade a submission:\n\n" ++
+    "    lake exe autograder --local <submission> <file in this project>\n\n" ++
+    "It never leaves the private repository.\n"
    else "")
 
 /-- Writes the generated project to `dest`: the extracted files, plus

DEVIATIONS.md

@@ -61,7 +61,7 @@ The exception: `IntroCS.lean`, described in that chapter's section below.
 Everywhere else, a construct in a code block is one an earlier chapter has
 presented.
 
-This document is the migration plan: which CSwFP sections each `CSwL` chapter consumes, in which order, and what each chapter presupposes. The order below is the book's order; the dependency columns are what justify it. Everything through CSwFP/6 is settled — where a section records a decision, that decision is made, not proposed. What remains is execution, tracked in `TODO.md`. Exercise-level correspondence with CSwFP is in `PROVENANCE.md`.
+This document is the migration plan: which CSwFP sections each `CSwL` chapter consumes, in which order, and what each chapter presupposes. The order below is the book's order; the dependency columns are what justify it. Everything through CSwFP/6 is settled — where a section records a decision, that decision is made, not proposed. What remains is execution, tracked in [GitHub issues](https://github.com/cslib-community/CSwL/issues). Exercise-level correspondence with CSwFP is in `PROVENANCE.md`.
 
 The current state of CSwL need major review to fulfill all decisions from this document.
 
@@ -353,7 +353,7 @@ CSwFP/7 (The Composition of Meaning in Natural Language) goes after `ModelChecki
 
 A proof system as data — CSLib's `Cslib.Logic.PL.Theory.Derivation` — is deferred rather than rejected, for the reasons in the `Logic.lean` section. It becomes attractive exactly where `CSwL` would have something to give back: CSLib has the derivations but no propositional semantics, and this book builds the valuation. Soundness — every derivable sequent is true under every valuation satisfying its context — needs both halves, and neither project has both today. `Cslib/Logics/README.md` invites exactly this ("we are interested in expanding them or creating new ones that can cover your use cases"). Its natural place is after `Sets.lean`, once relations and quantifiers are available. It stays out of the plan until CSwFP/1–6 are in place.
 
-Mathlib's `ContextFreeGrammar` for the grammars of `Games.lean` is deferred on the same footing, and for reasons that are ours rather than the library's — see "Reusing Mathlib and CSLib". It is the one deferred item that would change a chapter already written, so it belongs after the pending work in `TODO.md`, not before it.
+Mathlib's `ContextFreeGrammar` for the grammars of `Games.lean` is deferred on the same footing, and for reasons that are ours rather than the library's — see "Reusing Mathlib and CSLib". It is the one deferred item that would change a chapter already written, so it belongs after the pending work already tracked, not before it.
 
 The related question — whether `PL.lean`'s valuation is written in CSLib's shape from the start — is settled above, and settled against it.