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 <zhouchun...@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/ _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
