proof-lib/lean Turn the prelude into a proper Lean package

[clementblaudeau]

Currently, the Lean prelude lives inside the proof-lib/lean folder. To make it easier for users, it should be turned into a proper lean package

[oliver-butterley]

(It's possible I haven't precisely understood the plan with this issue so forgive me if I'm talking about different things.)

• I would propose that in the near future hax-lib/proof-libs/lean becomes a separate repo with automatic releases coinciding with Lean releases, This would make it more convenient to add Hax as a require in a Lean project and allow Hax it to keep up with the latest Lean whilst some users can keep working with prior versions if convenient for them.

• Concerning the boilerplate (lean-toolchain, lakefile, etc) that is required to make a lean project and so work with the lean file produced in the extraction folder: just a basic example repo setup with the rust files, and lean files together and related ci could be a low effort way to massively help people who want to get started quick with hax into lean.

[github-actions]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.