Repository navigation
some feature advices #1
Description
- Search for nodes by name(en/ch)
- Provide an external link to the corresponding file in mathlib4
- highlight the most primary concept node e.g.(Algebra.Group.Baise/Ring/Field...)
- provide the shortest path navigation between two concept and highlight the nearest father node
Activity
Crispher commentedon Jun 2, 2024
Thanks for the suggestions, but I don't have time for them recently.
For (3), I actually did try it by hardcoding. It turns out that there are more "Basic" nodes than I thought. They don't seem to carry that much meaning.
ekibun commentedon Jan 17, 2025
I have implemented a new web explorer with a newer build of mathlib4.
In the recently build of mathlib4, almost all the nodes have a common parent Mathlib/Tactic/Linter/Header, and make it extremely large. To avoid this, i change the size to relate to the decl_count and the "Basic" nodes got a relative large weight. I am new to the mathlib4, are they the "primary concept nodes"?