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.

Cheers,
Gerwin

_______________________________________________
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems

Reply via email to