Hi,
i build a simple hello-world example besides the tutorials and it works, but the cmake build system behaves strage:
When i do a fresh configuration and build with:
>> cmake --no-warn-unused-cli -DCROSS_COMPILER_PREFIX=arm-linux-gnueabi- -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -DCMAKE_EXPORT_COMPILE_COMMANDS:BOOL=TRUE -DCMAKE_BUILD_TYPE:STRING=Debug -S/workspaces/seL4-hello-world -B/workspaces/seL4-hello-world/build -G Ninja
>> ninja
i don’t get an output from the kernel or rootserver when running in qemu.
But when i run the cmake command a second time or run cmake . in the build directory and run ninja again it suddenly works and i get the output from the kernel and rootserver.
It seems like the second time cmake is run it adds LibSel4PlatSupportUseDebugPutChar=ON to the CMakeCache.
Why do i get different results when running cmake multiple times without changing anything? Maybe somebody has a hint what i am missing?
If I remember correctly (I’m by no means an expert on the build system), what you’re seeing is “normal” behaviour: the build system does not support reusing a build directory after a config change, i.e. it’ll rebuild incrementally after source changes, but not config changes.
I think this has something to do with how cmake generates and caches things and selects source files depending on config.
@kent-mcleod2 can you confirm?
What I usually do for a config change is nuke the build directory and start with a fresh cmake invocation. This might be overkill – if someone has a more incremental method, please do post it here.
It’d be great if we could at least detect and warn for such circumstances or even better do something about incremental support, because I keep expecting that to work myself before I remember that it doesn’t.
It’s to do with the release/verification config options being applied after the kernel project has been loaded: seL4-hello-world/CMakeLists.txt at master · moritz-meier/seL4-hello-world · GitHub.
These helper functions set kernel configuration options and need to be called in the settings.cmake file (or anywhere else before the kernel CMake project is included in all.cmake).
Here is sel4test’s settings.cmake file: sel4test/settings.cmake at master · seL4/sel4test · GitHub
You would need to include the CMake module defining those functions in your settings.cmake file:
list(APPEND CMAKE_MODULE_PATH tools/seL4/cmake-tool/helpers)
include(application_settings)
ApplyCommonReleaseVerificationSettings(FALSE FALSE)
ApplyCommonSimulationSettings(${KernelSel4Arch})
Thanks,
that fixed it. Running cmake the first time now sets LibSel4PlatUseDebugPutChar=ON and printfs from the kernel and rootserver work in qemu.
Also running cmake a second time does not change the CMakeCache.txt anymore.