How to reproduce ReProver training offline? #41
Unanswered
laetitia-teo
asked this question in
Q&A
Replies: 0 comments
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
-
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:
But when importing the leandojo module, the latter tries to access github (
LEAN4_REPO = GITHUB.get_repo("leanprover/lean4")
, line 76 ofsrc/leandojo/constants/py
); which fails with an error on my nodes. Any guidance on how to run this offline?Beta Was this translation helpful? Give feedback.
All reactions