Skip to content

Conversation

@stephen-huan
Copy link
Contributor

Purely vanity change, feel free to close if you think it's unnecessary!

Inspired by the goal completion message

After using rfl, the resulting state is:
All goals completed! 🐙

in the lean language reference. I was curious where this came from, and bisected it to leanprover/verso (41b85d4).

Technically the message for no goals can already be configured with vim.g.lean_no_goals_message, but this is an implementation detail and must be done with an autocmd like the following as the lsp itself sets it on initialization.

vim.api.nvim_create_autocmd("LspAttach", {
    group = "vimrc",
    pattern = { "*.lean" },
    callback = function()
        vim.g.lean_no_goals_message = "No goals!"
    end,
})

@stephen-huan
Copy link
Contributor Author

The macos tests seem a bit flaky, but I guess they're re-ran until they succeed?

@Julian
Copy link
Owner

Julian commented May 25, 2025

Thanks!

Technically the message for no goals can already be configured with vim.g.lean_no_goals_message but this is an implementation detail

Yeah this indeed was just meant as an implementation detail (and really just because of <4.19) -- though I did have this exact customization functionality on my TODO list (albeit quite low priority). So I'm happy to take a PR for it (thanks!) though what I had in mind originally was to allow specifying a table where the key is the number of goals and the value is the message (in other words e.g. lean.infoview.goals_message[n] should return the message for n goals, and so you'd override 0 if you want to change the goals accomplished message.

I'm not 100% bothered though with whatever configuration so I'm fine with just doing it as you have it -- though I would like a test. Could you try to have a look at that, you should be able to essentially cargo cult an existing spec file for this.

The macos tests seem a bit flaky, but I guess they're re-ran until they succeed?

Yeah I've put in a lot of work to try to get the test suite to be less flaky but there's still a bit of missing synchronization. If/when I find where it is I'll fix it, but as I say I've done a ton of that already to get us to this point where it at least passes most of the time. If you do see something specific that's missing (usually a missing wait) of course let me know.

@Julian
Copy link
Owner

Julian commented Jul 15, 2025

Hey @stephen-huan the CI flakiness should be fixed if you merge main -- lemme know if my comment made sense / if you're still interested in this PR!

@stephen-huan
Copy link
Contributor Author

Yep, it makes a lot of sense, thanks for the tips and fixing the ci! I've been super busy recently but I haven't forgotten about this and will ping you once I make my changes (probably in another few months...). Is that ok with you?

I can try to make some time next week, but no promises : )

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants