What is a bracket anyway?

Stream: lean4

[Steven Ulin]

I'm learning lean4 and I'm annoyed that when I type "section Foo ... end Foo" my syntax highlighter highlights "end" in red. The highlighter thinks that "end" is missing a matching "begin". See the language config for bracket. [1]

Should ["namespace", "end"] and ["section", "end"] also be considered brackets for consistency?

What do y'all think?

[1]: https://github.com/leanprover/vscode-lean4/commit/5b60161091add847def2c347c1f3d9d29708c029

[Bryan Gin-ge Chen]

Yes, that should probably be fixed. If that doesn't work, we could also consider removing ["begin", "end"].

[Steven Ulin]

I can throw together a quick pull request if you want. I'm not sure the what the etiquette is about small pull requests tho

[Chris B]

I would have thought this was a remnant of Lean 3's tactic syntax, but now I'm curious why "consistency with the vs-code verilog package" would be a desired feature in Lean's vscode extension.

[Chris B]

@Eric Wieser Can you elaborate on the tie-in with verilog/whether this would be safe to remove now that begin/end isn't used for tactics?

[Mario Carneiro]

end cannot be meaningfully construed as a bracket in lean 4:

namespace A
section C
namespace B
end A.C.B

namespace A.B
end B
end A

namespace Unclosed

[Chris B]

The one person who uses the macro begin/end will be very upset you said that.

[Kevin Buzzard]

I had problems with the begin/end macro in the manual, I can't remember the details, but I decided to switch to the lean 4 version because of them (basically because I didn't know enough about macro writing to diagnose and fix)

[Eric Wieser]

Note that that commit was made for the lean3 highlighter in the lean 3 repo

[Eric Wieser]

The verilog argument was simply "this other language uses begin/end in an analogous way, and their syntax highlighter decided to call it a bracket, so let's do it too"

[Eric Wieser]

Mario, is that valid in lean3 too?

[Mario Carneiro]

No

[Mario Carneiro]

namespace/end and section/end act like strict brackets in lean 3

[Mario Carneiro]

oh but you can use #exit while there are still unclosed namespaces/sections

[Steven Ulin]

Well here's a pull request so this discussion isn't forgotten https://github.com/leanprover/vscode-lean4/pull/41

I'm not a "GitHub collaborator" so I cannot add the "awaiting-review" label.

Thanks for taking the time to look at this yall! XD