Tooling / docs / examples role lab

This role lab is generated from the shared four-stage contract. Page identity, route, prerequisites, first-edit seams, and gates are manifest-owned; prose, checks, the fixture, and additional seams are content-owned.

Prerequisites

1. Retrieve and predict

Start from the existing logger-counting chain. The canonical program owns source behavior; its checked expected.txt owns accepted stdout; the serialized example fact owns evidence metadata; the page manifest owns route identity and status; and the generated Markdown is only a public projection. Read each authority before editing and predict which files a source-only comment will change after regeneration.

Retrieve:

Locate the source and accepted stdout in examples/logger-counting/main.bang and examples/logger-counting/expected.txt.
Locate the existing example vocabulary in docfacts/schema/example.schema.json and its serialized record in docfacts/examples/logger-counting.json.
Locate the generator tools/docfacts_logger.py and the manifest page that publishes docs/reference/examples/logger-counting.md.

Predict before running:

Predict the stdout under env, oracle, and compiled before running the edited example.
Predict that one shared source-only comment changes the example pair, fact, and page but not runner-produced stdout.
Predict why editing the Markdown or typing an evidence label would be overwritten or rejected.

2. Trace the seam

Trace one canonical example through the established owners. check-examples.sh --update is the only snapshot-acceptance interface and runs the lane-built binary. check --json and query dump expose source facts without becoming another authority. tools/docfacts_logger.py reads the canonical source and accepted output, validates the existing example schema, serializes the fact, reloads that boundary, and renders the public Markdown. The page manifest resolves the validated evidence pointer and owns the public route; the Markdown owns neither.

Checks:

Name the owners of source, accepted output, evidence status, route identity, and rendered page.
Explain why the update interface may write expected stdout while a hand-written expected value may not.
Explain how the generator check and manifest schema poles make copied evidence styling fail loud.

Tracked seams:

3. Practise in isolation

Use the fixture below as a bounded, semantic-preserving edit to the canonical logger-counting example inside the disposable exact-HEAD clone. Derive its related silent variant from the same fixture so the existing handler-clause-only evidence remains truthful. Remove the counting example's accepted output and recreate it only with just update-example logger-counting, which uses the binary built in that clone. Run every declared engine plus check --json and query dump. First require the stale fact check to reject the source change; then regenerate through the existing logger generator, inspect the source/fact/page diff, and prove a second regeneration is byte-identical. Do not edit production Lean, type expected stdout, copy an evidence label, or hand-edit the projection.

Start from the clean, ready checkout used for the common journey. The project helper creates an independent full clone at its exact commit; all writes and gates below happen there.

set -euo pipefail
root="$(git rev-parse --show-toplevel)"
test -z "$(git -C "$root" status --porcelain)"
base="$(git -C "$root" rev-parse HEAD)"
parent="$(mktemp -d)"
lane="$parent/repo"
branch="practice/tooling-docs-examples-$(date +%s)-$$"
"$root/tools/new-worktree.sh" "$lane" "$branch" "$base"
cd "$lane"
practice="$lane/main.bang"
bundle="$parent/evidence"
mkdir "$bundle"
cat > "$practice" <<'BANG'
-- Role-lab practice: canonical source flows through checked projections.
effect Log { log : Int -> Int }
 
handle
  (logger.log(10)) + (logger.log(20)) + (logger.log(30))
with Log as logger {
  log(msg) => 1
}
BANG

Run every step in order:

nix develop --command lake build bang
example="$lane/examples/logger-counting"
silent="$lane/examples/logger-silent"
fact="$lane/docfacts/examples/logger-counting.json"
page="$lane/docs/reference/examples/logger-counting.md"
cp "$example/main.bang" "$bundle/original-main.bang" && cp "$example/expected.txt" "$bundle/original-expected.txt" && cp "$silent/main.bang" "$bundle/original-silent-main.bang"
cp "$practice" "$example/main.bang" && sed 's/log(msg) => 1/log(msg) => 0/' "$practice" > "$silent/main.bang" && rm "$practice" "$example/expected.txt"
nix develop --command just update-example logger-counting 2>&1 | tee "$bundle/update.txt"
./.lake/build/bin/bang run --engine=env "$example/main.bang" > "$bundle/env.txt" && diff -u "$example/expected.txt" "$bundle/env.txt"
./.lake/build/bin/bang run --engine=oracle "$example/main.bang" > "$bundle/oracle.txt" && diff -u "$example/expected.txt" "$bundle/oracle.txt"
./.lake/build/bin/bang run --engine=compiled "$example/main.bang" > "$bundle/compiled.txt" && diff -u "$example/expected.txt" "$bundle/compiled.txt"
./.lake/build/bin/bang check --json "$example/main.bang" > "$bundle/check.json"
./.lake/build/bin/bang query dump "$example/main.bang" > "$bundle/query.json"
if nix develop --command python3 tools/docfacts_logger.py --check > "$bundle/stale-projection.txt" 2>&1; then printf '%s\n' 'STOP: stale example projection was accepted.' >&2; false; fi
nix develop --command python3 tools/docfacts_logger.py
git diff --check -- examples/logger-counting/main.bang examples/logger-counting/expected.txt examples/logger-silent/main.bang docfacts/examples/logger-counting.json docs/reference/examples/logger-counting.md
git diff -- examples/logger-counting/main.bang examples/logger-counting/expected.txt examples/logger-silent/main.bang docfacts/examples/logger-counting.json docs/reference/examples/logger-counting.md > "$bundle/practice.diff" && test -s "$bundle/practice.diff"
cp "$fact" "$bundle/logger-counting.json" && cp "$page" "$bundle/logger-counting.md"
sha256sum "$fact" "$page" > "$bundle/projection.sha256"
nix develop --command python3 tools/docfacts_logger.py
sha256sum --check "$bundle/projection.sha256"
nix develop --command just test-docfacts-logger > "$bundle/docfacts-check.txt" 2>&1
nix develop --command just docs-check > "$bundle/docs-check.txt" 2>&1
nix develop --command just test-role-lab-tooling-docs-examples > "$bundle/harness.txt" 2>&1
git restore -- examples/logger-counting/main.bang examples/logger-counting/expected.txt examples/logger-silent/main.bang docfacts/examples/logger-counting.json docs/reference/examples/logger-counting.md
test -z "$(git status --porcelain)"

Bounded outcome: The lane-built runner recreates the accepted output; env, oracle, and compiled agree; the mechanically related silent variant preserves the declared differential; check/query facts succeed; stale metadata is rejected; one existing generator deterministically updates the validated fact and public page; cleanup leaves the exact-HEAD clone clean.

4. Inspect evidence and select live work

Keep the original source/output, three engine observations, structured CLI facts, stale-check rejection, generated JSON/Markdown, deterministic hashes, and focused gate output as one external evidence bundle. Read the diff by authority: source is intent, expected output is runner acceptance, the fact is validated metadata, the manifest is route identity, and Markdown is derived presentation. Only then select current tooling, documentation, or example work through a read-only issue query.

Evidence checks:

Require the accepted output to be absent before and recreated by the named update interface, never by a literal write.
Require env, oracle, and compiled to run from the exact-HEAD lane binary and match the one accepted output.
Require check --json and query dump to return successful structured facts for the edited source.
Require the stale projection to fail before regeneration and the existing schema/manifest poles to pass afterward.
Require source, fact, and page diffs plus byte-identical first and second generated outputs.
Confirm no production Lean source changed and cleanup returned the exact-HEAD clone to a clean state.
Record the real narrow and full gate exit statuses; a skipped gate is not a pass.

Narrow gate:

nix develop --command bash -lc 'just check-examples && just check-examples-env && just docs-check'

Full gate:

nix develop --command just verify

Read-only issue selection:

Run gh issue list --repo phibkro/bang --state open --search "tooling OR docs OR examples"; set issue=<candidate-number> and inspect it with gh issue view "$issue" --repo phibkro/bang. Recommend one only after naming the source, expected-output, fact, manifest, and projection owners plus the smallest falsifying gate; do not claim, comment on, or mutate it.