Skip to content

Run traced_repo = trace(repo) meet the error like KeyError: 'batteries' #1160

@zx1384187

Description

@zx1384187

when i run "traced_repo = trace(repo) "I met the error below:
Traceback (most recent call last): File "/data1/yanhuiyuan/workspace/InternLM-Math/tests/test_lean_dojo.py", line 12, in <module> traced_repo = trace(repo) ^^^^^^^^^^^ File "/home/yanhuiyuan/anaconda3/envs/atp/lib/python3.11/site-packages/lean_dojo/data_extraction/trace.py", line 250, in trace traced_repo.check_sanity() File "/home/yanhuiyuan/anaconda3/envs/atp/lib/python3.11/site-packages/lean_dojo/data_extraction/traced_data.py", line 1081, in check_sanity tf.check_sanity() File "/home/yanhuiyuan/anaconda3/envs/atp/lib/python3.11/site-packages/lean_dojo/data_extraction/traced_data.py", line 711, in check_sanity for t in self.get_traced_theorems(): ^^^^^^^^^^^^^^^^^^^^^^^^^^ File "/home/yanhuiyuan/anaconda3/envs/atp/lib/python3.11/site-packages/lean_dojo/data_extraction/traced_data.py", line 807, in get_traced_theorems self.traverse_preorder(_callback, node_cls=None) File "/home/yanhuiyuan/anaconda3/envs/atp/lib/python3.11/site-packages/lean_dojo/data_extraction/traced_data.py", line 724, in traverse_preorder self.ast.traverse_preorder(callback, node_cls) File "/home/yanhuiyuan/anaconda3/envs/atp/lib/python3.11/site-packages/lean_dojo/data_extraction/ast.py", line 56, in traverse_preorder child.traverse_preorder(callback, node_cls, parents + [self]) File "/home/yanhuiyuan/anaconda3/envs/atp/lib/python3.11/site-packages/lean_dojo/data_extraction/ast.py", line 56, in traverse_preorder child.traverse_preorder(callback, node_cls, parents + [self]) File "/home/yanhuiyuan/anaconda3/envs/atp/lib/python3.11/site-packages/lean_dojo/data_extraction/ast.py", line 53, in traverse_preorder if callback(self, parents): ^^^^^^^^^^^^^^^^^^^^^^^ File "/home/yanhuiyuan/anaconda3/envs/atp/lib/python3.11/site-packages/lean_dojo/data_extraction/traced_data.py", line 798, in _callback repo, path = self._get_repo_and_relative_path() ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ File "/home/yanhuiyuan/anaconda3/envs/atp/lib/python3.11/site-packages/lean_dojo/data_extraction/traced_data.py", line 733, in _get_repo_and_relative_path repo = self.traced_repo.dependencies[name] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~^^^^^^ KeyError: 'batteries'

But i have build completed successfully.like
info: downloading https://github.com/leanprover/lean4/releases/download/v4.10.0-rc1/lean-4.10.0-rc1-linux.tar.zst 191.9 MiB / 191.9 MiB (100 %) 11.6 MiB/s ETA: 0 s info: installing /home/yanhuiyuan/.elan/toolchains/leanprover--lean4---v4.10.0-rc1 info: batteries: cloning https://github.com/leanprover-community/batteries to '././.lake/packages/batteries' info: Qq: cloning https://github.com/leanprover-community/quote4 to '././.lake/packages/Qq' info: aesop: cloning https://github.com/leanprover-community/aesop to '././.lake/packages/aesop' info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4 to '././.lake/packages/proofwidgets' info: importGraph: cloning https://github.com/leanprover-community/import-graph to '././.lake/packages/importGraph' info: Cli: cloning https://github.com/leanprover/lean4-cli to '././.lake/packages/Cli' Build completed successfully.

Besides,how can i do to make sure it does not neet to recompile when i run"traced_repo = trace(repo)"?
Could someone give me some help?Please.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions