Julian / lean.nvim

Neovim support for the Lean theorem prover
MIT License
277 stars 26 forks source link

Update for neovim/neovim#15585. #134

Closed rish987 closed 3 years ago

rish987 commented 3 years ago

This I believe covers it. Do you know what needs to be done for the backwards compatibility issue?

codecov[bot] commented 3 years ago

Codecov Report

Merging #134 (5cf0b3f) into main (eac7dbd) will decrease coverage by 0.00%. The diff coverage is 100.00%.

Impacted file tree graph

@@            Coverage Diff             @@
##             main     #134      +/-   ##
==========================================
- Coverage   93.82%   93.81%   -0.01%     
==========================================
  Files          36       36              
  Lines        2137     2134       -3     
==========================================
- Hits         2005     2002       -3     
  Misses        132      132              
Impacted Files Coverage Δ
lua/lean/trythis.lua 100.00% <100.00%> (ø)
lua/tests/helpers.lua 97.77% <100.00%> (ø)

Continue to review full report at Codecov.

Legend - Click here to learn more Δ = absolute <relative> (impact), ø = not affected, ? = missing data Powered by Codecov. Last update eac7dbd...5cf0b3f. Read the comment docs.

Julian commented 3 years ago

Thanks! I had some slightly tedious stuff locally that did:

diff --git a/syntax/leaninfo.vim b/syntax/leaninfo.vim
index ad70db7..08a184a 100644
--- a/syntax/leaninfo.vim
+++ b/syntax/leaninfo.vim
@@ -16,7 +16,14 @@ hi def link leanInfoGoalHyp Type
 hi def link leanInfoGoalVDash Operator
 hi def link leanInfoExpectedType Special

-hi def link leanInfoError LspDiagnosticsDefaultError
-hi def link leanInfoWarning LspDiagnosticsDefaultWarning
-hi def link leanInfoInfo LspDiagnosticsDefaultInformation
+" Old neovims (0.5) pre https://github.com/neovim/neovim/pull/15585
+if luaeval('vim.diagnostic == nil')
+    hi def link DiagnosticError LspDiagnosticsDefaultError
+    hi def link DiagnosticWarning LspDiagnosticsDefaultWarning
+    hi def link DiagnosticInformation LspDiagnosticsDefaultInformation
+endif
+
+hi def link leanInfoError DiagnosticError
+hi def link leanInfoWarning DiagnosticWarning
+hi def link leanInfoInfo DiagnosticInformation
 hi def link leanInfoComment Comment

for backwards compat, but got annoyed when I saw how different the vim.diagnostic API was and gave up. I think what we do is just stop supporting 0.5 (I'll just push a branch with the latest commit right now) and then move main to only support HEAD again.

gebner commented 3 years ago

I think what we do is just stop supporting 0.5

That's really unfortunate. I'm running 0.5 and don't plan to go back to building neovim from git. Ideally we'd keep 0.5 compatibility at least until 0.6 is released.

gebner commented 3 years ago

Another earlier commit already broke 0.5 compatibility: 6674cbece7de9487a77488ce8a251be6dd923991

With that commit, I no longer see diagnostics.

Julian commented 3 years ago

@gebner didn't know you were on 0.5 -- I did leave an 0.5 (frozen) branch just in case anyone was on it, though it's a bit annoying if 6674cbe broke 0.5 (and that therefore that branch won't work) -- that commit was in theory done that way specifically to preserve 0.5. But there's essentially the key at the minute, which is 0.5 doesn't run in CI.

From talking to other neovim plugin maintainers at least a few told me the same (that they had frozen 0.5 support).

I'm not against trying to continue to support it further, but we definitely need to run it side by side in CI if it's going to stay working, and I don't think I'll have time to do that today.

If one of you two does though obviously totally fine with me. Otherwise I'll try to do it when I get a moment, or otherwise at least make sure the 0.5 branch actually functions on 0.5.

gebner commented 3 years ago

135

@rish987 AFAICT the vim.lsp.diagnostic functions are still working in neovim nightly (but I didn't build a nightly to check). Was this PR even necessary to support the nightly builds?

rish987 commented 3 years ago

Not sure what's going on with the nightly builds, but if you build from source -- see for example this run -- you should run into an issue on trythis_spec.lua.