asc-community / asc-community/AngouriMath

The property harnesses run in 8.5 minutes and CI runs none of them

Open
#1,256 1 comment 0 reactions 0 assignees View on GitHub
Proposal
Dominant language
C#
Stars
831
Forks
79
Avg merge
3h 23m
Merged PRs (30d)
309

Description

#746's standing condition *"correctness coverage grows with the surface"* is marked **Met**, with one caveat attached: the in-CI corpus is small and a set of property harnesses exists that CI never runs. This issue is about that caveat, and it is filed because measuring it showed the obstacle is not what I assumed.

### The measurement

Ten self-contained harnesses, run one at a time against `2dbeedf7` on one desktop, library already built:

| harness | what it asks | wall |
|---|---|---|
| `confluence` | do the rule sets converge | 2s |
| `boundcheck` | does `Simplify` keep the value **at the boundary** — across a branch cut, off the real line, beside a pole | 3s |
| `canoncheck` | is there a canonical form — idempotence, order independence, agreement between writings | 4s |
| `casbench` | does a corpus with known answers still solve — wrong / error / timeout, not just solved | 5s |
| `rootcheck` | is the root set **complete**, on polynomials built from known factors | 9s |
| `propcheck` | does each transformation satisfy a property it must satisfy, numerically | 10s |
| `egraph` | equality saturation against memory cost | 70s |
| `simpsweep` | does a simplification keep the value, at sampled real points | 72s |
| `rulecheck` | does a rule set do what it **declares** — termination, value preservation | 87s |
| `crashcheck` | does anything take the process down — one child process per case, 1890 cases | 245s |
| | **total** | **≈8.5 min** |

All ten exited 0. I had assumed this was a nightly-sized job and proposed it as one; it is a **test-job-sized** job. `crashcheck` alone is half of it, and it is half of it because it spawns 1890 child processes — that cost would grow on a shared runner and much more so on Windows.

Not included, and each for its own reason: `docsamples` needs the wiki and website checked out; `intbench` needs the Rubi suite, which is downloaded rather than vendored because it carries no licence statement; `libcompare` pulls `MathNet.Symbolics` and `Symbolism` from NuGet and was not timed. `sympyparity` is a special case — `SymPyParity.yml` already runs a scheduled in-repo watch, so that one is partly answered already.

### Why this is not just "add a workflow"

The harnesses live in a separate private workspace, not in this repository, so nothing here can run them today. That makes this a question for maintainers rather than a patch: **would you want them in-repo?** The code is mine to contribute if so.

There is already a shape to copy. `AotSmokeTest` and `DotnetBenchmark` are console projects under `Sources/Tests/` that are in the solution, are driven by a workflow, and are *not* picked up by `dotnet test`. A `Sources/Tests/Harnesses/` folder would sit alongside them. (One practical note: `dotnet sln add` rewrites the whole solution file — a single project added came out as several hundred changed lines, line endings and extra platform configurations included. The three entries are better inserted by hand.)

### The part that needs deciding, and it is not the runtime

These harnesses **generate reports**; they do not assert. Wiring them to CI means choosing what fails the build, and the naive choice is wrong: a count moving is usually not a regression. `boundcheck` went from 41 rewritten shapes to 35 over a fortnight with 0 disagreements throughout, which reads like `Simplify` losing capability and was nothing of the kind — a parser fix had stopped `1/3` arriving as a division, so the fold that used to happen no longer had anything to fold.

So the gate should be *the list, not the number* — and this repository already has that pattern twice:

* `Corpus/corpus-baseline.tsv` — a committed baseline, one line per problem, regenerated rather than hand-edited, diffed per commit.
* `PerformanceGate` — reads a committed baseline and fails on allocation moving more than 3%, while reporting time rather than failing on it, because a shared runner's wall clock belongs to whoever else is on the host.

The same for a harness: commit the list of shapes it flags, fail when the list changes, and let the counts move freely.

Two constraints that follow from the harnesses' own semantics:

* `casbench` and `crashcheck` report a **timeout as a verdict**, so they must not share a runner with competing load or CI turns into a finding. That is already why the workspace's own runner script runs them alone and first.
* Wall clock must never be the assertion, for the reason `PerformanceGate` already documents.

### Suggested first step

One workflow, the six harnesses under 10s (`confluence`, `boundcheck`, `canoncheck`, `casbench`, `rootcheck`, `propcheck` — 33s together), each gated on a committed list. That is small enough to run on every push rather than nightly, and it answers the caveat for the properties a corpus structurally cannot check: completeness of a root set, behaviour at a branch cut, idempotence of a normal form. The four slower ones can follow on a schedule once the baseline mechanism has proven itself.

Part of #746 — the "correctness coverage grows with the surface" standing condition.

Contributor guide

Open the contributing guide

Research direction

Start by reading the existing AotSmokeTest and DotnetBenchmark projects under Sources/Tests/, the workflow that drives them, and the PerformanceGate baseline pattern. The private harness workspace and the desired failure policy still require maintainer agreement; done would be an agreed in-repository approach for the proposed six fast harnesses and their committed flagged-item baselines.

Written by the indexing model from the issue text.

Assessment

Tech stack
csharp
Domain
ci-cd, testing
Issue type
Feature
Difficulty
5/5
Estimated time
Over a week
Activity status
Active
Clarity
Needs clarification
Newbie friendliness
28/100

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.