Axel Heider

Seems to me that is the usual trade off between debug features and release code. In Debug mode you want to be able to have some insights and thus need...

It is still failing with another issue: ``` [182/299] Building C object apps/sel4bench/seL4_libs/libsel4bench/CMakeFiles/sel4bench.dir/src/arch/arm/armv/armv8-a/event_counters.c.obj FAILED: apps/sel4bench/seL4_libs/libsel4bench/CMakeFiles/sel4bench.dir/src/arch/arm/armv/armv8-a/event_counters.c.obj /usr/bin/ccache /usr/bin/aarch64-linux-gnu-gcc --sysroot=/github/workspace/build -I/github/workspace/projects/seL4_libs/libsel4bench/include -I/github/workspace/projects/seL4_libs/libsel4bench/arch_include/arm/armv/armv8-a -I/github/workspace/projects/seL4_libs/libsel4bench/arch_include/arm/cpu/cortex-a55 -I/github/workspace/projects/seL4_libs/libsel4bench/sel4_arch_include/aarch64 -I/github/workspace/projects/seL4_libs/libsel4bench/arch_include/arm -I/github/workspace/projects/seL4_libs/libsel4bench/src -Iapps/sel4bench/musllibc/build-temp/stage/include -I/github/workspace/kernel/libsel4/include -I/github/workspace/kernel/libsel4/arch_include/arm -I/github/workspace/kernel/libsel4/sel4_arch_include/aarch64 -I/github/workspace/kernel/libsel4/sel4_plat_include/quartz64 -I/github/workspace/kernel/libsel4/mode_include/64...

Seem this patch gets us a bit further in the build., see https://github.com/seL4/sel4bench/actions/runs/3602291771/jobs/6069082715 Now the linker fails because the (missing) timer needs to be configured ``` FAILED: apps/sel4bench/irquser/irquser : &&...

Please provide a bit more context, what you are trying to do and what seL4 system you are using. By default seL4 does not come with a file storage driver...

That would be one option, but running a VMM might be overkill depending on what you are trying to build.

Could you rebase this and have a look into the CI issues. Unfortunately, the logs have been deleted, so I can't see why RV32 complains about.

Making this a draft PR for now. Currently, my main motivation for having a clang build also is to see, if this reports something other than the gcc build. And...

@wom-bat: can you make a PR for this?

see PR https://github.com/seL4/sel4bench/pull/20

If the concern is about hardware resources, it could be a topic for the budget planning.