Zulip Chat Archive

Stream: general

Topic: support for libraries other than mathlib


view this post on Zulip Jason Rute (May 30 2020 at 19:01):

I know the most common setup for Lean is to have the following three sources of lean files

  • lean core library (from elan)
  • mathlib (in _target directory)
  • current project src directory

Is there a natural way to have another dependency as follows?

  • lean core library (from elan)
  • mathlib (in _target directory)
  • some 3rd party library of lean files from another repo
  • current project src directory

Let's say someone (like me) makes a library of lean tools, but for certain reasons these shouldn't go in mathlib (maybe they require tensorflow). Is there a way for a user to use those tools in their current project alongside mathlib? Is this doable with leanproject?

view this post on Zulip Yury G. Kudryashov (May 30 2020 at 19:05):

Add to [dependencies] in leanpkg.toml?

view this post on Zulip Alex J. Best (May 30 2020 at 19:06):

Yeah leanpkg add should do this for you, putting the repo in _target.

view this post on Zulip Patrick Massot (May 30 2020 at 19:10):

I don't remember if I wrapped that leanpkg feature in leanproject (I've never used it).

view this post on Zulip Jason Rute (May 30 2020 at 19:13):

Is it safe to modify leanpkg.toml? Does it interfere with leanproject? I've been told in the past that it is not safe to modify leanpkg.path.

view this post on Zulip Patrick Massot (May 30 2020 at 19:13):

It is safe

view this post on Zulip Patrick Massot (May 30 2020 at 19:13):

I hope

view this post on Zulip Patrick Massot (May 30 2020 at 19:14):

leanpkg.path definitely isn't

view this post on Zulip Jason Rute (May 30 2020 at 19:14):

Ok, I might test it later.

view this post on Zulip Patrick Massot (May 30 2020 at 19:15):

I mean it should be safe but it's totally untested since nobody has project depending on something which is not mathlib

view this post on Zulip Kevin Buzzard (May 30 2020 at 19:51):

In the old days before leanproject, people used to update their mathlib dependency by pulling a new mathlib in _target, compiling it, and then editing their leanpkg.toml. Then there was some cache-olean program (which may or may not still work) which meant that you might not have to compile mathlib when you updated it. Of course if you're prepared to compile mathlib while you're sleeping, then you can just do it the old days way (2018)

view this post on Zulip Johan Commelin (May 30 2020 at 19:53):

Nowadays I can compile mathlib again during my coffee break...

view this post on Zulip Jason Rute (May 30 2020 at 19:53):

I'd rather not. (I didn't think about .oleans and compiling, but right now, everything I have in my library will compile fast.)

view this post on Zulip Kevin Buzzard (May 30 2020 at 20:00):

One thing I used to do with a project which I kept up to date with mathlib in the old days, was that when I updated mathlib I just recompiled the project, rather than recompiling mathlib. That way only the bits of mathlib which I needed got recompiled.

view this post on Zulip Reid Barton (May 30 2020 at 20:17):

Kevin Buzzard said:

In the old days before leanproject, people used to update their mathlib dependency by pulling a new mathlib in _target, compiling it, and then editing their leanpkg.toml.

Or just edit leanpkg.toml and leanpkg will do the other things for you.


Last updated: May 11 2021 at 22:14 UTC