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):
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