support for libraries other than mathlib

Stream: general

[Jason Rute]

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?

[Yury G. Kudryashov]

Add to [dependencies] in leanpkg.toml?

[Alex J. Best]

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

[Patrick Massot]

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

[Jason Rute]

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.

[Patrick Massot]

It is safe

[Patrick Massot]

I hope

[Patrick Massot]

leanpkg.path definitely isn't

[Jason Rute]

Ok, I might test it later.

[Patrick Massot]

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

[Kevin Buzzard]

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)

[Johan Commelin]

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

[Jason Rute]

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

[Kevin Buzzard]

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.

[Reid Barton]

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.