[seL4] Re: Issues with PR

On 21 Nov 2020, at 11:36, Demi M. Obenour wrote:

Signed PGP part On 11/20/20 5:21 PM, Klein, Gerwin (Data61, Kensington NSW) wrote:

...

If changes do break the proof, then we'd need to discuss how to verify them and who will do the work for it. Looking at your PR, I think they would be fine, but I’ll start a proof run and comment on the PR when it is done.

A couple of related questions:

1. Are formatting changes (whitespace, comments, etc) guaranteed to not break the proofs?

Some comments are proof annotations. As long as those don’t change, other whitespace and comment change will not break the proofs.

2. If a change does break the proofs, would you be willing to coach someone on fixing them?

Yes, depending on the change. If it is a 10 person-year project less likely :-). If it is something small then usually yes. Cheers, Gerwin