lean-auto usage instructions

Stream: general

[Shreyas Srinivas]

The README.md on the lean-auto repository gives no instructions for installing it and there don't seem to be any version tags. Is the repository not meant to be used at present?

[Mauricio Collares]

There's a v4.11.0 tag, but I assume you're wondering about the lack of more recent ones.

[Shreyas Srinivas]

Yes

[Shreyas Srinivas]

Another confusing point is, lean-auto seems to depend on duper (based on README), but duper in-turn seems to depend on lean-auto (based on a look at the lakefile of duper, which pin lean-auto to a specific commit)

[Shreyas Srinivas]

what comes first? The chicken or the egg? More precisely, what's the correct way to get working with them

[Chris Bailey]

Shreyas Srinivas said:

lean-auto seems to depend on duper (based on README)

Where does the README say this?

[Shreyas Srinivas]

Currently, proof reconstruction can be handled by Duper, a higher-order superposition prover written in Lean. To enable Duper, please import the duper repo in your project, and set the following options:

[Chris Bailey]

Taking the fact that duper is not in the project's manifest into account, I'm pretty sure "please import the duper repo in your project" means "you can import and use duper downstream to construct and feed proofs to lean-auto".

[Shreyas Srinivas]

Yes, but then which version of lean-auto am I using when I add duper along with lean-auto to my dependencies?

[Shreyas Srinivas]

the lean-auto in my lakefile or the lean-auto that duper depends on?

[Shreyas Srinivas]

It is another issue that just trying to add duper causes a lot of trouble: https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Bug.3A.20lake.20update.20making.20unwanted.20toolchain.20update/near/486526809

[Chris Bailey]

Shreyas Srinivas said:

Yes, but then which version of lean-auto am I using when I add duper along with lean-auto to my dependencies?

If you depend on duper, you will be able to import and use lean-auto (or whatever other downstream deps) without adding them to your project's dependencies. If I build a project that only imports duper, the example from the lean-auto readme works without my project explicitly importing lean-auto.

[Chris Bailey]

In which case you'll obviously be using the version duper imports. AFAIK you can't do the rust thing where your project depends on a different version of a library also used by a dependency.