MathlibExplorer icon indicating copy to clipboard operation
MathlibExplorer copied to clipboard

some feature advices

Open lhyundeadsoul opened this issue 1 year ago • 2 comments

  1. Search for nodes by name(en/ch)
  2. Provide an external link to the corresponding file in mathlib4
  3. highlight the most primary concept node e.g.(Algebra.Group.Baise/Ring/Field...)
  4. provide the shortest path navigation between two concept and highlight the nearest father node

lhyundeadsoul avatar May 31 '24 11:05 lhyundeadsoul

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.

Crispher avatar Jun 02 '24 09:06 Crispher

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"?

ekibun avatar Jan 17 '25 12:01 ekibun