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/10c74eb1-c0c4-400c-b964-cc304b7996ean%40googlegroups.com.
