CI: run the Cranelift verifier. - #14207
Conversation
This PR adds a GitHub workflow that runs on pushes to main and on PRs. It restores the verifier's SMT query cache from the shared actions cache, runs 'verify.sh rebuild-cache' on top of it, and (on main) republishes the rebuilt cache as the isle-veri-cache.tar.gz asset on the rolling dev release plus a run artifact for use by local developers. It also adds a script, cranelift/isle/veri/setup/download-cache.sh, so a local user can download the current CI cache from the dev release and verify incrementally on top of it.
|
Let's see how long the run takes on the branch... |
|
Hmm, it seems that new workflows don't run until merge to main -- do I need to merge PRs as part of a debug loop?! That's awfully silly... (good security reasons for this I suppose but still) |
|
@cfallin it seems like you can manually trigger without merging to |
|
Unfortunately it seems there is no "Approve workflows to run" option, at least for me. I wonder if the set of workflows is somehow fixed based on what is in |
alexcrichton
left a comment
alexcrichton
left a comment
There was a problem hiding this comment.
If it works I'd recommend moving this to main.yml because otherwise we need to reconfigure repository settings to actually gate on this check where if it's in main.yml we can just manage it via the text configuration there.
github-actions
Bot
added
cranelift
Subscribe to Label ActionDetailsThis issue or pull request has been labeled: "cranelift", "isle"Thus the following users have been cc'd because of the following labels:
To subscribe or unsubscribe from this label, edit the |
1533989 to
9e2f162
Compare
- Move job into `main.yml` workflow. - Add branch spec to PR section.
9e2f162 to
7b3702c
Compare
|
Cool, the job finishes in 3h58m on a GitHub runner. That's definitely longer than I would have hoped for, but as long as the cache isn't dropped or mass-invalidated by some change it should be OK? (We should merge when the merge queue is otherwise quiet of course...) |
|
Woo! 🎉 A few things:
|
| - name: Install SMT solvers (cvc5, z3) | ||
| if: steps.smt-solvers.outputs.cache-hit != 'true' | ||
| run: | | ||
| solver_dir="$HOME/.cache/smt-solvers" | ||
| mkdir -p "${solver_dir}/bin" | ||
| ./cranelift/isle/veri/setup/install-cvc5.sh -i "${solver_dir}" | ||
| ./cranelift/isle/veri/setup/install-z3.sh -b "${solver_dir}/bin" |
There was a problem hiding this comment.
In CI this step took 3 seconds, so perhaps overkill to cache this step? Are you worried about flaky installation though?
There was a problem hiding this comment.
Oh, no, I was just worried it would take longer (and didn't have numbers until actually creating the PR). I can remove the caching step here.
| - name: Update dev release | ||
| if: github.ref_name == 'main' | ||
| env: | ||
| GH_TOKEN: ${{ github.token }} | ||
| run: | | ||
| if gh release view dev >/dev/null 2>&1; then | ||
| gh release upload dev isle-veri-cache.tar.gz --clobber | ||
| else | ||
| # Can happen on the very first run, before publish-artifacts | ||
| # has created the dev release yet. The tarball is still | ||
| # available as a run artifact, and the next run will pick up | ||
| # the rebuilt cache from the actions cache anyway. | ||
| echo "::warning::The dev release does not exist yet; skipping the release upload." | ||
| fi |
There was a problem hiding this comment.
This should happen through the publish-artifacts.yml workflow which is already responsible for uploading artifacts. For example all artifacts from the commit are downloaded here, shuffled around here, and uploaded here.
There's custom handling of the gh-pages artifact and you can shuffle aruond isle-veri-cache.tar.gz in that workflow.
| # Only runs landing on `main` write to the shared cache; PR and | ||
| # release-branch runs restore it read-only. | ||
| if: github.ref_name == 'main' |
There was a problem hiding this comment.
I think this should be removed and the cache should always be saved, and that way PRs can incrementally build up their own cache. PR caches aren't read by main and all workflow runs have a "branch base" where PRs are a different base than the main branch.
| - name: Restore verifier SMT query cache | ||
| uses: actions/cache/restore@v5 | ||
| with: | ||
| path: cranelift/isle/veri/cache | ||
| # Cache entries are immutable: each run saves under a unique key and | ||
| # restores the most recent entry by prefix. Bump `v1` if the cache | ||
| # format changes. | ||
| key: isle-veri-cache-v1-${{ github.run_id }} | ||
| restore-keys: | | ||
| isle-veri-cache-v1- |
There was a problem hiding this comment.
Could this use actions/cache to auto restore/save? I commented below but I don't believe there's any need to conditionally save.
Additionally, instead of using github.run_id could the key be a hash of input files? For example maybe the veri source code and aarch64 ISLE? That way when nothing is changing we're not making more caches.
Also, does the cvc5/z3 version need to be factored into this cache key?
|
Oh, also, as-is this is going to run on every PR which while probably fine we perhaps want to tweak a bit to only run conditionally like we do for most other jobs. If you copy this configuration it'll only run with
I'll caution that this'll probably need an iteration or two of landing on main to fiddle with the logic around caching and the |
3 participants
This PR adds a GitHub workflow that runs on pushes to main and on PRs. It restores the verifier's SMT query cache from the shared actions cache, runs 'verify.sh rebuild-cache' on top of it, and (on main) republishes the rebuilt cache as the isle-veri-cache.tar.gz asset on the rolling dev release plus a run artifact for use by local developers.
It also adds a script, cranelift/isle/veri/setup/download-cache.sh, so a local user can download the current CI cache from the dev release and verify incrementally on top of it.
Note that the cache needs a unique key per run on
main, because a cache entry is immutable oncecreated. Fortunately we can select the latest key by prefix.