Issue with Importing Mathlib Modules on Windows Using Lean 4

Stream: mathlib4

[Pak Kin LAU]

I'm having trouble importing modules from Mathlib in my Lean 4 project on Windows. Specifically, when trying to import Mathlib.LinearAlgebra.Basic, I encounter an error related to file paths. Below is the error message I receive:

`c:\Users\kinla\.elan\toolchains\leanprover--lean4---v4.17.0-rc1\bin\lake.exe setup-file C:/LeanProjects/HW6/HW6.lean Init Mathlib.LinearAlgebra.Basic --no-build --no-cache` failed:

stderr:
✖ [2/3] Running Mathlib.LinearAlgebra.Basic
error: no such file or directory (error code: 2)
  file: .\.\.lake/packages\mathlib\.\.\Mathlib\LinearAlgebra\Basic.lean
✖ [3/3] Running imports (C:/LeanProjects/HW6/HW6.lean)
error: C:/LeanProjects/HW6/HW6.lean: bad import 'Mathlib.LinearAlgebra.Basic'
Some required builds logged failures:
- Mathlib.LinearAlgebra.Basic
- imports (C:/LeanProjects/HW6/HW6.lean)
error: build failed

Detailed Steps Taken:

1. Installation:
   I followed the instructions for setting up Lean 4 and Mathlib using lake:

   • Ensured that elan is up-to-date (elan --version 2.0.0).

   • Initialized a new Lean project and added Mathlib as a dependency in lakefile.toml:

     ```toml
     name = "HW6"
     version = "0.1.0"
     keywords = ["math"]
     defaultTargets = ["HW6"]

[leanOptions]
pp.unicode.fun = true # pretty-prints fun a ↦ b
autoImplicit = false

[[require]]
name = "mathlib"
scope = "leanprover-community"

[[lean_lib]]
name = "HW6"

```

2. Rebuilding the Project:
   I ran lake clean, lake update, and lake build several times, but the issue persists. I also tried importing other modules from Mathlib, such as Mathlib, which worked fine, but Mathlib.LinearAlgebra.Basic gives the error.

3. Path Issue:
   The error suggests a path resolution issue:

   file: .\.\.lake/packages\mathlib\.\.\Mathlib\LinearAlgebra\Basic.lean

   The relative path resolution seems incorrect, with multiple .\.\ causing the problem.

Environment:

• Operating System: Windows
• VS Code: Lean 4 extension installed
• Lean Version: Lean (version 4.17.0-rc1, x86_64-w64-windows-gnu, commit 93d4ae6635c0, Release)
• Lean Toolchain Version: leanprover/lean4:v4.17.0-rc1

• Project Setup: The Lean project is located in C:/LeanProjects/HW6/
  Troubleshooting Steps Taken:

• Moved the project to a simpler path (C:/LeanProjects/HW6/).

• Ensured that Mathlib was correctly installed and updated.
• Verified that the Matrix.lean file exists in .lake/packages/mathlib/Mathlib/LinearAlgebra/.
• Tried using absolute paths for imports (but this is not ideal and was just for debugging).
  Possible Cause: It seems like Lean is not correctly resolving the file paths, particularly when there are relative references like .\.\. This could be related to how Lean handles path resolution on Windows, or a configuration issue.

Request for Assistance:

• Has anyone encountered similar issues with path resolution on Windows when using Mathlib with Lean 4?
• Could this be related to the Windows file system, or is there a specific configuration I need to check or update?
• Any guidance on how to resolve these path resolution issues or suggestions for troubleshooting further would be appreciated.

[Kevin Buzzard]

file#LinearAlgebra.Basic

[Kevin Buzzard]

The error says that mathlib has no file called LinearAlgebra/Basic.lean and looking at GitHub I can confirm that no such file exists. So things are working as expected.

[Ruben Van de Velde]

It used to (I removed it last year)

[Ruben Van de Velde]

I'm a bit confused that you went looking for Matrix.lean when troubleshooting while you seemingly tried to import Basic.lean

[Ruben Van de Velde]

@Pak Kin LAU ^