Compare commits

...

3 Commits

Author SHA1 Message Date
Axel Heider
bf02b59c46 CI: debug
Signed-off-by: Axel Heider <axelheider@gmx.de>
2024-04-12 20:08:41 +02:00
Axel Heider
0fe0bfb55c CI: reduce load
Signed-off-by: Axel Heider <axelheider@gmx.de>
2024-04-12 20:08:41 +02:00
Axel Heider
799c8b130f CI: use ci-actions patch-axel-17
Signed-off-by: Axel Heider <axelheider@gmx.de>
2024-04-12 20:08:41 +02:00
9 changed files with 19 additions and 316 deletions

View File

@@ -1,37 +0,0 @@
# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
#
# SPDX-License-Identifier: BSD-2-Clause
# Compilation actions to run on pull requests
name: Compile
on:
push:
branches:
- master
pull_request:
# To reduce the load we cancel any older runs of this workflow for the current
# PR. For deployment to the master branch, the workflow will run on each push,
# and the `run_id` parameter will prevent cancellation.
concurrency:
group: ${{ github.workflow }}-${{ github.event_name == 'pull_request' && format('pr-{0}', github.event.number) || format('run-{0}', github.run_id) }}
cancel-in-progress: ${{ github.event_name == 'pull_request' }}
jobs:
standalone_kernel:
name: kernel
runs-on: ubuntu-latest
strategy:
fail-fast: false
matrix:
# RISCV32 and IA32 are left out, as they have no verified config
arch: [ARM, ARM_HYP, AARCH64, RISCV64, X64]
compiler: [gcc, llvm]
steps:
- uses: actions/checkout@v4
- uses: seL4/ci-actions/standalone-kernel@master
with:
ARCH: ${{ matrix.arch }}
COMPILER: ${{ matrix.compiler }}

View File

@@ -1,21 +0,0 @@
# Copyright 2021, Proofcraft Pty Ltd
#
# SPDX-License-Identifier: BSD-2-Clause
# Run the verification C parser on the main kernel configurations
#
# See cparser-run/builds.yml in the repo seL4/ci-actions for configs.
name: C Parser
on:
push:
branches: [master]
pull_request:
jobs:
cparser:
name: C Parser
runs-on: ubuntu-latest
steps:
- uses: seL4/ci-actions/cparser-run@master

View File

@@ -1,23 +0,0 @@
# Copyright 2021, Proofcraft Pty Ltd
#
# SPDX-License-Identifier: BSD-2-Clause
# Build a PDF of the seL4 reference manual
name: RefMan
on:
push:
branches:
- master
pull_request:
jobs:
manual:
name: Build PDF
runs-on: ubuntu-latest
steps:
- uses: seL4/ci-actions/seL4-manual@master
- uses: actions/upload-artifact@v4
with:
name: PDF
path: manual/manual.pdf

View File

@@ -1,55 +0,0 @@
# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
#
# SPDX-License-Identifier: BSD-2-Clause
# Actions to run on pull requests
name: PR
on: [pull_request]
jobs:
gitlint:
name: Gitlint
runs-on: ubuntu-latest
steps:
- uses: seL4/ci-actions/gitlint@master
whitespace:
name: 'Trailing Whitespace'
runs-on: ubuntu-latest
steps:
- uses: seL4/ci-actions/git-diff-check@master
shell:
name: 'Portable Shell'
runs-on: ubuntu-latest
steps:
- uses: seL4/ci-actions/bashisms@master
style:
name: Style
runs-on: ubuntu-latest
steps:
- uses: seL4/ci-actions/style@master
preprocess:
name: Preprocess
runs-on: ubuntu-latest
strategy:
fail-fast: false
matrix:
arch: [ARM, ARM_HYP, AARCH64, RISCV64, X64]
feature: ["", MCS]
exclude:
- arch: ARM_HYP
feature: MCS
- arch: AARCH64
feature: MCS
- arch: X64
feature: MCS
steps:
- uses: seL4/ci-actions/preprocess@master
with:
L4V_ARCH: ${{ matrix.arch }}
L4V_FEATURES: ${{ matrix.feature }}

View File

@@ -1,64 +0,0 @@
# Copyright 2021 Proofcraft Pty Ltd
#
# SPDX-License-Identifier: BSD-2-Clause
name: Proofs
on:
pull_request_target:
types: [labeled, synchronize]
jobs:
cproof:
name: C Proofs
runs-on: ubuntu-latest
# run on any normal trigger when the label exists, and run when the label is added
# don't run again when other labels are added
if: ${{ github.repository_owner == 'seL4' &&
(github.event.action != 'labeled' &&
contains(github.event.pull_request.labels.*.name, 'proof-test') ||
github.event.action == 'labeled' && github.event.label.name == 'proof-test') }}
strategy:
fail-fast: false
matrix:
include:
- arch: ARM
session: CRefine SimplExportAndRefine
- arch: ARM_HYP
session: CRefine
- arch: RISCV64
session: CRefine SimplExportAndRefine
- arch: X64
session: CRefine
- arch: AARCH64
session: CRefine
- arch: RISCV64
features: MCS
session: CRefine
# test only most recent push to PR:
concurrency: seL4-PR-C-proofs-pr-${{ github.event.number }}-idx-${{ strategy.job-index }}
steps:
- name: Proofs
uses: seL4/ci-actions/aws-proofs@master
with:
L4V_ARCH: ${{ matrix.arch }}
L4V_FEATURES: ${{ matrix.features }}
isa_branch: ts-2023
session: ${{ matrix.session }}
manifest: ${{ matrix.features == 'MCS' && 'mcs.xml' || 'default.xml' }}
env:
AWS_ACCESS_KEY_ID: ${{ secrets.AWS_ACCESS_KEY_ID }}
AWS_SECRET_ACCESS_KEY: ${{ secrets.AWS_SECRET_ACCESS_KEY }}
AWS_SSH: ${{ secrets.AWS_SSH }}
GH_HEAD_SHA: ${{ github.event.pull_request.head.sha }}
- name: Upload kernel builds
uses: actions/upload-artifact@v4
with:
name: kernel-builds-${{ matrix.arch }}-${{ matrix.features }}
path: artifacts/kernel-builds
if-no-files-found: ignore
- name: Upload logs
uses: actions/upload-artifact@v4
with:
name: logs-${{ matrix.arch }}-${{ matrix.features }}
path: logs.tar.xz

View File

@@ -1,25 +0,0 @@
# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
#
# SPDX-License-Identifier: BSD-2-Clause
# Actions to run on Push and Pull Request
name: CI
on:
push:
branches:
- master
pull_request:
jobs:
check:
name: License Check
runs-on: ubuntu-latest
steps:
- uses: seL4/ci-actions/license-check@master
links:
name: Links
runs-on: ubuntu-latest
steps:
- uses: seL4/ci-actions/link-check@master

View File

@@ -31,9 +31,25 @@ concurrency:
cancel-in-progress: true
jobs:
the_matrix:
name: Matrix
runs-on: ubuntu-latest
outputs:
matrix: ${{ steps.matrix.outputs.matrix }}
steps:
- id: matrix
uses: axel-h/ci-actions/sel4test-hw-matrix@patch-axel-17
- env:
json_steps_matrix: ${{ toJSON(steps.matrix) }}
json_steps_matrix_outputs_matrix: ${{ toJSON(steps.matrix.outputs.matrix) }}
run: |
echo steps.matrix = ${json_steps_matrix}
echo steps.matrix.outputs.matrix = ${json_steps_matrix_outputs_matrix}
hw-build:
name: HW Build
runs-on: ubuntu-latest
needs: the_matrix
if: ${{ github.event_name == 'push' ||
github.event_name == 'pull_request_target' &&
github.event.action != 'labeled' &&
@@ -51,7 +67,7 @@ jobs:
compiler: [gcc, clang]
steps:
- name: Build
uses: seL4/ci-actions/sel4test-hw@master
uses: axel-h/ci-actions/sel4test-hw@patch-axel-17
with:
march: ${{ matrix.march }}
compiler: ${{ matrix.compiler }}
@@ -67,20 +83,10 @@ jobs:
name: kernel.elf-${{ matrix.march }}-${{ matrix.compiler }}
path: '*-kernel.elf'
the_matrix:
name: Matrix
needs: hw-build
runs-on: ubuntu-latest
outputs:
matrix: ${{ steps.matrix.outputs.matrix }}
steps:
- id: matrix
uses: seL4/ci-actions/sel4test-hw-matrix@master
hw-run:
name: HW Run
runs-on: ubuntu-latest
needs: the_matrix
needs: [the_matrix, hw-build]
if: ${{ github.repository_owner == 'seL4' &&
(github.event_name == 'push' ||
github.event_name == 'pull_request_target' &&
@@ -103,7 +109,7 @@ jobs:
with:
name: images-${{ matrix.march }}-${{ matrix.compiler }}
- name: Run
uses: seL4/ci-actions/sel4test-hw-run@master
uses: axel-h/ci-actions/sel4test-hw-run@patch-axel-17
with:
platform: ${{ matrix.platform }}
compiler: ${{ matrix.compiler }}

View File

@@ -1,39 +0,0 @@
# Copyright 2021, Proofcraft Pty Ltd
#
# SPDX-License-Identifier: BSD-2-Clause
# sel4test simulation runs
#
# See sel4test-sim/builds.yml in the repo seL4/ci-actions for configs.
name: seL4Test-Sim
on:
pull_request:
paths-ignore:
- 'manual/**'
- 'LICENSES/**'
- '*.md'
# To reduce the load we cancel any older runs of this workflow for the current
# PR. Such runs exist, if there were new pushes to the PR's branch without
# waiting for the workflow to finish. As a side effect, pushing new commits now
# becomes a convenient way to cancel all the older runs, e.g. if they are stuck
# and would only be stopped by the timeout eventually.
concurrency:
group: ${{ github.workflow }}-pr-${{ github.event.number }}
cancel-in-progress: true
jobs:
sim:
name: Simulation
runs-on: ubuntu-latest
strategy:
matrix:
march: [armv7a, armv8a, nehalem, rv32imac, rv64imac]
compiler: [gcc, clang]
steps:
- uses: seL4/ci-actions/sel4test-sim@master
with:
march: ${{ matrix.march }}
compiler: ${{ matrix.compiler }}

View File

@@ -1,39 +0,0 @@
# Copyright 2021, Proofcraft Pty Ltd
#
# SPDX-License-Identifier: BSD-2-Clause
# xmllint for seL4 IDL files
name: XML
on:
push:
branches:
- master
paths:
- 'libsel4/**/sel4*.xml'
- 'libsel4/**/sel4*.xsd'
- 'libsel4/include/api/syscall.xml'
- 'libsel4/include/api/syscall.xsd'
pull_request:
paths:
- 'libsel4/**/sel4*.xml'
- 'libsel4/**/sel4*.xsd'
- 'libsel4/include/api/syscall.xml'
- 'libsel4/include/api/syscall.xsd'
jobs:
xmllint:
name: XML Lint
runs-on: ubuntu-latest
steps:
- name: apt-get update
run: sudo apt-get update
- name: install xmllint
run: sudo apt-get install libxml2-utils
- uses: actions/checkout@v4
- name: run xmllint
run: |
find libsel4 -name "sel4*.xml" | \
xargs xmllint --schema libsel4/tools/sel4_idl.xsd --noout
xmllint --schema libsel4/include/api/syscall.xsd --noout libsel4/include/api/syscall.xml