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
Replace generated-driver compilation with the template model.
cph-typst:
- driver.rs DELETED (generate_driver, static-include driver, numbering-threading).
- New manifest.rs: build_augmented_manifest(&Lesson) emits a TOML doc with [info]
+ ordered [[parts]] each carrying a `fields` array = the kind's content fields
whose <root>/<path>/<field>.typ exists on disk. Reuses cph-schema's
content_field_names (new dep; no cycle). This closes the OPEN point WU-C'
surfaced: typst has no file-exists primitive, so the engine (which has disk
access) tells the template which optional content (lemma proof) is present.
- World main = the real engineering-file template (<root>/<template>); the
augmented manifest is served as an in-memory virtual file at /.cph/manifest.toml
(never written to the tree), injected via sys.inputs.manifest. render_dir kept
only for @local/cph-render + vendored @preview/numbly resolution.
- Artifact handling: SingleFile+TypstCompile compiles; FileTree, shell-only, and
undeclared-target are blocking "deferred/not-declared" diagnostics (ADR-0011).
- Engine public signatures unchanged; LessonWorld::new takes template+manifest_src.
cph-check: no source change needed (only uses lesson.targets/target.name +
unchanged Engine methods); pipeline + Legal alignment intact.
Fixtures: mini gets exports/{student,teacher}.typ (from render/templates/) + v2
manifest + a second proof-less lemma to exercise optional content. render-stub
retired (tests use the real render/). Through-template PDFs offline: student 44KB,
teacher 56KB; proof-less lemma compiles clean (optional-content confirmed).
Workspace: fmt + clippy -D warnings + all tests green.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
[targets.*] reworked: artifact is now an inline table with a type discriminator
({type="single-file",filepath} / {type="file-tree",root,outputs}) and steps is an
ordered array-of-tables ({type="typst-compile",template} / {type="shell",run}).
numbering removed entirely (presentation lives in the template per ADR-0011).
TargetConfig { name, artifact: Artifact, steps: Vec<Step> }; Artifact and Step
mirror Spec.Courseware.Artifact / Spec.Courseware.Step (doc-cited). Sensible
defaults so a bare [targets.student] still works: single-file build/<name>.pdf +
one typst-compile exports/<name>.typ. Malformed artifact/step type → non-fatal
SchemaViolation with fallback. 8 tests green.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Integrate the WU-B (structured targets) and WU-C (numbly, config) changes.
cph-typst:
- World resolves any @preview/* package from the in-repo vendored dir
(<render_dir>/vendor/typst-packages/preview/<name>/<version>/), fully offline —
no typst-kit download. Proven: build_pdf_with_real_render compiles the real
render package (which imports @preview/numbly:0.1.0) through the embedded
engine, PDF out.
- Driver threads each target's presentation config: looks up the TargetConfig by
name, emits `config: (numbering: (heading: (...)))` (escaped) when an override
is present, else `config: (:)` (render default).
- target_precheck guards artifact/target: FileTree → blocking diagnostic (MVP is
single-file, deferred per ADR-0009); --target not declared → blocking
diagnostic; no-targets lesson still defaults through.
cph-check:
- Migrated to Lesson.targets: Vec<TargetConfig> (target_names() / target.name at
the 6 sites). Pipeline unchanged (already matches ADR-0010 phases). Documented
that !has_errors() implements Spec.Courseware.Legal (no error-level diagnostic).
Workspace: fmt + clippy -D warnings + all tests green.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
manifest.toml [targets.*] upgraded from bare names to structured build configs.
Lesson.targets: Vec<String> → Vec<TargetConfig> { name, artifact, numbering }.
ArtifactKind { SingleFile, FileTree } mirrors Spec.Courseware.Artifact.
NumberingConfig.heading: Option<Vec<String>> — None means "use framework
default" (render package owns it), so absence is distinguishable from a value.
Empty [targets.x] body = all defaults, no diagnostics. Malformed config (bad
artifact value, non-array numbering.heading) → non-fatal SchemaViolation, target
kept with defaults. Enabled toml `preserve_order` so target declaration order is
real (the old Vec<String> never actually preserved order). target_names() helper
for call sites that only want names. 8 tests green.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The heart of the pipeline. Embeds the typst 0.15 compiler as a library to
compile-check a lesson and export a PDF, with diagnostics mapped back to source
spans (the product's value).
- LessonWorld: a typst World over the engineering-file directory tree. vpath =
real relative path (ADR-0007); the per-target driver is mounted in-memory as
`main` (.cph/driver-<target>.typ, never written to disk); @local/cph-render is
resolved from render_dir (CPH_RENDER_DIR / with_render_dir), no package install
or network. Fonts via typst-kit FontStore (system CJK).
- Driver generation: from the manifest, per target — static root-relative
`include` of each content file (⇒ module body content, ADR-0006), assembled
into the frozen `display(info, target, parts)` call; optional lemma proof
emitted only if proof.typ exists; example `source` scalar threaded through.
- Diagnostics: typst SourceDiagnostic (errors + warnings) → cph_diag::Diagnostic.
0.15 DiagSpan handled via span.id() + WorldExt::range → file-relative
SourceSpan with 1-based line/col; driver-internal spans re-pointed with a
"generated driver" hint, never dropped. typst hints/trace carried through.
- Engine API: new / with_render_dir / compile_check / build_pdf.
- 6 tests incl. build_pdf_with_real_render — full World→driver→cph-render→PDF
producing real PDF-1.7 output (student 42KB / teacher 54KB). clippy/fmt clean.
Also fixes render/typst.toml `compiler = ">=0.15.0"` → `"0.15.0"`: typst 0.15's
manifest parser rejects a `>=` comparator on the compiler field (the 0.14 CLU
WU-2 tested against was lenient). This unblocks loading the real render package.
Pinned: typst/typst-pdf/typst-syntax/typst-library/typst-layout/typst-kit =0.15.0.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Declarative JSON Schema per kind (segment/example/lemma/sop), embedded as real
.json artifacts (ADR-0006) and validated by a small hand-rolled interpreter
(properties/required/type/enum/additionalProperties + the `x-cph-content`
marker) — no jsonschema-crate churn for a one-optional-string scalar surface.
`x-cph-content: true` marks content fields (not in element.toml; require sibling
<field>.typ); everything else is an element.toml scalar. `validate(desc)` is
self-contained: UnknownKind for unknown kinds, MissingContentFile (path named in
message) for absent required .typ, SchemaViolation for bad scalars; lemma proof
optional ⇒ no diagnostic when absent. 8 tests green.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Stand up the Rust implementation of the rule-based checker (the thing that
"stands in Lean's position" at product runtime). Single repo-wide cargo
workspace at the repo root so future components (e.g. an exporter) can reuse
shared crates.
- workspace: 6 member crates under crates/; cph-schema/cph-typst/cph-check/
cph-cli are stubs for later WUs that compile clean today.
- cph-diag: shared diagnostic vocabulary. Severity { Warning, Error } mirrors
Spec.Courseware.Diagnostic.Severity exactly (two-valued, no info/note — a
contract decision documented in-code since there's no CI gate for alignment).
Closed DiagCode set with stable string forms; Diagnostic with optional span +
fix hint; Display renders `error[CODE]: msg / --> file:line:col / hint: …`.
- cph-model: the ADR-0008 loader. Reads manifest.toml ([project]/[info]/ordered
[[parts]]/[targets.*]) + each part's element.toml into an ordered Lesson
(mirrors Lean `Lesson = List (Element P)`). Structure-only: cross-checks
part.kind == element.toml kind, rejects `..` traversal; does NOT do schema
validation (WU-3), content-file existence (WU-3), or typst (WU-4).
`load(root) -> (Option<Lesson>, Vec<Diagnostic>)`: Some even on collectible
part errors, None only on hard manifest failure.
- 13 tests (7 cph-diag, 6 cph-model incl. static fixtures doubling as format
docs). build + test + clippy -D warnings + fmt --check all green.
Judgment call flagged for review: cph-diag has no ManifestMalformed code, so
manifest-structure errors map to SchemaViolation (TODO noted in-code).
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
hongjr03
sjfhsjfh
