Buggy output of --dump-formula

[GinoGiotto]

I'm using the demo0.mm example of the set.mm repository.

If I write:

> metamath-knife demo0.mm --dump-formula

The output is:

0 diagnostics issued.
Formula Dump:
maj: |- ( P -> Q )
min: |- P
th1: |- t = t

Which looks incomplete: min and maj are hypotheses of mp, but that's not printed, also a1 and a2 are not printed as well. I'm guessing that it was originally designed to not print $a statements, overlooking the fact that corresponding $e statements should be hidden as well.

Proposal: I would print axioms, group hypotheses with their corresponding statements and visualize their keywords, like this:

0 diagnostics issued.
Formula Dump:

a1 $a: |- ( t = r -> ( t = s -> r = s ) )

a2 $a: |- ( t + 0 ) = t

maj $e: |- ( P -> Q )
min $e: |- P
mp $a: |- Q

th1 $p: |- t = t

This makes the output more clear and easier to read.

The remaining statements of demo0.mm are wff and term types. I think it's ok to not print those.

Personal note: I used to work with matamath-exe to print lists of statements, but it's quite slow. Unfortunately the metamath-knife version is quite slow as well because it prints the list of statements on the command line, so I have to wait the program to display the whole database, which takes a while (also I have difficulties extracting information from the command line display). It would be so much better if the list would be written in a file instead, the same way axiom usage metamath-knife set.mm --axiom-use ax.txt is implemented.

[digama0]

Personal note: I used to work with matamath-exe to print lists of statements, but it's quite slow. Unfortunately the metamath-knife version is quite slow as well because it prints the list of statements on the command line, so I have to wait the program to display the whole database, which takes a while (also I have difficulties extracting information from the command line display). It would be so much better if the list would be written in a file instead, the same way axiom usage metamath-knife set.mm --axiom-use ax.txt is implemented.

Note: Metamath-knife is first and foremost a library. That is, the intended way for users to perform complex activities is by writing code, in this project or a dependent. While it has a rudimentary CLI, it is not designed for complex interaction loops, and if you are calling it hundreds or thousands of times in a script you're doing it wrong. The library interface is fairly convenient and can be used to get really high performance programs; an example of doing complex display and analysis on metamath databases is mm-web-rs. IMO implementing all these little scripts as additional flags in metamath-knife is not long-term sustainable, or at least it will result in the code getting large and haphazard like the project it's trying to replace.

It would be so much better if the list would be written in a file instead, the same way axiom usage metamath-knife set.mm --axiom-use ax.txt is implemented.

There should not be a significant performance difference between printing to stdout and printing to a file, as long as you don't actually send stdout to the console. Just pipe it to disk as in metamath-knife > dump.log and it should run a lot faster.

[GinoGiotto]

There should not be a significant performance difference between printing to stdout and printing to a file, as long as you don't actually send stdout to the console. Just pipe it to disk as in metamath-knife > dump.log and it should run a lot faster.

Ah right, I haven't thought about that. I tried this way and it takes a few seconds, so it's good.

Note: Metamath-knife is first and foremost a library. That is, the intended way for users to perform complex activities is by writing code, in this project or a dependent.

The readme file only mentions the CLI interface (and doesn't even call it a library), perhaps this could be specified.

About the output of --dump-formula what do you think about my proposed visualization?

[tirix]

To explain the speed: The option --dump-formula was intended as a test for the database grammar parser. The idea was to parse the statement into a Formula AST tree, then dump the tree back to a string of tokens, so it can be reviewed.

If the goal is to quickly dump all formulas, there are more efficient ways, without switching to the tree structure and back.

In the mean time I've added a better check, in the form of the --verify-parse-stmt option, which does the same operation on all statements, automatically checks that they match the original math token string, and outputs any issue.

The readme file only mentions the CLI interface (and doesn't even call it a library), perhaps this could be specified.

For reference, this is the issue #117... still open!

[GinoGiotto]

To explain the speed: The option --dump-formula was intended as a test for the database grammar parser. The idea was to parse the statement into a Formula AST tree, then dump the tree back to a string of tokens, so it can be reviewed.

Ok, so this is not what I thought it was. I thought this was the equivalent of MM> SHOW STATEMENT * in meramath-exe and I was thinking with that paradigm in mind. But even if this was meant as a test for the grammar parser shouldn't it print $a statements anyway? Are we not interested in checking the correctness of those as well?

If the goal is to quickly dump all formulas, there are more efficient ways, without switching to the tree structure and back.

Can you name one? This is useful for something I'm working on, but at the moment I only know how to do it with metamath-exe, which is slow (it's slow even using the trick of printing the output directly on a file instead of the command line).

In the mean time I've added a better check, in the form of the --verify-parse-stmt option, which does the same operation on all statements, automatically checks that they match the original math token string, and outputs any issue.

Indeed. I saw that option and by reading the help section I assumed this one was for an other purpose (for --dump-formula the help option simply says "Dumps the formulas of this database").

Given the fact that a better tool is implemented, and given the fact that --dump-formula is not supposed to be used to just dump all formulas, is this command simply redundant now? It doesn't have any advantage compared to any other tool?

The readme file only mentions the CLI interface (and doesn't even call it a library), perhaps this could be specified.

For reference, this is the issue #117... still open!

Does exist somewhere a list of all library features of metamath-knife? For metamath-exe there is a lot of documentation which is well explained, so with time I gained a somewhat decent confidence with the tool. But here I'm not really sure where to start, as I can't find some help documentation about the library interface. I feel the only thing I should do would be to learn rust and read the code by myself, which is something I was contemplating doing.

[tirix]

If the goal is to quickly dump all formulas, there are more efficient ways, without switching to the tree structure and back.

Can you name one?

I was thinking about the way a simple Rust executable would use metamath-knife as a library and list all statements... I can quickly write one, but I might not have the time for that until this weekend.

Does exist somewhere a list of all library features of metamath-knife?

You can obtain the doc by launching:

cargo doc --lib --no-deps

From the directory where you checked out metamath-knife.

Then you can browse your own computer somewhere like: file:///Users/Gino/metamath-knife/target/doc/metamath_knife/index.html (needs to be fixed for your actual path)

Because metamath-knife is not an official crate yet, its doc is not on the web yet, otherwise it would be on https://docs.rs/. And my understanding is that we prefer not to make it a crate until it is properly split into a command line tool and a library, that is, until #117 is resolved.

[GinoGiotto]

You can obtain the doc by launching:

cargo doc --lib --no-deps

Thanks! It works, only a thing:

On the README.md I read:

We actively work to eliminate compiler warnings. This tends to counter errors, make the code more readable, and improve performance (e.g., by eliminating unnecessary clone() calls).

But when I execute cargo doc --lib --no-deps these warnings appear:

warning: unresolved link to `StartMathMode`
  --> src\comment_parser.rs:38:19
   |
38 |     /// Between [`StartMathMode`] and [`EndMathMode`],
   |                   ^^^^^^^^^^^^^ no item named `StartMathMode` in scope
   |
   = help: to escape `[` and `]` characters, add '\' before them like `\[` or `\]`
   = note: `#[warn(rustdoc::broken_intra_doc_links)]` on by default

warning: unresolved link to `EndMathMode`
  --> src\comment_parser.rs:38:41
   |
38 |     /// Between [`StartMathMode`] and [`EndMathMode`],
   |                                         ^^^^^^^^^^^ no item named `EndMathMode` in scope
   |
   = help: to escape `[` and `]` characters, add '\' before them like `\[` or `\]`

warning: unresolved link to `MathToken`
  --> src\comment_parser.rs:39:53
   |
39 |     /// there will be no comment items other than [`MathToken`].
   |                                                     ^^^^^^^^^ no item named `MathToken` in scope
   |
   = help: to escape `[` and `]` characters, add '\' before them like `\[` or `\]`

warning: unresolved link to `StartMathMode`
  --> src\comment_parser.rs:42:19
   |
42 |     /// Between [`StartMathMode`] and [`EndMathMode`],
   |                   ^^^^^^^^^^^^^ no item named `StartMathMode` in scope
   |
   = help: to escape `[` and `]` characters, add '\' before them like `\[` or `\]`

warning: unresolved link to `EndMathMode`
  --> src\comment_parser.rs:42:41
   |
42 |     /// Between [`StartMathMode`] and [`EndMathMode`],
   |                                         ^^^^^^^^^^^ no item named `EndMathMode` in scope
   |
   = help: to escape `[` and `]` characters, add '\' before them like `\[` or `\]`

warning: unresolved link to `MathToken`
  --> src\comment_parser.rs:43:53
   |
43 |     /// there will be no comment items other than [`MathToken`].
   |                                                     ^^^^^^^^^ no item named `MathToken` in scope
   |
   = help: to escape `[` and `]` characters, add '\' before them like `\[` or `\]`

warning: unresolved link to `Database::usage_pass`
   --> src\database.rs:645:29
    |
645 |     /// Returns `None` if [`Database::usage_pass`] was not previously called.
    |                             ^^^^^^^^^^^^^^^^^^^^ the struct `Database` has no field or associated item named `usage_pass`

warning: unresolved link to `TypesettingData::html_bibliography`
   --> src\verify_markup.rs:524:7
    |
524 | /// [`TypesettingData::html_bibliography`],
    |       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ no item named `TypesettingData` in scope

warning: unresolved link to `TypesettingData::ext_html_label`
   --> src\verify_markup.rs:525:34
    |
525 | /// while references after the [`TypesettingData::ext_html_label`] go to the
    |                                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ no item named `TypesettingData` in scope

warning: unresolved link to `TypesettingData::ext_html_bibliography`
   --> src\verify_markup.rs:526:7
    |
526 | /// [`TypesettingData::ext_html_bibliography`].
    |       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ no item named `TypesettingData` in scope

warning: `metamath-knife` (lib doc) generated 10 warnings
    Finished dev [optimized + debuginfo] target(s) in 3m 04s

Should I report them in a separate issue? Or we don't need to worry about these?

I was thinking about the way a simple Rust executable would use metamath-knife as a library and list all statements... I can quickly write one, but I might not have the time for that until this weekend.

That would be nice! However I don't want to assign work, so if you don't have time I'll figure something myself at some point :-)

[tirix]

Should I report them in a separate issue? Or we don't need to worry about these?

Yes, we should fix those in order to have the correct hyperlinks in the docs. A separate issue would be nice. Actually a CI check to ensure this does not happen again would be ideal.

[GinoGiotto]

Getting back to the topic of this issue, what I understand is:

• --dump-formula is not designed to show statements of a database.
• The actual purpose of this command has been reimplemented in --verify-parse-stmt making this one deprecated.

Therefore there probably aren't many compelling reasons to update the output with my proposal, however I still have the question if $a statements should be showed (it still looks weird to me that $e statements of a rule of inference are printed without the actual statement of that rule of inference).

Unless the plan is to remove it and there is no need to fix anything.

[tirix]

I was thinking about the way a simple Rust executable would use metamath-knife as a library and list all statements...

That would be nice!

I've published it under #150, though it's yet another option for the command line tool.

I still have the question if $a statements should be showed

Actually axioms are showed (at least, some are), what's not shown are syntactic axioms, as they are explicitly skipped here. It should be easy to add them back in, let's continue to track this with this issue.

[GinoGiotto]

Actually axioms are showed (at least, some are), what's not shown are syntactic axioms, as they are explicitly skipped here. It should be easy to add them back in, let's continue to track this with this issue.

Strange, indeed I checked with set.mm and turnstile axioms are showed (even if statements are not showed in the conventional order). So the reason why turnstile axioms are not showed for demo0.mm is getting more puzzling. I even tried to edit the label names of a1 a2 and mp into ax-1 ax-2 and ax-mp to see if there was some hard coded naming issue there, but they are still not showed in the output of --dump-formula. I'm guessing this is a true bug then.

[tirix]

With #153 all axioms are shown, including a1, a2 and mp.

The reason they were not shown was that that database is missing the $j syntax '|-' as 'wff' command which helps the grammar make the difference between formal axioms (typed as the declared |-) and syntactic axioms (the rest). All axioms were considered syntactic.

The output is still not organized, but with the independent --list-statements command, I don't think it's worth improving on that.

[GinoGiotto]

The reason they were not shown was that that database is missing the $j syntax '|-' as 'wff' command which helps the grammar make the difference between formal axioms (typed as the declared |-) and syntactic axioms (the rest). All axioms were considered syntactic.

I understand now, therefore #153 is a valid fix.

The output is still not organized, but with the independent --list-statements command, I don't think it's worth improving on that.

I agree, if --dump-formula is just used for testing there is no need to do that.