Should namespaces be indented?

Stream: new members

[Markus Schmaus]

I think in Mathlib namespaces are generally not indented, but in the Lean Manual in the section on namespaces they are indented. The #style guide is silent on this issue.

[Kevin Buzzard]

Mathlib is pretty non-silent about the issue in some sense :-) I am not sure I've ever seen an indented namespace in mathlib, and I've seen a lot of namespaces.

[Damiano Testa]

To follow up what Kevin said, this is a sample of the counts of (total line count, lines in a namespace):

Mathlib/RingTheory/Polynomial/IntegralNormalization.lean                         (157,   137)
Mathlib/RingTheory/Polynomial/Nilpotent.lean                                     (169,   151)
Mathlib/RingTheory/Polynomial/Opposites.lean                                     (123,   99)
Mathlib/RingTheory/Polynomial/Pochhammer.lean                                    (367,   0)
Mathlib/RingTheory/Polynomial/Quotient.lean                                      (287,   265)
Mathlib/RingTheory/Polynomial/RationalRoot.lean                                  (139,   12)
Mathlib/RingTheory/Polynomial/ScaleRoots.lean                                    (157,   137)
Mathlib/RingTheory/Polynomial/Selmer.lean                                        (88,    64)
Mathlib/RingTheory/Polynomial/Tower.lean                                         (92,    65)
Mathlib/RingTheory/Polynomial/Vieta.lean                                         (195,   128)
Mathlib/RingTheory/PolynomialAlgebra.lean                                        (295,   142)
Mathlib/RingTheory/PowerBasis.lean                                               (517,   413)
Mathlib/RingTheory/PowerSeries/Basic.lean                                        (2840,  2749)
Mathlib/RingTheory/PowerSeries/WellKnown.lean                                    (209,   185)
Mathlib/RingTheory/Prime.lean                                                    (77,    0)

I would say that this is quite common:

• either, there is namespace X at the beginning, right after copyright and module docs and everything is in the namespace,
• or everything is in _root_.

Indenting namespaces would essentially mean indenting almost all lines of almost all files, which seems undesirable.

[David Loeffler]

I think that if a namespace (or section etc) contains enough code to span multiple screenfuls, then indenting it doesn't really add readability (and it makes the coveted 1-line proofs harder to get).

[Damiano Testa]

Fun fact: the only indented theorem that I could find in Mathlib is docs#QuotientGroup.mk_prod and it looks like a typo!

[Damiano Testa]

#7659: let's see whether this is desirable un-indentation! :smile:

[Eric Wieser]

I don't think anyone is advocating for the one-space indentation we see there!

[Markus Schmaus]

This makes sense and confirms my understanding about namespaces in Mathlib. And I guess the recommendation is to follow Mathlib. If this is the case, it would be less confusing for new members if the Lean Manual used this style as well, and maybe include it in the #style guide.

[Utensil Song]

My impression is there were explicit explanation of why it should not indent namespaces (and sections) in Lean, back in Lean 3 materials, even for nested namespaces. I could not find it now.

[Sebastian Ullrich]

lean4#2681

[Jireh Loreaux]

@Markus Schmaus thanks for pointing out this omission in #style. I have created a PR to address it.

[Jireh Loreaux]

I think a good way to think about this, although it's my own personal idea not necessarily sanctioned by the devs / community, is that anything that naturally alters the Environment (e.g., def, theorem, notation, etc.) should be a top-level (i.e., flush-left) item in the editor.

[Mario Carneiro]

By the way, one thing that really made it clear to me that it wouldn't really work to have indented namespaces, is that namespace/end are not scoping constructs in lean 4, unlike lean 3. People are probably aware that you can omit end at the end of files, so "your brackets don't have to match", but it's more than that: namespace and section commands don't really have to be paired with end at all, unless you imagine them as macro expanding to bracket clusters:

namespace A
  namespace B.C
      def foo := 1
    end C
    namespace D.E
        def bar := 1
  end B.D.E
  section F
    section
      def baz := 1
end A.F.«»

[Mario Carneiro]

(needless to say, you shouldn't write code like that :point_up: )

[Eric Wieser]

People are probably aware that you can omit end at the end of files,

This seems like a bad thing to me; I've had merge conflicts introduce section Foo section Foo, and not noticed because there was no corresponding end marker to flag the issue

[Mario Carneiro]

you could end up with the same merge conflict on the end markers though, right?

[Eric Wieser]

Yes, but it's less likely

[Mario Carneiro]

one advantage is that it means that you can always just truncate a file between commands and get something that is valid

[Mario Carneiro]

you would need some kind of #where like command to do that otherwise