ci: Add Aiur compile + typecheck benchmark workflow#449
Merged
Conversation
samuelburnham
changed the title
samuelburnham
force-pushed
the
sb/aiur-ci-bench
branch
4 times, most recently
from
6315cba to
cc23c22
Compare
Merge the Ix-compiler benchmark and a new Aiur execute/prove benchmark into one workflow (aiur-bench.yml): per library env, 'ix compile' produces a per-bench .ixe (compile-throughput metrics; cached to actions/cache), then bench-typecheck STARK-checks selected constants over that same .ixe (execute, prove, and peak-RSS metrics). The env loads lazily via Ixon.deEnvAnon so Mathlib statements check at ~10GB peak RSS instead of the ~100GB eager load. Shared bencher + toolchain-bump-reset logic lives in the .github/actions/bencher-track composite action (pinned to bencher v0.6.7, authenticating with a project-scoped BENCHER_API_KEY); constants are inline in the workflow matrix. Replaces compile.yml. Also share CLI name resolution: extract parseName/resolveName/ixNameToLeanName/ resolveIxeAddr from Ix.Cli.CheckCmd into a lightweight Ix.Cli.NameResolve module (depends only on Address/Environment/Ixon). 'ix addr-of --ixe' gains the toString fallback 'ix check' uses, and bench-typecheck resolves names through the same module instead of duplicating the helpers.
Revert before merging. Scopes the push trigger to this branch so the benchmark workflow can be exercised end-to-end; Bencher data lands under the `sb/aiur-ci-bench` branch, isolated from `main`'s plots.
samuelburnham
force-pushed
the
sb/aiur-ci-bench
branch
from
cc23c22 to
5ac9ab1
Compare
arthurpaulino
approved these changes
Jun 19, 2026
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
2 participants
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.
Two main changes:
CheckNatAddComm.leanbenchmark to a genericTypecheck.leanbenchmark, with optional JSON output for CI integration.ix compilebenchmark onmainto also benchmark Aiur execution + proving on the following InitStd and Mathlib constants:Because of Aiur's memory restraints these are all light enough to run easily on the 128GB runner, whereas
Vector.extract_appendhit OOM on execution. These constants should thus be changed to cover more unique workloads as Aiur RAM usage improves.The prove benchmarks have the following measurements, each with their own thresholds which will fail CI/create an alert when a percentage-based regression from the last 64 runs is detected:
Note
The
ubuntu-latestrunner builds thebench-typecheckbinary but it does not have support AVX-512. This means the proving benchmarks will be significantly slower (10-30%), and are mainly meant to test for performance regression than absolute numbers. Later we can upgrade to a more powerful runner.Successful run:
https://github.com/argumentcomputer/ix/actions/runs/27778973973
After argumentcomputer/tracing-texray#2