Duper & Mathlib

Stream: general

[Luigi Massacci]

Maybe I just missed a thread with the answer, but is there an approximate timeline as to when (if?) it will be possible to use duper in mathlib contributions?

[Ruben Van de Velde]

Not as far as I'm aware

[Luigi Massacci]

I forgot to tag @Josh Clune

[Josh Clune]

We do very much intend/hope to add a Mathlib dependency on Duper so that it will be possible to use Duper in Mathlib contributions. Currently, there is a technical challenge pertaining to how olean files are compiled that makes supporting Mathlib's lake exe cache get difficult with a Duper dependency. Our current plan is to work towards a full sledgehammer-like pipeline first (that work is actively underway) and then discuss these technical challenges with the maintainers once there is greater demand. We've been operating under the assumption that most users would find Duper somewhat difficult to regularly use before it's integrated in a full sledgehammer-like pipeline, but I'm open to reconsidering the order in which these problems are tackled if that assumption is off-base. Out of curiosity @Luigi Massacci, are you asking because you're currently wanting to use Duper in Mathlib contributions, or was this just a more general question?

[Kim Morrison]

There's a chicken and egg problem adding large dependencies to Mathlib. We need to have sufficient confidence in the maintainability of the project (through whatever combination of long term external maintainers and Mathlib maintainers is available). But until it is usable in Mathlib it's harder to get enough usage to polish the project, and recruit the team who will support it!

Being associated or run out of the Hoskinson Centre certainly helps for credible sustainability externally.

[Kim Morrison]

I'm really excited about sledgehammers coming to Lean!

[Luigi Massacci]

Josh Clune said:

Out of curiosity Luigi Massacci, are you asking because you're currently wanting to use Duper in Mathlib contributions, or was this just a more general question?

I asked because I've been playing around with it on toy examples and found it quite cool, but of course I would like to be able to use on non-toy stuff, which is fairly synonymous with Mathlib in my mind

[Marcus Rossel]

Josh Clune said:

Our current plan is to work towards a full sledgehammer-like pipeline first (that work is actively underway)

Is that work public somewhere?

[Floris van Doorn]

I believe it is this repo: https://github.com/leanprover-community/lean-auto

[Josh Clune]

The lean-auto repository that Floris linked is the repository being used to manage the connection between Lean and external provers. It also is used to manage Duper's preprocessing, so Duper has a dependency on it.

Ultimately, I expect that the repository that actually has the full sledgehammer-like pipeline won't be the lean-auto repository itself, but instead, a separate repository that depends on Duper, on the lean-auto repository, and on a repository that implements premise selection.