Gerwin Klein

Results 628 comments of Gerwin Klein

> For some reason `if (config_set(CONFIG_HAVE_FPU))` doesn't work to hide things. Easily fixed by creating an empty `fpuRelease`, but I wouldn't expect that would be necessary. Any suggestions? > >...

Tests are looking good now, I'll rebase for the cmake restyling.

Alright, things are finally passing. The link check is failing on the RFC link that will only exist once merged, and the zcu106 is failure is unrelated. Will go ahead...

It doesn't seem to matter which period the thread is set to or what else runs in the system. I encountered the behaviour with experimental domain support on, but Alain...

Do you get it deterministically on sel4test? Because I'm sure I saw it working there when I tried to reproduce Alain's initial report. Edit: a possible explanation is a difference...

Factoring things out would make sense. I still need a separate file per platform for the verification build system to pick the right combination of things, but if they all...

Ok, I've now factored these out into a main include file per major architecture, and single platforms are then only: ```cmake include(${CMAKE_CURRENT_LIST_DIR}/include/ARM_verified_include.cmake) set(KernelPlatform "tk1" CACHE STRING "") ``` Still need...

Just pointing out here that this discussion has happened before in almost the same words and ended in using Google repo.

You're free to decide whatever you like, I'm just pointing out that I see history repeating. Both options suck. Monorepos also suck. All solutions to this problem that I have...

> I'd expect threads that aren't running underneath a guest OS to behave identically to when seL4 is built without hypervisor support. I would not generally expect that. EL1 and...