Zulip Chat Archive

Stream: general

Topic: curly braces


Johan Commelin (Nov 11 2021 at 19:03):

Following up on the indentation linter, #10280 adds a curly braces linter.
This might be somewhat controversial. But I firmly believe that there is a net gain from having these linters. The way mathlib styles { .. }-blocks is somewhat unusual compared to what is common in other languages. (But I've become very fond of our style!) Anyway, I think this linter will help newcomers to style their {} correctly.
It comes with scripts that automatically reflow offending lines.

Riccardo Brasca (Nov 11 2021 at 19:27):

What about conv? In the examples in the doc the syntax is something like

conv_lhs {
...
}

For example here

Johan Commelin (Nov 11 2021 at 19:32):

Hmm, then I propose that we update the doc

Kyle Miller (Nov 11 2021 at 20:41):

Should spaces between closing curly braces be part of the linter? I saw this:

  suffices : p  q  p.num * q.denom  q.num * p.denom, by
  { split; intro h,
    { exact lt_iff_le_and_ne.elim_right h.left, (this.elim_left h.right)⟩ },
    { have tmp := lt_iff_le_and_ne.elim_left h, exact tmp.left, this.elim_right tmp.right }},

https://github.com/leanprover-community/mathlib/pull/10280/files#diff-a6293477a7756230fad4d65d40f466a069910ccef462a6698e5a7d5223fd8596R144

Johan Commelin (Nov 11 2021 at 20:43):

Ideally, yes. But what about nested set-builder notation?

-- we want some singleton in `set (set X)`
exact {{x | P x}}

Kyle Miller (Nov 11 2021 at 20:53):

Oh, I see now, the rule is literally about lines ending or starting with { and }. That seems like a nice and simple rule.

Mario Carneiro (Nov 11 2021 at 21:02):

If you can do bracket matching, one way to do it is to say that a space/comma/newline should follow a bracket whose matching pair is the first thing on the line. It still has false positives, but I don't think you can do better without using the ast data

Johan Commelin (Nov 11 2021 at 21:08):

I'm inclined to go with the stupid simple thing that this PR does. It will catch most of the mistakes that I flag during PR reviews.

Kyle Miller (Nov 11 2021 at 21:17):

If you did bracket matching, you'd probably also have to do string parsing, since for example {{ is how you escape curly braces in format!.

Mario Carneiro (Nov 11 2021 at 21:19):

no, because brackets still match

Mario Carneiro (Nov 11 2021 at 21:20):

It is possible to write unmatched brackets in comments but that is enough of an edge case that I don't think it is worth worrying about

Kyle Miller (Nov 11 2021 at 21:21):

The brackets don't match in format! though, since it's format!"foo {{bar} baz" to get foo {bar} baz

Mario Carneiro (Nov 11 2021 at 21:21):

isn't it format!"foo {{bar}} baz"?

Kyle Miller (Nov 11 2021 at 21:22):

What do you think about normalizing whether there's a comma at endings, like }, }, }, },? While I'm usually one to include these, it seems like banning close curly, any number of spaces, comma, any number of spaces, curly wouldn't break anything.

Mario Carneiro (Nov 11 2021 at 21:22):

even if what you wrote works I don't think it should be considered good style

Kyle Miller (Nov 11 2021 at 21:22):

Mario Carneiro said:

isn't it format!"foo {{bar}} baz"?

That gives foo {bar}} baz

Mario Carneiro (Nov 11 2021 at 21:23):

clearly we need to fix that then

Mario Carneiro (Nov 11 2021 at 21:23):

or use \{

Kyle Miller (Nov 11 2021 at 21:23):

Can format see the backslash escape though? It's getting a parsed string I believe.

Mario Carneiro (Nov 11 2021 at 21:24):

maybe \\{ then

Mario Carneiro (Nov 11 2021 at 21:24):

some string parsers fall back to literal inclusion of the backslash, in which case it's not needed

Kyle Miller (Nov 11 2021 at 21:26):

This would be a curly brace fix for lean/library/init/meta/interactive_base.lean:

private meta def parse_format : string  list char  parser pexpr
| acc []            := pure ``(to_fmt %%(reflect acc))
| acc ('\n'::s)     :=
do f  parse_format "" s,
   pure ``(to_fmt %%(reflect acc) ++ format.line ++ %%f)
| acc ('{'::'{'::s) := parse_format (acc ++ "{") s
| acc ('{'::s) :=
do (e, s)  with_input (lean.parser.pexpr 0) s.as_string,
   '}'::s  return s.to_list | fail "'}' expected",
   f  parse_format "" s,
   pure ``(to_fmt %%(reflect acc) ++ to_fmt %%e ++ %%f)
| acc ('}'::'}'::s) := parse_format (acc ++ "}") s  -- new
| acc ('}'::s) := fail "'}}' expected"  -- new
| acc (c::s) := parse_format (acc.str c) s

Mario Carneiro (Nov 11 2021 at 21:27):

just what I was going to say

Mario Carneiro (Nov 11 2021 at 21:27):

(also this has to be fixed in mathport, which also parses format strings)

Kyle Miller (Nov 11 2021 at 21:29):

Lean 3 complains about invalid escape sequences in strings, so it'd be \\{ if you wanted to go that way

Mario Carneiro (Nov 11 2021 at 21:29):

I think I prefer the {{ }} escapes

Mario Carneiro (Nov 11 2021 at 21:30):

also it's simpler since you don't have to worry about escaping \

Johan Commelin (Nov 12 2021 at 04:07):

@Mario Carneiro @Kyle Miller I'm lost about what exactly this is now about. Would you mind pushing to the PR if you have improvements?

Johan Commelin (Nov 12 2021 at 05:04):

This PR is already attracting merge conflicts. If people like this change, is it ok to defer improvements to a later PR?

Mario Carneiro (Nov 12 2021 at 05:10):

The {{}} escape thing is independent of this PR (and it has been PR'd as lean#650)

Johan Commelin (Nov 12 2021 at 05:13):

Aha, thanks for clarifying

Arthur Paulino (Nov 12 2021 at 13:05):

Would it be possible to have something like this accessible locally via, say, leanproject format?

Arthur Paulino (Nov 12 2021 at 13:16):

Or something less dangerous, that allows formatting particular files. Because you usually don't want to have a PR that formats the whole repository :sweat_smile:

Johan Commelin (Nov 15 2021 at 19:25):

What do people think of #10280. Objections against merging it?

Yaël Dillies (Nov 15 2021 at 20:22):

Fine to me!

Johan Commelin (Nov 17 2021 at 07:15):

Riccardo Brasca said:

What about conv? In the examples in the doc the syntax is something like

conv_lhs {
...
}

For example here

@Rob Lewis where do I modify this example? I can't find the source.

Mario Carneiro (Nov 17 2021 at 07:20):

https://github.com/leanprover-community/mathlib/blob/master/src/tactic/doc_commands.lean#L369-L417

Johan Commelin (Nov 17 2021 at 07:34):

Nice. So my script automatically fixed it already (-;


Last updated: Dec 20 2023 at 11:08 UTC