scrolling with lean --make on command line

Stream: general

[Kevin Buzzard]

I have a Lean project sufficently deep in a filespace heierarchy that lean --make -M4000 sheaf_on_opens_total_glueing.lean from the command line makes the console start scrolling. The only fix I know is to make the console window massive. There must be a more hygenic way to stop this from happening (on Ubuntu)

[Reid Barton]

I often have the same problem and I haven't found a good way to deal with it without making the window massive

[Reid Barton]

One thing you can do is pipe the output into less (normally I do this when I expect there to be a lot of errors), which disables the feedback about which file is being built entirely

[Kevin Buzzard]

I am normally interested in the first error and not much more

[Reid Barton]

that's another advantage to piping through less