scrolling when compiling in linux

Stream: general

[Kevin Buzzard]

When I type lean --make in Ubuntu, in the directory /home/buzzard/Encfs/Computer_languages/Lean/lean-projects/lean-perfectoid-spaces/_target/deps/mathlib, I get a lot of output which scrolls and scrolls because it's a lot more than 80 characters long. If I make my terminal window super-big and the font super-small so that everything fits onto one line then the scrolling doesn't happen, and it's better when the scrolling doesn't happen because then any errors are far more apparent (I would not expect errors in mathlib but say I'm compiling one of my own projects). Is there any way of stopping the scrolling somehow? I notice that in Windows there doesn't seem to be any output at all. If I redirect STDOUT to /dev/null I could reproduce this -- but then do I still see errors reported? Are they piped to STDERR?

Related I guess -- is it safe to stop compilation with Ctrl-C and then type lean --make again?

[Mario Carneiro]

I think you can pipe lean through a command to disable the progress reporting (i.e. the windows experience). Does lean --make | cat work?

[Rob Lewis]

It's safe to stop compilation with Ctrl-C on Linux. I've noticed this doesn't work in the msys2 shell on Windows, but I've never investigated, maybe there's an easy fix.

[Mario Carneiro]

I have never had an issue, but possibly you have to Ctrl-C twice

[Rob Lewis]

It locks up the whole terminal for me more often than not, and I have to kill Lean from the process manager.

[Rob Lewis]

But yeah, if it works for you then there's probably an easy fix for me that I should look for!

[Kevin Buzzard]

I'd rather see the names of the files flashing by all on one line without any scrolling, and then a scroll iff there's a sorry / error