Git Product home page Git Product logo

idris2-nvim's People

Contributors

buzden avatar gwerbin avatar jumper149 avatar mattpolzin avatar shinkage avatar

Stargazers

 avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar

Watchers

 avatar  avatar  avatar  avatar  avatar

idris2-nvim's Issues

No autocomplete

I'm not getting any autocomplete when I use this plugin, but everything else seems to work (code actions, inline errors, etc.)

vscode has the same functionality but also have autocompletion working.

I see textDocument/completion responses coming through in my log when I type in nvim, so the LSP seems to be receiving requests and responding properly, they're just not showing up in neovim.

Running 0.8.3 nvim

Nothing works except for syntax highlighting

Hello, I have been trying to setup this plugin for my neovim.
I have installed idris2 and idris2-pack using this bash -c "$(curl -fsSL https://raw.githubusercontent.com/stefan-hoeck/idris2-pack/main/install.bash)" shown on their github page. Then I proceed to install idris2-lsp by using their recommended method (pack). I added this plugin with packer for neovim and I inserted require('idris2').setup({}) into my config file. When I edit any idris file (a file that ends with .idr). I get syntax highlighting but no autocomplete, no error reporting and no interactive development. I am sorry if this is an invalid issue but I have exhausted all solutions I could think of.
Thanks for your time!
PS: here is my nvim config: https://github.com/RHL120/neovimcfg. The only files that matter are probably:

Not completely working in vim

I only get syntax highlighting in nvim, i.e. no auto complete, no hover, etc. capabilities. Neovim 0.8.3, with require("idris2").setup({}) in the init.lua, and use({ "ShinKage/idris2-nvim", requires = { "neovim/nvim-lspconfig", "MunifTanjim/nui.nvim" } }) in the plugins-setup.lua file. I using packer as the packer manager.

Need some assistance trying to debug what is wrong.

Error messages when `idris2` isn't in `$PATH`

Issue description

Running Neovim will always cause it to start with the following error message:

Error in packer_compiled: Vim:E475: Invalid value for argument cmd: 'idris2' is not executable
Please check your config for correctness

This error message occurs even if the filetype opened isn't Idris2.

How to reproduce:

Start neovim with idris2-nvim setup, without idris2 in $PATH. This issue doesn't occur with idris2-lsp missing, unless opening an Idris2 file (which seems reasonable to me).

I use Packer as my plugin manager and could reproduce the issue with the startup command only being require('idris2').setup({}), as per the README.

Expected behaviour/Proposed solution:

I think this error message should only pop up when opening Idris2 files.
I hate having to comment/uncomment this plugin on my system depending on whether or not I have access to idris2 on my system.

Also, there are certain use-cases like Nix/Guix where people might only install certain packages as a dependency of project through nix-shell and Idris2 might be one of them.

Maybe this issue can also be circumvented by setting the plugin as optional on Packer or whatever, but I don't really know how to do that and I don't think all plugin managers would support that.

Don't assume all LSP clients provide "textDocument/semanticTokens/full"

When using https://github.com/zbirenbaum/copilot.lua, GitHub Copilot runs as an LSP client in the buffer alongside other LSP providers (e.g. idris2-lsp), and doesn't provide the functionality this plugin expects. Is there perhaps a way to handle such errors gracefully, or to not request functionality from the wrong LSP clients in the first place?

What happens whenever the plugin runs alongside any such clients:

Error executing vim.schedule lua callback: /usr/share/nvim/runtime/lua/vim/lsp.lua:1018: not found: "textDocument/semanticTokens/full" request handler for client "copilot".
stack traceback:
        [C]: in function 'error'
        /usr/share/nvim/runtime/lua/vim/lsp.lua:1018: in function 'request'
        /usr/share/nvim/runtime/lua/vim/lsp.lua:1485: in function 'fn'
        /usr/share/nvim/runtime/lua/vim/lsp.lua:164: in function 'for_each_buffer_client'
        /usr/share/nvim/runtime/lua/vim/lsp.lua:1484: in function 'buf_request'
        ...te/pack/packer/start/idris2-nvim/lua/idris2/semantic.lua:8: in function 'request'
        ...m/site/pack/packer/start/idris2-nvim/lua/idris2/init.lua:18: in function '_on_attach'
        ...ck/packer/start/nvim-lspconfig/lua/lspconfig/configs.lua:273: in function '_setup_buffer'
        ...ck/packer/start/nvim-lspconfig/lua/lspconfig/configs.lua:183: in function ''
        vim/_editor.lua: in function <vim/_editor.lua:0>

The relevant code:

function M.request(bufnr)
local bufnr = bufnr or 0
local text_params = vim.lsp.util.make_text_document_params()
vim.lsp.buf_request(bufnr, 'textDocument/semanticTokens/full', { textDocument = text_params })
end

Idris2 LSP Response Buffer is empty

I installed idris2-nvim and it seems to mostly work (e.g. if I have a syntax error it highlights the line and shows error).

However, if I do idris2.hover.open_split(), it opens the buffer but it is always empty. I also never have any popups appearing unless I do something like "evaluate" (seems like they should appear passively although I am not completely sure).

Due to this problem, I am not able to check types and usability is significantly limited.

I have neovim 0.9.0 on Manjaro Linux.

Error when executing `metavars.request_all`

What

When executing :lua require("idris2.metavars").request_all(), the following error appears:

Error executing vim.schedule lua callback: vim/shared.lua:0: Expected table, got nil
stack traceback:
        [C]: in function 'assert'
        vim/shared.lua: in function 'tbl_isempty'
        ...te/pack/packer/start/idris2-nvim/lua/idris2/metavars.lua:77: in function 'handler'
        /usr/share/nvim/runtime/lua/vim/lsp.lua:995: in function ''
        vim.lua: in function <vim.lua:0>

Why?

I think this is a bug in this check:

return function (err, result, ctx, config)
if vim.tbl_isempty(result) then

The argument result might be nil (see :help lsp-handler), so the call to tbl_isempty fails.

Installed software

Neovim:

$ nvim --version
NVIM v0.7.0-dev+848-gb4fbb9dcf2
Build type: RelWithDebInfo
LuaJIT 2.0.5
Compilation: /usr/bin/cc -march=x86-64 -mtune=generic -O2 -pipe -fno-plt -DNVIM_TS_HAS_SET_MATCH_LIMIT -O2 -g -Og -g -Wall -Wextra -pedantic -Wno-unused-parameter -Wstrict-prototypes -std=gnu99 -Wshadow -Wconversion -Wmissing-prototypes -Wimplicit-fallthrough -Wvla -fstack-protector-strong -fno-common -fdiagnostics-color=auto -DINCLUDE_GENERATED_DECLARATIONS -D_GNU_SOURCE -DNVIM_MSGPACK_HAS_FLOAT32 -DNVIM_UNIBI_HAS_VAR_FROM -DMIN_LOG_LEVEL=3 -I/build/neovim-git/src/build/config -I/build/neovim-git/src/neovim-git/src -I/usr/include -I/build/neovim-git/src/build/src/nvim/auto -I/build/neovim-git/src/build/include
Compiled by builduser

Features: +acl +iconv +tui
See ":help feature-compile"

   system vimrc file: "$VIM/sysinit.vim"
  fall-back for $VIM: "/usr/share/nvim"

Run :checkhealth for more info

highlight not working by default

Here's my config with lazy:

  { 'ShinKage/idris2-nvim',
    dependencies = {'neovim/nvim-lspconfig', 'MunifTanjim/nui.nvim'},
    -- ft = 'idr',
    lazy = false,
    config = function()
      require('idris2').setup({})
      vim.cmd [[highlight link LspSemantic_type Include]]
    end
  },

image

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    ๐Ÿ–– Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. ๐Ÿ“Š๐Ÿ“ˆ๐ŸŽ‰

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google โค๏ธ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.