VSCode server crashes on unusual paths

Stream: lean4

[Raghuram]

When opening files with certain paths containing ' and/or " in VSCode, the Lean 4 server crashes repeatedly until VSCode stops trying to restart it. The error messages shown in the Output pane are about /bin/sh, -c and matching quotes/unexpected EOFs

[Raghuram]

Does this happen for anyone using Emacs?

[Julian Berman]

I don't see that in neovim (it seems to work), if that helps.

[Julian Berman]

(and in the background I see julian 11760 0.0 0.7 409823072 59408 s001 S+ 5:17PM 0:00.10 /opt/homebrew/Cellar/lean@4/HEAD-d13fac6/bin/lean --worker file:///Users/julian/Development/lean-scratch4/Scratch/foobar%22baz.lean)

[Sebastian Ullrich]

@Raghuram Could you post the messages?

[Raghuram]

In the Output pane:

Lean (version 4.0.0-nightly-2022-05-19, commit d13fac6f458b, Release)
/bin/sh: -c: line 1: unexpected EOF while looking for matching `''
/bin/sh: -c: line 2: syntax error: unexpected end of file
[Info  - 1:31:22 pm] Connection to server got closed. Server will restart.

with the last 3 lines repeating until VSCode gives up. This is for the path ~/Desktop/Folder'/File.lean.

[Sebastian Ullrich]

Hmm, it's not clear to me where that shell script is coming from

[Eric Wieser]

Maybe https://github.com/leanprover/vscode-lean4/blob/06aef42870aa8afaf714e69b493bab86559c7cdf/vscode-lean4/src/leanclient.ts#L167?

[Eric Wieser]

shell = True usually means "who knows whether this is going to be sensibly escaped"

[Raghuram]

Eric Wieser said:

Maybe https://github.com/leanprover/vscode-lean4/blob/06aef42870aa8afaf714e69b493bab86559c7cdf/vscode-lean4/src/leanclient.ts#L167?

There is a function escapeRegexp on line 33 of the same file which (I think) adds \s before matches for /[.*+?^${}()|[\]\\]/g; maybe ' and " need to be added to that regexp?

[Raghuram]

Never mind; that's only used to construct another regexp.

[Gabriel Ebner]

That's used for something different. Namely when you move your cursor over a word, then it highlights all occurrences of the word in the file (unless the server has better information). The regexp is used to use escape that word.