*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/acb95c47-cefe-4cfa-86ed-5c524d064cc9n%40googlegroups.com.
