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