LeanDojo plugin is unable to fetch the theorem from the provided Lean4 GitHub repo URL within ChatGPT

Deep0Thinking commented 1 year ago

Description

LeanDojo plugin is unable to fetch the theorem from the provided Lean4 GitHub repo URL within ChatGPT.

Detailed Steps to Reproduce the Behavior

Logs in Debug Mode

louisliu@Louiss-MacBook-Pro LeanDojoChatGPT-main % python3.10 main.py --port 23456 --url https://github.com/yangky11/lean4-example --commit 7d711f6da4584ecb7d4f057715e1f72ba175c910
2023-07-17 12:03:45.063 | INFO     | __main__:main:104 - Namespace(url='https://github.com/yangky11/lean4-example', commit='7d711f6da4584ecb7d4f057715e1f72ba175c910', port=23456)
 * Serving Quart app 'main'
 * Environment: production
 * Please use an ASGI server (e.g. Hypercorn) directly in production
 * Debug mode: True
 * Running on http://localhost:23456 (CTRL + C to quit)
[2023-07-17 12:03:45 +0700] [3665] [INFO] Running on http://127.0.0.1:23456 (CTRL + C to quit)
[2023-07-17 12:06:04 +0700] [3665] [INFO] 127.0.0.1:54461 OPTIONS /logo.jpg 1.1 200 0 9552
[2023-07-17 12:06:14 +0700] [3665] [INFO] 127.0.0.1:54464 OPTIONS /initialize_proof_search 1.1 200 0 3806
2023-07-17 12:06:15.417 | WARNING  | lean_dojo.interaction.dojo:__post_init__:171 - Using Lean 4 without a hard timeout may lead to problems if a tactic hangs indefinitely.
[2023-07-17 12:06:17,388] ERROR in app: Exception on request POST /initialize_proof_search
Traceback (most recent call last):
  File "/opt/homebrew/lib/python3.10/site-packages/lean_dojo/interaction/dojo.py", line 224, in __enter__
    traced_file = TracedFile.from_traced_file(
  File "/opt/homebrew/lib/python3.10/site-packages/lean_dojo/data_extraction/traced_data.py", line 595, in from_traced_file
    raise FileNotFoundError(f"{json_path} does not exist")
FileNotFoundError: /Users/louisliu/.cache/lean_dojo/yangky11-lean4-example-7d711f6da4584ecb7d4f057715e1f72ba175c910/lean4-example/build/ir/https:/github.com/yangky11/lean4-example/blob/main/Lean4Example.ast.json does not exist

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
  File "/opt/homebrew/lib/python3.10/site-packages/quart/app.py", line 1650, in handle_request
    return await self.full_dispatch_request(request_context)
  File "/opt/homebrew/lib/python3.10/site-packages/quart/app.py", line 1675, in full_dispatch_request
    result = await self.handle_user_exception(error)
  File "/opt/homebrew/lib/python3.10/site-packages/quart/app.py", line 1107, in handle_user_exception
    raise error
  File "/opt/homebrew/lib/python3.10/site-packages/quart/app.py", line 1673, in full_dispatch_request
    result = await self.dispatch_request(request_context)
  File "/opt/homebrew/lib/python3.10/site-packages/quart/app.py", line 1718, in dispatch_request
    return await self.ensure_async(handler)(**request_.view_args)
  File "/Users/louisliu/Downloads/LeanDojoChatGPT-main/main.py", line 29, in initialize_proof_search
    (dojo, s) = Dojo(theorem).__enter__()
  File "/opt/homebrew/lib/python3.10/site-packages/lean_dojo/interaction/dojo.py", line 302, in __enter__
    raise ex
  File "/opt/homebrew/lib/python3.10/site-packages/lean_dojo/interaction/dojo.py", line 228, in __enter__
    raise DojoInitError(f"Cannot find the file {json_path}")
lean_dojo.interaction.dojo.DojoInitError: Cannot find the file build/ir/https:/github.com/yangky11/lean4-example/blob/main/Lean4Example.ast.json
Executing <Task pending name='Task-29' coro=<ASGIHTTPConnection.handle_request() running at /opt/homebrew/lib/python3.10/site-packages/quart/asgi.py:102> wait_for=<Future pending cb=[Task.task_wakeup()] created at /opt/homebrew/Cellar/python@3.10/3.10.12_1/Frameworks/Python.framework/Versions/3.10/lib/python3.10/asyncio/base_events.py:429> cb=[_wait.<locals>._on_completion() at /opt/homebrew/Cellar/python@3.10/3.10.12_1/Frameworks/Python.framework/Versions/3.10/lib/python3.10/asyncio/tasks.py:475] created at /opt/homebrew/Cellar/python@3.10/3.10.12_1/Frameworks/Python.framework/Versions/3.10/lib/python3.10/asyncio/tasks.py:636> took 2.524 seconds
[2023-07-17 12:06:17 +0700] [3665] [INFO] 127.0.0.1:54464 POST /initialize_proof_search 1.1 500 66207 2527585

Screenshots

Platform Information

macOS Ventura 13.4
Chrome
LeanDojo v1.1.2

yangky11 commented 1 year ago

Hi,

I wasn't able to reproduce this error, but it looks like ChatGPT was using incorrect "theorem_file_path" parameter. It should be just the file name, without the URL. Maybe removing the URL from the prompt would help: https://github.com/lean-dojo/LeanDojoChatGPT/commit/cb6798bb1f71003aa5fe7acc0147709cfec54729

Deep0Thinking commented 1 year ago

Hi,

I wasn't able to reproduce this error, but it looks like ChatGPT was using incorrect "theorem_file_path" parameter. It should be just the file name, without the URL. Maybe removing the URL from the prompt would help: cb6798b

Removed the URL from "theorem_file_path" as suggested and it solved the issue (ChatGPT conversation history). Thanks for the quick help!

lean-dojo / LeanDojoChatGPT