rajames/LithosAnanke
1
1
Fork 0
Code Issues 45 Pull Requests Actions 1 Packages Projects Releases Activity

release: v4.0.0-alpha.2; release.yml keeps the image's Isabelle #130

Merged
rajames merged 5 commits from StarForth-v4.0.0 into master 2026-11-07 19:32:31 +00:00
Conversation 0 Commits 5 Files Changed 19
+53 -2
rajames commented 2026-11-07 18:55:42 +00:00
Owner
Copy Link
Copy Source

What and why

v4.0.0-alpha.2, the first published alpha. v4.0.0-alpha.1 (233025da) was accepted and tagged, but its release run (196) was killed in the proofs step: release.yml ran a full make init for the documents' packages, which also fetched Isabelle into the workspace and pointed isabelle at it -- an Isabelle without the runner image's prebuilt HOL-Library -- so the proofs built HOL-Library from scratch (exit 137). Nothing was published.

Ruled (Captain Bob, 2026-11-07): the alpha.1 tag stays where it is; this PR

  • runs make ... init INIT_PROOFS=0 in release.yml, as nightly-docs.yml does, so the image's Isabelle (with HOL-Library) is the one used;
  • sets LITHOS_VERSION to 4.0.0-alpha.2; after it merges, master is tagged v4.0.0-alpha.2.

Records: FABRIC-3 XLVII.5, CHANGELOG. Part of #17.

Acceptance

The Acceptance check runs on this pull request. By hand, on this tree (04006bff):

  • Logs committed in logs/: amd64 20261107-184040, aarch64 -184241, riscv64 -184616 (POST 538/538, dict_hash=0xfec8c47cfc6f437f on all three), the stick loaded high -184753, test-32 (39 programs, 0 failures), the proofs -185450
  • Hardware this was tried on, if any: none

The record

  • docs/fabric/FABRIC-3.md XLVII.5
  • CHANGELOG.md
  • Nothing in this PR is a fix nobody asked for (.claude/CLAUDE.md, Hard Rules)

🤖 Generated with Claude Code

https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2

## What and why **v4.0.0-alpha.2, the first published alpha.** `v4.0.0-alpha.1` (`233025da`) was accepted and tagged, but its release run (196) was killed in the proofs step: `release.yml` ran a full `make init` for the documents' packages, which also fetched Isabelle into the workspace and pointed `isabelle` at it -- an Isabelle without the runner image's prebuilt HOL-Library -- so the proofs built HOL-Library from scratch (exit 137). Nothing was published. Ruled (Captain Bob, 2026-11-07): the alpha.1 tag stays where it is; this PR - runs `make ... init INIT_PROOFS=0` in `release.yml`, as `nightly-docs.yml` does, so the image's Isabelle (with HOL-Library) is the one used; - sets `LITHOS_VERSION` to `4.0.0-alpha.2`; after it merges, master is tagged `v4.0.0-alpha.2`. Records: FABRIC-3 XLVII.5, CHANGELOG. Part of #17. ## Acceptance The **Acceptance** check runs on this pull request. By hand, on this tree (`04006bff`): - [x] Logs committed in `logs/`: amd64 `20261107-184040`, aarch64 `-184241`, riscv64 `-184616` (POST 538/538, `dict_hash=0xfec8c47cfc6f437f` on all three), the stick loaded high `-184753`, `test-32` (39 programs, 0 failures), the proofs `-185450` - [ ] Hardware this was tried on, if any: none ## The record - [x] `docs/fabric/FABRIC-3.md` XLVII.5 - [x] `CHANGELOG.md` - [x] Nothing in this PR is a fix nobody asked for (`.claude/CLAUDE.md`, Hard Rules) 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2
rajames added 2 commits 2026-11-07 18:55:43 +00:00
release: v4.0.0-alpha.2; release.yml keeps the image's Isabelle [skip ci] 04006bff12 
v4.0.0-alpha.1's release run (196) was killed in the proofs: release.yml's
full `make init` fetched Isabelle into the workspace and pointed isabelle
at it, without the image's prebuilt HOL-Library, so the proofs built it
from scratch. Nothing was published. Ruled: the tag stays; release.yml runs
`init INIT_PROOFS=0`; LITHOS_VERSION 4.0.0-alpha.2, the first published
alpha. FABRIC-3.md XLVII.5, CHANGELOG.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2
release v4.0.0-alpha.2: accepted in full, logs [skip ci] d8bf2e1121 
The protocol on 04006bff (LithosAnanke v4.0.0-alpha.2), in this session,
one QEMU at a time in the foreground: amd64 logs/20261107-184040, aarch64
-184241, riscv64 -184616 (POST 538/538, dict_hash=0xfec8c47cfc6f437f on all
three), the stick loaded high -184753, test-32 (39 programs, 0 failures),
the Isabelle/HOL proofs (logs/20261107-185450/).

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2
rajames added 1 commit 2026-11-07 18:56:19 +00:00
release v4.0.0-alpha.2: run the acceptance check on #130 4a125cdd21 
The commits before this one carry [skip ci], which Gitea also applies to
the pull request's checks. No change to the tree.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2
rajames closed this pull request 2026-11-07 18:57:16 +00:00
rajames reopened this pull request 2026-11-07 18:57:16 +00:00
rajames added 1 commit 2026-11-07 18:59:36 +00:00
release v4.0.0-alpha.2: start #130's acceptance check
Acceptance / Acceptance (pull_request) Failing after 8m7s
Details
cabe974872 
The commit before this one quoted the skip marker in its message, so Gitea
skipped its checks too. No change to the tree.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2
rajames added 1 commit 2026-11-07 19:15:06 +00:00
logs: three riscv64 boots of v4.0.0-alpha.2, looking for run 197's failure
Build / Image MILKV (push) Canceled after 0s
Details
Acceptance / Acceptance (pull_request) Successful in 16m36s
Details
Build / Image RASPI (push) Canceled after 0s
Details
Build / v4 tests (32- and 64-bit cells) (push) Canceled after 0s
Details
Build / Image PC (push) Canceled after 0s
Details
37f62d688b 
Acceptance run 197 (#130) failed one riscv64 check: no 'Boot disk: not a
StarshipOS stick' line, with POST, the identity and the prompt all passing.
Booted three more times here on the same tree: each printed the line and
passed (4 of 4 with logs/20261107-184616). The Zuse stick has no ESP
(--esp-mib 0), so the firmware cannot have booted from it; the serial
capture losing or garbling the line is what is left to check, against run
197's own log.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2
rajames merged commit 2d43db252a into master 2026-11-07 19:32:31 +00:00
Sign in to join this conversation.
Reviewers
No Reviewers
Labels
Clear labels
area/capsules
capsules/ and mkcapsule
 area/docs
docs/
 area/kernel
kernel/ -- LithosAnanke
 area/proofs
proof/ -- Isabelle/HOL
 area/v3
v3/ -- the original StarForth VM
 area/v4
v4/ and capsules/v4 -- the F18 engine
 board/milkv
Milk-V Mars
 board/pc
Generic x86-64 PC (SER5)
 board/raspi4
Raspberry Pi 4 (not ported)
 board/raspi5
Raspberry Pi 5
 board/zynq7020
Zynq-7020 (ARMv7 port in progress)
kind
bug
Something is wrong
kind
chore
Housekeeping, repo hygiene
kind
ci
Build, CI, nightly, release
kind
docs
Documentation only
kind
feature
New capability
priority
must
Needed for v4.0.0 (JUSTIFICATION.md 14/16)
priority
nice
Nice to have
priority
should
Needed for the product, not for the tag
status
backlog
Not started
status
blocked
Waiting on something else
status
in-progress
Being worked on
status
needs-acceptance
Done; the QEMU acceptance boots are still to run
status
rejected
Decided against; closed
No labels
Milestone
No items
No Milestone
Projects
Clear projects
No projects
Assignees
Clear assignees
rajames (Robert A. James (Captain Bob))
No Assignees
1 Participants
Notifications
Due Date
No due date set.
Dependencies

No dependencies set.

Reference: rajames/LithosAnanke#130