new nvim behavior for accomplished goals

Stream: mathlib4

[Antoine Chambert-Loir]

The new nvim behavior for accomplished goals hides most of the file, and I don't find this convenient. Could someone help me to deactivate it?

[Matthew Ballard]

Screenshot 2025-04-03 at 8.38.23 AM.png
This is very festive

[Antoine Chambert-Loir]

image.png

[Matthew Ballard]

I am not sure I have updated my nvim plugins recently though...

[Julian Berman]

Antoine Chambert-Loir said:

image.png

I don't understand what's happening here, you're seeing literally the contents of buffers hidden?

[Julian Berman]

If you want to turn this off hopefully these instructions help: https://github.com/Julian/lean.nvim/wiki/The-lean.nvim-Manual#goal-markers -- set infoview = { goal_markers = { accomplished = '' } } -- and of course if most people want it off I can turn it off for everyone by default, what I did now is try to match the new vscode-lean4 behavior but I also find them a bit noisy myself

[Johan Commelin]

That screenshot is taking proof irrelevance to a new level (-;

[Julian Berman]

Matthew Ballard said:

This is very festive

(not sure if this was just meant as an amusing comment or if you are indeed asking for different behavior, but just to share context, in VSCode this looks like:

Screenshot 2025-04-03 at 08.56.53.png

but the double check mark isn't a unicode character, in VSCode the sign column uses images, so I had to pick a default of some character -- and given the other supported option in VSCode is this tada emoji, I just went with that for now, thinking we can do whatever people want after)

[Marc Huisinga]

(By the way, in VS Code you can also change the icon to :octopus: or :tada: if you don't find those icons to be too noisy compared to the checkmarks :-))

[Antoine Chambert-Loir]

It might be a color scheme problem… What surprises me is that it appeared at once.

[Julian Berman]

@Antoine Chambert-Loir I'm still trying to understand what you see! Your buffer is totally blank?

[Antoine Chambert-Loir]

No, it's just written in the same color as the background. When I highlight it, it appears… But this is clearly an issue of the lean/neovim interface because it is OK until the file has been processed by Lean.

[Julian Berman]

Ah interesting -- can you perhaps tell me what you get from running :Inspect (capital I) on top of some invisible text?

[Julian Berman]

It will indeed probably (hopefully??) just be a colorscheme issue

[Antoine Chambert-Loir]

Syntax
  - leanEncl

Extmarks
  - leanGoalsAccomplished lean.goal.markers
  - LspReferenceText nvim.lsp.references

[Antoine Chambert-Loir]

or

Syntax
  - leanOp links to Operator

Extmarks
  - leanGoalsAccomplished lean.goal.markers

[Julian Berman]

And are those words themselves colored in strange colors?

[Julian Berman]

Usually they should be colored whatever color the text is colored

[Antoine Chambert-Loir]

image.png

[Antoine Chambert-Loir]

image.png

[Julian Berman]

So no that looks fine

[Julian Berman]

Can you try a different colorscheme just to see?

[Antoine Chambert-Loir]

Here, I'm selecting some stuff and it appears.
image.png

[Antoine Chambert-Loir]

Which colorscheme could I try?

[Julian Berman]

kanagawa is what I use: https://github.com/rebelot/kanagawa.nvim

[Julian Berman]

Though I've never seen anythign this bad with any colorscheme -- can you tell me which one you're using as well so I can see whether I can reproduce?

[Julian Berman]

Are your dotfiles public perhaps?

[Antoine Chambert-Loir]

https://github.com/AntoineChambert-Loir/nvim

[Julian Berman]

Haaa ok I see the issue, and Johan is more right than he thought he was.

[Antoine Chambert-Loir]

???

[Julian Berman]

The issue is that kickstart I guess changes the default for conceallevel to 2, which is basically "hide any text that is concealable"

[Julian Berman]

So set conceallevel=0 which is the default will bring everything back again, but I'm trying to see whose "fault" this is

[Antoine Chambert-Loir]

(I am trying to install kanagawa but that seems to be beyond my skill level)

[Julian Berman]

Yes forget about that it's not a color scheme issue

[Julian Berman]

conceal is kind of like folding, it's for hiding things when you don't want to see them

[Julian Berman]

changing that default seems very strange to me

[Antoine Chambert-Loir]

Still: once I have downloaded the kanagawa files, what do I need to know to make nvim knowledgeable about them?

[Julian Berman]

You shouldn't need to download it yourself, just uncommenting this line: https://github.com/AntoineChambert-Loir/nvim/blob/b6bdf3b70063da7acfe8169bed2d823987faaf13/lua/lazy-plugins.lua#L292 and https://github.com/AntoineChambert-Loir/nvim/blob/b6bdf3b70063da7acfe8169bed2d823987faaf13/lua/options.lua#L54 that one, and commenting out the cappuccin ones