Evaluator cache, prover speed, flaky pong spec, parallel CI - #12
Merged
Merged
Conversation
added 2 commits
September 25, 2026 10:50
'(a b) and '[a b] are = in Clojure, so a law quoting a list ran the fn compiled for an earlier law quoting the same elements as a vector, and failed or passed depending on which law came first.
The examples ran one after another in a single job, 30-40 minutes, and a hang sat until the 6 hour limit. The runner now takes the namespaces to run, and rejects names it doesn't know so a typo can't pass.
yogthos
changed the title
added 7 commits
September 25, 2026 12:20
A CI job ran for an hour with no output, so a slow check and a hang looked the same. Give pong, which proves every edge of its graph, a longer timeout.
Pong's checks spend most of their time proving its graph edges. writ already takes a cached proof only when its own source, the spec and the code are unchanged, so restoring an older cache is safe.
sort-by with pr-str prints both sides of every comparison, so a sorted set of facts was printed about 2 log n times per fact.
A trace shares its subterms, and summary walked it seven times with tree-seq, which expands the sharing: pong's traces have 16k distinct nodes walked as 325k. The prover's own pr-str sorts move to t/sort-printed too. The summary no longer says "with the solver" twice when a proof both evaluated symbolically and called the solver.
A jolt release with the new loop-local check rejects the loop otherwise, and writ would stop loading.
The search stops at the first witness, so this costs time only when one is rare. Pong's playing -> won step needs a game a point from won with the ball past the paddle, and 100 values sometimes had none, failing the spec at random. With that step found, the adequacy check ran for seeds it had been skipped on, and showed no law pinned new-game down; pong's spec now says what a new game is.
yogthos
changed the title
It finishes in under four minutes now.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The evaluator cached compiled term fns under [vars term]. '(a b) and '[a b] are = in Clojure, so a law quoting a list got the fn compiled for an earlier law quoting a vector with the same elements. Found in ensemble's pattern spec.
The prover sorted terms with sort-by pr-str, printing both sides of every comparison, and summarised each proof trace with seven tree-seq walks that expand shared subtrees (pong: 16k distinct nodes walked as 325k). Terms are printed once now, and the summary walks each subtree once.
search.clj binds first-pass with an if, so writ keeps loading once jolt's loop-local check ships.
An exists witness is looked for among at least 1000 values. Pong's playing -> won step sometimes had none in 100, failing the spec at random; once found, the adequacy check showed nothing pinned new-game down, so the spec now says what a new game is.
CI: each example runs as its own job with a timeout, jolt is pinned so the parallel installs don't hit the API rate limit, the runner prints each test as it runs, and the examples' proof cache is kept between runs. Pong was also slow from a quadratic concat in jolt, fixed in jolt-lang/jolt#1143.