Julian / lean.nvim

Neovim support for the Lean theorem prover
MIT License
280 stars 27 forks source link

lean.nvim emits logs on other files to ~/.local/state/nvim.log #343

Open MangoIV opened 4 months ago

MangoIV commented 4 months ago
[ERROR][2024-07-04 10:54:16] .../lean/stderr.lua:74 "rpc"   "haskell-language-server-wrapper"   "stderr"    "N"
[ERROR][2024-07-04 10:54:16] .../lean/stderr.lua:74 "rpc"   "haskell-language-server-wrapper"   "stderr"    "o 'hie.yaml' found. Try to discover the project type!\n"
[ERROR][2024-07-04 10:54:16] .../lean/stderr.lua:74 "rpc"   "haskell-language-server-wrapper"   "stderr"    "Run entered for "
[ERROR][2024-07-04 10:54:16] .../lean/stderr.lua:74 "rpc"   "haskell-language-server-wrapper"   "stderr"    "haskell-language-server-wrapper(haskell-language-server-wrapper) Version 2"
[ERROR][2024-07-04 10:54:16] .../lean/stderr.lua:74 "rpc"   "haskell-language-server-wrapper"   "stderr"    ".8.0.0 x86_64 ghc-9.8.2"
[ERROR][2024-07-04 10:54:16] .../lean/stderr.lua:74 "rpc"   "haskell-language-server-wrapper"   "stderr"    "\nCurrent direc"
[ERROR][2024-07-04 10:54:16] .../lean/stderr.lua:74 "rpc"   "haskell-language-server-wrapper"   "stderr"    "tory: /home/mangoi"
[ERROR][2024-07-04 10:54:16] .../lean/stderr.lua:74 "rpc"   "haskell-language-server-wrapper"   "stderr"    "v/Devel/hs\nOperating system: linux\nArg"
[ERROR][2024-07-04 10:54:16] .../lean/stderr.lua:74 "rpc"   "haskell-language-server-wrapper"   "stderr"    'uments: ["--lsp","--l'
[ERROR][2024-07-04 10:54:16] .../lean/stderr.lua:74 "rpc"   "haskell-language-server-wrapper"   "stderr"    'ogfile","/tmp/nix-'
[ERROR][2024-07-04 10:54:16] .../lean/stderr.lua:74 "rpc"   "haskell-language-server-wrapper"   "stderr"    "shell.yzvVWi/nvi"
[ERROR][2024-07-04 10:54:16] .../lean/stderr.lua:74 "rpc"   "haskell-language-server-wrapper"   "stderr"    "m.mangoiv/BJ7D7"
[ERROR][2024-07-04 10:54:16] .../lean/stderr.lua:74 "rpc"   "haskell-language-server-wrapper"   "stderr"    "Q/0-haskell-langu"
[ERROR][2024-07-04 10:54:16] .../lean/stderr.lua:74 "rpc"   "haskell-language-server-wrapper"   "stderr"    "age-server.l"
[ERROR][2024-07-04 10:54:16] .../lean/stderr.lua:74 "rpc"   "haskell-language-server-wrapper"   "stderr"    'og"]\nCradle di'
[ERROR][2024-07-04 10:54:16] .../lean/stderr.lua:74 "rpc"   "haskell-language-server-wrapper"   "stderr"    "rectory: /home/ma"
[ERROR][2024-07-04 10:54:16] .../lean/stderr.lua:74 "rpc"   "haskell-language-server-wrapper"   "stderr"    "ngoiv/Devel/hs\nCrad"
[ERROR][2024-07-04 10:54:16] .../lean/stderr.lua:74 "rpc"   "haskell-language-server-wrapper"   "stderr"    "le type: Default\n"
[ERROR][2024-07-04 10:54:16] .../lean/stderr.lua:74 "rpc"   "haskell-language-server-wrapper"   "stderr"    "\nTool version"
[ERROR][2024-07-04 10:54:16] .../lean/stderr.lua:74 "rpc"   "haskell-language-server-wrapper"   "stderr"    "s found on the $PATH\ncabal:       "
[ERROR][2024-07-04 10:54:16] .../lean/stderr.lua:74 "rpc"   "haskell-language-server-wrapper"   "stderr"    "   "
[ERROR][2024-07-04 10:54:16] .../lean/stderr.lua:74 "rpc"   "haskell-language-server-wrapper"   "stderr"    "3."
[ERROR][2024-07-04 10:54:16] .../lean/stderr.lua:74 "rpc"   "haskell-language-server-wrapper"   "stderr"    "10.3."
[ERROR][2024-07-04 10:54:16] .../lean/stderr.lua:74 "rpc"   "haskell-language-server-wrapper"   "stderr"    "0\nstack: "
[ERROR][2024-07-04 10:54:16] .../lean/stderr.lua:74 "rpc"   "haskell-language-server-wrapper"   "stderr"    "         No"
[ERROR][2024-07-04 10:54:16] .../lean/stderr.lua:74 "rpc"   "haskell-language-server-wrapper"   "stderr"    "t found\nghc"
[ERROR][2024-07-04 10:54:16] .../lean/stderr.lua:74 "rpc"   "haskell-language-server-wrapper"   "stderr"    ":            "
[ERROR][2024-07-04 10:54:16] .../lean/stderr.lua:74 "rpc"   "haskell-language-server-wrapper"   "stderr"    "9.8.2\n\n\nConsulting "
[ERROR][2024-07-04 10:54:16] .../lean/stderr.lua:74 "rpc"   "haskell-language-server-wrapper"   "stderr"    "the cradle t"
[ERROR][2024-07-04 10:54:16] .../lean/stderr.lua:74 "rpc"   "haskell-language-server-wrapper"   "stderr"    "o get pr"
[ERROR][2024-07-04 10:54:16] .../lean/stderr.lua:74 "rpc"   "haskell-language-server-wrapper"   "stderr"    "oject "
[ERROR][2024-07-04 10:54:16] .../lean/stderr.lua:74 "rpc"   "haskell-language-server-wrapper"   "stderr"    "GHC ve"

it goes on like this. I think the plugin should not do anything when the user is not viewing a lean file.

Julian commented 4 months ago

Seems likely something is attaching to a buffer and not detaching, or else is attaching without checking the filetype.

It'd be helpful to include steps to reproduce this.

(And PR welcome of course, otherwise someone'll get to it at some point).

MangoIV commented 4 months ago

Hi! Thank you for taking the time to have a look at this. In my init.lua I have the following pieces of configuration that influence the behaviour of the lean language server:

vim.api.nvim_create_autocmd("VimResized", { callback = require("lean.infoview").reposition })
require("lean").setup({
    lsp = {
        capabilities = capabilities_def,
    },
    mappings = true,
    abbreviations = {
        builtin = true,
        enable = true,
        leader = ",",
    },
})

I have looked a the README and the VimResized part doesn't appear anymore, could it cause it? Can I remove it? If not, I would say, this should happen anywhere, it definitely happens on multiple language servers. I normally set them up with nvim-lspconfig but there's also some that I do not, like rust and haskell.