installation fails if a startup script in the terminal asks for input

[bryangingechen]

Description

(Background info: I installed oh my zsh on a whim and one of the things it occasionally does is prompts the user if they'd like to update when starting a new shell. Today happened to be a day where it decided to ask if I wanted to update.)

I tried installing lean4 using the "Walkthrough" provided by vscode-lean4, and when I clicked the "Install Lean Version Manager" button, a terminal window opened, and the b in the bash -c ... installation command got eaten by the above-mentioned prompt and only ash -c ... was executed, leading to a funny ashc not found command. (I unfortunately have closed the window so I can't provide a screenshot or exact log).

After I figured out what was going on, I laughed and then tried to click the install button again, but the extension complained that the installation process was still in progress. After scratching my head for a second, I realized I had to first kill the still-open terminal. Once I did that though, the installation button worked.

This is most likely an extremely niche issue (and also relatively easy to resolve by the user), but I thought I'd share it here in case it was useful.

Context

[Broader context that the issue occured in. If there was any prior discussion on the Lean Zulip, link it here as well.]

Steps to Reproduce

1. have something in your shell scripts that cause it to ask for input on startup
2. try to install Lean 4 using the "Install Lean Version Manager" button

Expected behavior: the extension waits for the user to deal with whatever pops up in the terminal before the actual command prompt shows up, and only then runs the installation command, or, if that isn't possible, fail in a way that doesn't require the user to kill the terminal manually.

Actual behavior: described above

Versions

[Version of vscode-lean4 (Hover over 'lean4' in the 'Extensions' menu)] 0.0.186
[Output of lean --version in the folder that the issue occured in] n/a
[OS version] macOS 15.1.1

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.

[mhuisi]

I'd really like to replace this strange way of installing Lean by opening a terminal and running commands in it entirely at some point.