Add eggcc container benchmark

.github/workflows/build.yml

@@ -41,7 +41,6 @@ jobs:
       - run: rustup component add clippy
       - uses: Swatinem/rust-cache@v2
       - run: cargo test --workspace
-      - run: cargo test --workspace proof
       - run: cargo clippy --workspace --all-targets -- -D warnings
 
   benchmark-smoke:
@@ -59,22 +58,29 @@ jobs:
       - run: uv run --locked ./bench.py --rounds 1 --treatments off --timeout-sec 120 --report .reports.ci.jsonl egglog/tests/integer_math.egg
 
   codspeed:
+    name: codspeed (${{ matrix.mode }})
     permissions:
       contents: read
       id-token: write
     runs-on: ubuntu-latest
     timeout-minutes: 20
+    strategy:
+      fail-fast: false
+      matrix:
+        mode:
+          - simulation
+          - memory
     steps:
       - run: echo "CARGO_INCREMENTAL=0" >> "$GITHUB_ENV"
       - uses: actions/checkout@v4
         with:
           persist-credentials: false
       - uses: taiki-e/install-action@v2
         with:
-          tool: cargo-codspeed@4.0.1
+          tool: cargo-codspeed@5.0.1
       - uses: Swatinem/rust-cache@v2
-      - run: cargo codspeed build -p egglog-experimental --bench files
+      - run: cargo codspeed build --measurement-mode ${{ matrix.mode }} -p egglog-experimental --bench files
       - uses: CodSpeedHQ/action@v4
         with:
-          run: cargo codspeed run files
-          mode: simulation
+          run: cargo codspeed run --measurement-mode ${{ matrix.mode }} files
+          mode: ${{ matrix.mode }}

AGENTS.md

@@ -17,11 +17,10 @@ session's `xhigh` reasoning effort instead.
 
 ## Tests
 
-Use this order for normal changes:
+Use this order for normal full validation:
 
 ```bash
 cargo test --workspace
-cargo test --workspace proof
 cargo clippy --workspace --all-targets -- -D warnings
 uv lock --check
 uv run --locked ruff format --check bench.py test_bench.py
@@ -30,31 +29,41 @@ uv run --locked mypy bench.py test_bench.py
 uv run --locked pytest -q
 ```
 
-For benchmark-runner changes, also smoke the CLI with a temporary report:
+For proof-focused changes, the filtered proof test is useful while iterating or
+when you want a focused proof rerun:
 
 ```bash
-uv run --locked ./bench.py --rounds 1 --treatments off --report .reports.smoke.jsonl \
-  egglog/tests/integer_math.egg
+cargo test --workspace --test files proof_unit
+cargo test --workspace --test files proof_integration
 ```
 
-For agent-readable benchmark smoke output, pipe report rows from stdout and keep
-runner status and build diagnostics on stderr:
+`proof_unit` runs small explicit `(prove ...)` fixtures under `tests/proofs`
+and snapshots their proof-mode output.
+`proof_integration` runs curated larger proof-testing cases that stay in their
+normal test locations, treating checks as proves and snapshotting generated
+proofs. Both are name-filtered subsets of `cargo test --workspace`, so do not
+run them after a full workspace test unless you want a focused proof rerun.
+
+For benchmark-runner changes, smoke the public CLI entrypoint with a temporary,
+machine-readable report. Use stdout report mode so the run does not read or
+append to the default benchmark cache; runner status and build diagnostics stay
+on stderr.
 
 ```bash
-uv run --locked ./bench.py --rounds 1 --treatments off --report - \
+./bench.py --rounds 1 --treatments off --report - \
   egglog/tests/integer_math.egg > /tmp/egglog-encoding-bench-smoke.jsonl
 ```
 
 ## Benchmarking
 
 - Use `./bench.py` as the public benchmark entrypoint.
-- Do not pass egglog's `--save-report` during timed benchmark collection; it
-  changes the measured work.
 - Keep `.reports.jsonl` append-only and ignored by git.
 - Use `--report -` when report rows should be streamed to stdout instead of
   appended to a cache file.
 - Runner status output always goes to stderr, including Rich progress and
   summary tables.
+- Benchmark inputs should not contain executable `(prove ...)` commands; use
+  `(check ...)` in benchmark fixtures and cover proof extraction in proof tests.
 - Benchmark files are resolved relative to the command invocation directory,
   not relative to comparison targets.
 - Cache reuse is decided by binary SHA-256, file SHA-256, treatment, and

README.md

@@ -19,7 +19,8 @@ The development loop is:
 cargo test --workspace
 
 # Run proof-focused tests while iterating.
-cargo test --workspace proof
+cargo test --workspace --test files proof_unit
+cargo test --workspace --test files proof_integration
 
 # Run lint checks across the workspace.
 cargo clippy --workspace --all-targets
@@ -35,6 +36,18 @@ The root workspace includes both `egglog` and `egglog-experimental`.
 `egglog-experimental` depends on the workspace `egglog` crate, which keeps proof
 changes and downstream experimental behavior in the same reviewable unit.
 
+Proof-specific file tests use two filter prefixes:
+
+- `proof_unit`: small explicit `(prove ...)` fixtures under `tests/proofs`,
+  with proof-mode output saved as snapshots.
+- `proof_integration`: curated larger proof-testing cases that stay in their
+  normal test locations, such as math-style workloads and the eggcc fixture.
+  Checks are treated as prove commands and the generated proofs are saved as
+  snapshots.
+
+Both filters are subsets of the full workspace test run. Use them for fast proof
+iteration and reserve `cargo test --workspace` for the final compatibility gate.
+
 ## Benchmarking
 
 The public benchmark entrypoint is an executable Python script:
@@ -120,10 +133,12 @@ If no files are provided, the default target benchmark suite is:
 - `egglog/tests/web-demo/rw-analysis.egg`
 - `egglog/tests/integer_math.egg`
 - `egglog/tests/web-demo/resolution.egg`
+- `egglog-experimental/tests/fixtures/eggcc-2mm-pass1-merge-old.egg`
 
-These four files are proof-compatible representative examples under the current
+These five files are proof-compatible representative examples under the current
 `egglog-experimental` CLI and run under the default `off`, `term`, and `proofs`
-treatment matrix.
+treatment matrix. The eggcc fixture is the heavy container/proof benchmark in
+the default suite.
 Relative file paths are resolved relative to the directory where `./bench.py`
 was invoked, not relative to each target checkout. The same file contents are
 used for every target, and `file.sha256` records the exact benchmark input.
@@ -513,17 +528,18 @@ Each benchmark report row records the binary hash used for that observation.
 
 ## CI
 
-CI runs on pull requests, manual dispatch, and pushes to `main`. It runs four
-jobs:
+CI runs on pull requests, manual dispatch, and pushes to `main`. It runs these
+job groups:
 
 - `python`: `uv lock --check`, ruff formatting, ruff linting, mypy, and pytest.
 - `rust`: workspace tests, proof-focused tests, and clippy.
 - `benchmark-smoke`: a one-round `./bench.py` run on
   `egglog/tests/integer_math.egg`.
 - `codspeed`: an in-process, proofs-only `egglog-experimental` benchmark
-  harness over a smaller representative file set. CodSpeed tracks proof-mode
-  movement without invoking `./bench.py`; the CLI benchmark report remains the
-  source for the full off/term/proofs comparison.
+  harness over a smaller representative file set, run through CodSpeed in both
+  simulation and memory modes. CodSpeed tracks proof-mode movement without
+  invoking `./bench.py`; the CLI benchmark report remains the source for the
+  full off/term/proofs comparison.
 
 Python checks are run as separate commands:
 

bench.py

@@ -50,6 +50,7 @@
     "egglog/tests/web-demo/rw-analysis.egg",
     "egglog/tests/integer_math.egg",
     "egglog/tests/web-demo/resolution.egg",
+    "egglog-experimental/tests/fixtures/eggcc-2mm-pass1-merge-old.egg",
 )
 TARGET_SPEED_CAPTION = (
     "Ratio is target / baseline. Values below 1x are faster; above 1x are slower. Intervals are 95% CIs."
@@ -434,6 +435,25 @@ def resolve_files(raw_files: Sequence[str], invocation_cwd: Path) -> tuple[FileS
     return tuple(files)
 
 
+def file_contains_executable_prove_command(path: Path) -> bool:
+    for line in path.read_text(encoding="utf-8").splitlines():
+        stripped = line.lstrip()
+        if stripped.startswith(";"):
+            continue
+        if re.match(r"\(prove(?:\s|\))", stripped):
+            return True
+    return False
+
+
+def validate_spec(spec: BenchmarkSpec) -> None:
+    for file_spec in spec.files:
+        if file_contains_executable_prove_command(file_spec.absolute_path):
+            raise ValueError(
+                f"{file_spec.display_path} contains an explicit prove command; "
+                "benchmark files should use check so proof extraction is not included in timed runs"
+            )
+
+
 def resolve_report_destination(raw_report: str, invocation_cwd: Path) -> ReportDestination:
     if raw_report == "-":
         return ReportDestination(path=None, stream=sys.stdout)
@@ -1779,6 +1799,7 @@ def main(argv: Sequence[str] | None = None) -> int:
             rounds=args.rounds,
             timeout_sec=args.timeout_sec,
         )
+        validate_spec(spec)
         target_specs = args.target if args.target is not None else ["."]
         target_requests = tuple(parse_target(raw) for raw in target_specs)
         rows = load_report(report_destination)

egglog-experimental/Cargo.toml

@@ -32,4 +32,5 @@ log = "0.4"
 [dev-dependencies]
 divan = { workspace = true }
 glob = "0.3.1"
+insta = "1.40"
 libtest-mimic = "0.8.1"