Lean Dojo files failing

Stream: general

[Frederick Pu]

When I try to run the lean dojo demo

from lean_dojo import LeanGitRepo, trace

repo = LeanGitRepo("https://github.com/yangky11/lean4-example", "7b6ecb9ad4829e4e73600a3329baeb3b5df8d23f")
trace(repo, dst_dir="traced_lean4-example")

i get the following error message

Traceback (most recent call last):
  File "C:\Users\pufre\Downloads\CodingProjects\AlphaProof\test.py", line 1, in <module>
    from lean_dojo import LeanGitRepo, trace
  File "C:\Users\pufre\.pyenv\pyenv-win\versions\3.9.0\lib\site-packages\lean_dojo\__init__.py", line 3, in <module>
    from .data_extraction.trace import (
  File "C:\Users\pufre\.pyenv\pyenv-win\versions\3.9.0\lib\site-packages\lean_dojo\data_extraction\trace.py", line 20, in <module>
    from .lean import LeanGitRepo
  File "C:\Users\pufre\.pyenv\pyenv-win\versions\3.9.0\lib\site-packages\lean_dojo\data_extraction\lean.py", line 19, in <module>
    from github import Github, Auth
  File "C:\Users\pufre\.pyenv\pyenv-win\versions\3.9.0\lib\site-packages\github\__init__.py", line 53, in <module>
    from . import Auth
  File "C:\Users\pufre\.pyenv\pyenv-win\versions\3.9.0\lib\site-packages\github\Auth.py", line 36, in <module>
    import jwt
  File "C:\Users\pufre\.pyenv\pyenv-win\versions\3.9.0\lib\site-packages\jwt\__init__.py", line 1, in <module>
    from .api_jwk import PyJWK, PyJWKSet
  File "C:\Users\pufre\.pyenv\pyenv-win\versions\3.9.0\lib\site-packages\jwt\api_jwk.py", line 7, in <module>
    from .algorithms import get_default_algorithms, has_crypto, requires_cryptography
  File "C:\Users\pufre\.pyenv\pyenv-win\versions\3.9.0\lib\site-packages\jwt\algorithms.py", line 11, in <module>
    from .utils import (
  File "C:\Users\pufre\.pyenv\pyenv-win\versions\3.9.0\lib\site-packages\jwt\utils.py", line 7, in <module>
    from cryptography.hazmat.primitives.asymmetric.ec import EllipticCurve
  File "C:\Users\pufre\.pyenv\pyenv-win\versions\3.9.0\lib\site-packages\cryptography\hazmat\primitives\asymmetric\ec.py", line 11, in <module>
    from cryptography.exceptions import UnsupportedAlgorithm, _Reasons
  File "C:\Users\pufre\.pyenv\pyenv-win\versions\3.9.0\lib\site-packages\cryptography\exceptions.py", line 9, in <module>
    from cryptography.hazmat.bindings._rust import exceptions as rust_exceptions
ImportError: DLL load failed while importing _rust: The specified procedure could not be found.

[Yakov Pechersky]

Your windows Python install is likely faulty, according to GitHub issues on the cryptography repo

[Yakov Pechersky]

Try upgrading to a more recent python, even a more recent 3.9

[Frederick Pu]

when i use python 3.12:

pip install lean-dojo
ERROR: Ignored the following versions that require a different python version: 1.0.0 Requires-Python <3.11,>=3.9; 1.1.0 Requires-Python <3.11,>=3.9; 1.1.1 Requires-Python <3.11,>=3.9; 1.1.2 Requires-Python <3.11,>=3.9; 1.2.0 Requires-Python <3.11,>=3.9; 1.2.1 Requires-Python <=3.11,>=3.9; 1.2.2 Requires-Python <=3.11,>=3.9; 1.2.3 Requires-Python <3.11,>=3.9; 1.2.4 Requires-Python <3.11,>=3.9; 1.2.5 Requires-Python <3.11,>=3.9; 1.2.6 Requires-Python <3.11,>=3.9; 1.3.0 Requires-Python <3.11,>=3.9; 1.4.0 Requires-Python <3.11,>=3.9; 1.4.1 Requires-Python <3.11,>=3.9; 1.4.2 Requires-Python <3.11,>=3.9; 1.4.3 Requires-Python <3.11,>=3.9; 1.4.4 Requires-Python <3.11,>=3.9; 1.4.5 Requires-Python <3.11,>=3.9; 1.5.0 Requires-Python <3.11,>=3.9; 1.5.1 Requires-Python <3.11,>=3.9; 1.6.0 Requires-Python <3.11,>=3.9; 1.7.0 Requires-Python <3.11,>=3.9; 1.7.1 Requires-Python <3.11,>=3.9; 1.8.0 Requires-Python <3.12,>=3.9; 1.8.1 Requires-Python <3.12,>=3.9; 1.8.2 Requires-Python <3.12,>=3.9; 1.9.0 Requires-Python <3.12,>=3.9; 2.0.0 Requires-Python <3.12,>=3.9; 2.0.1 Requires-Python <3.12,>=3.9; 2.0.2 Requires-Python <3.12,>=3.9; 2.0.3 Requires-Python <3.12,>=3.9; 2.1.0 Requires-Python <3.12,>=3.9; 2.1.1 Requires-Python <3.12,>=3.9; 2.1.2 Requires-Python <3.12,>=3.9; 2.1.3 Requires-Python <3.12,>=3.9
ERROR: Could not find a version that satisfies the requirement lean-dojo (from versions: none)
ERROR: No matching distribution found for lean-dojo

[Frederick Pu]

I managed to get it working by installing python 11. But now i get a different error message:

Traceback (most recent call last):
  File "<string>", line 1, in <module>
  File "C:\Users\pufre\AppData\Local\Programs\Python\Python311\Lib\multiprocessing\spawn.py", line 122, in spawn_main
    exitcode = _main(fd, parent_sentinel)
               ^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "C:\Users\pufre\AppData\Local\Programs\Python\Python311\Lib\multiprocessing\spawn.py", line 131, in _main
    prepare(preparation_data)
  File "C:\Users\pufre\AppData\Local\Programs\Python\Python311\Lib\multiprocessing\spawn.py", line 246, in prepare
    _fixup_main_from_path(data['init_main_from_path'])
  File "C:\Users\pufre\AppData\Local\Programs\Python\Python311\Lib\multiprocessing\spawn.py", line 297, in _fixup_main_from_path
    main_content = runpy.run_path(main_path,
                   ^^^^^^^^^^^^^^^^^^^^^^^^^
  File "<frozen runpy>", line 291, in run_path
  File "<frozen runpy>", line 98, in _run_module_code
  File "<frozen runpy>", line 88, in _run_code
  File "C:\Users\pufre\Downloads\CodingProjects\AlphaProof\test.py", line 4, in <module>
    trace(repo, dst_dir="traced_lean4-example")
  File "C:\Users\pufre\AppData\Local\Programs\Python\Python311\Lib\site-packages\lean_dojo\data_extraction\trace.py", line 247, in trace
    cached_path = get_traced_repo_path(repo, build_deps)
                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "C:\Users\pufre\AppData\Local\Programs\Python\Python311\Lib\site-packages\lean_dojo\data_extraction\trace.py", line 213, in get_traced_repo_path
    _trace(repo, build_deps)
  File "C:\Users\pufre\AppData\Local\Programs\Python\Python311\Lib\site-packages\lean_dojo\data_extraction\trace.py", line 157, in _trace
    with launch_progressbar(dirs_to_monitor):
  File "C:\Users\pufre\AppData\Local\Programs\Python\Python311\Lib\contextlib.py", line 137, in __enter__
    return next(self.gen)
           ^^^^^^^^^^^^^^
  File "C:\Users\pufre\AppData\Local\Programs\Python\Python311\Lib\site-packages\lean_dojo\data_extraction\trace.py", line 65, in launch_progressbar
    p.start()
  File "C:\Users\pufre\AppData\Local\Programs\Python\Python311\Lib\multiprocessing\process.py", line 121, in start
    self._popen = self._Popen(self)
                  ^^^^^^^^^^^^^^^^^
  File "C:\Users\pufre\AppData\Local\Programs\Python\Python311\Lib\multiprocessing\context.py", line 224, in _Popen
    return _default_context.get_context().Process._Popen(process_obj)
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "C:\Users\pufre\AppData\Local\Programs\Python\Python311\Lib\multiprocessing\context.py", line 336, in _Popen
    return Popen(process_obj)
           ^^^^^^^^^^^^^^^^^^
  File "C:\Users\pufre\AppData\Local\Programs\Python\Python311\Lib\multiprocessing\popen_spawn_win32.py", line 46, in __init__
    prep_data = spawn.get_preparation_data(process_obj._name)
                ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "C:\Users\pufre\AppData\Local\Programs\Python\Python311\Lib\multiprocessing\spawn.py", line 164, in get_preparation_data
    _check_not_importing_main()
  File "C:\Users\pufre\AppData\Local\Programs\Python\Python311\Lib\multiprocessing\spawn.py", line 140, in _check_not_importing_main
    raise RuntimeError('''
RuntimeError:
        An attempt has been made to start a new process before the
        current process has finished its bootstrapping phase.

        This probably means that you are not using fork to start your
        child processes and you have forgotten to use the proper idiom
        in the main module:

            if __name__ == '__main__':
                freeze_support()
                ...

        The "freeze_support()" line can be omitted if the program
        is not going to be frozen to produce an executable.

        To fix this issue, refer to the "Safe importing of main module"
        section in https://docs.python.org/3/library/multiprocessing.html