Zulip Chat Archive
Stream: new members
Topic: libraries, different version of mathlib
Martin Dvořák (Dec 12 2022 at 07:58):
Can a project depend on two libraries, each of which depends on a different version of mathlib?
Ruben Van de Velde (Dec 12 2022 at 08:00):
That sounds like a recipe for pain
Reid Barton (Dec 12 2022 at 08:23):
Even if it's somehow technically possible, surely not a good idea
Martin Dvořák (Dec 12 2022 at 08:30):
What mechanism prevents me from proving false? Does every use of a definition from mathlib carry the information which version of mathlib it is from, making two different definitions incompatible in one theorem?
Reid Barton (Dec 12 2022 at 08:33):
I think Lean will just complain about definitions in the environment with the same name
Reid Barton (Dec 12 2022 at 08:45):
Or more likely leanpkg will just grab one of the two versions of mathlib and your other dependency will have to deal with having the "wrong" version
Martin Dvořák (Dec 12 2022 at 09:09):
What do you mean? Will the other dependency be recompiled as it is with the "wrong" definitions, and possibly fail?
Kevin Buzzard (Dec 12 2022 at 11:16):
Why don't you try it and find out? Sounds like other people don't particularly want pain.
Martin Dvořák (Dec 12 2022 at 11:18):
I thought it was generally known to everybody except newbies like me.
Kevin Buzzard (Dec 12 2022 at 11:18):
I'm afraid it's only generally known that this is clearly a bad idea.
Kevin Buzzard (Dec 12 2022 at 11:20):
Please report back :-)
Martin Dvořák (Dec 12 2022 at 12:05):
Kevin Buzzard said:
Why don't you try it and find out? Sounds like other people don't particularly want pain.
It will take me a long time — I don't know how dependencies work (and this experiment will require a non-trivial amount of work with them).
Alex J. Best (Dec 12 2022 at 12:44):
Martin Dvořák said:
I thought it was generally known to everybody except newbies like me.
Most people here (even experts) tend to only use a dependency chain of their favourite project -> mathlib I would guess
Martin Dvořák (Dec 12 2022 at 13:21):
Alex J. Best said:
Most people here (even experts) tend to only use a dependency chain of
their favourite project -> mathlibI would guess
It probably means that our community is doing exceptionally well in avoiding dependency hell!
Martin Dvořák (Dec 12 2022 at 13:23):
I actually like that there is practically only one library for Lean 3.
Eric Wieser (Dec 12 2022 at 13:26):
If you try and use leanpkg with two dependencies A and B that use different versions of mathlib, it will either pick one arbitrarily (likely causing one of A or B not to build any more), or tell you that your project configuration is invalid
Last updated: Dec 20 2023 at 11:08 UTC