forked from EduCraft/curriculum-project-hub
chore: remove Lean spec; ADRs are the single source of truth
The spec/ Lean semantic master had no conformance gate, no codegen, and no CI tie to implementations — alignment was carried entirely by human review, the same mechanism that carries the ADRs. In practice the ADRs plus greppable code comments were already the load-bearing artifacts, so spec/ was the most expensive kind of stale documentation. - delete spec/ and the spec-check CI workflow - README: constitution rewritten around ADRs as decision truth - AGENTS.md/CLAUDE.md: discipline re-anchored (new decisions -> new ADR, never rewrite ADR history; supersede instead) - code comments: re-anchor 'Mirrors Spec.X' invariants to ADR numbers (cph-diag, cph-check, cph-model, hub runner/capacity/org, prisma) - leave ADR bodies and .scratch audit snapshots untouched (history); fix live references in open readiness tickets
This commit is contained in:
+25
-38
@@ -3,9 +3,7 @@
|
||||
//! This crate is the **loader**, not the full checker. It reads
|
||||
//! `<root>/manifest.toml` (project / info / ordered `[[parts]]` / declared
|
||||
//! `[targets.*]`) and each part's `<root>/<path>/element.toml`, and produces an
|
||||
//! ordered [`Lesson`] — mirroring the Lean master's `Lesson = List (Element P)`
|
||||
//! (`spec/Spec/Courseware/Model/Lesson.lean`), where the order of `parts` carries
|
||||
//! teaching semantics.
|
||||
//! ordered [`Lesson`], where the order of `parts` carries teaching semantics.
|
||||
//!
|
||||
//! Scope boundaries (deliberately staying in lane):
|
||||
//! - It validates **structure** only: manifest shape, element.toml shape, and
|
||||
@@ -23,7 +21,7 @@ use serde::{Deserialize, Serialize};
|
||||
|
||||
/// An ordered, in-memory lesson loaded from an engineering file.
|
||||
///
|
||||
/// Mirrors the Lean master's `Lesson = List (Element P)`: `parts` is an ordered
|
||||
/// `parts` is an ordered
|
||||
/// `Vec`, and that order is the lesson's order (ADR-0008 §"the lesson manifest
|
||||
/// is declarative" — the `[[parts]]` array order is the single source of truth).
|
||||
#[derive(Debug, Clone, PartialEq, Serialize)]
|
||||
@@ -86,9 +84,8 @@ pub struct TargetConfig {
|
||||
/// with template `exports/<name>.typ` when no `[[steps]]` are given.
|
||||
pub steps: Vec<Step>,
|
||||
/// The **render-coverage declaration**: which element kinds this target
|
||||
/// renders. Realizes `Spec.Courseware.TargetSpec.covers : KindId → Prop`
|
||||
/// (`spec/Spec/Courseware/Export/Render.lean`) and ADR-0011's "render
|
||||
/// coverage is a declaration, not a payload": the contract keeps *which
|
||||
/// renders. Realizes ADR-0011's "render
|
||||
/// coverage is a declaration, not a payload": the declaration keeps *which
|
||||
/// kinds a target renders* (used by the `renderIgnored` seed diagnostic),
|
||||
/// while the rendering "how" lives in the template/steps.
|
||||
///
|
||||
@@ -102,13 +99,10 @@ pub struct TargetConfig {
|
||||
|
||||
/// The artifact an export target produces (ADR-0009/0011).
|
||||
///
|
||||
/// **Mirrors `Spec.Courseware.Artifact`** in the Lean semantic master
|
||||
/// (`spec/Spec/Courseware/Export/Artifact.lean`), whose definition is exactly:
|
||||
/// **Pinned by ADR-0011** as an ADT with fields:
|
||||
///
|
||||
/// ```text
|
||||
/// inductive Artifact where
|
||||
/// | singleFile (filepath : String)
|
||||
/// | fileTree (root : String) (outputs : String)
|
||||
/// Artifact = singleFile (filepath) | fileTree (root, outputs)
|
||||
/// ```
|
||||
///
|
||||
/// ADR-0011 pinned the artifact as an ADT **with fields**: "what the product
|
||||
@@ -120,20 +114,20 @@ pub struct TargetConfig {
|
||||
/// `"single-file"` → [`Artifact::SingleFile`], `"file-tree"` →
|
||||
/// [`Artifact::FileTree`].
|
||||
///
|
||||
/// As with `cph-diag`'s `Severity`, there is no CI gate enforcing this
|
||||
/// alignment (see the repo constitution) — it is maintained by review, which is
|
||||
/// why the correspondence is documented here.
|
||||
/// As with `cph-diag`'s `Severity`, there is no CI gate enforcing ADR↔
|
||||
/// implementation alignment (see the repo constitution) — it is maintained by
|
||||
/// review, which is why the decision is documented here.
|
||||
#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
|
||||
pub enum Artifact {
|
||||
/// One bundled document landing at `filepath` (relative to the engineering
|
||||
/// root). Mirrors Lean `Artifact.singleFile`. The default artifact shape.
|
||||
/// root). ADR-0011 `singleFile`. The default artifact shape.
|
||||
SingleFile {
|
||||
/// Where the single product is written (relative to the engineering
|
||||
/// root), e.g. `build/student.pdf`.
|
||||
filepath: PathBuf,
|
||||
},
|
||||
/// A set of files under `root` matching the `outputs` glob. Mirrors Lean
|
||||
/// `Artifact.fileTree`.
|
||||
/// A set of files under `root` matching the `outputs` glob. ADR-0011
|
||||
/// `fileTree`.
|
||||
FileTree {
|
||||
/// The output directory (relative to the engineering root).
|
||||
root: PathBuf,
|
||||
@@ -156,14 +150,10 @@ impl Artifact {
|
||||
|
||||
/// One typed build step (ADR-0011).
|
||||
///
|
||||
/// **Mirrors `Spec.Courseware.Step`** in the Lean semantic master
|
||||
/// (`spec/Spec/Courseware/Export/Render.lean`), whose definition is exactly:
|
||||
/// **Pinned by ADR-0011** as an ADT:
|
||||
///
|
||||
/// ```text
|
||||
/// inductive Step where
|
||||
/// | typstCompile (template : String)
|
||||
/// | shell (run : String)
|
||||
/// | assembleMarkdown (field : String)
|
||||
/// Step = typstCompile (template) | shell (run) | assembleMarkdown (field)
|
||||
/// ```
|
||||
///
|
||||
/// A step is a *typed* operation (extensible): `TypstCompile` compiles a
|
||||
@@ -183,20 +173,20 @@ impl Artifact {
|
||||
#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
|
||||
pub enum Step {
|
||||
/// Compile a template file (relative to the engineering root) into the
|
||||
/// artifact; the framework injects the manifest. Mirrors Lean
|
||||
/// `Step.typstCompile`.
|
||||
/// artifact; the framework injects the manifest. ADR-0011
|
||||
/// `typstCompile`.
|
||||
TypstCompile {
|
||||
/// The template file to compile as main, e.g. `exports/student.typ`.
|
||||
template: PathBuf,
|
||||
},
|
||||
/// Run a shell command — the escape hatch. Mirrors Lean `Step.shell`.
|
||||
/// Run a shell command — the escape hatch. ADR-0011 `shell`.
|
||||
Shell {
|
||||
/// The command line to run.
|
||||
run: String,
|
||||
},
|
||||
/// Assemble a single-file markdown deliverable by concatenating each
|
||||
/// element's `field` markdown content file in `[[parts]]` order. Mirrors
|
||||
/// Lean `Step.assembleMarkdown` (ADR-0015). Not a typst build — the
|
||||
/// element's `field` markdown content file in `[[parts]]` order. ADR-0011
|
||||
/// `assembleMarkdown` (ADR-0015). Not a typst build — the
|
||||
/// framework owns the read/concatenate/write itself.
|
||||
AssembleMarkdown {
|
||||
/// The per-element markdown content field to assemble (e.g. `slides`,
|
||||
@@ -226,12 +216,11 @@ pub struct Project {
|
||||
|
||||
/// `[info]` table (passed through to render targets verbatim).
|
||||
///
|
||||
/// **Mirrors `Spec.Courseware.Info`** in the Lean semantic master
|
||||
/// (`spec/Spec/Courseware/Model/Info.lean`): the *canonical* model whose
|
||||
/// The *canonical* model whose
|
||||
/// `authors` is always a list. The authoring-surface form (string-or-array
|
||||
/// `author`) is the separate [`RawInfo`] / [`RawAuthor`], normalized into this
|
||||
/// at the load boundary — mirroring the Lean `RawInfo` / `RawAuthor` split. No
|
||||
/// CI gate enforces this alignment (repo constitution); it is kept greppable.
|
||||
/// at the load boundary. No
|
||||
/// CI gate enforces ADR↔implementation alignment (repo constitution); it is kept greppable.
|
||||
#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
|
||||
pub struct Info {
|
||||
/// Lesson title.
|
||||
@@ -240,7 +229,6 @@ pub struct Info {
|
||||
/// so this is a list, not a single name. Empty when `[info]` declares no
|
||||
/// `author`. The on-disk `author` accepts either a bare string (one author)
|
||||
/// or an array of strings (see [`RawAuthor`]); both load into this `Vec`.
|
||||
/// Mirrors Lean `Info.authors : List String`.
|
||||
pub authors: Vec<String>,
|
||||
}
|
||||
|
||||
@@ -290,8 +278,7 @@ struct RawProject {
|
||||
name: String,
|
||||
}
|
||||
|
||||
/// The authoring-surface `[info]` (mirrors Lean `RawInfo` in
|
||||
/// `spec/Spec/Courseware/Model/Info.lean`): the raw form that exists for
|
||||
/// The authoring-surface `[info]`: the raw form that exists for
|
||||
/// fill-in convenience, normalized into the canonical [`Info`] at the load
|
||||
/// boundary. Not the form the rest of the model traffics in.
|
||||
#[derive(Debug, Deserialize)]
|
||||
@@ -301,7 +288,7 @@ struct RawInfo {
|
||||
}
|
||||
|
||||
/// On-disk `author`: either a single name (`author = "…"`) or a list
|
||||
/// (`author = ["…", "…"]`). Mirrors Lean `RawAuthor`: a fill-in convenience whose
|
||||
/// (`author = ["…", "…"]`). A fill-in convenience whose
|
||||
/// string-or-array union lives **only** at the load boundary — [`RawAuthor::into_vec`]
|
||||
/// folds it into the canonical [`Info::authors`] `Vec`, after which it never appears.
|
||||
#[derive(Debug, Deserialize)]
|
||||
@@ -312,7 +299,7 @@ enum RawAuthor {
|
||||
}
|
||||
|
||||
impl RawAuthor {
|
||||
/// Flatten to the ordered author list (Lean `RawAuthor.normalize`): a single
|
||||
/// Flatten to the ordered author list: a single
|
||||
/// name becomes a one-element list; a list passes through verbatim.
|
||||
fn into_vec(self) -> Vec<String> {
|
||||
match self {
|
||||
|
||||
Reference in New Issue
Block a user