Use of mathlib?

Stream: iris-lean

[Quang Dao]

Should iris-lean import mathlib? Currently it does not, but I imagine that we will want all kinds of results from mathlib, like algebraic theories, big operators, category theory, etc.

[suhr]

I would prefer not to: Mathlib is a huge dependency. Importing Batteries and Aesop might be a good idea though.

[Mario Carneiro]

Batteries used to be a dependency, but recent changes to lean have made it unnecessary. I'm open to restoring that import if it becomes useful

[Mario Carneiro]

I think we should try to avoid importing mathlib, but it's easier to have this kind of discussion with respect to a concrete definition or theory we want rather than "algebraic theories, big operators, category theory, etc.". Iris is a library, it is intended to supply things for other downstream users, and those users may well import mathlib if they want those other things. But at least within Iris, so far it has seemed profitable to keep the category theory to the concrete side (Rocq-Iris also doesn't use any generic category theory and rolls their own classes here) so I don't think we really need anything from mathlib yet. Maybe we'll want something from lattice theory? I wouldn't be surprised if the things we need aren't upstreamed to lean or Batteries on their own, and we can also induce things to upstream if needed.

[Quang Dao]

I agree that the theory being supported should be discussed case-by-case, and also that things in Mathlib might be moved down to Batteries or Lean core in the future. I also don’t want iris-lean to be “blind” to mathlib definitions, so that other projects building on Iris needs to roll their own compatibility layer (which might lead to duplicate work across different repos).

Perhaps one could structure iris-lean as multiple Lean libraries. There could be an IrisCore library that has the basic theory and doesn’t import mathlib, then various extensions that does (for instance, I care about something like an IrisProb library for reasoning about probabilistic computations).

[Mario Carneiro]

we could have a compatibility layer as another lean project, unclear if it can live in the same repo without interfering with usage of the core project but that would be nice

[Mario Carneiro]

But I think this is largely hypothetical at this point, iris-lean has no users right now and I doubt that can change until it progresses to the point where it has the basic API like iProp

[Kevin Buzzard]

Just to remark that the equational theories project didn't depend on mathlib, and then they wanted to use mathlib a bit but it turned out that they had got definitions which conflicted with mathlib's definitions so they couldn't use mathlib. Of course the project was small and new so it wasn't too hard to sort out, but it's just a cautionary tale.

[Mario Carneiro]

there was already recently a PR which fixes a definition that clashes with mathlib, so I think this is sorted now

[Mario Carneiro]

it wasn't so much a clash as a direct borrowing

[Shreyas Srinivas]

Kevin Buzzard said:

Just to remark that the equational theories project didn't depend on mathlib, and then they wanted to use mathlib a bit but it turned out that they had got definitions which conflicted with mathlib's definitions so they couldn't use mathlib. Of course the project was small and new so it wasn't too hard to sort out, but it's just a cautionary tale.

Arguably it is mathlib that should do the responsible thing of not deciding what math concepts should mean for downstream users, by careful namespacing

[Shreyas Srinivas]

But I agree with Mario that mathlib is a huge dependency. Further, if it depended on mathlib, iris lean will have the extra job of maintaining compatibility with successive mathlib versions, while also keeping up with developments in Iris itself. This could result in conflicts if Iris benefits from a certain definition of a concept that mathlib doesn’t use.

[Mario Carneiro]

I don't think that iris definitions diverging from mathlib are likely to be a major problem. We'll just have separate definitions and not use mathlib's in that case (and provide a compatibility layer if appropriate)

[Mario Carneiro]

it's actually the opposite situation that is more problematic: if iris wants to use a definition from mathlib which is the same, it can't introduce it in a way that does not cause clashes or separate types which require a compatibility layer. That's basically what happened with the try? definition, it's a literal copy paste from mathlib because it's a useful function but having it causes troubles for importing mathlib and iris together