Devel

devel@sel4.systems

9 participants
1390 discussions

01 Aug '14

Hi, 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. HW42

2 1

run_tests needs mlton-compiler gcc-arm-none-eabi
by Harry Butterworth 01 Aug '14

01 Aug '14

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.

2 1

AM335X (BeagleBone) support?
by Tim Newsham 31 Jul '14

31 Jul '14

What is the state of "AM335X (BeagleBone)" support in the main and experimental branches? Tim

2 1

Running seL4 on a Raspberry Pi?
by Quigley, Joseph 31 Jul '14

31 Jul '14

Hello! 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? -- --Joe Quigley

2 1

(simple?) build error?
by Tim Newsham 31 Jul '14

31 Jul '14

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: [KERNEL] [CC] kernel_final.s src/sel4/sel4test/kernel/src/arch/ia32/kernel/vspace.c: In function ‘init_boot_pd’: src/sel4/sel4test/kernel/src/arch/ia32/kernel/vspace.c:58:23: error: array subscript is above array bounds [-Werror=array-bounds] cc1: all warnings being treated as errors make[1]: *** [kernel_final.s] Error 1 make: *** [kernel_elf] Error 2 Attached is the output of "make V=2" (for verbosity). Tim

3 2

virtualization and linux?
by Tim Newsham 31 Jul '14

31 Jul '14

Is there any documentation on using the VMM support for x86 seL4? Also, when can we hear more about "Served by Apache on Linux on seL4."? Tim

1 0

Does the kernel build support the gold linker?
by Stephen Thomas 30 Jul '14

30 Jul '14

I tried building the kernel for ARCH=ia32 and PLAT=pc99 and I fail with a linker errror. Is there a linker script that supports the gold linker (for linux). Cheers Thomo

2 1

Initial architecture/processor support in seL4
by Peter Howard 26 Jun '14

26 Jun '14

HI, I'm wondering what CPUs the initial source release for seL4 will support. In http://www.nicta.com.au/pub?doc=6930&filename=Elphinstone_Heiser_13.pdf It references Core i7 32-bit, ARM11, and Cortex A9 - covering x86, ARMv6, and ARMv7. What else will be in there? Thanks, -- Peter Howard <pjh(a)northern-ridge.com.au>

2 2

Re: [seL4] Question about seL4 on July 29th
by Gernot Heiser 21 Jun '14

21 Jun '14

On 21 Jun 2014, at 11:59 , Jorge Ventura <jorge.araujo.ventura(a)gmail.com> wrote: > Anybody knows what kind of Open Source License is expected > to be deployed with seL4 on July 29th ? The seL4 developers mailing list (copied) is probably the better place for this question. Short answer: can’t tell you yet. Longer answer: we have a clear idea of the licenses that will be used for the various parts, but have not yet concluded all formal agreements between the various parties having a say in this, and until that is the case, we cannot reveal more. What I can say is that I expect the community will be happy with the outcome. Gernot

1 0

We're live!
by Gernot Heiser 05 Jun '14

05 Jun '14

This list is probably not of much use until 29 July, but then it will be the place for technical discussions about building systems on seL4. Enjoy, Gernot ________________________________ 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.

1 0

Jump to page:

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel