MM Diff

[tirix]

@benjub asked in a thread:

how easy/useful would it be to have the CI check/warn if dependencies were added in any proof in an MR ? (by comparing the outputs of show trace xxx /axioms for all xxx modified by the PR) ?

I think generally it would be interesting to make a tool to check differences between two versions of a MM file and output useful information like:

• which theorems were changed
• which comments were changed
• are the changes in the Mathboxes?
• axiom usage change, etc.

I don't think any existing tool provides this kind of functionality. git diff provides the lines changed, so its output could be used as an input for computing these changes. And git diff can be run within a GitHub action to get the changes in the current PR.

My question is: should this functionality be built-in in metamath-knife, or should we consider a new mm-diff tool based on metamath-knife?

[david-a-wheeler]

My two cents:

I would like the Metamath-knife program to be a general-purpose library callable by others, and a general-purpose CLI tool that can be told to do arbitrary things. So I guess I'd prefer that it be built into metamath-knife as an option, but the library part should do all the actual work.

[tirix]

That would make metamath-knife look more like metamath-exe.

There are rust libraries which can help write such CLI, like console and dialoguer.

If we prefer to keep metamath-knife as a library only, there seems to be rust-script which allows to run rust code just like a script.

[digama0]

I agree with @tirix , I think there should be some separation between the library and the CLI, even if both are hosted in this repo. Ideally the library should be designed so that the CLI is easy to implement, but the library shouldn't commit to any particular user interface choices.

[tirix]

I'm thinking maybe we could structure the command-line parameters in this way: A set of parameters to define a list of input theorems:

• * for all theorems, or a glob for matching certain names,
• or a list of theorems, either in the command line, or from a file,
• or a list of theorems changed, from a diff file,
• maybe options to include/exclude mathboxes, etc.

A set of parameters to define what to do with those theorems:

• just display the list of theorem names,
• display the statements,
• export the corresponding proofs, in MMP format (or JSON c.f other discussions),
• list their axiom dependencies