Server Filename Windows Bug

Stream: lean4

[Mac]

On Windows, the filename of the elaborating Lean file is improperly escaped:

import Lean.Elab.ElabRules
open Lean Syntax Elab Term

elab stx:"__file__" : term <= expectedType => do
  let exp := quote (← getFileName)
  withMacroExpansion stx exp <| elabTerm exp expectedType

#eval __file__ -- "\\e%3A\\Sync\\Programs\\lean4\\playpen\\FileName.lean"

I am not sure whether this is a Lean server bug (@Sebastian Ullrich ) or a VSCode extension bug (@Gabriel Ebner ). Part of me suspects the the later due to the weird presence of a stating \ to the path and the URL escape sequence, which makes it seem like the path is derived from some escaped file:// URL used by VSCode.

[Sebastian Ullrich]

Right, the URL decoding is very simplistic right now https://github.com/leanprover/lean4/blob/67087ac16edc8b8d25964e1a489e2824b8efec2c/src/Lean/Server/Utils.lean#L74

[Sebastian Ullrich]

The leading backslash is also wrong