Skip to content

Commit

Permalink
ci: temporarily remove mcs-export from proof-deploy
Browse files Browse the repository at this point in the history
This removes the mcs-export matrix job from the proof-deploy workflow,
as the first step towards solving #497. This should unblock
verification manifest deployments.

The mcs-export job was added to the proof-deploy workflow to perform
SimplExportAndRefine for binary verification targets. It took a short
cut, using the master branch of l4v to perform SimplExportAndRefine for
MCS configurations, since there were no differences between rt and
master that were relevant to SimplExportAndRefine. This is no longer the
case, because MCS seL4 C code now contains C parser annotations that use
symbols only available in the rt branch of l4v.

We intend to add an equivalent job that uses the rt branch of l4v for
MCS SimplExportAndRefine, but are still working out the best way to do
that.

Signed-off-by: Matthew Brecknell <matt@kry10.com>
  • Loading branch information
mbrcknl committed Jul 6, 2022
1 parent 8f75837 commit 66e9f1c
Showing 1 changed file with 2 additions and 36 deletions.
38 changes: 2 additions & 36 deletions .github/workflows/proof-deploy.yml
Original file line number Diff line number Diff line change
Expand Up @@ -59,44 +59,10 @@ jobs:
name: logs-${{ matrix.arch }}
path: logs.tar.xz

mcs-export:
name: MCS
needs: code
runs-on: ubuntu-latest
strategy:
fail-fast: false
matrix:
arch: [ARM, RISCV64]
# test only most recent push:
concurrency: l4v-regression-${{ github.ref }}-${{ strategy.job-index }}-mcs
steps:
- name: SimplExport
uses: seL4/ci-actions/aws-proofs@master
with:
L4V_ARCH: ${{ matrix.arch }}
L4V_FEATURES: MCS
xml: ${{ needs.code.outputs.xml }}
session: SimplExportAndRefine
env:
AWS_ACCESS_KEY_ID: ${{ secrets.AWS_ACCESS_KEY_ID }}
AWS_SECRET_ACCESS_KEY: ${{ secrets.AWS_SECRET_ACCESS_KEY }}
AWS_SSH: ${{ secrets.AWS_SSH }}
- name: Upload C graph-lang
uses: actions/upload-artifact@v3
with:
name: c-graph-lang
path: artifacts/simpl-export
if-no-files-found: ignore
- name: Upload logs
uses: actions/upload-artifact@v3
with:
name: logs-${{ matrix.arch }}-MCS
path: logs.tar.xz

deploy:
name: Deploy manifest
runs-on: ubuntu-latest
needs: [code, proofs, mcs-export]
needs: [code, proofs]
steps:
- uses: seL4/ci-actions/l4v-deploy@master
with:
Expand All @@ -107,7 +73,7 @@ jobs:
binary-verification:
name: Trigger binary verification
runs-on: ubuntu-latest
needs: [code, proofs, mcs-export]
needs: [code, proofs]
steps:
# download-artifact doesn't have an option to ignore missing artifacts,
# so we download them all to test if c-graph-lang exists.
Expand Down

0 comments on commit 66e9f1c

Please sign in to comment.