Skip to content

Merge upstream egglog: 41 commits, and it is faster everywhere - #45

Merged
saulshanabrook merged 9 commits into
saulshanabrook:mainfrom
oflatt-claude:upstream-merge
Aug 11, 2026
Merged

Merge upstream egglog: 41 commits, and it is faster everywhere#45
saulshanabrook merged 9 commits into
saulshanabrook:mainfrom
oflatt-claude:upstream-merge

Conversation

@oflatt-claude

@oflatt-claude oflatt-claude commented Aug 1, 2026

Copy link
Copy Markdown

This branch was cut on top of #44, but 452628f removes that PR's work, so this now stands alone: the diff is the upstream subtree merge (f327c769, 5da0a5c8) plus a rustdoc link fix (d771599), a merge of main (4327e9a), and the thread-count integration fixes below (2ebd348). #44's two commits are still in the log, but they contribute nothing to the diff — proof_encoding.rs, proof_encoding.md, and rebuild_cost.md match main exactly. Re-apply the uf_clear work on top once #44 lands.

egglog/ is a squash-based git subtree whose recorded split (6f0d26e3) was 41 commits / 9 upstream PRs behind egraphs-good/egglog.

Why merge now

Three of the missing PRs are search-path performance work, and one is our own lineage coming back refined.

  • #948 — per-subset column indexes as sorted arrays instead of hash maps. On-the-fly indexes are iterated once and probed a bounded number of times, so building a hash table was pure overhead.
  • #949 — shared trie roots across the plans of one rule-set run. Plans scanning the same table under the same fast constraints reuse one root, so per-subset index construction happens once per run rather than once per plan. This lands squarely on the encoding, which runs many plans over the same view and @UF tables every round.
  • #952 — monomorphized column gather behind index construction.
  • #955 / #914 — rebuild. #914 is our WIP: Materialized rebuild index + single-rule UF rebuild #19 lineage upstreamed and then refined: it adds an already-sorted fast path and the monomorphized gather, so upstream's hash_index is a strict superset of ours. Taken wholesale, with only our two downstream-only methods re-added.
  • #910 replaces rayon with an egglog-concurrency non-work-stealing pool and makes thread count per-EGraph.

Also: ~40 reachable panics became errors (#920), debug assertions in release tests (#917), a no-default-features build fix (#961), and new luminal inputs.

Measured

bench.py, 3 rounds per endpoint, serial, against 5cc4dc1. Ratios are candidate/baseline, so lower is better.

file native term proofs
eggcc-2mm-pass1 0.692 0.854 0.877
luminal-llama 0.844 0.963 0.964
hardboiled_conv1d_32 0.870 0.899 0.936
herbie 0.950 0.926 0.966
math-microbenchmark 0.965 0.943 0.962
pointer-analysis-small 0.990 1.013 1.172
geomean 0.879 0.932 0.975

Every treatment improves. The one regression is pointer-analysis-small under proofs, a 57 ms benchmark going to 67 ms.

Worth stating plainly: the win is largest for native and smallest for proofs, so proof mode's ratio to native gets worse even though its absolute time improves — eggcc-2mm-pass1 goes from 3.60x native to 4.56x. This merge is a real speedup for everyone; it is not progress toward the under-2x proof-mode target.

Integration work, not just conflict-picking

20 files, 59 hunks, 1383 conflict lines. Three resolutions were design decisions:

  1. The declared occurrence index cannot be a sorted array. Upstream changed DynamicIndex::DynamicColumn to hold SortedColumnIndex, but a declared (any …) index is disjunctive — one row is reachable under several keys — which a sorted array over one column cannot express. A separate DynamicIndex::DynamicOccurrence(Arc<ColumnIndex>) variant lets both coexist, so ordinary single-column atoms keep the full #948/#949 win.
  2. Backend gained set_num_threads/num_threads (defaulted, overridden for the bridge) so upstream's per-e-graph thread configuration reaches the backend SPI.
  3. Upstream's panic-to-error conversions were re-applied individually on top of our rewrites of fail desugaring, input_file, rule registration, and the scheduler, so upstream's tests/no_panic.rs passes unmodified.

Two expectation updates, both deterministic across reruns: the 5 new luminal programs join MANUAL_PROOF_DISABLED_FILES (keeping our manual_proof_disable_reason mechanism rather than upstream's parallel hardcoded list), and array_proof_testing records a different — still valid, still verified — derivation because the new index ordering changes which match is found first.

Merged main

main moved 38 commits ahead, so this branch merges it (4327e9a). #48 rewrote the same proof-encoding code the upstream merge touched: 7 conflict hunks in 4 files. #48 renamed delete_subsume_ruleset_name to subsume_ruleset_name; and its prove-exists now reads the proof off the view row instead of looking it up in a proof table, which deletes the block item 3 above had converted from a panic — so ProveExistsError::ProofsNotEnabled goes with it.

Three seams where upstream's per-e-graph thread count meets downstream code are fixed in 2ebd348: with_execution_state_tracked and get_container_value ran under the ambient pool rather than install_thread_pool(self.thread_pool(), …) like their siblings; with_term_encoding built its typechecker from a bare EGraph::default(), dropping the caller's thread count; and with_num_threads's doc still described the removed global rayon pool.

State

make rust-test (cargo test --workspace) 1497 passed, 0 failed
make rust-nits (fmt --check, clippy --all-targets, rustdoc -D warnings) clean

The Python side (make check) has not been run.

🤖 Generated with Claude Code

Summary by CodeRabbit

  • New Features

    • Added configurable per-instance thread counts for EGraphs and backend integrations.
    • Improved parallel execution and indexing performance with adaptive configuration.
    • Added support for safely escaping quotes and backslashes in displayed strings.
    • Preserved sort names containing hyphens during serialization.
  • Bug Fixes

    • Replaced many runtime crashes with actionable, source-located errors.
    • Improved handling of invalid inputs, malformed declarations, failed extraction, and primitive operations.
    • Added support for builds without default features.
  • Tests

    • Expanded coverage for concurrency, serialization, error handling, indexing, and large benchmarks.

oflatt and others added 5 commits July 31, 2026 23:29
The union-find's only readers are the maintenance rules: path compression,
the rebuild rules driven by a @uf delta, and the container rebuild
primitive. Once the rebuild loop saturates, every row a query, delete, or
subsume can reach is canonical, so the edges that got it there are dead.
Drop them, so the next iteration's rebuild reads only its own unions.

A @uf_clear ruleset holds one :naive delete-everything rule per eq-sort and
runs last in the maintenance schedule. Set EGGLOG_UF_CLEAR=0 to keep every
edge, which restores the previous encoding byte for byte.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…t-in

Clearing @uf each iteration is sound — 801 file tests pass with proof
snapshots byte-identical — but it is not faster. The rebuild rule is
:unsafe-seminaive, so its driving @uf atom already reads only the delta and
the rows a clear drops are ones its join never visits. At 6 rounds it is
1.006x on math-microbenchmark and 1.027x with +43 MiB on eggcc-2mm-pass1:
the clear costs +134 ms while @parent saves 27 ms. Time in @parent is 0.2-3%
of wall, so a free clear could not win more. It also loses stale-value
canonicalization, which find_canonical needs, and lets a rule re-deriving one
union per iteration keep saturate from terminating. Now off unless
EGGLOG_UF_CLEAR=1; the default encoding is unchanged byte for byte.

rebuild_cost.md records that and what the search time is actually made of:
the encoded rebuild is ~4.5x native's, native chooses its full-table-scan
branch on 93-99.8% of rebuilds where the encoding can never scan, and the
larger share of the gap on most files is in user rules rather than
maintenance -- for reasons that are not join width, contrary to what the two
desugared programs suggest.

EGGLOG_REBUILD_TRACE=1 logs native's per-table rebuild branch and its inputs.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
53b9721b Merge pull request #961 from oflatt-claude/fix/add-primitive-syn-full
5af563c8 Merge pull request #952 from egraphs-good/specialize-scan-and-refine
ead49f80 Merge remote-tracking branch 'origin/main' into specialize-scan-and-refine
c601b68f Merge pull request #955 from egraphs-good/perf-rebuild-patch-in-place
2630f5a9 add_primitive: depend on syn with the "full" feature
6575930c Merge pull request #917 from saulshanabrook/debug-assertions-release-tests
931a7558 Merge pull request #920 from egraphs-good/no-panic
60aa0844 Merge pull request #5 from egraphs-good/main
45866518 Merge branch 'main' into no-panic
0e1925eb don't sort if already sorted
572d154c Patch canonicalized rows in place in the rebuild output buffer
30eedcc1 Merge pull request #949 from egraphs-good/perf-shared-trie-nodes
e40dd754 fix nits
7971cb79 Monomorphize the column-gather loop used to build sorted column indexes
93e43d9d cherry-pick
225ad44d add a comment
9a84b92b Share trie roots across query plans within a rule-set run
56b84600 Merge pull request #948 from egraphs-good/perf-sorted-column-index
383b2bfa Exclude tests/header/ from test discovery
e67fb1c4 Bypass luminal transformer benchmarks in the test suite
14a81499 add more luminal benchmarks
1b5dea21 Build per-subset join indexes as sorted arrays instead of hash maps
6f0d696d bench: point harness at tests-bench and add transformer benchmarks
60eed0d8 Merge pull request #914 from egraphs-good/yihozhang-better-index-order-fix
4e7c8812 Only dedup the stdlib sort baseline for multi-column inputs
45ba1906 Unify unstable-fn primitive resolution errors with direct calls
7b4f81c3 Add microbenchmarks and random test
3bce29bc Fix issues from #898
a1918259 Merge remote-tracking branch 'origin/main' into no-panic
ced62ccc Merge remote-tracking branch 'origin/main' into yihozhang-better-index-order-fix
07ae68ea Replace Rayon with our own, non-workstealing thread pool (#910)
7bdf0465 Address review: keep internal prove-exists failures as invariants
a3ace918 Merge index-rebuild blocks with ping-pong buffers
53869105 Address review: keep proof-encoding internal parses as invariants
a66a4231 Add committed no-panic regression tests
d9783e0a Return errors instead of panicking for reachable failures
894b9ba5 Scope debug assertions to release tests
49d8020a Enable debug assertions in release builds
8ed30f98 Use balanced tournament merge for multi-column index rebuild
f895dfdb Rebuild ColumnIndex via per-column radix sort + merge
201579af Fix multi-column column index rebuild ordering

git-subtree-dir: egglog
git-subtree-split: 53b9721b9706741edff2b7c1e379fc37137184d9
Squashed subtree merge of egraphs-good/egglog 53b9721b (up from
6f0d26e3). Brings in the sorted-array per-subset column index, shared
trie roots, in-place rebuild patching, the radix-sort/tournament-merge
index rebuild, the egglog-concurrency thread pool replacing rayon, and
the reachable-panic-to-error conversions.

Integration notes:
- The encoding's occurrence index keeps its hash-keyed `ColumnIndex`
  through a new `DynamicIndex::DynamicOccurrence` variant, since a
  disjunctive index reaches one row under several keys and cannot be a
  sorted array over one column.
- `Backend` gains `set_num_threads`/`num_threads` so per-e-graph thread
  configuration reaches a custom backend.
- `(fail ...)` keeps this branch's multi-command form and now reports an
  empty expansion as an error.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The merge kept this branch's rewritten `fail` desugaring, `input_file`,
and rule registration, so upstream's no-panic conversions had to be
reapplied on top of them: an `include` or an empty expansion inside
`(fail ...)`, an unknown `(input ...)` target, and a duplicate rule name
now return an error. `parallel_execution_keeps_split_phase_timing_unavailable`
and the experimental `files` bench move to the per-e-graph thread pool.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
@coderabbitai

coderabbitai Bot commented Aug 1, 2026

Copy link
Copy Markdown

Review Change Stack

📝 Walkthrough

Walkthrough

This PR adds scoped per-EGraph thread pools, replaces Rayon-based relation execution, improves free-join and index processing, and converts many panic paths into structured errors. It also adds regression tests, benchmarks, CI checks, and changelog entries.

Changes

Runtime concurrency

Layer / File(s) Summary
Scoped pools and EGraph configuration
egglog/concurrency/..., egglog/egglog-bridge/..., egglog/src/lib.rs
Adds scoped ThreadPool APIs and per-EGraph thread configuration.
Relation and query execution
egglog/core-relations/...
Uses local parallel helpers, sorted indexes, shared trie roots, borrowed refinement, and configurable batching.
Diagnostics and fallible operations
egglog/src/..., egglog-experimental/src/...
Propagates type, desugaring, extraction, I/O, and primitive-resolution errors instead of panicking.
Validation and tooling
egglog/tests/..., egglog/concurrency/benches/..., .github/workflows/build.yml, egglog/Makefile
Adds concurrency, index, no-panic, serialization, and scheduler tests, plus benchmarks and CI coverage.

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

Possibly related PRs

Suggested reviewers: oflatt

🚥 Pre-merge checks | ✅ 5
✅ Passed checks (5 passed)
Check name Status Explanation
Docstring Coverage ✅ Passed Docstring coverage is 100.00% which is sufficient. The required threshold is 80.00%.
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.
Description Check ✅ Passed Check skipped - CodeRabbit’s high-level summary is enabled.
Title check ✅ Passed The title accurately identifies the upstream egglog merge and highlights the documented performance improvements.

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

codspeed-hq Bot commented Aug 1, 2026

Copy link
Copy Markdown

Merging this PR will not alter performance

✅ 6 untouched benchmarks


Comparing oflatt-claude:upstream-merge (452628f) with main (6333234)

Open in CodSpeed

Upstream's IndexCatalog doc links [`Arc`], but Arc is not imported in
hash_index, so `make rust-doc-links` fails under -D warnings. Upstream
does not run rustdoc with --document-private-items, so it never sees this.
@oflatt-claude oflatt-claude reopened this Aug 6, 2026
@saulshanabrook
saulshanabrook marked this pull request as ready for review August 7, 2026 13:05

@coderabbitai coderabbitai Bot left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actionable comments posted: 31

Caution

Some comments are outside the diff and can’t be posted inline due to platform limitations.

⚠️ Outside diff range comments (2)
egglog/src/proofs/rebuild_cost.md (1)

1-160: 📐 Maintainability & Code Quality | 🟠 Major | ⚡ Quick win

Reduce the document to the supported contract.

This file includes commit-specific measurements and untested explanations. Move the experiment log to the PR or a tracking issue. Keep only the caller-facing behavior of EGGLOG_UF_CLEAR and EGGLOG_REBUILD_TRACE.

Before merge, run cd egglog && make nits.

🤖 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/src/proofs/rebuild_cost.md` around lines 1 - 160, Reduce
rebuild_cost.md to documented caller-facing behavior for EGGLOG_UF_CLEAR and
EGGLOG_REBUILD_TRACE only. Remove commit-specific benchmarks, experiment
results, and untested hypotheses, moving them to the PR or tracking issue
instead; retain only supported usage and semantics for both environment
variables. Before completing the change, run cd egglog && make nits.

Source: Coding guidelines

egglog/core-relations/src/table/sharded_hash_table.rs (1)

16-21: 🚀 Performance & Scalability | 🟠 Major | ⚡ Quick win

Pass EGraph thread count into ShardedHashTable::default() construction.

SortedWritesTable::new creates ShardedHashTable::<TableEntry>::default() before the parallel execution pool can be installed. egglog_concurrency::current_num_threads() returns 1 outside an installed pool, so the table keeps one shard and parallel_delete later maps onto that single shard. Move shard initialization to EGraph::with_num_threads/EGraph, or pass the intended shard count explicitly, instead of relying on thread-local pool installation at construction time.

🤖 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/core-relations/src/table/sharded_hash_table.rs` around lines 16 - 21,
Update ShardedHashTable construction used by SortedWritesTable::new so it
receives the intended EGraph thread count rather than calling default() before
the execution pool is installed. Thread the count through
EGraph::with_num_threads/EGraph initialization or pass it explicitly when
creating the table, ensuring shard initialization reflects the configured
parallelism.
🤖 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/benches/rust_api_benchmarking.rs`:
- Line 299: Update the benchmark setup around EGraph::new(1) to use the same
EGraph::default() construction as the other Rust API benchmarks, unless this
benchmark explicitly requires a different thread count.

In `@egglog/CHANGELOG.md`:
- Line 62: Update the changelog entry’s compound modifier to hyphenate
“egglog-concurrency-scoped” before “ThreadPool,” leaving the surrounding content
unchanged.
- Line 27: Shorten the changelog entry by replacing the exhaustive
implementation inventory with concise user-facing bullets covering the major
behavior changes: recoverable errors instead of panics, partial numeric and
collection primitives, improved scheduler and variable-free rule handling,
explicit primitive-resolution errors, and safe scheduler-state restoration.
Remove the detailed examples and implementation-level symbol lists from this
entry.

In `@egglog/concurrency/benches/sum_vector.rs`:
- Line 7: Reduce DEFAULT_ITEMS to a substantially smaller default that avoids
excessive memory use during a standard cargo bench run, or add a module comment
beside it documenting the approximately 1 GiB resident-memory requirement caused
by data() retaining the u32 vector.

In `@egglog/concurrency/src/threadpool/mod.rs`:
- Around line 390-407: Remove the unsynchronized `self.state.sender.take()`
mutation from `ThreadPool::drop`. Keep the owning sender in `ThreadPool` so
dropping it closes the channel only after workers are no longer using shared
`ThreadPoolState`, or place sender access behind synchronization and update
`Scope::new` to clone it through that mechanism. Preserve the
`ThreadPoolStatePtr` invariant that workers only read immutable state and retain
the existing worker-join shutdown behavior.

In `@egglog/concurrency/src/threadpool/tests.rs`:
- Around line 352-357: Extend dropping_pool_closes_workers to submit work that
remains queued or running, keep a worker occupied with synchronization, then
drop the ThreadPool in a nested scope while that work is in flight. Ensure the
test waits for the job or synchronization signal afterward so worker shutdown
completes, exercising concurrent sender removal and worker access to
ThreadPoolState.

In `@egglog/core-relations/benches/build_index.rs`:
- Around line 81-88: Update build_parallel to create or install the thread pool
outside the bench_refs timed closure, reusing it for every input build. Avoid
calling with_threads inside the per-iteration closure; if Bencher ownership
prevents wrapping the sampling loop, add a bench_support helper that constructs
a reusable pool and executes the benchmark through it.

In `@egglog/core-relations/src/free_join/execute.rs`:
- Around line 1489-1491: In the comment near drain_updates_parallel, correct the
typo “eevn” to “even” without changing the surrounding explanation.
- Around line 458-479: In the trie_cache initialization block, remove the stale
first documentation paragraph describing database-size gating, growing
estimates, and small-run behavior. Keep the following paragraph that accurately
explains enabling sharing only when shared roots exist and the resulting None
behavior.
- Around line 1027-1036: Move the TrieNode child-subset computation out of the
map write lock in the cache-miss path around TrieNode::new and the children map
guard. Compute sub() before acquiring guard, then recheck the value and edge_cs
under the lock, returning the existing node when matched and otherwise inserting
the precomputed node; preserve the race-loser discard behavior and run the
release performance check via script/bench.py or make test.
- Around line 196-215: Update SortedColumnIndex::build_for_subset to allocate
the scratch buffer only when pairs.len() meets the radix-sort threshold used by
radix_sort_slice_by_value (64 or greater); pass the appropriately sized buffer
to that sorter while preserving the existing sorting and index construction
behavior. Measure the performance impact with script/bench.py before landing the
change.
- Around line 1149-1164: Update root_node so an empty result from
build_root_subset is represented by and inserted into trie_cache.roots before
returning, rather than propagating None before roots.entry(key). Cache the
shared empty TrieNode under the computed RootKey, while preserving the existing
non-empty node reuse and return behavior.

In `@egglog/core-relations/src/hash_index/mod.rs`:
- Around line 1093-1108: Update
egglog/core-relations/src/hash_index/mod.rs:1093-1108 so the index thread pool
derives its width from the configured backend thread count at use time rather
than a first-use global snapshot, and make num_shards() use that same worker
width. Update egglog/core-relations/src/hash_index/bench_support.rs:77-81 to
state that with_threads affects shard count only, not ColumnIndex worker-pool
size. Update egglog/core-relations/src/hash_index/tests.rs:290-296 to state that
installing a four-thread pool raises shard count but does not make the merge
fork.
- Around line 34-36: Update the core-relations dependency configuration so rand
is excluded from regular builds: move rand from [dependencies] to
[dev-dependencies], and adjust the bench_support module exposure or feature
gating as needed to keep benchmark consumers working without a normal-library
rand dependency.

In `@egglog/core-relations/src/hash_index/tests.rs`:
- Around line 290-296: The comment above the local ThreadPool installation
incorrectly claims it forces merge_parallel to fork. Update that comment to
state only that the pool changes num_shards() and exercises the
multi-shard/sharded code path, while retaining the existing correctness intent
and assertions.
- Around line 255-257: Update the randomized oracle test’s body to invoke
ColumnIndex::build_for_subset with a small single-column subset that exercises
its row-at-a-time branch, then assert its output matches the existing sorted,
de-duplicated oracle alongside rebuild_full and merge_parallel. Keep the
documentation claim only if this coverage is added.

In `@egglog/core-relations/src/parallel_heuristics.rs`:
- Around line 77-114: Update the parallel heuristics documentation by adding a
changelog bullet and a module-level list covering all eight EGGLOG_PARALLEL_*
environment overrides with their defaults. In cutoff, distinguish missing
variables from present-but-unparsable values and do not silently use the default
for invalid input; preserve default fallback only when the variable is absent.

In `@egglog/core-relations/src/parallel.rs`:
- Around line 78-111: Add a focused test in the parallel relations test module
that compares parallel and serial results from map_mut and map across several
input lengths, including lengths not divisible by the configured chunk size.
Initialize a multi-thread pool so the parallel path executes, and assert that
result ordering and global indices match the serial implementation.

In `@egglog/core-relations/src/row_buffer/mod.rs`:
- Around line 447-477: Refactor add_row to delegate its row insertion to
add_row_with, supplying a no-op patch closure so the shared arity validation,
refresh, data pushes, and total_rows update exist only in add_row_with. Preserve
add_row’s current return value and row/RowId behavior, and remove any duplicated
insertion sequence or synchronization comment that is no longer needed.

In `@egglog/core-relations/src/table/mod.rs`:
- Around line 634-641: Update the comments in
egglog/core-relations/src/table/mod.rs at lines 634-641 and 949-951: in the
SAFETY comment around set_stale_shared, replace the per-shard thread claim with
wording that each task owns a disjoint set of shards; move the read_handle
batching comment to the let read_handle = row_writer.read_handle() statement, or
remove it if redundant.
- Around line 1161-1166: Update the setup around parallel::for_each_mut to
preserve the scratch pointer returned by self.data.scratch.raw_rows() as a raw
pointer rather than converting it to usize; capture it in the required Send
wrapper and reconstruct/use the pointer inside the closure without an integer
round trip.

In `@egglog/core-relations/src/table/rebuild.rs`:
- Around line 158-179: Update the incremental rebuild path around the
`parallel::map` over `ids` so mutation buffers, cloned execution state, and
`TaggedRowBuffer` scratch storage are allocated once per work chunk rather than
once per scanned id. Add or reuse a chunked parallel helper in `parallel.rs`, or
partition `ids` into slices before mapping, while preserving per-id subset
lookup and row processing; at minimum, defer `new_buffer()` and
`exec_state.clone()` until after `rebuild_index.get_subset(id)` confirms work
exists.
- Around line 63-78: Update the trace handling in do_rebuild to call a cached
rebuild_trace_enabled accessor backed by OnceLock instead of reading
EGGLOG_REBUILD_TRACE directly. Hoist the incremental_rebuild predicate into a
local and reuse it for both the trace branch label and the existing rebuild
selection, avoiding duplicate evaluation. Add rebuild_trace_enabled near the
bottom of the file.

In `@egglog/egglog-bridge/src/lib.rs`:
- Around line 162-180: Add a # Panics section to the doc comments for the public
methods EGraph::new, EGraph::with_num_threads, and EGraph::set_num_threads,
documenting that they panic on wasm when the requested thread count exceeds one.
Keep the existing behavior in normalize_thread_count unchanged.
- Around line 1233-1234: Update with_execution_state_tracked and
get_container_value to invoke their self.db operations inside
install_thread_pool(self.thread_pool(), ...), matching the existing
execution-state wrapper. Ensure both entry points consistently use the EGraph’s
configured thread pool rather than the ambient pool.

In `@egglog/src/lib.rs`:
- Around line 696-700: Preserve the caller-selected thread count when term
encoding creates the original typechecker: update the default typechecker
initialization in enable_term_encoding (or the corresponding attachment path) to
use self.num_threads() instead of EGraph::default() settings. Keep
set_num_threads synchronized for already-attached original_typechecking
instances.

In `@egglog/src/proofs/proof_encoding_helpers.rs`:
- Line 59: Remove runtime UF-clearing semantics from proof encoding: delete the
uf_clear_ruleset_name field and its allocation/environment switch in
proof_encoding_helpers.rs (lines 59, 372, and 381-392), and stop declaring the
destructive ruleset there (lines 518-535). In proof_encoding.rs (lines 739-765
and 2053-2068), remove generation and scheduling of rules that delete persistent
union-find edges. Update proof_encoding.md (lines 293-296) to describe the
behavior only as an isolated benchmark-only experiment, if retained.

In `@egglog/src/proofs/proof_extraction.rs`:
- Around line 17-18: Update the ProofsNotEnabled error message and the
associated prove-exists validation path to report that prove-exists requires a
proof-enabled equality-sort result, not merely globally enabled proofs;
alternatively introduce a distinct error for base-sort outputs and return it
from that path.

In `@egglog/src/sort/fn.rs`:
- Around line 120-141: Update the input-name collection in the presort argument
handling around `Self::presort_name()` so each input variable retains its
original expression span alongside its name. Use that input span when
constructing `TypeError::UndefinedSort` for missing sorts, while preserving the
existing validation and successful sort lookup behavior.

In `@egglog/src/sort/multiset.rs`:
- Line 531: Prevalidate every multiplicity in the row before calling
action.insert in the surrounding multiset-building flow, rejecting any value
that cannot convert to isize. Only insert the row after all conversions succeed,
and preserve the existing None return behavior without leaving ExecutionState
partially updated, including the FullPrim path.

In `@egglog/tests/no_panic.rs`:
- Around line 50-52: Remove the user-reachable todo! handling for non-trivial
BigRat log and cbrt operations, routing these failures through
parse_and_run_program as structured errors instead. Preserve separate outcomes
for unsupported operations versus valid operations that have no rational result,
and add regression cases in the relevant tests after the fallible path is
implemented.

---

Outside diff comments:
In `@egglog/core-relations/src/table/sharded_hash_table.rs`:
- Around line 16-21: Update ShardedHashTable construction used by
SortedWritesTable::new so it receives the intended EGraph thread count rather
than calling default() before the execution pool is installed. Thread the count
through EGraph::with_num_threads/EGraph initialization or pass it explicitly
when creating the table, ensuring shard initialization reflects the configured
parallelism.

In `@egglog/src/proofs/rebuild_cost.md`:
- Around line 1-160: Reduce rebuild_cost.md to documented caller-facing behavior
for EGGLOG_UF_CLEAR and EGGLOG_REBUILD_TRACE only. Remove commit-specific
benchmarks, experiment results, and untested hypotheses, moving them to the PR
or tracking issue instead; retain only supported usage and semantics for both
environment variables. Before completing the change, run cd egglog && make nits.
🪄 Autofix

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: Organization UI

Review profile: ASSERTIVE

Plan: Pro Plus

Run ID: 541e772e-7f44-48d8-8072-d0172505c686

📥 Commits

Reviewing files that changed from the base of the PR and between 3364576 and d771599.

⛔ Files ignored due to path filters (19)
  • Cargo.lock is excluded by !**/*.lock
  • egglog/Cargo.lock is excluded by !**/*.lock
  • egglog/tests/cykjson.egg is excluded by !**/*.egg
  • egglog/tests/gemma.egg is excluded by !**/*.egg
  • egglog/tests/gemma4_moe.egg is excluded by !**/*.egg
  • egglog/tests/header/luminal-header.egg is excluded by !**/*.egg
  • egglog/tests/llama.egg is excluded by !**/*.egg
  • egglog/tests/paged_llama.egg is excluded by !**/*.egg
  • egglog/tests/qwen.egg is excluded by !**/*.egg
  • egglog/tests/qwen3_moe.egg is excluded by !**/*.egg
  • egglog/tests/snapshots/files__proof_manual_disabled_files.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__proofs__array_proof_testing.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__shared_snapshot_eggcc_2mm.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__shared_snapshot_llama.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__shared_snapshot_paged_llama.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__shared_snapshot_qwen.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__shared_snapshot_qwen3_moe.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__shared_snapshot_whisper.snap is excluded by !**/*.snap
  • egglog/tests/whisper.egg is excluded by !**/*.egg
📒 Files selected for processing (70)
  • egglog-experimental/benches/files.rs
  • egglog-experimental/src/either.rs
  • egglog-experimental/src/maybe.rs
  • egglog/.github/workflows/build.yml
  • egglog/CHANGELOG.md
  • egglog/Cargo.toml
  • egglog/Makefile
  • egglog/benches/common.rs
  • egglog/benches/rust_api_benchmarking.rs
  • egglog/concurrency/Cargo.toml
  • egglog/concurrency/benches/sum_vector.rs
  • egglog/concurrency/src/lib.rs
  • egglog/concurrency/src/threadpool/mod.rs
  • egglog/concurrency/src/threadpool/tests.rs
  • egglog/core-relations/Cargo.toml
  • egglog/core-relations/benches/build_index.rs
  • egglog/core-relations/src/containers/mod.rs
  • egglog/core-relations/src/free_join/execute.rs
  • egglog/core-relations/src/free_join/mod.rs
  • egglog/core-relations/src/hash_index/bench_support.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/parallel.rs
  • egglog/core-relations/src/parallel_heuristics.rs
  • egglog/core-relations/src/pool/mod.rs
  • egglog/core-relations/src/row_buffer/mod.rs
  • egglog/core-relations/src/table/mod.rs
  • egglog/core-relations/src/table/rebuild.rs
  • egglog/core-relations/src/table/sharded_hash_table.rs
  • egglog/core-relations/src/table_spec.rs
  • egglog/core-relations/src/tests.rs
  • egglog/core-relations/src/uf/mod.rs
  • egglog/egglog-ast/src/generic_ast_helpers.rs
  • egglog/egglog-backend-trait/src/backend_impl.rs
  • egglog/egglog-backend-trait/src/lib.rs
  • egglog/egglog-bridge/Cargo.toml
  • egglog/egglog-bridge/src/lib.rs
  • egglog/numeric-id/Cargo.toml
  • egglog/numeric-id/src/lib.rs
  • egglog/scripts/bench.py
  • egglog/src/ast/desugar.rs
  • egglog/src/cli.rs
  • egglog/src/constraint.rs
  • egglog/src/core.rs
  • egglog/src/extract.rs
  • egglog/src/lib.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/rebuild_cost.md
  • egglog/src/scheduler.rs
  • egglog/src/serialize.rs
  • egglog/src/sort/add_primitive/Cargo.toml
  • egglog/src/sort/add_primitive/src/lib.rs
  • egglog/src/sort/bigint.rs
  • egglog/src/sort/fn.rs
  • egglog/src/sort/i64.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/typechecking.rs
  • egglog/tests/files.rs
  • egglog/tests/integration_test.rs
  • egglog/tests/no_panic.rs
  • egglog/tests/typed_primitive.rs
💤 Files with no reviewable changes (2)
  • egglog/Cargo.toml
  • egglog/numeric-id/Cargo.toml

Comment thread egglog/benches/rust_api_benchmarking.rs
Comment thread egglog/CHANGELOG.md
Comment thread egglog/CHANGELOG.md
Comment thread egglog/concurrency/benches/sum_vector.rs
Comment thread egglog/concurrency/src/threadpool/mod.rs
Comment thread egglog/src/proofs/proof_encoding_helpers.rs Outdated
Comment thread egglog/src/proofs/proof_extraction.rs Outdated
Comment thread egglog/src/sort/fn.rs
Comment thread egglog/src/sort/multiset.rs
Comment thread egglog/tests/no_panic.rs
oflatt added 2 commits August 7, 2026 16:14
# Conflicts:
#	egglog/egglog-bridge/src/lib.rs
#	egglog/src/proofs/proof_encoding.rs
#	egglog/src/proofs/proof_encoding_helpers.rs
#	egglog/src/proofs/proof_extraction.rs
Upstream's per-e-graph thread count (#910) meets three downstream seams
this merge created:

- `with_execution_state_tracked` and `get_container_value` called
  `self.db` directly, so they ran under the ambient pool while their
  siblings wrapped in `install_thread_pool`.
- `with_term_encoding` built its typechecker from a bare
  `EGraph::default()`, dropping the caller's thread count; the three
  sibling paths all inherit it.
- `with_num_threads`'s doc still described the removed global rayon
  pool, under a `# Panics` heading with no body. Restored upstream's text.

@coderabbitai coderabbitai Bot left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Caution

Some comments are outside the diff and can’t be posted inline due to platform limitations.

⚠️ Outside diff range comments (2)
egglog/src/sort/map.rs (2)

93-100: 🎯 Functional Correctness | 🟠 Major | ⚡ Quick win

Reject non-injective maps in inverse.

Line 99 silently overwrites an earlier key when two map keys have the same value. map-insert permits that input, so (inverse {1 ↦ 3, 2 ↦ 3}) currently returns {3 ↦ 2} instead of reporting that no inverse exists.

Make both inverse aliases fallible and reject duplicate inverse keys.

Proposed fix
-fn renaming_inverse(m: &BTreeMap<Value, Value>) -> BTreeMap<Value, Value> {
-    m.iter().map(|(k, v)| (*v, *k)).collect()
+fn renaming_inverse(m: &BTreeMap<Value, Value>) -> Option<BTreeMap<Value, Value>> {
+    let mut inverse = BTreeMap::new();
+    for (key, value) in m {
+        if inverse.insert(*value, *key).is_some_and(|old| old != *key) {
+            return None;
+        }
+    }
+    Some(inverse)
 }
 
-add_primitive!(eg, "inverse" = |a: `@MapContainer` (arc)| -> `@MapContainer` (arc) { MapContainer { data: renaming_inverse(&a.data), ..a } });
-add_primitive!(eg, "map-inverse" = |a: `@MapContainer` (arc)| -> `@MapContainer` (arc) { MapContainer { data: renaming_inverse(&a.data), ..a } });
+add_primitive!(eg, "inverse" = |a: `@MapContainer` (arc)| -?> `@MapContainer` (arc) {
+    Some(MapContainer { data: renaming_inverse(&a.data)?, ..a })
+});
+add_primitive!(eg, "map-inverse" = |a: `@MapContainer` (arc)| -?> `@MapContainer` (arc) {
+    Some(MapContainer { data: renaming_inverse(&a.data)?, ..a })
+});

Also applies to: 344-346

🤖 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/src/sort/map.rs` around lines 93 - 100, Update renaming_inverse and
both inverse aliases to be fallible, detect duplicate values while constructing
the inverse map, and return an error instead of overwriting an existing key.
Propagate this failure through the inverse operation so non-injective maps such
as multiple keys mapping to the same value are rejected.

337-354: 🎯 Functional Correctness | 🟡 Minor | ⚡ Quick win

Mark the new map primitives as proof-unsupported.

map-union, compose, inverse, map-inverse, and find-mapping are registered without validators, so proof mode rejects them as unsupported proof commands. Add an explicit note that these renaming helpers are runtime-only, or add validators and the corresponding proof-mode regression tests.

🤖 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/src/sort/map.rs` around lines 337 - 354, Mark the map primitives
map-union, compose, inverse, map-inverse, and find-mapping as explicitly
unsupported in proof mode, using the repository’s established runtime-only
annotation or registration mechanism. Apply this to each add_primitive!
registration, including the conditionally registered renaming helpers, without
changing their runtime behavior.
🤖 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.

Outside diff comments:
In `@egglog/src/sort/map.rs`:
- Around line 93-100: Update renaming_inverse and both inverse aliases to be
fallible, detect duplicate values while constructing the inverse map, and return
an error instead of overwriting an existing key. Propagate this failure through
the inverse operation so non-injective maps such as multiple keys mapping to the
same value are rejected.
- Around line 337-354: Mark the map primitives map-union, compose, inverse,
map-inverse, and find-mapping as explicitly unsupported in proof mode, using the
repository’s established runtime-only annotation or registration mechanism.
Apply this to each add_primitive! registration, including the conditionally
registered renaming helpers, without changing their runtime behavior.

ℹ️ Review info
⚙️ Run configuration

Configuration used: Organization UI

Review profile: ASSERTIVE

Plan: Pro Plus

Run ID: 03c77555-18b8-42f6-ac18-62d48d632da6

📥 Commits

Reviewing files that changed from the base of the PR and between d771599 and 2ebd348.

📒 Files selected for processing (15)
  • egglog/CHANGELOG.md
  • egglog/core-relations/src/table/mod.rs
  • egglog/core-relations/src/tests.rs
  • egglog/egglog-backend-trait/src/backend_impl.rs
  • egglog/egglog-backend-trait/src/lib.rs
  • egglog/egglog-bridge/src/lib.rs
  • egglog/src/ast/desugar.rs
  • egglog/src/extract.rs
  • egglog/src/lib.rs
  • egglog/src/proofs/proof_encoding.md
  • egglog/src/proofs/proof_encoding.rs
  • egglog/src/proofs/proof_encoding_helpers.rs
  • egglog/src/sort/map.rs
  • egglog/src/typechecking.rs
  • egglog/tests/integration_test.rs
💤 Files with no reviewable changes (1)
  • egglog/src/ast/desugar.rs

This branch was cut on top of saulshanabrook#44, so its diff carried that PR's
`uf_clear` knob and rebuild-cost measurement. None of it is needed to
merge upstream, and reviewing the two together conflates them.

Removes the `EGGLOG_UF_CLEAR` switch and its generated ruleset, rule,
and schedule step; the `EGGLOG_REBUILD_TRACE` logging in
`table/rebuild.rs`; and `rebuild_cost.md` with the paragraph citing it.
`proof_encoding.rs`, `proof_encoding.md`, and `rebuild_cost.md` now
match `main` exactly. Re-apply on top once saulshanabrook#44 lands.

@coderabbitai coderabbitai Bot left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Caution

Some comments are outside the diff and can’t be posted inline due to platform limitations.

⚠️ Outside diff range comments (1)
egglog/src/proofs/proof_encoding_helpers.rs (1)

478-480: 🩺 Stability & Availability | 🟠 Major | 🏗️ Heavy lift

Return generated-parse failures as errors.

parse_program, parse_program_as_local_actions, term_header, parse_schedule, parse_facts, parse_expr, and related helpers still panic through Result::expect when generated text is rejected. Change these helpers to return Result, restore egraph.parser.ensure_no_reserved_symbols with a scope guard, and propagate the errors through term_encode_command and term_encode.

🤖 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/src/proofs/proof_encoding_helpers.rs` around lines 478 - 480, Replace
expect-based handling in the generated-program parsing helpers, including
parse_program, parse_program_as_local_actions, term_header, parse_schedule,
parse_facts, and parse_expr, with propagated Result errors. Restore
egraph.parser.ensure_no_reserved_symbols using a scope guard, then update
term_encode_command and term_encode to return and propagate these parsing
failures instead of panicking.
🤖 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.

Outside diff comments:
In `@egglog/src/proofs/proof_encoding_helpers.rs`:
- Around line 478-480: Replace expect-based handling in the generated-program
parsing helpers, including parse_program, parse_program_as_local_actions,
term_header, parse_schedule, parse_facts, and parse_expr, with propagated Result
errors. Restore egraph.parser.ensure_no_reserved_symbols using a scope guard,
then update term_encode_command and term_encode to return and propagate these
parsing failures instead of panicking.

ℹ️ Review info
⚙️ Run configuration

Configuration used: Organization UI

Review profile: ASSERTIVE

Plan: Pro Plus

Run ID: 1df05380-6c94-47fe-9f18-00ed2fdf981b

📥 Commits

Reviewing files that changed from the base of the PR and between 2ebd348 and 452628f.

📒 Files selected for processing (2)
  • egglog/core-relations/src/table/rebuild.rs
  • egglog/src/proofs/proof_encoding_helpers.rs
💤 Files with no reviewable changes (1)
  • egglog/core-relations/src/table/rebuild.rs

@saulshanabrook saulshanabrook left a comment

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good!

No merge-specific findings. PR #45 looks safe to merge from a code/integration
standpoint.

  • Clean worktree: /Users/saul/p/wt/egglog-encoding/pr45-upstream-merge

  • Local and live PR head match: 452628f

  • The merged main parent is the current base SHA, so there is no base drift.

  • The subtree squash tree exactly matches upstream 53b9721b.

  • Audited the manual subtree and main conflict resolutions; downstream
    occurrence indexes, proof behavior, panic-to-error handling, and per-EGraph
    threading were preserved.

  • Confirmed #44’s work is fully absent from the final diff.

  • make check passed, including 172 Python tests and the complete Rust
    workspace suite.

  • make benchmark-smoke passed with both off and proofs.

  • All seven GitHub checks are green and all 31 CodeRabbit threads are
    resolved.

@saulshanabrook
saulshanabrook merged commit bd4752e into saulshanabrook:main Aug 11, 2026
7 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants