On 11/20/20 5:21 PM, Klein, Gerwin (Data61, Kensington NSW) wrote: > Hi Iker, > > I'm having certain issues with the PR where I propose another way to get > the gic cpu id directly from hardware registers instead of guessing like > before. > > First of all: thanks for the PR! I assume you mean > https://github.com/seL4/seL4/pull/283 > > > First of all, inside CI/Links some errors appear about sel4 webpage links > that I haven't touched, how can I solve this? > > It’s Ok to ignore this one. Looking at the links that are failing, they have > moved recently (yesterday), and we should update them in a separate PR. > > > At last, on the PR/Preprocess test failure appears but it's not clear what > the problem is and after the compilation test is successful. > > The preprocess test is indeed not yet well documented. Its purpose is to tell > wether the proposed changes will change something in the verified > configurations of seL4 and might therefore need proof updates. > > I had planned to chain this test with a full proof run when it fails (the > preprocess test just sees that something changed, but for many small changes > the proof still works), but it turns out the github CI infrastructure is too > weak to run the proofs (not enough memory on the test runners). We’re looking > into using something else for that, maybe AWS, but I haven’t had time yet to > actually do that (it’s non-trivial to set up, at least if you want to be able > to prevent abuse, and AWS costs money of course). > > So for now, the right course of action, which I’ll document next week, is to > ask for help when the preprocess test fails, so that someone in the > verification team can either review it or run the proofs to check if they > still work. > > 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? 2. If a change does break the proofs, would you be willing to coach someone on fixing them? > Cheers, > Gerwin Sincerely, Demi
OpenPGP_0xB288B55FFF9C22C1.asc
Description: application/pgp-keys
OpenPGP_signature
Description: OpenPGP digital signature
_______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
