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=dockera cada comandomake. - 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. Rodemake containerde 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).