From 9947fed0ae7373a28e8292782a3f9be8c0daca56 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Tue, 22 Jul 2014 15:20:36 +0200 Subject: [PATCH 1/6] Add overview to README --- README | 79 ++++++++++++++++++++++++++++++++++++++++------------------ 1 file changed, 55 insertions(+), 24 deletions(-) diff --git a/README b/README index d793f687b..53d507785 100644 --- a/README +++ b/README @@ -1,35 +1,66 @@ -# -# Copyright 2014, General Dynamics C4 Systems -# -# This software may be distributed and modified according to the terms of -# the GNU General Public License version 2. Note that NO WARRANTY is provided. -# See "LICENSE_GPLv2.txt" for details. -# -# @TAG(GD_GPL) -# + -'make' instructions +The seL4 Repository =================== -tl;dr: TOOLPREFIX=arm-none-eabi- ARCH=arm PLAT=imx31 ARMV=armv6 \ - CPU=arm1136jf-s make +This repository contains the source code of seL4 microkernel. + +This repository is usually not used in isolation, but as part of the build +system in a larger project. + + +Repository Overview +------------------- + + * `include` and `src`: C and ASM source code of seL4 + * `tools`: build tools + * `haskell`: Haskell model of the seL4 kernel, + kept in sync with the C version. + * `libsel4`: C bindings for the seL4 ABI + * `manual`: LaTeX sourced of the seL4 reference manual + + +Build Instructions +------------------ + +tl;dr: + + TOOLPREFIX=arm-none-eabi- ARCH=arm PLAT=imx31 ARMV=armv6 CPU=arm1136jf-s \ + make The kernel source requires a cross-compiler for the target architecture. To -build using make, follow these instructions: +build using `make`, follow these instructions: - * Ensure that the appropriate cross-compiler is installed. + * Ensure that the appropriate cross-compiler for your target + architecture is installed. - * Set the TOOLPREFIX environment variable to your cross-compiler's prefix. E.g. - arm-none-eabi-. + * Set the `TOOLPREFIX` environment variable to your cross-compiler's + prefix. E.g. `arm-none-eabi-`. - * Set the ARCH, PLAT, ARMV and CPU variables for the intended target + * Set the `ARCH`, `PLAT`, `ARMV` and `CPU` variables for the intended target architecture and platform, chosen from the following lists: - ARCH PLAT ARMV CPU - ------------------------------------ - arm imx31 armv6 arm1136jf-s - arm omap3 armv7-a cortex-a8 - arm am335x armv7-a cortex-a8 - ia32 pc99 + ARCH | PLAT | ARMV | CPU + -----|--------|---------|----------- + arm | imx31 | armv6 | arm1136jf-s + arm | omap3 | armv7-a | cortex-a8 + arm | am335x | armv7-a | cortex-a8 + ia32 | pc99 | | + + * For a debug build, append `DEBUG=y`. - * For a debug build, append "DEBUG=y". + +License +======= + +The files in this repository are released under standard open source licenses. +Please see the individual file headers and `LICENSE_GPLv2.txt` and +`LICENSE_BSD2.txt` files for details. From addc9a9054e9da4e1130ba3fca044b397cd0b8b4 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Tue, 22 Jul 2014 15:20:54 +0200 Subject: [PATCH 2/6] prefer markdown for github --- README => README.md | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename README => README.md (100%) diff --git a/README b/README.md similarity index 100% rename from README rename to README.md From 9711f8134f1e4b48010b1168f4b1acd94f4c2ee4 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Sun, 27 Jul 2014 20:42:40 +0200 Subject: [PATCH 3/6] bump API version number --- manual/VERSION | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/manual/VERSION b/manual/VERSION index 5625e59da..7e32cd569 100644 --- a/manual/VERSION +++ b/manual/VERSION @@ -1 +1 @@ -1.2 +1.3 From 64b43f444784f902d4259aa07333651f95be8119 Mon Sep 17 00:00:00 2001 From: David Greenaway Date: Tue, 29 Jul 2014 19:58:26 +1000 Subject: [PATCH 4/6] Add links to "seL4.systems" website to "README.md". --- README.md | 24 +++++++++++++++--------- 1 file changed, 15 insertions(+), 9 deletions(-) diff --git a/README.md b/README.md index 53d507785..1dbf74ca2 100644 --- a/README.md +++ b/README.md @@ -1,10 +1,10 @@ - @@ -13,25 +13,31 @@ The seL4 Repository This repository contains the source code of seL4 microkernel. +For details about the seL4 microkernel, including details about the proof, +please see the [`sel4.systems`][1] website and associated [FAQ][2]. + This repository is usually not used in isolation, but as part of the build system in a larger project. + [1]: http://sel4.systems/ + [2]: http://sel4.systems/FAQ/ + Repository Overview ------------------- * `include` and `src`: C and ASM source code of seL4 * `tools`: build tools - * `haskell`: Haskell model of the seL4 kernel, + * `haskell`: Haskell model of the seL4 kernel, kept in sync with the C version. * `libsel4`: C bindings for the seL4 ABI - * `manual`: LaTeX sourced of the seL4 reference manual + * `manual`: LaTeX sourced of the seL4 reference manual Build Instructions ------------------ -tl;dr: +tl;dr: TOOLPREFIX=arm-none-eabi- ARCH=arm PLAT=imx31 ARMV=armv6 CPU=arm1136jf-s \ make @@ -39,10 +45,10 @@ tl;dr: The kernel source requires a cross-compiler for the target architecture. To build using `make`, follow these instructions: - * Ensure that the appropriate cross-compiler for your target + * Ensure that the appropriate cross-compiler for your target architecture is installed. - * Set the `TOOLPREFIX` environment variable to your cross-compiler's + * Set the `TOOLPREFIX` environment variable to your cross-compiler's prefix. E.g. `arm-none-eabi-`. * Set the `ARCH`, `PLAT`, `ARMV` and `CPU` variables for the intended target @@ -54,7 +60,7 @@ build using `make`, follow these instructions: arm | omap3 | armv7-a | cortex-a8 arm | am335x | armv7-a | cortex-a8 ia32 | pc99 | | - + * For a debug build, append `DEBUG=y`. From f5b2a6f9c796ff50301d486d39c438edcb3e1ad2 Mon Sep 17 00:00:00 2001 From: Adrian Danis Date: Wed, 30 Jul 2014 14:21:33 +1000 Subject: [PATCH 5/6] Do not discard user PYTHONPATH when building --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 0d9de5aa8..67d312300 100644 --- a/Makefile +++ b/Makefile @@ -147,7 +147,7 @@ default: all ### Paths ############################################################ -PYTHONPATH = ${SOURCE_ROOT}/tools +PYTHONPATH := ${PYTHONPATH}:${SOURCE_ROOT}/tools export PYTHONPATH vpath %.c ${SOURCE_ROOT} From 53941f4beb317ea51bbb7cc6a95962091f24f93a Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Thu, 31 Jul 2014 15:05:12 +1000 Subject: [PATCH 6/6] remove unsupported platform --- Kconfig | 14 -------------- 1 file changed, 14 deletions(-) diff --git a/Kconfig b/Kconfig index 8f3c3e3ab..8b5c79646 100644 --- a/Kconfig +++ b/Kconfig @@ -55,13 +55,6 @@ config ARCH_IA32 help Support for ARM1136JF-S - config ARM926EJ_S - bool "ARM926EJ-S" - depends on ARCH_ARM - select ARCH_ARM_V5 - help - Support for ARM926EJ_S - config ARM_CORTEX_A8 bool "Cortex A8" depends on ARCH_ARM @@ -97,13 +90,6 @@ config ARCH_IA32 help Support for the KZM platform - config PLAT_INTEGRATORCP - bool "IntegratorCP Platform" - depends on ARCH_ARM - depends on ARM926EJ_S - help - Support for the IntegratorCP platform - config PLAT_OMAP3 bool "OMAP3 (BeagleBoard)" depends on ARCH_ARM