Add function to export theorem dependencies in GraphML format

[tirix]

As per discussion on the google groups:

This adds a new option --export-graphml-deps [FILE] (no shortcut), which allows to export the theorem dependencies in GraphML format. Requires to be compiled with the xml feature.

[GinoGiotto]

I don't have the competence to review, but I wanted to show my support for this. I think a graph database of theorems dependencies would be a really cool tool to play with. In 2022 Stephen Wolfram wrote an article with a visualization for set.mm https://writings.stephenwolfram.com/2022/03/the-physicalization-of-metamathematics-and-its-implications-for-the-foundations-of-mathematics/

Here is his graph:

Probably there are ways to make it prettier and less "chaotic", but at least this should give an idea of what it could look like.

[david-a-wheeler]

It's a different visualization, but Metamath Proof Explorer (set.mm) contributions visualized with Gource through 2020-04-29 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, but it may be of interest. I'll post to the mailing list too.

[humanitiesclinic]

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

For more information try --help

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

[humanitiesclinic]

I am not completely familiar with Rust and Cargo, please pardon me for this

[humanitiesclinic]

on a separate but relevant note, @tirix @digama0, 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: https://github.com/david-a-wheeler/metamath-knife/issues/113#issuecomment-1578063268

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

https://github.com/david-a-wheeler/metamath-knife/pull/1 /Users/user/Documents/graph/index.php(26): Graphp\GraphML\Loader->loadContents('/Users/user/Doc...') https://github.com/david-a-wheeler/metamath-knife/pull/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..

[humanitiesclinic]

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

[tirix]

I'll try to add it whenever I can find some free time, but it's hard to commit on a date.

[humanitiesclinic]

ok yes pls

[humanitiesclinic]

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

[jkingdon]

As @digama0 said on the mailing list:

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.

and I agree that having an xml feature seems like maybe an inelegant way of handling what would be better organized as multiple crates (not that I've looked at the code much, just based on the idea that we were hoping to design metamath-knife in a modular way which featured a core library with a bunch of other packages built on top of it).

[tirix]

Ok, so we have this PR pending, then #116, which depends on this, and also a proposal to split metamath-knife into two crates. I suggest we first merge this PR, then #116, then possibly release, and then do the split.

I agree that having an xml feature seems like maybe an inelegant way of handling what would be better organized as multiple crates

Yes, as a result of the split, the library crate will not depend on xml, and it will not need to be optional in the binary crate. And that's much better.

[jkingdon]

I suggest we first merge this PR, then #116, then possibly release, and then do the split.

I'd gladly defer to people more involved in metamath-knife development than I am, but sounds sensible to me.

[tirix]

I have started by merging #107 . This PR can come next, and then #116, then we can release and then refactor.

[digama0]

What do you mean by "release"?

[tirix]

What do you mean by "release"?

Last release was 0.3.6, I mean baseline a 0.3.7 for example.