curly braces

Stream: general

[Johan Commelin]

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]

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

conv_lhs {
...
}

For example here

[Johan Commelin]

Hmm, then I propose that we update the doc

[Kyle Miller]

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]

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

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

[Kyle Miller]

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]

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]

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]

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]

no, because brackets still match

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Kyle Miller]

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]

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

[Kyle Miller]

Mario Carneiro said:

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

That gives foo {bar}} baz

[Mario Carneiro]

clearly we need to fix that then

[Mario Carneiro]

or use \{

[Kyle Miller]

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

[Mario Carneiro]

maybe \\{ then

[Mario Carneiro]

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

[Kyle Miller]

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]

just what I was going to say

[Mario Carneiro]

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

[Kyle Miller]

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

[Mario Carneiro]

I think I prefer the {{ }} escapes

[Mario Carneiro]

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

[Johan Commelin]

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

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

[Mario Carneiro]

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

[Johan Commelin]

Aha, thanks for clarifying

[Arthur Paulino]

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

[Arthur Paulino]

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]

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

[Yaël Dillies]

Fine to me!

[Johan Commelin]

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]

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

[Johan Commelin]

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