diff --git a/.gitea/workflows/nightly-docs.yml b/.gitea/workflows/nightly-docs.yml new file mode 100644 index 00000000..8abc0360 --- /dev/null +++ b/.gitea/workflows/nightly-docs.yml @@ -0,0 +1,47 @@ +# Nightly snapshot of the documents: the book, the formal volumes and the API reference +# (scripts/nightly.sh docs), then Nexus. +# +# org.starship:documentation:-SNAPSHOT, starshipos-snapshots +# classifier book the book (make docs) +# classifier vol1, vol2, vol3 the formal volumes (make -C docs/formal vols) +# classifier api the API reference (make -C docs/formal doxygen) +# +# Gitea runs a schedule from the default branch. Until StarForth-v4.0.0 is merged to master, +# master carries a copy of this file whose checkout names that branch. +name: Nightly documents + +on: + schedule: + - cron: '0 4 * * *' # 04:00 UTC, after the images (nightly.yml, 03:00) + workflow_dispatch: + +jobs: + docs: + name: Book, volumes, API reference + runs-on: ubuntu-latest + timeout-minutes: 90 + steps: + - uses: actions/checkout@v4 + with: + fetch-depth: 0 + lfs: false + + - name: Install the documents' dependencies + run: | + make ARCH=amd64 init INIT_PROOFS=0 + DEBIAN_FRONTEND=noninteractive apt-get install -y -qq maven default-jre-headless + + - name: Documents + run: scripts/nightly.sh docs + + - name: Publish to Nexus + env: + NEXUS_USER: ci-publisher + NEXUS_PASSWORD: ${{ secrets.NEXUS_CI_PASSWORD }} + run: scripts/nightly.sh publish-docs https://nexus.starshipos-f18.org/repository/starshipos-snapshots + + - name: Keep the documents + uses: actions/upload-artifact@v3 + with: + name: documents-${{ github.run_number }} + path: build/nightly-docs/ diff --git a/.gitea/workflows/nightly.yml b/.gitea/workflows/nightly.yml new file mode 100644 index 00000000..f7746c0e --- /dev/null +++ b/.gitea/workflows/nightly.yml @@ -0,0 +1,71 @@ +# Nightly snapshot of the kernel images: the acceptance protocol, the proofs, the board images, +# then Nexus. Each stage is a step of scripts/nightly.sh (its header says what each does); any +# failure stops the run, and nothing is published unless every stage before it passed. +# +# org.starship:kernelImage:-SNAPSHOT, starshipos-snapshots +# classifier pc StarshipOS.iso amd64, UEFI -- the ISO the amd64 acceptance boot booted +# classifier raspi5 raspi5.img.xz Raspberry Pi 5, for Raspberry Pi Imager +# classifier milkv MilkV.img.xz Milk-V Mars +# classifier logs logs.tar.gz this run's serial logs, proof log and DoE CSVs +# +# Gitea runs a schedule from the default branch. Until StarForth-v4.0.0 is merged to master, +# master carries a copy of this file whose checkout names that branch. +name: Nightly snapshot + +on: + schedule: + - cron: '0 3 * * *' # 03:00 UTC; the documents are at 04:00 (nightly-docs.yml) + workflow_dispatch: + +jobs: + nightly: + name: Acceptance, proofs, images + runs-on: ubuntu-latest + timeout-minutes: 150 + steps: + - uses: actions/checkout@v4 + with: + fetch-depth: 0 # the SBOM's version is git describe + lfs: false # only the logs and DoE CSVs are in LFS; the build needs neither + + - name: Install the build's dependencies + run: | + make ARCH=amd64,aarch64,riscv64 init INIT_DOCS=0 + DEBIAN_FRONTEND=noninteractive apt-get install -y -qq maven default-jre-headless + + - name: Acceptance amd64 + run: scripts/nightly.sh accept amd64 + - name: Acceptance aarch64 + run: scripts/nightly.sh accept aarch64 + - name: Acceptance riscv64 + run: scripts/nightly.sh accept riscv64 + - name: Acceptance PC stick loaded high + run: scripts/nightly.sh accept stick-high + - name: Acceptance 32-bit build + run: scripts/nightly.sh test-32 + - name: Isabelle/HOL proofs + run: scripts/nightly.sh proofs + + - name: Images + run: scripts/nightly.sh images + + - name: Publish to Nexus + env: + NEXUS_USER: ci-publisher + NEXUS_PASSWORD: ${{ secrets.NEXUS_CI_PASSWORD }} + run: scripts/nightly.sh publish https://nexus.starshipos-f18.org/repository/starshipos-snapshots + + - name: Keep the images + uses: actions/upload-artifact@v3 + with: + name: kernel-images-${{ github.run_number }} + path: build/nightly/ + + - name: Keep the logs and DoE CSVs + if: always() + uses: actions/upload-artifact@v3 + with: + name: logs-${{ github.run_number }} + path: | + logs/ + experiments/bare_metal/runs/ diff --git a/.gitea/workflows/release.yml b/.gitea/workflows/release.yml new file mode 100644 index 00000000..f195f0e9 --- /dev/null +++ b/.gitea/workflows/release.yml @@ -0,0 +1,79 @@ +# A release: pushing a tag v builds that commit exactly as the nightly does -- the +# acceptance protocol, the proofs, the board images -- and the documents, and publishes both to +# starshipos-releases at that version: +# +# org.starship:kernelImage: classifiers pc, raspi5, milkv, logs (nightly.yml) +# org.starship:documentation: classifiers book, vol1, vol2, vol3, api (nightly-docs.yml) +# +# The tag must name the version the tree says it is: v (kernel/Makefile). A tag +# that does not is refused before anything is built. A release repository takes a version once. +name: Release + +on: + push: + tags: ['v*'] + +jobs: + release: + name: Release ${{ github.ref_name }} + runs-on: ubuntu-latest + timeout-minutes: 240 + steps: + - uses: actions/checkout@v4 + with: + fetch-depth: 0 + lfs: false + + - name: The tag names the tree's version + run: | + tree="v$(sed -n 's/^LITHOS_VERSION *?= *//p' kernel/Makefile)" + echo "tag ${{ github.ref_name }}, kernel/Makefile LITHOS_VERSION -> $tree" + [ "${{ github.ref_name }}" = "$tree" ] || { echo "The tag must be $tree, or LITHOS_VERSION changed first."; exit 1; } + echo "NIGHTLY_VERSION=${tree#v}" >> "$GITHUB_ENV" + + - name: Install the dependencies + run: | + make ARCH=amd64,aarch64,riscv64 init + DEBIAN_FRONTEND=noninteractive apt-get install -y -qq maven default-jre-headless + + - name: Acceptance amd64 + run: scripts/nightly.sh accept amd64 + - name: Acceptance aarch64 + run: scripts/nightly.sh accept aarch64 + - name: Acceptance riscv64 + run: scripts/nightly.sh accept riscv64 + - name: Acceptance PC stick loaded high + run: scripts/nightly.sh accept stick-high + - name: Acceptance 32-bit build + run: scripts/nightly.sh test-32 + - name: Isabelle/HOL proofs + run: scripts/nightly.sh proofs + - name: Images + run: scripts/nightly.sh images + - name: Documents + run: scripts/nightly.sh docs + + - name: Publish to Nexus + env: + NEXUS_USER: ci-publisher + NEXUS_PASSWORD: ${{ secrets.NEXUS_CI_PASSWORD }} + run: | + scripts/nightly.sh publish https://nexus.starshipos-f18.org/repository/starshipos-releases + scripts/nightly.sh publish-docs https://nexus.starshipos-f18.org/repository/starshipos-releases + + - name: Keep the release + uses: actions/upload-artifact@v3 + with: + name: release-${{ github.ref_name }} + path: | + build/nightly/ + build/nightly-docs/ + + - name: Keep the logs and DoE CSVs + if: always() + uses: actions/upload-artifact@v3 + with: + name: release-logs-${{ github.ref_name }} + path: | + logs/ + experiments/bare_metal/runs/ diff --git a/Makefile b/Makefile index 67f1eff9..d9afdf7b 100644 --- a/Makefile +++ b/Makefile @@ -44,11 +44,12 @@ # 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' and -# proofs' tools (TeX, Doxygen, Isabelle) -# scripts/nightly.sh boot | images | publish -# the nightly snapshot: boot-check, the -# board images, and Nexus +# 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) # ============================================================================== @@ -257,9 +258,11 @@ write_stick: # 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 and the proofs need (the TeX and Doxygen -# packages, and Isabelle): what a build of the images needs, as the nightly (scripts/nightly.sh). +# 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 \ @@ -317,19 +320,15 @@ init: 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_DOCS),0) +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)" - @echo "" - @echo "Ready for $(INIT_ARCHES): make ARCH= clean qemu, make -C v4 test, make docs," - @echo " make sbom, isabelle build -D proof/" -else - @echo "" - @echo "Ready for $(INIT_ARCHES), without the documents' and proofs' tools: make ARCH= clean qemu," - @echo " make boot_image TARGET=, make sbom" 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\}//' diff --git a/scripts/nightly.sh b/scripts/nightly.sh index 8d6a6b6c..a749fc85 100755 --- a/scripts/nightly.sh +++ b/scripts/nightly.sh @@ -1,49 +1,127 @@ #!/bin/bash -# nightly.sh -- the nightly snapshot: boot-check each ISA, build the board images, publish them. -# Three stages, run in this order (.gitea/workflows/nightly.yml runs each as a step): +# nightly.sh -- the nightly and release builds: the acceptance protocol, the proofs, the board +# images, the documents, and Nexus. One stage per call; the workflows run each as a step +# (.gitea/workflows/nightly.yml, release.yml, nightly-docs.yml). # -# scripts/nightly.sh boot -# Boots that ISA headless in QEMU (scripts/qemu_session.py headless: POST: PASSED, and no -# prompt with no Zuse drive), in the foreground; one QEMU at a time, the acceptance order -# amd64, aarch64, riscv64. A failure ends the nightly. amd64 also keeps the ISO it booted, -# byte for byte, as build/nightly/StarshipOS.iso. +# The images, in this order (any failure ends the run; nothing is published after it): +# +# scripts/nightly.sh accept +# One boot of the acceptance protocol (.claude/CLAUDE.md), in the foreground, one QEMU at a +# time, in that order: scripts/qemu_session.py zuse -- [zuse@Hera] ok>, `3 4 + .` +# -> 7 ok, POST passed -- or stick_zuse amd64 --target qemu-stick-high, the PC stick loaded +# above 2 GiB. amd64 keeps the ISO it booted, byte for byte, as build/nightly/StarshipOS.iso. +# The last of the four (stick-high) also checks PARITY:V4_SYSTEM's dict_hash is the same +# on amd64, aarch64 and riscv64. +# scripts/nightly.sh test-32 +# make -C v4 test-32: v4 with 32-bit cells, every test (the acceptance's last part). +# scripts/nightly.sh proofs +# isabelle build -c -D proof/: the StarForth session checked afresh every run, whatever is +# cached (HOL-Library is reused); its log is logs//isabelle/, as a boot's is. # scripts/nightly.sh images # The board images, into build/nightly/: # raspi5.img.xz Raspberry Pi 5 (make boot_image TARGET=RASPI), for Raspberry Pi Imager # MilkV.img.xz Milk-V Mars (make boot_image TARGET=MILKV) # SHA256SUMS of StarshipOS.iso and both images, before and after compression -# (Imager's extract_sha256 is the uncompressed one) # QEMU boots the aarch64 and riscv64 kernels, not these images: they are built from the # same sources, for hardware QEMU does not model. # scripts/nightly.sh publish -# Deploys the three to a Maven repository (Nexus's starshipos-snapshots) as -# org.starship:kernelImage:-SNAPSHOT, one classifier per board -- -# pc (iso), raspi5 (img.xz), milkv (img.xz) -- in one deploy, so they share a timestamp. -# NEXUS_USER (default ci-publisher) and NEXUS_PASSWORD. Needs mvn and a JRE. +# org.starship:kernelImage: to that Maven repository, in one deploy (one +# timestamp): classifier pc (iso), raspi5 and milkv (img.xz), and logs (tar.gz: this +# run's serial logs, proof log and DoE CSVs -- the evidence for the rest). # -# NIGHTLY_VERSION overrides the version. The serial logs are logs/// and the DoE CSVs -# experiments/bare_metal/runs/, as for any boot (.claude/CLAUDE.md). Needs what -# make ARCH=amd64,aarch64,riscv64 init INIT_DOCS=0 installs. +# The documents (a separate pipeline): +# +# scripts/nightly.sh docs +# The book (make docs), the formal volumes (make -C docs/formal vols) and the API reference +# (make -C docs/formal doxygen), into build/nightly-docs/. +# scripts/nightly.sh publish-docs +# org.starship:documentation:: classifier book, vol1, vol2, vol3, api (pdf). +# +# VERSION is -SNAPSHOT, or NIGHTLY_VERSION when set (a release sets it from its +# tag). NEXUS_USER (default ci-publisher) and NEXUS_PASSWORD; publishing needs mvn and a JRE. +# Needs what make ARCH=amd64,aarch64,riscv64 init installs (INIT_DOCS=0 for the images, +# INIT_PROOFS=0 for the documents). set -euo pipefail cd "$(dirname "$0")/.." OUT=build/nightly +DOCS=build/nightly-docs LITHOS=$(sed -n 's/^LITHOS_VERSION *?= *//p' kernel/Makefile) VERSION=${NIGHTLY_VERSION:-$LITHOS-SNAPSHOT} -usage() { echo "Usage: scripts/nightly.sh boot | images | publish " >&2; exit 2; } +usage() { + echo "Usage: scripts/nightly.sh accept | test-32 | proofs | images" >&2 + echo " | publish | docs | publish-docs " >&2 + exit 2 +} +need() { for f in "$@"; do [ -f "$f" ] || { echo "nightly: no $f -- run the stages before this one" >&2; exit 1; }; done; } + +# deploy
[file ext classifier]... +deploy() { + local url=$1 artifact=$2 file=$3 ext=$4 cls=$5 files= exts= clss= settings + shift 5 + while [ $# -gt 0 ]; do files+=${files:+,}$1; exts+=${exts:+,}$2; clss+=${clss:+,}$3; shift 3; done + : "${NEXUS_PASSWORD:?publishing needs NEXUS_PASSWORD}" + command -v mvn >/dev/null || { echo "nightly: publishing needs mvn (apt-get install maven)" >&2; exit 1; } + settings=$(mktemp) + cat > "$settings" <<'EOF' + + starship-nexus + ${env.NEXUS_USER} + ${env.NEXUS_PASSWORD} + +EOF + export NEXUS_USER=${NEXUS_USER:-ci-publisher} + echo "=== nightly: publish org.starship:$artifact:$VERSION -> $url" + mvn -B -q -s "$settings" org.apache.maven.plugins:maven-deploy-plugin:3.1.2:deploy-file \ + -Durl="$url" -DrepositoryId=starship-nexus \ + -DgroupId=org.starship -DartifactId="$artifact" -Dversion="$VERSION" \ + -Dfile="$file" -Dpackaging="$ext" -Dclassifier="$cls" \ + ${files:+-Dfiles="$files" -Dtypes="$exts" -Dclassifiers="$clss"} -DgeneratePom=true \ + || { rm -f "$settings"; exit 1; } + rm -f "$settings" + echo "=== nightly: published" +} case ${1:-} in -boot) - arch=${2:-} - case $arch in amd64|aarch64|riscv64) ;; *) usage ;; esac - [ "$arch" != amd64 ] || { rm -rf "$OUT"; mkdir -p "$OUT"; } # amd64 is the first stage - echo "=== nightly: org.starship:kernelImage:$VERSION from $(git rev-parse --short HEAD); boot check $arch" - git checkout -q -- disk/zuse-scratch # the committed Zuse pair, as before each acceptance boot - python3 scripts/qemu_session.py headless "$arch" --label "nightly-$arch" --make "QEMU_DISPLAY=none" - [ "$arch" != amd64 ] || cp build/amd64/kernel/starkernel.iso "$OUT/StarshipOS.iso" +accept) + what=${2:-} + case $what in + amd64) rm -rf "$OUT"; mkdir -p "$OUT"; touch "$OUT/.started" # the first stage + mode=zuse; arch=amd64; extra= ;; + aarch64|riscv64) mode=zuse; arch=$what; extra= ;; + stick-high) mode=stick_zuse; arch=amd64; extra="--target qemu-stick-high" ;; + *) usage ;; + esac + need "$OUT/.started" + echo "=== nightly: org.starship:kernelImage:$VERSION from $(git rev-parse --short HEAD); accept $what" + git checkout -q -- disk/zuse-scratch # the committed Zuse pair, before each architecture + python3 scripts/qemu_session.py $mode $arch $extra --label "nightly-$what" --make "QEMU_DISPLAY=none" \ + | tee "$OUT/accept-$what.txt" + [ "$what" != amd64 ] || cp build/amd64/kernel/starkernel.iso "$OUT/StarshipOS.iso" + if [ "$what" = stick-high ]; then + # the three architectures' boots of this run: one dict_hash + hashes=$(for a in amd64 aarch64 riscv64; do + log=$(sed -n 's/^LOG: //p' "$OUT/accept-$a.txt") + grep -aoE "PARITY:V4_SYSTEM [^[:cntrl:]]*" "$log" | sed -n 's/.*dict_hash=//p' + done | sort -u) + echo "=== nightly: dict_hash on the three: $hashes" + [ "$(echo "$hashes" | wc -l)" = 1 ] && [ -n "$hashes" ] \ + || { echo "nightly: the three architectures do not agree on dict_hash" >&2; exit 1; } + fi + ;; +test-32) + need "$OUT/.started" + make --no-print-directory -C v4 test-32 2>&1 | tee "$OUT/test-32.txt" + echo "=== nightly: test-32: $(grep -cE '[0-9]+ checks, 0 failures' "$OUT/test-32.txt") programs, 0 failures" + ;; +proofs) + need "$OUT/.started" + ts=$(date -u +%Y%m%d-%H%M%S) + mkdir -p "logs/$ts/isabelle" + isabelle build -c -v -D proof/ 2>&1 | tee "logs/$ts/isabelle/isabelle-$ts.log" ;; images) - [ -f "$OUT/StarshipOS.iso" ] || { echo "nightly: no $OUT/StarshipOS.iso -- run boot amd64 first" >&2; exit 1; } + need "$OUT/StarshipOS.iso" for b in "RASPI raspi/lithos-raspi.img raspi5.img" "MILKV milkv/lithos-milkv.img MilkV.img"; do set -- $b echo "=== nightly: image $1" @@ -58,31 +136,32 @@ images) (cd "$OUT" && sha256sum raspi5.img.xz MilkV.img.xz >> SHA256SUMS && cat SHA256SUMS) ;; publish) - url=${2:-} - [ -n "$url" ] || usage - : "${NEXUS_PASSWORD:?publish needs NEXUS_PASSWORD}" - command -v mvn >/dev/null || { echo "nightly: publish needs mvn (apt-get install maven)" >&2; exit 1; } - for f in StarshipOS.iso raspi5.img.xz MilkV.img.xz; do - [ -f "$OUT/$f" ] || { echo "nightly: no $OUT/$f -- run boot and images first" >&2; exit 1; } - done - settings=$(mktemp) - trap 'rm -f "$settings"' EXIT - cat > "$settings" <<'EOF' - - starship-nexus - ${env.NEXUS_USER} - ${env.NEXUS_PASSWORD} - -EOF - export NEXUS_USER=${NEXUS_USER:-ci-publisher} - echo "=== nightly: publish org.starship:kernelImage:$VERSION -> $url" - mvn -B -q -s "$settings" org.apache.maven.plugins:maven-deploy-plugin:3.1.2:deploy-file \ - -Durl="$url" -DrepositoryId=starship-nexus \ - -DgroupId=org.starship -DartifactId=kernelImage -Dversion="$VERSION" \ - -Dfile="$OUT/StarshipOS.iso" -Dpackaging=iso -Dclassifier=pc \ - -Dfiles="$OUT/raspi5.img.xz,$OUT/MilkV.img.xz" -Dclassifiers=raspi5,milkv -Dtypes=img.xz,img.xz \ - -DgeneratePom=true - echo "=== nightly: published" + url=${2:-}; [ -n "$url" ] || usage + need "$OUT/StarshipOS.iso" "$OUT/raspi5.img.xz" "$OUT/MilkV.img.xz" + # the evidence: what this run wrote under logs/ and experiments/bare_metal/runs/ + find logs experiments/bare_metal/runs -type f -newer "$OUT/.started" -print0 \ + | tar --null -czf "$OUT/logs.tar.gz" -T - + echo "=== nightly: logs.tar.gz: $(tar -tzf "$OUT/logs.tar.gz" | wc -l) files" + deploy "$url" kernelImage "$OUT/StarshipOS.iso" iso pc \ + "$OUT/raspi5.img.xz" img.xz raspi5 \ + "$OUT/MilkV.img.xz" img.xz milkv \ + "$OUT/logs.tar.gz" tar.gz logs + ;; +docs) + rm -rf "$DOCS"; mkdir -p "$DOCS" + make --no-print-directory docs + make --no-print-directory -C docs/formal vols doxygen + cp build/docs/LithosAnanke.pdf "$DOCS/book.pdf" + for v in 1 2 3; do cp "docs/formal/build/vol$v/main.pdf" "$DOCS/vol$v.pdf"; done + cp docs/formal/build/doxygen/StarForth-API-Reference.pdf "$DOCS/api.pdf" + (cd "$DOCS" && sha256sum ./*.pdf | tee SHA256SUMS) + ;; +publish-docs) + url=${2:-}; [ -n "$url" ] || usage + need "$DOCS/book.pdf" "$DOCS/vol1.pdf" "$DOCS/vol2.pdf" "$DOCS/vol3.pdf" "$DOCS/api.pdf" + deploy "$url" documentation "$DOCS/book.pdf" pdf book \ + "$DOCS/vol1.pdf" pdf vol1 "$DOCS/vol2.pdf" pdf vol2 "$DOCS/vol3.pdf" pdf vol3 \ + "$DOCS/api.pdf" pdf api ;; *) usage ;; esac