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/