set ts-2025 for master branch l4v and leave on ts-2024 for MCS until MCS
is updated to Isabelle2025 as well.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
We're currently using AWS Arm VMs, and vanilla Isabelle2024 ships a Z3
version that does not work on Arm. Using the ts-2024 branch fixes this
until we have upgraded everything to Isabelle2025.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Deploy the MCS verification manifest for versions that have no MCS
preprocess differences. These may be different from non-MCS preprocess
outcomes, and since the MCS verification is on a branch, we can deploy
it separately.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The new reusable workflow feature of GitHub allows us to avoid
repeating the workflow definitions and collect them in the ci-actions
repo instead.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The default python version changes on ubuntu-24, which breaks the
version of cmake-format we are currently using.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Before, some object API XML files conflicted when the include,
arch_include, and sel4_arch_include directories were combined:
- include/interfaces/sel4.xml
- arch_include/*/interfaces/sel4arch.xml
- sel4_arch_include/*/interfaces/sel4arch.xml
This commit renames them to:
- include/interfaces/object-api.xml
- arch_include/*/interfaces/object-api-arch.xml
- sel4_arch_include/*/interfaces/object-api-sel4-arch.xml
Now, when the include, arch_include, and sel4_arch_include directories
are combined, we are left with:
- interfaces/object-api.xml
- interfaces/object-api-arch.xml
- interfaces/object-api-sel4-arch.xml
Signed-off-by: Nick Spinale <nick@nickspinale.com>
Use the Isabelle version set in the verification manifest instead of
overriding to a specific version here. This will automatically update
as the verification repository updates to new Isabelle versions.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Proof artifact upload had name clashes for different artifacts from the
same job that previously would overwrite each other and with v4 actions
now error. This commit disambiguates the names.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Remove the space in the workflow name to ensure there are no side
effects when using it as an identifier.
Signed-off-by: Axel Heider <axelheider@gmx.de>
GitHub has updated the LTS node.js version from 16 to 20 and is
starting to show warnings for node16 actions.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The kernel.elf file is occasionally more useful for debugging than the
final board image.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
These proofs are currently still in progress (unfinished), but already
check large parts of the kernel and can break when the MCS preprocess
check fails.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
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>
