Add eggcc container benchmark and proof coverage by saulshanabrook · Pull Request #10 · saulshanabrook/egglog-encoding

saulshanabrook · 2026-07-08T19:12:08Z

Summary

Stacked on #9.

This PR contains the local work on top of the subtree sync:

add the eggcc container fixture to the default CLI benchmark suite
add proof-focused snapshots and proof integration coverage
wire CodSpeed simulation and memory modes
update benchmark/docs guidance
address review comments around proof checking, fixture assertions, merge validators, nightly benchmark resilience, and pinned nightly dependencies

Review Notes

This branch has one commit on top of codex/eggcc-container-subtree-sync, so the diff should show only the local changes rather than the imported subtree updates.

The egglog/core-relations/src/hash_index fix from egraphs-good/egglog#914 lives in #9, not this PR.

The final tree is identical to the previously reviewed codex/eggcc-container-benchmark tip 5adee2de.

Validation

cargo test --workspace --test files proof_integration

coderabbitai · 2026-07-08T19:12:16Z

Important

Review skipped

Auto reviews are disabled on base/target branches other than the default branch.

Please check the settings in the CodeRabbit UI or the .coderabbit.yaml file in this repository. To trigger a single review, invoke the @coderabbitai review command.

⚙️ Run configuration

Configuration used: defaults

Review profile: CHILL

Plan: Pro

Run ID: 9b3ab1b6-08ae-4092-a060-d3bd0a4217aa

You can disable this status message by setting the reviews.review_status to false in the CodeRabbit configuration file.

Use the checkbox below for a quick retry:

🔍 Trigger review

✨ Finishing Touches

🧪 Generate unit tests (beta)

Create PR with unit tests
Commit unit tests in branch codex/eggcc-container-benchmark-updates

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

_{Comment @coderabbitai help to get the list of available commands.}

codspeed-hq · 2026-07-08T19:20:25Z

Merging this PR will not alter performance

✅ 3 untouched benchmarks
🆕 3 new benchmarks

Performance Changes

	Mode	Benchmark	`BASE`	`HEAD`	Efficiency
🆕	Memory	`files[integer_math_proofs]`	N/A	10.4 MB	N/A
🆕	Memory	`files[resolution_proofs]`	N/A	4.2 MB	N/A
🆕	Memory	`files[rw_analysis_proofs]`	N/A	10.6 MB	N/A

_{Comparing codex/eggcc-container-benchmark-updates (fa99cfc) with codex/eggcc-container-subtree-sync (cf26722)¹}

No successful run was found on codex/eggcc-container-subtree-sync (fa99cfc) during the generation of this report, so 2ced0f8 was used instead as the comparison base. There might be some changes unrelated to this pull request in this report. ↩

oflatt

Had roughly two concerns, one with proof checker (hiding a bug?) and another with files.rs getting more complex (and also hiding another bug perhaps?)

oflatt · 2026-07-08T20:16:25Z

        subst: &mut HashMap<String, TermId>,
        rule_name: &str,
    ) -> Result<(), ProofCheckError> {
-        let ResolvedFact::Eq(_, lhs, rhs) = fact else {


Why this change? The old comment says is_container_side_condition only flags eq. This seems bad if you ran into otherwise. Actually I wonder if we should have thrown a panic here before

Removed the changes, they weren't necessary it seems like

oflatt · 2026-07-08T20:19:18Z

+        self.term_encoding || self.proofs || self.proof_testing
+    }
+
+    fn is_curated_proof_integration(&self) -> bool {


what is the point of is_curated_proof_integration?

Removed this. Now all proof compatible files will be run with proof testing and we create snapshots of their proofs

oflatt · 2026-07-08T20:20:00Z

-        if !should_fail && supports_proofs {
+        if !should_fail
+            && !proof_manually_disabled
+            && (supports_proofs || run.is_curated_proof_integration())


Why would something be supports_proofs but not is_curated_proof_integration? I think I could imagine this case due to a known bug in the proof support detection and globals

Fixed it to be this

oflatt · 2026-07-08T20:21:55Z

@@ -1,26 +1,57 @@
-use std::path::PathBuf;


Yikes, lots of code duplication with the other files.rs... worth fixing in our fork? I'd love to fix in upstream as well

Yeah I think we could at some point, I think the stuff with testing de-sugarring is also a bit different, was disabled on experimental at some point? Def worth looking into

yeah we did have to disable desugar round trip on experimental at some opint

Stacked on the subtree-sync branch. This preserves the final reviewed tree from codex/eggcc-container-benchmark while separating local benchmark, proof, CI, and review-fix changes from the subtree merge commits. The hash index ordering fix from egraphs-good/egglog#914 lives in the subtree-sync branch.

oflatt

just some details on files.rs

oflatt · 2026-07-08T23:10:36Z

@@ -1,26 +1,57 @@
-use std::path::PathBuf;


yeah we did have to disable desugar round trip on experimental at some opint

oflatt

yay files.rs looks like a cleanup now. had one nit, but approving now

6f0d26e3 Merge pull request #927 from oflatt/oflatt-container-proofs 85ba2626 small feedback fixes 4141a970 Merge pull request #935 from egraphs-good/nightly 5009aaee simplify map.rs e45cd547 address feedback from Saul 3960015c Merge pull request #885 from saulshanabrook/codex/split-scheduler-stale-match-cleanup bd1697a3 Tighten the Containers section of proof_encoding.md (saulshanabrook#10) 5fca83b7 Add container support to the term/proof encoding 7f111370 nightly: prefer the rustup cargo shim over the system cargo (#942) 15888b87 nightly: install deps into a venv to satisfy PEP 668 (#939) f295052e scheduler: skip subsumed fresh matches d1418d20 Merge remote-tracking branch 'upstream/main' into codex/split-scheduler-stale-match-cleanup f99482a2 Merge pull request #936 from oflatt-claude/nightly-eval-live fe240e6b Render nightly benchmark report with eval-live 5bb42afc nightly 6c6f01d5 scheduler: simplify changelog entry c1420100 scheduler: reduce held validation churn ce4ef0b5 scheduler: validate only held matches f0d4822b scheduler: keep stale validation focused 1dedb505 scheduler: condense changelog entry 939339b1 scheduler: simplify stale match validation ed6aa6e9 scheduler: preserve existing match handling 8602f56e scheduler: split action-key dedup cleanup 89779541 scheduler: validate only held matches e24d1468 scheduler: clarify stale match validation eaf4ab4f Merge remote-tracking branch 'upstream/main' into codex/split-scheduler-stale-match-cleanup 0804bee1 scheduler: deduplicate residual match keys 2c55caff Merge remote-tracking branch 'upstream/main' into codex/split-scheduler-stale-match-cleanup 09b8c002 scheduler: document stale match validation 2c749b89 scheduler: clean stale matches git-subtree-dir: egglog git-subtree-split: 6f0d26e37241055a1230bdcdb33f0c5d3f01e935

saulshanabrook force-pushed the codex/eggcc-container-benchmark-updates branch from 87185c7 to d1a80c5 Compare July 8, 2026 19:44

saulshanabrook mentioned this pull request Jul 8, 2026

Sync egglog subtrees for eggcc container benchmark #9

Merged

saulshanabrook force-pushed the codex/eggcc-container-benchmark-updates branch 2 times, most recently from e33dd55 to 919030c Compare July 8, 2026 19:52

oflatt requested changes Jul 8, 2026

View reviewed changes

saulshanabrook force-pushed the codex/eggcc-container-benchmark-updates branch from 919030c to bc02144 Compare July 8, 2026 21:03

saulshanabrook mentioned this pull request Jul 8, 2026

Add eggcc container benchmark #8

Closed

saulshanabrook force-pushed the codex/eggcc-container-benchmark-updates branch 2 times, most recently from f9289da to 7d8e104 Compare July 8, 2026 21:21

saulshanabrook force-pushed the codex/eggcc-container-benchmark-updates branch from 7d8e104 to 64ddf2f Compare July 8, 2026 21:39

oflatt requested changes Jul 8, 2026

View reviewed changes

Simplify file proof tests to proof-testing mode

6a42294

oflatt approved these changes Jul 9, 2026

View reviewed changes

Comment thread egglog/tests/files.rs Outdated

Keep proof-testing snapshot policy in helper

fa99cfc

saulshanabrook merged commit e71edaf into codex/eggcc-container-subtree-sync Jul 9, 2026
6 checks passed

saulshanabrook deleted the codex/eggcc-container-benchmark-updates branch July 9, 2026 17:38

Conversation

saulshanabrook commented Jul 8, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Review Notes

Validation

Uh oh!

coderabbitai Bot commented Jul 8, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Review skipped

Uh oh!

codspeed-hq Bot commented Jul 8, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Merging this PR will not alter performance

Performance Changes

Footnotes

Uh oh!

oflatt left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

oflatt left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

oflatt left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

saulshanabrook commented Jul 8, 2026 •

edited

Loading

coderabbitai Bot commented Jul 8, 2026 •

edited

Loading

codspeed-hq Bot commented Jul 8, 2026 •

edited

Loading