ci: temporarily remove mcs-export from proof-deploy

This removes the mcs-export matrix job from the proof-deploy workflow,
as the first step towards solving seL4/l4v#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>
This commit is contained in:
Matthew Brecknell 2022-07-06 14:56:32 +10:00 committed by Matthew Brecknell
parent 8f758375c8
commit 81423c2200
1 changed files with 2 additions and 36 deletions

View File

@ -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:
@ -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.