FreeAlgebra.Rel

Stream: mathlib4

[Utensil Song]

I am reading the code in docs#FreeAlgebra.Rel and I have 2 questions:

1. the comments are ported incorrectly, it has something incorrect like central_scalar {r : R} {a : Pre R X} : Rel (r * a) (a * r)-- commutative additive semigroup which mistakenly omitted a line break and added one after it compared to mathlib 3, thus turns a opening comment into a line comment that looks like a summarizing comment.

It was confusing for me at first until I realized that it was a porting issue and became concerned about whether there are other cases like this in Mathlib 4. I wonder: Can they be detected and semi-auto-fixed? Is there such tooling available?

2. FreeAlgebra.Rel re-stated lots of Props of other type classes, then proved that it is an instance for these type classes. It works fine but I can't help to wonder: Why is this necessary? Is it still the best practice for similar constructs? Is the rationale documented somewhere for similar scenarios?

[Kevin Buzzard]

For 2 it might be that the typeclass inference system needed some help to find the right path. Sometimes it can't get from A to D quickly without hints saying "by the way you can go via B and C". Without the hints the system might be slower and need a heartbeat bump.

[Utensil Song]

In general yes, but I wonder about the specifics, or how to play with it to gain more insights on this.

[Utensil Song]

#mil introduced a few type class path tricks but there are many more drastically different variants, and library notes, porting notes, and implementation details do not cover them all.

[Ruben Van de Velde]

For 1, I don't think we're going to see anything automated, but feel free to open a PR to clarify

[Utensil Song]

#7824 (merged)

[Utensil Song]

/-- The canonical function `X → FreeAlgebra R X`.
-/
irreducible_def ι : X → FreeAlgebra R X := fun m ↦ Quot.mk _ m

renders to FreeAlgebra.ι = FreeAlgebra.wrapped✝.1 in Equations in docs#FreeAlgebra.ι where FreeAlgebra.wrapped✝is less readable than Lean code and it links to FreeAlgebra.wrapped._@.Mathlib.Algebra.FreeAlgebra._hyg.2002but it doesn't exist.

Is this a case that might be improved? @Henrik Böving

[Henrik Böving]

In principle sure, but this is not something that doc-gen can improve as far as I can tell. I only read what the environment has to offer for me. If that is these declarations then I link to them in that way. If the env has other stuff to offer I show that.

[Utensil Song]

Henrik Böving said:

In principle sure, but this is not something that doc-gen can improve as far as I can tell. I only read what the environment has to offer for me. If that is these declarations then I link to them in that way. If the env has other stuff to offer I show that.

Thanks, I thought it's something retrievable from environment. I'll keep it in mind and revisit when I learn more about what the environment has to offer in similar cases.

Doc-gen4 (and the old docgen) usually spell mathematics better than code, particularly when it flattens things so what's hidden in complicated hierarchy/induction in code is revealed in doc. But in some cases, the code expressed the semantics clearly in the un-elaborated form but lost in the elaborated result, like this one.