rajames/LithosAnanake
0
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

build: init downloads syft and Isabelle/HOL, checked by SHA-256

Browse Source 
Neither is packaged. make ARCH=<arch> init now downloads both to
build/cache/downloads, checks each archive's SHA-256, unpacks it into
build/cache/tools (both kept by make clean) and links it into
/usr/local/bin:

- syft 1.52.0, the version sbom.spdx was made with (make sbom,
  boot_image); sums from the release's checksums.txt;
- Isabelle2025-2, the version proof/COVERAGE.md names (isabelle build
  -D proof/), from the release's own site (the /dist mirror answered
  503); Isabelle publishes no sums, so these are of the archives as
  downloaded on 2026-11-06.

An archive already there with the right sum is not downloaded again;
a download with the wrong sum is deleted and init stops. The host's
build is chosen by uname -m (amd64 or arm64).

Checked on Ubuntu 24.04 (x86_64): both fetched, checked and run (syft
1.52.0, Isabelle2025-2); a wrong sum is refused and deleted; isabelle
build -n -D proof/ finds the StarForth session.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2
This commit is contained in:
rajames
2026-11-06 01:25:47 +00:00
co-authored by Claude Opus 5.5
parent d8e3fa81eb
commit 4cef0431bf
1 changed files with 53 additions and 5 deletions
Download Patch File Download Diff File Expand all files Collapse all files
Makefile
+53 -5
View File
@@ -40,7 +40,10 @@
# boot it in QEMU and build the documents # boot it in QEMU and build the documents
# (Debian/Ubuntu, apt-get; sudo if not root). # (Debian/Ubuntu, apt-get; sudo if not root).
# ARCH=amd64,aarch64,riscv64 sets up all # ARCH=amd64,aarch64,riscv64 sets up all
# three, for the full acceptance # 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)
# make <other goal> goes to v3/Makefile (make help-hosted) # make <other goal> goes to v3/Makefile (make help-hosted)
# ============================================================================== # ==============================================================================
@@ -242,9 +245,14 @@ write_stick:
# the logs and DoE CSVs (.gitattributes), and the documents: the book (docs/book/Makefile's own # 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). # 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 # 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 installed: syft, which make sbom and # TOOLCHAIN; aarch64's loader is clang + lld-link).
# boot_image need -- it is not packaged; see the message make sbom prints. # Not packaged, so downloaded, checked against the SHA-256 below and installed: syft (make sbom,
INIT_COMMON := build-essential make git git-lfs python3 xorriso mtools gdisk dosfstools fdisk \ # 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_COMMON := build-essential make git git-lfs python3 curl ca-certificates xorriso mtools gdisk dosfstools fdisk \
pandoc latexmk texlive-xetex texlive-latex-base texlive-latex-recommended \ pandoc latexmk texlive-xetex texlive-latex-base texlive-latex-recommended \
texlive-latex-extra texlive-pictures texlive-fonts-recommended lmodern \ texlive-latex-extra texlive-pictures texlive-fonts-recommended lmodern \
fonts-dejavu fonts-dejavu-extra doxygen graphviz fonts-dejavu fonts-dejavu-extra doxygen graphviz
@@ -256,6 +264,36 @@ INIT_ARCHES := $(subst $(comma),$(space),$(ARCH))
INIT_BAD := $(filter-out amd64 aarch64 riscv64,$(INIT_ARCHES)) INIT_BAD := $(filter-out amd64 aarch64 riscv64,$(INIT_ARCHES))
SUDO := $(if $(filter 0,$(shell id -u)),,sudo) 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: init:
@[ -n "$(INIT_ARCHES)" ] && [ -z "$(INIT_BAD)" ] || { \ @[ -n "$(INIT_ARCHES)" ] && [ -z "$(INIT_BAD)" ] || { \
echo "Usage: make ARCH=<amd64|aarch64|riscv64>[,...] init (e.g. ARCH=amd64,aarch64,riscv64)"; exit 1; } echo "Usage: make ARCH=<amd64|aarch64|riscv64>[,...] init (e.g. ARCH=amd64,aarch64,riscv64)"; exit 1; }
@@ -265,8 +303,18 @@ init:
$(SUDO) env DEBIAN_FRONTEND=noninteractive apt-get install -y -qq \ $(SUDO) env DEBIAN_FRONTEND=noninteractive apt-get install -y -qq \
$(INIT_COMMON) $(foreach a,$(INIT_ARCHES),$(INIT_$(a))) $(INIT_COMMON) $(foreach a,$(INIT_ARCHES),$(INIT_$(a)))
git lfs install --local git lfs install --local
$(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
$(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
@syft version | sed -n 's/^Version: */ syft /p'
@echo " isabelle $$(isabelle version)"
@echo "" @echo ""
@echo "Ready for $(INIT_ARCHES): make ARCH=<arch> clean qemu, make -C v4 test, make docs" @echo "Ready for $(INIT_ARCHES): make ARCH=<arch> clean qemu, make -C v4 test, make docs,"
@echo " make sbom, isabelle build -D proof/"
help: help:
@sed -n '/^# TARGET is/,/^# =====/p' Makefile | sed '$$d; s/^# \{0,1\}//' @sed -n '/^# TARGET is/,/^# =====/p' Makefile | sed '$$d; s/^# \{0,1\}//'