Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Building and Running: fire build / fire run

fire build compiles a project to a bootable Microkit image; fire run builds and then launches it as configured in fire.toml — mimicking the cargo tools.

🚧 The build / run subcommands land with PR #174. On earlier versions the same behaviour is the bare fire <PROJECT_DIR> invocation.

Usage

fire build [PROJECT_DIR] [-o <IMG>]   # produce the image only
fire run   [PROJECT_DIR] [-o <IMG>]   # build, then launch
Argument / flagDescription
PROJECT_DIRDirectory containing fire.toml. Defaults to the current directory.
-o, --output <IMG>Override the output .img path (default: <src>/build/<name>.img).

What it does

  1. Reads fire.toml from PROJECT_DIR and resolves the source directory (project.src).
  2. Builds the image — incrementally, like cargo: when build/<name>.img is already newer than every source file and fire.toml, the rebuild is skipped (✓ image up to date). Otherwise it invokes fic <src> --board <board> --build-profile <profile> (image generation is fic’s default mode), with the toolchain from [run.target] (or the MICROKIT_SDK / GCC / LD environment). This compiles each PD’s C file, patches the mapping setvars, and packs the loader, seL4 kernel, and PD ELFs into build/<name>.img. The freshness check is mtime-based — coarser than cargo’s fingerprints, but any source edit triggers a rebuild.
  3. (fire run only) In mode = "qemu", launches qemu-system-aarch64 with the [run] args, substituting {img} with the built image path. mode = "hardware" is reserved and not yet implemented.

Walkthrough: the data-diode demo

$ fire run demo/datadiode/
fire: building datadiode for qemu_virt_aarch64 (debug)
  ✓ Parsed 1 system + 3 program files
  ✓ Resolved data layer (2 structs, 1 consts)
  ✓ Resolved names
  ✓ Resolved mapping vaddrs
  ✓ Type-checked information flow
  ✓ Checked channel dependency acyclicity (WF2)
MICROKIT|CAPDL SPEC: number of root objects = 84, spec footprint = 12.44 KiB
MICROKIT|INITIAL TASK: memory size = 412 KiB
MICROKIT|LOADER: image file size = 2.59 MiB
fire: launching QEMU ...

QEMU then boots the image; with -serial mon:stdio the PDs’ serial output appears in your terminal. Exit QEMU with Ctrl-A x.

To produce the image without launching:

fire build demo/datadiode/
ls demo/datadiode/build/datadiode.img

A Microkit build report is written next to the image at build/report.txt — useful for inspecting the memory layout and the setvar patches applied to each PD.

Troubleshooting

SymptomLikely cause / fix
could not read .../fire.tomlPROJECT_DIR doesn’t contain a manifest; pass the project directory, not the repo root.
Could not read MICROKIT_SDK environment variableSet $MICROKIT_SDK or [run.target] sdk. Same pattern for GCC / LD.
board path '...' does not exist[run.target] board/profile doesn’t match a directory under <sdk>/board/.
fic: command not foundInstall fic on PATH or set $FIRE_FIC to the binary.
could not patch symbol '...' ... no symbol named '...'A channel declared in the .fis has no matching uint64_t <chan>; symbol in the PD’s C file. Mapping symbols (<mapping>_vaddr …) are emitted only when declared, but channel-ID symbols are required.
WF2 violation: channel dependency graph contains a cycleThe topology is cyclic. Either restructure the channels, or establish deadlock-freedom with fire verify and set allow_wf2_cycles = true in [run.target].
C compile errorsfic compiles each <pd>.c with -Wall -Werror; fix the warning or build the file out-of-band.
QEMU exits immediatelyCheck the [run] args device/loader address against the board; the demo uses addr=0x70000000 for qemu_virt_aarch64.