search

Julian / lean.nvim

neovim support for the Lean theorem prover
MIT License
255 stars 25 forks source link

git password prompt in lakefile breaks neovim #274

Open gebner opened 2 years ago

gebner commented 2 years ago

Put the following in a lakefile:

require std4 from git "https://github.com/leanprover-community/std4" @ "main"

Note that I made a mistake: this repo does not exist since std4 is in the leanprover organization.

When I open this file in neovim, it then shows the following:

  meta if get_config? doc = some "on" then -- do not download and build doc-gen4 by default
  require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"
+
+ Username for 'https://github.com': ub.com/leanprover-community/std4" @ "main"

There is a password prompt, and it shown on top of the neovim TUI. Even worse, there is no way to either enter a password or interact with neovim.

Julian commented 2 years ago

I don't see that here -- anything else you can share about reproducing?

What I see isn't much (no error at all):

https://user-images.githubusercontent.com/329822/188221771-d0ec468d-68a7-4073-9f1a-bfaa7411c43b.mov

gebner commented 2 years ago

This could be a difference between macOS and Linux. From what I can tell the git password prompt goes to extreme lengths so that it is shown (and accepts input!) even when you redirect all outputs:

$ git clone https://github.com/leanprover-community/std4 </dev/null >/dev/null 2>/dev/null
Username for 'https://github.com': gebner
Password for 'https://gebner@github.com':
Julian commented 2 years ago

Got it, will give a shot on a Linux box then I guess (though what you show there is the same as the behavior on macOS -- I think it just chooses to read/write directly to /dev/tty?)