Companion repository for the TUI from Zero Coursera course — a planned addition to the Rust for Data Engineering specialization (slot TBD; see docs/tui-from-zero-design.md in the course-studio repo for the in-progress curriculum spec).

The course teaches presentar — the pure-Rust TUI framework from paiml/aprender. Every crate in this workspace depends on real, published aprender-present-* crates from crates.io (v0.33 at time of writing) and uses aprender-present-test (probar) as a dev-dependency for snapshot testing.

• No reinvention. The cell buffer, diff renderer, widget trait, color type, and 20+ TUI widgets all come from presentar — the same crate the production ptop ships against. Your m1-cellbuffer::CellBuffer IS presentar_terminal::CellBuffer.
• Contracts as the source of truth. Three YAML files in contracts/ declare every invariant; pv validates them; runtime asserts in each demo binary check the obligation at exit; Lean 4 theorems discharge the universal claim.
• Probar snapshot tests, one per crate. tests/probar_snapshot.rs in each crate uses the snapshot pattern pioneered by jugar-probar / aprender-present-test to assert presentar's CellBuffer output against an inline golden — TUI testing without a browser, without Selenium.

Current pv score (5-dimension rubric):

tui-lifecycle-v1 — 0.81 (B)  Spec 0.75 · Falsify 1.00 · Kani 0.50 · Lean 1.00 · Bind 1.00
tui-rendering-v1 — 0.65 (C)  Spec 0.75 · Falsify 1.00 · Kani 0.66 · Lean 1.00 · Bind 0.00
tui-panels-v1    — 0.60 (D)  Spec 0.75 · Falsify 1.00 · Kani 0.44 · Lean 1.00 · Bind 0.00

Lifting Kani (model-checking) and Bind (presentar binding registry) is the next iteration. See contracts/binding.yaml for the contract → crate map.

Nine workspace crates, one demo binary each. Each binary prints contract: <name> — OK on stderr at exit; the CI workflow greps for that marker as the runtime half of the proof.

make demo runs all nine in single-frame mode and asserts every contract marker. cargo run --release --bin ptop-mini (no --ci) enters the live crossterm loop on a real terminal — press q, Esc, or Ctrl-C to exit.

No git deps, no path deps to a sibling checkout — everything fetches from crates.io.

make install

This runs cargo install aprender-contracts-cli for the pv binary if it isn't already on PATH. Everything else (presentar, probar, crossterm) downloads through cargo build.

• Rust 1.75+ (rustup default stable)
• Optional: elan + Lean 4 v4.13 for make lean-build
• Optional: cargo-llvm-cov for make coverage-test

git clone https://github.com/paiml/tui-from-zero
cd tui-from-zero
make install

# Gate the contracts (schema + rubric)
make validate       # pv validate per contract — 0 errors expected
make score          # pv score per contract — prints the 5-dim rubric

# Build + run every demo
make build
make demo

# Type-check the Lean 4 proofs (~1 s)
make lean-build

# Probar snapshot tests (per-crate tests/probar_snapshot.rs)
cargo test --workspace --test probar_snapshot

# Full pre-merge gate
make ci             # fmt + clippy + workspace tests + coverage + pv lint

make ci runs locally; the CI workflow runs the same gates plus runtime contract assertions on every push.

contracts/
  tui-rendering-v1.yaml      Render-pillar invariants
  tui-lifecycle-v1.yaml      React-pillar invariants
  tui-panels-v1.yaml         Compose-pillar invariants
  binding.yaml               Contract → Rust crate binding manifest
  binding-index.json         Same in JSON for tooling
m1-cellbuffer/               re-export of presentar_terminal types + helpers
m1-widgets/                  Widget trait + Container/Row/Column + Block/Label
m2-elm-counter/              init/update/view (Elm architecture)
m2-input/                    KeyEvent → Msg dispatch (totality)
m3-sparkline/                Unicode block-glyph sparkline
m3-panels/                   CpuGrid + ProcessTable + memory bar
m4-yaml-scene/               .prs scene compiler → Widget tree
m4-tests/                    snapshot() + diff_snapshot() (probar-style)
m5-ptop-mini/                capstone — composes everything into a live ptop dashboard
lean/                        Lean 4 lakefile + theorems per pillar
.github/workflows/ci.yml     pv-gated CI
Makefile                     pv + cargo + lake one-button targets
assets/hero.{svg,png}        the image at the top of this README

Dual-licensed under MIT or Apache-2.0 — pick the one that fits your downstream use. SPDX: MIT OR Apache-2.0.