LS-Lab/KeYmaeraX-release

Archive only uploads halfway when some entries contain non-fatal errors

rbohrer opened this issue · 0 comments

Version: 4.9.8

Reproduce: Upload attached archive under "structured" then check model list
Got: Model contains archives, only one appears in the list. NOTE: The one that uploads successfully is the one that contains the error. Presumably because it's first. And there's no error message about the error, on UI, command line, or dev console
Expected: Clear error message on UI (not command line or dev console) or upload both models despite the minor error.

What the error is: The first archive entry forgets to declare "y" in ProgramVariables. If you add the declaration, both models load fine.

archiveHalfwayUpload.kyx.txt