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

release: v4.0.0-alpha.3; the proofs run capped to fit the server

Browse Source 
v4.0.0-alpha.2's release run (200) was killed in the StarForth session:
Isabelle's defaults (Java 4 GiB, a thread per CPU). scripts/nightly.sh
proofs now runs one thread, Java 512 MiB, Poly/ML 900 MiB, through a
settings file of a home made for the run (heaps linked to the user's):
47 s, ~1.8 GiB, logs/20261107-195341. Nothing was published from alpha.2;
its tag stays. LITHOS_VERSION 4.0.0-alpha.3. FABRIC-3.md XLVII.6.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GE3SDvQn5EoxdGufk84zz2
This commit is contained in:
Claude
2026-11-07 19:54:47 +00:00
parent 2d43db252a
commit 50d2bc98d9
5 changed files with 45 additions and 4 deletions
Download Patch File Download Diff File Expand all files Collapse all files
scripts/nightly.sh
+15 -2
View File
@@ -16,7 +16,8 @@
# 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
# isabelle build -c -D proof/, capped to fit the server (one thread, small heaps): the StarForth
# session checked afresh every run, whatever is
# cached (HOL-Library is reused: the CI image has it built, ci/runner-image); its log is
# logs/<TS>/isabelle/, as a boot's is.
# scripts/nightly.sh images
@@ -121,7 +122,19 @@ 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"
# Within the server's memory: one thread, Java's heap 512 MiB, Poly/ML's 900 MiB -- the
# StarForth session peaks at ~1.7 GiB so (46 s), where Isabelle's defaults (Java 4 GiB, a thread
# per CPU) were killed (release run 200, v4.0.0-alpha.2). The caps go in a settings file of a
# home made for the run; its heaps are the user's own, linked in, and the image's HOL-Library
# is found as always, with Isabelle itself.
isahome=$(mktemp -d)
isaver=$(isabelle getenv -b ISABELLE_IDENTIFIER)
mkdir -p "$isahome/.isabelle/$isaver/etc" "$HOME/.isabelle/$isaver/heaps"
ln -s "$HOME/.isabelle/$isaver/heaps" "$isahome/.isabelle/$isaver/heaps"
printf '%s\n' 'ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms128m -Xmx512m -Xss16m"' \
'ML_OPTIONS="--minheap 200 --maxheap 900"' > "$isahome/.isabelle/$isaver/etc/settings"
USER_HOME="$isahome" isabelle build -o threads=1 -c -v -D proof/ 2>&1 | tee "logs/$ts/isabelle/isabelle-$ts.log"
rm -rf "$isahome"
;;
images)
need "$OUT/StarshipOS.iso"