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.

[Daniel Rehsmann]

Hello there, I am quite new to Lean, and have following question.
I have a very strange behavior importing a mathlib folder.
While both of these work

import Mathlib.Tactic
import Mathlib.Analysis.Calculus.Deriv.Abs

when running lake build.
Following code, however,
import Mathlib.Analysis.Calculus.Deriv
gives the error:

error: no such file or directory (error code: 2)

This does not seem very plausible to me. The same problems occur when I want to import any Analysis folder. What am I missing?

[Notification Bot]

A message was moved here from #mathlib4 > queueboard survey by Daniel Rehsmann.

[Patrick Massot]

This is probably a problem with your project setup.

[Patrick Massot]

Or maybe you typed this in a project created a long time ago and files were renamed.

[Damiano Testa]

Also, the fact that the module Mathlib.Analysis.Calculus.Deriv does not seem to exist: this is a folder, but there is no Mathlib/Analysis/Calculus/Deriv.lean file.

[Daniel Rehsmann]

But this argument holds also for Mathlib.Tactic

[Damiano Testa]

No, there is a Mathlib/Tactic.lean file.

[Patrick Massot]

Oh sorry, I read the message too quickly.

[Patrick Massot]

Discard what I wrote and read Damiano’s messages instead.

[Daniel Rehsmann]

I see so I cannot import folders in general?

[Damiano Testa]

What is confusing is the error message that says error: no such file or directory (error code: 2), emphasis on the directory. You can only import files.

[Damiano Testa]

Daniel Rehsmann said:

I see so I cannot import folders in general?

Correct, the workaround is to create the files in the directories that you want to import that consist just of lines of the form import <all files in your dir>.

[Damiano Testa]

The Mathlib.lean, Mathlib/Tactic.lean and a couple more are generated by a script and kept up to date. For everything else... you are on your own! :smile:

[Daniel Rehsmann]

Perfect. I understand. The error message was really confusing (together with the fact that Tactics is a folder AND a directory).
Thank you for the blazingly fast help. Where can I file a bug report on the error message - is this a Lean issue?

[Damiano Testa]

You may first report the error message by posting an example in the #lean4 channel. If it does not get solved right away, you may be asked to open an issue for it.

[Kim Morrison]

Yes, please open an issue!