`lake lean` silently exits when given a process-substituted input

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

lake lean <(printf 'NOT VALID LEAN')

exits silently when given the named FIFO / /dev/fd substitution above, even though the lean CLI does not when given it directly.

Context

zsh supports syntax for "process substitution" using the syntax <(subprocess ...). Quoting the manpage:

In the case of the < or > forms, the shell runs the commands in list as a subprocess of the job executing the shell command line. If the system supports the /dev/fd mechanism, the command argument is the name of the device file corresponding to a file descriptor; otherwise, if the system supports named pipes (FIFOs), the command argument will be a named pipe.

It also supports a second form, =(subproces ...):

If =(...) is used instead of <(...), then the file passed as an argument will be the name of a temporary file containing the output of the list process.

The lean CLI has no issue with either substitution (here I'm on macOS, so this is /dev/fd input):

⊙  lean <(print '#check 37')
37 : Nat

and of course a tempfile is fine:

lean =(print '#check 37')
37 : Nat

Steps to Reproduce

lake lean only is happy with the latter:

⊙  lake lean <(print '#check 37')

~/Development/ProofWidgets4 is a git repository on main 
⊙  lake lean =(print '#check 37')
37 : Nat

exiting silently when given the "normal" tempfile-less substitution.

Expected behavior: Ideally lake lean <(...) should work identically (to lean and to its own =(...) behavior), though if lake really wants to seek or otherwise rely on it being a file, an error should be shown of some sort rather than silent success.

Actual behavior: lake exits with exit code 0.

Versions

[Output of #version or #eval Lean.versionString]
[OS version, if not using live.lean-lang.org.]

lake --version
Lake version 5.0.0-045d07d (Lean version 4.19.0-rc3)

macOS 15.4.1

Additional Information

lake env lean of course has the correct behavior here (which is what I ended up using), which makes this even lower presumably.

Impact

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

Start at the lake lean CLI entry point and compare its handling with lake env lean and direct lean for the shown process-substituted input. Reproduce both <(print '#check 37') and =(print '#check 37'); done means lake lean <(...) behaves like lean or reports a visible error instead of exiting successfully and silently.