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. This no longer works, 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, but are
still working out the best way to do that.
  • Loading branch information
mbrcknl committed Jul 6, 2022
1 parent 8f75837 commit fbf84a3
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 fbf84a3

Please sign in to comment.