mathlib4 as a dependency?

Stream: mathlib4

[Kevin Buzzard]

Can someone talk me through how to use mathlib4 as a dependency in a lean4 project? On Thursday evenings I goof around with mini Lean 4 experiments and I'm sick of copying Data.Set.Basic around from repo to repo.

[Daniel Selsam]

Do your goofing in a directory in mathlib4 that you don't commit?

[Kevin Buzzard]

Are you saying it's not possible right now?

[Daniel Selsam]

It is definitely possible. I use a custom setup though so I am unable to advise on the canonical way to do it. I thought this local-directory trick might be a satisfactory workaround for you for the very short-term.

[Marc Huisinga]

Kevin Buzzard said:

Can someone talk me through how to use mathlib4 as a dependency in a lean4 project? On Thursday evenings I goof around with mini Lean 4 experiments and I'm sick of copying Data.Set.Basic around from repo to repo.

You should be able to add it as a dependency to your leanpkg.toml like here:
https://github.com/mhuisi/lean4-cli/blob/main/leanpkg.toml

[François G. Dorais]

That's been working since January but the parser had issues with line breaks and spacing, maybe that can be fixed easily so we can put rev= on a separate line. In your leanpkg.toml add:

[dependencies]
MathLib4 = {git = "https://github.com/leanprover-community/mathlib4", rev = "<fill_me_in>"}

[Mario Carneiro]

regarding line breaks, that's just the way toml works. If you want multiple lines you can use something like

[dependencies.MathLib4]
git = "https://github.com/leanprover-community/mathlib"
rev = "<fill_me_in>"

(IIRC)

[Mark Wilhelm]

Hi is this supported currently? I tried creating a new empty package and importing mathlib4 like so --

lakefile.lean:

import Lake
open Lake DSL

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

Scratch5.lean:

import Mathlib.Logic.Basic
def hello := "world"

and "lake build" gives:

info: mathlib: trying to update ./lean_packages/mathlib to revision master
> LEAN_PATH=./build/lib:./lean_packages/mathlib/./build/lib /root/.elan/toolchains/leanprover--lean4---stable/bin/lean ./lean_packages/mathlib/././Mathlib/Tactic/OpenPrivate.lean -R ./lean_packages/mathlib/./. -o ./lean_packages/mathlib/./build/lib/Mathlib/Tactic/OpenPrivate.olean -i ./lean_packages/mathlib/./build/lib/Mathlib/Tactic/OpenPrivate.ilean -c ./lean_packages/mathlib/./build/ir/Mathlib/Tactic/OpenPrivate.c
> LEAN_PATH=./build/lib:./lean_packages/mathlib/./build/lib /root/.elan/toolchains/leanprover--lean4---stable/bin/lean ./lean_packages/mathlib/././Mathlib/Tactic/RCases.lean -R ./lean_packages/mathlib/./. -o ./lean_packages/mathlib/./build/lib/Mathlib/Tactic/RCases.olean -i ./lean_packages/mathlib/./build/lib/Mathlib/Tactic/RCases.ilean -c ./lean_packages/mathlib/./build/ir/Mathlib/Tactic/RCases.c
./lean_packages/mathlib/././Mathlib/Tactic/OpenPrivate.lean:36:24: error: cannot lift `(<- ...)` over a binder, this error usually happens when you are trying to lift a method nested in a `fun`, `let`, or `match`-alternative, and it can often be fixed by adding a missing `do`
./lean_packages/mathlib/././Mathlib/Tactic/OpenPrivate.lean:37:6: error: expected command

error: external command /root/.elan/toolchains/leanprover--lean4---stable/bin/lean exited with status 1
./lean_packages/mathlib/././Mathlib/Tactic/RCases.lean:328:8: error: expected '=>'
./lean_packages/mathlib/././Mathlib/Tactic/RCases.lean:371:0: error: invalid 'end', name is missing
./lean_packages/mathlib/././Mathlib/Tactic/RCases.lean:386:24: error: unknown identifier 'TermElabM'
./lean_packages/mathlib/././Mathlib/Tactic/RCases.lean:393:52: error: unknown identifier 'RCasesPatt'
./lean_packages/mathlib/././Mathlib/Tactic/RCases.lean:396:11: error: unknown identifier 'RCasesPatt.alts''
./lean_packages/mathlib/././Mathlib/Tactic/RCases.lean:398:11: error: unknown identifier 'RCasesPatt.typed'
./lean_packages/mathlib/././Mathlib/Tactic/RCases.lean:400:30: error: unknown identifier 'RCasesPatt.one'
./lean_packages/mathlib/././Mathlib/Tactic/RCases.lean:401:37: error: unknown identifier 'RCasesPatt.one'
./lean_packages/mathlib/././Mathlib/Tactic/RCases.lean:402:30: error: unknown identifier 'RCasesPatt.clear'
./lean_packages/mathlib/././Mathlib/Tactic/RCases.lean:404:11: error: unknown identifier 'RCasesPatt.tuple'
./lean_packages/mathlib/././Mathlib/Tactic/RCases.lean:425:9: error: unknown identifier 'RCasesPatt'
./lean_packages/mathlib/././Mathlib/Tactic/RCases.lean:432:6: error: unsupported pattern in syntax match
  RCasesPatt.typed ref pat ty
./lean_packages/mathlib/././Mathlib/Tactic/RCases.lean:429:15: error: unknown identifier 'processConstructor'
./lean_packages/mathlib/././Mathlib/Tactic/RCases.lean:437:11: error: unknown identifier 'rcasesContinue'
./lean_packages/mathlib/././Mathlib/Tactic/RCases.lean:438:7: error: invalid field notation, type is not of the form (C ...) where C is a constant
  gs
has type
  ?m.19077
./lean_packages/mathlib/././Mathlib/Tactic/RCases.lean:443:22: error: unknown identifier 'RCasesPatt'
./lean_packages/mathlib/././Mathlib/Tactic/RCases.lean:447:11: error: unknown identifier 'rcasesCore'
./lean_packages/mathlib/././Mathlib/Tactic/RCases.lean:448:22: error: invalid field notation, type is not of the form (C ...) where C is a constant
  gs
has type
  ?m.19643 pat ty✝ g ty g₁ a✝ discr✝ v g₂
./lean_packages/mathlib/././Mathlib/Tactic/RCases.lean:459:4: error: unknown identifier 'rcasesCore'
./lean_packages/mathlib/././Mathlib/Tactic/RCases.lean:458:26: error: invalid field notation, type is not of the form (C ...) where C is a constant
  pat
has type
  ?m.20541 g fs clears a ref pat✝¹ ty? cont a✝
./lean_packages/mathlib/././Mathlib/Tactic/RCases.lean:480:0: error: invalid 'end', insufficient scopes
./lean_packages/mathlib/././Mathlib/Tactic/RCases.lean:496:23: error: unknown identifier 'RCases.rcases'
./lean_packages/mathlib/././Mathlib/Tactic/RCases.lean:507:25: error: unknown identifier 'RCases.obtainNone'
./lean_packages/mathlib/././Mathlib/Tactic/RCases.lean:513:25: error: unknown identifier 'RCases.rcases'
./lean_packages/mathlib/././Mathlib/Tactic/RCases.lean:521:23: error: unknown identifier 'RCases.rintro'

error: external command /root/.elan/toolchains/leanprover--lean4---stable/bin/lean exited with status 1
error: build failed

should this work?

[Mario Carneiro]

mathport uses mathlib4 as a dependency, you might use that as an example

[Mario Carneiro]

My guess is that you are compiling mathlib with the wrong lean version. Mathport has a lean-toolchain file in the project root which is used by lake to select the right nightly version; right now it says leanprover/lean4:nightly-2022-02-17, which matches the lean-toolchain version inside the selected version of mathlib4

[Mark Wilhelm]

yes! that fixed it, thank you