Files

T

feat(spec): build out System layer and element schema model

Picture the whole framework, then pin the element-kind language layer.

System platform layer — rebuild the semantics likec4 can't draw (ADR-0001..0004):
- Prelude: opaque Identifiers carrier (ProjectId/RunId/SessionId/Principal)
- System/Run: RunState + Terminal subset (set completeness left OPEN, no invented pending)
- System/Lock: lock owner=run (typed), LockTable exclusivity, WellFormed invariant
  (a lock holder must be a non-terminal run — couples Lock and Run)
- System/Permission: read<edit<manage role lattice, capability derivation,
  can_mono monotonicity theorem; force-release sits outside the lattice (admin-only)
- System/Audit: intentionally thin (mostly plumbing, OPEN)

Courseware product layer — split the single Lesson file into focused modules and
fix doc tautology: Primitives / Element / Lesson / Render / Diagnostic, plus
QuestionBank and Course skeletons (core relations OPEN, not invented).
Diagnostic upgrades WarnsIgnored into a severity-tagged checker rule.

Element schema + rich-content model (ADR-0006, ADR-0007):
- docs/adr/0006: kind schema is declarative JSON Schema; field types are built-in
  scalars plus a `content` extension; a `content` value is typst source taken as
  module body; rich content must carry a VirtualPath (else click-to-jump and
  relative import break — verified against typst source); import boundary =
  within the engineering file + @package
- docs/adr/0007: on-disk form is a real directory tree (agent/grep friendly);
  VirtualPath = real relative path; layout conventions deferred
- spec/Courseware/RichContent: prose anchor for rich content (opaque VPath,
  RichContentRef); ElementData kept abstract — JSON/typst internals are
  implementation detail, not contract

lake build green (18 jobs), no sorry, toolchain v4.31.0.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

2026-06-22 00:31:14 +08:00

6.2 KiB

Raw Blame History

ADR 0006: Element Schema Is Declarative, Rich Content Is Typst

Status

Accepted — for the decisions below. Several sub-decisions are deliberately left open; see Open Questions / Deferred.

Builds on ADR-0005, which fixed that an element instance = a kind tag + data conforming to that kind's schema, and that a kind's minimal contract to the framework is its data schema only. This ADR fixes how that schema is expressed and what the schema's "rich content" leaves actually are.

Context

ADR-0005 left the schema representation and the kind-definition mechanism as the largest OPEN items — and they are the foundation the rule-based checker stands on (the checker validates "does this data conform to its kind's schema?"). The domain is formula-heavy and content-structured: a worked example has a problem statement, options, a solution; a theorem has a statement, a proof, prerequisite lemmas. These fields are not bare strings — they are rich content.

Two facts about Typst were verified against its source (/Users/sjfhsjfh/Typst/typst) and drive the decisions below:

A .typ file evaluates to a Module that carries both a scope of #let exports and a body Content (the rendered top-level markup). Content retains a Span that resolves back to a FileId + byte range, so click-to-jump from rendered content to source is possible.
Content has no Deserialize; and Typst's Source::new requires a FileId. Source evaluated with a detached span loses its file identity: span.id() becomes None (click-to-jump breaks) and a relative import "../x" fails with "cannot access file system from here". Relative imports and click-to-jump only work when the source is a real file (with a VirtualPath) in the compiler's World.

Decision

The data schema is declarative — a JSON Schema

A kind declares its data shape as a declarative JSON Schema (field names, types, constraints), not as a program and not as a bespoke schema DSL. The checker reads the schema and validates instance data structurally against it. Whether stdlib kinds author their schema by hand-written JSON or via a host- language builder is an implementation detail, not part of this contract.

Field types: built-in scalars plus a `content` leaf type

Schema field types are the built-in scalars (string / number / boolean / enum / list / object, as in ordinary JSON Schema) plus one extension type: content. JSON Schema has no native notion of "typst content", so this is a deliberate extension of JSON Schema (a custom type / format). Any implementation must honor the same content extension rather than inventing its own — this is the seam between the schema layer (A) and the rich-content layer.

A `content` value is a Typst source; its meaning is the module's body content

The value of a content field is a Typst source. Its denotation is the body content of that source evaluated as a module (Typst's Module.content) — not its #let exports. The canonical stored form is the source text, not a serialized Content: Content cannot be deserialized and its spans are only meaningful with the source present, so content is re-evaluated from source when needed, never round-tripped as data.

Rich content is never free-floating — it has a virtual path

Because detached Typst source loses click-to-jump and cannot do relative imports, a content value is not an anonymous text blob. It is a first-class file in the compiler's World, carrying a virtual path. This is what makes its spans resolve (click-to-jump) and its relative imports anchor. Concretely, the engineering file constitutes a virtual file system with internal path structure; each rich-content field sits at a path within it.

(This ADR commits only to "there is a path structure". Its concrete on-disk form — that the engineering file is a real directory tree — is fixed separately in ADR-0007. ADR-0006 does not assume the path structure is a disk directory.)

Import boundary: within the engineering file, plus packages

A relative import inside a rich-content source may resolve only to other paths within the same engineering file's path structure (reusing definitions local to this lesson), plus Typst @package ecosystem imports. It may not reach into other engineering files. Cross-lesson reuse, if any, goes through a separate mechanism (question bank / reuse — still OPEN, see ADR-0005 Deferred), not through raw cross-file imports.

Consequences

The checker can introspect a rendered Content (its element type, fields, downcasts) to validate rich content beyond "is it present", and can use spans to point diagnostics back at the offending source location.
Canonical state is source text; Content is a transient product of evaluation. Storage, diffing, and agent edits all operate on source, not on serialized content.
Extending JSON Schema with content means conformance has a shared extension point: implementations align on one content semantics instead of each inventing a rich-text encoding.
Rich content requiring a virtual path means the engineering file is inherently a path-structured container, not a bag of anonymous snippets — which is what ADR-0007 then grounds on disk.
The import boundary keeps an engineering file self-contained: it depends only on itself and on published packages, never on a sibling lesson's internals.

Open Questions / Deferred

Content element constraints (Y) — whether a content field may be further constrained to admit only certain Typst element kinds (e.g. "inline only, no figure", "exactly one final expression"). Deferred: we will know which constraints are needed only once real stdlib kinds exist. Until then a content field means "a block of content", inner element shape unconstrained.
stdlib kind set — the first batch of framework-provided kinds and their individual schemas (each is later, per-kind work).
JSON Schema dialect — which draft, and exactly which keywords are permitted in a kind schema (a subset/profile is likely, to keep the checker tractable). Not pinned here.
On-disk form — fixed in ADR-0007 (directory tree); layout conventions (manifest, element ordering) deferred beyond that.

6.2 KiB Raw Blame History