Which specific Lean version will leandojo use?

[wclsn]

Hello, everyone
I am curious about the specific lean version that Dojo will utilize when I use it to interact with Lean, such as running run_tac(). I have multiple toolchains installed on my computer, and I would like to know which particular lean version Dojo will employ for these interactions, the default one?

[darabos]

I think you get to run_tac() from picking a theorem from a repo. That repo has a lean-toolchain file that specifies the Lean version. LeanDojo will use that version.