diff --git a/.github/workflows/proof-deploy.yml b/.github/workflows/proof-deploy.yml index bf2006f651c..0e7e86dba8a 100644 --- a/.github/workflows/proof-deploy.yml +++ b/.github/workflows/proof-deploy.yml @@ -1,18 +1,15 @@ -# Copyright 2021 Proofcraft Pty Ltd +# Copyright 2023 Proofcraft Pty Ltd # # SPDX-License-Identifier: BSD-2-Clause -# On push to master only: run proofs and deploy manifest update. +# Run proofs and rebase plaform branch. -name: Proofs +name: Platform Proofs Exynos 5 on: push: branches: - - master - repository_dispatch: - types: - - manifest-update + - exynos5-ver-rebased # for testing: workflow_dispatch: @@ -36,14 +33,16 @@ jobs: strategy: fail-fast: false matrix: - arch: [ARM, ARM_HYP, AARCH64, RISCV64, X64] + arch: [ARM_HYP] + plat: [exynos5] # test only most recent push: - concurrency: l4v-regression-${{ github.ref }}-${{ strategy.job-index }} + concurrency: l4v-${{ github.ref }}-${{ strategy.job-index }} steps: - name: Proofs uses: seL4/ci-actions/aws-proofs@master with: L4V_ARCH: ${{ matrix.arch }} + L4V_PLAT: ${{ matrix.plat }} xml: ${{ needs.code.outputs.xml }} env: AWS_ACCESS_KEY_ID: ${{ secrets.AWS_ACCESS_KEY_ID }} @@ -61,47 +60,19 @@ jobs: name: logs-${{ matrix.arch }} path: logs.tar.xz - deploy: - name: Deploy manifest - runs-on: ubuntu-latest - needs: [code, proofs] - steps: - - uses: seL4/ci-actions/l4v-deploy@master - with: - xml: ${{ needs.code.outputs.xml }} - env: - GH_SSH: ${{ secrets.CI_SSH }} - - name: Trigger binary verification - uses: seL4/ci-actions/bv-trigger@master - with: - token: ${{ secrets.PRIV_REPO_TOKEN }} - tag: "l4v/proof-deploy/${{ github.event_name }}" - - rebase: - name: Rebase platform branches + push: + name: Push rebased branch runs-on: ubuntu-latest - strategy: - fail-fast: false - matrix: - branch: [imx8-fpu-ver, exynos5-ver] + needs: [proofs] steps: - name: Checkout uses: actions/checkout@v3 with: - ref: ${{ matrix.branch }} - path: l4v-${{ matrix.branch }} + ref: exynos5-ver-rebased fetch-depth: 0 - # needed to trigger push actions on the -rebased branch - # (implict GITHUB_TOKEN does not trigger further push actions). - token: ${{ secrets.PRIV_REPO_TOKEN }} - - name: Rebase + - name: Push run: | - cd l4v-${{ matrix.branch }} git config --global user.name "seL4 CI" git config --global user.email "ci@sel4.systems" - git rebase origin/master git status - - name: Push - run: | - cd l4v-${{ matrix.branch }} - git push -f origin HEAD:${{ matrix.branch }}-rebased + git push -f origin HEAD:exynos5-ver diff --git a/.github/workflows/proof.yml b/.github/workflows/proof.yml index 329394868b5..df00bf3daaf 100644 --- a/.github/workflows/proof.yml +++ b/.github/workflows/proof.yml @@ -5,12 +5,6 @@ name: Proof PR on: - push: - paths-ignore: - - '**.md' - - '**.txt' - branches: - - rt # this action needs access to secrets. # The actual test runs in a no-privilege VM, so it's Ok to run on untrusted PRs. pull_request_target: @@ -27,14 +21,16 @@ jobs: strategy: fail-fast: false matrix: - arch: [ARM, ARM_HYP, AARCH64, RISCV64, X64] - # test only most recent push to PR: + arch: [ARM_HYP] + plat: [exynos5] + # test only most recent push to PR or branch: concurrency: l4v-pr-${{ github.event.number }}-idx-${{ strategy.job-index }} steps: - name: Proofs uses: seL4/ci-actions/aws-proofs@master with: L4V_ARCH: ${{ matrix.arch }} + L4V_PLAT: ${{ matrix.plat }} session: '-x AutoCorresSEL4' # exclude large AutoCorresSEL4 session for PRs env: AWS_ACCESS_KEY_ID: ${{ secrets.AWS_ACCESS_KEY_ID }}