Referencing mathlib 4 from module

Stream: mathlib4

[Paul Chisholm]

I create a Lean 4 package with leanpkg init using the latest nightly. How do I then reference mathlib4 from modules in that package.

[Paul Chisholm]

To clarify, I don't mean how to import, I mean how to get mathlib4 on some search path so it is picked by imports in VS Code.

[Scott Morrison]

You probably want to switch from using leanpkg to using lake (which will be replacing it).

[Scott Morrison]

See https://github.com/leanprover/lake#creating-and-building-a-package

[Scott Morrison]

A minimal lakefile.lean that depends on mathlib4 might be:

import Lake

open Lake DSL System

package my_package
{ dependencies := #[
  { name := "mathlib",
    src := Source.git "https://github.com/leanprover-community/mathlib4.git", }], }

[Paul Chisholm]

Thanks very much, I have it working. A couple of things:

• I replaced the , after the URL string with "eaab772ea564d50801dc2a42af857a49038b8a54" to make it type check, picking up that string from the last commit in GitHub. Do I always have to include a specific value, and if so is the one I used correct?
• I notice the mathlib module lean-toolchain references a specific nightly. If the nightly my package uses is different, could that cause conflict?

[Mac]

@Paul Chisholm Yes on all accounts.