Using LeanDojo in Google Colab

[ZIYU-DEEP]

I am attempting to use the package in colab notebook but facing some minor issues.

Setup steps:

## Preparation
import os

os.environ['CONTAINER'] = 'native'
os.environ['VERBOSE'] = '1'
os.environ['GITHUB_ACCESS_TOKEN'] = input()

## elan and lean installation
# Download the binary
!wget https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz

# Extract the content
!tar -xzf elan-x86_64-unknown-linux-gnu.tar.gz

# Move the the local bin directory
!mv elan-init /usr/local/bin/elan

# Verify the downloaded elan
!/usr/local/bin/elan --version

# Download Lean
!/usr/local/bin/elan default stable

# Check the lean version
!elan which lean

# Add the above path to the environment
lean_bin_path = '/root/.elan/toolchains/stable/bin'
os.environ['PATH'] += ':' + lean_bin_path

# Check the lean version
!lean --version

## Test LeanDojo
!pip install lean-dojo

Initial issue: running as the root

from lean_dojo import *

This will trigger an error due to __init__.py raising an exception for running as root. It seems to be a bit cumbersome to run as a non-root user in colab, so i just comment out the error-raising lines in order to proceed. What would be some better practices to handle this issue?

Subsequent issue: tracing repository stalls

repo = LeanGitRepo(
    'https://github.com/yangky11/lean4-example', 
    '3f8c5eb303a225cdef609498b8d87262e5ef344b'  # Using the Lean version 4.7.0
    )

trace(repo, dst_dir='traced_lean4-example')

Below are the logs:

2024-04-10 23:23:06.240 | INFO     | lean_dojo.data_extraction.trace:get_traced_repo_path:79 - Tracing LeanGitRepo(url='https://github.com/yangky11/lean4-example', commit='3f8c5eb303a225cdef609498b8d87262e5ef344b')
2024-04-10 23:23:06.243 | DEBUG    | lean_dojo.data_extraction.trace:get_traced_repo_path:81 - Working in the temporary directory /tmp/tmpak727a5s
2024-04-10 23:23:06.246 | DEBUG    | lean_dojo.data_extraction.lean:clone_and_checkout:475 - Cloning LeanGitRepo(url='https://github.com/yangky11/lean4-example', commit='3f8c5eb303a225cdef609498b8d87262e5ef344b')
2024-04-10 23:23:06.626 | DEBUG    | lean_dojo.data_extraction.trace:_trace:33 - Tracing LeanGitRepo(url='https://github.com/yangky11/lean4-example', commit='3f8c5eb303a225cdef609498b8d87262e5ef344b')
2024-04-10 23:23:06.637 | DEBUG    | lean_dojo.container:run:184 - NUM_PROCS=2 python build_lean4_repo.py lean4-example

And it looks like the process gets stuck at NUM_PROCS=2 python build_lean4_repo.py lean4-example. I am wondering what are some suggestions to help diagnose the issue. Many thanks.

[yangky11]

so i just comment out the error-raising lines in order to proceed.

I haven't used Colab a lot before. How to edit a source file on Colab?

[ZIYU-DEEP]

Hi Kaiyu – directly clicking the filename (/usr/local/lib/python3.10/dist-packages/lean_dojo/__init__.py) in the error message should open it as a editable file in the right side pane; or using the files tab on the left sidebar to navigate to the file.

[yangky11]

It looks like Colab cannot find elan, lake, etc. I got an error when running

os.system("lake --help")

@ZIYU-DEEP Do you have the same issue?

[ZIYU-DEEP]

Hi Kaiyu, it looks to be working in my case.

os.system('lake --help')

>>> 0

To check the output:

import subprocess
result = subprocess.run(['lake', '--help'], stdout=subprocess.PIPE, text=True)
print(result.stdout)

or:

!lake --help

Both can give:

>>> Lake version 5.0.0-6fce8f7 (Lean version 4.7.0)
>>>
>>> USAGE:
>>>   lake [OPTIONS] <COMMAND>
>>>
>>> COMMANDS:
>>>   new <name> <temp>     create a Lean package in a new directory
>>>   init <name> <temp>    create a Lean package in the current directory
>>>   build <targets>...    build targets
>>>   exe <exe> <args>...   build an exe and run it in Lake's environment
>>>   clean                 remove build outputs
>>>   env <cmd> <args>...   execute a command in Lake's environment
>>>   update                update dependencies and save them to the manifest
>>>   upload <tag>          upload build artifacts to a GitHub release
>>>   script                manage and run workspace scripts
>>>   scripts               shorthand for `lake script list`
>>>   run <script>          shorthand for `lake script run`
>>>   serve                 start the Lean language server
>>>
>>> OPTIONS:
>>>   --version             print version and exit
>>>   --help, -h            print help of the program or a command and exit
>>>   --dir, -d=file        use the package configuration in a specific directory
>>>   --file, -f=file       use a specific file for the package configuration
>>>   --quiet, -q           hide progress messages
>>>   --verbose, -v         show verbose information (command invocations)
>>>   --lean=cmd            specify the `lean` command used by Lake
>>>   -K key[=value]        set the configuration file option named key
>>>   --old                 only rebuild modified modules (ignore transitive deps)
>>>   --rehash, -H          hash all files for traces (do not trust `.hash` files)
>>>   --update, -U          update manifest before building
>>>   --reconfigure, -R     elaborate configuration files instead of using OLeans
>>>
>>> See `lake help <command>` for more information on a specific command.

@yangky11 Here is the colab link: .

[ZIYU-DEEP]

@yangky11 the environment works! here is a colab version of demo-lean4.ipynb.