How to reproduce ReProver training offline?

[laetitia-teo]

I'm on a cluster on which the nodes are not directly connected to the internet. I'm trying to run the following command, from the ReProver section:

(ReProver) bash-4.4$ python generator/main.py fit --config generator/confs/cli_lean3_random.yaml

But when importing the leandojo module, the latter tries to access github (LEAN4_REPO = GITHUB.get_repo("leanprover/lean4"), line 76 of src/leandojo/constants/py); which fails with an error on my nodes. Any guidance on how to run this offline?

[yangky11]

LeanDojo may support it after lean-dojo/LeanDojo#179 is merged.