error: unknown package 'Mathlib'

Stream: lean4

[Jaeboum Kim]

When I use vscode I do not have errors.
However, I execute "lean test.lean" on console mode on linux sever or MacBook. I got the "error: unknown package 'Mathlib'".
Could you help me to fix the error?

[Kevin Buzzard]

Is the file test.lean in a correctly-formatted lean 4 project which has mathlib as a dependency?

[Kevin Buzzard]

Wait -- I think you're supposed to use lake for building files on the command line. Does it work with lake build?

[Chris Bailey]

I think you have to do something like lake env lean test.lean if you're not running a built binary.

[Jaeboum Kim]

The file includes this line. The error occurred at the line
import Mathlib.Data.Real.Sqrt

$ lake build
info: myproject: no previous manifest, creating one from scratch
[0/6] Building Myproject.Basic
[1/6] Compiling Myproject.Basic
[1/6] Building Myproject
[3/6] Compiling Myproject
[3/6] Building Main
[4/6] Compiling Main
[6/6] Linking myproject

$ lake env lean test.lean
test.lean:1:0: error: unknown package 'Mathlib'
test.lean:5:10: error: expected token

$ lean --version
Lean (version 4.7.0, x86_64-unknown-linux-gnu, commit 6fce8f7d5cd1, Release)
$ lake --version
Lake version 5.0.0-6fce8f7 (Lean version 4.7.0)

[Chris Bailey]

Can you share the contents of your lakefile.lean?

[Jaeboum Kim]

@Chris Bailey Thanks for your comment.
I added require mathlib ~~~.

-

--[lakefile.lean]----
import Lake
open Lake DSL

package «myproject» where
  -- add package configuration options here

lean_lib «Myproject» where
  -- add library configuration options here

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git"

@[default_target]
lean_exe «myproject» where
  root := `Main

However, I got the following errors..

$ lake update
mathlib: cloning https://github.com/leanprover-community/mathlib4.git to './.lake/packages/mathlib'
error: ./.lake/packages/mathlib/lakefile.lean:90:2: error: unknown attribute [test_driver]
error: ./.lake/packages/mathlib/lakefile.lean: package configuration has errors

[Chris Bailey]

Your version (4.7.0) is behind mathlib's master, try updating your lean-toolchain file:

leanprover/lean4:v4.9.0-rc2

[Chris Bailey]

(Things are still moving pretty quickly)

[Chris Bailey]

If you're a vscode user, there's also an option in the command pane for "Lean 4 Project: Create Project Using Mathlib" that should get you a working setup with mathlib.

[Jaeboum Kim]

Chris Bailey said:

Your version (4.7.0) is behind mathlib's master, try updating your lean-toolchain file:

leanprover/lean4:v4.9.0-rc2

I updated lean-toolchain file with "leanprover/lean4:v4.9.0-rc2"

and execute the following commands

lake update
lake rebuild

Finally, I fixed the problem!!! Thank you so much!