limit max CPU time per process

joneugster · joneugster · commit 07c5cdecf696 · 2025-04-03T14:11:35.000+02:00
diff --git a/server/bubblewrap.sh b/server/bubblewrap.sh
@@ -1,5 +1,9 @@
 #/bin/bash
 
+# Limit CPU time per process to 1h
+ulimit -t 3600
+# NB: The RSS limit (ulimit -m) is not supported by modern linux!
+
 LEAN_ROOT="$(cd $1 && lean --print-prefix)"
 LEAN_PATH="$(cd $1 && lake env printenv LEAN_PATH)"
 
