> > > On 04/06/2023 15:14, Humanities Clinic 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.
> On Jun 4, 2023, at 4:11 PM, Thierry Arnoux <[email protected]> wrote: > I've quickly written an extension to metamath-knife which generates a GraphML > file with all theorem dependencies. You can find the PR here: > https://github.com/david-a-wheeler/metamath-knife/pull/112 > It adds an option "export-graphml-deps", so that the tool can be called using: > metamath-knife set.mm --time --export-graphml-deps deps.xml > which generates a "deps.xml" GraphML file. > The file generated using the current version of set.mm is around 60Mb, > includes 43922 nodes and 1324402 edges. Thierry: Thanks so much! That looks really helpful. Clearly what's needed now is something that can read a GraphML file and provide the UI desired. I don't know what tools can do that, but I did a quick search and found information about GraphML viewers. These links might be helpful.: * yWorks' yEd tools - https://www.yworks.com/products/graphmlviewer#editors * Gephi - https://github.com/gephi/gephi * https://stackoverflow.com/questions/30928008/view-graphml-file (you can use graphviz) * https://en.wikipedia.org/wiki/GraphML If you have a tool with the interface desired, but requires a different input format, I imagine it shouldn't be hard to convert GraphML into what you need. --- 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/873B9FC5-AFAB-46ED-A0A9-3E6FA30AC39B%40dwheeler.com.
