Hi guys, I am a newbie of seL4 and I am trying to get some understanding of it. So, my first question is about the build system of seL4: 1. Why cmake has been taken to build it? I think there are at least two shortcomings about current build system based on CMakeLists.txt: - Some build options were implied in the CMakeLists.txt. It's not easy to get a complete and comprehensive understanding of all the options. And some options depends on other options. Such as, ./init-build.sh -DPLATFORM=odroidc2 -DAARCH64=1 A new guys couldn't get a support list of PLATFORM option, and know AARCH64 is only for ARMv8 SoC easily. - There are too much branches of platform or SoC Architectures. Such as: if(KernelArchARM) include_directories("include/arch/arm/armv/${KernelArmArmV}/") include_directories("include/arch/arm/armv/${KernelArmArmV}/${KernelWordSize}") endif() if(KernelArmMach STREQUAL "exynos") include_directories("include/plat/exynos_common/") endif() if(KernelArchRiscV) include_directories("include/arch/${KernelArch}/arch/${KernelWordSize}") include_directories("include/plat/${KernelPlatform}/plat/${KernelWordSize}") endif() Linux Build System places the special build options and source files into the directory related with each architectures, and will generated a configure file (.config) during building. It's very good in my opinion. In Android Build System, a given project building inherits a common build options set, and update these parts only related the given project. It's very good for integration. And I want to know if there is a plan to update the build system or accept patches from volunteer? 2. I notice that, all kernel source files have been concatenated into a kernel_all.c, and compile the kernel_all.c. Is there some special reason for this step? It's a slight strange for me? Anyway, I am a new guy. I just want to understand it and if I could provide something to change it. Any comments are appreciated. Thanks, Jerry
Hi Jerry,
"Jerry" == Jerry Zhou <zhouchunhua@lixiang.com> writes:
Jerry> 1. Why cmake has been taken to build it? I think there are at Jerry> least two shortcomings about current build system based on Jerry> CMakeLists.txt: We used to use the KBuild system (same as Linux Kernel). Switching to CMake/Ninja cuts build times to less than a third what they used to be. Patches for improvement are welcome. Jerry> 2. I notice that, all kernel source files have been Jerry> concatenated into a kernel_all.c, and compile the Jerry> kernel_all.c. Is there some special reason for this step? It's Jerry> a slight strange for me? This is so it can easily be imported into Isabelle for the proof. The importer needs the file after the preprocessor has run. and needs all the code in one go. Peter C -- Peter Chubb Principal Research Engineer | Trustworthy Systems | Data61 | CSIRO +61 2 9490 5852 | http://ts.data61.csiro.au/
Hi Peter, I am so glad to get a reply from you. And the following are my understandings. Thanks, Jerry On Sun, Mar 28, 2021 at 04:11:36AM +0000, Chubb, Peter (Data61, Eveleigh) wrote:
Hi Jerry,
"Jerry" == Jerry Zhou <zhouchunhua@lixiang.com> writes:
Jerry> 1. Why cmake has been taken to build it? I think there are at Jerry> least two shortcomings about current build system based on Jerry> CMakeLists.txt:
We used to use the KBuild system (same as Linux Kernel). Switching to CMake/Ninja cuts build times to less than a third what they used to be.
Patches for improvement are welcome.
Good! I will try it.
Jerry> 2. I notice that, all kernel source files have been Jerry> concatenated into a kernel_all.c, and compile the Jerry> kernel_all.c. Is there some special reason for this step? It's Jerry> a slight strange for me?
This is so it can easily be imported into Isabelle for the proof. The importer needs the file after the preprocessor has run. and needs all the code in one go.
Great! It seams reasonable.
Peter C -- Peter Chubb Principal Research Engineer | Trustworthy Systems | Data61 | CSIRO +61 2 9490 5852 | http://ts.data61.csiro.au/
participants (2)
-
Chubb, Peter (Data61, Eveleigh) -
Jerry Zhou