Trouble with imports

Stream: general

[Kind Bubble]

In a file Main.lean I have the text:

import Init.Data.ToString.Basic
def a := 1
def main := IO.println ""

And it produces this error when I run

cd ; cd /Users/elliotyoung/Documents/Workflow/WorkflowI/template; lean --run Main.lean > output.txt

/Users/elliotyoung/Documents/Workflow/WorkflowI/template/Main.lean:1:0: error: file 'Init/Data/ToString/Basic' not found in the search path
Use 'lean --path' to see where lean is looking, or https://leanprover-community.github.io/file-not-found.html for more
/Users/elliotyoung/Documents/Workflow/WorkflowI/template/Main.lean:1:0: error: invalid import: Init.Data.ToString.Basic
could not resolve import: Init.Data.ToString.Basic
/Users/elliotyoung/Documents/Workflow/WorkflowI/template/Main.lean:3:12: error: unknown identifier 'IO.println'
/Users/elliotyoung/Documents/Workflow/WorkflowI/template/Main.lean:3:4: error: don't know how to synthesize placeholder
context:
⊢ Sort ?
<unknown>:1:1: error: could not resolve import: Init.Data.ToString.Basic

It appears I have math lib installed but that there's something about having a Mac M2 that's giving me trouble?

[Sebastian Ullrich]

It looks like you're running Lean 3

[Sebastian Ullrich]

Btw, Init is imported automatically

[Kind Bubble]

How might I switch to Lean 4? Will I have to uninstall Lean 3?

[Kevin Buzzard]

If you have a correctly formatted lean 4 project then lean 4 should just work. You don't have to uninstall lean 3.

[Kevin Buzzard]

You'll need the lean 4 VS Code extension and a correct project (I just use mathlib4)

[Arthur Paulino]

Did you use lake to start your project?

[Bolton Bailey]

I am also not clear on how to import files in Lean 4. I have import Foo.Bar at the top of my file, and it says:

unknown package 'Foo'
You might need to open '/Users/boltonbailey/Desktop/test/testproject' as a workspace in your editor

But I opened the project in VSCode like any other project. Am I doing something wrong?

[Bolton Bailey]

My directory structure looks like

testproject
  Foo
    Bar.lean
    Baz.lean
Importtest.lean
lakefile.lean
Main.lean

I ran lake init and then added the Foo directory

[Bolton Bailey]

Seems this thread might be important

[Mario Carneiro]

what does your lakefile look like?

[Sebastian Ullrich]

Foomust be in the same directory as the lakefile

[Lisa Chen]

I've been trying for a total of like 4 hours and I cannot get the imports to work. I'm honestly not sure where I'm going wrong ;-;
Screenshot 2025-04-15 at 1.20.50 PM.png
Screenshot 2025-04-15 at 1.21.02 PM.png

[Kyle Miller]

Has lake exe cache get worked?

[Lisa Chen]

Screenshot 2025-04-15 at 1.32.42 PM.png
It did, but I had it removed because I thought maybe it was affecting the downloads I was getting from MathLib

[Lisa Chen]

But I added it back now, is it suppose to do something?

[Kyle Miller]

I'm meaning to ask whether you were able to run the lake exe cache get command from a terminal. A lake_exe declaration in a lakefile is different (it's specifying an executable that should be built). It should have no effect on your problem.

[Lisa Chen]

Ohh i see

[Lisa Chen]

I'll run it and let you know what happens

[Lisa Chen]

Screenshot 2025-04-15 at 1.43.36 PM.png

It runs successfully it that says anything

[Kyle Miller]

Can you try lake build?

[Lisa Chen]

Screenshot 2025-04-15 at 1.44.42 PM.png
It also builds successfully

[Kyle Miller]

Make user your Basic.lean file is saved. We're wanting to test importing.

[Lisa Chen]

Alright, so I just saved the file and ran the commands again but it says the same thing

[Kyle Miller]

If that lake build works, maybe if you restart VS Code everything will Just Work.

[Kyle Miller]

(There are commands you could run from within VS Code, but sometimes it's easier to say turn it off and on again.)

[Lisa Chen]

LOL alright, i'll try that

[Kyle Miller]

Relevant commands for the future:

• "Lean 4: Restart server" will kill and restart Lean
• "Developer: Reload window" seems to do that while also restarting the extension and resetting everything
• I don't think I've ever needed to actually close VS Code fully, except when updating it.

[Mario Carneiro]

(I think changes to environment variables need a restart of vscode)

[Lisa Chen]

So it did work, but it also caused other parts of my code to fail. So i need to now fix my python parts because the lean stuff is interfering with it.

[Lisa Chen]

Screenshot 2025-04-15 at 1.59.13 PM.png
Screenshot 2025-04-15 at 1.59.27 PM.png
I pasted some lean code in there but now other parts of the lean code isn't working ;-;
Is my Mathlib working?

[Mario Carneiro]

that's lean 3 code, is this LLM generated? (yes - I just noticed the project name)

[Mario Carneiro]

from what I can see the server is correctly responding to the text

[Lisa Chen]

Yep! It's LLM generated lmao. Lemme change the prompt so it'll generate lean 4 code
Thank you!

[Lisa Chen]

Screenshot 2025-04-15 at 2.21.40 PM.png
Sooo the same problem is happening as before which is the imports. For some reason the imports are not recognized.

[Ruben Van de Velde]

Well duh, that's still lean 3

[Lisa Chen]

oh...

[Ruben Van de Velde]

I suggest you read some of the documentation on the website rather than have an LLM hallucinate some code at you

[Kyle Miller]

I don't think we can expect anyone new to Lean to be able to spot the differences between Lean 3 and Lean 4. (But also Lisa, please don't expect anyone here to want to help debug LLM-generated code; people are very willing to help others learn Lean here though!)

Giveaways that it's Lean 3:

• lower-case imports
• no Mathlib. prefixes in the imports
• | m :=, which is now | m =>
• let ... in
• lambdas with commas instead of => or \mapsto

Lean 4 is a different language from Lean 3. It's similar enough that all of mathlib3 was ported to Lean 4, but it's a significant effort.

[Michael Rothgang]

begin ... end was another signal, in the version code version