Zulip Chat Archive

Stream: general

Topic: Extract errors from logs

Yaël Dillies (Dec 16 2023 at 12:02):

Would it be possible to extract the errors from the lake build log in mathlib CI? Currently, jobs like this one are a sea of [X/4024] Building <file> to scroll through to get to an error.

Mauricio Collares (Dec 16 2023 at 12:05):

The annotations section at https://github.com/leanprover-community/mathlib4/actions/runs/7231435450 is not perfect but it's better than nothing

Yaël Dillies (Dec 16 2023 at 12:10):

That's too little info :sad:

Eric Wieser (Dec 16 2023 at 13:24):

We had a nice version of this in Lean3 because lean --make took a --json flag

Eric Wieser (Dec 16 2023 at 13:25):

(one that showed all the lines of error in the annotations)

Alex J. Best (Dec 16 2023 at 16:55):

Indeed as far as I recall there wasn't a good way of getting githubs problem matchers to match multiple lines

Alex J. Best (Dec 16 2023 at 16:56):

We could perhaps try and pipe all the errors into an actions summary file, that might be more useful

Eric Wieser (Dec 16 2023 at 17:16):

Maybe we can extract the errors from the infotree so that we don't need the json flag?

Last updated: Dec 20 2023 at 11:08 UTC