doc-gen print global doc-string first

Stream: mathlib4

[Damiano Testa]

Dear All,

maybe this has already been addressed, but I could not find it.

Suppose that there is a declaration such as

/-- Main doc -/
structure foo where
  /-- this is an implementation detail -/
  bar : String

I think that the documentation page would display this something like

structure foo
    this is an implementation detail
  bar : String
Main doc

Would it be possible/desirable to display Main doc first, and then everything else? Something along the lines of

structure foo
Main doc
    this is an implementation detail
  bar : String

I am bringing this up, since I just looked up docs#MeasurableSpace and the first thing that I read is Predicate saying that a given set is measurable. Use MeasurableSet in the root namespace instead. which confused me, until I realized that this was actually talking about docs#MeasurableSpace.MeasurableSet' instead!

[Eric Wieser]

Personally I think it should be

structure foo
  Main doc

  bar : String
    this is an implementation detail

It's jarring having some docstrings before the thing they document and others after

[Eric Wieser]

Though I think even with leaving the main doc in the same place, that would help; compare:

image.png
image.png

[Damiano Testa]

Eric, I like your suggestion. And I agree that with your suggestion I would probably not have been confused.

[Eric Wieser]

https://github.com/leanprover/doc-gen4/pull/137

[Damiano Testa]

Would making the list have bullets be an improvement?

[Eric Wieser]

I think that might be confusing for Nat, for which the corresponding versions are

image.png
image.png

[Damiano Testa]

Ah, sure, inductives already have their |. Maybe only for structures?

[Damiano Testa]

In any case, from what you showed earlier, I find the current change already a big readability improvement!

[Damiano Testa]

Eric, if I wanted to see the effect of the changes that you are putting in the PR, how could I do that?

[Damiano Testa]

(I mean, generating a sample doc-page -- the actual changes I can see in github! :upside_down: )

[Eric Wieser]

Damiano Testa said:

Eric, if I wanted to see the effect of the changes that you are putting in the PR, how could I do that?

Wait for @Henrik Böving to decide if the changes are good and for it to be merged if so... I previewed the change by manually tweaking the page in the web inspector.

[Henrik Böving]

Damiano Testa said:

Eric, if I wanted to see the effect of the changes that you are putting in the PR, how could I do that?

I have a local std4 laying around that I usually look at with a custom doc-gen

[Henrik Böving]

It's merged now, should be in the next update for mathlib's docs in a couple of hours

[Damiano Testa]

Thank you very much! Also, the docs are great -- I'm very grateful for all the work that goes into making it available for everyone!

[Damiano Testa]

The new format is live and I find it great! Thank you very much!