Run `lake build` and jump to next error

Stream: Is there code for X?

[Joachim Breitner]

When updating mathlib after a change to core, I find most of the time is spent running lake build, looking at the error message, finding the file name and location, opening it in VSCode, jumping to the right location, and only then doing the edit.

Is there a way to say “run lake build and jump to the next error”?

[Joachim Breitner]

Ah, simply using the VSCode built-in terminal turns the file locations into links. That helps.

[Kim Morrison]

I have a script which I run as errors lake build which opens all the files mentioned in errors.

[Kim Morrison]

I'm away from a computer for the weekend so can't post the script now, but will later.

[Kim Morrison]

It is helpful, but unfortunately it grabs focus as it opens each file.

[Joachim Breitner]

Nice! But no hurry, clicking in the terminal is pretty close to optimal – I can even do it while it still works on more files.

[Damiano Testa]

I usually run

lake build |
  sed -n 's=[./]*\(Mathlib[^ ]*\): .*=code -r -g \1=p'

which produces an output with many lines like

code -r -g <filename:lin:col>

and copy-pasting those lines -recycles an open VSCode and -goes to the specified file-line-column.