From c81b26d9c2201cd19ca55252855db85359652dc0 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Thu, 2 Jul 2026 16:23:30 +0200 Subject: [PATCH] lean-guard: disable core dumps (no more apport popups on capped aborts) Co-Authored-By: Claude Fable 5 --- verification/check.sh | 1 + verification/lean-guard | 7 ++++++- 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/verification/check.sh b/verification/check.sh index 045a03e..ea4c306 100755 --- a/verification/check.sh +++ b/verification/check.sh @@ -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). diff --git a/verification/lean-guard b/verification/lean-guard index 60d98bc..256ef42 100755 --- a/verification/lean-guard +++ b/verification/lean-guard @@ -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" "$@"