For proof workflow runs on seL4 PRs, upload kernel build artifacts
generated by the aws-proofs action. These can be used to run binary
verification, although we currently still require binary verification to
be manually triggered.
Signed-off-by: Matthew Brecknell <matt@kry10.com>
Like the sel4test hardware runs, a sel4bench run can be requested via
adding a label (`hw-bench`) to any PR.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
There is now an `AARCH64_verified` configuration which is used in
ongoing verification of the seL4 AArch64 port. This commit enables
the preprocess check for this config so that verification impact
becomes visible on pull requests.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Merge to master is infrequent enough that we can let the hardware test
suite run to completion even if one of the tests failed. This will
provide more information in the history on which boards worked for
which commits, even if the test for one is broken for some time.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
${{github.ref}} is not what it seems for pull request target. It will
point to the base branch instead of refs/pulls/<num> like the docs
would suggest. Using the PR number directly should work.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
By default GitHub spawns a new test for each push to a PR. Since the
proof tests have limited resources, we want only the most recent push
to be triggered, intermediate pushes will be skipped.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The matrix for hardware runs is now generated centrally from the
ci-actions repo to avoid inconsistencies when the workflow is replicated
in other repos.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Some of the Github actions in this repository require secrets for
access to hardware test or other compute infrastructure, or for
deployment. When these are run in a fork on GitHub they are safe,
but generate annoying error messages.
This commit adds tests in the relevant actions whether they are run
from the seL4 org or not, and skips the action when they are run
outside. This should make the remaining actions more useful on forks.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Since the build system defaults to python3 now, these have not worked
as advertised in a while now (they have test py3 twice).
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The trigger action sends repository_dispatch events to all
main test repositories of the manifests this repo is part of.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Previous "Kernel" showed up for the badge and main checks group, which
is not very informative.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Previously the `concurrency` statement also prevented concurrency
within the build matrix which we do not want.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit pulls out a separate workflow for sel4test (simulation +
hardware runs) on pushes to master, and deploys a new default.xml to
sel4test-manifest when the test is successful.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This switched the action from pull_request to pull_request_target,
because we need access to secrets. GITHUB_TOKEN permissions are
downgraded to PR-like permissions, and the action needs to be triggered
manually by labelling with label 'hw-test'.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The reason is that with separate workflow files allow different
triggers. In particular, we don't want to re-run all simulations
on all `labeled` triggers, but if we explicitly skip the simulation
job for those triggers, than previous simulation runs are not
shown any more in the GitHub check status, so failed runs will be
overlooked.
This should achieve both: no unnecessary runs, and visible status.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The previous trigger would start duplicate builds for each new
label added to a PR. This commit locks this down a bit more so
that builds only run when the trigger label is added or on other
triggers when the label is present.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The action is triggered on push to master or when the label "hw-build"
is present on pull requests.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The SimplExportAndRefine session is one of the steps of binary
verification and only available for ARM and RISCV64.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This action will run the C proofs when the label `proof-test` is added
to a pull request. Intended to be used when the preprocess test has
failed and the PR is ready to check proofs.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This action runs the verification C parser on the main kernel
configurations to check that the code is in the C verification subset.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This will build a PDF of the reference manual in draft mode
and upload that PDF as a build artifact.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit refactors the github workflows into two
file (push/pull request), makes use of the new central
seL4 github actions, and adds the preprocess test for
pull requests.
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
This should not change behaviour, but makes sure we replicate the test
setup more precisely.
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
