import real numbers

Stream: new members

[Atieh Hosseinizadeh]

Hello all
I wanted to import real numbers in Lean 4, however I got this error

import data.real.nnreal

error: unknown package 'data'

Do I need to install mathlib too?

[Heather Macbeth]

@Atieh Hosseinizadeh Yes, you need to install mathlib. And once you do, the filename convention is different from Lean 3 (which is where the line you quoted comes from); try

import Mathlib.Data.Real.NNReal

[Atieh Hosseinizadeh]

Thank you
I tried to install mathlib using this command:
pip3 install mathlibtool

and I got this error:
ERROR: Could not find a version that satisfies the requirement mathlibtool (from versions: none)
ERROR: No matching distribution found for mathlibtool

[Kalle Kytölä]

Should it be mathlibtools?

[Atieh Hosseinizadeh]

yeah thank you
it worked

[Atieh Hosseinizadeh]

After installing Mathlib I used this one:
import Mathlib.Data.Real.NNReal

but it's written:
unknown package 'Mathlib'

[Kevin Buzzard]

Do you want to use Lean 3 or Lean 4, or don't you know? Right now you are trying to use a mixture of both. mathlibtools is mathlib3. If you want to install mathlib4 then follow the instructions on the mathlib4 github page: https://github.com/leanprover-community/mathlib4/ .

[Atieh Hosseinizadeh]

I want to use Lean4
Okay thank you
Kevin Buzzard said:

Do you want to use Lean 3 or Lean 4, or don't you know? Right now you are trying to use a mixture of both. mathlibtools is mathlib3. If you want to install mathlib4 then follow the instructions on the mathlib4 github page: https://github.com/leanprover-community/mathlib4/ .

[Atieh Hosseinizadeh]

I installed Mathlib4 and I have all of its package on this directory:
C:\Users\Lenovo\.elan\bin>Mathlib
That is the place that I installed elan and lean too (for example: C:\Users\Lenovo\.elan\bin\elan)

But when I want to import one package like this: import Mathlib.Data.Real.NNReal

I got this error: unknown package 'Mathlib'

Why it doesn't know Mathlib?????? (I want to use Lean4)

[Kevin Buzzard]

Have you opened the root directory of a correctly formatted lean 4 project with mathlib as a dependency, in VS Code?

[Atieh Hosseinizadeh]

yeas I did it
I tried to use Std4 instead of Mathlib too but it didn't recognize Std package too

[Kevin Buzzard]

Maybe send a screenshot of VS Code showing the error and with the file manager open?

[Kevin Buzzard]

By the way did you actually put Mathlib inside .elan? Folders with a dot in their names are not in general places where users should be putting their stuff. Why not move Mathlib to somewhere else and then open the folder with VS Code?

[Ethan See]

Hi, I have a similar error when trying to import packages in lean4,
image.png

I think mathlib4 was not installed, when I try to do so following the instructions on https://github.com/leanprover-community/mathlib4/, I run into an error here,

image.png
Was my original lean installation not properly done? I know lean in general works, cause #eval and other commands work, the problem is only in importing packages so far.

What should I do to fix the package imports?

[Reid Barton]

data.nat looks like a Lean 3 module name, not a Lean 4 one, so that is an easy one.

[Ethan See]

I changed it to the other lean4 package name just now after reading the top comments. image.png

The problem remains tho.

[Reid Barton]

I think we saw an error like this defaultTarget one recently and it has something to do with having an older version of lean/lake installed

[Ethan See]

Should I just try reinstalling lean?

[Ethan See]

I did try the "elan self updates" command to see if everything was up to date

[Reid Barton]

What does elan toolchain list print?

[Ethan See]

image.png

[Reid Barton]

Then it seems like you may have skipped step 2 from the instructions you linked to:

Update your default toolchain to one that is sufficiently recent with elan default leanprover/lean4:nightly-2023-02-04

[Reid Barton]

Maybe elan toolchain install leanprover/lean4:nightly will also work.

[Ethan See]

Thanks, I am trying elan toolchain install leanprover/lean4:nightly now

[Ethan See]

As for the above step 2, does the command you suggested sync/ update the toolchain?

[Ethan See]

Ended up getting this, image.png

[Reid Barton]

(An explanation is that the name default_target that should appear in the lakefile (which describes how to build your package) used to be defaultTarget ~5 months ago, so if you downloaded the lean4:nightly toolchain before then and haven't updated since then you would have an old version that creates the wrong syntax for the current version.)

[Reid Barton]

Interesting... do you have any more luck with elan default leanprover/lean4:nightly-2023-02-04?

[Ethan See]

Yeah I have had more luck with that, image.png

[Reid Barton]

OK, then try creating a new project again continuing from step 3 (lake new ...)

[Ethan See]

I actually havent done this step of guide yet, image.png

When I try I get this,
image.png

[Ethan See]

Could I ask how different terminals in Vs Code might affect the installation processes, cause originally i installed lean via WSL Ubuntu cause I use Windows. On Vs Code I tend to use Git Bash instead. Is it better to try sticking to WSL Ubuntu terminal or can I switch between them?

[Reid Barton]

I wouldn't worry about lake exe cache get until your project is otherwise working.

[Reid Barton]

I don't use Windows (or VS Code) so I can't say for sure, but I guess that at least these errors so far are not due to mixing them.

[Ethan See]

image.png

I ran the lake new command, it seems to work

[Ethan See]

Or at least it didnt throw errors

[Ethan See]

I have gotten to this step before it throws the error below.
image.png
image.png

[Reid Barton]

Did you change directory into the new project? (probably cd lean4-samples)

[Ethan See]

I didnt, thanks, changing it now

[Ethan See]

image.png

[Ethan See]

It says it cant find lakefile.lean but in my file explorer I can find multiple instances of it
image.png

There are quite a few cause I cloned the directory from github and in each sample project, there is an instance of lakefile.lean

[Reid Barton]

I feel like what you're doing isn't the same as what you're saying you're doing.

[Reid Barton]

I thought you were making a new project; how can it have all these different subdirectories already?

[Ethan See]

That is true, I thought just to run the lake new command to see if it was working

[Reid Barton]

None of the steps listed at https://github.com/leanprover-community/mathlib4 are "clone the lean4-samples directory from somewhere".

[Reid Barton]

OK, well, pick one thing; try to do it; see where you get stuck; explain the error, and what you did so far.

[Reid Barton]

Otherwise, it's too hard.

[Ethan See]

Ok, thanks for your help

[Ethan See]

Hi Reid, I successfully built the new project, image.png

Thank you so much for your time and help just now.