Error for files with special characters in path name

[ianjauslin-rutgers]

I've run into an issue when I open a lean file in a directory that has a '+' in its name. After opening the file, I get the error Error executing vim.schedule lua callback: .../share/nvim/plugged/lean.nvim/lua/lean/progress_bars.lua:17: bad argument #1 to 'ipairs' (table expected, got nil) Everything works fine if I rename the directory to something that does not contain '+'.

I am running Arch Linux with neovim version 0.8.0 and have updated lean.nvim (commit 60d71f3...).

[rish987]

It looks like the Lean 3 server itself is not processing the characters correctly. If I rename mathlib to mathlib+ and add a print of the params.textDocument.uri in require"lean.progress".update, I get (for example) file:///home/gcloud/mathlib%2B/src/analysis/hofer.lean, while on the progress_bars.lua side vim.uri_from_bufnr() correctly gets us file:///home/gcloud/mathlib+/src/analysis/hofer.lean.

@gebner is this perhaps a known issue with the underlying Lean 3 server? If not, there's probably something at https://github.com/leanprover/lean-client-js/tree/master/lean-language-server that we can patch.

[Julian]

If this is Lean 3 I doubt it's something upstream will care to fix (unless we do it, which I don't think seems like something I'd work on personally). Going to close this then as "upstream issue"? Feel free to chime in if either of you disagree.

[gebner]

Nobody has the time to support + in file names, not in Lean 4, and certainly not in Lean 3.