error with imports

Stream: new members

[Dean Young]

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

init.default
tactic.positivity
topology.algebra.order.compact
topology.bornology.constructions
topology.metric_space.emetric_space

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]

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

[Dean Young]

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]

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]

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

[Yaël Dillies]

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

Mathlib.Tactic.Positivity
Mathlib.Topology.Algebra.Order.Compact
Mathlib.Topology.Bornology.Constructions
Mathlib.Topology.MetricSpace.EMetricSpace

[Dean Young]

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": [
    "/Users/elliotyoung/.elan/toolchains/stable/bin/../library",
    "/Users/elliotyoung/.elan/toolchains/stable/bin/../lib/lean/library"
  ]
}

[MonadMaverick]

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

[MonadMaverick]

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