lean.nvim does not highlight tactics

Stream: general

[Matei Adriel]

Hi! I am learning lean using the lean.nvim plugin. Is there any way to get it to highlight tactic code like the book?

[Yaël Dillies]

I'm sure @Julian Berman can pull it off.

[Julian Berman]

Hi hi. @Matei Adriel is this Lean 4 highlighting you're asking about? Or Lean 3?

[Matei Adriel]

@Julian Berman lean 4

[Julian Berman]

I see. For Lean 4 we're waiting for neovim to merge support for LSP syntax highlighting, which means it will be Lean itself that can draw proper syntax highlighting. That PR is here: https://github.com/neovim/neovim/pull/15723 so you can follow that.

[Julian Berman]

There are some things we could do in the interim but it's somewhat lower priority given that as soon as that PR (and a follow-up or two) is merged, things should just work.