Uncompatible lean version for different libraries

[MarkJYC001]

REPL is a really wonderful tool to use. I really appreciate your efforts on this.

However, I have a problem automatically evaluating datasets from different Lean version

For instance:
I am trying MiniF2F-lean4, a lean 4 version lean library with many organized statements, but it is of version leanprover/lean4:v4.20.0. Thus, I can not find a version of lean that is compatible with both REPL and MiniF2F-lean4.

[augustepoiroux]

Hi @MarkJYC001, shameless plug: if you are interested in a specific Lean version, I maintain a fork of the REPL that backports support for each Lean version from v4.7.0-rc1 to v4.22.0-rc4 (repo). It also includes Lean v4.20.0 (which was a bit tricky to get at the time ^^'). All versions are tested against the same set of tests.
Also, you can check out LeanInteract (code, doc) which builds on top of it with a Python interface and extra features ;)