Run a fixed corpus on every commit, reporting solved / wrong / error / timeout (#529, #500) - #945
Merged
Merged
Conversation
…d timeout (#529, #500) #746 v1.0 names this as required infrastructure and it was the last piece of it not built. The point is the four-way split. A suite that passes or fails cannot tell answered wrongly from declined to answer, and AGENTS.md is explicit that a change solving one more problem and introducing one wrong answer is a regression rather than progress -- which a green suite would report as progress. Forty problems across simplification, solving, integration and limits, each carrying the verdict it currently earns. The gate fails on any wrong answer, and on any case that stops matching its recorded verdict -- including one that improves, so that the record cannot quietly drift from the library. Answers are checked rather than compared against stored text. A root is substituted back into its equation, an antiderivative is differentiated back, a simplification is evaluated against the expression it came from. So the corpus does not record what the library happens to print today, a change of form is not a failure, and only a change of value is. Sampling is complex and off the axes on purpose: a rule that is wrong away from the real line is the kind this library keeps finding, and real sample points cannot see it. A point where both sides are undefined proves nothing and is skipped; a point where one has a value and the other does not is a disagreement, which is how a rewrite that widens or narrows a domain gets caught. Two things the first run caught, both in the checking rather than in the library. A root may carry a parameter -- sin(x) = 0 is solved by 2*pi*n for every integer n -- and calling that unverifiable would have marked a correct answer unsolved. Each parameter is given four integer values, so solve:trig now verifies eight roots and checks the parameterisation rather than one branch of it. An antiderivative is checked on the positive reals rather than off the axis, unlike everything else here. The integral of 1/x comes back as ln(abs(x)) + C, and abs is not holomorphic, so differentiating it does not reproduce 1/x away from the real line. Whether ln(x) is the better answer is a real question, and it is not one a regression gate should settle by failing every build until somebody answers it. It is worth answering separately. This is a gate and not the harness. The harnesses stay outside the repository where they can generate inputs, take minutes and be read by a person; this runs in CI on every commit, takes about a second, and answers one question: did anything get worse. The problems are the library's own, from its issue tracker, plus a few standard limits; nothing is vendored from another project's suite. Measured on this tree: solved 39, unsolved 1, wrong 0, error 0, timeout 0, of 40. Suite 7119 passed / 0 failed. #529 #500 #746 Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
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
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.
#746 v1.0 names this as required infrastructure, and it was the last piece of it not built.
The point is the four-way split. A suite that passes or fails cannot tell answered wrongly from declined to answer — and
AGENTS.mdis explicit that a change which solves one more problem and introduces one wrong answer is a regression. A green suite would report that as progress.Forty problems across simplification, solving, integration and limits, each carrying the verdict it currently earns. The gate fails on any wrong answer, and on any case that stops matching its recorded verdict — including one that improves, so the record cannot quietly drift from the library.
Answers are checked, not compared to stored text
A root is substituted back into its equation. An antiderivative is differentiated back. A simplification is evaluated against the expression it came from. So the corpus does not record what the library happens to print today: a change of form is not a failure, and only a change of value is.
Sampling is complex and off the axes on purpose — a rule that is wrong away from the real line is the kind this library keeps finding, and real sample points cannot see it. A point where both sides are undefined proves nothing and is skipped; a point where one has a value and the other does not is a disagreement, which is how a rewrite that widens or narrows a domain gets caught.
Two things the first run caught — both in my checking, not in the library
A root may carry a parameter.
sin(x) = 0is solved by2*pi*nfor every integern, and calling that unverifiable would have marked a correct answer unsolved. Each parameter now gets four integer values, sosolve:trigverifies eight roots and checks the parameterisation rather than one branch of it.An antiderivative is checked on the positive reals, unlike everything else here.
∫1/xcomes back asln(abs(x)) + C, andabsis not holomorphic, so differentiating it does not reproduce1/xaway from the real line.Whether
ln(x)would be the better answer is a real question — most CAS return it, and differentiating the current answer does not give back the integrand off the reals. But it is not a question a regression gate should settle by failing every build until someone answers it. Worth raising separately; I have not changed the behaviour.A gate, not a harness
The measurement harnesses stay outside the repository, where they can generate inputs, take minutes, and be read by a person. This runs in CI on every commit, takes about a second, and answers one question: did anything get worse. It needs no new workflow — it rides the existing test job.
The problems are the library's own, drawn from its issue tracker where each was reported as something that ought to work, plus a few standard limits. Nothing is vendored from another project's test suite.
Measured
Suite 7119 passed / 0 failed. The corpus pins several recent gains —
solve:quintic-factorableverifies all five roots, which is #918's improvement held in place.Closes the last v1.0 infrastructure item alongside #529 and #500.
🤖 Generated with Claude Code