Via 'foldexpr' presumably.

Currently, :quitting the last Lean buffer in a tab leaves the infoview dangling in a detached state. Instead, it should automatically close the associated infoview, and :close should leave it in a detached state.

This will likely involve including the set of associated windows as part of the Infoview object, adding/removing these windows on Lean file BufEnter/BufExit, and once the last such buffer is exited, this will trigger the infoview to close as well. We should also make it (dynamically) configurable per-infoview whether or not this autoclose happens, in case someone doesn't like this -- that is, some kind of pin function that keeps the infoview around even when no Lean buffers are open.

Right now when opening /foo/bar/baz, we still look for leanpkg.toml in cwd.

Just the basics -- enter \a, assert conversion to alpha.

When you scroll down the infoview, it remembers the position. When the infoview then updates and the new content is shorter than the old one, you have an empty infoview. In that case it scroll back up again so that you at least see that it's not empty.

Similar to #26 in that I don't yet see how to deterministically reproduce, I occasionally get:

Error detected while processing CursorHold Autocommands for "*.lean":                                                                                                                                                                                                                       
E5108: Error executing lua /Users/julian/Development/lean.nvim/lua/lean/infoview.lua:37: attempt to index local 'result' (a number value)                                                                                                                                                   

when opening a lean file. Here it's rare, and only happens occasionally.

I don't know how result is getting to be a number there. Perhaps just ignoring it when it is will silence the error, but it'd be nice to know why it's happening.

Running :tabe with no filename, followed by :vsplit foo.lean–which both opens foo.lean as well as potentially autoopens an infoview–causes even foo.lean's size to be set to 50.

• Provide a unified API for (re)-configuring sub-functionality, rather than ad hoc functions like infoview.set_autoopen. Inspiration probably can be taken from vim.diagnostic.config (i.e. we probably should use a similar API).
• Unknown options provided to a config table should warn or error. Right now an unknown option is silently ignored, which allows typos (or mistakes due to backward incompatibility).

When the client has no connection to the lean server, it'd probably be nice if that was persistently shown in the infoview instead of just being in :messages.

Relates to #37 probably.

Given a sequence of tactics, load the goal state text at the end of each tactic into the quickfix list and allow a sequential (text) vimdiff of the state from one to the next.

When using the abbreviation support in compe, writing \mu and completing the mu will insert the mu but leave the slash in place, resulting in \µ in the buffer.

I cannot tell if this is a compe bug (e.g. that it is calculating ranges to remove on word boundaries or something) or me writing the compe code we have wrongly. Defining a .confirm() function seems like a possible way to evade even the possible bug.

(Filing this as another "known issue", though I have not been able to figure it out... :/)

compe also isn't tested in CI, which it should be alongside the snippets.nvim tests.

When first opening a file, the infoview doesn't display the first state of the file (until a second update e.g. by moving the cursor).

Most likely the CursorHold triggers before the server is ready.

Demo below (for Lean 3):

Creating a new Lean 3 file and putting #check "foo" in it doesn't seem to show a working LSP connection.

Lean 4 works fine, as does writing the new Lean 3 file then reopening it, where the LSP comes alive.

The goal counting and diagnostic-showing parts of the infoview work essentially unchanged on Lean3.

Just need a bit of refactoring to split apart the update function a bit better.

(The last item in #17 is obviously related, but this likely is a lot simpler to do for now).

Someone may want to have infoviews be closed by default, and selectively open them for specific tabs. Currently, setting enable = false disables infoviews altogether. Instead, this should be a "soft" option that just disables auto-open, still allowing for manual open if desired.

Another hard to reproduce bug, but often, I find diagnostics persist in a buffer even after the underlying issue has been fixed, and the diagnostic only disappears after re-editing the file.

neovim 0.5 should release today (July 2).

Once it does we can update the README and CI to use it (and thereby make CI not take ages on macOS)

If you've previously closed an infoview and enter a new tab and open a Lean buffer, the infoview doesn't auto-open. TDD test case here.

Because when an infoview is closed, its buffer is deleted. The solution seems to be to cancel all pending requests on infoview close.

In simple cases I think there are simple changes we can make.

E.g. probably we should set indentkeys+==where and := for Lean 4.

For more complex cases, if or when tree-sitter-lean is good enough to use, nvim-treesitter allows us to define indentation rules via it (via an indents.scm file).

Similar to VSCode, this should take a character under the cursor and show what abbreviation would produce it in a floating window.

I.e. allow for adding extra translations locally.

Add a configuration option infoview.autoclose = true (default) which indicates the infoview should be closed if no Lean buffers are updating it anymore (e.g. particularly if it is the last remaining window).

(Right now the cursor is left at the bottom).

Given multiple different suggestions in the diagnostics, it's probably better to decide which to insert via a normal pum / completion selection.

E.g. stripping _inst lines from the state.

Similar to VSCode, it should be possible to pin/unpin infoview messages.

VSCode seems to support "live" messages that are automatically updated as the surrounding code changes. To me this seems a bit unexpected, and I would prefer to just have pinned messages be permanently "paused" and only update when specifically requested. Not to mention this would make the code simpler. Obviously if someone wants to simulate live updates this could be done with autocmds. Though keep in mind I don't have as much experience writing Lean code myself as reading it, so do let me know if there are other opinions.

See here:

The solution should be similar to that of #77, also cancelling all requests at the beginning of every update() call so only the most recent one survives.

E.g. pass this test:

  -- Emitted by e.g. show_term
  it('replaces redundant term and tactic mode', helpers.clean_buffer([[
namespace tactic.interactive
meta def foo (t: itactic) : itactic :=
  (do tactic.trace "Try this: exact λ x y hxy, hf (hg hxy)\n")
end tactic.interactive

example {X Y Z : Type} {f : X → Y} {g : Y → Z} (hf : function.injective f) (hg : function.injective g) : function.injective (g ∘ f) :=
begin
  foo {
    intros x y hxy,
    apply hf,
    apply hg,
    apply hxy,
  }
end]], function()
    local expected = vim.api.nvim_buf_get_lines(0, 0, 5, true)

    vim.api.nvim_command('normal 8gg3|')
    helpers.wait_for_line_diagnostics()

    require('lean.trythis').swap()
    vim.list_extend(
      expected, {
        'example {X Y Z : Type} {f : X → Y} {g : Y → Z} (hf : function.injective f) (hg : function.injective g) : function.injective (g ∘ f) :=',
        'λ x y hxy, hf (hg hxy)',
      }
    )

    assert.contents.are(expected)
  end))

  -- Emitted by e.g. show_term
  it('replaces trythis messages before the position', helpers.clean_buffer([[
]], function()
    assert.is.same(2, 2)
  end))
end)

The relevant vscode-lean (3) heuristic is here: https://github.com/leanprover/vscode-lean/blob/8ad0609f560f279512ff792589f06d18aa92fb3f/src/tacticsuggestions.ts#L76

Given an execution of the simp tactic, show a completion menu that peeks the definition of all the lemmas used by the simp (without needing to replace the text inside the buffer).

Each README feature could likely benefit from a quick GIF or image showing it off.

The builtin abbreviation expansion inserts a trailing space when hitting both <Space> or <Tab>.

So foo x\1<Tab> expands to foo x₁ . This doesn't match my fingers' muscle memory for completion in general, which expect no space there, particularly if I'm inserting something in the middle of an existing line (e.g. in Lean 3 on a line like foo bar|, baz quux, where I'm going back to the middle of the line to insert something).

@gebner let me know if you prefer things this way (if so I suppose I can make it configurable)

These are a few other minor possible tweaks for the infoview. Some probably should be defaults, some configurable:

• have one infoview per :tab
• #171
• split the infoview horizontally if there are already two vertical splits on the tab when it is opened
• #172

In VSCode snippets, $CURSOR tells VSCode where to leave the cursor when expanding the snippet (and is immediately removed from the buffer).

We support this functional behavior when expanding snippets via snippets.nvim but not yet in the compe.nvim or builtin expanders.

The Lean server prints many fatal and not-so-fatal errors on stderr (like stack overflows, panics, assertion failures etc.). These should be shown somehow.

Maybe it'd be nice (and reasonably easy?) to have a list of simp-normal forms and to highlight non-simp-normal terms as warnings.

Zulip and the docs have an existing list of these kinds of terms.

If it's invoked from normal mode it should probably end up in normal mode.

(In addition to running against lean 3)

Unlike in vscode, diagnostics aren't underlining where they apply to.

This is true even though underline is on by default for e.g. native LSP client in neovim, so somehow that information either isn't being passed from the vanilla LSP lean server (and is being done in the vscode extension outside of the LSP server) or isn't being processed within neovim... Will have to hunt down which.

Lean 4's LSP server treats the didOpen and didClose notifications specially: it spawns a server process for every opened document. That is, closing a document stops the corresponding server process, and reopening the document causes Lean to restart the server process and the file starts parsing again from the beginning.

For neovim, this has the effect that only open buffers have a server process. For example, go-to-definition typically closes the current buffer and opens another buffer for the file with the definition. Then the Lean server starts parsing the new file.
When you go back to the original file, the Lean server kills the server process for the file with the definition. And it starts parsing the original file again from the beginning.

We might therefore want to set hidden (or something) by default.

(A prerequisite here is PRing a change to nvim-lspconfig and/or doing the appropriate dispatch here within this repo.)

The LSP (for Lean 3) doesn't natively lint, but there's a linter for mathlib in its repo which runs in mathlib CI.

I think that linter can be run via e.g. efm-langserver so that diagnostics populate if one is working on mathlib.

leanprover/vscode-lean#149 is likely relevant too.

Standalone files (i.e. not part of any project structure) are assumed to always be Lean 4, regardless of whether you had set elan default ... to be Lean 3.

Potential fix described at #81.

There are a number of neovim-based GUIs.

Some notable ones are:

uivonim
vimr
gnvim
vv

and likely more, given I don't personally stay too much on top of these. The first one is likely particularly interesting given it has contributors who are neovim core devs.

We currently support TUI-based widgets, but for more complex ones such as e.g. the sudoku solver which truly rely on HTML rendering, a GUI (with access to a real browser) is needed.

We could attempt to follow something like bracey's model even for terminal nvim by opening an optional browser window which updates not on save but on infoview update.

(probably wise to implement this after #84)

Like in VSCode, we should maintain a per-URI state describing the point in the file that the language server has reached, which is initialized to zero for each URI, updated on fileProgress server notification, and cleared once the file has been parsed (or some other indicator).

We can then short-circuit attempting to update the infoview if the current URI hasn't been fully processed yet, printing a Loading... message, and having the URI progress state trigger an update for all relevant messages on parse completion for that file.

When editing a Lean 4 file, I am getting the following kind of error very frequently:

LSP[leanls]: Error NO_RESULT_CALLBACK_FOUND: {
  id = 101,
  jsonrpc = "2.0"
}

Sometimes the response is clearly from autocompletion. Is there something obvious that I should be doing?

(and possibly implement autoinstalling it)

When I (accidentally) close the infoview buffer, the following error repeats very quickly:

Error executing vim.schedule lua callback: /home/gebner/lean.nvim/lua/lean/infoview.lua:61: Invalid buffer id: 3

It would also be nice to have commands to reopen or toggle the infoview.

In the infoview, it'd be nice if vim.lsp.buf.definition() (or hovering, etc.) on a term which is defined in the corresponding buffer functioned similarly to doing so in the original buffer -- i.e. jumps to the definition, etc.

Doing this for terms embedded in e.g. try this: messages would also be nice albeit require a bit more work.

In the infoview, the term goal support uses the current cursor position when requesting $/lean/plainTermGoal, whereas we shift forward by 1 column for the goal state, which is more ergonomic in vim.

However, in the hover support for :LeanPlainGoal and :LeanPlainTermGoal we shift forward for both.

I didn't check which behavior is correct, but given that Gabriel wrote the first one it's likely the correct one and I just didn't notice. Probably the code should be shared between the modules a bit better anyhow.