ci: temporarily remove mcs-export from proof-deploy #498
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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>
mbrcknl
added a commit
that referenced
this pull request
Jul 7, 2022
This adds adds an mcs-export workflow, as a further step towards solving 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. 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. Signed-off-by: Matthew Brecknell <matt@kry10.com>
mbrcknl
added a commit
that referenced
this pull request
Jul 7, 2022
This adds adds an mcs-export workflow, as a further step towards solving 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
added a commit
that referenced
this pull request
Jul 7, 2022
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>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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