These seem to be missing from the system documentation, especially on
how to use it with qemu. I've built the simulator, but am unsure how
to use it. The build generates a libHSSEL4-0.3.a, but I can't find an
Also, the simulator manual says it is out-of-date, but the manual
seems to include the Haskell literate sources directly. It also says
the Haskell code is kept up-to-date. That sounds a bit contradictory.
Are the comments in the sources that obsolete?
[Congratulations on the open-sourcing and excellent license choices!]
I really like to see big formally verified software.
But it seems your provide no way to verify the downloads from your
repositories. I think you should use signed git tags and also ensure
that repo verify those.
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
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.
My name is Joe Quigley, I found out about the project recently and want to
start experimenting with it on a Rasberry Pi I have floating around.
Because it uses a very similar ARMv6 CPU as the KZM-ARM11-01, am I correct
in assuming it will work with that kernel?
I'm getting an error when building from Ubuntu.
I'm building from: repo init -u https://github.com/seL4/sel4test-manifest.git
I've configured with: make ia32_simulation_release_xml_defconfig
and done "make menuconfig" accepting the defaults.
Finally I run make and get errors:
src/sel4/sel4test/kernel/src/arch/ia32/kernel/vspace.c: In function
array subscript is above array bounds [-Werror=array-bounds]
cc1: all warnings being treated as errors
make: *** [kernel_final.s] Error 1
make: *** [kernel_elf] Error 2
Attached is the output of "make V=2" (for verbosity).