Matthew Brecknell
Matthew Brecknell
Switched to draft while thinking about https://github.com/seL4/l4v/issues/497.
I'll take a look now.
@lsf37 Thinking about how to do this... Do you think it would be worth pulling the `mcs-export` job out into a separate workflow? Just thinking that proof-deploy.yml is the wrong...
@lsf37 Thinking about this some more... IIUC, proof-deploy runs if there's a push to l4v master, or a manual bump of the devel.xml manifest. That's useful for BV, since it...
> * seL4 auto-deploys to `devel.xml`. cpp-compatible updates are not recorded in `default.xml` Right you are. I didn't actually look at the seL4-pp script, and just assumed it updated both...
> I had been wanting these to give me a checkout that can work with MCS proofs, to the extent that we have them, if only I switch l4v to...
> Which gcc version does binary verification assume? :) BV does not have particularly strong assumptions on compiler versions, in the sense that compiler feature support doesn't have much bearing...
Switching to draft while we think a bit more about seL4/l4v#497.
> It does seem though that the grant right on the reply cap is fairly redundant (but probably required for consistency). At the risk of further analogising with the non-MCS...
> > I'd be fine with leaving it in for now. It's easier to do a second round that removes it than a second round that adds it back in...