docs-compiler 0.1.0

Docs compiler composing the estate's docs crates: include-symbol, witness, lean-check, and island fences resolved to static HTML via docs-core (docs-core extension program, SPEC.md M3/M4)
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57

# docs-compiler

The composition CLI for the estate's docs crates (docs-core extension
program, `docs-core/SPEC.md` M3/M4): scan a markdown document for the
four directive kinds, resolve each through the crate that owns it,
substitute raw HTML, and render the page with docs-core. Any failing
directive fails the build with a typed error naming its source; nothing
degrades to a silent placeholder.

## Directive fences

| Fence | Resolved by | Emitted |
|---|---|---|
| `include-symbol file=... symbol=...` | docs-symbols | `<figure class="docs-symbol" data-anchor="...">` with the byte-exact span |
| `witness wasm=... [fuel=...] [assert_exit=...] [assert_stdout=...]` | docs-witness | `<div class="docs-witness" data-exit data-fuel>` with captured stdout |
| `lean-check file=... theorem=... toolchain=...` | out-of-process `lean` + docs-proof | proof badge + `<script type="application/json" data-proof-certificate>` |
| `island ...` | docs-core (native) | `<docs-island>` (astro-island-compatible) |

## Guarantees (M3/M4, honest)

- **Build-time resolution**: all four kinds resolve during compilation;
  the emitted page is static HTML. Lean is spawned as an external
  process (REQ-P1: never linked).
- **Real kernel verdicts or no badge** (REQ-P2): nonzero exit, kernel
  errors, or Lean's `declaration uses \`sorry\`` diagnostic (which exits
  0 - it is caught) fail the build with the theorem named. The oracle
  suite runs real lean against the fixture package (positive, kernel
  rejection, sorry).
- **Certificates bind bytes** (REQ-P3): the badge embeds the SHA-256 of
  the exact Lean source; docs-proof's verifier re-checks on every build.
- **Fences are CommonMark-fenced**: an opening fence whose info string
  contains backticks is not a directive (it would swallow the rest of
  the file); unknown fences pass through as plain code.

## CLI

```
docs-compiler <input.md> [-o out.html] [--root dir]
```

Directive-relative paths resolve against `--root` (default: the input's
directory).

## Layer

L3 - composition: docs-core (L2) + docs-symbols/docs-witness/docs-proof
(L0/L1) + clap. `lean` is spawned, not linked.

## Tests

`cargo test` under clippy `-D warnings` (denies lifted in test targets
only): fence scanning and attribute parsing, the end-to-end four-kind
page (M3/M4 close criterion), typed failures per directive, and the
`lean_oracle` suite, which requires `lean` on PATH (CI installs elan
with the pinned `leanprover/lean4:v4.35.0`).

Licensed under MIT OR Apache-2.0.