Zulip Chat Archive

Stream: new members

Topic: Style for section and namespace


view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Julian Berman (Sep 16 2020 at 01:33):

Got it. Makes sense.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip 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:

view this post on Zulip Julian Berman (Sep 16 2020 at 03:00):

Yeah

view this post on Zulip Julian Berman (Sep 16 2020 at 03:00):

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

view this post on Zulip Julian Berman (Sep 16 2020 at 03:01):

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

view this post on Zulip 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.

view this post on Zulip Julian Berman (Sep 16 2020 at 12:44):

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

view this post on Zulip 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