--export-graphml-deps error despite PR request for this feature approved

[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

[digama0]

It appears you did not check out the export_graphml_deps branch, instead you cloned metamath-knife into a directory named export_graphml_deps. Try git checkout export_graphml_deps instead.

The second line is also strange, why did you cd /Users/user/.cargo/git/checkouts/export_graphml_deps? You should not directly modify anything in the .cargo directory, that directory is maintained by cargo. Instead you should go into the cloned metamath-knife repo and run cargo build --release there.

[humanitiesclinic]

oh thank u

[humanitiesclinic]

oh but wait

[humanitiesclinic]

there's no export_graphml_deps branch. See: #112

A merge to the main branch, of 4 commits from a fork has been approved.

So shouldn't I just

git clone https://github.com/tirix/metamath-knife.git

Even when I did that, I still had the same error...

[digama0]

The bottom of the page has "command line instructions" for checking out the PR:

git checkout -b tirix-export_graphml_deps main
git pull https://github.com/tirix/metamath-knife.git export_graphml_deps

[humanitiesclinic]

I really apologise.. But I am utterly confused.. everything I tried is not working, including:

git checkout -b tirix-export_graphml_deps main
git pull https://github.com/tirix/metamath-knife.git export_graphml_deps

and there are so many confusing commands and concepts eg. branch, fork, checkout.. I am not a master in Git as well. I usually only clone repos, never worked with branches or forks.. Do u have a list of commands I can follow from start to end?

[digama0]

Delete the metamath-knife repo you have cloned. From your documents folder or wherever you would like to put this project:

# check out main repo to metamath-knife/ directory
git clone https://github.com/david-a-wheeler/metamath-knife.git
# enter metamath-knife/
cd metamath-knife
# create a new branch to track tirix's PR
git checkout -b tirix-export_graphml_deps main
# Pull the changes from the PR into your local branch
git pull https://github.com/tirix/metamath-knife.git export_graphml_deps
# Build and run
cargo run --release --features xml -- --export-graphml-deps out.gml path/to/set.mm

[tirix]

@digama0 thanks for stepping in and providing support.
@humanitiesclinic the steps listed by @digama0 are the correct ones and should work.

[humanitiesclinic]

greatly appreciate

[humanitiesclinic]

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?

(And do I need to open a new issue for this, since this is a different although related issue?)

[humanitiesclinic]

this is also on https://groups.google.com/g/metamath/c/Pc2z1qz38XE

[tirix]

dependencies between definitions are missing

Yes, this is not part of the export introduced in #112.
It is possible to add this function to metamath-knife, too. I could do that in a separated PR.

I believe syntax axiom dependencies should be a completely separated graph.

[humanitiesclinic]

ok appreciate it, will wait for it then..

[tirix]

Hence, each constant can be a node, and there can be an edge for each "used in the definition of" relation.

Rather than each constant to be a node, I believe each definitional axiom should be a node.
That is, instead of Grp depending on Mnd, the dependency would be between df-grp and df-mnd, whereas df-mnd itself relies on further definitions.

I think this makes more sense (e.g. we have a constant ( used in several different places, and it does not make sense to link those).

This requires the ability to identify definitions, so there is a interaction with #103 .

[digama0]

I think the most sensible version of this would involve not the constant symbols, or the definitions, but rather the syntax axioms, because you can take df-grp and parse it to get the list of all syntax axioms used in the definition on the RHS, and the syntax axiom for the defined notion on the LHS, which gives you the desired graph structure.

[tirix]

It was also my first thought to use syntax axioms, but then the graph obtained would only be one layer deep:
df-grp would depend on cgrp, just like df-subg (subgroup) and df-ghm (group homomorphism), but those would not depend on anything else in turn.

I thought a graph of definitions would probably make more sense: df-grp (Group) then depends of df-mnd (Monoid), which depends itself on df-sgrp (Semigroup), which depends on df-mgm (Magma), and so on. This is probably much more meaningful.

Actually @humanitiesclinic it depends what you need this for.

[humanitiesclinic]

@tirix yes I think the graph of definitions as mentioned in "I thought a graph of definitions would probably make more sense: df-grp (Group) then depends of df-mnd (Monoid), which depends itself on df-sgrp (Semigroup), which depends on df-mgm (Magma), and so on. This is probably much more meaningful." is the closest to look what I need..

[digama0]

It was also my first thought to use syntax axioms, but then the graph obtained would only be one layer deep:
df-grp would depend on cgrp, just like df-subg (subgroup) and df-ghm (group homomorphism), but those would not depend on anything else in turn.

The idea would be to use df-grp to inform the edges cgrp <- cmnd, cab, ... because the LHS of df-grp defines cgrp and the RHS uses cmnd, cab, .... By collecting up these edges over all the definitions you get a graph on the syntax axioms. You can also relabel the graph to use df-grp in place of cgrp everywhere (i.e. rewrite cgrp <- cmnd to df-grp <- df-mnd) but this breaks down when you have primitive syntax like cab.

[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:
#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..

[humanitiesclinic]

Here's the screenshot of error on Gephi

Here's the non-zipped version of the graphML file if you need it: https://file.io/TEBU1HreQNUo

[digama0]

looks like the file extension (which I guessed at) is .graphml not .gml. With that modification Gephi seems to accept it.

[humanitiesclinic]

oh ok

[humanitiesclinic]

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

[humanitiesclinic]

regarding, #113 (comment), because I am not fully clear about the technicalities regarding the difference between syntax axioms and definitions, I cannot comment.. as long as it is something like "I thought a graph of definitions would probably make more sense: df-grp (Group) then depends of df-mnd (Monoid), which depends itself on df-sgrp (Semigroup), which depends on df-mgm (Magma), and so on. This is probably much more meaningful.", it should probably be alright for me..

[humanitiesclinic]

hope that's ok..

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

[digama0]

Note that definitions are already topologically sorted in the MM file, since you can't introduce a notion until you have introduced all the things it relies on.

[humanitiesclinic]

oh no! thank you so much for pointing that out.. ;(;(

[humanitiesclinic]

but 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?

[humanitiesclinic]

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

[tirix]

First of all, if you are only interested in the interdependencies between algebraic and topological structures, there is a dedicated page for that, I suggest you take a look at it.
Most boxes and arrows are clickable, so you have a direct link with the database itself. That is probably a much better introduction if you're interested in Algebra.

I've posted my in-progress work in #116 . That version is far from final and has flows, but it actually outputs a graph for definitions.

These GraphML exports are probably most suitable for research, data mining kind of work, in order to build graphs like in @david-a-wheeler Gource video or Stephen Wolfram's book, and a lot of processing will be required to build teaching material out of it.

It might help if you explained better what you are teaching, at what level, and how you intend to use the data.

[tirix]

FYI here is the current output: def.graphml.gz.

[humanitiesclinic]

thank you very much.. I appreciate it very much...

[humanitiesclinic]

I'll have a look and get back

[humanitiesclinic]

@tirix sorry to inform that the def.graphml has this error:

while out.graphml is now ok

[tirix]

It looks like the file in my previous comment did not upload correctly.

This version works: def.graphml.gz

With Gephi's Force Atlas layout, nodes with a lot of edges are isolated, so we can see clearly how central df-fv, df-ov, df-mpt, df-mpt2, df-1 and df-base are:

[tirix]

@humanitiesclinic have you been able to use the data?
It would be nice if you could share the material you produced based on the graphs.

I'll close this issue if there is no more problem with the graphs.