Issues importing mathlib4

Stream: mathlib4

[Adam Topaz]

I'm having some issues getting mathlib4 working.... here are the steps I follow:

lake new foobar math && cd foobar && echo "import Mathlib" > Foobar.lean && lake build

This results in several errors, the last one being

error: external command `/home/adam/.elan/toolchains/leanprover--lean4---nightly-2022-09-26/bin/lean` exited with code 1

What am I doing wrong?

[Adam Topaz]

A few more errors that look relevant:

error: stdout:
./lean_packages/mathlib/././Mathlib/Tactic/HelpCmd.lean:46:18: error: unknown identifier 'Lean.RBMap'
./lean_packages/mathlib/././Mathlib/Tactic/HelpCmd.lean:47:27: error: unknown identifier 'Lean.RBMap'
./lean_packages/mathlib/././Mathlib/Tactic/HelpCmd.lean:47:2: error: failed to construct 'ForIn' instance for collection
  ?m.827 _fun_discr✝ a✝

[Adam Topaz]

Most of the errors look to be related to RBMap

[Floris van Doorn]

It looks like you've set a globally default version of Lean, and mathlib4 uses a newer version.

[Adam Topaz]

$ lean --version
Lean (version 4.0.0-nightly-2022-09-26, commit fd1ae3118cd6, Release)

[Adam Topaz]

I'm confused why elan doesn't pick up the lean_toolchain file?

[Floris van Doorn]

on the latest mathlib4 I get

Floris@MSI MINGW64 /d/projects/mathlib4 ((a6c72be...))
$ lean --version
info: downloading component 'lean'
info: installing component 'lean'
Lean (version 4.0.0-nightly-2022-10-12, commit aa845dee98e3, Release)

[Adam Topaz]

Shouldn't that override the default one?

[Floris van Doorn]

I'm not sure how it works. Does elan self update help? What is the result of elan show?

[Adam Topaz]

Right, 2022-10-12 nightly matches what's listed in mathlib4

[Adam Topaz]

elan show gives this as the active toolchain in foobar:

active toolchain
----------------

leanprover/lean4:nightly-2022-09-26 (overridden by '/home/adam/foobar/lean-toolchain')
Lean (version 4.0.0-nightly-2022-09-26, commit fd1ae3118cd6, Release)

[Adam Topaz]

Is there a flag I can pass to lake that would generate the correct lean-toolchain file?

[Adam Topaz]

that seems to be the issue

[Floris van Doorn]

probably elan override unset might help

[Adam Topaz]

I have "/home/adam" = "leanprover/lean4:nightly" under ovverides in .elan/settings.toml.

[Adam Topaz]

If I remove that, then elan would revert to

default_toolchain = "leanprover-community/lean:3.42.1"

in my home folder, which means that I won't have lake available.

[Floris van Doorn]

I don't think you need overrides? Just let the repository tell you which version of Lean you want to use.
And if you need an override do it on project-by-project basis (not for mathlib4).

[Adam Topaz]

right, if I remove the override from my home folder, it reverts to lean3 as the default, which means that lake new foobar1 math doesn't work at all.

[Adam Topaz]

I guess the overarching question is this: What's the process to create a project with mathlib4 as a dependency?

[Adam Topaz]

I could manually modify the lean-toolchain file, but I don't think that's the intended behavior

[Floris van Doorn]

I have not done this yet, so I don't know...

[Adam Topaz]

Anyway, for now I just resorted to copying the lean-toolchain file from mathliv4 into my project's main dir, and everything builds just fine (as expected!).

[Adam Topaz]

A quick summary of the discussion: When using lake new foobar math, lake creates a new directory with a lean-toolchain file based on the version of lean from the directory in which lake was called, while also adding mathlib4 as a dependency. The problem is that this version of lean need not match the version required by the imported mathlib4.

When using lake new foobar math I would have guessed that lake would ensure that the lean-toolchain file in foobar matches the toolchain file from the version of mathlib4 that it adds as an import, but this is not the case.

[Scott Morrison]

Can you create an issue on the lake repository?

[Adam Topaz]

done @ https://github.com/leanprover/lake/issues/129

[pdc20]

So I was trying out Lean4 on vscode by following a tutorial here https://www.youtube.com/watch?v=DXvA1qaQFtY. Unfortunately when I typed import Mathlib at the top, I was greeted with an error from the IDE saying that the package was unrecognised. I was about 1:25 into the tutorial when the error popped up. I am on windows 10.

Does anyone know what the problem is?

[Mario Carneiro]

The step that includes mathlib as a dependency is lake new myproject math at the beginning of the video

[Mario Carneiro]

if you don't do that, you can still add mathlib as a dependency later by adding the following to lakefile.lean:

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

[pdc20]

I ended up removing the extension, deleting the .elan directory entirely and reinstalling elan and lake by reinstalling the extension. It seems to work now. I didn't have to make a new math project.
For those on windows who are having the same issue, you can usually expect to find the .elan directory in C:\users\username\.
I think this issue can be closed now. Thanks for your suggestion and taking the time to help me out!

[Mario Carneiro]

ah, ... yes you can do that too. Not my first recommendation but I suppose it works if you don't have anything you want to preserve

[pdc20]

I had only just started using lean, so I didn't have anything to lose.

[Topo_Space]

I have installed Lean4 extension on VSCode followed by elan and lake. it builds Mathlib without any errors, but I'm getting unknown package 'Mathlib' output in Lean Infoview. Is it compatible with apple silicon?

[Alistair Tucker]

Yes it should be. What invocation did you use for lake?

[Topo_Space]

similar to first post:

lake new foobar math && cd foobar &&  lake update && echo "import Mathlib" > Foobar.lean && lake build

[Topo_Space]

and also my lean4 extension doesn't able to download new libraries in realtime when I import them. I have to run lake build to download imported libraries

[Alistair Tucker]

I had some trouble before I matched the Lean version with mathlib's. Does elan show give the active toolchain as leanprover/lean4:nightly-2023-01-16?

[Topo_Space]

yes, they were matched.

[Topo_Space]

based on this instruction, it seems elan is incompatible with apple silicon. although it's for lean 3

[Alistair Tucker]

Yes elan works fine on Apple silicon.

[Topo_Space]

Specifically, elan – which is installed as part of the above instructions – will not be able to fetch Lean binaries on these devices if installed the normal way.

[Topo_Space]

i should install it with rosetta i guess

[Alistair Tucker]

There is the issue that no precompiled binaries are available for Lean 3

[Alistair Tucker]

But that is not the case with Lean 4. I have it working on this computer that doesn't have Rosetta installed.

[Topo_Space]

Alistair Tucker said:

But that is not the case with Lean 4. I have it working on this computer that doesn't have Rosetta installed.

MacOS Ventura 13.1?

[Alistair Tucker]

Yes.

[Alistair Tucker]

I'm sorry I can't help you more. I made a new lake project for the first time this morning and after some trial and error, with several restarts, it worked. But my problem was with the lean versions I think.

[Topo_Space]

is it possible to manually restart lean in terminal?

[James Gallicchio]

You can always ps -k any lean processes, that's worked well in the past for me :P

[James Gallicchio]

In vscode if you do Ctrl+Shift+P it brings up the command palette, and then you can select Lean 4: Restart Server which should (?) restart it

[James Gallicchio]

but if that doesn't work, pkill -f lean definitely will kill the lean processes, and then you should be able to trigger new server instances with the same vscode command

[Alistair Tucker]

(Did you check with elan show that the 2023-01-16 toolchain is active in the directory from which you are calling lake new?)

[Topo_Space]

yes, it's the same

[Topo_Space]

I have tried to install elan and lean extension using rosetta2, nothing changed. something is wrong here.

[Alistair Tucker]

If you're interested in Mathlib, perhaps you'd be better off with Lean 3 anyway? Right now it's only a small fraction of Mathlib that has been ported to Lean 4.

[Topo_Space]

Alistair Tucker said:

If you're interested in Mathlib, perhaps you'd be better off with Lean 3 anyway? Right now it's only a small fraction of Mathlib that has been ported to Lean 4.

same problem on Lean 3 :)

[Topo_Space]

I'll ask under its topic.

[Topo_Space]

only the project must be opened with vscode. not parent folder. problem solved.