Skip to content

docs: correct TEST-NEEDS counts (e2e/property tests and benchmarks exist) #65

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
hyperpolymath merged 13 commits into from
Oct 10, 2026
Merged

docs: correct TEST-NEEDS counts (e2e/property tests and benchmarks exist) #65

Changes from all commits
Commits
Show all changes
13 commits
Select commit Hold shift + click to select a range
841076c
docs: record the #43 check-triage ultraplan and its execution record
hyperpolymath Oct 10, 2026
cda05cb
fix(ci): install Z3 on the ubuntu CI legs so solver-backed tests run …
hyperpolymath Oct 10, 2026
ce3f3db
fix(ci): explain the boj-build soft gate and fix the trigger payload …
hyperpolymath Oct 10, 2026
8fbc840
fix(docs): retire the stale docs/make.jl (#60)
hyperpolymath Oct 10, 2026
a905071
docs: fill PROJECT_UNIQUE_STRENGTH and retire REQUIRES_INITIALISATION…
hyperpolymath Oct 10, 2026
fb1d6d1
chore(ci): adopt actions.lock (#58)
hyperpolymath Oct 10, 2026
5c0c375
Update .machine_readable/bot_directives/methodology.a2ml
hyperpolymath Oct 10, 2026
bd59686
fix: address CodeRabbit review — jq-encode the boj payload, correct c…
hyperpolymath Oct 10, 2026
deb8d7b
Merge remote-tracking branch 'origin/arena/cbd1e29d-smtlib-jl' into a…
hyperpolymath Oct 10, 2026
6325d53
docs: restore the standards#994 cross-reference in the ultraplan
hyperpolymath Oct 10, 2026
f600b15
Merge remote-tracking branch 'origin/main' into arena/cbd1e29d-smtlib-jl
hyperpolymath Oct 10, 2026
3dcc1cf
docs: correct TEST-NEEDS counts — e2e/property tests and benchmarks e…
hyperpolymath Oct 10, 2026
274d235
Merge branch 'main' into arena/cbd1e29d-smtlib-jl
hyperpolymath Oct 10, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 5 additions & 5 deletions TEST-NEEDS.adoc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,21 +8,21 @@
|===
|Category |Count |Details
|*Source modules* |12 |3,586 lines
|*Test files* |1 |1,578 lines, 650 @test/@testset
|*Benchmarks* |0 |None
|*E2E tests* |0 |None
|*Test files* |3 |`test/runtests.jl` (650+ @test/@testset), `test/e2e_test.jl`, `test/property_test.jl`
|*Benchmarks* |1 |`benches/benchmarks.jl` (BenchmarkTools `SUITE`)
|*E2E tests* |1 |`test/e2e_test.jl` (declare → assert → check_sat; script building)
|===

=== What’s Missing

==== E2E Tests

* [ ] No test running SMTLib against actual SMT solvers (Z3, CVC5)
* [x] Solver-backed tests (Z3) exist and run when `z3` is on `PATH` — and since #62 the ubuntu CI legs install Z3, so they execute in CI instead of skipping.
* [ ] No roundtrip test (generate SMTLib2 -> parse back)

==== Aspect Tests

* [ ] *Performance*: SMT solving is performance-critical, 0 benchmarks
* [x] *Performance*: `benches/benchmarks.jl` provides a BenchmarkTools `SUITE` (generation/latency).
* [ ] *Error handling*: No tests for unsatisfiable formulas, timeout,
solver crashes
* [ ] *Concurrency*: No parallel solving tests
Expand Down
Loading