NoWayOS
PT
GitHub
MenuFechar

Comece aqui

Primeiros passos

Monte o contêiner de desenvolvimento do NoWayOS e rode a sua demo clicável, com cada quadro verificado, sem precisar de hardware nem de conhecimento de seL4.

O NoWayOS é compilado dentro de um único contêiner de desenvolvimento com versões fixadas, então a sua máquina precisa de muito pouco por conta própria. Esta página leva você do zero até a demo rodando. A próxima página inicializa um sistema seL4 de verdade no QEMU, e uma página mais adiante o coloca num Raspberry Pi 5.

Do que você precisa

  • Podman e GNU Make. Docker também funciona: acrescente ENGINE=docker a cada comando make.
  • git, para clonar os repositórios.
  • Nada de Rust nem de ferramentas do seL4 na sua máquina. Os toolchains de Rust, o SDK do Microkit e o QEMU estão todos dentro do contêiner de desenvolvimento, fixados em versões exatas.

No macOS, o Podman roda contêineres numa máquina virtual. Crie-a e inicie-a uma vez, com algumas CPUs e vários gigabytes de memória, por exemplo:

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

O NoWayOS é desenvolvido em Apple silicon (arm64). Em x86-64, os pacotes da imagem de desenvolvimento também são fixados e revisados, mas a imagem ainda não foi compilada e testada de ponta a ponta nessa arquitetura.

Dê ao NoWayOS uma pasta só dele

O contêiner de desenvolvimento monta a pasta acima do seu clone, para que repositórios clonados lado a lado possam usar uns aos outros na compilação. Crie primeiro uma pasta para eles:

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

Monte o contêiner de desenvolvimento

make container

Isso monta a imagem de desenvolvimento com versões fixadas: os toolchains de Rust, o SDK do Microkit, o QEMU e as ferramentas de verificação. O primeiro build leva alguns minutos (menos de quatro num Mac com Apple silicon) e gera uma imagem de cerca de 4,7 GB. Rode de novo sempre que tools/container/Containerfile mudar; todos os outros alvos se recusam a rodar sobre uma imagem desatualizada e avisam você disso.

Rode a demo

make demo

A demo é uma pequena aplicação de formulário com uma sessão roteirizada de toques, cliques e teclas. Ela roda como uma simulação no host, sem seL4 e sem QEMU, e desenha o quadro de cada passo com o núcleo de UI e o renderizador reais do NoWayOS. Cada quadro é comparado com uma imagem aprovada, e a execução termina assim:

demo: PASS - … steps, every frame as approved

Se qualquer quadro diferir em um único pixel, a execução diz em qual passo e falha.

Dê uma olhada

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

Todo alvo roda no contêiner de desenvolvimento e o inicia para você. O DEVELOPING.md do repositório lista todos eles, com a organização do código.

Se algo der errado

  • error: … was not built from the current … Containerfile: a definição do contêiner mudou desde que você o montou. Rode make container de novo, como diz a mensagem.
  • O Podman não pode ser acessado: no macOS, inicie a máquina virtual dele com podman machine start.
  • Um build fica sem memória: dê mais memória à máquina virtual do Podman. A bateria completa de verificações, make ci, executa provas de model checking que precisam de muito mais do que a demo (Verificações e evidências).