Hi, Does it work if you try ../init --plat pc99 --tut hello-1 on version 10.0.0 or later of the tutorials? I am aware of an issue where the tutorial documentation on https://docs.sel4.systems/Tutorials was updated to reflect version 10.0.0, but the link to the sources wasn't updated from 9.0.1. The error you are getting seems consistent with trying to apply instructions from 10.0.0 on an earlier version. With regards to seL4bench. If I use the following in a new build directory: ../init-build.sh -DPLATFORM=ia32 -DHARDWARE=TRUE -DRELEASE=TRUE -DFAULT=TRUE -DFASTPATH=TRUE? when I invoke ninja it builds the correct images for me located in ./images/. I noticed that you have -DAARCH32 in your configure line, which will try and use an aarch32 toolchain. Kind regards, Kent. ________________________________ From: Devel on behalf of 송대영 Sent: Friday, June 15, 2018 12:17 PM To: devel@sel4.systems Subject: [seL4] ninja build tool error Hello, I have q the problem? uestion about sel4's new ninja build tool. 1. From now on, sel4-tutorials use ninja build tool, so I repo new sel4-tutorials. Last step, I executue this command "../init-build.sh --plat pc99 --tut hello-1" but It prints with this error messages. What's --------------------------------------------------------------------------------------------- CMake Warning at tools/cmake-tool/flags.cmake:123 (message): Kernel supports hardware floating point but toolchain does not Call Stack (most recent call first): tools/cmake-tool/base.cmake:58 (include) tools/cmake-tool/all.cmake:16 (include) CMakeLists.txt:23 (include) CMake Error at projects/sel4-tutorials/CMakeLists.txt:34 (message): You must select a tutorial for compilation. Select using -DTUTORIAL=<PREFERENCE>. Choose one of hello-1;hello-2;hello-2-nolibs;hello-3;hello-3-nolibs;hello-4;hello-4-app;hello-timer;hello-timer-client. -- Configuring incomplete, errors occurred! See also "/home/scribnote5/sel4-tutorials-manifest/build_hello_1/CMakeFiles/CMakeOutput.log". 2. How can I build sel4 ia32 images in sel4bench? This command "../init-build.sh -DPLATFORM=ia32 -DHARDWARE=TRUE -DAARCH32=TRUE -DRELEASE=TRUE -DFAULT=TRUE -DFASTPATH=TRUE" doesn't make sel4bench image file.