Fix known bugs related to dependency graph building
This pull request addresses the known bug that dependency graph does not contain external library files (e.g., Std).
This PR modifies ExtractData.lean to produce an improved version of .dep_paths files where all module paths are relative to the repo head, including those from external libraries.
For development purpose, this PR changed the "if" statement in the build_dependency_graph method to assertion. This PR currently keeps this modification, because we believe all the edges we are attempting to add should indeed be able to be added. We cannot think of a case that this "add-edge" can be expected to fail.
This PR has been tested by tracing the whole Mathlib4. Both Lean4-related .ipython notebooks are updated. Please refer to their contents for results.
Important: This PR generates a newer version of benchmark4, which calls to update the remote cache.
Fix known bugs related to dependency graph building
This pull request addresses the known bug that dependency graph does not contain external library files (e.g.,
Std).This PR modifies
ExtractData.leanto produce an improved version of.dep_pathsfiles where all module paths are relative to the repo head, including those from external libraries.For development purpose, this PR changed the "if" statement in the
build_dependency_graphmethod to assertion. This PR currently keeps this modification, because we believe all the edges we are attempting to add should indeed be able to be added. We cannot think of a case that this "add-edge" can be expected to fail.This PR has been tested by tracing the whole
Mathlib4. Both Lean4-related.ipythonnotebooks are updated. Please refer to their contents for results.Important: This PR generates a newer version of benchmark4, which calls to update the remote cache.