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 to preprocess-deploy #876

Closed
wants to merge 1 commit into from

Conversation

mbrcknl
Copy link
Member

@mbrcknl mbrcknl commented Jul 7, 2022

This commit will cause the preprocess-deploy workflow to fail if there
are changes to the preprocessed seL4 sources in MCS configurations
covered by the proofs. This means that changes to proof-relevant MCS
configurations will require a manual verification manifest update.

Previously, only non-MCS configurations were covered, which meant that
new verification manifests would be automatically deployed even if there
were proof-relevant changes to MCS code.

This commit will cause the preprocess-deploy workflow to fail if there
are changes to the preprocessed seL4 sources in MCS configurations
covered by the proofs. This means that changes to proof-relevant MCS
configurations will require a manual verification manifest update.

Previously, only non-MCS configurations were covered, which meant that
new verification manifests would be automatically deployed even if there
were proof-relevant changes to MCS code.

Signed-off-by: Matthew Brecknell <matt@kry10.com>
@mbrcknl mbrcknl added verification Needs formal verification input/change, or is motivated by verification CI related to continuous integration and testing labels Jul 7, 2022
@mbrcknl mbrcknl requested a review from lsf37 July 7, 2022 05:26
@mbrcknl mbrcknl marked this pull request as draft July 7, 2022 08:16
@mbrcknl
Copy link
Member Author

mbrcknl commented Jul 7, 2022

Switching to draft while we think a bit more about seL4/l4v#497.

@axel-h
Copy link
Member

axel-h commented Sep 12, 2022

This seem to copy what the preprocess step in https://github.com/seL4/seL4/blob/master/.github/workflows/pr.yml does already, right? Maybe this could be unified then?

@lsf37
Copy link
Member

lsf37 commented Sep 13, 2022

I don't think this can be unified, the MCS setup is a separate manifest and separate set of branches in the verification. It'll needs its own stream.

@lsf37
Copy link
Member

lsf37 commented Sep 13, 2022

Maybe I should phrase this differently: the current setup is already too unified and makes the assumption that in the verification the rt and master branches verify the same revision of the seL4 kernel. That assumption was fine before the C proofs started, but it is not true any more. Of course they should eventually converge and ideally remain at the same one, but that's the goal state, not the necessarily the current state.

@mbrcknl
Copy link
Member Author

mbrcknl commented Dec 5, 2022

Closing for now. Will open new PRs when I have a proper solution to #497, i.e. automatic CPP-compatible updates in a separate stream for MCS.

@mbrcknl mbrcknl closed this Dec 5, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
CI related to continuous integration and testing verification Needs formal verification input/change, or is motivated by verification
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants