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/052cbdba-13ea-4ae4-a558-0d49253ef43cn%40googlegroups.com.
