Style for section and namespace

Stream: new members

[Julian Berman]

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]

(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]

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]

Got it. Makes sense.

[Julian Berman]

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]

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]

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]

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

[Julian Berman]

Yeah

[Julian Berman]

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

[Julian Berman]

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

[Eric Wieser]

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]

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

[Julian Berman]

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