From ab93b8a9b1dbb4c8a0c17351c62e026355e54e2e Mon Sep 17 00:00:00 2001
From: Sankalp Thakur <31366524+sankalpsthakur@users.noreply.github.com>
Date: Tue, 4 Aug 2026 07:17:42 +0530
Subject: [PATCH] fix: reject a zero thread count

---
 src/Lean/Shell.lean        |  5 +++++
 tests/misc/threads_zero.sh | 11 +++++++++++
 2 files changed, 16 insertions(+)
 create mode 100755 tests/misc/threads_zero.sh

diff --git a/src/Lean/Shell.lean b/src/Lean/Shell.lean
index 3f73f6fe35d1..6d7c8685f19a 100644
--- a/src/Lean/Shell.lean
+++ b/src/Lean/Shell.lean
@@ -301,6 +301,8 @@ def ShellOptions.process (opts : ShellOptions)
     let arg ← checkOptArg "j" optArg?
     let some numThreads := arg.toNat?
       | throwExpectedNumeric "j"
+    if numThreads == 0 then
+      throwExpectedPositive "j"
     if h : numThreads < UInt32.size then
       let numThreads := UInt32.ofNatLT numThreads h
       let forwardedArgs := opts.forwardedArgs.push s!"-j{arg}";
@@ -460,6 +462,9 @@ where
   @[inline] throwExpectedNumeric opt := do
     eprint s!"error: expected numeric argument for option '-{opt}'\n"
     throw 1
+  @[inline] throwExpectedPositive opt := do
+    eprint s!"error: expected positive numeric argument for option '-{opt}'\n"
+    throw 1
   @[inline] throwTooLarge opt := do
     eprint s!"error: argument value for '-{opt}' is too large\n"
     throw 1
diff --git a/tests/misc/threads_zero.sh b/tests/misc/threads_zero.sh
new file mode 100755
index 000000000000..48b67a61c6d8
--- /dev/null
+++ b/tests/misc/threads_zero.sh
@@ -0,0 +1,11 @@
+set -euo pipefail
+
+out="${NAME}.out"
+trap 'rm -f "$out"' EXIT
+
+if lean -j0 >"$out" 2>&1; then
+  echo "lean -j0 unexpectedly succeeded" >&2
+  exit 1
+fi
+
+grep -Fx "error: expected positive numeric argument for option '-j'" "$out"