Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

ci: add mcs-export workflow #499

Closed
wants to merge 1 commit into from
Closed

Commits on Jul 7, 2022

  1. ci: add mcs-export workflow

    This adds adds an mcs-export workflow, as a further step towards solving
    issue #497. This replaces the mcs-export matrix job that was removed
    from the proof-deploy workflow in #498.
    
    This workflow has some similarities to the proof-deploy workflow:
    - Both workflows check out a manifest, run some proofs, and trigger
      a binary verification workflow.
    - Both workflows are triggered by an update to an l4v branch.
    - Both workflows can be triggered by manual updates to the development
      verification-manifest, but not automatic updates due to a successful
      preprocess test.
    
    The differences are:
    - proof-deploy updates the default verification-manifest, whereas the
      mcs-export workflow does not.
    - proof-deploy uses l4v master, whereas mcs-export uses the rt branch.
    
    When MCS CRefine proofs are sufficiently advanced, the proof-deploy
    workflow will need to be updated to check MCS proofs before updating the
    default verification-manifest. At that point, this workflow could be
    reintegrated into the proof-deploy workflow.
    
    Signed-off-by: Matthew Brecknell <matt@kry10.com>
    mbrcknl committed Jul 7, 2022
    Configuration menu
    Copy the full SHA
    0821215 View commit details
    Browse the repository at this point in the history