It doesn't compile

[digama0]

I tried to compile it and the metamath_knife::diag::Notation type doesn't exist. Neither https://github.com/david-a-wheeler/metamath-knife nor https://github.com/tirix/metamath-knife contains a definition of this type, and the toml file here refers to your local copy of metamath-knife, which presumably has the required changes. Could you push those changes to https://github.com/tirix/metamath-knife for reproducibility?

(The reason I wanted to compile it was to see how others are using metamath-knife API to generate new theorems.)

[tirix]

Thanks for your interest!

I've pushed a commit to this directory which aligns it with changes in metamath-knife v0.3.6. That latest version should compile and run.

Here's how to run it:

• first change directory to the crate rumm (inside of the respository which is also called rumm),
• you need to have a version of set.mm in ../../set.mm/set.mm (that is, set.mm checked out is the same directory as rumm)
• you can then run the example from using cargo run.

The example dumps a lot of debug information, but basically just proves two theorems, a simple closure theorem rummex1 which is defined in examples/examples.mm and inftmrel from set.mm. You'll see the MMJ2 like proof for the second theorem at the end of the output, and the proof for the first theorem somewhere lost in the middle of the output, above the ====== line.

Look at the end of examples/set.rmm to see the tactics applied: the proof of rummex1 only consists in using one "real closure" tactics, while the proof of inftmrel involves using the definition of <<< and then applying a suitable substitution.

You can then look at the rest of set.rmm to see how those tactics are defined.

[tirix]

If you're interested to see how metamath-knife is used to build a proof, you can look at lang::proof_definition. If a tactics is successful, it basically returns a ProofStep enum, which includes either a hypothesis to simply refer to, or theorem to apply. The proof step enum is a tree-like recursive structure, i.e. it points itself to the sub-proofs that sub-tactics generated.

That file's as_proof_tree_array function generates the corresponding metamath-knife ProofTreeArray structure, which is used to export the proof in the MMP format using export_mmp_proof_tree.

[tirix]

@digama0 did you manage to run rumm? Can I close this issue?

[digama0]

Yes, it works now.