search

leanprover / doc-gen4

Document Generator for Lean 4
Apache License 2.0
62 stars 41 forks source link

Auto-generated lemmas appear before declaration #163

Open alreadydone opened 9 months ago

alreadydone commented 9 months ago

For example, FundamentalGroupoid.ext_iff appears before FundamentalGroupoid, completelyRegularSpace_iff appears before CompletelyRegularSpace, Pi.nonUnitalRingHom_apply appears before Pi.nonUnitalRingHom. These are due to the attributes @[ext], @[mk_iff], and @[simps] respectively. The additive version produced by @[to_additive] also comes before the multiplicative version (e.g. EckmannHilton.AddZeroClass.IsUnital) but those don't necessitates a fix.

(Inspired by #161 which is also about ordering)

hargoniX commented 9 months ago

doc-gen sorts declarations according to their declared line number: https://github.com/leanprover/doc-gen4/blob/96147eaa0c066a95210fe5518c987e77be034b9f/DocGen4/Process/Analyze.lean#L145 if the declared line number of the generated things was below the original things it would sort correctly.