On a separate but relevant note, Thierry, sorry to inform that I seem to have a problem with the current GraphML output. Pls see the attached output which is exactly what I got when I ran the commands in: #113 (comment) <https://github.com/david-a-wheeler/metamath-knife/issues/113#issuecomment-1578063268>
out.gml.zip <https://github.com/david-a-wheeler/metamath-knife/files/11667837/out.gml.zip> On Gephi, I have a Invalid GML Parsing error. On GraPhP with PHP (https://github.com/graphp/graph), I am having the following error: Fatal error: Uncaught Exception: String could not be parsed as XML in /Users/user/Documents/graph/vendor/graphp/graphml/src/Loader.php:13 Stack trace: #0 /Users/user/Documents/graph/vendor/graphp/graphml/src/Loader.php(13): SimpleXMLElement->__construct('/Users/user/Doc...') #1 <https://github.com/david-a-wheeler/metamath-knife/pull/1> /Users/user/Documents/graph/index.php(26): Graphp\GraphML\Loader->loadContents('/Users/user/Doc...') #2 <https://github.com/david-a-wheeler/metamath-knife/pull/2> {main} thrown in /Users/user/Documents/graph/vendor/graphp/graphml/src/Loader.php on line 13 It appears that the GraphML output is not well-formed, but I dun have enough knowledge now to check manually what is the exact problem. Hopefully, you can fix this problem while you add the feature for the definitions dependency graph.. On Tuesday, June 6, 2023 at 7:33:46 PM UTC+8 Humanities Clinic wrote: > With assistance on the Github repo page itself, I was able to solve the > problem, appreciated it. > > I have found that both on the web pages of MPE and on the GraphML output > from running, metamath-knife set.mm --time --export-graphml-deps > deps.xml, dependencies between definitions are missing. > > For example, df-grp is defined in terms of the following constants: > Mnd > Base > ` > +g > 0g > (And all other "primitive" constants" like { A. ...) > > Hence, each constant can be a node, and there can be an edge for each > "used in the definition of" relation. > > Can this sort of graph be extracted from set.mm using metamath-knife, or > be obtained by any other means? > > On Tuesday, June 6, 2023 at 1:07:43 PM UTC+8 Humanities Clinic wrote: > >> Hi Thierry, >> >> Is there an issue with this, or did I do anything wrong? >> >> On Monday, June 5, 2023 at 8:17:51 PM UTC+8 Humanities Clinic wrote: >> >>> I even tried downloading the specific fork/branch directly, and still >>> have the same problem: >>> >>> git clone https://github.com/tirix/metamath-knife.git >>> export_graphml_deps >>> >>> Cloning into 'export_graphml_deps'... >>> >>> remote: Enumerating objects: 2377, done. >>> >>> remote: Counting objects: 100% (645/645), done. >>> >>> remote: Compressing objects: 100% (175/175), done. >>> >>> remote: Total 2377 (delta 523), reused 526 (delta 466), pack-reused 1732 >>> >>> Receiving objects: 100% (2377/2377), 20.79 MiB | 6.67 MiB/s, done. >>> >>> Resolving deltas: 100% (1704/1704), done. >>> >>> Users-MacBook-Pro-5:checkouts user$ cd >>> /Users/user/.cargo/git/checkouts/export_graphml_deps >>> >>> Users-MacBook-Pro-5:export_graphml_deps user$ cargo build --release >>> >>> >>> >>> >>> >>> On Monday, June 5, 2023 at 8:15:51 PM UTC+8 Humanities Clinic wrote: >>> >>>> 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/b989b6d0-0a9f-462b-9f61-1f42c1e1bec5n%40googlegroups.com.
