The script was already tested on mac. Looking at the .travis.yml configuration, can you see a reason why the problem you're highlighting was not caught by testing?

The travis test executes the file locally. That works. But according to @PatrickMassot, the preferred way of using the script is by curl https://raw.githubusercontent.com/leanprover-community/mathlib/master/scripts/remote-install-update-mathlib.sh -sSf | sh, see https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Installing.20mathlib/near/162600876. And here we run into the issue that sh has it STDIN set to the output of the pipe. So the read command in the script will try to read from the pipe, not /dev/tty, which doesn't make sense in this context.

That's very odd. I'm using a Mac and I've never had that issue.

Did you ever try the script without python being installed?

I have not. Is this related to using /dev/tty?

Can you adapt the tests in .travis.yml file to exhibit the issue please? Instead of:

        - sh scripts/remote-install-update-mathlib.sh

try:

- curl https://raw.githubusercontent.com/leanprover-community/$TRAVIS_BRANCH/scripts/remote-install-update-mathlib.sh -sSf | sh

Yes, the </dev/tty is necessary if there's a read call. This happens only if no python is installed, i.e. on a Mac if both conditions ! which pip3 and which brew are met.

In this case the user is asked if they want to proceed, for this STDIN has to be set to /dev/tty.

It doesn't make sense to test this on travis unless we're simulating user input (the y(es)). I don't know how to do that. In particular since that would require reading the output of the script, and waiting for the right moment to say yes.

A reasonable alternative to this change is to stop asking the user for confirmation. We could just print an error message along the lines of

install pip3 / python3, e.g. using brew install python3

I think we can test the user input by piping echo y into the script. I'm not against adding /dev/tty. I just want to make sure it works on more than just your system.

Of course you echo y into a a pipe. But that somehow circumvents the issue. The problem at the moment is that when executing

curl https://raw.githubusercontent.com/leanprover-community/mathlib/master/scripts/remote-install-update-mathlib.sh -sSf | sh,

the y is suppose to come from the pipe, the same pipe through which curl feeds code into sh. Now we could write code to create another pipe, but that doesn't touch the issue. It would just be another implementation ...

I'm increasingly in favour of just removing those questions and printing a warning. It's cleaner and simpler. And I doubt anybody would miss the functionality.

If you don't object, I modify the PR.

I really prefer if the script install what it can. A lot of the users are not programmers and I'd like them to be able to use mathlib without having to look into how to install python.

Can we use /dev/tty and still pipe things into the script?

I wouldn't know how to.

This was incorporated in #968

Thanks @jdsalchow!