Large scale verification with latest lean version (v4.24)

Stream: Machine Learning for Theorem Proving

[Ayush Agrawal]

It seems that lean repl does not work with the latest lean version. I tried tools for verifying large scale lean code such as kimina-lean-server and LeanInteract (https://github.com/augustepoiroux/LeanInteract/tree/main). However, none of these work properly with the latest lean version. Are there tools/ways I am missing to do the same?

[Kim Morrison]

What do you mean? The REPL tests all succeed in the v4.24.0 tag of the REPL repository. You'll have to show us what you expect to work differently.

[Ayush Agrawal]

I see, I think I might have missed updating to the latest version tag. Checking and will get back. Thanks for the help.

[Ayush Agrawal]

@Kim Morrison thanks. I think there were issues in the repl build. It works perfectly fine now. Sorry for the confusion.