Broken reference

Stream: mathlib4

[Violeta Hernández]

Randomly noticed the first reference here is broken
https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Jordan/Basic.html

[Violeta Hernández]

Is there a way to fix it without exceeding the 100 character per line limit?

[Damiano Testa]

There is an analogous issue in exactly one other place in mathlib that you can find by grepping set_option linter.longLine false in (untested).

[Damiano Testa]

Basically, you segment the doc-module string and silence the syntax linter by setting the option.

[Damiano Testa]

Then you add an exception to the text-based linter.

[Damiano Testa]

I wanted to remove the need for the second silencing, but have not gotten around to it.

[Damiano Testa]

(On mobile, sorry for the terse instructions.)

[Damiano Testa]

Also, I'm not too happy about long references having to be "fixed" like this, but I could not find a better way of automatically excluding them from the linter.

[Damiano Testa]

URLs are excluded by automatically ignoring lines containing http as a substring, but these [...][...] references are trickier.

[Violeta Hernández]

It'd be nice if there were a mechanism for dealing with this within the Markdown itself. Maybe a line could have a trailing \ to signal that whitespace/newlines immediately following it should be ignored?

[Violeta Hernández]

/-- This is a veeeeeeeeee\
  eeeeery long word! -/

[Damiano Testa]

Would the reference survive that, though?

[Violeta Hernández]

This would be a very early step in parsing, so it should treat it as if it were just a long line

[Violeta Hernández]

I don't know how/if this could be implemented, though

[Violeta Hernández]

What's the GitHub repo for the tool building the documentation?

[Bryan Gin-ge Chen]

It's here: https://github.com/leanprover/doc-gen4

(The repo containing the workflow that actually builds and deploys mathlib4 docs is here)

[Damiano Testa]

Would the substring <!----> in a doc-module/doc-string be displayed by doc-gen?

[Damiano Testa]

Damiano Testa said:

There is an analogous issue in exactly one other place in mathlib that you can find by grepping set_option linter.longLine false in (untested).

The exception is in Mathlib/Data/QPF/Multivariate/Basic.lean

/-!
...
each proves that some operations on functors preserves the QPF structure
-/

set_option linter.longLine false in
/-!
## Reference

[Jeremy Avigad, Mario M. Carneiro and Simon Hudon, *Data Types as Quotients of Polynomial Functors*][avigad-carneiro-hudon2019]
-/

[Damiano Testa]

If <!----> in doc-module strings is "invisible" to doc-gen, then the linter could ignore lines containing it as well.

[Yaël Dillies]

We already ignore lines containing http (or something like that) in the long lines linter(s). Can't we ignore lines that contain [...](...) or [...][...]?

[Damiano Testa]

Yes, but that may also ignore some (not properly spaced) assumptions in a lemma.

[Yaël Dillies]

Well, hopefully someone will write a separate linter against that? :wink:

[Damiano Testa]

Actually, Jon reviewed my "pedantic linter" that does check for whitespace issues!

[Damiano Testa]

However, that linter is really too strict, so the expectation is that it is not run by default.

[Damiano Testa]

For seriously linting style there should probably be a formatter for lean code.

[Violeta Hernández]

There's another one here: https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/Artinian.html

[Violeta Hernández]

[samuel]