Not completely working in vim about idris2-nvim HOT 7 CLOSED

• What is the version of idris2-lsp?
• What is the output of :LspInfo on a buffer with an idris file open?
• Idris2-LSP requires an ipkg file. Did you try to load a standalone idris file?

from idris2-nvim.

1. I installed idris2-lsp last week, not sure how to get version.
2. I wasn't sure I needed an ipkg, instructions were not clear. Idris2 --init?
3. Info from :LspInfo
   Language client log: /Users/gregory/.local/state/nvim/lsp.log
   Detected filetype: markdown

0 client(s) attached to this buffer:

2 active client(s) not attached to this buffer:

Client: lua_ls (id: 1, bufnr: [14, 13, 69])
filetypes: lua
autostart: true
root directory: Running in single file mode.
cmd: lua-language-server

Client: null-ls (id: 2, bufnr: [14, 13, 69])
filetypes: handlebars, typescriptreact, markdown, json, css, typescript, javascript, javascriptreact, vue, scss, html, jsonc, yaml, less, graphql, markdown.mdx, luau, lua
autostart: false
root directory: /Users/gregory/Haskell/Idris
cmd:

Other clients that match the filetype: markdown

Config: tailwindcss
Refer to :h lspconfig-root-detection for help.
filetypes: aspnetcorerazor, astro, astro-markdown, blade, clojure, django-html, htmldjango, edge, eelixir, elixir, ejs, erb, eruby, gohtml, haml, handlebars, hbs, html, html-eex, heex, jade, leaf, liquid, markdown, mdx, mustache, njk, nunjucks, php, razor, slim, twig, css, less, postcss, sass, scss, stylus, sugarss, javascript, javascriptreact, reason, rescript, typescript, typescriptreact, vue, svelte
root directory: Not found.
cmd: tailwindcss-language-server --stdio
cmd is executable: true
autostart: true
custom handlers:

Configured servers list: html, lua_ls, emmet_ls, idris2_lsp, tailwindcss, tsserver, cssls

from idris2-nvim.

Perhaps I don't have the idris2-lsp. I was just reviewing the installation procedure again using pack. I don't recall doing all that and I can find no evidence idris2-lsp exists. -- and follow up -- how does one create an ipkg and when is it required?

from idris2-nvim.

Yeah. :LspInfo provides the following info

Other clients that match the filetype: idris2

   ** Config: idris2_lsp
Refer to :h lspconfig-root-detection for help.
filetypes:         idris2
root directory:    Not found.
cmd:               idris2-lsp

**cmd is executable: Unable to find executable. Please check your path and ensure the server is installed**

autostart:         true
custom handlers:   workspace/semanticTokens/refresh, textDocument/hover, textDocument/semanticTokens/full

Configured servers list: html, lua_ls, emmet_ls, idris2_lsp, tailwindcss, tsserver, cssls

from idris2-nvim.

I suggest using pack, you can install lsp with pack install-app lsp.
Regarding the ipkg you can use either the compiler with the interactive idris2 --init, or better pack with pack new.

from idris2-nvim.

from idris2-nvim.

Okay. I am still in need of some help. I have installed pack ( including building idris2 from source). I have an ipkg ( "testing.ipkg") in my root directory. ${HOME}/.pack has been exported ( I can call idris-lsp from a teminal).

I assume that this process will let me do Chapter 3 of the Type Driven Developement with Idris

:LspInfo:

Language client log: /Users/gregory/.local/state/nvim/lsp.log
Detected filetype: idris2

1 client(s) attached to this buffer:

Client: idris2_lsp (id: 1, bufnr: [1])
filetypes: idris2
autostart: true
root directory: /Users/gregory/Idris
cmd: idris2-lsp

Configured servers list: idris2_lsp, lua_ls, html, tsserver, cssls, tailwindcss, emmet_ls

lsp.log:

[ERROR][2023-03-24 13:42:45] .../vim/lsp/rpc.lua:733 "rpc" "idris2-lsp" "stderr" "LOG INFO:Communication.Channel: Received didOpen notification for file:///Users/gregory/Idris/Average.idr\nLOG INFO:Server: Loading file file:///Users/gregory/Idris/Average.idr\n"
[ERROR][2023-03-24 13:42:45] .../vim/lsp/rpc.lua:733 "rpc" "idris2-lsp" "stderr" "LOG INFO:Notification.Diagnostic: Sending diagnostic message for file:///Users/gregory/Idris/Average.idr\n"
[ERROR][2023-03-24 13:42:45] .../vim/lsp/rpc.lua:733 "rpc" "idris2-lsp" "stderr" 'LOG INFO:Communication.Channel: Sent notification message for method "textDocument/publishDiagnostics"\nLOG DEBUG:Communication.Channel: Notification sent: {"jsonrpc":"2.0","method":"textDocument/publishDiagnostics","params":{"uri":"file:///Users/gregory/Idris/Average.idr","version":0,"diagnostics":[]}}\nLOG DEBUG:Request.Completion: Found namespaces: Data.List Main Prelude System.REPL Data.String\n'
[ERROR][2023-03-24 13:42:45] .../vim/lsp/rpc.lua:733 "rpc" "idris2-lsp" "stderr" "LOG DEBUG:Request.Completion: Found 495 completion entries.\n"
[ERROR][2023-03-24 13:42:45] .../vim/lsp/rpc.lua:733 "rpc" "idris2-lsp" "stderr" 'LOG DEBUG:Communication.Channel: Received message: {"params":{"textDocument":{"uri":"file:\/\/\/Users\/gregory\/Idris\/Average.idr"}},"jsonrpc":"2.0","id":2,"method":"textDocument\/semanticTokens\/full"}\n'
[ERROR][2023-03-24 13:42:45] .../vim/lsp/rpc.lua:733 "rpc" "idris2-lsp" "stderr" 'LOG INFO:Communication.Channel: Received request for method "textDocument/semanticTokens/full"\n'
[ERROR][2023-03-24 13:42:45] .../vim/lsp/rpc.lua:733 "rpc" "idris2-lsp" "stderr" "LOG DEBUG:Notification.SemanticTokens: Fetching semantic highlightning metadata\nLOG DEBUG:Notification.SemanticTokens: Removing overlapping tokens\nLOG DEBUG:Notification.SemanticTokens: Splitting multiline tokens\n"
[ERROR][2023-03-24 13:42:45] .../vim/lsp/rpc.lua:733 "rpc" "idris2-lsp" "stderr" "LOG DEBUG:Notification.SemanticTokens: Encoding semantic tokens\n"
[ERROR][2023-03-24 13:42:45] .../vim/lsp/rpc.lua:733 "rpc" "idris2-lsp" "stderr" 'LOG INFO:Communication.Channel: Sent response message for method "textDocument/semanticTokens/full"\n'
[ERROR][2023-03-24 13:42:45] .../vim/lsp/rpc.lua:733 "rpc" "idris2-lsp" "stderr" 'LOG DEBUG:Communication.Channel: Response sent: {"jsonrpc":"2.0","id":2,"result":{"data":[0,0,6,4,0,0,7,4,7,0,2,0,6,4,0,0,7,11,7,0,0,12,14,8,0,1,0,6,4,0,0,7,9,7,0,0,12,24,8,0,1,0,6,4,0,0,7,11,7,0,0,12,13,8,0,2,0,54,8,0,1,0,60,8,0,1,0,6,4,0,1,0,7,1,0,0,8,1,4,0,0,2,1,4,0,0,1,3,3,0,0,4,1,4,0,0,1,6,0,0,0,6,1,4,0,0,2,2,4,0,0,3,6,0,0,1,0,7,1,0,0,8,3,3,0,0,4,1,4,0,0,2,3,4,0,0,4,8,3,0,0,9,1,4,0,0,2,9,1,0,0,10,3,3,0,1,18,11,3,0,0,12,1,4,0,0,2,3,1,0,0,4,1,4,0,0,1,10,1,0,0,11,1,4,0,0,2,5,1,0,0,6,3,3,0,0,3,1,4,0,0,1,1,4,0,0,2,2,4,0,1,18,4,1,0,0,5,11,3,0,0,12,1,1,0,0,2,4,1,0,0,5,8,3,0,1,2,5,4,0,1,4,9,1,0,0,10,1,4,0,0,2,6,0,0,0,8,2,4,0,0,3,3,0,0,1,4,9,1,0,0,10,3,3,0,0,4,1,4,0,0,2,6,1,0,0,7,1,4,0,0,1,5,1,0,0,6,3,3,0,0,3,1,4,0,2,4,10,1,0,0,11,1,4,0,0,2,4,0,0,0,5,6,0,0,0,7,2,4,0,0,3,4,0,0,0,5,3,0,0,1,4,10,1,0,0,11,4,3,0,0,5,1,4,0,0,2,3,1,0,0,4,6,1,0,0,7,4,3,0,2,0,11,1,0,0,12,1,4,0,0,2,6,0,0,0,7,2,4,0,0,3,6,0,0,1,0,11,1,0,0,12,3,3,0,0,4,1,4,0,0,2,33,2,0,0,34,2,1,0,1,18,4,1,0,0,5,1,4,0,0,1,7,1,0,0,9,3,3,0,0,3,1,4,0,0,2,2,1,0,0,3,4,2,0,2,0,4,1,0,0,5,1,4,0,0,2,2,0,0,0,3,2,0,0,1,0,4,1,0,0,5,1,4,0,0,2,4,1,0,0,5,19,2,0,0,20,11,1,0]}}\n'

from idris2-nvim.