use scrolling mode when used non-interactively

[digama0]

Use isatty to find out whether the user is typing directly in the terminal or if this is a tool-driven run, and set the default scroll mode accordingly. This should help tests to avoid hanging on input.

[jkingdon]

Ooh, this is a bit of a tough call. On the one hand, we've traditionally wanted to stick to Standard C and this has some consequences at least on Windows (even trying to figure out exactly what we would need to do from https://docs.microsoft.com/en-us/cpp/c-runtime-library/reference/posix-isatty?view=msvc-170 wasn't immediately clear to me).

On the other hand, I can see how our traditional approach of putting set scroll continuous everywhere is, well error prone as we've seen in #58 (comment) .

Even strictly in a unix context, although this kind of isatty check has a long pedigree, I'm a bit unclear about whether it is considered a best practice. At least some tools have an interactive variant and a batch variant (for example irb versus ruby).

[benjub]

Why not make "continuous" the default in every case ?

[digama0]

Why not make "continuous" the default in every case ?

Because it's not good for regular use: if I use search * "+ ( ? +" I will get a bunch of results and don't want them to just scroll off the screen, especially if the terminal emulator has poor support for scrolling the screen and/or has a small screen buffer.

I will replicate the alternative suggestions I posted on the other issue here:

• Add a command line flag or environment variable to change the default scroll mode, which would only be enabled in the test harness
• The test harness would add SET SCROLL CONTINUOUS to the start of the .in file, and wouldn't bother filtering the output; this would bloat all the .expected files and might make reading them more annoying though

By the way, you can also make tests to click through the prompts: you just have to say s\ns\ns to keep scrolling, and I think there is another letter for "scroll to end".

[jkingdon]

• The test harness would add SET SCROLL CONTINUOUS to the start of the .in file, and wouldn't bother filtering the output

I'm now leaning towards this solution. It isn't hard to implement, and I guess feels like the right balance in terms of keeping things simple, but not too simple.

; this would bloat all the .expected files and might make reading them more annoying though

The more I think about this the more I'm not especially bothered by this factor. The boilerplate output (e.g. size of empty.expected) goes from 9 lines to 10.

I've submitted a pull request for this one at #62

[digama0]

Replying to @jkingdon, #62 (comment):

Still not sure this is the direction we should take, but the contents of the PR itself look fine.

🤷 Yeah, it isn't really a slam dunk for me either. I sort of go back and forth about whether my being wary of isatty is just my own aesthetic distate, or whether avoiding isatty for a little while until we make our mind is the thing to do, or whether it'll be fine and we'll come up with a Windows fix without too much trouble or whether we should do the Windows fix first (dropping Windows support, which I guess #59 does as currently written, seems like a big step) or what.

Could you elaborate on how this breaks windows? I see it's a deprecated function on windows but it sounds like it should work anyway. I'd rather not drop windows support just for this (or at all, really), but we can use preprocessor flags if necessary. I will try this out on windows myself and see what the situation is. (We should also run the tests on windows in CI; I think this is not hard to set up.)

[jkingdon]

Could you elaborate on how this breaks windows?

Windows doesn't have unistd.h does it? (I'm thinking of the Visual Studio compiler or whatever the vanilla windows setup is these days, not like cygwin or whatever Microsoft calls their latest linux subsystem or whatever it is).

I will try this out on windows myself and see what the situation is. (We should also run the tests on windows in CI; I think this is not hard to set up.)

Both of those seem like a better idea than me trying to find the answer based on dim memories or trying to find the right documentation by internet searches and not being sure I understand it correctly.

[digama0]

Okay, I have a tested setup now. On windows we call the _isatty function instead. Unfortunately, it still doesn't work correctly with MSYS2 and Cygwin terminals (including git bash for windows), and we will incorrectly guess that these are not TTYs and will set scroll continuous for them. However, the fix for this is sketchy (https://github.com/softprops/atty/blob/master/src/lib.rs#L116-L154) and is an awful lot of code for such a niche situation. My guess is that most windows users are going to download precompiled binaries and use cmd.exe (or just double click the executable), and it works fine there.

[jkingdon]

On windows . . . Unfortunately . . . However, the fix for [one case] is sketchy

Well, first of all thanks for digging into this. I'm not sure I have a lot of firm conclusions except the obvious "looks like this isn't as simple as we might have been hoping".

Aside from Windows are there any environments we might care about which just support Standard C? I'm thinking of things like https://compcert.org/man/manual005.html#sec49 although at least for now their answer seems to be "we are worrying about the compiler, not the OS or standard library". Another example would be if there are compilers which emit Proof Carrying Code or ...... well I'm not sure how much these things even exist, especially for C, I'm just thinking if they did metamath enthusiasts might be a bit more likely than most people to care about them.

[digama0]

Okay. I'm a little sad this can't just automagically work on every system but it's more important that we don't regress the user experience than the tests, so false positives are not good. I'm closing this PR, but if new information comes up regarding terminals in use or better ways to implement the check then we can revisit this.