search

lean-dojo / LeanDojo

Tool for data extraction and interacting with Lean programmatically.
https://leandojo.org
MIT License
536 stars 80 forks source link

ImportError: cannot import name 'TacticError' from 'lean_dojo' #49

Closed sangjun7 closed 1 year ago

sangjun7 commented 1 year ago

Description Hello, I tried to evaluate your prover model without retrieval. But I got the following error for 'TacticError':

/usr/lib/python3/dist-packages/requests/init.py:89: RequestsDependencyWarning: urllib3 (1.26.16) or chardet (3.0.4) doesn't match a supported version! warnings.warn("urllib3 ({}) or chardet ({}) doesn't match a supported " [2023-08-28 02:07:30,563] [INFO] [real_accelerator.py:158:get_accelerator] Setting ds_accelerator to cuda (auto detect) Traceback (most recent call last): File "/app/lean-dojo/ReProver/evaluate.py", line 15, in from prover.proof_search import Status, DistributedProver File "/app/lean-dojo/ReProver/prover/proof_search.py", line 9, in from lean_dojo import ( ImportError: cannot import name 'TacticError' from 'lean_dojo' (/usr/lib/python3/dist-packages/lean_dojo/init.py)

When I checked the 'init.py' file, there was no 'TacticError'. Only 'LeanError' could be found: image

Detailed Steps to Reproduce the Behavior

  1. I built docker image for remote server. In docker, I installed python 3.10.12, pytorch 1.13.1 and required packages for lean-dojo based on ubuntu 20.04.
  2. Then installed lean-dojo by pip install lean-dojo.
  3. I ran the evaluate code in remote server by python lean-dojo/ReProver/evaluate.py --data-path /app/input/dataset/leandojo-dataset/random/ --split test --ckpt_path /app/input/dataset/leandojo-model-origin/generator_random.ckpt --num-sampled-tactics 64 --timeout 600 --num-cpus 32 --with-gpus

Logs in Debug Mode

/usr/lib/python3/dist-packages/requests/init.py:89: RequestsDependencyWarning: urllib3 (1.26.16) or chardet (3.0.4) doesn't match a supported version! warnings.warn("urllib3 ({}) or chardet ({}) doesn't match a supported " [2023-08-28 02:29:12,210] [INFO] [real_accelerator.py:158:get_accelerator] Setting ds_accelerator to cuda (auto detect) Traceback (most recent call last): File "/app/lean-dojo/ReProver/evaluate.py", line 15, in from prover.proof_search import Status, DistributedProver File "/app/lean-dojo/ReProver/prover/proof_search.py", line 9, in from lean_dojo import ( ImportError: cannot import name 'TacticError' from 'lean_dojo' (/usr/lib/python3/dist-packages/lean_dojo/init.py)

Platform Information

yangky11 commented 1 year ago

TacticError was renamed to LeanError. Just fixed: https://github.com/lean-dojo/ReProver/commit/acc6fd3e9a4f474d62e2285030d9fb9c0bc77770. Thanks.