NoWayOS
DE
GitHub
MenüSchließen

Hier beginnen

Erste Schritte

Bauen Sie den Dev-Container von NoWayOS und starten Sie seine klickbare Demo, jedes Frame geprüft, ganz ohne Hardware und ohne seL4-Kenntnisse.

NoWayOS wird in einem einzigen, fest versionierten Dev-Container gebaut, sodass Ihr Rechner selbst sehr wenig braucht. Diese Seite bringt Sie von null bis zur laufenden Demo. Die nächste Seite bootet ein echtes seL4-System in QEMU, und eine spätere bringt es auf einen Raspberry Pi 5.

Was Sie brauchen

  • Podman und GNU Make. Docker funktioniert auch: Ergänzen Sie jeden make-Befehl um ENGINE=docker.
  • git, um die Repositories zu klonen.
  • Kein Rust und keine seL4-Werkzeuge auf Ihrem Rechner. Die Rust-Toolchains, das Microkit SDK und QEMU stecken alle im Dev-Container, festgelegt auf exakte Versionen.

Unter macOS führt Podman Container in einer virtuellen Maschine aus. Legen Sie diese einmal an und starten Sie sie, mit ein paar CPUs und mehreren Gigabyte Arbeitsspeicher, zum Beispiel:

podman machine init --cpus 4 --memory 8192
podman machine start

NoWayOS wird auf Apple Silicon (arm64) entwickelt. Auch für x86-64 sind die Pakete des Dev-Images fest versioniert und geprüft, doch dort wurde das Image noch nicht durchgängig gebaut und getestet.

Geben Sie NoWayOS einen eigenen Ordner

Der Dev-Container bindet den Ordner oberhalb Ihres Klons ein, damit nebeneinander geklonte Repositories gegeneinander bauen können. Legen Sie dafür zuerst einen Ordner an:

mkdir nowayos-work && cd nowayos-work
git clone https://github.com/NoWayOS/nowayos.git
cd nowayos

Den Dev-Container bauen

make container

Das baut das fest versionierte Dev-Image: die Rust-Toolchains, das Microkit SDK, QEMU und die Prüfwerkzeuge. Der erste Build dauert ein paar Minuten (unter vier auf einem Mac mit Apple Silicon) und erzeugt ein Image von etwa 4,7 GB. Führen Sie ihn erneut aus, sobald sich tools/container/Containerfile ändert; jedes andere Target verweigert die Ausführung auf einem veralteten Image und sagt Ihnen das auch.

Die Demo starten

make demo

Die Demo ist eine kleine Formularanwendung mit einer gescripteten Sitzung aus Touch-Eingaben, Klicks und Tastendrücken. Sie läuft als Host-Simulation, ohne seL4 und ohne QEMU, und zeichnet das Frame jedes Schritts mit dem echten UI-Kern und Renderer von NoWayOS. Jedes Frame wird mit einem abgenommenen Bild verglichen, und der Lauf endet mit:

demo: PASS - … steps, every frame as approved

Weicht ein Frame auch nur um ein einziges Pixel ab, nennt der Lauf den Schritt und schlägt fehl.

Sich umsehen

make # every target, with a line on each
make test # unit, property, doc and golden-image tests
make lint # rustfmt, then clippy with warnings as errors

Jedes Target läuft im Dev-Container und startet ihn für Sie. Die DEVELOPING.md des Repositorys listet sie alle auf, zusammen mit der Struktur des Codes.

Wenn etwas schiefgeht

  • error: … was not built from the current … Containerfile: Die Definition des Containers hat sich geändert, seit Sie ihn gebaut haben. Führen Sie make container erneut aus, wie die Meldung sagt.
  • Podman ist nicht erreichbar: Starten Sie unter macOS seine virtuelle Maschine mit podman machine start.
  • Einem Build geht der Speicher aus: Geben Sie der virtuellen Maschine von Podman mehr Arbeitsspeicher. Das komplette Gate, make ci, führt Model-Checking-Beweise aus, die weit mehr brauchen als die Demo (Prüfungen und Nachweise).