Re: [SPITBALL] Jehanne as another kernel option / porting target

[Vincent Legoll <vincent.legoll@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 358 bytes --]

On Fri, Mar 19, 2021 at 7:02 PM Vincent Legoll <vincent.legoll@gmail.com> wrote:
> I have created a guix build recipe for seL4 recently, it builds, but I don't
> know what to do with it :-)
>
> I'll send it as a followup to this thread, if any one is interested.

Here it is, ukernel only, hardcoded arch, nothing fancy like camkes, etc.

-- 
Vincent Legoll

[-- Attachment #2: 0001-gnu-Add-sel4.patch --]
[-- Type: text/x-patch, Size: 4243 bytes --]

From 607cef41839131fd740fbf754d30f3a9277c5a0a Mon Sep 17 00:00:00 2001
From: Vincent Legoll <vincent.legoll@gmail.com>
Date: Fri, 19 Feb 2021 23:49:43 +0100
Subject: [PATCH] gnu: Add sel4.

* gnu/packages/sel4.scm: New file...
* gnu/local.mk (GNU_SYSTEM_MODULES): ...Add it here.
---
 gnu/local.mk          |  1 +
 gnu/packages/sel4.scm | 83 +++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 84 insertions(+)
 create mode 100644 gnu/packages/sel4.scm

diff --git a/gnu/local.mk b/gnu/local.mk
index 33da7b979a..6d4ddb2bdd 100644
--- a/gnu/local.mk
+++ b/gnu/local.mk
@@ -502,6 +502,7 @@ GNU_SYSTEM_MODULES =				\
   %D%/packages/sdl.scm				\
   %D%/packages/search.scm			\
   %D%/packages/security-token.scm		\
+  %D%/packages/sel4.scm				\
   %D%/packages/selinux.scm			\
   %D%/packages/sequoia.scm			\
   %D%/packages/serialization.scm		\
diff --git a/gnu/packages/sel4.scm b/gnu/packages/sel4.scm
new file mode 100644
index 0000000000..6fc3f88ac2
--- /dev/null
+++ b/gnu/packages/sel4.scm
@@ -0,0 +1,83 @@
+;;; GNU Guix --- Functional package management for GNU
+;;; Copyright © 2021 Vincent Legoll <vincent.legoll@gmail.com>
+;;;
+;;; This file is part of GNU Guix.
+;;;
+;;; GNU Guix is free software; you can redistribute it and/or modify it
+;;; under the terms of the GNU General Public License as published by
+;;; the Free Software Foundation; either version 3 of the License, or (at
+;;; your option) any later version.
+;;;
+;;; GNU Guix is distributed in the hope that it will be useful, but
+;;; WITHOUT ANY WARRANTY; without even the implied warranty of
+;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+;;; GNU General Public License for more details.
+;;;
+;;; You should have received a copy of the GNU General Public License
+;;; along with GNU Guix.  If not, see <http://www.gnu.org/licenses/>.
+
+(define-module (gnu packages sel4)
+  #:use-module (gnu packages)
+  #:use-module (gnu packages python)
+  #:use-module (gnu packages python-xyz)
+  #:use-module (gnu packages python-web)
+  #:use-module (gnu packages ninja)
+  #:use-module (gnu packages xml)
+  #:use-module (guix build-system cmake)
+  #:use-module ((guix licenses) #:prefix license:)
+  #:use-module (guix packages)
+  #:use-module (guix git-download))
+
+(define-public sel4
+  (package
+    (name "sel4")
+    (version "12.0.0")
+    (source
+     (origin
+       (method git-fetch)
+       (uri (git-reference
+             (url "https://github.com/seL4/seL4")
+             (commit version)))
+       (file-name (git-file-name name version))
+       (sha256
+        (base32 "1zkx6x5jly8f75ph9jxd2jrp1kg5l001zkfqpmjf8ancsi1b43y7"))))
+    (build-system cmake-build-system)
+    (arguments
+     '(#:tests? #f ;; No need for tests when you have formal proof of correctness
+       #:configure-flags
+       (list
+        "-G" "Ninja"
+        "-DKernelArch=x86"
+        "-DCROSS_COMPILER_PREFIX="
+        "-DCMAKE_TOOLCHAIN_FILE=../source/gcc.cmake"
+        "-C" "../source/configs/X64_verified.cmake")
+       #:phases (modify-phases %standard-phases
+                  (replace 'build
+                    (lambda _
+                      (invoke "ninja" "kernel.elf")))
+                  (replace 'install
+                    (lambda _
+                      (mkdir-p %output)
+                      (copy-file "kernel.elf"
+                                 (string-append %output "/kernel.elf")))))))
+    (native-inputs
+     `(("libxml2" ,libxml2)
+       ("ninja" ,ninja)
+       ("python" ,python-3)
+       ("python-future" ,python-future)
+       ("python-jinja2" ,python-jinja2)
+       ("python-paste" ,python-paste)
+       ("python-ply" ,python-ply)
+       ("python-six" ,python-six)
+       ))
+    (synopsis "Operating System microkernel")
+    (description "Formally verified member of the L4 microkernel family.")
+    (home-page "https://sel4.systems")
+    (license (list license:asl2.0 ; And also a variant in LICENSES/SHL-0.51.txt
+                   license:bsd-2
+                   license:bsd-3
+                   license:cc-by-sa4.0
+                   license:gpl2
+                   license:gpl2+
+                   license:lppl1.3c
+                   license:x11))))
-- 
2.30.0