Enter the attached text in the model editor window
Start Proof
Save
I then observe that there is no error message (including web dev console or command prompt) and press "start proof" again. I get a modal popup window saying there is a syntax error, but there is no error indicated on the editor, plus no message in web dev console or command prompt. Once I exit out of the editor window, the models list shows that both models exist, and I can start a proof of either one.
I assume the issue is along the lines of: If there are two models in the archive, then it's not obvious which one you would want to prove, so accidentally KeYmaera X does something weird instead.
While debugging, I also ran into some sad interactions with the "save before exiting the editor" dialog, I'll raise a separate issue for that.
On 4.9.6 I did:
I assume the issue is along the lines of: If there are two models in the archive, then it's not obvious which one you would want to prove, so accidentally KeYmaera X does something weird instead.
While debugging, I also ran into some sad interactions with the "save before exiting the editor" dialog, I'll raise a separate issue for that.
new-model-bug.kyx.txt .