Thank you for this. Is it me, or is there something not quite right with
the new PR. I keep on getting the error:
*error:* Found argument '--export-graphml-deps' which wasn't expected, or
isn't valid in this context
Did you mean --export?
USAGE:
metamath-knife <DATABASE> --export <LABEL>... --time
For more information try --help
On Monday, June 5, 2023 at 7:47:29 AM UTC+8 David A. Wheeler wrote:
>
> > On Jun 4, 2023, at 9:14 AM, Humanities Clinic <[email protected]>
> wrote:
> >
> > I am stating more specifically the goals I have in mind when I asked:
> https://groups.google.com/d/msgid/metamath/CAFXXJSvQt6D6xoufTE5%2BbvyKmfUVN0R0AZK0Ch_7qfLbR95Duw%40mail.gmail.com?utm_medium=email&utm_source=footer
> >
> > I need to explore the "graph" of statements in set.mm. Specifically, I
> need to (1) find all sinks and sources quickly (2) Isolate one
> walk/path/trail between two specified nodes (3a) MOST IMPORTANTLY: With
> arrow keys on the keyboard, navigate between adjacent nodes. Up arrow - for
> the parent of the node. Down arrow - for the child of the node. Left and
> right arrows - for the siblings of the node (3b) I need to explore the
> subgraph of (only) all definitions in the way outlined in (3a), so I need
> to be able isolate this subgraph from the entire graph.
>
> I think building on Thierry's code will get you there.
>
> It's a different visualization, but you might also be interested in my
> video "Metamath Proof Explorer (set.mm) contributions visualized with
> Gource through 2020-04-29" at <https://www.youtube.com/watch?v=LVGSeDjWzUo
> >.
>
> This video shows the set.mm database's structure and growth over time.
> Each little circle represents an assertion (mostly theorems). It's
> structured by section and subsection, not by internal theorem dependencies.
> Even so, it may be of interest to you. The code to generate this is all
> publicly available.
>
> --- David A. Wheeler
>
>
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/e51ecae9-f02b-49d5-99af-c0f2f90b4944n%40googlegroups.com.
