leanprover-community / lean-auto

Experiments in automation for Lean
Apache License 2.0
75 stars 12 forks source link

feat: bump Std #17

Closed kim-em closed 9 months ago

kim-em commented 9 months ago

The newly open-sourced LNSym repository uses lean-auto, but I would like to update it to use a recent version of Std (so that in turn I can remove the dependency on Mathlib entirely).

However lean-auto is not compatible with the main branch of Std.

This PR updates it.

I propose that going forward the main branch of lean-auto tracks the main branch of Std as closely as proves necessary for downstream projects (I'm happy to contribute maintenance PRs here for major consumers like LNSym). If it is appropriate to have pinned versions I recommend that we create tags e.g. v4.6.0 or v4.7.0-rc1, that are on particular toolchains, and ideally depend on the corresponding tag for Std.