search

tlaplus / vscode-tlaplus

TLA+ language support for Visual Studio Code
MIT License
346 stars 31 forks source link

TLAPM: Show meaningful information in the current proof step view if tlaps is disabled. #334

Open kape1395 opened 4 hours ago

kape1395 commented 4 hours ago

It could either show instructions on how to enable the TLAPS support or should be hidden at all.

lemmy commented 4 hours ago

To make it easier for TLA+ beginners, I recommend hiding the proof step view (and the commands) until TLAPS is activated.

lemmy commented 4 hours ago

Alternatively, the wording could be adjusted so that beginners understand they likely don't need TLAPS at this stage and can simply ignore the view. The message could also include instructions on how to manually hide the view if desired.

"This view is related to the TLA+ proof system. If you are focused on model checking with TLC or Apalache, which is typical for most TLA+ beginners, you can ignore this view. To hide it, simply right-click on the VSCode action bar and uncheck 'TLA+'. If you later want to use the TLA+ proof system, you can enable it by going to the VSCode settings and checking the appropriate TLA+ integration options."