lean path on Windows

Stream: general

[Frédéric Le Roux]

I am trying to use Lean on Windows (in a virtual machine running on Ubuntu).
My leanpkg.path contains path like

path C:\Users\Lerou\.deaduction\lean\lib\lean\library

But Lean does not find its way, and indeed running '''lean --path''' shows that it seems to mistake the paths as relative paths instead of absolute paths, i.e. I get

 "is_user_leanpkg_path": false,
  "leanpkg_path_file": "C:\\Users\\Lerou\\.deaduction\\leanpkg.path",
  "path": [ "C:\\Users\\Lerou\\.deaduction\\C:\\Users\\Lerou\\.deaduction\\lean\\lib\\lean\\library"
  ]
}

What is strange is that this issue does not appear on Linux nor Mac.
Is there an explanation for this? And an easy way around?

[Kevin Buzzard]

Did you create the leanpkg.path file with Windows tools?

[Frédéric Le Roux]

No, this is not a standard installation at all... The leanpkg.path is created by a Python script.

[Frédéric Le Roux]

But it is working on Linux/Mac!

[Gabriel Ebner]

#if defined(LEAN_WINDOWS)
std::string resolve(std::string const & rel_or_abs, std::string const & base) {
    // TODO(gabriel): detect absolute pathnames
    return base + g_sep + rel_or_abs;
}

[Gabriel Ebner]

Could you switch to relative paths? This seems to be the easiest solution here.

[Frédéric Le Roux]

That would be great. How do I do that? Am I supposed to insert these lines of code somewhere?

[Gabriel Ebner]

What I posted was a literal quote from the Lean source code. The case for absolute paths on windows has been missing since I wrote that function six years ago.

[Gabriel Ebner]

My suggestion was to write path lean\lib\lean\library instead of the absolute path (hoping that this works and is good enough for what you want to do).

[Frédéric Le Roux]

The problem is that some imports are not relative to the directory from which Lean is launched, and may vary according to the user installation.
Then I have to change that... Thanks for the suggestion, anyway!

[Mario Carneiro]

the paths should be relative to the leanpkg.path file, not the lean launch directory

[Frédéric Le Roux]

OK, thanks. I will try that.