search

lean-dojo / ReProver

Retrieval-Augmented Theorem Provers for Lean
https://leandojo.org
MIT License
195 stars 40 forks source link

Evaluating ReProver without training local checkpoints / Model checkpoints access #54

Open Yingjia-Wan opened 1 month ago

Yingjia-Wan commented 1 month ago

Hi! Thank you for the inspiring work. I am replicating the evaluation of LeanDojo ReProver and want to skip training from scratch as the repo instructions tell me. The evaluation.py does not seem to support this as it requires local checkpoints. Can we directly evaluate your model without training a local checkpoint?

As a potential solution, could you please upload the model checkpoint files to the huggingface repos of the three models?

(I randomly found this separate repo of leandojo checkpoints by the authors. However, it was not mentioned anywhere in the paper or repo. When I tried to use the checkpoints for evaluation, there was an incompatible checkpoint version name issue. )

yangky11 commented 1 month ago

Maybe these two posts are relevant?

https://github.com/lean-dojo/ReProver/discussions/51

https://github.com/lean-dojo/ReProver/discussions/53

Let me know if the error persists.

Yingjia-Wan commented 1 month ago

Thank you so much for the redirected links. I gained correct access to the model checkpoints by renaming the retriever folder based on [#53].

However, I am encountering another error below when running evaluate.py. I would appreciate your insight regarding any solution to this. Do I perhaps need to git clone and import the Lean4Repl repo?

subprocess.CalledProcessError: Command 'lake build Lean4Repl' returned non-zero exit status 127.
Yingjia-Wan commented 1 month ago

Thank you so much for the redirected links. I gained correct access to the model checkpoints by renaming the retriever folder based on [#53].

However, I am encountering another error below when running evaluate.py. I would appreciate your insight regarding any solution to this. Do I perhaps need to git clone and import the Lean4Repl repo?

subprocess.CalledProcessError: Command 'lake build Lean4Repl' returned non-zero exit status 127.

As this issue has not been addressed yet, here is some additional information about the error I encountered: 5751718158573_ pic

Here is the related code in the lean_dojo package that the ReProver's evaluate.py code imports, where it requires running lake build Lean4Repl: 5731718158456_ pic

I would really appreciate any guidance on fixing this issue and getting the evaluate code running. For example, do I need to clone and set up Lean4Repl in a specific directory? Or is there an alternative?

yangky11 commented 1 month ago

Hi, I'll be able to take a look next week.

yangky11 commented 1 month ago

I'm trying to reproduce the error but found that the current convert_zero_checkpoint_to_fp32_state_dict can no longer load previously saved checkpoints (probably due to a breaking change in the checkpoint format). I'm trying to re-train the models and save them in the new checkpoint format.

Meanwhile, I think the problem you encountered is related to LeanDojo rather than the model. It would be really helpful if you can come up with a minimal Python script for reproducing the error, similar to the testing examples in https://github.com/lean-dojo/LeanDojo/blob/main/tests/interaction/test_tactics.py.

Yingjia-Wan commented 2 weeks ago

Thank you for the reply! I wrote a test Python script based on your examples and following the LeanDojo documentation as the following. However, it renders an assertion error.

I tried testing the script in either the ReProver or lean4-example project (after lake update lake build). But the error persists. In fact, I got returned the assertion error even by simply tracing the lean4-example repo.

Could you help speculate the issue and the error? I would appreciate any form of feedback about what I did wrong.

Trace:

from lean_dojo import LeanGitRepo, trace

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

test_tactics_dojo.py

import os
import requests
from lean_dojo import *

repo = LeanGitRepo("https://github.com/yangky11/lean4-example", '7b6ecb9ad4829e4e73600a3329baeb3b5df8d23f' )
theorem = Theorem(repo, "Lean4Example.lean", "hello_world")

with Dojo(theorem) as (dojo, init_state):
    print(init_state)
    result = dojo.run_tac(init_state, "rw [add_assoc, add_comm b, -add_assoc]")
    assert isinstance(result, ProofFinished)
    print(result)

Error:

(ReProver) yingjiawan@skcpu3:~/alisa/lean4-example$ python test_tactics_dojo3.py 
Rate limit remaining: 4997
2024-07-11 11:56:06.448 | WARNING  | lean_dojo.interaction.dojo:__init__:162 - Using Lean 4 without a hard timeout may hang indefinitely.
2024-07-11 11:56:07.089 | INFO     | lean_dojo.data_extraction.trace:get_traced_repo_path:79 - Tracing LeanGitRepo(url='https://github.com/yangky11/lean4-example', commit='7b6ecb9ad4829e4e73600a3329baeb3b5df8d23f')
2024-07-11 11:56:08.816 | INFO     | __main__:main:165 - Building lean4-example
Build completed successfully.
2024-07-11 11:56:10.349 | INFO     | __main__:main:188 - Tracing lean4-example
2024-07-11 11:56:10.361 | DEBUG    | __main__:main:193 - lake env lean --threads 32 --run ExtractData.lean
100%|█████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████▍| 904/907 [02:25<00:00,  3.52it/s]2024-07-11 11:58:40.264 | WARNING  | __main__:check_files:132 - Missing /tmp/tmpfh65qy2n/workspace/lean4-example/.lake/build/ir/Lean4Example.dep_paths
2024-07-11 11:58:40.264 | WARNING  | __main__:check_files:132 - Missing /tmp/tmpfh65qy2n/workspace/lean4-example/.lake/build/ir/Lean4Example.ast.json
2024-07-11 11:58:42,544 INFO worker.py:1740 -- Started a local Ray instance. View the dashboard at 127.0.0.1:8266 
  0%|                                                                                                                                                                        | 0/906 [00:02<?, ?it/s]
Traceback (most recent call last):
  File "/home/yingjiawan/alisa/lean4-example/test_tactics_dojo3.py", line 35, in <module>
    with Dojo(theorem) as (dojo, init_state):
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/interaction/dojo.py", line 265, in __enter__
    raise ex
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/interaction/dojo.py", line 185, in __enter__
    traced_repo_path = get_traced_repo_path(self.repo)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/trace.py", line 83, in get_traced_repo_path
    traced_repo = TracedRepo.from_traced_files(tmp_dir / repo.name, build_deps)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/traced_data.py", line 1099, in from_traced_files
    traced_files = list(
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/tqdm/std.py", line 1181, in __iter__
    for obj in iterable:
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/ray/util/actor_pool.py", line 170, in get_generator
    yield self.get_next_unordered()
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/ray/util/actor_pool.py", line 370, in get_next_unordered
    return ray.get(future)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/ray/_private/auto_init_hook.py", line 21, in auto_init_wrapper
    return fn(*args, **kwargs)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/ray/_private/client_mode_hook.py", line 103, in wrapper
    return func(*args, **kwargs)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/ray/_private/worker.py", line 2623, in get
    values, debugger_breakpoint = worker.get_objects(object_refs, timeout=timeout)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/ray/_private/worker.py", line 861, in get_objects
    raise value.as_instanceof_cause()
ray.exceptions.RayTaskError(AssertionError): ray::_TracedRepoHelper.parse_traced_file() (pid=1261620, ip=143.89.191.27, actor_id=d34a75ce57ca90348413713d01000000, repr=<lean_dojo.data_extraction.traced_data._TracedRepoHelper object at 0x7ff15c27f580>)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/traced_data.py", line 965, in parse_traced_file
    return TracedFile.from_traced_file(self.root_dir, path, self.repo)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/traced_data.py", line 527, in from_traced_file
    return cls._from_lean4_traced_file(root_dir, json_path, repo)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/traced_data.py", line 547, in _from_lean4_traced_file
    ast = FileNode.from_data(data, lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 251, in from_data
    node = Node.from_data(node_data, lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 27, in from_data
    return subcls.from_data(node_data, lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 473, in from_data
    children = _parse_children(node_data, lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 265, in _parse_children
    node = Node.from_data(d["node"], lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 27, in from_data
    return subcls.from_data(node_data, lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 1492, in from_data
    children = _parse_children(node_data, lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 265, in _parse_children
    node = Node.from_data(d["node"], lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 27, in from_data
    return subcls.from_data(node_data, lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 1000, in from_data
    children = _parse_children(node_data, lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 265, in _parse_children
    node = Node.from_data(d["node"], lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 27, in from_data
    return subcls.from_data(node_data, lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 1492, in from_data
    children = _parse_children(node_data, lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 265, in _parse_children
    node = Node.from_data(d["node"], lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 27, in from_data
    return subcls.from_data(node_data, lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 1492, in from_data
    children = _parse_children(node_data, lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 265, in _parse_children
    node = Node.from_data(d["node"], lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 27, in from_data
    return subcls.from_data(node_data, lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 590, in from_data
    children = _parse_children(node_data, lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 265, in _parse_children
    node = Node.from_data(d["node"], lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 27, in from_data
    return subcls.from_data(node_data, lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 1492, in from_data
    children = _parse_children(node_data, lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 265, in _parse_children
    node = Node.from_data(d["node"], lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 27, in from_data
    return subcls.from_data(node_data, lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 1492, in from_data
    children = _parse_children(node_data, lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 265, in _parse_children
    node = Node.from_data(d["node"], lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 27, in from_data
    return subcls.from_data(node_data, lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 1492, in from_data
    children = _parse_children(node_data, lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 265, in _parse_children
    node = Node.from_data(d["node"], lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 27, in from_data
    return subcls.from_data(node_data, lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 590, in from_data
    children = _parse_children(node_data, lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 265, in _parse_children
    node = Node.from_data(d["node"], lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 27, in from_data
    return subcls.from_data(node_data, lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 1492, in from_data
    children = _parse_children(node_data, lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 265, in _parse_children
    node = Node.from_data(d["node"], lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 27, in from_data
    return subcls.from_data(node_data, lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 1492, in from_data
    children = _parse_children(node_data, lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 265, in _parse_children
    node = Node.from_data(d["node"], lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 27, in from_data
    return subcls.from_data(node_data, lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 1492, in from_data
    children = _parse_children(node_data, lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 265, in _parse_children
    node = Node.from_data(d["node"], lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 27, in from_data
    return subcls.from_data(node_data, lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 1492, in from_data
    children = _parse_children(node_data, lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 265, in _parse_children
    node = Node.from_data(d["node"], lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 27, in from_data
    return subcls.from_data(node_data, lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 1492, in from_data
    children = _parse_children(node_data, lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 265, in _parse_children
    node = Node.from_data(d["node"], lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 27, in from_data
    return subcls.from_data(node_data, lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 590, in from_data
    children = _parse_children(node_data, lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 265, in _parse_children
    node = Node.from_data(d["node"], lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 27, in from_data
    return subcls.from_data(node_data, lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 1492, in from_data
    children = _parse_children(node_data, lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 265, in _parse_children
    node = Node.from_data(d["node"], lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 27, in from_data
    return subcls.from_data(node_data, lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 590, in from_data
    children = _parse_children(node_data, lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 265, in _parse_children
    node = Node.from_data(d["node"], lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 27, in from_data
    return subcls.from_data(node_data, lean_file)
  File "/home/yingjiawan/anaconda3/envs/ReProver/lib/python3.10/site-packages/lean_dojo/data_extraction/ast.py", line 479, in from_data
    assert type(children[1]) in (
AssertionError
yangky11 commented 1 week ago

I tried on the latest LeanDojo v2.0.2 but didn't see the same error:

(ReProver) (base) kaiyuy@devfair0618:~/LeanDojo$ VERBOSE=1 ipython
Python 3.11.9 (main, Apr 19 2024, 16:48:06) [GCC 11.2.0]
Type 'copyright', 'credits' or 'license' for more information
IPython 8.25.0 -- An enhanced Interactive Python. Type '?' for help.

In [1]: from lean_dojo import LeanGitRepo, trace
   ...: 
   ...: repo = LeanGitRepo("https://github.com/yangky11/lean4-example", "7b6ecb9ad4829e4e73600a3329baeb3b5df8d23f")
   ...: trace(repo, dst_dir="traced_lean4-example")

2024-07-16 15:12:10.759 | DEBUG    | lean_dojo.data_extraction.lean:<module>:37 - Using GitHub personal access token for authentication
2024-07-16 15:12:12.528 | DEBUG    | lean_dojo.data_extraction.lean:_to_commit_hash:88 - Querying the commit hash for lean4 v4.9.0-rc3
2024-07-16 15:12:13.061 | DEBUG    | lean_dojo.data_extraction.trace:get_traced_repo_path:217 - The traced repo is available in the cache.
2024-07-16 15:12:13.061 | INFO     | lean_dojo.data_extraction.trace:trace:246 - Loading the traced repo from /private/home/kaiyuy/.cache/lean_dojo/yangky11-lean4-example-7b6ecb9ad4829e4e73600a3329baeb3b5df8d23f/lean4-example
2024-07-16 15:12:13.073 | DEBUG    | lean_dojo.utils:execute:110 - git remote get-url origin
2024-07-16 15:12:13.079 | DEBUG    | lean_dojo.utils:execute:110 - git log -n 1
2024-07-16 15:12:13.658 | DEBUG    | lean_dojo.data_extraction.traced_data:load_from_disk:1169 - Loading 907 traced XML files from /private/home/kaiyuy/.cache/lean_dojo/yangky11-lean4-example-7b6ecb9ad4829e4e73600a3329baeb3b5df8d23f/lean4-example with 31 workers
2024-07-16 15:12:18,147 INFO worker.py:1779 -- Started a local Ray instance. View the dashboard at http://127.0.0.1:8265 
  0%|                                                                                                                                                                                             | 0/907 [00:00<?, ?it/s](pid=1674267) 2024-07-16 15:12:21.139 | DEBUG    | lean_dojo.data_extraction.lean:<module>:37 - Using GitHub personal access token for authentication
100%|███████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████| 907/907 [01:02<00:00, 14.60it/s]
(pid=1674291) 2024-07-16 15:12:21.285 | DEBUG    | lean_dojo.data_extraction.lean:<module>:37 - Using GitHub personal access token for authentication [repeated 30x across cluster] (Ray deduplicates logs by default. Set RAY_DEDUP_LOGS=0 to disable log deduplication, or see https://docs.ray.io/en/master/ray-observability/user-guides/configure-logging.html#log-deduplication for more options.)
2024-07-16 15:13:23.458 | DEBUG    | lean_dojo.data_extraction.lean:get_dependencies:489 - Querying the dependencies of LeanGitRepo(url='https://github.com/yangky11/lean4-example', commit='7b6ecb9ad4829e4e73600a3329baeb3b5df8d23f')
2024-07-16 15:13:26.193 | DEBUG    | lean_dojo.data_extraction.traced_data:check_sanity:1032 - Checking the sanity of TracedRepo(repo=LeanGitRepo(url='https://github.com/yangky11/lean4-example', commit='7b6ecb9ad4829e4e73600a3329baeb3b5df8d23f'), dependencies={'lean4': LeanGitRepo(url='https://github.com/leanprover/lean4', commit='141856d6e6d808a85b9147a530294fee8e48e15f')}, root_dir=PosixPath('/private/home/kaiyuy/.cache/lean_dojo/yangky11-lean4-example-7b6ecb9ad4829e4e73600a3329baeb3b5df8d23f/lean4-example'))
Out[1]: TracedRepo(repo=LeanGitRepo(url='https://github.com/yangky11/lean4-example', commit='7b6ecb9ad4829e4e73600a3329baeb3b5df8d23f'), dependencies={'lean4': LeanGitRepo(url='https://github.com/leanprover/lean4', commit='141856d6e6d808a85b9147a530294fee8e48e15f')}, root_dir=PosixPath('/private/home/kaiyuy/.cache/lean_dojo/yangky11-lean4-example-7b6ecb9ad4829e4e73600a3329baeb3b5df8d23f/lean4-example'))

In [2]: 

In [2]: import os
   ...: import requests
   ...: from lean_dojo import *
   ...: 
   ...: repo = LeanGitRepo("https://github.com/yangky11/lean4-example", '7b6ecb9ad4829e4e73600a3329baeb3b5df8d23f' )
   ...: theorem = Theorem(repo, "Lean4Example.lean", "hello_world")
   ...: 
   ...: with Dojo(theorem) as (dojo, init_state):
   ...:     print(init_state)
   ...:     result = dojo.run_tac(init_state, "rw [add_assoc, add_comm b, -add_assoc]")
   ...:     assert isinstance(result, ProofFinished)
   ...:     print(result)
   ...: 
2024-07-16 15:20:42.029 | DEBUG    | lean_dojo.interaction.dojo:__enter__:159 - Initializing Dojo for Theorem(repo=LeanGitRepo(url='https://github.com/yangky11/lean4-example', commit='7b6ecb9ad4829e4e73600a3329baeb3b5df8d23f'), file_path=PosixPath('Lean4Example.lean'), full_name='hello_world')
2024-07-16 15:20:42.033 | DEBUG    | lean_dojo.data_extraction.trace:get_traced_repo_path:217 - The traced repo is available in the cache.
2024-07-16 15:20:42.040 | DEBUG    | lean_dojo.interaction.dojo:_modify_file:253 - Modifying `Lean4Example.lean` into `/private/home/kaiyuy/.cache/lean_dojo/yangky11-lean4-example-7b6ecb9ad4829e4e73600a3329baeb3b5df8d23f/lean4-example/Lean4Example8duxk1kd.lean`
TacticState(pp='a b c : Nat\n⊢ a + b + c = a + c + b', id=0, message=None)
2024-07-16 15:20:43.355 | DEBUG    | lean_dojo.interaction.dojo:_submit_request:372 - {"sid": 0, "cmd": "rw [add_assoc, add_comm b, -add_assoc]"}
2024-07-16 15:20:43.434 | DEBUG    | lean_dojo.interaction.dojo:__exit__:222 - Cleaning up.
---------------------------------------------------------------------------
AssertionError                            Traceback (most recent call last)
Cell In[2], line 11
      9 print(init_state)
     10 result = dojo.run_tac(init_state, "rw [add_assoc, add_comm b, -add_assoc]")
---> 11 assert isinstance(result, ProofFinished)
     12 print(result)

AssertionError: 

In [3]: result
Out[3]: LeanError(error="tactic 'rewrite' failed, equality or iff proof expected\n  ?m.142\na b c : Nat\n⊢ a + (c + b) = a + c + b")

BTW, I just updated ReProver to use Hugging Face checkpoints instead of PyTorch Ligthning checkpoints, which can hopefully remove the previous headache in evaluation. Please see the current README.

Yingjia-Wan commented 1 week ago

Thanks for the new update! After reinstalling lean_dojo (especially deleting the cache rm -rf ~/.cache/lean_dojo) and completing all setups in a newly cloned repo, I can run the example script like expected.

Regarding evaluating the model, I am running the script for evaluation successfully! Thank you for maintaining the whole project. Big appreciation for the wonderful work.

yangky11 commented 1 week ago

@Yingjia-Wan You're welcome.

How did you solve the "Unexpected EOF" problem you mentioned? A friend of mine is having a similar issue.

Yingjia-Wan commented 6 days ago

I experienced "Unexpected EOF" when running evaluation on a subset of the novel_promises set of LeanDojo benchmark. But there were hardly "Unexpected EOF" messages when running evaluation on the entire original novel_promise set.

Specify the paths for input (test.json) and output (mini_test.json) files

input_file_path = "./leandojo_benchmark_4/novel_premises/test.json" output_file_path = "./leandojo_benchmark_4/novel_premises/mini_test.json"

Function to extract the first n samples from a JSON file

def extract_first_n_samples(input_file, output_file, n=20):

Read and parse the JSON data from the input file

with open(input_file, 'r') as f:
    data = json.load(f)

# Extract the first n samples from the parsed JSON data
extracted_samples = data[:n]

# Write the extracted samples to the output file
with open(output_file, 'w') as f:
    json.dump(extracted_samples, f, indent=4)

print(f"Successfully created {output_file} with the first {n} samples.")

Call the function to extract the first 20 samples and create mini_test.json

extract_first_n_samples(input_file_path, output_file_path, n=20)

- Command:

python prover/evaluate.py --data-path data/leandojo_benchmark_4/mini_novel_premises/ --gen_ckpt_path kaiyuy/leandojo-lean4-tacgen-byt5-small --split test --num-workers 4 --num-gpus 4


- Output

(ReProver) yingjiawan@skcpu3:~/alisa/ReProver$ python prover/evaluate.py --data-path data/leandojo_benchmark_4/mini_novel_premises/ --gen_ckpt_path kaiyuy/leandojo-lean4-tacgen-byt5-small --split test --num-workers 4 --num-gpus 4 [2024-07-23 10:59:46,561] [INFO] [real_accelerator.py:203:get_accelerator] Setting ds_accelerator to cuda (auto detect) [WARNING] Please specify the CUTLASS repo directory as environment variable $CUTLASS_PATH [WARNING] sparse_attn requires a torch version >= 1.5 and < 2.0 but detected 2.3 [WARNING] using untested triton version (2.3.0), only 1.0.0 is known to be compatible 2024-07-23 10:59:47.933 | INFO | main:main:243 - PID: 3315410 2024-07-23 10:59:47.933 | INFO | main:main:244 - Namespace(data_path='data/leandojo_benchmark_4/mini_novel_premises/', exp_id=None, split='test', file_path=None, full_name=None, name_filter=None, num_theorems=None, use_vllm=False, gen_ckpt_path='kaiyuy/leandojo-lean4-tacgen-byt5-small', ret_ckpt_path=None, indexed_corpus_path=None, max_inp_seq_len=2048, max_oup_seq_len=512, length_penalty=0.0, tactic=None, module=None, num_sampled_tactics=64, timeout=600, num_workers=4, num_gpus=4, save_results=False, verbose=False) 2024-07-23 10:59:49.560 | INFO | main:_get_theorems_from_files:86 - 20 theorems loaded from data/leandojo_benchmark_4/mini_novel_premises/ 2024-07-23 10:59:50.443 | INFO | prover.proof_search:init:424 - Launching 4 workers with 4 GPUs. (pid=3320844) [2024-07-23 10:59:59,544] [INFO] [real_accelerator.py:203:get_accelerator] Setting ds_accelerator to cuda (auto detect) (pid=3320846) [2024-07-23 10:59:59,497] [INFO] [real_accelerator.py:203:get_accelerator] Setting ds_accelerator to cuda (auto detect) (pid=3320845) [2024-07-23 10:59:59,494] [INFO] [real_accelerator.py:203:get_accelerator] Setting ds_accelerator to cuda (auto detect) (pid=3320844) [WARNING] Please specify the CUTLASS repo directory as environment variable $CUTLASS_PATH (pid=3320846) [WARNING] Please specify the CUTLASS repo directory as environment variable $CUTLASS_PATH (pid=3320845) [WARNING] Please specify the CUTLASS repo directory as environment variable $CUTLASS_PATH (pid=3320847) [2024-07-23 10:59:59,800] [INFO] [real_accelerator.py:203:get_accelerator] Setting ds_accelerator to cuda (auto detect) (pid=3320847) [WARNING] Please specify the CUTLASS repo directory as environment variable $CUTLASS_PATH (pid=3320844) [WARNING] sparse_attn requires a torch version >= 1.5 and < 2.0 but detected 2.3 (pid=3320844) [WARNING] using untested triton version (2.3.0), only 1.0.0 is known to be compatible (pid=3320846) [WARNING] sparse_attn requires a torch version >= 1.5 and < 2.0 but detected 2.3 (pid=3320846) [WARNING] using untested triton version (2.3.0), only 1.0.0 is known to be compatible (pid=3320845) [WARNING] sparse_attn requires a torch version >= 1.5 and < 2.0 but detected 2.3 (pid=3320845) [WARNING] using untested triton version (2.3.0), only 1.0.0 is known to be compatible (pid=3320847) [WARNING] sparse_attn requires a torch version >= 1.5 and < 2.0 but detected 2.3 (pid=3320847) [WARNING] using untested triton version (2.3.0), only 1.0.0 is known to be compatible (ProverActor pid=3320846) 2024-07-23 11:00:02.918 | INFO | prover.proof_search:search:81 - Proving Theorem(repo=LeanGitRepo(url='https://github.com/leanprover-community/mathlib4', commit='fe4454af900584467d21f4fd4fe951d29d9332a7'), file_path=PosixPath('Mathlib/Order/MinMax.lean'), full_name='min_lt_iff') (ProverActor pid=3320844) 2024-07-23 11:00:02.948 | INFO | prover.proof_search:search:81 - Proving Theorem(repo=LeanGitRepo(url='https://github.com/leanprover-community/mathlib4', commit='fe4454af900584467d21f4fd4fe951d29d9332a7'), file_path=PosixPath('Mathlib/FieldTheory/RatFunc.lean'), full_name='RatFunc.mk_eq_mk') (ProverActor pid=3320845) 2024-07-23 11:00:03.016 | INFO | prover.proof_search:search:81 - Proving Theorem(repo=LeanGitRepo(url='https://github.com/leanprover-community/mathlib4', commit='fe4454af900584467d21f4fd4fe951d29d9332a7'), file_path=PosixPath('Mathlib/LinearAlgebra/Lagrange.lean'), full_name='Lagrange.interpolate_singleton') (ProverActor pid=3320847) 2024-07-23 11:00:03.132 | INFO | prover.proof_search:search:81 - Proving Theorem(repo=LeanGitRepo(url='https://github.com/leanprover-community/mathlib4', commit='fe4454af900584467d21f4fd4fe951d29d9332a7'), file_path=PosixPath('Mathlib/LinearAlgebra/FreeModule/PID.lean'), full_name='Module.free_of_finite_type_torsion_free') (ProverActor pid=3320846) 2024-07-23 11:00:03.182 | WARNING | prover.proof_search:search:132 - Unexpected EOF (ProverActor pid=3320846) 2024-07-23 11:00:03.189 | INFO | prover.proof_search:search:81 - Proving Theorem(repo=LeanGitRepo(url='https://github.com/leanprover-community/mathlib4', commit='fe4454af900584467d21f4fd4fe951d29d9332a7'), file_path=PosixPath('Mathlib/FieldTheory/Finite/Polynomial.lean'), full_name='MvPolynomial.ker_evalₗ') (ProverActor pid=3320846) 2024-07-23 11:00:03.528 | WARNING | prover.proof_search:search:132 - Unexpected EOF (ProverActor pid=3320846) 2024-07-23 11:00:03.535 | INFO | prover.proof_search:search:81 - Proving Theorem(repo=LeanGitRepo(url='https://github.com/leanprover-community/mathlib4', commit='fe4454af900584467d21f4fd4fe951d29d9332a7'), file_path=PosixPath('Mathlib/FieldTheory/PerfectClosure.lean'), full_name='PerfectClosure.frobenius_mk') (ProverActor pid=3320845) 2024-07-23 11:00:03.712 | WARNING | prover.proof_search:search:132 - Unexpected EOF (ProverActor pid=3320845) 2024-07-23 11:00:03.719 | INFO | prover.proof_search:search:81 - Proving Theorem(repo=LeanGitRepo(url='https://github.com/leanprover-community/mathlib4', commit='fe4454af900584467d21f4fd4fe951d29d9332a7'), file_path=PosixPath('Mathlib/Order/Cover.lean'), full_name='Set.covBy_iff_exists_sdiff_singleton') (ProverActor pid=3320847) 2024-07-23 11:00:03.757 | WARNING | prover.proof_search:search:132 - Unexpected EOF (ProverActor pid=3320847) 2024-07-23 11:00:03.765 | INFO | prover.proof_search:search:81 - Proving Theorem(repo=LeanGitRepo(url='https://github.com/leanprover-community/mathlib4', commit='fe4454af900584467d21f4fd4fe951d29d9332a7'), file_path=PosixPath('Mathlib/CategoryTheory/Limits/Shapes/StrictInitial.lean'), full_name='CategoryTheory.Limits.mulIsInitial_inv') (ProverActor pid=3320847) 2024-07-23 11:00:04.095 | WARNING | prover.proof_search:search:132 - Unexpected EOF (ProverActor pid=3320847) 2024-07-23 11:00:04.106 | INFO | prover.proof_search:search:81 - Proving Theorem(repo=LeanGitRepo(url='https://github.com/leanprover-community/mathlib4', commit='fe4454af900584467d21f4fd4fe951d29d9332a7'), file_path=PosixPath('Mathlib/FieldTheory/AbelRuffini.lean'), full_name='gal_mul_isSolvable') (ProverActor pid=3320846) 2024-07-23 11:00:04.132 | WARNING | prover.proof_search:search:132 - Unexpected EOF (ProverActor pid=3320846) 2024-07-23 11:00:04.140 | INFO | prover.proof_search:search:81 - Proving Theorem(repo=LeanGitRepo(url='https://github.com/leanprover-community/mathlib4', commit='fe4454af900584467d21f4fd4fe951d29d9332a7'), file_path=PosixPath('Mathlib/CategoryTheory/GradedObject.lean'), full_name='CategoryTheory.GradedObject.isIso_of_isIso_apply') (ProverActor pid=3320845) 2024-07-23 11:00:04.656 | WARNING | prover.proof_search:search:132 - Unexpected EOF (ProverActor pid=3320845) 2024-07-23 11:00:04.664 | INFO | prover.proof_search:search:81 - Proving Theorem(repo=LeanGitRepo(url='https://github.com/leanprover-community/mathlib4', commit='fe4454af900584467d21f4fd4fe951d29d9332a7'), file_path=PosixPath('Mathlib/Order/Disjointed.lean'), full_name='iUnion_disjointed') (ProverActor pid=3320847) 2024-07-23 11:00:04.907 | WARNING | prover.proof_search:search:132 - Unexpected EOF (ProverActor pid=3320847) 2024-07-23 11:00:04.915 | INFO | prover.proof_search:search:81 - Proving Theorem(repo=LeanGitRepo(url='https://github.com/leanprover-community/mathlib4', commit='fe4454af900584467d21f4fd4fe951d29d9332a7'), file_path=PosixPath('Mathlib/CategoryTheory/Limits/Fubini.lean'), full_name='CategoryTheory.Limits.colimitCurrySwapCompColimIsoColimitCurryCompColim_ι_ι_inv') (ProverActor pid=3320846) 2024-07-23 11:00:04.868 | WARNING | prover.proof_search:search:132 - Unexpected EOF (ProverActor pid=3320846) 2024-07-23 11:00:04.876 | INFO | prover.proof_search:search:81 - Proving Theorem(repo=LeanGitRepo(url='https://github.com/leanprover-community/mathlib4', commit='fe4454af900584467d21f4fd4fe951d29d9332a7'), file_path=PosixPath('Mathlib/Order/Filter/Basic.lean'), full_name='Filter.bind_mono') (ProverActor pid=3320845) 2024-07-23 11:00:04.958 | WARNING | prover.proof_search:search:132 - Unexpected EOF (ProverActor pid=3320845) 2024-07-23 11:00:04.965 | INFO | prover.proof_search:search:81 - Proving Theorem(repo=LeanGitRepo(url='https://github.com/leanprover-community/mathlib4', commit='fe4454af900584467d21f4fd4fe951d29d9332a7'), file_path=PosixPath('Mathlib/CategoryTheory/Abelian/Basic.lean'), full_name='CategoryTheory.Abelian.mono_inl_of_factor_thru_epi_mono_factorization') (ProverActor pid=3320847) 2024-07-23 11:00:05.484 | WARNING | prover.proof_search:search:132 - Unexpected EOF (ProverActor pid=3320847) 2024-07-23 11:00:05.492 | INFO | prover.proof_search:search:81 - Proving Theorem(repo=LeanGitRepo(url='https://github.com/leanprover-community/mathlib4', commit='fe4454af900584467d21f4fd4fe951d29d9332a7'), file_path=PosixPath('Mathlib/Order/RelIso/Basic.lean'), full_name='RelIso.cast_trans') (ProverActor pid=3320845) 2024-07-23 11:00:05.705 | WARNING | prover.proof_search:search:132 - Unexpected EOF (ProverActor pid=3320845) 2024-07-23 11:00:05.711 | INFO | prover.proof_search:search:81 - Proving Theorem(repo=LeanGitRepo(url='https://github.com/leanprover-community/mathlib4', commit='fe4454af900584467d21f4fd4fe951d29d9332a7'), file_path=PosixPath('Mathlib/FieldTheory/AbelRuffini.lean'), full_name='gal_X_pow_sub_one_isSolvable') (ProverActor pid=3320844) 2024-07-23 11:00:05.865 | WARNING | prover.proof_search:search:132 - Unexpected EOF (ProverActor pid=3320844) 2024-07-23 11:00:05.988 | INFO | prover.proof_search:search:81 - Proving Theorem(repo=LeanGitRepo(url='https://github.com/leanprover-community/mathlib4', commit='fe4454af900584467d21f4fd4fe951d29d9332a7'), file_path=PosixPath('Mathlib/Order/WellFoundedSet.lean'), full_name='Set.WellFoundedOn.insert') (ProverActor pid=3320845) 2024-07-23 11:00:06.466 | WARNING | prover.proof_search:search:132 - Unexpected EOF (ProverActor pid=3320845) 2024-07-23 11:00:06.472 | INFO | prover.proof_search:search:81 - Proving Theorem(repo=LeanGitRepo(url='https://github.com/leanprover-community/mathlib4', commit='fe4454af900584467d21f4fd4fe951d29d9332a7'), file_path=PosixPath('Mathlib/CategoryTheory/Limits/Constructions/Filtered.lean'), full_name='CategoryTheory.Limits.has_limits_of_finite_and_cofiltered') (ProverActor pid=3320847) 2024-07-23 11:00:06.668 | WARNING | prover.proof_search:search:132 - Unexpected EOF (ProverActor pid=3320847) 2024-07-23 11:00:06.675 | INFO | prover.proof_search:search:81 - Proving Theorem(repo=LeanGitRepo(url='https://github.com/leanprover-community/mathlib4', commit='fe4454af900584467d21f4fd4fe951d29d9332a7'), file_path=PosixPath('Mathlib/FieldTheory/Finiteness.lean'), full_name='IsNoetherian.coeSort_finsetBasisIndex') (ProverActor pid=3320845) 2024-07-23 11:00:06.747 | WARNING | prover.proof_search:search:132 - Unexpected EOF (ProverActor pid=3320845) 2024-07-23 11:00:06.755 | INFO | prover.proof_search:search:81 - Proving Theorem(repo=LeanGitRepo(url='https://github.com/leanprover-community/mathlib4', commit='fe4454af900584467d21f4fd4fe951d29d9332a7'), file_path=PosixPath('Mathlib/Order/SymmDiff.lean'), full_name='symmDiff_assoc') (ProverActor pid=3320847) 2024-07-23 11:00:06.941 | WARNING | prover.proof_search:search:132 - Unexpected EOF (ProverActor pid=3320844) 2024-07-23 11:00:07.331 | WARNING | prover.proof_search:search:132 - Unexpected EOF (ProverActor pid=3320845) 2024-07-23 11:00:07.629 | WARNING | prover.proof_search:search:132 - Unexpected EOF 2024-07-23 11:00:15.159 | INFO | main:evaluate:153 - Evaluation done! 0 theorems proved, 0 theorems failed, 20 non-theorems discarded 2024-07-23 11:00:15.161 | INFO | main:main:271 - Pass@1: nan (ProverActor pid=3320846) 2024-07-23 11:00:15.157 | WARNING | prover.proof_search:search:132 - Unexpected EOF