Skip to content

fix: reject a zero thread count - #14652

Open
sankalpsthakur wants to merge 1 commit into
leanprover:masterfrom
sankalpsthakur:agent/reject-zero-threads
Open

fix: reject a zero thread count#14652
sankalpsthakur wants to merge 1 commit into
leanprover:masterfrom
sankalpsthakur:agent/reject-zero-threads

Conversation

@sankalpsthakur

Copy link
Copy Markdown
Contributor

This PR rejects -j0 / --threads=0 during shell option processing instead of allowing an invalid task-manager size to reach the runtime.

The runtime requires a positive worker count in multithreaded builds. Add an explicit zero check alongside the existing numeric and upper-bound validation, with a focused tests/misc regression asserting a clean diagnostic and nonzero exit.

Closes #4927

Validation

  • Added tests/misc/threads_zero.sh
  • The branch diff contains only the shell validation and focused CLI regression
  • Full Lean CI is the authoritative validation

AI assistance

AI tools assisted with issue triage, duplicate-PR search, implementation, and regression preparation. I reviewed the shell option path and final two-file diff.

@sankalpsthakur
sankalpsthakur marked this pull request as ready for review August 2, 2026 06:37
@github-actions github-actions Bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Aug 2, 2026
@mathlib-lean-pr-testing

mathlib-lean-pr-testing Bot commented Aug 2, 2026

Copy link
Copy Markdown

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 05a6ddfb52c033f12967c96443a93b0ca7b8a58a --onto 5b8d06c1764fa367a1e27b3e89f64667eac425af. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-02 06:40:37)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 945e78b86645b179655123cd2fdba83d89d28d07 --onto 110db9cb751afaee8b2ac344887d6c7e632f77b4. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-04 02:10:40)

@leanprover-bot

leanprover-bot commented Aug 2, 2026

Copy link
Copy Markdown
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 05a6ddfb52c033f12967c96443a93b0ca7b8a58a --onto 23393b959b33e3a8d15796b2397f8a04c315b9f4. You can force reference manual CI using the force-manual-ci label. (2026-08-02 06:40:39)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 945e78b86645b179655123cd2fdba83d89d28d07 --onto 23393b959b33e3a8d15796b2397f8a04c315b9f4. You can force reference manual CI using the force-manual-ci label. (2026-08-04 02:10:42)

@sankalpsthakur
sankalpsthakur force-pushed the agent/reject-zero-threads branch from a8708bf to ab93b8a Compare August 4, 2026 01:47
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

--threads=0 leads to an assertion violation

2 participants