Proof editing features

[digama0]

Right now metamath-exe never actually writes .mm files itself. This makes it difficult to implement things like save proof * /compressed or comment rewrapping, which is one of the essential functions of metamath-exe. Tools that generate proofs also want to be able to construct mm snippets, and whole file refactors like theorem renaming or inlining require editing a .mm file, not just generating one from scratch (if we want to minimize the diff). Metamath-knife is well positioned to do these things, and to some extent it was designed for this with "incremental mode" support, but there is still some work to be done to make it actually work and have a useful API.

[tirix]

So what kind of API do you have in mind? I'm thinking maybe:

• a set_proof API which would set the proof for a given (possibly previously incomplete) theorem
• an insert_scope / insert_statement API which would create a new scope or statement within a scope
• a save API to save the whole (modified) database

The save function by itself would already be useful e.g. for rewrapping.

The set_proof function could be used to provide e.g. minimized proofs.

Wouldn't the database modification API be problematic? I think metamath-knife is originally designed to work on files. It would be nice to have a different underlying data structure, like e.g. a rope, in order to support such partial modifications efficiently. This would also allow metamath-knife to handle both text change events from text editors (a nice feature for a VSCode plugin!), and also to internally handle changes from rewrapping, proof or comments modifications.

[digama0]

One option that would perform reasonably well would be a "delayed change" model, where you can queue up modifications and then call a function which applies them all at once. If these are statement-oriented change requests (like changing a comment body or replacing a proof) then they will all essentially be either disjoint or clobber each other, so you can just sort them all and rewrite the whole database top to bottom to apply everything. It also enables the "simple case" where you just want to apply a single change and don't care that it is costly to rewrite the whole chunk.

The main drawback of such a model is that you can't see the effect of a modification until you apply it. Cases where that will matter are mostly where you change the statement of a theorem in the middle of the database and want to see what breaks, and I'm okay with that not being so fast since there are a couple things you could do to approximate such a query without actually applying the change.

[tirix]

Maybe we could first add to database a "pending_changes" structure, which would allow to store a map of theorems and their new respective proofs.

Then upon saving, we check if the current theorem has such a proof, and write it instead of the statement's math_proof().

That feature might still be useful for an IDE integrated proof assistant, either as a manual action which would trigger a reload, or as an accessor which would pull the text changes to be done for these new proofs.