Request for retrievers trained on both random and novel_premises splits

[JobPetrovcic]

The README explains how to train separate retrievers on the random and novel_premises splits of LeanDojo Benchmark 4. On Hugging Face, however, there appears to be only one published retriever checkpoint: kaiyuy/leandojo-lean4-retriever-byt5-small.

Could you please clarify which split this checkpoint was trained on? Additionally, would it be possible to release the retriever trained on the other split as well? I’d like to test both in my experiments and avoid having to retrain.