unknown package Mathlib

Stream: lean4

[Ashvni Narayanan]

@Matej Penciak and I have been trying to use Mathlibport to view Mathlib 3 files in Lean 4. However, we get the error : unknown package Mathlib .
On importing Mathbin files, I get the error :
object file '.\lean_packages\mathlib\.\build\lib\Mathlib.olean' of module Mathlib does not exist
Can this be resolved?
Any help is appreciated, thank you!

[Mac]

What version of Lean are you on?

[Ashvni Narayanan]

Lean (version 4.0.0-nightly-2022-06-13, commit fb574af873d7, Release)

[Mac]

Ah, okay, yeah that does appear to be the correct version. What does your Lakefile look like?

[Ashvni Narayanan]

import Lake
open Lake DSL

package ZkSNARK

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

[Alexander Bentkamp]

I also get this error sometimes. My workaround/hack is the following:

cd lean_packages/mathlib
lake build

You might have to do the same in the other subdirectories of lean_packages.

[Ashvni Narayanan]

I get a build failed error

[Ashvni Narayanan]

I rebuilt it and it seems to be working now! Thank you!

[Alexander Bentkamp]

Would still be good to know from @Mac if there is a better solution or what might be causing this :-)

[Mac]

How are you importing Mathbin?

[Mac]

If you are doing something other than import Mathbin, mathlib will not get built (as only the top-level Mathbin explicitly imports Mathlib). Otherwise, if you are doing an import Mathbin.* (importing just some submodule), you need to also import Mathlib to ensure Mathlib gets built.

[Ashvni Narayanan]

I see (although currently the file seems to work without a Mathlib import)

[Mac]

@Ashvni Narayanan Well you just manually built Mathlib, so that's why. :wink: (That's what @Alexander Bentkamp had you do.)

[Ashvni Narayanan]

Ah right, sorry about that

[Mac]

'tis fine :big_smile:

[Alexander Bentkamp]

Thanks, I have been doing this wrong for 6 months or so :-)

[Alexander Bentkamp]

cc @Ramon Fernandez Mir