Support for simultaneous lean3/lean4 (in separate windows/tabs) #35

rish987 · 2021-06-02T19:44:40Z

Depends on a merge of nvim-lspconfig that adds lean4 as a new language server.

…ncy; broken infoview.

syntax/lean.vim

README.rst

ftplugin/lean4/switch.vim

indent/lean.vim

lua/lean/lsp.lua

…an4, minor README changes.

Julian

I still haven't tried actually using this yet so I don't have functional feedback yet, but just a few things that I'm thinking about:

I'm not sure yet whether personally I expect per-window infoviews or per-tab infoviews -- what I had in mind was the latter (so switching between windows on one tab would reuse the same shared infoview). I'm guessing from scanning this that you did the former, which I guess may also be reasonable, but yeah I want to see how natural that feels
Probably what we were discussing on Zulip affects the lspconfig PR as well -- namely when you modify the LSP there we should consider already whether to modify the leanls one to look for a lean3 filetype (instead of lean which is what it looks for now)
I think the default behavior you have here is the opposite of the current one if I read it right, namely the current code chooses lean 4 by default if there's no leanpkg.toml in the cwd, whereas I think here you default to lean 3?

Will try to leave some more comments as soon as I get a chance to set this up fully. And thanks again!

ftplugin/lean4/lean.vim

Julian · 2021-06-03T09:01:39Z

lua/lean/util.lua

+local uv = vim.loop
+local M = {}
+
+-- M.path copied from lspconfig/util to avoid creating a dependency...


lspconfig is Apache 2.0 licensed so in theory we're supposed to add the little blurb here.

syntax/lean.vim

rish987 · 2021-06-03T14:34:27Z

I'm not sure yet whether personally I expect per-window infoviews or per-tab infoviews -- what I had in mind was the latter (so switching between windows on one tab would reuse the same shared infoview). I'm guessing from scanning this that you did the former, which I guess may also be reasonable, but yeah I want to see how natural that feels

I think it makes the most sense for per-window/per-tab to be a configurable option. On larger screens, per-window infoviews could be more convenient. Working on this now...

Julian · 2021-06-03T15:10:27Z

README.rst

-       4-only.
+Note that many simple syntactical things are not yet implemented
+(help is of course welcome), and that ``tree-sitter-lean`` is lean
+4-only.

 Installation
 ------------


Should remove line 37 here suggesting installing lean.vim I suppose

Julian

This is starting to look great!

lua/lean/init.lua

Julian · 2021-06-03T16:20:51Z

lua/lean/infoview.lua

-    vim.api.nvim_win_close(M._infoviews[src_win].win, true)
+function M.close_win(src_winnr)
+  if M._infoviews[src_winnr] then
+    vim.api.nvim_win_close(M._infoviews[src_winnr].win, true)
  end

  -- NOTE: it seems this isn't necessary since unlisted buffers are deleted automatically?


I added this I believe while seeing tests fail for different reasons and causing later tests to fail. But it's possible it indeed isn't necessary. If it doesn't seem to be, feel free to kill it.

lua/lean/infoview.lua

…in().

…rrors in per-tab mode.

…tab mode causes infoview to close.

rish987 · 2021-06-08T19:43:05Z

This is expected - when you enter per-window mode, the tab's infoview is closed, and infoviews will only be opened in other windows when you trigger CursorHold (i.e. M.update())

rish987 · 2021-06-08T23:06:58Z

@Julian You can put your review on pause for a bit - I'm going to slightly refactor things to put them clearly in terms of persistent infoview state between close/open. Should result in a bit simpler code.

lua/lean/infoview.lua

rish987 · 2021-06-09T03:44:59Z

Alright I've done the refactor with a good amount of testing. The code is a bit longer (because of some utility functions), but I find it conceptually simpler. It's ready for you to check out here: https://github.com/rish987/lean.nvim/tree/infoview_persistence_refactor

This refactor should significantly help us in the future, as we implement many new kinds of infoview states that should persist when the window is closed/opened. Though it's up to you whether you want it to go in this PR or a future one. What we have now should be functional enough already if you want to put this off for a bit.

An unexpected immediate benefit of this refactor is that we can now preserve open/close states between :LeanInfoPerTab and :LeanInfoPerWin changes:

https://asciinema.org/a/7AfLVjFzx0F3jVS71sIXK1uJm

I'm going to do a bit more testing tomorrow morning... have to start a compile of the latest Lean nightly so I can try out the new term goal stuff

Julian · 2021-06-10T09:11:04Z

Making some progress here -- I pulled out the piece that fixes #20. In the process I introduced some merge conflicts, sorry, will get to fixing them as I keep merging pieces.

The next thing I want to do is remove the erase logic and alongside it _infoviews_open (like we discussed above) and just have closed, until we get to persistent windows.

Julian · 2021-06-10T10:50:54Z

Aha, ok now re-watching the demo from your last comment, I see finally at least some of the functionality you were implementing beyond the above list -- you want persistent window layout even when switching back and forth too.

That makes sense to me too, and explains why things are implemented this way (with the 2 state open), but yeah a bit of this is why I'm finding understanding the implementation hard to follow step-by-step.

lua/lean/infoview.lua

We can add close support if/when it's needed to preserve state.

There are lots of issues in the repo which likely constitute some form of roadmap but who knows what order we'll get to them in. The infoview section probably belongs, but we can document closing and quitting if/when we have persistent windows.

Things work differently on this branch where the check for opening the infoview is done on each update loop, so this actually is broken (but I broke it in an earlier commit). I don't yet see why to do it that way (to check whether to open an infoview) rather than just when entering new lean buffers , but merging this in anyways since I already broke it here and will need to rejigger update() to fix it.

It's true, but it's way too early to mention prominently or think about too hard, other than keeping Lean3 related code in the same place rather than scattered across the plugin.

This makes it a hard dependency for now, but I'd rather do that than copy paste in its path manipulation, at least for the moment. We can worry about removing that dependency later if we want to.

Closes: Julian#13. Co-authored-by: Rishikesh Vaishnav <[email protected]>

rish987 · 2021-06-11T12:44:31Z

lua/lean/infoview.lua

@@ -257,13 +246,7 @@ function M.close_win_wrapper(src_winnr, src_tabnr, close_info, already_closed)
    end
  end

-  if close_info then


The removal of this distinction results in E855: Autocommands caused commands to abort when closing the last (Lean) window in a tab with :close - I don't think WinClosed is designed to be able to handle physically closing other windows. From :help QuitPre: Can be used to close any non-essential window if the current window is the last ordinary window. No similar support exists for WinClosed.

rish987 · 2021-06-11T12:57:13Z

lua/lean/infoview.lua

@@ -280,8 +280,17 @@ end
 -- Close the infoview associated with the current window.
 function M.close()
  if not M.is_open() then return end
+  local infoview = M._teardown(get_idx())


What's being done here seems to be identical to what close_win() was doing previously - looks like this was an attempt to fix window closing/toggling? See latest commit.

What I was trying to do overall is to get rid of close_win and close_win_raw vs. close_win_wrapper, and handle their functionality in infoview.close() for the functionality of "close this window" and an autocmd for "a window was closed, possibly via another means than infoview.close maybe update the sizes of things and clean up state".

Don't quite get it yet - feel free to have a go at it and maybe I'll understand once I see the code.

Julian · 2021-06-11T13:30:57Z

Jumped on some work calls which means putting this on hold at least for a few hours, but I see you're already fixing more mistakes of mine -- what I'm trying to do at a high level is two things:

the first is in this comment, namely to incrementally understand what code is required for what functionality
the second, really part of the first, is a lot of code (nearly all of it) was moved here into the update function -- that seems quite odd to me, rather than the way things were done previously where events (autocmds) essentially are added or removed when associated windows come into being. I fully expect that something may require this kind of thing (it may even be what you pointed out about tabs), but because I can't put my finger on what that is yet, and all the functionality I've crossed off in that comment is merged already to main and works with the single-infoview setup, I want to get to where it's obvious what functionality is driving a design change here. Hopefully that makes sense.

In order to do the above I've been really doing some quite bad things, but it's the best I can come up with to untangle at the minute :/

Let me review your comments (and thanks again for fixing!)

rish987 added 10 commits June 1, 2021 15:57

Implement lean3 vs. lean4 filetype detection; remove lean.vim depende…

d7e0685

…ncy; broken infoview.

Fix infoview.

1de6b3b

Fix 4-second lean4 updatetime.

cd18592

Implement multi-tab infoview.

d6ea036

Fix infoview toggle.

70dca5d

Index infoviews by windows rather than buffers.

5976501

Update README and add infoview server startup grace period.

23522d4

Merge remote-tracking branch 'upstream/main' into main

f15f610

More README notes and add all remaining lean.vim files.

c2db67d

README formatting.

f9ac13a

gebner reviewed Jun 2, 2021

View reviewed changes

gebner referenced this pull request in neovim/nvim-lspconfig Jun 2, 2021

Add lean4ls and improve Lean root directory search.

e6cc39c

rish987 added 3 commits June 2, 2021 18:03

Bring syntax files up-to-date, duplicate plugin files from lean to le…

edeaa70

…an4, minor README changes.

Remove some lean3 switch mappings from lean4.

81ab591

Update indent file for lean4.

e6c4656

Julian reviewed Jun 3, 2021

View reviewed changes

Remove lean4 executable path stuff from README.

50953f9

Julian reviewed Jun 3, 2021

View reviewed changes

Implement dynamically configurable per-tab/per-window option.

7a90e25

Julian reviewed Jun 3, 2021

View reviewed changes

rish987 added 9 commits June 3, 2021 11:13

Slight refactor of infoview.lua.

b9e0576

Fix default one_per_tab setting.

d3ebca1

Merge remote-tracking branch 'upstream/main' into main

0a9a20f

Fix some remaining instances of indexing solely by nvim_get_current_w…

bcef288

…in().

Rename src_winnr -> src_idx (readability).

126690c

Get seemingly working auto-infoview-close functionality, but throws e…

5d45699

…rrors in per-tab mode.

Fix closing single source with multiple source windows in tab in per-…

adf970d

…tab mode causes infoview to close.

Refactor autocmds.

d039630

Remove debug print, minor formatting.

333c84a

rish987 commented Jun 9, 2021

View reviewed changes

lua/lean/infoview.lua Outdated Show resolved Hide resolved

Merge remote-tracking branch 'upstream/main' into main

beef5e4

Julian mentioned this pull request Jun 10, 2021

Configurably autoclose the infoview if it has no Lean buffers updating it #43

Open

rish987 commented Jun 10, 2021

View reviewed changes

lua/lean/infoview.lua Outdated Show resolved Hide resolved

rish987 and others added 14 commits June 10, 2021 11:25

Revert a couple ternary refactors and minor close_win_wrapper() fix.

24a4137

For now, always erase infoviews.

d48c9f8

We can add close support if/when it's needed to preserve state.

Pull in some upstream changes.

e73cc6d

Remove dead code.

c63b1eb

Remove some sections from the README.

f97b0a0

There are lots of issues in the repo which likely constitute some form of roadmap but who knows what order we'll get to them in. The infoview section probably belongs, but we can document closing and quitting if/when we have persistent windows.

Pull in the max_width change.

1033ed2

Pull in the augroup helper

0e3e2f6

Use is_lean3_project in _update to detect lean3 projects.

01d6f99

Guard against lean3ls not existing yet until the PR is merged.

e3b1063

Remove the note about Lean3 being removed in the future.

ac92804

It's true, but it's way too early to mention prominently or think about too hard, other than keeping Lean3 related code in the same place rather than scattered across the plugin.

Use lspconfig.util to find leanpkg.toml

6cb1154

This makes it a hard dependency for now, but I'd rather do that than copy paste in its path manipulation, at least for the moment. We can worry about removing that dependency later if we want to.

Get rid of lean3.detect if we already have ft.detect.

58da940

Properly detect leanpkg.toml relative to the lean file, not cwd.

3cdad44

Closes: Julian#13. Co-authored-by: Rishikesh Vaishnav <[email protected]>

rish987 commented Jun 11, 2021

View reviewed changes

Fix infoview closing.

eb4cd45

rish987 commented Jun 11, 2021

View reviewed changes

rish987 closed this Jun 12, 2021

rish987 mentioned this pull request Jun 13, 2021

Add Lean 4 syntax support. #54

Merged

rish987 mentioned this pull request Sep 1, 2021

Per-window infoviews #128

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Support for simultaneous lean3/lean4 (in separate windows/tabs) #35

Support for simultaneous lean3/lean4 (in separate windows/tabs) #35

rish987 commented Jun 2, 2021

Julian left a comment

Julian Jun 3, 2021

rish987 commented Jun 3, 2021

Julian Jun 3, 2021

Julian left a comment

Julian Jun 3, 2021

rish987 commented Jun 8, 2021

rish987 commented Jun 8, 2021 •

edited

Loading

rish987 commented Jun 9, 2021

Julian commented Jun 10, 2021

Julian commented Jun 10, 2021

rish987 Jun 11, 2021

rish987 Jun 11, 2021

Julian Jun 11, 2021

rish987 Jun 11, 2021

Julian commented Jun 11, 2021 •

edited

Loading

Support for simultaneous lean3/lean4 (in separate windows/tabs) #35

Support for simultaneous lean3/lean4 (in separate windows/tabs) #35

Conversation

rish987 commented Jun 2, 2021

Julian left a comment

Choose a reason for hiding this comment

Julian Jun 3, 2021

Choose a reason for hiding this comment

rish987 commented Jun 3, 2021

Julian Jun 3, 2021

Choose a reason for hiding this comment

Julian left a comment

Choose a reason for hiding this comment

Julian Jun 3, 2021

Choose a reason for hiding this comment

rish987 commented Jun 8, 2021

rish987 commented Jun 8, 2021 • edited Loading

rish987 commented Jun 9, 2021

Julian commented Jun 10, 2021

Julian commented Jun 10, 2021

rish987 Jun 11, 2021

Choose a reason for hiding this comment

rish987 Jun 11, 2021

Choose a reason for hiding this comment

Julian Jun 11, 2021

Choose a reason for hiding this comment

rish987 Jun 11, 2021

Choose a reason for hiding this comment

Julian commented Jun 11, 2021 • edited Loading

rish987 commented Jun 8, 2021 •

edited

Loading

Julian commented Jun 11, 2021 •

edited

Loading