Prepare v1.0.0 with reproducible offline demos and verified PDF dossiers

.github/workflows/ci.yml

@@ -79,6 +79,17 @@ jobs:
           sudo apt-get update
           sudo apt-get install --yes --no-install-recommends texlive-latex-base
 
+      - name: Set up the documented demo
+        run: make demo-setup
+
+      - name: Run the narrated checks and a new-input PDF demo
+        env:
+          UV_OFFLINE: "1"
+          UV_PYTHON_DOWNLOADS: never
+        run: |
+          make demo-check
+          make demo INPUT=tests/instances/demo_sat.cm13 TIMEOUT=300
+
       - name: Compile opt-in run dossier without shell escape
         run: make run-dossier-smoke
 

Makefile

@@ -6,6 +6,11 @@ VALGRIND ?= valgrind
 PAGES_BUILD_DIR ?= build/pages
 UV_CACHE_DIR ?= $(CURDIR)/.uv-cache
 export UV_CACHE_DIR
+# Set the default before unexport, which otherwise defines an empty variable.
+TIMEOUT ?= 300
+# Command-line values are otherwise expanded for Make's implicit environment,
+# even by parse-time $(shell ...) calls. Export only the raw demo copies below.
+unexport INPUT TIMEOUT
 
 CPPFLAGS ?= -Iinclude
 CFLAGS ?= -std=c17 -Wall -Wextra -Wpedantic -O2
@@ -84,7 +89,7 @@ SERIAL_LIBRARY := $(LIB_DIR)/libwang.a
 SHARED_LIBRARY := $(LIB_DIR)/libwang.so
 OPENMP_LIBRARY := $(LIB_DIR)/libwang_openmp.a
 
-.PHONY: all setup serial shared openmp check c-check python-check pages-check \
+.PHONY: all setup demo-setup demo demo-check serial shared openmp check c-check python-check pages-check \
 	generated-pages-check \
 	strict-check sanitizer-check analyzer-check valgrind-check \
 	cachegrind-check benchmark benchmark-smoke benchmark-compare \
@@ -97,6 +102,26 @@ all: serial shared
 setup:
 	$(UV) sync --frozen
 
+# Keep these steps in one recipe: missing prerequisites must stop setup even -j.
+demo-setup: export DEMO_SETUP_CC = $(CC)
+demo-setup: export DEMO_SETUP_UV = $(UV)
+demo-setup:
+	@$(PYTHON) tools/demo_setup.py preflight
+	$(UV) sync --locked
+	$(UV) sync --locked --directory renderer
+	$(MAKE) shared
+	@$(PYTHON) tools/demo_setup.py verify
+
+# Pass raw values through the environment: filenames are not shell/Make code.
+demo: export TILING_DEMO_INPUT = $(value INPUT)
+demo: export TILING_DEMO_TIMEOUT = $(value TIMEOUT)
+demo:
+	@$(PYTHON) tools/demo.py
+
+demo-check: export TILING_DEMO_TIMEOUT = $(value TIMEOUT)
+demo-check:
+	@$(PYTHON) tools/demo_check.py
+
 serial: $(SERIAL_LIBRARY)
 
 shared: $(SHARED_LIBRARY)

README.md

@@ -3,17 +3,19 @@
 [![CI](https://github.com/xtraid/tiling-foundry/actions/workflows/ci.yml/badge.svg)](https://github.com/xtraid/tiling-foundry/actions/workflows/ci.yml)
 [![License](https://img.shields.io/badge/license-MIT-blue.svg)](LICENSE)
 
-Can a fixed set of just 23 Wang tiles encode an NP-complete problem? Tiling
-Foundry turns the Yang--Zhang construction into an inspectable, tested software
-pipeline: a formula becomes a finite simply connected region, independent
-engines decide it, and separate checkers validate every published SAT witness.
+Can a fixed set of just 23 Wang tiles encode an NP-complete problem?
 
-This is a research implementation, not a general-purpose tiling library. Its
+Tiling Foundry turns the Yang–Zhang construction into an experimental framework
+for finding, cross-verifying, and explaining solutions, with an eye toward
+performance.
+
+This is not a general-purpose tiling library. Its
 main concern is keeping the mathematical reduction, search, verification, and
 presentation boundaries visible enough to audit and measure. The previous
 experimental codebase remains frozen under `legacy/`.
 
 **Read:** [Documentation](https://xtraid.github.io/tiling-foundry/) ·
+[Presentazione](https://xtraid.github.io/tiling-foundry/presentazione/) ·
 [Pipeline](https://xtraid.github.io/tiling-foundry/pipeline/) ·
 [Worked example](https://xtraid.github.io/tiling-foundry/worked-example/) ·
 [Reference](https://xtraid.github.io/tiling-foundry/reference/) ·
@@ -22,15 +24,16 @@ experimental codebase remains frozen under `legacy/`.
 
 ## Why this repository exists
 
-The 2024 Yang--Zhang result proves NP-completeness for tiling finite simply
+The 2024 Yang--Zhang result establishes NP-completeness for tiling finite simply
 connected regions with one fixed set of 23 Wang tiles. Turning that compact
 proof into software exposes practical questions: which representation owns a
 claim, how the reduction is checked apart from search, how independent engines
 are compared, and what evidence is needed before parallelism.
 
-Tiling Foundry answers those questions with explicit ownership, an executable
-reference solver, differential tests, independent oracles and verifiers, and
-reproducible captures.
+The repository implements the construction, two serial search paths, and
+separate Boolean and Wang checks. Reproducible runs connect each result to its
+input, witnesses, and diagnostics. These tests check the software; the theorem
+and its proof belong to the [Yang–Zhang paper](#primary-reference).
 
 ## Quick start
 
@@ -39,18 +42,102 @@ userspace. The toolchain uses Linux/POSIX facilities including `mmap`, `/proc`,
 Valgrind, and dynamic loading of `libwang.so`; Windows and macOS are not
 currently supported.
 
-Install a C17 compiler, `make`, OpenMP support, and
-[`uv`](https://docs.astral.sh/uv/), then run:
+For the full dossier, install a C17 compiler, `make`, Python 3.11 or newer,
+Git, [`uv`](https://docs.astral.sh/uv/getting-started/installation/), and
+pdfLaTeX. On Debian 13, the system packages are:
+
+```sh
+sudo apt-get update
+sudo apt-get install --no-install-recommends \
+  build-essential python3 git ca-certificates curl texlive-latex-base
+```
+
+On Arch Linux / Omarchy, install the equivalent prerequisites:
+
+```sh
+sudo pacman -Syu --needed base-devel python git ca-certificates curl texlive-latex
+```
+
+Arch's [`texlive-latex`](https://archlinux.org/packages/extra/any/texlive-latex/)
+pulls in `texlive-basic` and `texlive-bin` and supplies the LaTeX packages used
+by the report. If setup reports `pdflatex is missing`, install this package,
+check `pdflatex --version`, then rerun `make demo-setup` while online.
+
+If `uv` is not installed, download and inspect the standalone installer before
+running it. The version used for the setup check is 0.12.1:
 
 ```sh
-git clone https://github.com/xtraid/tiling-foundry.git
+curl -LsSf https://astral.sh/uv/0.12.1/install.sh -o /tmp/uv-install.sh
+cat /tmp/uv-install.sh
+sh /tmp/uv-install.sh
+export PATH="$HOME/.local/bin:$PATH"
+uv --version
+```
+
+Clone the fixed release and prepare the project:
+
+```sh
+git clone --branch v1.0.0 --depth 1 https://github.com/xtraid/tiling-foundry.git
 cd tiling-foundry
-make check
+make demo-setup
 ```
 
-`make check` builds the serial executable and shared library, runs the C and
-core Python tests, builds the OpenMP scaffold, and exercises both serial solver
-paths. It does not require a GPU.
+`demo-setup` checks the compiler and compiles a small PDF with the real report
+template before installing dependencies. It then builds `libwang.so` and
+checks Z3, image rendering, and fonts. A missing prerequisite stops setup with
+an error; the target does not install system packages.
+
+The two Python environments stay separate: `.venv` uses Python 3.11 or newer;
+`renderer/.venv` uses Python 3.14, selected by `renderer/.python-version`.
+Both are installed with `uv sync --locked`. The first setup needs network
+access to download packages and, when absent, the renderer's Python. Keep the
+environments and uv-managed interpreter installed for offline use. No global
+`pip` installation or GPU is needed.
+
+Generate the first complete dossier from the included SAT case:
+
+```sh
+UV_OFFLINE=1 uv run --locked python tools/generate_run_dossier.py \
+  examples/run-cases-v2/pipeline-sat.json \
+  build/first-dossier --pdf
+```
+
+Open `build/first-dossier/report.pdf`. The output directory must be new for each
+run. `UV_OFFLINE=1` also reaches the renderer subprocesses. The command runs
+the four engines and checks the recorded results before producing the figures
+and PDF.
+
+Run the short, narrated verification suite after setup:
+
+```sh
+make demo-check
+```
+
+It checks parsing, known SAT and UNSAT cases, agreement between the four engines,
+and rejection of an altered witness. It stops at the first failure and prints
+the measured duration after success. See the
+[suite guide](docs/run_dossiers.md#suite-breve-commentata)
+for the six checks, diagnostics, and timeout options.
+
+### Run a new input
+
+After `make demo-setup`, give the demo a CM1-in-3 file without an expected result:
+
+```sh
+make demo INPUT='path/to/new formula.cm13' TIMEOUT=300
+```
+
+The command copies the input, runs each of the four engines once, checks their
+results, and produces the figures and PDF using the installed environments
+offline. It prints the PDF path only after the complete dossier succeeds.
+Each invocation retains its input, original name/hash and log in a new directory
+under `build/demo/`.
+
+`TIMEOUT` is a global limit in seconds, including capture, figures and PDF.
+Timeout, cancellation, UNKNOWN, disagreement or an incomplete trace fail with
+diagnostics; they do not mean UNSAT. Arbitrary inputs have no completion-time
+guarantee. The [dossier guide](docs/run_dossiers.md#new-cm1-in-3-input)
+describes the input format, output and diagnostic options.
 
 ## Current status
 
@@ -121,19 +208,32 @@ follows one named SAT source through the same contracts and checks.
 - Parallel search is deferred until the cleaned serial baseline has new
   evidence and explicit ownership tests.
 
-## Next milestones
+## Exam Ready release and next milestones
+
+**v1.0.0 Exam Ready** provides three commands: `make demo-setup` prepares the
+environment, `make demo INPUT=...` produces a checked dossier and PDF, and
+`make demo-check` runs the short narrated suite. The full workflow has been
+rehearsed on Debian and on an Omarchy laptop, including offline runs and PDF
+inspection. See the [release notes](RELEASE_NOTES.md) for prerequisites,
+measured rehearsal times, and limits.
 
-Work proceeds in this order:
+**Release checkpoint:** publish the tag and GitHub Release, then verify the
+documented commands from a fresh clone of that tag and open the resulting
+dossier on the presentation computer. A local freeze or merged PR alone does
+not complete this milestone.
 
-1. freeze the current visual documentation and PDF work;
-2. T99: split fast, integration, and evidence verification into reusable CI
+The [Exam Ready plan](docs/plans/2026-09-15-exam-ready-v1.0.md) records the six
+sessions and acceptance criteria. After the release and project defense, work
+resumes in this order:
+
+1. split fast, integration, and evidence verification into reusable CI
    levels;
-3. T100: perform a behavior-preserving structural cleanup of the serial
+2. perform a behavior-preserving structural cleanup of the serial
    solver;
-4. collect a new serial baseline, hard-UNSAT evidence, and the public option
+3. collect a new serial baseline, hard-UNSAT evidence, and the public option
    matrix;
-5. introduce a minimal `TaskPlan` with an equivalent serial executor;
-6. add and measure real OpenMP execution only after those gates pass.
+4. introduce a minimal `TaskPlan` with an equivalent serial executor;
+5. add and measure real OpenMP execution only after those gates pass.
 
 ## Build, test, and reproduce
 
@@ -144,6 +244,12 @@ make clean
 make check
 ```
 
+`make check` builds the serial libraries, runs the C and core Python tests,
+builds the OpenMP scaffold, and exercises both serial solver paths. The core
+checks require a C17 compiler with OpenMP support, `make`, Python and `uv`;
+they do not require LaTeX. The full dossier setup above also prepares the
+renderer and PDF tools.
+
 The renderer is an isolated locked Python project and has its own suite:
 
 ```sh

RELEASE_NOTES.md

@@ -0,0 +1,73 @@
+# v1.0.0 — Exam Ready
+
+This release packages the serial Yang–Zhang pipeline for a reproducible
+demonstration: prepare the environments, check known cases, and turn a new
+CM1-in-3 input into a verified dossier with figures and a PDF.
+
+## Run the release
+
+Install the Linux system prerequisites in the [README](README.md#quick-start),
+including pdfLaTeX. Debian and Arch/Omarchy commands are provided there.
+The first setup needs network access; later demo commands use the installed
+environments offline.
+
+```sh
+git clone --branch v1.0.0 --depth 1 https://github.com/xtraid/tiling-foundry.git
+cd tiling-foundry
+make demo-setup
+make demo-check
+make demo INPUT=tests/instances/demo_sat.cm13
+make demo INPUT=tests/instances/pipeline_unsat_search.cm13
+```
+
+To demonstrate offline operation, disconnect the network after setup and run
+the last three commands. Open the PDF path printed after each successful demo.
+Keep the installed environments, managed Python interpreter, and generated
+materials available for the presentation. Save presentation copies outside
+`build/`, which is removed by `make clean`.
+
+For a new input, use `make demo INPUT='path/to/formula.cm13' TIMEOUT=300`.
+The header must be `p cm13 n n`, followed by `n` three-literal clauses;
+each declared variable occurs exactly three times, including repeated
+occurrences within a clause. The [dossier guide](docs/run_dossiers.md)
+describes the full format and output.
+
+## What is included
+
+- `make demo-setup` checks C17, the real PDF template, Z3, rendering and fonts,
+  and prepares both locked Python environments.
+- `make demo-check` narrates six checks covering parsing, SAT/UNSAT, agreement
+  between four engines, and rejection of a corrupted witness.
+- `make demo INPUT=...` accepts an input without an expected result. Reference,
+  optimized, Boolean Z3 and Wang Z3 each run once; figures and PDF reuse the
+  recorded capture. Input bytes, original name/hash and diagnostics survive.
+- SAT witnesses are independently checked. UNSAT records engine agreement
+  and marks witness-only sections not applicable. Trace is not an independent
+  UNSAT certificate.
+- Timeout, UNKNOWN, disagreement, incomplete traces and cancellation are
+  failures. They never become UNSAT or a completed dossier. Every invocation
+  uses a new directory, preserving earlier successful runs.
+- The documentation, figures and PDF support the demonstration, including
+  compact-region trace legends and routing labels that fit their boxes.
+
+## Rehearsal evidence and limits
+
+The workflow was exercised on Debian and an Omarchy laptop. On Omarchy, the
+initial rehearsal at `7ea377e` measured setup at 28.644 s, the six-check suite
+at 12.781 s, SAT/PDF at 132.138 s and UNSAT/PDF at 69.300 s. After the layout
+correction, UNSAT/PDF at `0215b73` took 66.289 s and the user confirmed that
+all text was readable. These are observations on that laptop, not timing
+guarantees or CI performance thresholds. Published-tag acceptance is recorded
+with the GitHub Release and its accompanying evidence.
+
+Linux is the supported platform. The core Python environment requires 3.11
+or newer; the renderer uses Python 3.14. NumPy, Pillow and Z3 are locked;
+the GPU is not required. Arbitrary inputs can exceed the global timeout or
+trace capacity, and wide regions can require zoom to inspect individual cells.
+Wang Z3 dominated the observed laptop runtime.
+
+Updated v2 readers accept earlier v2 dossiers. A strict older reader may
+reject a new-input dossier whose `expected_status` is null; use the readers
+shipped with this release. Dossier v1 and the independent solver/checker
+boundaries remain supported. No OpenMP solver or new serial optimization is
+introduced here; CI restructuring and serial cleanup follow the exam.