Zulip Chat Archive

Stream: lean4

Topic: Server Filename Windows Bug


Mac (Jun 11 2022 at 19:52):

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 (Jun 11 2022 at 21:57):

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

Sebastian Ullrich (Jun 11 2022 at 21:57):

The leading backslash is also wrong


Last updated: Dec 20 2023 at 11:08 UTC