Is it possible to build a google colab for Lean Dojo?

[brando90]

Due to the docker requirements and Lean, I was wondering if it is at all possible to build Lean Dojo in a Google Colab?

[yangky11]

The Docker requirement is primarily for Lean 3. I plan to drop it for Lean 4 but haven't got the capacity to do that yet. For Lean 4, you should feel free to set CONTAINER=native to run LeanDojo without Docker.

[yangky11]

Update: We have made "running w/o Docker" the default setting: #74. It should work out of the box for Lean 4. If you use LeanDojo with Lean 3, now you need to set the environment variable CONTAINER to docker.