With assistance on the Github repo page itself, I was able to solve the
problem, appreciated it.
I have found that both on the web pages of MPE and on the GraphML output
from running, metamath-knife set.mm --time --export-graphml-deps deps.xml,
dependencies between definitions are missing.
For example, df-grp is defined in terms of the following constants:
Mnd
Base
`
+g
0g
(And all other "primitive" constants" like { A. ...)
Hence, each constant can be a node, and there can be an edge for each "used
in the definition of" relation.
Can this sort of graph be extracted from set.mm using metamath-knife, or be
obtained by any other means?
On Tuesday, June 6, 2023 at 1:07:43 PM UTC+8 Humanities Clinic wrote:
> 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/d22cc1fc-3e09-49ba-8a3a-1149030766e5n%40googlegroups.com.
