Premiers pas

NoWayOS se construit dans un unique conteneur de développement aux versions figées : votre machine n’a besoin de presque rien en propre. Cette page vous mène de zéro jusqu’à la démo en fonctionnement. La page suivante démarre un vrai système seL4 dans QEMU, et une autre, plus loin, le fait tourner sur un Raspberry Pi 5.

Ce qu’il vous faut

• Podman et GNU Make. Docker fonctionne aussi : ajoutez ENGINE=docker à chaque commande make.
• git, pour cloner les dépôts.
• Ni Rust ni outils seL4 sur votre machine. Les chaînes d’outils Rust, le SDK Microkit et QEMU se trouvent tous dans le conteneur de développement, figés à des versions exactes.

Sur macOS, Podman exécute les conteneurs dans une machine virtuelle. Créez-la et démarrez-la une fois, en lui donnant quelques CPU et plusieurs gigaoctets de mémoire, par exemple :

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

NoWayOS est développé sur Apple silicon (arm64). Sur x86-64, les paquets de l’image de développement sont eux aussi figés et relus, mais l’image n’y a pas encore été construite et testée de bout en bout.

Donnez à NoWayOS un dossier rien qu’à lui

Le conteneur de développement monte le dossier au-dessus de votre clone, pour que des dépôts clonés côte à côte puissent se compiler les uns avec les autres. Créez-leur d’abord un dossier :

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

Construire le conteneur de développement

make container

Cette commande construit l’image de développement figée : les chaînes d’outils Rust, le SDK Microkit, QEMU et les outils de vérification. La première construction prend quelques minutes (moins de quatre sur un Mac Apple silicon) et produit une image d’environ 4,7 Go. Relancez-la chaque fois que tools/container/Containerfile change ; toutes les autres cibles refusent de s’exécuter sur une image périmée, et vous le signalent.

Lancer la démo

make demo

La démo est une petite application de formulaire, avec une session scriptée d’appuis tactiles, de clics et de frappes au clavier. Elle s’exécute en simulation sur l’hôte, sans seL4 ni QEMU, et dessine l’image de chaque étape avec le vrai cœur d’interface et le vrai moteur de rendu de NoWayOS. Chaque image est comparée à une image approuvée, et l’exécution se termine ainsi :

demo: PASS - … steps, every frame as approved

Si une image diffère d’un seul pixel, l’exécution indique à quelle étape, et échoue.

Faire le tour

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

Chaque cible s’exécute dans le conteneur de développement, et le démarre pour vous. Le DEVELOPING.md du dépôt les liste toutes, avec l’organisation du code.

En cas de problème

• error: … was not built from the current … Containerfile : la définition du conteneur a changé depuis que vous l’avez construit. Relancez make container, comme l’indique le message.
• Podman est injoignable : sur macOS, démarrez sa machine virtuelle avec podman machine start.
• Une compilation manque de mémoire : donnez davantage de mémoire à la machine virtuelle de Podman. Le contrôle complet, make ci, exécute des preuves par vérification de modèles qui demandent bien plus que la démo (Vérifications et éléments de preuve).