Add eggcc container benchmark

[saulshanabrook]

Pulls in egglog main, egraphs-good/egglog-experimental#56, and egraphs-good/egglog#914 (to fix some panics), so that we can have a working eggcc benchmark.

It also cleans up the testing, so that we can run proof focused testing easily:

cargo test --workspace --test files proof_unit
cargo test --workspace --test files proof_integration

The unit tests are in the proofs/ subdirectory and the integration tests are a list of hard coded files that are run in proof testing mode, like eggcc. That way their proofs are saved as snapshots.

I tried to add hardboiled, but failed because it uses unstable function. Also luminal failed to run in proof mode.

Summary by CodeRabbit

• New Features
  • Added expanded proof and container support, including container rebuild/canonicalization for vectors, sets, maps, multisets, pairs, plus maybe/either helpers.
  • Introduced map-of canonical map representation and deterministic term ordering.
  • Added a nightly benchmarking workflow with an auto-generated HTML dashboard.
• Bug Fixes
  • Improved proof checking and normalization for container side conditions.
  • Fixed scheduler behavior so subsumed matches aren’t treated as fresh.
• Documentation / Tests
  • Updated daily proof/benchmark instructions to use proof-filtered runs and check-based benchmark files.

[coderabbitai]

No actionable comments were generated in the recent review. 🎉

ℹ️ Recent review info

⚙️ Run configuration

Configuration used: defaults

Review profile: CHILL

Plan: Pro

Run ID: 2ea35fea-b076-46ad-ae36-74f535677211

📥 Commits

Reviewing files that changed from the base of the PR and between 86f9417 and 5adee2d.

📒 Files selected for processing (9)

• .github/workflows/build.yml
• README.md
• egglog-experimental/src/container_primitives.rs
• egglog-experimental/src/maybe.rs
• egglog-experimental/tests/eggcc_2mm_proof.rs
• egglog/scripts/nightly_bench.py
• egglog/scripts/requirements.txt
• egglog/src/proofs/proof_checker.rs
• egglog/tests/files.rs

🚧 Files skipped from review as they are similar to previous changes (8)

• egglog/scripts/requirements.txt
• egglog-experimental/tests/eggcc_2mm_proof.rs
• README.md
• egglog-experimental/src/container_primitives.rs
• egglog/scripts/nightly_bench.py
• egglog/tests/files.rs
• egglog/src/proofs/proof_checker.rs
• egglog-experimental/src/maybe.rs

---

📝 Walkthrough

Walkthrough

This PR adds container-sort support to egglog’s term/proof encoding, including rebuild primitives, proof normalization, and side-condition checking. It also adds Either/Maybe container sorts and merge primitives in egglog-experimental, updates benchmark validation, and adds a nightly benchmark harness.

Changes

Container proof/term encoding in egglog core

Layer / File(s)	Summary
ValueRebuilder trait split egglog/core-relations/src/{containers/mod.rs,containers/tests.rs,table_spec.rs,uf/mod.rs,lib.rs}, egglog/egglog-bridge/src/tests.rs, egglog/src/sort/{mod.rs,fn.rs,pair.rs,vec.rs,set.rs,map.rs,multiset.rs}	Introduces ValueRebuilder separate from Rebuilder, plus the updated container rebuild signatures that use it.
AST/parser for container-rebuild annotations egglog/src/ast/{mod.rs,parse.rs,desugar.rs}, egglog/src/prelude.rs	Adds ContainerRebuildSpec/ProofConstructorNames, updates Sort fields, parsing, display, and desugaring.
Container canonicalization & OrdTerm egglog/src/sort/{map.rs,set.rs,multiset.rs,pair.rs,vec.rs}, egglog/src/termdag.rs	Adds canonical proof-term validators for each container sort and deterministic ast_cmp/OrdTerm ordering.
Rebuild primitive registration & encoding rules egglog/src/proofs/{proof_container_rebuild.rs,proof_encoding.rs,proof_encoding_helpers.rs}	Registers per-sort rebuild/proof primitives and extends rebuild-rule generation to cover container columns and congruence proofs.
Proof checking/format/normal-form/simplification egglog/src/proofs/{proof_checker.rs,proof_format.rs,proof_normal_form.rs,proof_simplification.rs,proof_extraction.rs}	Adds ContainerNormalize/Eval handling, container side-condition checking, and redundancy elimination.
Typechecking/EGraph wiring egglog/src/typechecking.rs, egglog/src/lib.rs	Wires new sort fields through typechecking, restores proof state, and exposes proof builder APIs publicly.
Scheduler fix & hash-index rewrite egglog/src/scheduler.rs, egglog/core-relations/src/hash_index/{mod.rs,tests.rs}	Fixes subsumed rows being offered as fresh matches; rewrites ColumnIndex::rebuild_full with block radix sort and merge.
Container tests and docs egglog/tests/{container_rebuild.rs,files.rs}, egglog/src/proofs/proof_tests.rs, egglog/{CHANGELOG.md,src/proofs/proof_encoding.md}	Adds end-to-end container rebuild tests, proof-mode test scenarios, and documentation updates.

egglog-experimental container primitives

Layer / File(s)	Summary
Either/Maybe sorts egglog-experimental/src/{either.rs,maybe.rs}	Adds EitherSort/MaybeSort container sorts with primitives and reconstruction logic.
Min/max primitives and wiring egglog-experimental/src/{container_primitives.rs,lib.rs,main.rs,set_cost.rs}, egglog-experimental/Cargo.toml	Adds pair/maybe/either min-max primitives, registers new sorts, updates the cost lookup call, and switches CLI to proof-mode e-graph construction.
Proof tests egglog-experimental/tests/{eggcc_2mm_proof.rs,files.rs}	Adds proof-integration test coverage and proof-aware trial generation.

Benchmarking infra

Layer / File(s)	Summary
bench.py validation bench.py, test_bench.py	Rejects benchmark files with executable prove commands.
Nightly harness egglog/scripts/nightly_bench.py, egglog/Makefile, egglog/.gitignore, egglog/scripts/requirements.txt	Adds a hyperfine-based nightly benchmark sweep and HTML dashboard generation.
Docs/CI updates .github/workflows/build.yml, AGENTS.md, README.md	Updates proof test filter guidance and benchmark fixture requirements.

Estimated code review effort: 5 (Critical) | ~150 minutes

Sequence Diagram(s)

sequenceDiagram
  participant RebuildRule as Rebuild rule
  participant ContainerRebuild as ContainerRebuild primitive
  participant ContainerRebuildProof as ContainerRebuildProof primitive
  participant CSortProof as CSortProof table
  participant ProofStore as Proof checker

  RebuildRule->>ContainerRebuild: rebuild container elements via UF leaders
  RebuildRule->>ContainerRebuildProof: request rebuild proof for changed elements
  ContainerRebuildProof->>CSortProof: read reflexive base proof
  ContainerRebuildProof->>ContainerRebuildProof: fold Congr chain over changed children
  ContainerRebuildProof->>ContainerRebuildProof: apply ContainerNormalize
  ContainerRebuildProof->>CSortProof: anchor new reflexive proof
  ProofStore->>ProofStore: check_side_condition re-evaluates container fact

Loading

Possibly related PRs

• saulshanabrook/egglog-encoding#5: Touches the same benchmarking validation path in bench.py and related docs.
  Suggested reviewers: oflatt

🚥 Pre-merge checks | ✅ 5

✅ Passed checks (5 passed)

Check name	Status	Explanation
Description Check	✅ Passed	Check skipped - CodeRabbit’s high-level summary is enabled.
Title check	✅ Passed	The title is concise and accurately summarizes the main change: adding an eggcc container benchmark.
Docstring Coverage	✅ Passed	No functions found in the changed files to evaluate docstring coverage. Skipping docstring coverage check.
Linked Issues check	✅ Passed	Check skipped because no linked issues were found for this pull request.
Out of Scope Changes check	✅ Passed	Check skipped because no linked issues were found for this pull request.

✨ Finishing Touches

📝 Generate docstrings

• Create stacked PR
• Commit on current branch

🧪 Generate unit tests (beta)

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

---

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

• X
• Mastodon
• Reddit
• LinkedIn

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

[codspeed-hq]

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 (5adee2d) with main (d9b4001)}

[coderabbitai]

Actionable comments posted: 2

🧹 Nitpick comments (5)

egglog/scripts/nightly_bench.py (1)

303-355: 🩺 Stability & Availability | 🔵 Trivial | ⚡ Quick win

Wrap per-benchmark loop body in try/except for nightly resilience.

An unexpected exception from probe(), hyperfine(), or json.load() (e.g., OSError, json.JSONDecodeError) would abort the entire sweep without generating a report. For a nightly harness, one bad benchmark file should not prevent the report from being produced.

♻️ Suggested resilience wrapper

     for path in benchmarks:
         name = path.relative_to(TEST_DIR).as_posix()
+        try:
             req = requires_proofs(path)
 
             # Qualification probes: the single-thread standard run and the proof run.
             std_probe = None if req else probe(path, 1, False)
             proof_probe = None if proof_excluded(path) else probe(path, 1, True)
             proof_supported = proof_probe is not None and proof_probe[0]
 
             std_qualifies = std_probe is not None and std_probe[0] and std_probe[1] >= MIN_BENCH_SECONDS
             proof_qualifies = proof_supported and proof_probe[1] >= MIN_BENCH_SECONDS
 
             if not (std_qualifies or proof_qualifies):
                 reason = "errored" if (req and not proof_supported) else "too-fast"
                 skipped.append({"name": name, "reason": reason})
                 continue
 
             cells: dict[str, dict] = {}
             for key, _label, threads, proof in CONFIGS:
                 if proof:
                     if not proof_supported:
                         cells[key] = {"status": "na"}  # proofs unsupported / excluded
                     else:
                         cells[key] = measure_cell(path, threads, True, proof_probe)
                 else:
                     if req:
                         cells[key] = {"status": "na"}  # needs proofs; no plain run
                     else:
                         pr = std_probe if threads == 1 else None
                         cells[key] = measure_cell(path, threads, False, pr)
 
             # Enforce the threshold on measured data: the cold qualification probe
             # can overshoot 50ms for a program whose warmed runs are all faster.
             measured = [c["mean"] for c in cells.values() if "mean" in c]
             if not measured or max(measured) < MIN_BENCH_SECONDS:
                 skipped.append({"name": name, "reason": "too-fast"})
                 continue
 
             rows.append({"name": name, "cells": cells})
 
             def fmt(key: str) -> str:
                 c = cells[key]
                 return f"{c['mean']:>10.3f}" if "mean" in c else f"{c.get('status', '—'):>10}"
             log(f"    {name:<40} " + "  ".join(fmt(k) for k, *_ in CONFIGS))
+        except Exception as exc:
+            log(f"    {name:<40} ERROR: {exc}")
+            skipped.append({"name": name, "reason": "error"})
+            continue

🤖 Prompt for AI Agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@egglog/scripts/nightly_bench.py` around lines 303 - 355, The per-benchmark
processing loop in nightly_bench.py should be made resilient so one failing
benchmark does not abort the full report. Wrap the body of the benchmark
iteration around the calls to probe(), measure_cell(), hyperfine(), and any JSON
loading path in a try/except that catches unexpected exceptions like OSError and
json.JSONDecodeError, then record the current benchmark in skipped with an
appropriate error reason and continue. Keep the existing row/skip bookkeeping in
the loop around benchmark names, and use the existing probe, measure_cell, and
skipped/rows flow to preserve output for all remaining benchmarks.

egglog/scripts/requirements.txt (1)

1-1: 📐 Maintainability & Code Quality | 🔵 Trivial | ⚡ Quick win

Pin eval-live to a commit SHA for reproducible nightly runs. The current git dependency tracks the default branch, so upstream changes can break the harness unexpectedly.

🤖 Prompt for AI Agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@egglog/scripts/requirements.txt` at line 1, The eval-live dependency is
currently floating on the default branch, which makes nightly runs
non-reproducible; update the requirement in requirements.txt to pin eval-live to
a specific commit SHA instead of an unpinned git reference. Keep the existing
git-based dependency form, but replace the branch-tracking reference with a
commit-specific one so future upstream changes do not alter harness behavior
unexpectedly.

egglog-experimental/src/maybe.rs (1)

184-264: 📐 Maintainability & Code Quality | 🔵 Trivial | ⚡ Quick win

Duplicated tolerance-merge logic between live primitive and TermDag validator.

The float-tolerance comparison (old_f == new_f || (old_f == 0.0 && new_f == -0.0) || ... || (old_f - new_f).abs() <= tolerance) is implemented twice — once in the PurePrim-style closure body (Lines 194-198) and again in validate_maybe_f64_merge_with_tol (Lines 257-260). If one copy is ever tweaked (e.g. tolerance semantics change) without updating the other, generated proofs could validate incorrectly against runtime behavior. Consider extracting the pure numeric comparison into a shared helper function reused by both.

🤖 Prompt for AI Agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@egglog-experimental/src/maybe.rs` around lines 184 - 264, The float-tolerance
merge condition is duplicated between the `maybe-f64-merge-with-tol` primitive
closure and `validate_maybe_f64_merge_with_tol`, so update both paths to use one
shared helper for the numeric comparison. Extract the `old_f/new_f/tolerance`
merge check into a reusable function and call it from both
`add_primitive_with_validator!` and the validator, keeping
`maybe_sorts`/`maybe_f64` flow unchanged.

egglog-experimental/src/container_primitives.rs (1)

193-245: 📐 Maintainability & Code Quality | 🔵 Trivial | ⚡ Quick win

Duplicated min/max comparison logic between bound_merge (runtime) and validate_maybe_either_i64_bool_merge (validator).

Both functions independently encode identical keep_old boolean logic for Min/Max over i64/bool. Consider factoring the comparison predicates (keep_old for int/bool given BoundMergeKind) into small shared helpers to avoid divergence between the live evaluator and the proof-term validator.

Also applies to: 304-331

🤖 Prompt for AI Agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@egglog-experimental/src/container_primitives.rs` around lines 193 - 245, The
`bound_merge` runtime path and `validate_maybe_either_i64_bool_merge` validator
duplicate the same `Min`/`Max` keep_old logic for `i64` and `bool`, so refactor
that predicate into shared helper(s) and have both functions call them. Use the
existing `BoundMergeKind`, `bound_merge`, and
`validate_maybe_either_i64_bool_merge` symbols to centralize the comparison
behavior and keep the runtime and validator in sync.

egglog/tests/files.rs (1)

430-446: 🎯 Functional Correctness | 🔵 Trivial | ⚡ Quick win

Manual proof-disable list can be silently bypassed for curated integration files.

proof_testing trials are generated when supports_proofs || run.is_curated_proof_integration(), but supports_proofs is the only branch that checks manual_proof_disable_reason. If a file is ever added to both PROOF_INTEGRATION_FILES and MANUAL_PROOF_DISABLED_FILES (no overlap today), the disable would be silently ignored for the proof_testing trial. Worth guarding now to avoid a future footgun.

♻️ Proposed guard

-        if !should_fail && (supports_proofs || run.is_curated_proof_integration()) {
+        if !should_fail
+            && manual_proof_disable_reason(&run.path).is_none()
+            && (supports_proofs || run.is_curated_proof_integration())
+        {

🤖 Prompt for AI Agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@egglog/tests/files.rs` around lines 430 - 446, The proof trial generation in
files.rs can bypass the manual proof-disable guard for curated integration files
because the check for manual_proof_disable_reason only runs under
supports_proofs, while is_curated_proof_integration() still enables
proof_testing trials. Update the trial-building logic around push_trial in the
proof-testing branch so manual_proof_disable_reason is consulted before adding
any proof_testing or desugar proof trials, regardless of whether the run came
from supports_proofs or is_curated_proof_integration(). Use the existing Run
fields and the proof integration gating in this loop to keep disabled files from
ever producing proof trials.

🤖 Prompt for all review comments with AI agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

Inline comments:
In `@egglog-experimental/tests/eggcc_2mm_proof.rs`:
- Around line 30-66: The required-string assertions in
eggcc_2mm_full_export_uses_container_helpers currently scan the raw program
text, so comment-only mentions can satisfy them. Reuse the non_comment_program
filtering already built in this test and check the required list against that
cleaned text instead of program, especially for the primitive-name symbols like
either-left, either-right, and the helper names. Keep the existing :no-merge and
:merge old assertions as they are.

In `@egglog/src/proofs/proof_checker.rs`:
- Around line 962-965: The Eq-only pattern in the proof checker branch allows
bare ResolvedFact::Fact(...) to bypass container side-condition validation, so
update the handling around is_container_side_condition and the ResolvedFact
match in proof_checker to either make Fact impossible there or explicitly
reject/handle it before the early return. Use the relevant proof-checking path
in the branch that destructures ResolvedFact::Eq to ensure all container facts
are checked, including any ResolvedFact::Fact case.

---

Nitpick comments:
In `@egglog-experimental/src/container_primitives.rs`:
- Around line 193-245: The `bound_merge` runtime path and
`validate_maybe_either_i64_bool_merge` validator duplicate the same `Min`/`Max`
keep_old logic for `i64` and `bool`, so refactor that predicate into shared
helper(s) and have both functions call them. Use the existing `BoundMergeKind`,
`bound_merge`, and `validate_maybe_either_i64_bool_merge` symbols to centralize
the comparison behavior and keep the runtime and validator in sync.

In `@egglog-experimental/src/maybe.rs`:
- Around line 184-264: The float-tolerance merge condition is duplicated between
the `maybe-f64-merge-with-tol` primitive closure and
`validate_maybe_f64_merge_with_tol`, so update both paths to use one shared
helper for the numeric comparison. Extract the `old_f/new_f/tolerance` merge
check into a reusable function and call it from both
`add_primitive_with_validator!` and the validator, keeping
`maybe_sorts`/`maybe_f64` flow unchanged.

In `@egglog/scripts/nightly_bench.py`:
- Around line 303-355: The per-benchmark processing loop in nightly_bench.py
should be made resilient so one failing benchmark does not abort the full
report. Wrap the body of the benchmark iteration around the calls to probe(),
measure_cell(), hyperfine(), and any JSON loading path in a try/except that
catches unexpected exceptions like OSError and json.JSONDecodeError, then record
the current benchmark in skipped with an appropriate error reason and continue.
Keep the existing row/skip bookkeeping in the loop around benchmark names, and
use the existing probe, measure_cell, and skipped/rows flow to preserve output
for all remaining benchmarks.

In `@egglog/scripts/requirements.txt`:
- Line 1: The eval-live dependency is currently floating on the default branch,
which makes nightly runs non-reproducible; update the requirement in
requirements.txt to pin eval-live to a specific commit SHA instead of an
unpinned git reference. Keep the existing git-based dependency form, but replace
the branch-tracking reference with a commit-specific one so future upstream
changes do not alter harness behavior unexpectedly.

In `@egglog/tests/files.rs`:
- Around line 430-446: The proof trial generation in files.rs can bypass the
manual proof-disable guard for curated integration files because the check for
manual_proof_disable_reason only runs under supports_proofs, while
is_curated_proof_integration() still enables proof_testing trials. Update the
trial-building logic around push_trial in the proof-testing branch so
manual_proof_disable_reason is consulted before adding any proof_testing or
desugar proof trials, regardless of whether the run came from supports_proofs or
is_curated_proof_integration(). Use the existing Run fields and the proof
integration gating in this loop to keep disabled files from ever producing proof
trials.

🪄 Autofix (Beta)

Fix all unresolved CodeRabbit comments on this PR:

• Push a commit to this branch (recommended)
• Create a new PR with the fixes

---

ℹ️ Review info

⚙️ Run configuration

Configuration used: defaults

Review profile: CHILL

Plan: Pro

Run ID: ed3cb262-e3d1-4ef0-8666-cd0981e4825d

📥 Commits

Reviewing files that changed from the base of the PR and between d9b4001 and 86f9417.

⛔ Files ignored due to path filters (23)

• Cargo.lock is excluded by !**/*.lock
• egglog-experimental/tests/fixtures/eggcc-2mm-pass1-merge-old.egg is excluded by !**/*.egg
• egglog-experimental/tests/proofs/unstable-fresh-proof.egg is excluded by !**/*.egg
• egglog-experimental/tests/snapshots/files__proof_integration_eggcc_2mm_pass1_merge_old.snap is excluded by !**/*.snap
• egglog-experimental/tests/snapshots/files__proof_unit_unstable_fresh_proof.snap is excluded by !**/*.snap
• egglog/src/proofs/snapshots/egglog__proofs__proof_tests__tests__doc_example_add_function1.snap is excluded by !**/*.snap
• egglog/tests/container-proofs.egg is excluded by !**/*.egg
• egglog/tests/proofs/container-set-collapse.egg is excluded by !**/*.egg
• egglog/tests/proofs/rule-head-fast-path.egg is excluded by !**/*.egg
• egglog/tests/snapshots/files__proof_integration__eqsolve_desugar_proof_testing.snap is excluded by !**/*.snap
• egglog/tests/snapshots/files__proof_integration__eqsolve_proof_testing.snap is excluded by !**/*.snap
• egglog/tests/snapshots/files__proof_integration__integer_math_desugar_proof_testing.snap is excluded by !**/*.snap
• egglog/tests/snapshots/files__proof_integration__integer_math_proof_testing.snap is excluded by !**/*.snap
• egglog/tests/snapshots/files__proof_integration__math_proof_testing.snap is excluded by !**/*.snap
• egglog/tests/snapshots/files__proof_integration__resolution_desugar_proof_testing.snap is excluded by !**/*.snap
• egglog/tests/snapshots/files__proof_integration__resolution_proof_testing.snap is excluded by !**/*.snap
• egglog/tests/snapshots/files__proof_integration__rw_analysis_desugar_proof_testing.snap is excluded by !**/*.snap
• egglog/tests/snapshots/files__proof_integration__rw_analysis_proof_testing.snap is excluded by !**/*.snap
• egglog/tests/snapshots/files__proof_manual_disabled_files.snap is excluded by !**/*.snap
• egglog/tests/snapshots/files__proof_unsupported_files.snap is excluded by !**/*.snap
• egglog/tests/snapshots/files__shared_snapshot_container_proofs.snap is excluded by !**/*.snap
• egglog/tests/snapshots/files__shared_snapshot_container_set_collapse.snap is excluded by !**/*.snap
• egglog/tests/snapshots/files__shared_snapshot_rule_head_fast_path.snap is excluded by !**/*.snap

📒 Files selected for processing (55)

• .github/workflows/build.yml
• AGENTS.md
• README.md
• bench.py
• egglog-experimental/Cargo.toml
• egglog-experimental/src/container_primitives.rs
• egglog-experimental/src/either.rs
• egglog-experimental/src/lib.rs
• egglog-experimental/src/main.rs
• egglog-experimental/src/maybe.rs
• egglog-experimental/src/set_cost.rs
• egglog-experimental/tests/eggcc_2mm_proof.rs
• egglog-experimental/tests/files.rs
• egglog/.gitignore
• egglog/CHANGELOG.md
• egglog/Makefile
• egglog/core-relations/src/containers/mod.rs
• egglog/core-relations/src/containers/tests.rs
• egglog/core-relations/src/hash_index/mod.rs
• egglog/core-relations/src/hash_index/tests.rs
• egglog/core-relations/src/lib.rs
• egglog/core-relations/src/table_spec.rs
• egglog/core-relations/src/uf/mod.rs
• egglog/egglog-bridge/src/tests.rs
• egglog/scripts/nightly_bench.py
• egglog/scripts/requirements.txt
• egglog/src/ast/desugar.rs
• egglog/src/ast/mod.rs
• egglog/src/ast/parse.rs
• egglog/src/lib.rs
• egglog/src/prelude.rs
• egglog/src/proofs/mod.rs
• egglog/src/proofs/proof_checker.rs
• egglog/src/proofs/proof_container_rebuild.rs
• egglog/src/proofs/proof_encoding.md
• egglog/src/proofs/proof_encoding.rs
• egglog/src/proofs/proof_encoding_helpers.rs
• egglog/src/proofs/proof_extraction.rs
• egglog/src/proofs/proof_format.rs
• egglog/src/proofs/proof_normal_form.rs
• egglog/src/proofs/proof_simplification.rs
• egglog/src/proofs/proof_tests.rs
• egglog/src/scheduler.rs
• egglog/src/sort/fn.rs
• egglog/src/sort/map.rs
• egglog/src/sort/mod.rs
• egglog/src/sort/multiset.rs
• egglog/src/sort/pair.rs
• egglog/src/sort/set.rs
• egglog/src/sort/vec.rs
• egglog/src/termdag.rs
• egglog/src/typechecking.rs
• egglog/tests/container_rebuild.rs
• egglog/tests/files.rs
• test_bench.py

💤 Files with no reviewable changes (1)

• .github/workflows/build.yml

[saulshanabrook]

Closed in favor of #9 and #10 which split this for easier review