はじめに

NoWayOSは、バージョンを固定したひとつの開発コンテナの中でビルドするので、手元のマシン自体に必要なものはごくわずかです。このページでは、何もない状態からデモを動かすところまでを案内します。次のページではQEMUで本物のseL4システムを起動し、その後のページではそれをRaspberry Pi 5に載せます。

必要なもの

• PodmanとGNU Make。Dockerでも動きます。その場合は、各makeコマンドにENGINE=dockerを付けてください。
• リポジトリをクローンするためのgit。
• 手元のマシンにRustもseL4のツールも要りません。 Rustのツールチェーン、Microkit SDK、QEMUはすべて開発コンテナの中にあり、バージョンが厳密に固定されています。

macOSでは、Podmanは仮想マシンの中でコンテナを動かします。最初に一度だけ、CPUを数個とメモリを数GB割り当てて、仮想マシンを作成し、起動してください。たとえば次のとおりです。

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

NoWayOSはApple silicon（arm64）で開発しています。x86-64でも開発イメージのパッケージは固定され、レビューも済んでいますが、そこでイメージをビルドし、端から端までテストしたことはまだありません。

NoWayOS専用のフォルダを用意する

開発コンテナは、クローンしたフォルダのひとつ上のフォルダをマウントします。並べてクローンしたリポジトリどうしが、互いを参照してビルドできるようにするためです。まず、それらを入れるフォルダを作ってください。

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

開発コンテナをビルドする

make container

これで、バージョンを固定した開発イメージがビルドされます。中身はRustのツールチェーン、Microkit SDK、QEMU、チェック用のツールです。初回のビルドには数分かかり（Apple siliconのMacで4分未満）、約4.7 GBのイメージができます。tools/container/Containerfileが変わったら、そのたびにもう一度実行してください。ほかのターゲットはすべて、古いイメージでは実行を拒否し、その旨を知らせます。

デモを動かす

make demo

デモは、タップ、クリック、キー入力をスクリプト化したセッションを持つ、小さなフォームアプリケーションです。seL4もQEMUも使わないホスト上のシミュレーションとして動き、NoWayOSの本物のUIコアとレンダラーで、各ステップのフレームを描きます。各フレームは承認済みの画像と比較され、実行は次の行で終わります。

demo: PASS - … steps, every frame as approved

1ピクセルでも違うフレームがあれば、どのステップかを示して失敗します。

見て回る

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

どのターゲットも開発コンテナの中で動き、コンテナは自動で起動します。リポジトリのDEVELOPING.mdに、すべてのターゲットとコードの構成が載っています。

うまくいかないときは

• error: … was not built from the current … Containerfile：ビルドした後で、コンテナの定義が変わっています。メッセージのとおり、make containerをもう一度実行してください。
• Podmanに接続できない：macOSでは、podman machine startで仮想マシンを起動してください。
• ビルド中にメモリが足りなくなる：Podmanの仮想マシンに、もっとメモリを割り当ててください。ゲート全体であるmake ciは、デモよりはるかに多くのメモリを必要とするモデル検査の証明を実行します（チェックと根拠）。