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>
CI: PR check to do a stand-alone kernel compile
On a PR, compile all verified configs of seL4.
Signed-off-by: Luke Mondy <luke.mondy@data61.csiro.au>
Co-authored-by: Luke Mondy <luke.mondy@data61.csiro.au>
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>
