# ============================================================================== # LithosAnanke / StarForth -- top-level Makefile # # Thin dispatcher. The real build lives in: # v3/Makefile -- hosted StarForth v3 (Linux userland VM, POST, DoE) # kernel/Makefile -- LithosAnanke kernel (UEFI loader, kernel ELF, QEMU) # boards// -- one directory per physical target (board.mk + boot files) # docs/book/Makefile -- the single LaTeX book (build/docs/*.pdf) # Every sub-make runs from this directory, so paths are always repo-relative. # # TARGET is either a board (PC RASPI MILKV ZYNQ7020), a hosted v3 profile # (standard fast fastest turbo asan ...), or empty: # # make [all] every board that has a kernel port, the # hosted v3 build, and the book # make [all] TARGET= that board's boot image + its book # make [all] TARGET= hosted v3 build with that profile # # make boot_image TARGET= only the board's boot image, with its SBOM # (build/boards//*.spdx*) and a fresh # source SBOM -- needs syft # make boot_images every board that has a kernel port # make write_stick DEVICE=/dev/sdX write the PC stick image to a USB stick, checked # first, read back and compared after # (scripts/write_stick.sh; Linux, sudo) # make docs [TARGET=] the book; a board adds its appendix # # make clean all of build/ except build/cache/ # make clean TARGET= the board's image + book and its ISA's kernel objects # make clean TARGET= build// for every arch # make clean-docs build/docs/ # # make sbom SPDX SBOM of the source tree (sbom.spdx, sbom.spdx.json) # make kernel ARCH= [GOAL=g] kernel/Makefile goal (default: all) # make ARCH= clean qemu the kernel for (amd64 aarch64 riscv64), # cleaned, built and booted in QEMU: the # acceptance boot (.claude/CLAUDE.md) # make boards list boards and whether they can be built # make ARCH= init install everything needed to build , # boot it in QEMU and build the documents # (Debian/Ubuntu, apt-get; sudo if not root). # ARCH=amd64,aarch64,riscv64 sets up all # three, for the full acceptance. syft and # Isabelle/HOL, not packaged, are downloaded, # checked by SHA-256 and linked into # /usr/local/bin (build/cache/tools). # INIT_DOCS=0: without the documents' tools # (TeX, Doxygen); INIT_PROOFS=0: without # Isabelle # scripts/nightly.sh the nightly and release builds: acceptance, # proofs, board images, documents, Nexus # (stages: the script's header) # make goes to v3/Makefile (make help-hosted) # ============================================================================== # Board name (as typed on the command line) -> boards/ directory. BOARD_DIR_PC := pc BOARD_DIR_RASPI := raspi BOARD_DIR_MILKV := milkv BOARD_DIR_ZYNQ7020 := zynq7020 BOARDS := PC RASPI MILKV ZYNQ7020 empty := space := $(empty) $(empty) board_field = $(if $(BOARD_DIR_$(1)),$(shell sed -n 's/^$(2) *:= *//p' boards/$(BOARD_DIR_$(1))/board.mk)) board_arch = $(call board_field,$(1),BOARD_ARCH) # A board can be built once its ISA's kernel port exists. board_ready = $(if $(call board_arch,$(1)),$(wildcard kernel/src/arch/$(call board_arch,$(1))/.)) READY_BOARDS := $(foreach b,$(BOARDS),$(if $(call board_ready,$(b)),$(b))) UNREADY_BOARDS := $(filter-out $(READY_BOARDS),$(BOARDS)) TARGET := $(strip $(TARGET)) BOARD_DIR := $(if $(TARGET),$(BOARD_DIR_$(TARGET))) SUBMAKE := $(MAKE) --no-print-directory .DEFAULT_GOAL := all .PHONY: all boot_image boot_images write_stick docs clean clean-docs kernel boards help help-hosted sbom sbom-board \ qemu qemu-esp qemu-gdb init # ARCH given on the command line and no TARGET: `clean` is the kernel's for that # ISA, as `qemu` always is (make ARCH= clean qemu). KERNEL_CLEAN := $(if $(TARGET),,$(filter command line,$(origin ARCH))) # ------------------------------------------------------------------------------ # all # ------------------------------------------------------------------------------ ifeq ($(TARGET),) all: @for b in $(READY_BOARDS); do \ $(SUBMAKE) boot_image TARGET=$$b || exit 1; \ done @$(SUBMAKE) -f v3/Makefile all @$(SUBMAKE) docs @echo "" @echo "Built:" @for b in $(READY_BOARDS); do \ d=$$(echo $$b | tr A-Z a-z); ls build/boards/$$d/*.img | sed 's/^/ /'; \ done @echo " build/docs/LithosAnanke.pdf" @$(foreach b,$(UNREADY_BOARDS),echo "Skipped $(b): needs kernel/src/arch/$(call board_arch,$(b)), which does not exist yet";) else ifneq ($(BOARD_DIR),) all: @$(SUBMAKE) boot_image TARGET=$(TARGET) @$(SUBMAKE) docs TARGET=$(TARGET) else all: @$(SUBMAKE) -f v3/Makefile all TARGET=$(TARGET) endif # ------------------------------------------------------------------------------ # boot images # ------------------------------------------------------------------------------ boot_image: @if [ -z "$(BOARD_DIR)" ]; then \ echo "Usage: make boot_image TARGET=<$(subst $(space),|,$(BOARDS))>"; \ [ -z "$(TARGET)" ] || echo "Unknown board TARGET='$(TARGET)'"; \ exit 1; \ fi @if [ -z "$(call board_ready,$(TARGET))" ]; then \ echo "Error: $(TARGET) needs the $(call board_arch,$(TARGET)) kernel port (kernel/src/arch/$(call board_arch,$(TARGET))), which does not exist yet."; \ echo " $(call board_field,$(TARGET),BOARD_DESC)"; \ exit 1; \ fi @# Both systems in one image, v4 unless the boot arguments say system=v3 @# (boards/BRINGUP.md A6, ruled 2026-10-14; v4 the default, same day). A clean build every time: the @# kernel objects are shared with `make qemu`, and make does not see a @# change of compile flags -- an image could otherwise carry objects built @# without v4, or without the bring-up console. @$(SUBMAKE) -f kernel/Makefile ARCH=$(call board_arch,$(TARGET)) TARGET=kernel clean @$(SUBMAKE) -f kernel/Makefile \ BOARD=$(BOARD_DIR) ARCH=$(call board_arch,$(TARGET)) TARGET=kernel \ STARFORTH_V4=1 V4_DEFAULT=1 boot_image @# Its SBOM, and the source tree's, are part of the build (2026-10-14). @$(SUBMAKE) sbom-board TARGET=$(TARGET) @$(SUBMAKE) sbom boot_images: @for b in $(READY_BOARDS); do \ $(SUBMAKE) boot_image TARGET=$$b || exit 1; \ done @$(foreach b,$(UNREADY_BOARDS),echo "Skipped $(b): needs kernel/src/arch/$(call board_arch,$(b)), which does not exist yet";) # ------------------------------------------------------------------------------ # SBOMs (SPDX 2.3, by syft; config mk/syft.yaml) -- part of every board build # ------------------------------------------------------------------------------ # The source SBOM covers what the product is built from: the tracked files of # the kernel, v3, v4, capsules, boards, build tooling and proofs, each with its # SHA-256 -- copied to build/sbom/src first, so nothing untracked in the # working directory is ever swept in. Not logs, documents, experiment data or # the disk images. A board's SBOM covers # its image and every file on it, copied off the image, so the SBOM is of what # is on the medium, not of what was meant to be. Versioned as the kernel # version and the commit. No syft: the build stops, as for any missing tool. SYFT ?= syft SBOM_VERSION = $(shell sed -n 's/^LITHOS_VERSION *?= *//p' kernel/Makefile)+$(shell git describe --always --dirty 2>/dev/null) # What the product is built from: tracked files only, in these places (never # untracked or ignored files in the working directory). SBOM_SOURCES := kernel v3 v4 capsules boards mk tools scripts proof configs \ Makefile Kconfig Kconfig.arch Kconfig.heartbeat Kconfig.kernel \ Kconfig.physics Kconfig.variant LICENSE NOTICE.md GIT_PLAIN := git -c filter.lfs.process= -c filter.lfs.smudge=cat -c filter.lfs.required=false define need_syft @command -v $(SYFT) >/dev/null 2>&1 || { \ echo "Error: syft not found -- the SBOM is part of this build."; \ echo " Install a release from https://github.com/anchore/syft/releases"; \ echo " (verify it against the release's checksums), or SYFT=/path/to/syft."; exit 1; } endef sbom: $(need_syft) @echo " SBOM source tree -> sbom.spdx, sbom.spdx.json ($(SBOM_VERSION))" @rm -rf build/sbom/src && mkdir -p build/sbom/src && \ $(GIT_PLAIN) ls-files -z -- $(SBOM_SOURCES) | xargs -0 cp --parents -t build/sbom/src && \ $(SYFT) -q -c mk/syft.yaml dir:build/sbom/src \ --source-name LithosAnanke --source-version "$(SBOM_VERSION)" \ -o spdx-json=sbom.spdx.json -o spdx=sbom.spdx sbom-board: $(need_syft) @if [ -z "$(BOARD_DIR)" ]; then echo "Usage: make sbom-board TARGET=<$(subst $(space),|,$(BOARDS))>"; exit 1; fi @img=build/boards/$(BOARD_DIR)/$(call board_field,$(TARGET),BOARD_IMAGE); \ if [ ! -f "$$img" ]; then echo "Error: $$img not built (make boot_image TARGET=$(TARGET))"; exit 1; fi; \ rm -rf build/boards/$(BOARD_DIR)/contents && mkdir -p build/boards/$(BOARD_DIR)/contents && \ mcopy -s -n -i "$$img@@1M" '::/*' build/boards/$(BOARD_DIR)/contents/ && \ echo " SBOM $$img -> $${img%.img}.spdx, $${img%.img}.spdx.json" && \ $(SYFT) -q -c mk/syft.yaml dir:build/boards/$(BOARD_DIR) \ --exclude './*.spdx' --exclude './*.spdx.json' \ --source-name "LithosAnanke-$(BOARD_DIR)" --source-version "$(SBOM_VERSION)" \ -o spdx-json=$${img%.img}.spdx.json -o spdx=$${img%.img}.spdx # ------------------------------------------------------------------------------ # docs # ------------------------------------------------------------------------------ docs: @if [ -n "$(TARGET)" ] && [ -z "$(BOARD_DIR)" ]; then \ echo "Error: make docs takes TARGET=<$(subst $(space),|,$(BOARDS))> or no TARGET; '$(TARGET)' is not a board."; \ exit 1; \ fi @$(SUBMAKE) -f docs/book/Makefile BOARD=$(BOARD_DIR) BOARD_NAME=$(TARGET) clean-docs: rm -rf build/docs # ------------------------------------------------------------------------------ # clean # ------------------------------------------------------------------------------ ifneq ($(KERNEL_CLEAN),) clean: @$(SUBMAKE) -f kernel/Makefile ARCH=$(ARCH) clean else ifeq ($(TARGET),) clean: @if [ -d build ]; then find build -mindepth 1 -maxdepth 1 ! -name cache -exec rm -rf {} +; fi rm -f v3/include/version.h rm -f v3/src/*.gcda v3/src/*.gcno v3/src/word_source/*.gcda v3/src/word_source/*.gcno @echo "Cleaned build/ (kept build/cache/)" else ifneq ($(BOARD_DIR),) clean: rm -rf build/boards/$(BOARD_DIR) build/$(call board_arch,$(TARGET))/kernel build/docs/$(BOARD_DIR) \ build/docs/LithosAnanke-$(BOARD_DIR).pdf else clean: rm -rf build/*/$(TARGET) endif # ------------------------------------------------------------------------------ # misc # ------------------------------------------------------------------------------ GOAL ?= all kernel: @$(SUBMAKE) -f kernel/Makefile TARGET=kernel $(GOAL) qemu qemu-esp qemu-gdb: @$(SUBMAKE) -f kernel/Makefile $(if $(ARCH),ARCH=$(ARCH)) $@ boards: @$(foreach b,$(BOARDS),printf ' %-9s %-8s %s\n' "$(b)" \ "$(if $(call board_ready,$(b)),ready,no port)" "$(call board_field,$(b),BOARD_DESC)";) # write_stick -- the PC stick image (make boot_image TARGET=PC) onto a USB stick, safely: # scripts/write_stick.sh refuses anything but a whole, removable, unmounted USB disk big enough, # asks for the device to be typed back, writes, flushes, reads back and compares. write_stick: @[ -n "$(DEVICE)" ] || { echo "Usage: make write_stick DEVICE=/dev/sdX (lsblk lists the disks)"; exit 1; } @bash scripts/write_stick.sh build/boards/pc/lithos-pc.img $(DEVICE) # init -- the packages this tree needs, for one ISA or several (ARCH=amd64,aarch64,riscv64). # Common: the build, the disk images (scripts/mkdiskimage.sh; sfdisk is in fdisk), git-lfs for # the logs and DoE CSVs (.gitattributes), and the documents: the book (docs/book/Makefile's own # list) and the formal volumes and API reference (docs/formal/Makefile: pdflatex, doxygen, dot). # Per ISA: its QEMU, its UEFI firmware (kernel/Makefile's paths) and its compiler (kernel/Makefile # TOOLCHAIN; aarch64's loader is clang + lld-link). # Not packaged, so downloaded, checked against the SHA-256 below and installed: syft (make sbom, # boot_image; the version sbom.spdx was made with) and Isabelle/HOL (isabelle build -D proof/; # the version proof/COVERAGE.md names). The archives are kept in build/cache/downloads and the # tools in build/cache/tools, which make clean keeps; each is linked into /usr/local/bin. syft's # sums are its release's checksums.txt; Isabelle publishes none, so its sums are of the archives # as downloaded on 2026-11-06 -- a download that differs is refused. # INIT_DOCS=0 leaves out what only the documents need (the TeX and Doxygen packages), and # INIT_PROOFS=0 what only the proofs need (Isabelle): the nightly build of the images takes the # first, the nightly documents the second (scripts/nightly.sh). INIT_DOCS ?= 1 INIT_PROOFS ?= 1 INIT_COMMON := build-essential make git git-lfs python3 curl ca-certificates xz-utils \ xorriso mtools gdisk dosfstools fdisk INIT_DOCPKGS := pandoc latexmk texlive-xetex texlive-latex-base texlive-latex-recommended \ texlive-latex-extra texlive-pictures texlive-fonts-recommended lmodern \ fonts-dejavu fonts-dejavu-extra doxygen graphviz INIT_amd64 := qemu-system-x86 ovmf INIT_aarch64 := qemu-system-arm qemu-efi-aarch64 gcc-aarch64-linux-gnu binutils-aarch64-linux-gnu clang lld INIT_riscv64 := qemu-system-misc qemu-efi-riscv64 gcc-riscv64-linux-gnu binutils-riscv64-linux-gnu comma := , INIT_ARCHES := $(subst $(comma),$(space),$(ARCH)) INIT_BAD := $(filter-out amd64 aarch64 riscv64,$(INIT_ARCHES)) SUDO := $(if $(filter 0,$(shell id -u)),,sudo) # The host the tools run on, not the ISA being built for: syft's and Isabelle's names for it. INIT_HOST := $(shell uname -m) SYFT_VERSION := 1.52.0 SYFT_ARCH := $(if $(filter aarch64 arm64,$(INIT_HOST)),arm64,amd64) SYFT_TGZ := syft_$(SYFT_VERSION)_linux_$(SYFT_ARCH).tar.gz SYFT_URL := https://github.com/anchore/syft/releases/download/v$(SYFT_VERSION)/$(SYFT_TGZ) SYFT_SHA_amd64 := caeedb81fb0491615f1ebd1761e4145d41ee86dd2cc7bf80669f9f5ad9d6133d SYFT_SHA_arm64 := c46d5e4c28e12aa4c5becfaa343ef1c7f89045b6b895f2c21d471c62db09c706 ISABELLE := Isabelle2025-2 ISABELLE_TGZ := $(ISABELLE)_$(if $(filter aarch64 arm64,$(INIT_HOST)),linux_arm,linux).tar.gz ISABELLE_URL := https://isabelle.in.tum.de/website-$(ISABELLE)/dist/$(ISABELLE_TGZ) ISABELLE_SHA_linux := a20a507bc7c1270d8be96a9f3fbec06345387789d2dc2c4d3df6260d47bfb33c ISABELLE_SHA_linux_arm := 650a9669b4a087675afb34294d82ded2f0704d47d580dd9ed45cddc9f1764bdd INIT_DL := build/cache/downloads INIT_TOOLS := build/cache/tools # $(call fetch,file,url,sha256): the archive in $(INIT_DL), downloaded unless it is there and # its sum is right; a download whose sum is wrong is deleted and the build stops. define fetch @mkdir -p $(INIT_DL) @if ! echo "$(3) $(INIT_DL)/$(1)" | sha256sum -c --status 2>/dev/null; then \ echo " FETCH $(2)"; \ curl -fsSL --retry 3 -o $(INIT_DL)/$(1).part $(2) && mv $(INIT_DL)/$(1).part $(INIT_DL)/$(1); \ echo "$(3) $(INIT_DL)/$(1)" | sha256sum -c --status || { \ echo "init: $(1) does not have the SHA-256 this Makefile expects -- deleted, not installed"; \ rm -f $(INIT_DL)/$(1); exit 1; }; \ fi @echo " OK $(1) (sha256 $(3))" endef init: @[ -n "$(INIT_ARCHES)" ] && [ -z "$(INIT_BAD)" ] || { \ echo "Usage: make ARCH=[,...] init (e.g. ARCH=amd64,aarch64,riscv64)"; exit 1; } @command -v apt-get >/dev/null 2>&1 || { \ echo "init: needs apt-get (Debian/Ubuntu). The packages are listed in the Makefile, at init."; exit 1; } $(SUDO) env DEBIAN_FRONTEND=noninteractive apt-get update -qq $(SUDO) env DEBIAN_FRONTEND=noninteractive apt-get install -y -qq \ $(INIT_COMMON) $(if $(filter 0,$(INIT_DOCS)),,$(INIT_DOCPKGS)) $(foreach a,$(INIT_ARCHES),$(INIT_$(a))) @# the LFS hook for this checkout -- none when init runs outside one (the CI image, ci/runner-image) if git rev-parse --is-inside-work-tree >/dev/null 2>&1; then git lfs install --local; fi $(call fetch,$(SYFT_TGZ),$(SYFT_URL),$(SYFT_SHA_$(SYFT_ARCH))) @mkdir -p $(INIT_TOOLS)/syft-$(SYFT_VERSION) tar -xzf $(INIT_DL)/$(SYFT_TGZ) -C $(INIT_TOOLS)/syft-$(SYFT_VERSION) syft $(SUDO) ln -sf $(abspath $(INIT_TOOLS))/syft-$(SYFT_VERSION)/syft /usr/local/bin/syft @syft version | sed -n 's/^Version: */ syft /p' ifneq ($(INIT_PROOFS),0) $(call fetch,$(ISABELLE_TGZ),$(ISABELLE_URL),$(ISABELLE_SHA_$(patsubst $(ISABELLE)_%.tar.gz,%,$(ISABELLE_TGZ)))) @[ -x $(INIT_TOOLS)/$(ISABELLE)/bin/isabelle ] || { mkdir -p $(INIT_TOOLS) && tar -xzf $(INIT_DL)/$(ISABELLE_TGZ) -C $(INIT_TOOLS); } $(SUDO) ln -sf $(abspath $(INIT_TOOLS))/$(ISABELLE)/bin/isabelle /usr/local/bin/isabelle @echo " isabelle $$(isabelle version)" endif @echo "" @echo "Ready for $(INIT_ARCHES): make ARCH= clean qemu, make -C v4 test, make sbom" \ "$(if $(filter 0,$(INIT_DOCS)),,make docs) $(if $(filter 0,$(INIT_PROOFS)),,isabelle build -D proof/)" help: @sed -n '/^# TARGET is/,/^# =====/p' Makefile | sed '$$d; s/^# \{0,1\}//' help-hosted: @$(SUBMAKE) -f v3/Makefile help # Everything else is the hosted v3 build, unchanged. (The empty Makefile # rule stops the match-anything rule from trying to remake this file.) Makefile: ; %: @$(SUBMAKE) -f v3/Makefile $@