Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Error tracing mathlib4 v4.15.0-rc1 #215

Closed
oOo0oOo opened this issue Dec 11, 2024 · 1 comment
Closed

Error tracing mathlib4 v4.15.0-rc1 #215

oOo0oOo opened this issue Dec 11, 2024 · 1 comment

Comments

@oOo0oOo
Copy link

oOo0oOo commented Dec 11, 2024 •
edited
Loading

Description
I cannot seem to trace the repo for v4.15.0-rc1. The same code worked for v4.13.0.

Tracing repeatedly tripped over this file:
https://github.com/leanprover-community/mathlib4/blob/41ff1f7899c971f91362710d4444e338b8acd644/Mathlib/Data/Char.lean

This is not crucial for my application, just wanted to report it here.
I might run some other versions overnight over the next few days.

Detailed Steps to Reproduce the Behavior

from lean_dojo import LeanGitRepo, trace

# v4.15.0-rc1 ==> 41ff1f7
# mathlib v4.13.0 ==> d731765 (this worked a month ago, although lean_dojo version might have been different)
repo = LeanGitRepo("https://github.com/leanprover-community/mathlib4", "41ff1f7")

# Some repo infos
print("Lean version:", repo.get_config("lean-toolchain")["content"])

traced_repo = trace(repo)

Logs in Debug Mode

Lean version: leanprover/lean4:v4.15.0-rc1

2024-12-10 21:54:38.993 | INFO     | lean_dojo.data_extraction.trace:get_traced_repo_path:210 - Tracing LeanGitRepo(url='https://github.com/leanprover-community/mathlib4', commit='41ff1f7899c971f91362710d4444e338b8acd644')
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision '8e5cb8d424df462f84997dd68af6f40e347c3e35'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient
info: LeanSearchClient: checking out revision 'd7caecce0d0f003fd5e9cce9a61f1dd6ba83142b'
info: importGraph: cloning https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision 'ed3b856bd8893ade75cafe13e8544d4c2660f377'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision '2b000e02d50394af68cfb4770a291113d94801b5'
info: aesop: cloning https://github.com/leanprover-community/aesop
info: aesop: checking out revision '8b6048aa0a4a4b6bcf83597802d8dee734e64b7e'
info: Qq: cloning https://github.com/leanprover-community/quote4
info: Qq: checking out revision 'ad942fdf0b15c38bface6acbb01d63855a2519ac'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision '7805acf1864ba1a2e359f86a8f092ccf1438ad83'
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision '0c8ea32a15a4f74143e4e1e107ba2c412adb90fd'
Build completed successfully.
100%|█████████████████████████████████████████████████████████████████████████████████████████████████████████████▊| 6936/6944 [1:11:16<00:05,  1.58it/s]2024-12-10 23:38:46.775 | WARNING  | lean_dojo.data_extraction.trace:check_files:120 - Missing /tmp/tmpeffjloob/mathlib4/.lake/packages/importGraph/.lake/build/ir/ImportGraph.ast.json
2024-12-10 23:38:46.775 | WARNING  | lean_dojo.data_extraction.trace:check_files:120 - Missing /tmp/tmpeffjloob/mathlib4/.lake/packages/importGraph/.lake/build/ir/ImportGraph.dep_paths
2024-12-10 23:38:46.775 | WARNING  | lean_dojo.data_extraction.trace:check_files:120 - Missing /tmp/tmpeffjloob/mathlib4/.lake/packages/importGraph/.lake/build/ir/ImportGraph/Cli.dep_paths
2024-12-10 23:38:46.775 | WARNING  | lean_dojo.data_extraction.trace:check_files:120 - Missing /tmp/tmpeffjloob/mathlib4/.lake/packages/importGraph/.lake/build/ir/ImportGraph/Cli.ast.json
2024-12-10 23:38:46.775 | WARNING  | lean_dojo.data_extraction.trace:check_files:120 - Missing /tmp/tmpeffjloob/mathlib4/.lake/packages/importGraph/.lake/build/ir/Main.dep_paths
2024-12-10 23:38:46.775 | WARNING  | lean_dojo.data_extraction.trace:check_files:120 - Missing /tmp/tmpeffjloob/mathlib4/.lake/packages/importGraph/.lake/build/ir/Main.ast.json
Build completed successfully.
2024-12-10 23:38:50,452	INFO worker.py:1812 -- Started a local Ray instance. View the dashboard at http://127.0.0.1:8265 
  7%|███████▌                                                                                                         | 464/6939 [00:18<04:22, 24.62it/s]
Traceback (most recent call last):
  File "~/Code/mathlib4_structure/data_extraction/extract.py", line 11, in <module>
    traced_repo = trace(repo)
                  ^^^^^^^^^^^
  File "~/Code/mathlib4_structure/data_extraction/venv/lib/python3.11/site-packages/lean_dojo/data_extraction/trace.py", line 247, in trace
    cached_path = get_traced_repo_path(repo, build_deps)
                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "~/Code/mathlib4_structure/data_extraction/venv/lib/python3.11/site-packages/lean_dojo/data_extraction/trace.py", line 215, in get_traced_repo_path
    traced_repo = TracedRepo.from_traced_files(src_dir, build_deps)
                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "~/Code/mathlib4_structure/data_extraction/venv/lib/python3.11/site-packages/lean_dojo/data_extraction/traced_data.py", line 1125, in from_traced_files
    traced_files = list(
                   ^^^^^
  File "~/Code/mathlib4_structure/data_extraction/venv/lib/python3.11/site-packages/tqdm/std.py", line 1181, in __iter__
    for obj in iterable:
  File "~/Code/mathlib4_structure/data_extraction/venv/lib/python3.11/site-packages/ray/util/actor_pool.py", line 170, in get_generator
    yield self.get_next_unordered()
          ^^^^^^^^^^^^^^^^^^^^^^^^^
  File "~/Code/mathlib4_structure/data_extraction/venv/lib/python3.11/site-packages/ray/util/actor_pool.py", line 370, in get_next_unordered
    return ray.get(future)
           ^^^^^^^^^^^^^^^
  File "~/Code/mathlib4_structure/data_extraction/venv/lib/python3.11/site-packages/ray/_private/auto_init_hook.py", line 21, in auto_init_wrapper
    return fn(*args, **kwargs)
           ^^^^^^^^^^^^^^^^^^^
  File "~/Code/mathlib4_structure/data_extraction/venv/lib/python3.11/site-packages/ray/_private/client_mode_hook.py", line 103, in wrapper
    return func(*args, **kwargs)
           ^^^^^^^^^^^^^^^^^^^^^
  File "~/Code/mathlib4_structure/data_extraction/venv/lib/python3.11/site-packages/ray/_private/worker.py", line 2755, in get
    values, debugger_breakpoint = worker.get_objects(object_refs, timeout=timeout)
                                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "~/Code/mathlib4_structure/data_extraction/venv/lib/python3.11/site-packages/ray/_private/worker.py", line 906, in get_objects
    raise value.as_instanceof_cause()
ray.exceptions.RayTaskError(ValueError): ray::_TracedRepoHelper.parse_traced_file() (pid=1371105, ip=192.168.1.137, actor_id=0f45543faaf574c6250a31e101000000, repr=<lean_dojo.data_extraction.traced_data._TracedRepoHelper object at 0x73a2d466ea50>)
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "~/Code/mathlib4_structure/data_extraction/venv/lib/python3.11/site-packages/lean_dojo/data_extraction/traced_data.py", line 991, in parse_traced_file
    return TracedFile.from_traced_file(self.root_dir, path, self.repo)
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "~/Code/mathlib4_structure/data_extraction/venv/lib/python3.11/site-packages/lean_dojo/data_extraction/traced_data.py", line 536, in from_traced_file
    return cls._from_lean4_traced_file(root_dir, json_path, repo)
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "~/Code/mathlib4_structure/data_extraction/venv/lib/python3.11/site-packages/lean_dojo/data_extraction/traced_data.py", line 558, in _from_lean4_traced_file
    TracedFile._post_process_lean4(
  File "~/Code/mathlib4_structure/data_extraction/venv/lib/python3.11/site-packages/lean_dojo/data_extraction/traced_data.py", line 582, in _post_process_lean4
    end = lean_file.convert_pos(t["endPos"])
          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "~/Code/mathlib4_structure/data_extraction/venv/lib/python3.11/site-packages/lean_dojo/data_extraction/lean.py", line 364, in convert_pos
    raise ValueError(f"Invalid byte index {byte_idx} in {self.path}.")
ValueError: Invalid byte index 1025 in Mathlib/Data/Char.lean.

Platform Information

  • OS: Ubuntu 24.04.1
  • LeanDojo Version 2.1.3

UPDATE

I have just tried to trace the most recent repo (nightly-2024-12-10, f0f251d)

There is an identical error in a different lean file.

2024-12-11 08:27:32.123 | WARNING  | lean_dojo.data_extraction.lean:__post_init__:579 - LeanGitRepo(url='https://github.com/leanprover-community/mathlib4', commit='f0f251d299ff907bada73f4dbfba2dfd0d619b69') relies on an unsupported Lean version: nightly-2024-12-10
Lean version: leanprover/lean4:nightly-2024-12-10

2024-12-11 08:27:32.668 | INFO     | lean_dojo.data_extraction.trace:get_traced_repo_path:210 - Tracing LeanGitRepo(url='https://github.com/leanprover-community/mathlib4', commit='f0f251d299ff907bada73f4dbfba2dfd0d619b69')
info: downloading component 'lean'
254.1 MiB / 254.1 MiB (100 %)  33.2 MiB/s ETA:   0 s
info: installing component 'lean'
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision '8e5cb8d424df462f84997dd68af6f40e347c3e35'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient
info: LeanSearchClient: checking out revision 'd7caecce0d0f003fd5e9cce9a61f1dd6ba83142b'
info: importGraph: cloning https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision 'ed3b856bd8893ade75cafe13e8544d4c2660f377'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision '2b000e02d50394af68cfb4770a291113d94801b5'
info: aesop: cloning https://github.com/leanprover-community/aesop
info: aesop: checking out revision '43bcb1964528411e47bfa4edd0c87d1face1fce4'
info: Qq: cloning https://github.com/leanprover-community/quote4
info: Qq: checking out revision 'ad942fdf0b15c38bface6acbb01d63855a2519ac'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision '82fb7dbd981552872423f5f8b5337aa04fe2a366'
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision '0c8ea32a15a4f74143e4e1e107ba2c412adb90fd'
Build completed successfully.
100%|█████████████████████████████████████████████████████████████████████████████████████████████████████████████▊| 6968/6983 [1:19:52<00:09,  1.65it/s]2024-12-11 10:23:13.323 | WARNING  | lean_dojo.data_extraction.trace:check_files:120 - Missing /tmp/tmpd1k4360u/mathlib4/.lake/packages/proofwidgets/.lake/build/ir/ProofWidgets/Demos/RbTree.ast.json
2024-12-11 10:23:13.323 | WARNING  | lean_dojo.data_extraction.trace:check_files:120 - Missing /tmp/tmpd1k4360u/mathlib4/.lake/packages/proofwidgets/.lake/build/ir/ProofWidgets/Component/InteractiveSvg.ast.json
2024-12-11 10:23:13.323 | WARNING  | lean_dojo.data_extraction.trace:check_files:120 - Missing /tmp/tmpd1k4360u/mathlib4/.lake/packages/proofwidgets/.lake/build/ir/ProofWidgets/Demos/Svg.ast.json
2024-12-11 10:23:13.323 | WARNING  | lean_dojo.data_extraction.trace:check_files:120 - Missing /tmp/tmpd1k4360u/mathlib4/.lake/packages/proofwidgets/.lake/build/ir/ProofWidgets/Demos/Plot.dep_paths
2024-12-11 10:23:13.323 | WARNING  | lean_dojo.data_extraction.trace:check_files:120 - Missing /tmp/tmpd1k4360u/mathlib4/.lake/packages/proofwidgets/.lake/build/ir/ProofWidgets/Demos/Graph/Basic.ast.json
2024-12-11 10:23:13.323 | WARNING  | lean_dojo.data_extraction.trace:check_files:120 - Missing /tmp/tmpd1k4360u/mathlib4/.lake/packages/proofwidgets/.lake/build/ir/ProofWidgets/Demos/Graph/ExprGraph.ast.json
2024-12-11 10:23:13.323 | WARNING  | lean_dojo.data_extraction.trace:check_files:120 - Missing /tmp/tmpd1k4360u/mathlib4/.lake/packages/proofwidgets/.lake/build/ir/ProofWidgets/Demos/InteractiveSvg.ast.json
2024-12-11 10:23:13.323 | WARNING  | lean_dojo.data_extraction.trace:check_files:120 - Missing /tmp/tmpd1k4360u/mathlib4/.lake/packages/proofwidgets/.lake/build/ir/ProofWidgets/Demos/RbTree.dep_paths
2024-12-11 10:23:13.323 | WARNING  | lean_dojo.data_extraction.trace:check_files:120 - Missing /tmp/tmpd1k4360u/mathlib4/.lake/packages/proofwidgets/.lake/build/ir/ProofWidgets/Demos/Plot.ast.json
2024-12-11 10:23:13.323 | WARNING  | lean_dojo.data_extraction.trace:check_files:120 - Missing /tmp/tmpd1k4360u/mathlib4/.lake/packages/proofwidgets/.lake/build/ir/ProofWidgets/Component/InteractiveSvg.dep_paths
2024-12-11 10:23:13.323 | WARNING  | lean_dojo.data_extraction.trace:check_files:120 - Missing /tmp/tmpd1k4360u/mathlib4/.lake/packages/proofwidgets/.lake/build/ir/ProofWidgets/Demos/InteractiveSvg.dep_paths
2024-12-11 10:23:13.323 | WARNING  | lean_dojo.data_extraction.trace:check_files:120 - Missing /tmp/tmpd1k4360u/mathlib4/.lake/packages/proofwidgets/.lake/build/ir/ProofWidgets/Demos/Graph/MVarGraph.ast.json
2024-12-11 10:23:13.323 | WARNING  | lean_dojo.data_extraction.trace:check_files:120 - Missing /tmp/tmpd1k4360u/mathlib4/.lake/packages/proofwidgets/.lake/build/ir/ProofWidgets.dep_paths
2024-12-11 10:23:13.323 | WARNING  | lean_dojo.data_extraction.trace:check_files:120 - Missing /tmp/tmpd1k4360u/mathlib4/.lake/packages/proofwidgets/.lake/build/ir/ProofWidgets/Demos/Graph/MVarGraph.dep_paths
2024-12-11 10:23:13.323 | WARNING  | lean_dojo.data_extraction.trace:check_files:120 - Missing /tmp/tmpd1k4360u/mathlib4/.lake/packages/proofwidgets/.lake/build/ir/ProofWidgets/Demos/Graph/Basic.dep_paths
2024-12-11 10:23:13.323 | WARNING  | lean_dojo.data_extraction.trace:check_files:120 - Missing /tmp/tmpd1k4360u/mathlib4/.lake/packages/proofwidgets/.lake/build/ir/ProofWidgets/Demos/Svg.dep_paths
2024-12-11 10:23:13.323 | WARNING  | lean_dojo.data_extraction.trace:check_files:120 - Missing /tmp/tmpd1k4360u/mathlib4/.lake/packages/proofwidgets/.lake/build/ir/ProofWidgets/Demos/ExprPresentation.dep_paths
2024-12-11 10:23:13.323 | WARNING  | lean_dojo.data_extraction.trace:check_files:120 - Missing /tmp/tmpd1k4360u/mathlib4/.lake/packages/proofwidgets/.lake/build/ir/ProofWidgets/Demos/ExprPresentation.ast.json
2024-12-11 10:23:13.323 | WARNING  | lean_dojo.data_extraction.trace:check_files:120 - Missing /tmp/tmpd1k4360u/mathlib4/.lake/packages/proofwidgets/.lake/build/ir/ProofWidgets/Demos/Graph/ExprGraph.dep_paths
2024-12-11 10:23:13.323 | WARNING  | lean_dojo.data_extraction.trace:check_files:120 - Missing /tmp/tmpd1k4360u/mathlib4/.lake/packages/proofwidgets/.lake/build/ir/ProofWidgets.ast.json
Build completed successfully.
2024-12-11 10:25:42.203 | WARNING  | lean_dojo.data_extraction.lean:__post_init__:579 - LeanGitRepo(url='/tmp/tmpd1k4360u/mathlib4', commit='f0f251d299ff907bada73f4dbfba2dfd0d619b69') relies on an unsupported Lean version: nightly-2024-12-10
2024-12-11 10:25:43,877	INFO worker.py:1812 -- Started a local Ray instance. View the dashboard at http://127.0.0.1:8265 
  8%|██████████                                                                                                              | 588/6971 [00:28<05:08, 20.66it/s]
Traceback (most recent call last):
  File "~/Code/mathlib4_structure/data_extraction/extract.py", line 12, in <module>
  File "~/Code/mathlib4_structure/data_extraction/venv/lib/python3.11/site-packages/lean_dojo/data_extraction/trace.py", line 247, in trace
    cached_path = get_traced_repo_path(repo, build_deps)
                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "~/Code/mathlib4_structure/data_extraction/venv/lib/python3.11/site-packages/lean_dojo/data_extraction/trace.py", line 215, in get_traced_repo_path
    traced_repo = TracedRepo.from_traced_files(src_dir, build_deps)
                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "~/Code/mathlib4_structure/data_extraction/venv/lib/python3.11/site-packages/lean_dojo/data_extraction/traced_data.py", line 1125, in from_traced_files
    traced_files = list(
                   ^^^^^
  File "~/Code/mathlib4_structure/data_extraction/venv/lib/python3.11/site-packages/tqdm/std.py", line 1181, in __iter__
    for obj in iterable:
  File "~/Code/mathlib4_structure/data_extraction/venv/lib/python3.11/site-packages/ray/util/actor_pool.py", line 170, in get_generator
    yield self.get_next_unordered()
          ^^^^^^^^^^^^^^^^^^^^^^^^^
  File "~/Code/mathlib4_structure/data_extraction/venv/lib/python3.11/site-packages/ray/util/actor_pool.py", line 370, in get_next_unordered
    return ray.get(future)
           ^^^^^^^^^^^^^^^
  File "~/Code/mathlib4_structure/data_extraction/venv/lib/python3.11/site-packages/ray/_private/auto_init_hook.py", line 21, in auto_init_wrapper
    return fn(*args, **kwargs)
           ^^^^^^^^^^^^^^^^^^^
  File "~/Code/mathlib4_structure/data_extraction/venv/lib/python3.11/site-packages/ray/_private/client_mode_hook.py", line 103, in wrapper
    return func(*args, **kwargs)
           ^^^^^^^^^^^^^^^^^^^^^
  File "~/Code/mathlib4_structure/data_extraction/venv/lib/python3.11/site-packages/ray/_private/worker.py", line 2755, in get
    values, debugger_breakpoint = worker.get_objects(object_refs, timeout=timeout)
                                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "~/Code/mathlib4_structure/data_extraction/venv/lib/python3.11/site-packages/ray/_private/worker.py", line 906, in get_objects
    raise value.as_instanceof_cause()
ray.exceptions.RayTaskError(ValueError): ray::_TracedRepoHelper.parse_traced_file() (pid=1773227, ip=192.168.1.137, actor_id=16bf68fe65b7ab3b65509c5801000000, repr=<lean_dojo.data_extraction.traced_data._TracedRepoHelper object at 0x7ec102d95150>)
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "~/Code/mathlib4_structure/data_extraction/venv/lib/python3.11/site-packages/lean_dojo/data_extraction/traced_data.py", line 991, in parse_traced_file
    return TracedFile.from_traced_file(self.root_dir, path, self.repo)
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "~/Code/mathlib4_structure/data_extraction/venv/lib/python3.11/site-packages/lean_dojo/data_extraction/traced_data.py", line 536, in from_traced_file
    return cls._from_lean4_traced_file(root_dir, json_path, repo)
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "~/Code/mathlib4_structure/data_extraction/venv/lib/python3.11/site-packages/lean_dojo/data_extraction/traced_data.py", line 558, in _from_lean4_traced_file
    TracedFile._post_process_lean4(
  File "~/Code/mathlib4_structure/data_extraction/venv/lib/python3.11/site-packages/lean_dojo/data_extraction/traced_data.py", line 582, in _post_process_lean4
    end = lean_file.convert_pos(t["endPos"])
          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "~/Code/mathlib4_structure/data_extraction/venv/lib/python3.11/site-packages/lean_dojo/data_extraction/lean.py", line 364, in convert_pos
    raise ValueError(f"Invalid byte index {byte_idx} in {self.path}.")
ValueError: Invalid byte index 4839 in Mathlib/Order/Category/FinBoolAlg.lean.

SOLUTION

OK, never mind. Upgrading to lean-dojo-2.2.0 (as per #214 ) worked and I could trace v4.15.0-rc1 without problems (see below).

I'll leave this here for someone official to close.

In any case, thanks for this amazing software! 🔝

Lean version: leanprover/lean4:v4.15.0-rc1

2024-12-11 11:14:06.981 | INFO     | lean_dojo.data_extraction.trace:get_traced_repo_path:210 - Tracing LeanGitRepo(url='https://github.com/leanprover-community/mathlib4', commit='41ff1f7899c971f91362710d4444e338b8acd644')
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision '8e5cb8d424df462f84997dd68af6f40e347c3e35'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient
info: LeanSearchClient: checking out revision 'd7caecce0d0f003fd5e9cce9a61f1dd6ba83142b'
info: importGraph: cloning https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision 'ed3b856bd8893ade75cafe13e8544d4c2660f377'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision '2b000e02d50394af68cfb4770a291113d94801b5'
info: aesop: cloning https://github.com/leanprover-community/aesop
info: aesop: checking out revision '8b6048aa0a4a4b6bcf83597802d8dee734e64b7e'
info: Qq: cloning https://github.com/leanprover-community/quote4
info: Qq: checking out revision 'ad942fdf0b15c38bface6acbb01d63855a2519ac'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision '7805acf1864ba1a2e359f86a8f092ccf1438ad83'
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision '0c8ea32a15a4f74143e4e1e107ba2c412adb90fd'
Build completed successfully.
100%|████████████████████████████████████████████████████████████████████████████████████████████████████████████████████▊| 6936/6944 [1:12:41<00:05,  1.38it/s]2024-12-11 12:59:31.583 | WARNING  | lean_dojo.data_extraction.trace:check_files:120 - Missing /tmp/tmpksck6zef/mathlib4/.lake/packages/importGraph/.lake/build/ir/ImportGraph/Cli.ast.json
2024-12-11 12:59:31.583 | WARNING  | lean_dojo.data_extraction.trace:check_files:120 - Missing /tmp/tmpksck6zef/mathlib4/.lake/packages/importGraph/.lake/build/ir/Main.ast.json
2024-12-11 12:59:31.583 | WARNING  | lean_dojo.data_extraction.trace:check_files:120 - Missing /tmp/tmpksck6zef/mathlib4/.lake/packages/importGraph/.lake/build/ir/Main.dep_paths
2024-12-11 12:59:31.583 | WARNING  | lean_dojo.data_extraction.trace:check_files:120 - Missing /tmp/tmpksck6zef/mathlib4/.lake/packages/importGraph/.lake/build/ir/ImportGraph.dep_paths
2024-12-11 12:59:31.583 | WARNING  | lean_dojo.data_extraction.trace:check_files:120 - Missing /tmp/tmpksck6zef/mathlib4/.lake/packages/importGraph/.lake/build/ir/ImportGraph.ast.json
2024-12-11 12:59:31.583 | WARNING  | lean_dojo.data_extraction.trace:check_files:120 - Missing /tmp/tmpksck6zef/mathlib4/.lake/packages/importGraph/.lake/build/ir/ImportGraph/Cli.dep_paths
Build completed successfully.
2024-12-11 12:59:35,469	INFO worker.py:1812 -- Started a local Ray instance. View the dashboard at http://127.0.0.1:8265 
100%|███████████████████████████████████████████████████████████████████████████████████████████████████████████████████████| 6939/6939 [06:52<00:00, 16.83it/s]
2024-12-11 13:06:58,481	INFO worker.py:1812 -- Started a local Ray instance. View the dashboard at http://127.0.0.1:8265 
100%|███████████████████████████████████████████████████████████████████████████████████████████████████████████████████████| 6939/6939 [02:12<00:00, 52.41it/s]
2024-12-11 13:09:49.415 | INFO     | lean_dojo.data_extraction.trace:trace:248 - Loading the traced repo from ~/.cache/lean_dojo/leanprover-community-mathlib4-41ff1f7899c971f91362710d4444e338b8acd644/mathlib4
2024-12-11 13:09:56,443	INFO worker.py:1812 -- Started a local Ray instance. View the dashboard at http://127.0.0.1:8265 
100%|███████████████████████████████████████████████████████████████████████████████████████████████████████████████████████| 6939/6939 [09:55<00:00, 11.66it/s]
@yangky11
Copy link
Member

Yes, it has been fixed in v2.2.0

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@oOo0oOo @yangky11