Zulip Chat Archive

Stream: new members

Topic: Import Mathlib not Working as Expected


Guest User (Oct 18 2024 at 00:01):

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

Guest User (Oct 18 2024 at 00:03):

Screenshot (9).png

Notification Bot (Oct 18 2024 at 00:05):

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

Eric Wieser (Oct 18 2024 at 00:06):

@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 (Oct 18 2024 at 00:10):

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 (Oct 18 2024 at 00:13):

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

Guest User (Oct 18 2024 at 01:04):

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 (Oct 18 2024 at 01:05):

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 (Oct 18 2024 at 01:06):

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

Eric Wieser (Oct 18 2024 at 01:51):

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


Last updated: May 02 2025 at 03:31 UTC