Gerwin Klein

Results 521 comments of Gerwin Klein

Ok, so if we want to make one more attempt at properly testing this before we merge (I'm fine with this PR as is, but we might need additional changes...

> I think the tests are failing since `-bios none` is missing from the QEMU command. You mean `QEMU_CMD` in the cmake change here or should should there be something...

If I understand @Ivan-Velickovic correctly, he meant adding ```cmake set(qemu_sim_extra_args "-bios none") ``` in https://github.com/seL4/seL4_tools/pull/154

> guess the manual is probably not the right place to document such details. I am thinking about a wiki for the purpose. Also we could extract some previous questions...

If the proofs pass, I have no strong feelings either way for this PR. Removing a little bit of duplication makes sense. I'm unclear on wether the new includes are...

> Yes, that would make sense. Now that the github CI action works, all the builds and simulates test work there also nicely. Just the proofs can't run there to...

It looks to me like there is still a potential bug here, but it needs more investigation. Draft would be appropriate, yes.

What do we do with this one? @xurtis I assume you're not going to be able to finish it. The PR as such seems close, and could be completed, but...

Ok, you be happy to be assigned to this and the PR being kept on draft until it is done?

> @lsf37, would it be possible to add an option to run sel4bench actions on seL4 kernel PRs via a label? Yes that could be done. I'm on leave this...