the reason why this needs to be done, is to avoid having to go through all the definitions before the so-called "target" node one wants to learn. say I wish to learn the definition df-grp.. it is the 400+th definition in set.mm... so it makes sense to isolate the subgraph on which it is dependent only, to avoid having to learn 400+ definitions first before reaching df-grp...
On Thursday, June 8, 2023 at 3:49:52 PM UTC+8 Humanities Clinic wrote: > also may I ask.. because there are 1000+ over definitions... and for some > definition node X, not every node that comes before it in a topological > sort is used to define node X.. it is therefore possible to isolate a > subgraph of only those nodes that node X is dependent on... do u have a > suggestion on how this can be done quickly, preferably on set.mm > directly? > > On Thursday, June 8, 2023 at 1:40:34 PM UTC+8 Humanities Clinic wrote: > >> *from the ground up >> >> On Thursday, June 8, 2023 at 1:38:57 PM UTC+8 Humanities Clinic wrote: >> >>> erm sorry to ask, but will it take long? because I need it for work and >>> teaching.. the definitions graph, when topologically sorted, can be used to >>> learn all definitions of objects from the group up.. >>> >>> On Wednesday, June 7, 2023 at 12:47:53 PM UTC+8 Humanities Clinic wrote: >>> >>>> Noted, may I know if the definitions graph have been added? I don't see >>>> any news yet.. >>>> >>>> On Wednesday, June 7, 2023 at 6:05:21 AM UTC+8 Thierry Arnoux wrote: >>>> >>>>> Yes, the PR has not been merged in yet, so until then you will need >>>>> check my branch out. >>>>> >>>>> >>>>> This feature required an "XML" library and I've kept it optional, so >>>>> you will only be able to access it if the program is compiled with the >>>>> "xml" feature, like so: >>>>> >>>>> cargo run --features xml -- ../set.mm/set.mm --time >>>>> --export-graphml-deps deps.graphml >>>>> >>>>> Or >>>>> >>>>> cargo build --features xml >>>>> >>>>> >>>>> Sorry, I should have mentioned that. >>>>> _ >>>>> Thierry >>>>> >>>>> >>>>> On 05/06/2023 14:17, 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/5d59c6af-a1e8-4a32-bfb1-85077310a17bn%40googlegroups.com >>>>> >>>>> <https://groups.google.com/d/msgid/metamath/5d59c6af-a1e8-4a32-bfb1-85077310a17bn%40googlegroups.com?utm_medium=email&utm_source=footer> >>>>> . >>>>> >>>>> -- 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/3eedc288-8f71-46cf-8c51-7e83b3efbc73n%40googlegroups.com.
