Trouble shooting: dep_path not relative to repo head in annotated tactics

[Peiyang-Song]

This pull request fixes the bug that some dep_path outputs from annotated tactics were not relative to the repo folder.

• This PR mainly modifies traced_data.py to post-process dep_path information. This was done by two main functions, find_absolute_path and find_relative_path, functionalities described in corresponding docstrings. A slight optimization is added to this part as well, shortcutting for the special case that the partial path head is itself a direct child of the repo folder.

• This PR has been tested with generate-benchmark-lean4.ipynb. Please refer to the last line of code which prints out annotated tactic outputs.

[Peiyang-Song]

PR updated

Switched to an alternative approach: getting desired dep_path outputs from processing the dependency graph.

• This PR implements two approaches for graph traversal: the second latest commit c156443 is a DFS-fashion solution while the latest commit d25b1c2 does BFS.

• Observing a slight improvement by using BFS, this PR ends up keeping the BFS version as the last commit, but feel free the check out the past commit and try DFS for some cases. Which one works better really depends on what the repo dependencies look like and accordingly the graph built from that.

• Major changes are in traced_data.py. See resulted features in generate-benchmark-lean4.ipynb.

[yangky11]

merge to dev