Lean.Core.Context fileName is mangled on Windows

[lovettchris]

Prerequisites

• 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 feat: rubiks cube sample leanprover-community/lean4-samples#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 #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 #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:

lean4/src/Lean/Server/Utils.lean

Lines 78 to 85 in da139ef

	/-- Return local path from file:// URI, if any. -/
	def toPath? (uri : DocumentUri) : Option System.FilePath := Id.run do
	if !uri.startsWith "file:///" then
	return none
	let mut p := uri.drop "file://".length
	if System.Platform.isWindows then
	p := p.map fun c => if c == '/' then '\\' else c
	some ⟨p⟩

. As you can see, it's a quite naive implementation right now, it doesn't do real URL decoding.

[lovettchris]

This is fixed by #1452