search

coq / vscoq

Visual Studio Code extension for Coq
MIT License
343 stars 69 forks source link

[feature] ability to interrupt Coq #373

Open maximedenes opened 1 year ago

gares commented 1 year ago

VSCode should message vscoqtop, the signal handler should flip the boolean, the exec manager recognize the interruption exception.

In continuous mode it is unclear to me if one should switch to manual mode until further notice.

RalfJung commented 1 month ago

The issue title and description don't exactly say much -- is this about canceling a long-running tactic? If so then yes, that's absolutely needed for development of tactic automation. Writing infinite loops (or exponential-time proof search) is very easy in Coq, so it should be easy to cancel that.

IMO the most "obvious" shortcut for that is Alt-Up -- I am saying "okay stop I don't mean it, go back to the previous command". A new dedicated shortcut could also work but makes it more likely that a frustrated user will not find it.