Multiline Comments Break Semantic Highlighting with rocks-lazy.nvim

[EmDash00]

Without a multiline comment:

With a multiline comment before:

Doing some prints to show the semantic tokens detected seems to show that adding the multiline comments doesn't change them.

[Julian]

Hey, thanks!

I can't reproduce this, what I see visually is the same in both cases which is:

Judging from the end of your comment when you say semantic highlighting I assume you just mean highlighting in general right? Semantic tokens are sent by the LSP, so if there were some broken behavior in which tokens were sent that'd be something we file upstream in the lean core repo. If lean.nvim's own (non-semantic token) extra highlighting were broken though obviously that's a bug here. Looking at the output of :Inspect on various places which seem to change highlighting in your screenshot, I don't see any difference with or without the multiline comment above.

Can you confirm perhaps some specific steps and what you see from :Inspect in places that change?

(Including the source code would be slightly helpful as well besides the screenshot)

[EmDash00]

Very odd indeed. :Inspect appears to show that after the block comment the syntax is leanBlockComment.

Here's me calling :Inspect on the "False" in the first example.

With comment:

Without comment:

Let me try to replicate with a minimal setup.

[EmDash00]

I replicated it with a minimal setup. You can find it over at EmDash00/LeanMinimal. I'm not sure if it's because I use rocks.nvim as my package manager. The minimal setup is bootstrapping though so it should install rocks.nvim. All you have to do after that is run :Rocks sync

[EmDash00]

Oh I nearly forgot to give the code. Here you go:

import Mathlib.Data.Nat.Prime.Defs

/- I mess things up. -/

example : (False) → (False) := λ h => h
example : (False) → (True) := λ h => True.intro
example : (True) → (True) := λ h => True.intro

[EmDash00]

Okay I seem to have found the issue. I was lazily loading the plugin using nvim-neorocks/rocks-lazy.nvim. I figured since you can load the plugin lazily with folke/lazy.nvim you could use Rocks' version of that. Sadly no. Here's the lazy loading code I used to try this. lsp_defaults just holds my default on_attach, capabilities, and flags.

I think in my hurry to replicate it, I must have forgotten to call :Rocks sync after deleting the code to lazily load it.

Simply loading the plugin in plugin/lean.lua doesn't have this issue. This is likely an issue with nvim-neorocks/rocks-lazy.nvim and I might open an issue there.

init.lua

require("lz.n").load("plugins")

lua/plugins/lean.lua

return {
  "lean.nvim",
  ft = { "lean" },
  after = function()
    local lsp_defaults = require("lsp_defaults")
    require("lz.n").trigger_load {
      "nvim-lspconfig",
      "plenary.nvim",
      "switch.vim",
      "satellite.nvim",
      "telescope.nvim",
    }
    require('lean').setup {
      lsp = {
        on_attach = lsp_defaults.on_attach,
        capabilities = lsp_defaults.capabilities,
        flags = lsp_defaults.flags
      },
      mappings = true
    }
  end
}

[Julian]

ft = lean looks slightly suspicious. This plugin defines the Lean filetype so you normally would need BufReadPre *.lean (and BufNew)

[EmDash00]

Ah that makes sense then. It might be good to merge in that filetypes upstream. Let me check the code in nvim-neorocks/rocks-lazy.nvim to see how they're loading the filetype.