search

lean-dojo / LeanDojo

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

demo-lean4: Dojo() does not recognize traced repo #165

Closed jganten closed 4 months ago

jganten commented 4 months ago

Description

In the demo-lean4 Jupyter notebook, the code fails to execute starting from the "Interacting with Lean" section. Specifically, the line:

dojo, state_0 = Dojo(theorem).__enter__()

produces the following output:

2024-05-20 18:59:51.881 | WARNING  | lean_dojo.interaction.dojo:__init__:162 - Using Lean 4 without a hard timeout may hang indefinitely.
2024-05-20 18:59:51.884 | INFO     | lean_dojo.data_extraction.cache:get:77 - Downloading the traced repo from the remote cache. Set the environment variable `DISABLE_REMOTE_CACHE` if you want to trace the repo locally.
../traced_repros/leanprover-community-mathlib4-fe4454af900584467d21f4fd4fe951d29d9332a7.tar.gz: Datei oder Verzeichnis nicht gefunden
[error messages because it fails to download the traced repo]

Detailed Steps to Reproduce the Behavior

  1. Manually download the leanprover-community-mathlib4-fe4454af900584467d21f4fd4fe951d29d9332a7.tar.gz file and unpack it into a directory. In my case, I unpacked it into ../traced_repros/. Note: There was a consistent typo in my folder name.
  2. Configure the .env file with my GitHub access token and enable verbose logging. Set the cache directory to ../traced_repros.
  3. Execute the Jupyter notebook until it fails at the mentioned line.

Expected Behavior

The line dojo, state_0 = Dojo(theorem).__enter__() should execute without errors, allowing interaction with Lean. Note that 'trace()' previously correctly recognized the existing traced file in the 'traced_repros' folder.

Actual Behavior

The execution fails with the following error message indicating that the required file or directory is not found:

../traced_repros/leanprover-community-mathlib4-fe4454af900584467d21f4fd4fe951d29d9332a7.tar.gz: Datei oder Verzeichnis nicht gefunden

Logs in Debug Mode

No significant logs were produced before the failure (at least to my knowledge).

Platform Information

Thanks for the help!

yangky11 commented 4 months ago

I'll be able to take a look around this weekend.

yangky11 commented 4 months ago

This bug has been fixed in the latest version (v1.9.0), which will be released in a few minutes.

yangky11 commented 4 months ago

Feel free to re-open this issue if the error still persists.