Hi Harry, thanks for reporting this. Will update the instructions. It doesn’t actually have to be gcc-arm-none-eabi (it only needs the C preprocessor and pretty much any will do, you just need to set the compiler prefix in the Makefile), but it’s best to use the exact same toolchain as for building the binary, so will make that the recommended version. Did you get other targets not building before you installed MLton? https://github.com/seL4/l4v/pull/1 seems to have had problems with other targets, but I haven’t been able to reproduce those yet. Cheers, Gerwin On 01.08.2014, at 1:04 am, Harry Butterworth mailto:heb1001@gmail.com> wrote: On Ubuntu 14.04, after attempting to follow the instructions, I found I needed to add two extra packages. I needed mlton-complier for CParserTools and gcc-arm-none-eabi for CBaseRefine. gcc-arm-linux-gnueabi is a documented dependency for 14.04 and was already installed when the CBaseRefine test was failing. After installing those two packages and the documented latex extras all 31 regression tests passed. _______________________________________________ Devel mailing list Devel@sel4.systemsmailto:Devel@sel4.systems https://sel4.systems/lists/listinfo/devel ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.