`--threads=0` leads to an assertion violation

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

As of Lean 4.9.0, --threads=0 gives an assertion violation.

Steps to Reproduce

1. Run lean --threads=0 <(echo "example : True := by simp")

Expected behavior: Either silent, or complains that threads=0 is illegal

Actual behavior:

LEAN ASSERTION VIOLATION
File: /home/runner/work/lean4/lean4/src/runtime/object.cpp
Line: 1053
g_task_manager
'unreachable' code was reached

from

https://github.com/leanprover/lean4/blob/daa22187642d4cf6954c39a23eab20d8a8675416/src/runtime/object.cpp#L1052-L1053

Versions

v4.9.0 onwards

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Reproduce the failure with lean --threads=0 <(echo "example : True := by simp"), then start at src/runtime/object.cpp around line 1052. Trace how the thread count reaches the task manager and ensure the command either completes silently or reports that zero threads is invalid, without an assertion violation.