Zulip Chat Archive

Stream: new members

Topic: error with imports

Dean Young (Mar 22 2023 at 20:09):

These imports don't seem to work in my MS code version:


I get this:

object file '/Users/elliotyoung/.elan/toolchains/leanprover--lean4---stable/lib/lean/init/default.olean' of module init.default does not exist

Alex J. Best (Mar 22 2023 at 20:11):

It looks like you are using lean 4 with lean 3 style imports?

Dean Young (Mar 22 2023 at 20:23):

Alex J. Best said:

It looks like you are using lean 4 with lean 3 style imports?

oh shoot...

I guess I still haven't learned how to import properly. I just want the metric spaces part right now, specifically pre metrics.

Alex J. Best (Mar 22 2023 at 20:46):

Are you using Lean 3 or Lean 4?
In Lean 3 import are lower case, in lean 4 they are upper case and start with Mathlib. or Lean..
You should also never need to import something from init

Dean Young (Mar 25 2023 at 00:37):

I'm using lean 4... can you help me convert these to lean 4 imports?

Yaël Dillies (Mar 25 2023 at 09:26):

Prepend each import with Mathlib. and capitalise each first letter:


Dean Young (Apr 15 2023 at 00:03):

I still get this:

/Users/elliotyoung/Documents/Math/Math/Main.lean:1:0: error: file 'Mathlib/Tactic/Positivity' 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/Math/Math/Main.lean:2:0: error: invalid import: Mathlib.Tactic.Positivity

and lean --path gives me

  "is_user_leanpkg_path": true,
  "leanpkg_path_file": "/Users/elliotyoung/.lean/leanpkg.path",
  "path": [

MonadMaverick (Apr 15 2023 at 00:13):

Mathlib/Tactic/Positivity looks like a mathlib4/lean4 file while stable toolchain is lean3

MonadMaverick (Apr 15 2023 at 00:30):

try run this in your project root directory:

echo "leanprover/lean4:nightly-2023-04-11" > lean-toolchain

Or a powershell equivalent if you don't have bash

Last updated: Dec 20 2023 at 11:08 UTC