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 <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 <http://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 <http://set.mm>) contributions visualized with Gource through 2020-04-29" at <https://www.youtube.com/watch?v=LVGSeDjWzUo>. This video shows the set.mm <http://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/f6a0a5a9-8ba0-c5f9-524d-1db55ef47882%40gmx.net.
