## Stream: new members

### Topic: Style for section and namespace

#### Julian Berman (Sep 16 2020 at 01:25):

Is there a general style preference for whether the bodies of sections and namespaces are indented? mathlib seems generally not to, but https://leanprover.github.io/theorem_proving_in_lean/dependent_type_theory.html#variables-and-sections shows them indented

#### Julian Berman (Sep 16 2020 at 01:26):

(ISTM that it's slightly nicer to indent them especially if the namespace and section are named the same thing, otherwise the end is harder to interpret, but I'd obviously rather just follow the general custom if there is one)

#### Floris van Doorn (Sep 16 2020 at 01:31):

Years ago we indented every namespace or section, and now we never do it, because it didn't actually help much with readability.
I think the best way to avoid confusion is to not name your sections the same as your namespaces.

#### Julian Berman (Sep 16 2020 at 01:33):

Got it. Makes sense.

#### Julian Berman (Sep 16 2020 at 01:35):

Oh! Also (different topic, not sure if this is bad Zulip style...) -- your name is at the top of the lint file I'm trying to understand :) -- if I can, I see there's #lint, and #lint_all, and #lint_mathlib, but not something in between... Meaning, I want #lint_notmathlib -- because I want to lint all the things I import in a project, but not lint mathlib itself which isn't under my control

#### Julian Berman (Sep 16 2020 at 01:36):

Is that not a thing that I should want to do? Or, if so, I have to define that myself by basically doing some filtering and redefining something from tactic.lint.frontend?

#### Floris van Doorn (Sep 16 2020 at 02:23):

Yes, you can modify lint_mathlib a little bit to define #lint_myproject yourself. The relevant declarations are
src#lint_mathlib_cmd src#lint_mathlib src#lint_mathlib_decls and src#tactic.​get_mathlib_dir
Note that get_mathlib_dir is a hackish way of knowing where mathlib is, but you can modify it to your own project (by picking an arbitrary declaration in your own project).

#### Bryan Gin-ge Chen (Sep 16 2020 at 02:40):

Adding a feature to lint files in a particular folder would make a nice PR :wink:

Yeah

#### Julian Berman (Sep 16 2020 at 03:00):

I was going to offer/ask that but I held my tongue

#### Julian Berman (Sep 16 2020 at 03:01):

Let's see if I'm capable of writing that first :D

#### Eric Wieser (Sep 16 2020 at 07:30):

Floris van Doorn said:

Years ago we indented every namespace or section, and now we never do it, because it didn't actually help much with readability.

Sometimes I wish mathlib did indent section and namespace contents internally, because then I would be able to code-fold sections I'm not interested in. Vs code doesn't seem to know how to fold namespace unless the contents are indented.

#### Julian Berman (Sep 16 2020 at 12:44):

I'm no VSCode expert but that has to be possible

#### Julian Berman (Sep 16 2020 at 12:45):

Googling finds e.g. https://marketplace.visualstudio.com/items?itemName=maptz.regionfolder which is more like manual folding but I'm sure poking in there will reveal what the vscode equivalent of vim's foldexpr or foldmethod are, presumably there should be some way to define folding regions

Last updated: May 14 2021 at 06:16 UTC