search

expln / metamath-lamp

Metamath-lamp (Lite Assistant for Metamath Proofs) is a GUI-based proof assistant for creating formal mathematical proofs in Metamath that does not require installation (just run it directly using your web browser).
https://expln.github.io/lamp/latest/index.html
MIT License
13 stars 5 forks source link

Renumber fails if the goal label is a number #207

Open BTernaryTau opened 6 days ago

BTernaryTau commented 6 days ago

If the label for the goal statement is a number, attempting to renumber steps will fail with the error Cannot renumber steps: there was an internal error during renumbering.

This case doesn't necessarily need to be supported by the renumber option, but there should probably be a more specific error message at the very least.

image
expln commented 5 days ago

Thanks for reporting this issue. It is fixed on dev. The fix was to exclude the goal step from automatic renumbering. The goal step is a special one, so users should manage its label manually. The error message was also improved, but it still will not show the exact root cause. It is not possible due to how renumbering is implemented.

The renumbering works in two stages: 1 - renumber using a special renumbering algorithm; 2 - check there are no errors in the editor after renumbering. If there are errors then renumbering results are discarded. The special renumbering algorithm is supposed to respect the rules checked on the second stage. But this may not always be true due to a bug in the code. For example, there is a rule that hypothesis steps and the goal step must have labels which don’t clash with symbols existing in the loaded context (because these labels will appear in the final proof which is supposed to be copy-pasted to the MM database). Before the fix, the goal step was renamed to 1. But there is such a constant in set.mm. Therefore this was an illegal label for the goal step. With the improved error message you would see the following (it is not possible to reproduce after the fix has been applied):

image

It is still not absolutely clear from this message why renumbering failed, but at least it points out to the statement |- ph and this may give the user some clue of what to look into (I guess you spent some time trying to find out the root cause when you faced this error for the first time).