Lean.Core.Context fileName is mangled on Windows

[lovettchris]

Prerequisites

• [x] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

elab (name := includeStr) "include_str " str:str : term => do
  let str := str.getString
  let ctx ← readThe Lean.Core.Context
  let srcPath := System.FilePath.mk ctx.fileName
  let some srcDir := srcPath.parent | throwError "{srcPath} not in a valid directory"
  let path := srcDir / str
  Lean.mkStrLit <$> IO.FS.readFile path

Steps to Reproduce

1. try and build https://github.com/leanprover/lean4-samples/pull/3 on Windows using lake build rubiksJs

Expected behavior:

Build should succeed.

Actual behavior:

error: no such file or directory (error code: 2)
error: build failed

The problem appears to be that the beginning of the ctx.fileName is mangled like this:

\d%3A\Temp\lean4-samples\RubiksCube\Rubiks.lean

It should be as follows instead:

d:\Temp\lean4-samples\RubiksCube\Rubiks.lean

This could be related to https://github.com/leanprover/lean4/pull/1257

Reproduces how often: 100%

Versions

Lean (version 4.0.0-nightly-2022-08-01, commit c76fa0681651, Release)

Additional Information

Any additional information, configuration or data that might be necessary to reproduce the issue.

[Kha]

I think this is DocumentUri.toPath? not supporting absolute Windows paths

[lovettchris]

Is that where ctx.fileName is coming from? I couldn't find the source code, can you include a pointer to the code so I can try and fix it on my machine?

[lovettchris]

Note that https://github.com/leanprover/lean4/pull/1257 fixes the npm build problem, but the Rubiks cube sample still doesn't work due to this path problem, so I see this in the editor:

[Kha]

Is that where ctx.fileName is coming from? I couldn't find the source code, can you include a pointer to the code so I can try and fix it on my machine?

It's here: https://github.com/leanprover/lean4/blob/da139efa08b773045af08524cc19f7d1aea9c27a/src/Lean/Server/Utils.lean#L78-L85. As you can see, it's a quite naive implementation right now, it doesn't do real URL decoding.

[lovettchris]

This is fixed by https://github.com/leanprover/lean4/pull/1452