Error messages

Stream: mathlib4

[Yuval Filmus]

The mathlib4 linter is sometimes unhappy with simp annotations.
The ensuing link to the documentation explaining how to debug this leads to the mathlib3 docs!

[Ruben Van de Velde]

Please elaborate.

[Michael Rothgang]

What you're describing sounds wrong and like it should be fixed --- but it's hard to guess what exactly you mean. If you provide more detail (so we can reproduce ourselves), we can investigate.

[David Ledvinka]

Perhaps he means this? (I ran into this issue earlier but fixed it) https://github.com/leanprover-community/mathlib4/actions/runs/19838703436/job/56842041319

[David Ledvinka]

but the link is to mathlib3 doc

[Chris Henson]

So really this is a batteries issue, as it appears on this line of the simpNF linter.

[Chris Henson]

It could be updated maybe to https://leanprover-community.github.io/extras/simp.html#simp-normal-form or https://lean-lang.org/doc/reference/latest/The-Simplifier/Simp-Normal-Forms/?

[Chris Henson]

Though those are a bit different from the original note giving specific tips about the linter.

[Yuval Filmus]

The error is part of continuous integration (mathlib forks).
The exact text (in a sample case) is:

/- The simpNF linter reports:

https://github.com/leanprover-community/mathlib4/actions/runs/19871554851/job/56948601734#step:37:22SOME SIMP LEMMAS ARE NOT IN SIMP-NORMAL FORM.

https://github.com/leanprover-community/mathlib4/actions/runs/19871554851/job/56948601734#step:37:23see note [simp-normal form] for tips how to debug this.

https://github.com/leanprover-community/mathlib4/actions/runs/19871554851/job/56948601734#step:37:24https://leanprover-community.github.io/mathlib_docs/notes.html#simp-normal%20form -/

https://github.com/leanprover-community/mathlib4/actions/runs/19871554851/job/56948601734#step:37:25-- Mathlib.Analysis.SpecialFunctions.Arcosh

https://github.com/leanprover-community/mathlib4/actions/runs/19871554851/job/56948601734#step:37:26Error: /home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/Mathlib/Analysis/SpecialFunctions/Arcosh.lean:183:3: error: Real.cosh'OrderIso_apply_coe Left-hand side simplifies from

https://github.com/leanprover-community/mathlib4/actions/runs/19871554851/job/56948601734#step:37:27↑(Real.cosh'OrderIso x)

https://github.com/leanprover-community/mathlib4/actions/runs/19871554851/job/56948601734#step:37:28to

https://github.com/leanprover-community/mathlib4/actions/runs/19871554851/job/56948601734#step:37:29↑(Real.cosh'OrderIso x)

https://github.com/leanprover-community/mathlib4/actions/runs/19871554851/job/56948601734#step:37:30using

https://github.com/leanprover-community/mathlib4/actions/runs/19871554851/job/56948601734#step:37:31dsimp only [*, AOReal.val_eq_coe]

https://github.com/leanprover-community/mathlib4/actions/runs/19871554851/job/56948601734#step:37:32Try to change the left-hand side to the simplified term!

[Michael Rothgang]

Thanks! batteries#1544 improves the error messages.

[Michael Rothgang]

CC @Anne Baanen Here's another documentation question: should the practical tips from https://leanprover-community.github.io/mathlib_docs/notes.html#simp-normal%20form be integrated into https://leanprover-community.github.io/extras/simp.html#simp-normal-form? Do you have capacity to do so?

[Michael Rothgang]

Actually, a better fix might be to port docs#LibraryNote to batteries, and then link to the documentation entry for the "simp normal form" library note as before. But you also wanted to do that, right?

[Anne Baanen]

Michael Rothgang said:

Actually, a better fix might be to port docs#LibraryNote to batteries, and then link to the documentation entry for the "simp normal form" library note as before. But you also wanted to do that, right?

Yes, that was my plan once I got doc-gen to output a library notes page. But I can already do the upstreaming right now, and then add the doc-gen support later.

[Chris Henson]

Michael Rothgang said:

Actually, a better fix might be to port docs#LibraryNote to batteries, and then link to the documentation entry for the "simp normal form" library note as before. But you also wanted to do that, right?

I agree this is better, for the reason I mention above of the note serving a different purpose than other docs. (A different Divio quadrant, to use the language of the new documentation overview.)

[Anne Baanen]

Upstreaming PR: batteries#1545 (should build now, I'll work on the Mathlib adaptation right now)

[Chris Henson]

So now all library notes, including downstream uses, fall under the _root_.LibraryNote namespace? This seems like an improvement to me.

I suppose you could have library_note take an optional top level namespace to nest under if you wanted to differentiate where they were added similar to what Mathlib has currently, but maybe that's unnecessary.