Error formatting

Stream: general

[Yaël Dillies]

I believe this has been discussed before, but I can't find the relevant discussions: Can we make rid lake's output of the irrelevant parts of the path to files?

[Yaël Dillies]

For example, this job prints

Warning: /home/lean/actions-runner/_work/mathlib4/mathlib4/Mathlib/Algebra/GroupWithZero/Int.lean:7:1: warning: import #[Mathlib.Algebra.Group.Int.Defs] instead
/home/lean/actions-runner/_work/mathlib4/mathlib4/Mathlib/Algebra/GroupWithZero/Int.lean:
  remove #[Mathlib.Algebra.Group.Int.TypeTags]
  add #[Mathlib.Algebra.Group.Int.Defs]
/home/lean/actions-runner/_work/mathlib4/mathlib4/Mathlib/Algebra/Order/Ring/IsNonarchimedean.lean:
  remove #[Mathlib.Algebra.GroupWithZero.Action.Defs]
/home/lean/actions-runner/_work/mathlib4/mathlib4/Mathlib/Algebra/Tropical/Basic.lean:
  remove #[Mathlib.Algebra.GroupWithZero.Action.Defs]
/home/lean/actions-runner/_work/mathlib4/mathlib4/Mathlib/RingTheory/Valuation/Discrete/Basic.lean:
  remove #[Mathlib.Algebra.GroupWithZero.Int]

[Yaël Dillies]

There are several things that are wrong with it:

• The first error is on the same line as Warning:, meaning it shows differently to the other ones, ie
  like this

  

• The repeated /home/lean/actions-runner/_work/mathlib4/mathlib4/ drown the important information

[Yaël Dillies]

It's possible part of this is an issue with https://github.com/leanprover-community/gh-problem-matcher-wrap

[Eric Wieser]

It looks like the --gh-style flag isn't doing as well as it could

[Eric Wieser]

Which confusingly, seems to currently mean --lean-style, which is then handled by the matcher you link

[Eric Wieser]

As opposed to directly using the actual github style

[Kim Morrison]

@Mac Malone is looking into fixing the absolute paths, if I understand correctly. Hopefully this will be better in the next release.