Comments (7)
- 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.
- I installed idris2-lsp last week, not sure how to get version.
- I wasn't sure I needed an ipkg, instructions were not clear. Idris2 --init?
- 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.
Related Issues (8)
- Don't assume all LSP clients provide "textDocument/semanticTokens/full" HOT 3
- Error messages when `idris2` isn't in `$PATH` HOT 4
- No autocomplete HOT 2
- Nothing works except for syntax highlighting HOT 5
- Idris2 LSP Response Buffer is empty HOT 2
- highlight not working by default HOT 4
- Error when executing `metavars.request_all`
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
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.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from idris2-nvim.