LS-Lab/KeYmaeraX-release

empty Tactic block => internal safety check violated

rbohrer opened this issue · 0 comments

Version: 4.9.8

Repro:

  • upload attached archive
  • error message when you press save on new model dialog

got: internal safety check violated

expected: error message telling me it's pretty unreasonable of me to upload an empty tactic. Or, even better, replacing empty tactic with "todo" or treating it like there's no Tactic block at all, those fixes would also make sense

Priority: would not be surprised if students run into it during labs and before projects. obvious workaround

tactic-display-on-limited-editing.kyx.txt