Is set.mm available in a more "graph-parseable" format other than in html or .mm, and/or what is the easiest way to perform graph-related operations on the set.mm dataset?

[Humanities Clinic]

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 am using macOS10.13.6.

May I know, is there any program already written for Metamath that can do this? Otherwise, what would be the fastest/easiest way to achieve the goals I outlined?

[Thierry Arnoux]

Hi,

I've quickly written an extension to metamath-knife which generates a GraphML file with all theorem dependencies. You can find the PR here:

https://github.com/david-a-wheeler/metamath-knife/pull/112

It adds an option "export-graphml-deps", so that the tool can be called using:

    metamath-knife set.mm --time --export-graphml-deps deps.xml

which generates a "deps.xml" GraphML file.

The file generated using the current version of set.mm is around 60Mb, includes 43922 nodes and 1324402 edges.

BR,
_
Thierry

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/acaf60be-aad3-4e11-9eb4-ecd92479f304n%40googlegroups.com.

[David A. Wheeler]

>
>
> On 04/06/2023 15:14, Humanities Clinic 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.

> On Jun 4, 2023, at 4:11 PM, Thierry Arnoux <thierry...@gmx.net> wrote:
> I've quickly written an extension to metamath-knife which generates a GraphML file with all theorem dependencies. You can find the PR here:
> https://github.com/david-a-wheeler/metamath-knife/pull/112
> It adds an option "export-graphml-deps", so that the tool can be called using:
> metamath-knife set.mm --time --export-graphml-deps deps.xml
> which generates a "deps.xml" GraphML file.
> The file generated using the current version of set.mm is around 60Mb, includes 43922 nodes and 1324402 edges.

Thierry: Thanks so much! That looks really helpful.

Clearly what's needed now is something that can read a GraphML file and provide the UI desired.
I don't know what tools can do that, but I did a quick search and found information about GraphML viewers.
These links might be helpful.:
* yWorks' yEd tools - https://www.yworks.com/products/graphmlviewer#editors
* Gephi - https://github.com/gephi/gephi
* https://stackoverflow.com/questions/30928008/view-graphml-file (you can use graphviz)
* https://en.wikipedia.org/wiki/GraphML

If you have a tool with the interface desired, but requires a different input format,
I imagine it shouldn't be hard to convert GraphML into what you need.

--- David A. Wheeler

[David A. Wheeler]

> On Jun 4, 2023, at 9:14 AM, Humanities Clinic <humaniti...@gmail.com> 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

[Humanities Clinic]

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

[Humanities Clinic]

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

[Humanities Clinic]

Hi Thierry,

Is there an issue with this, or did I do anything wrong?

[Humanities Clinic]

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?

[David A. Wheeler]

> On Jun 6, 2023, at 7:33 AM, Humanities Clinic <humaniti...@gmail.com> wrote:
>
> 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?

I'm sure metamath-knife could be modified to do that.

Another approach, though a little painful, is that you could scrape the generated HTML about set.mm to get this information.

I don't remember if metamath-exe has an option to list the constants in use (other than when generating the HTML). It obviously *has* that information internally.

--- David A. Wheeler

[Humanities Clinic]

On a separate but relevant note, Thierry, sorry to inform that I seem to have a problem with the current GraphML output. Pls see the attached output which is exactly what I got when I ran the commands in:
#113 (comment)

out.gml.zip

On Gephi, I have a Invalid GML Parsing error.

On GraPhP with PHP (https://github.com/graphp/graph), I am having the following error:
Fatal error: Uncaught Exception: String could not be parsed as XML in /Users/user/Documents/graph/vendor/graphp/graphml/src/Loader.php:13
Stack trace:
#0 /Users/user/Documents/graph/vendor/graphp/graphml/src/Loader.php(13): SimpleXMLElement->__construct('/Users/user/Doc...')
#1 /Users/user/Documents/graph/index.php(26): Graphp\GraphML\Loader->loadContents('/Users/user/Doc...')
#2 {main}
thrown in /Users/user/Documents/graph/vendor/graphp/graphml/src/Loader.php on line 13

It appears that the GraphML output is not well-formed, but I dun have enough knowledge now to check manually what is the exact problem.

Hopefully, you can fix this problem while you add the feature for the definitions dependency graph..

[Thierry Arnoux]

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

--
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 metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/5d59c6af-a1e8-4a32-bfb1-85077310a17bn%40googlegroups.com.

[Humanities Clinic]

Noted, may I know if the definitions graph have been added? I don't see any news yet..

[Humanities Clinic]

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..

[Humanities Clinic]

*from the ground up

[Humanities Clinic]

also may I ask.. because there are 1000+ over definitions... and for some definition node X, not every node that comes before it in a topological sort is used to define node X.. it is therefore possible to isolate a subgraph of only those nodes that node X is dependent on... do u have a suggestion on how this can be done quickly, preferably on set.mm directly? 

[Humanities Clinic]

the reason why this needs to be done, is to avoid having to go through all the definitions before the so-called "target" node one wants to learn. say I wish to learn the definition df-grp.. it is the 400+th definition in set.mm... so it makes sense to isolate the subgraph on which it is dependent only, to avoid having to learn 400+ definitions first before reaching df-grp...

[Igor Ieskov]

Hi Humanities Clinic,

If you want to manually browse definitions in set.mm, you may try metamath-lamp tool. Currently, its latest version doesn't have such possibility, but its "development" version does have.

latest version (no possibility to browse definitions at the moment) - https://expln.github.io/lamp/latest/index.html

"development" version (allows to browse definitions but may be less stable than the latest version) - https://expln.github.io/lamp/dev/index.html

Here is a short video instruction how to browse definitions (no sound) - https://drive.google.com/file/d/1toV3EUwDm6ijPeLhxeqjwaNmNWr9ilUk/view?usp=sharing

If you want to learn more about metamath-lamp and set.mm related topics you may read this guide written by David A. Wheeler - https://lamp-guide.metamath.org

Please note, both the tool and the guide are being actively developed at the moment. So you may see some inconsistencies between them.

-
Igor

[David A. Wheeler]

> On Jun 5, 2023, at 8:48 AM, Thierry Arnoux <thierry...@gmx.net> 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

I appreciate making it optional.

Can you make it so the *default* is to include it, and then optionally exclude it?
That way, people can use options to build it for special purposes, but the
"out of the box" functionality has whatever people might like?

--- David A. Wheeler

[Mario Carneiro]

I am actually a bit concerned at the growth in behaviors of what is ostensibly a library. We need better separation between the proof assistant and the library, possibly a second crate in the same repo.

--
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 metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/03E6D2BE-FC76-4663-A563-9BE08D9DF2A1%40dwheeler.com.

[Thierry Arnoux]

Yes this feature is quite far away from a core functionality.

The `metamath-knife` crate is actually both the library and a command-line tool.

What do you have in mind here?

- still keeping both library and command-line together, but moving some functionality (like graph exports) to another command-line crate,

- or splitting library and command-line tool, with the graph export functionality moving to the command-line tool part?

_
Thierry

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSu4TttF50YBYg%3D1x5vwKde6vUcTm1BFLDb%3D_RUU0pxshA%40mail.gmail.com.

[Mario Carneiro]

I was thinking of the latter: have two crates, one for the library and one for the executable, and put assorted functionality in the command line tool and keep the library focused to things that make it easy to write the CLI and are metamath-related.