Import Mathlib not Working as Expected

Stream: new members

[Guest User]

Could anyone please help resolve this issue?
Screenshot (8).png

[Guest User]

Screenshot (9).png

[Notification Bot]

This topic was moved here from #mathlib4 > Import Mathlib not Working as Expected by Eric Wieser.

[Eric Wieser]

@Guest User, please don't post the same question in multiple channels, because then people might not see if your question is already answered

[Guest User]

Eric Wieser said:

Guest User, please don't post the same question in multiple channels, because then people might not see if your question is already answered

I am sorry

[Eric Wieser]

What error do you get with import Mathlib? Can you paste it here in #backticks, rather than as a screenshot?

[Guest User]

Eric Wieser said:

What error do you get with import Mathlib? Can you paste it here in #backticks, rather than as a screenshot?

c:\Users\piyus\.elan\toolchains\leanprover--lean4---v4.13.0-rc3\bin\lake.exe setup-file D:/My Lean Stuff/my_project/MyProject.lean Init MyProject.Basic --no-build --no-cache failed:

stderr:
info: mathlib: URL has changed; you might need to delete '.\.\.lake/packages\mathlib' manually
trace: .\.\.lake/packages\mathlib> git fetch --tags --force origin
trace: stderr:
fatal: detected dubious ownership in repository at 'D:/My Lean Stuff/my_project/.lake/packages/mathlib'
'D:/My Lean Stuff/my_project/.lake/packages/mathlib' is owned by:
BUILTIN/Administrators (S-1-5-32-544)
but the current user is:
DESKTOP-SPTUF2T/piyus (S-1-5-21-3275850383-1562340433-442471243-1001)
To add an exception for this directory, call:

git config --global --add safe.directory 'D:/My Lean Stuff/my_project/.lake/packages/mathlib'

error: external command 'git' exited with code 128
Invalid Lake configuration. Please restart the server after fixing the Lake configuration file.

[Guest User]

c:\Users\piyus\.elan\toolchains\leanprover--lean4---v4.13.0-rc3\bin\lake.exe setup-file D:/My Lean Stuff/my_project/MyProject.lean Init MyProject.Basic --no-build --no-cache failed:

stderr:

info: mathlib: URL has changed; you might need to delete '.\.\.lake/packages\mathlib' manually

trace: .\.\.lake/packages\mathlib> git fetch --tags --force origin

trace: stderr:

fatal: detected dubious ownership in repository at 'D:/My Lean Stuff/my_project/.lake/packages/mathlib'

'D:/My Lean Stuff/my_project/.lake/packages/mathlib' is owned by:

BUILTIN/Administrators (S-1-5-32-544)

but the current user is:

DESKTOP-SPTUF2T/piyus (S-1-5-21-3275850383-1562340433-442471243-1001)

To add an exception for this directory, call:

git config --global --add safe.directory 'D:/My Lean Stuff/my_project/.lake/packages/mathlib'

error: external command 'git' exited with code 128

Invalid Lake configuration. Please restart the server after fixing the Lake configuration file.

[Guest User]

For backtricks it says, "This repository has been archived by the owner on Jul 24, 2024. It is now read-only."

[Eric Wieser]

Guest User said:

For backticks it says, "This repository has been archived by the owner on Jul 24, 2024. It is now read-only."

Please read the rest of that page anyway, but thanks for pointing this out