saymrwulf/dalek-ed25519-verified
1
0
Fork 0
mirror of https://github.com/saymrwulf/dalek-ed25519-verified.git synced 2026-09-04 20:24:12 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

lean-guard: disable core dumps (no more apport popups on capped aborts)

Browse source 
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This commit is contained in:
mrwulf 2026-07-02 16:23:30 +02:00
parent 67f1b11730
commit c81b26d9c2
2 changed files with 7 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
verification/check.sh
View file

@ -20,6 +20,7 @@ source ~/aeneas-toolchain/env.sh
HERE="$(cd "$(dirname "$0")" && pwd)"
AENEAS_LEAN="$AENEAS_HOME/backends/lean"
TIMEOUT="${LEAN_TIMEOUT:-300}"
export LEAN_MEM_MB="${LEAN_MEM_MB:-6144}"
CORES="${LEAN_MAX_CORES:-0-3}"
# Layer manifests (extended as the pyramid grows; ORDER = import order).

7
verification/lean-guard
View file

@ -37,6 +37,11 @@
# ────────────────────────────────────────────────────────────────────────────
set -uo pipefail
# No core dumps: hitting the memory cap makes lean (and uutils `timeout`) abort;
# those aborts are EXPECTED and their core dumps only trigger Ubuntu apport
# popups and fill /var/crash. ulimit applies to this shell and every child.
ulimit -c 0 2>/dev/null || true
TIMEOUT_SEC=${LEAN_TIMEOUT:-400}
MEM_MB=${LEAN_MEM_MB:-4096}
CGROUP_MB=${LEAN_CGROUP_MB:-$((MEM_MB + 1024))}
@ -101,7 +106,7 @@ if systemd-run --user --scope -p MemoryMax=10M --quiet -- /bin/true 2>/dev/null;
# --scope runs the command as a child of THIS shell (env inherited),
# merely placing it in a fresh cgroup with the hard caps below.
systemd-run --user --scope --quiet \
-p MemoryMax="${CGROUP_MB}M" -p MemorySwapMax=256M \
-p MemoryMax="${CGROUP_MB}M" -p MemorySwapMax=256M -p LimitCORE=0 \
-- taskset -c "$CORES" \
timeout --signal=TERM --kill-after=15 "$TIMEOUT_SEC" \
lean -M "$MEM_MB" -o "$OLEAN_FILE" "$LEAN_FILE" "$@"