Zulip Chat Archive

Stream: mathlib4

Topic: Issues importing mathlib4


Adam Topaz (Oct 13 2022 at 13:58):

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 (Oct 13 2022 at 13:59):

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 (Oct 13 2022 at 14:01):

Most of the errors look to be related to RBMap

Floris van Doorn (Oct 13 2022 at 14:05):

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

Adam Topaz (Oct 13 2022 at 14:06):

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

Adam Topaz (Oct 13 2022 at 14:07):

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

Floris van Doorn (Oct 13 2022 at 14:07):

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 (Oct 13 2022 at 14:07):

Shouldn't that override the default one?

Floris van Doorn (Oct 13 2022 at 14:08):

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

Adam Topaz (Oct 13 2022 at 14:08):

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

Adam Topaz (Oct 13 2022 at 14:09):

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 (Oct 13 2022 at 14:10):

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

Adam Topaz (Oct 13 2022 at 14:10):

that seems to be the issue

Floris van Doorn (Oct 13 2022 at 14:10):

probably elan override unset might help

Adam Topaz (Oct 13 2022 at 14:11):

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

Adam Topaz (Oct 13 2022 at 14:12):

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 (Oct 13 2022 at 14:12):

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 (Oct 13 2022 at 14:16):

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 (Oct 13 2022 at 14:16):

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

Adam Topaz (Oct 13 2022 at 14:17):

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

Floris van Doorn (Oct 13 2022 at 14:18):

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

Adam Topaz (Oct 13 2022 at 14:23):

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 (Oct 13 2022 at 14:35):

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 (Oct 13 2022 at 21:56):

Can you create an issue on the lake repository?

Adam Topaz (Oct 13 2022 at 22:04):

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

pdc20 (Nov 03 2022 at 07:38):

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 (Nov 03 2022 at 07:47):

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

Mario Carneiro (Nov 03 2022 at 07:48):

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 (Nov 03 2022 at 07:58):

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 (Nov 03 2022 at 08:07):

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 (Nov 03 2022 at 08:25):

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

Topo_Space (Jan 21 2023 at 16:20):

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 (Jan 21 2023 at 16:52):

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

Topo_Space (Jan 21 2023 at 16:56):

similar to first post:

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

Topo_Space (Jan 21 2023 at 16:58):

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 (Jan 21 2023 at 17:09):

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 (Jan 21 2023 at 17:13):

yes, they were matched.

Topo_Space (Jan 21 2023 at 17:15):

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

Alistair Tucker (Jan 21 2023 at 17:16):

Yes elan works fine on Apple silicon.

Topo_Space (Jan 21 2023 at 17:17):

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 (Jan 21 2023 at 17:17):

i should install it with rosetta i guess

Alistair Tucker (Jan 21 2023 at 17:18):

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

Alistair Tucker (Jan 21 2023 at 17:18):

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

Topo_Space (Jan 21 2023 at 17:19):

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 (Jan 21 2023 at 17:19):

Yes.

Alistair Tucker (Jan 21 2023 at 17:21):

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 (Jan 21 2023 at 17:52):

is it possible to manually restart lean in terminal?

James Gallicchio (Jan 21 2023 at 17:53):

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

James Gallicchio (Jan 21 2023 at 17:56):

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 (Jan 21 2023 at 17:57):

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 (Jan 21 2023 at 20:00):

(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 (Jan 21 2023 at 21:07):

yes, it's the same

Topo_Space (Jan 21 2023 at 21:32):

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

Alistair Tucker (Jan 21 2023 at 22:21):

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 (Jan 22 2023 at 15:27):

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 (Jan 22 2023 at 15:27):

I'll ask under its topic.

Topo_Space (Jan 22 2023 at 16:31):

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


Last updated: Dec 20 2023 at 11:08 UTC