Proof API

[sorear]

There's a broad consensus that we want something sort of like a parsed representation of an MMJ2 worksheet. The details need to be worked out, probably in connection with smm-webui work to use the API for proof visualization and editing.

[sorear]

I think that this is the riskiest part remaining, in terms of how much has yet to be designed and the fact that it'll require scopeck to stop pretending that its only client is verify. @digama0 I think you expressed an interest in this area?

[digama0]

Here's a plan for IDE integration:

Introduce a new file format for single proofs (essentially the same idea as .mmp files). Such a file will contain a reference to the root .mm file and the target theorem label in the header, and undergoes verification by smm3, which will produce a list of errors if validated with --verify. If it passes muster, it can also be validated with --import, which will take the proof and splice it into the .mm file, replacing the existing theorem. This should give a sufficient suite of tools for an IDE to be able to pop out proofs as needed.

smetamath set.mm --export 2p2e4  # Create a stub proof file for 2p2e4, equivalent to mmj2 ctrl-g 2p2e4
smetamath set.mm --verify 2p2e4  # Verify the proof file, producing a list of errors that can be highlighted by IDE, equivalent to mmj2 ctrl-u
smetamath set.mm --import 2p2e4  # Verify the proof file and write the proof to set.mm, equivalent to MM-PA save new_proof

[digama0]

A relevant proposal for this is https://groups.google.com/d/msg/metamath/ZlRle52FVO0/94ZTXaAfCQAJ.

[digama0]

@sorear I have written a new proof assistant proposal at https://groups.google.com/d/msg/metamath/_ky_6Si-UQo/wtBsAFToBwAJ, and I'd like to know what you think of it. Is it worth pursuing?