If we don't provide the additional name fragment, previous artifacts
would be overwritten, which leads to a failure with error message on
GitHub.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This will now test with the following num_domains settings:
- PRs: default as in config file, no matrix
- push to master: with NUM_DOMAINS = 1 and default (= '')
- weekly test: with NUM_DOMAINS = 1, 7, and default
The default in the current config files is 16. 1 leads to structural
code changes is the setting most likely to break. 7 is for checking
that the proofs also work with a value that is not a power of 2.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The implicit GITHUB_TOKEN does not trigger further push actions in
the same repo, but in this case we do want the push action to happen
on the `-rebased` branches, so we use an explicit auth token instead.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The action will abort when no clean rebase is possible, and force-push
the rebased branch when the rebase over origin/master was clean.
The push will trigger proof runs on the rebased branches.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The worklow_dispatch trigger adds a button in the GitHub UI that lets
one trigger the workflow manually. Useful for testing the workflows.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
A previous commit added a new job which depended on a job that didn't
exist. We rename the `all` job to `proofs` for consistency with other
workflows.
Signed-off-by: Matthew Brecknell <matt@kry10.com>
The decompilation process (part of binary verification) is more tightly
coupled to the graph-refine repository than l4v, so it makes more sense
to perform decompilation in graph-refine. (It was temporarily performed
here in l4v because the graph-refine branches needed some stabilisation
work.)
This also modifies proof workflows:
- All proof workflows now upload kernel build artifacts. These can be
used as inputs to binary verification.
- Proof workflows other than the one for pull requests (proof.yml)
automatically trigger a decompilation workflow. We can still manually
initiate a decompilation workflow using the uploaded artifacts, but
doint so automatically would consume too many parallel runners.
Signed-off-by: Matthew Brecknell <matt@kry10.com>
Need to check out the ci-actions repo first (where the nl-unescape.sh
script is located).
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This removes the mcs-export matrix job from the proof-deploy workflow,
as the first step towards solving seL4/l4v#497. This should unblock
verification manifest deployments.
The mcs-export job was added to the proof-deploy workflow to perform
SimplExportAndRefine for binary verification targets. It took a short
cut, using the master branch of l4v to perform SimplExportAndRefine for
MCS configurations, since there were no differences between rt and
master that were relevant to SimplExportAndRefine. This is no longer the
case, because MCS seL4 C code now contains C parser annotations that use
symbols only available in the rt branch of l4v.
We intend to add an equivalent job that uses the rt branch of l4v for
MCS SimplExportAndRefine, but are still working out the best way to do
that.
Signed-off-by: Matthew Brecknell <matt@kry10.com>
The repo token allows the action to work on a private repo, and
the S3 cache bucket name allows it to charge a different org.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit will only come into full effect when it is merged into
master, which is also the time AARCH64 tests should run regularly
in the main repository.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This is a separate workflow instead of being added to `proof.yml` so
that it can be switched on/off separately.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The previous version of the `binary` workflow assumed that its input
artifacts would be available for download before a `binary` workflow run
is started. However, the `binary` workflow typically wants to download
those artifacts from the same workflow run that triggered the `binary`
run via `repository_dispatch`.
It appears that GitHub Actions does not make artifacts available for
download from a workflow until *after* the relevant job has finished.
Hence, there's a race between the `binary` workflow and the workflow
that triggered it. We resolve this by making the `binary` workflow retry
its artifact download for up to 10 minutes.
Signed-off-by: Matthew Brecknell <matt@kry10.com>
The previous version was erroneously downloading artifacts from the repo
in which the `binary` workflow was triggered, when it should have been
downloading from the repo identified by the payload of the trigger.
Signed-off-by: Matthew Brecknell <matt@kry10.com>
ci-actions/aws-proofs no longer excludes the AutoCorresSEL4 session by
default, so we no longer need to provide a fake argument to the session
parameter to not exclude it.
This is significant, because we now want the default to be non-verbose
since we're running multiple sessions in parallel.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- Add a new workflow to prepare graph-refine inputs and submit them to a
back end over SSH. Intended to be triggered by the proof-deploy
workflow. Fetches C graph-lang artifacts from the triggering workflow,
and runs the decompiler to generate ASM graph-lang.
- Add a job to the l4v-proof workflow to trigger the decompilation
workflow.
Signed-off-by: Matthew Brecknell <matt@kry10.com>
Add a second matrix job that runs SimplExportAndRefine for MCS C kernel
configurations that support it (currently ARM and RISCV64).
Note that this uses the master branch of l4v to generate the CSpec, and
to run SimplExportAndRefine, not the rt branch. This works because the
rt branch does not yet connect to the CSpec, and there are no meaningful
differences between rt and master in CSpec or SimplExportAndRefine. For
now, this simplifies workflows for binary verification. But when MCS
proofs connect to the CSpec, this will need to be refactored to use the
rt branch.
Signed-off-by: Matthew Brecknell <matt@kry10.com>
Upload an artifact for any C graph-lang generated by
SimplExportAndRefine during a proof-deploy workflow.
Signed-off-by: Matthew Brecknell <matt@kry10.com>
${{github.ref}} will resolve to the base branch of the PR, not the
PR branch, so it is not useful for distinguishing PRs. The pull request
number will do the job.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
By default GitHub spawns a new test for each push event. To avoid
hitting the maximum number of AWS instances too quickly, we run the PR
and master proof tests only on the most recent push since the last test
finished.
The concurrency exclusion is per git ref, i.e. separate PRs and
separate branches still run tests concurrently.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The default test setup now uses the correct branch from devel.xml
in the verification-manifest repo.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The repository_dispatch event will be generated in the
verification-manifest repo when devel.xml is updated by anyone other
than the seL4-ci user.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This refactors the proof runs into a separate run for the master branch
(which has deployment) and development branches (currently RT and PRs).
For the test on the master branch, we need to make sure that all tests
and the deployment action see the same revisions of all participating
repos.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
External means default.xml and vanilla Isabelle instead of internal TS
Isabelle and devel.xml.
The weekly clean test runs without reading the proof image cache,
writing back a fresh cache state.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This makes the full low-level logs available in the "Artifacts" tab of
the "Actions" screen.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This completes the previous commit to run all proof tests on reasonably
high-powered AWS VMs instead of GitHub runners. All tests run in one
go for efficiency.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This action triggers docker container deployment in the repo
seL4/ci-actions when the C parser changes here.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The annotation action only works for in-repo pull requests. This flag
ignores any errors from this action so that forked pull requests don't
get spurious test failures.
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
This github action checks PRs for unwanted outer syntax commands like
`sorry`, `sledgehammer`, or `thm`. The check is non-required, so can be
ignored for those cases where the command is wanted after all.
In addition to console output, the action annotates the sources in the
"changed files" tab. This only works for PRs from within the same repo,
unfortunately (forks have insufficient rights for annotations)
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
With Isabelle2020 the Refine sessions are too close to memory
boundaries on github runners, the tests randomly fail with out-of-store
exceptions in polyml (but also randomly succeed without change).
Removing the session here until we have a better solution.
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
This commit ignores the Isabelle version set in the repo manifest and fixes
Isabelle2020 instead for github CI checks. The main purpose is to test this
function and to make sure the test can remain working while the repo manifest
is being updated.
After that has happened, this commit can be reverted.
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
Gerwin Klein
Matthew Brecknell
Peter Chubb
Gerwin Klein
Gerwin Klein
Robert Sison