axonos-kernel v0.1.7 #19
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # AxonOS Kernels — Continuous Integration | |
| # | |
| # Every job has an explicit timeout so a hanging tool cannot block the | |
| # entire pipeline. Kani jobs run with `continue-on-error: true` so that a | |
| # slow or hung BMC proof does not turn the whole CI red — they report | |
| # their status independently and are inspected manually after every push. | |
| name: ci | |
| on: | |
| push: | |
| branches: [main] | |
| pull_request: | |
| workflow_dispatch: | |
| env: | |
| CARGO_TERM_COLOR: always | |
| RUST_BACKTRACE: 1 | |
| # Cancel in-flight runs on the same branch when a new push arrives. | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.ref }} | |
| cancel-in-progress: true | |
| jobs: | |
| # ── 1. Tests across three host operating systems ───────────────────────── | |
| test: | |
| name: test (${{ matrix.os }}) | |
| runs-on: ${{ matrix.os }} | |
| timeout-minutes: 15 | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| os: [ubuntu-latest, macos-latest, windows-latest] | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - uses: dtolnay/rust-toolchain@stable | |
| - uses: Swatinem/rust-cache@v2 | |
| - name: cargo test --workspace | |
| run: cargo test --workspace --all-features | |
| # ── 2. Format check ─────────────────────────────────────────────────────── | |
| fmt: | |
| name: rustfmt --check | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 5 | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - uses: dtolnay/rust-toolchain@stable | |
| with: | |
| components: rustfmt | |
| - run: cargo fmt --all -- --check | |
| # ── 3. Clippy ───────────────────────────────────────────────────────────── | |
| clippy: | |
| name: clippy -D warnings | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 15 | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - uses: dtolnay/rust-toolchain@stable | |
| with: | |
| components: clippy | |
| - uses: Swatinem/rust-cache@v2 | |
| - run: cargo clippy --workspace --all-targets --all-features -- -D warnings | |
| # ── 4. MSRV pin ─────────────────────────────────────────────────────────── | |
| msrv: | |
| name: MSRV (1.75) | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 15 | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - uses: dtolnay/rust-toolchain@1.75 | |
| - uses: Swatinem/rust-cache@v2 | |
| - run: cargo check --workspace --all-features | |
| # ── 5. no_std builds on embedded targets ───────────────────────────────── | |
| no-std: | |
| name: no_std (${{ matrix.target }}) | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 15 | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| target: | |
| - thumbv7em-none-eabihf | |
| - thumbv8m.main-none-eabihf | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - uses: dtolnay/rust-toolchain@stable | |
| with: | |
| targets: ${{ matrix.target }} | |
| - uses: Swatinem/rust-cache@v2 | |
| - name: cargo build --target ${{ matrix.target }} | |
| # Exclude firmware (it builds separately in its own job). | |
| run: | | |
| cargo build --release --target ${{ matrix.target }} \ | |
| -p axonos-spsc \ | |
| -p axonos-scheduler \ | |
| -p axonos-capability \ | |
| -p axonos-time \ | |
| -p axonos-intent \ | |
| -p axonos-kernel-core | |
| # ── 6. Documentation build ─────────────────────────────────────────────── | |
| docs: | |
| name: docs -D rustdoc warnings | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 10 | |
| env: | |
| RUSTDOCFLAGS: "-D warnings" | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - uses: dtolnay/rust-toolchain@stable | |
| - uses: Swatinem/rust-cache@v2 | |
| - run: cargo doc --workspace --no-deps --all-features | |
| # ── 7. Miri (undefined behaviour detection on the unsafe surface) ──────── | |
| miri: | |
| name: miri (axonos-spsc) | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 20 | |
| continue-on-error: true | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - uses: dtolnay/rust-toolchain@nightly | |
| with: | |
| components: miri | |
| - uses: Swatinem/rust-cache@v2 | |
| - name: miri test axonos-spsc | |
| run: cargo miri test -p axonos-spsc | |
| # ── 8. Kani bounded model checking ─────────────────────────────────────── | |
| # Each crate runs as an independent matrix job with its own timeout. | |
| # `continue-on-error: true` means a hung or failing Kani proof does NOT | |
| # fail the entire pipeline — the result is reported independently. | |
| # Inspect each kani job's log after a push to see what proved and what | |
| # timed out. | |
| # | |
| # To run locally: | |
| # cargo install --locked kani-verifier | |
| # cargo kani setup | |
| # cd axonos-X/kani-proofs && cargo kani --default-unwind 16 | |
| kani: | |
| name: kani (${{ matrix.crate }}) | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 35 | |
| continue-on-error: true | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| crate: | |
| - axonos-spsc | |
| - axonos-scheduler | |
| - axonos-capability | |
| - axonos-time | |
| - axonos-intent | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - uses: model-checking/kani-github-action@v1 | |
| with: | |
| working-directory: ${{ matrix.crate }}/kani-proofs | |
| args: "--default-unwind 16" | |
| # ── 9. Bare-metal firmware build (Cortex-M4F) ──────────────────────────── | |
| # The firmware crate is excluded from the parent workspace and built | |
| # independently with its target-specific .cargo/config.toml. | |
| firmware: | |
| name: firmware (STM32F407) | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 15 | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - uses: dtolnay/rust-toolchain@stable | |
| with: | |
| targets: thumbv7em-none-eabihf | |
| - uses: Swatinem/rust-cache@v2 | |
| - name: Build firmware | |
| working-directory: axonos-firmware-stm32f407 | |
| # Explicit --target: relying on .cargo/config.toml has proven | |
| # fragile in some CI environments. Passing the target on the | |
| # command line is the canonical way. | |
| run: cargo build --release --target thumbv7em-none-eabihf | |
| # ── 10. cargo-deny (licence + advisory + bans audit) ───────────────────── | |
| # Pinned to v1: v2 has compatibility issues with cargo-deny 0.15+ where it | |
| # tries to invoke non-existent top-level subcommands. continue-on-error is | |
| # set because licence/advisory checks are informational at pre-1.0 stage. | |
| deny: | |
| name: cargo-deny | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 10 | |
| continue-on-error: true | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - uses: EmbarkStudios/cargo-deny-action@v1 | |
| with: | |
| command: check bans licenses sources |