Tau Sparse-Impact Demo

Patch a Tau checkout, build it, and run a generated sparse impacted-factor spec that reports the measured indexed-factor speedup.

Feature-gated patch Local timing Fallback boundary

What this demo checks

24 factors, 3 impacted

The generated Tau formula is a top-level conjunction. Only three factors mention d0, so the patched diagnostic route can compare all-factor solving with impacted-factor solving.

Scope

This is a local research demo. A large speedup here does not imply that every Tau formula speeds up. The confirmed benchmark claim remains the checked sparse-impact result described in Tutorial 52.

One command

From the repository root, point the script at a Tau checkout:

python3 scripts/run_tau_sparse_impact_demo.py --tau-checkout /path/to/tau-lang-latest

The script applies the patch if needed, rebuilds Tau, writes the generated demo spec, runs the patched Tau binary, and writes a JSON report.

Files

Patch

Tau source patch

patches/tau/indexed-factor-sparse-impact-demo.patch

Runner

Demo script

scripts/run_tau_sparse_impact_demo.py

Spec

Generated Tau command

examples/tau/sparse_impact_factor_speedup_demo.tau

Expected output shape

Exact timings depend on the machine and checkout, but a successful run prints a JSON summary like this:

{
  "status": "passed",
  "median_speedup": 41.1025,
  "scope": "sparse top-level conjunction with 24 factors and 3 factors impacted by d0"
}

The important fields in the full report are:

factors = 24
impacted_indexed = 3
saved_factors = 21
scan_equals_indexed = 1
full_errors = 0
indexed_errors = 0

Interpretation

The demo is a smoke test for the sparse-impact route. It checks that the support index selects the same impacted factors as a scan, and that the patched diagnostic path solves far fewer factors on this generated case.

It is not a production optimizer. It does not solve the automatic route-selector problem. For the full evidence and falsifications, read the research log.