Hi Humanities Clinic, If you want to manually browse definitions in set.mm, you may try metamath-lamp tool. Currently, its latest version doesn't have such possibility, but its "development" version does have.
latest version (no possibility to browse definitions at the moment) - https://expln.github.io/lamp/latest/index.html "development" version (allows to browse definitions but may be less stable than the latest version) - https://expln.github.io/lamp/dev/index.html Here is a short video instruction how to browse definitions (no sound) - https://drive.google.com/file/d/1toV3EUwDm6ijPeLhxeqjwaNmNWr9ilUk/view?usp=sharing If you want to learn more about metamath-lamp and set.mm related topics you may read this guide written by David A. Wheeler - https://lamp-guide.metamath.org Please note, both the tool and the guide are being actively developed at the moment. So you may see some inconsistencies between them. - Igor On Thursday, June 8, 2023 at 9:50:07 AM UTC+2 Humanities Clinic wrote: > 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/974acede-7c1d-4c29-814e-0e321173bd6en%40googlegroups.com.
