Error while importing Mathlib

Stream: new members

[Aatman Supkar]

I just started a new project, which doesn't generate errors, except for this one import line:
import Mathlib.Combinatorics.SimpleGraph.Basic
When I do add this line at the top of the project, the Lean infoview says:

`/Users/aatmansupkar/.elan/toolchains/leanprover--lean4---v4.16.0-rc1/bin/lake setup-file /Volumes/amazon/maths/lean_projects/graph-boxicity/GraphBoxicity/Basic.lean Init Mathlib.Combinatorics.SimpleGraph.Basic` failed:

stderr:
✖ [420/584] Running proofwidgets/widgetJsAll
error: Tried to read file '././.lake/packages/proofwidgets/widget/src/._animatedHtml.tsx' containing non UTF-8 data.
error: Tried to read file '././.lake/packages/proofwidgets/widget/src/._cancellable.ts' containing non UTF-8 data.
error: Tried to read file '././.lake/packages/proofwidgets/widget/src/._d3Graph.tsx' containing non UTF-8 data.
error: Tried to read file '././.lake/packages/proofwidgets/widget/src/._exprPresentation.tsx' containing non UTF-8 data.
error: Tried to read file '././.lake/packages/proofwidgets/widget/src/._filterDetails.tsx' containing non UTF-8 data.

And a lot more of those 'tried to read file, non-UTF-8 data' errors. Not sure what went wrong. Can someone help me find and correct the issue? Thanks!

[Mauricio Collares]

If you're starting a new project (and not working on mathlib itself), please use Lean v4.15.0 and the mathlib v4.15.0 tag for now.

[Mauricio Collares]

(It's not the cause of this particular error, but you will encounter other problems later on)

[Mauricio Collares]

See also #general > Updating to 4.15.0 @ 💬

[Aatman Supkar]

I'll add further details. I haven't quite figured out how to downgrade to 4.15, because despite initialising the project with the lake new ... math command followed by lake exe cache get, I cannot find a file whose extension is .toml. I am working on MacOS 15 Sequoia. The errors seem to be the same even if I just write import Mathlib at the top.

[Ruben Van de Velde]

Do you have a file called lakefile.lean?

[Aatman Supkar]

Ah, this one I do have. I couldn't find the syntax to work with this in the above link, though.

[Aatman Supkar]

lakefile.lean
I'm attaching the lakefile.lean in its current state, based on some consultation. I'm getting the error "mathlib has already been declared". Any help with fixing this will be much appreciated.

[Aatman Supkar]

I've removed the first require line. I then deleted the whole .lake directory and ran lake update -R in the terminal. But it says error: mathlib: failed to fetch cache

[Aatman Supkar]

Once again, I'll attach the lakefile and the toolchain, to assist the debugging.
lean-toolchain
lakefile.lean

[Aatman Supkar]

Further inquiry seems to reveal that this is a very Mac-specific issue. I'll point out that I did not use Homebrew to get Lean, and used the VS Code extension instead.

[Aatman Supkar]

As one last attempt, I deleted both the .lake directory and the lake-manifest, and ran lake update. The error persists. If further work requires that I upload content from more files, please let me know. I'm not sure what all is relevant here. Thanks!

[Ruben Van de Velde]

I think require "leanprover-community" / "mathlib" @ git "v4.15.0" is right? It looks plausible, at least. So I'm not sure what's wrong now

[Mauricio Collares]

(deleted)

[Mauricio Collares]

Can you paste the full error you're getting? Or a screenshot if pasting is not an option.

[Mauricio Collares]

Also, if you enter the project directory, what is the output of elan -V and elan show?

[Aatman Supkar]

A complete log of what happened after lake update:
image.png
Output from elan -V and elan show:
image.png

[Ruben Van de Velde]

That all looks okay. Does lake exe cache get say anything more?

[Aatman Supkar]

Nope. Ran without saying anything at all.

[Mauricio Collares]

Honestly I'd just delete ~/.cache/mathlib and try again. The most likely explanation is a corrupted leangz binary, but I'm not sure why it would just quit.

[Mauricio Collares]

If if doesn't work, can you check if you have a file called ~/.cache/mathlib/leantar-0.1.14 after running lake exe cache get?

[Aatman Supkar]

Sorry if this sounds a bit stupid, but I really can't locate this .cache folder at all :sweat_smile:

[Ruben Van de Velde]

It should be under your home directory - unless lake exe cache get just doesn't even get far enough to create it

[Aatman Supkar]

Wait... the Lean project itself is on an SSD outside my device, and this directory should still be under home?

[Ruben Van de Velde]

Yes

[Ruben Van de Velde]

(Technically, unless you've got XDG_CACHE_HOME or similar set)

[Aatman Supkar]

Wow, you really meant the ~ in ~/.cache/mathlib. My bad.
Very sorry for this, but what all should I try again after deleting that, exactly?

[Aatman Supkar]

After removing the ~/.cache/mathlib, I seem to be unable to run any command to get mathlib back. Any ideas?

[Julian Berman]

What command are you now running and what error does it produce?

[Mauricio Collares]

lake exe cache get should recreate it. Either way, my current best guess for the problem is that you probably don't have curl on your PATH, but that feels unlikely somehow.

[Julian Berman]

Last I recall cache will download a curl binary if one isn't present or new enough.

[Mauricio Collares]

It does download a new version of curl if it detects an old one. But it uses curl to do that, so you're in trouble if you have no version at all.

[Julian Berman]

Aha.

[Julian Berman]

(curl on macOS is in /usr/bin/ so that would be strange to not have one at all especially with SIP enabled unless you cleared out your PATH somehow, but let's see...)

[Aatman Supkar]

curl -V works, so I think that's quite alright. The current error is Lean just repeatedly crashing after every restart.

[Mauricio Collares]

This is quite a mystery, please provide more information if you have it! Stack traces, for example, or anything you think could be relevant

[Aatman Supkar]

Apologies, I'm very new to this. I'm not sure what all is relevant. I won't know what stack traces are, or how/where to find them. I'll be travelling for a while, and won't be able to communicate for about a day now. Further apologies for that.

[Julian Berman]

Can you just reconfirm which command you're running and its output -- I think I'd be trying to run lake exe cache get directly to start. You said it completes with no output? Can you run it and then tell us what echo $? says -- i.e. does it succeed? If so the issue will be with elan run --install it would seem (from glancing at the lakefile). But yeah good to confirm that first.

[Mauricio Collares]

Aatman Supkar said:

Apologies, I'm very new to this. I'm not sure what all is relevant. I won't know what stack traces are, or how/where to find them. I'll be travelling for a while, and won't be able to communicate for about a day now. Further apologies for that.

No worries! The only reason I mentioned "stack trace" is because you said Lean was crashing. What I meant to say is that any information that shows up with the crash (if any) will be helpful in diagnosing it.

[Aatman Supkar]

I ran echo $? after lake exe cache get. It returned 137. Assuming this is supposed to be printing the exit code from the previous message, this sounds like ... bad news?

Also, the VS Code GUI does not give me any actual information about the crash. Sorry about that :(

[Julian Berman]

Yes that at least confirms that it was silent and also failed.

[Julian Berman]

So it just runs and exits with no output?

[Aatman Supkar]

Yep.

[Julian Berman]

Can you also try lake exe cache get! (with the exclamation point) just in case as well.

[Aatman Supkar]

Nope, nothing. There were some intermediate dialogues that existed for a split-second, but in the end I have nothing.

Out of curiosity, may I ask what that does?

By the way, I feel like I should state this conjecture: My professor suspects that the problem is somehow MacOS specific.

[Julian Berman]

It's around the same as lake exe cache get (without the !) but rather than just downloading what you're missing it downloads everything.

[Julian Berman]

Sorry to still be shooting in the dark a bit, but would you mind deleting ~/.cache/mathlib as you did above, and then immediately running lake exe cache get! and then tell us what you see? That I should hope should have some output.

By the way, I feel like I should state this conjecture: My professor suspects that the problem is somehow MacOS specific.

It's always possible, but many of us, myself included, are on macOS.

[Aatman Supkar]

I have a surprise for you here. This folder has not been formed again.

[Julian Berman]

I have a surprise for you: I am never surprised by computers not doing what they're supposed to. But ok hm. Your ~/.cache doesn't have funny permissions perhaps? You can check that by running ls -l ~/.cache and telling us what you see in the output (or just ls -ld ~/.cache should suffice if you have lots of stuff there.

[Aatman Supkar]

image.png
I got this upon running the latter command. Are things alright? Do you think starting the project on an external SSD or something could be responsible, somehow? Just a conjecture I have...

[Julian Berman]

That looks OK to me. What do you mean by on an external SSD? Your home directory is on a different volume? Or you're saying you made this project on some other filesystem and transferred it over?

[Julian Berman]

Let's try something else. What happens if you run MATHLIB_CACHE_DIR=~/Library/Caches/mathlib lake exe cache get!? Any output? And does ~/Library/Caches/mathlib get created?

[Aatman Supkar]

The home directory is on my laptop. The project is on an external SSD connected to my laptop. After copy-pasting your command to the terminal, I can't find any output. This directory does not get created. Exit code 137.

[Julian Berman]

Hmmm. Is the external SSD an ancient filesystem like FAT? If not probably it doesn't matter I'd suspect. If you're not sure, diskutil list should say what filesystem it is. I'm out of ideas for tonight but I'm sure we're missing something simple so I'm pretty sure we'll get you sorted tomorrow if someone doesn't see it sooner!

[Yakov Pechersky]

There's always strace to figure out what syscalls are happening before the error exit

[Julian Berman]

fs_usage (or dtruss) given this is macOS, but yeah that's a good idea.

[Aatman Supkar]

Output of diskutil list:
image.png

How am I supposed to use the fs_usage thing? Sorry, I've not seen this thing before :sweat_smile:

I purchased the SSD last year. I doubt the file system should be all that archaic.

[Aatman Supkar]

Hi! Any input on the problem would be deeply appreciated. Even if you don't have any clear diagnoses, please recommend any tests I should be running. Also, does anyone have any idea what the error code 137 means? Is there a documentation for the error codes?

[Julian Berman]

Hmmm... I take it the external drive is the bottom one from that output -- and from that output it's an NTFS volume. I don't recall how good macOS's support for NTFS is at this point. Let's check.

[Julian Berman]

(Certainly if you only use the drive with macOS it would have been wise to re-partition it as an APFS volume, but if you've been using it for awhile or if you use it as a shared volume then that may not be convenient -- also it may not be relevant, but you're right that it at least could be)

[Julian Berman]

Yeah google would seem to suggest that NTFS still isn't a writable filesystem on macOS -- that's the drive the project is on? How did you even get it onto it? Do you pay for Paragon NTFS, or did you connect this drive to a Windows computer, or?

[Aatman Supkar]

A friend once borrowed the drive for a temporary backup on his Windows PC. That might be it. What am I supposed to do from here?

[Julian Berman]

Do you have any data on the drive?

[Julian Berman]

Or is it empty and you're trying to put your project on it? I'm still slightly unclear there

[Aatman Supkar]

Yep, the is some data on the drive already. But I am not facing issues while using anything else on the drive.

[Julian Berman]

I think copying the project to the same filesystem your home directory is on and trying to edit it there is worth trying if you haven't yet done so

[Aatman Supkar]

Could I somehow change the file system on the drive? My laptop has low storage and I'd like to avoid keeping the project in its storage...

[Kevin Buzzard]

Sure, but this is not a lean question, just reformat the drive (note you'll lose all data on it); do a web search for more details.

[Aatman Supkar]

Cool, thanks.

[Aatman Supkar]

The community here has been incredibly helpful, so I think it's a moral responsibility for me to let you guys know that the setup finally works! The drive encryption was precisely the issue. The reason I didn't notice this in forever was because macs can read Windows NTFS, but not write into it. Everything works smoothly with the formatted drive. Thanks guys!!

Moderators should feel free to label the topic resolved. I can't do it, now that some messages have existed here for over seven days.

[Mauricio Collares]

If you don't mind me asking, how did you clone the project in the first place? Did you plug the external drive on a Windows machine?