-
Notifications
You must be signed in to change notification settings - Fork 128
Description
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.