How to use a local Lean project?

[TitiSkywalker]

Hello! I have a customized local Lean project. I followed the README instructions:

project = LocalProject(
    directory="/path/to/my/project/", auto_build=False
)
config = LeanREPLConfig(project=project)

For REPL to work, I included it in my project's lakefile.toml

[[require]]
name = "REPL"
git = "https://github.com/leanprover-community/repl"

I already executed lake update successfully, so I turned off auto_build. However, the LeanREPLConfig line triggers the following error:

ValueError: An error occurred while preparing the Lean REPL. The requested Lean version `v4.28.0-rc1` does not match the fetched Lean version in the repository `v4.8.0-rc1`.Please open an issue on GitHub if you think this is a bug.

Is there a way to change the v4.8.0-rc1 setting? My local project is using Lean 4.28.0-rc1. 😺

[nihaljn]

I looked around and it was difficult to figure out how to get it to use the correct repl version through git/cache on its own.

What worked finally for me was:

1. Manually clone repl and checkout the version you're looking for. For you it would be:

git clone https://github.com/leanprover-community/repl # clones at ./repl
git checkout tags/v4.28.0-rc1

2. Initialize config as

config = LeanREPLConfig(project=project, local_repl_path="./repl")

[augustepoiroux]

Hello! This is curious indeed. In general, if LeanInteract falls back to v4.8.0-rc1 it is because it has failed to find the Lean version in the project. Would you be able to share more about your local setup so that I can debug this issue more properly?
Also, there is no need to add REPL in your project's lakefile, LeanInteract downloads it automatically on the side. Here, the issue seems to be that it didn't detect the right Lean version.
Maybe a guess: are you using the latest LeanInteract python package? If the version you use is relatively old, then it will not be able to use more recent Lean versions. Because of the way LeanInteract works, updating the python package version is always necessary to use the latest Lean versions. You can check in the release notes if the LeanInteract version you use includes the Lean version you want.
Thanks @nihaljn, this is a good workaround, although some features like incremental and parallel processing will be missing when using the official REPL.