ZIYU-DEEP
commented
8 months ago Hi Kaiyu, it seems the latest version of LeanDojo-1.7.1 is not compatible with the miniF2F-Lean4 repository. I have created a new branch and put the error messages in the README.md for your review.
Below is a minimal script (debug.py) to reproduce the issue.
import json
from lean_dojo import *
# Helper Function
def load_data_dojo(dataset_name: str='minif2f',
dataset_path: str='./data/minif2f_lean4_dojo.jsonl',
split: str='valid'):
"""
Load the data and the repo to LeanGitRepo.
"""
if 'minif2f' in dataset_name:
data = []
with open(dataset_path) as f:
for line in f.readlines():
data_ = json.loads(line)
data.append(data_)
if 'valid' in split.lower():
data = [x for x in data if x['split'] != 'test']
else:
data = [x for x in data if x['split'] == 'test']
repo = LeanGitRepo(data[0]['url'], data[0]['commit'])
else:
raise NotImplementedError(split)
return repo, data
# Set the repo
repo, data = load_data_dojo(dataset_path='./data/minif2f_lean4_dojo.jsonl',
split='valid')
# Check the error message
for example in data:
# Set up the data
file_path = example['file_path']
theorem_name = example.get('full_name', example.get('id'))
theorem = Theorem(repo, file_path, theorem_name)
# Set the environment
with Dojo(theorem, hard_timeout=600) as (dojo, init_state):
breakpoint()Here, the ./data/minif2f_lean4_dojo.jsonl is adapted from the original file the latest URL and commit entries to match the miniF2F-lean4 repository. The error messages will be about missing files of .ast.json and .dep_paths for ProofWidgets, and denied permission for /tmp/ray/.../node_ip_address.json.lock. I plan to revisit this issue after the SMT integration (will create a new pull). Meanwhile, it would be awesome if you could help look into this!
Thank you!
yangky11
Hi,
I noticed that LeanDojo is pinned to an early version. https://github.com/ZIYU-DEEP/bilevel-reasoner/blob/885166b8fab4d88da914bece06307c0c50aea159/requirements.txt#L8
That may cause issues because Lean 4 frequently breaks backward compatibility, and LeanDojo is constantly updated to keep up with those changes. I'd suggest upgrading to the latest version.