On 23 Jan 2020, at 13:08, Demi M. Obenour <demioben...@gmail.com> wrote: > > Would you be willing to accept PRs that include the corresponding > changes to the proofs, or which don’t affect verification?
PRs that don’t affect verification will be accepted subject to standard quality control (and availability of a CLA). These are not frequent, but happen. Typically they are platform ports. One of the things we’d like to set up is a way for developers to check this for themselves, which should certainly help contributions. Not sure when this will be ready. The same applies, in principle, to PRs that come with proof updates. We haven’t seen one of these yet. The bar will be higher if the change affects kernel semantics (even if accompanied by proof), as we need to ensure that the design stays clean and principled. Gernot
signature.asc
Description: Message signed with OpenPGP
_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
