Unpopular opinion: I absolutely despise Isabelle/jEdit's asynchronous proof processing. Wastes my CPU battery like crazy and causes unpleasant lags all the time. I would rather go back to Proof General's locked regions but doesn't support PG anymore :(
Conversation
Yeah, we’re not talking running typecheckers in the background, we’re talking running SMT solvers, first order tactics, arithmetic solvers, massive rewrite sets, potentially non-terminating proof searches etc. in the background, running constantly, updating as you type.
1
1
There is really no way to make that a pleasant experience IMO, no matter how much computational power you want to throw at it.
1
2
Yeah, that is one of the reasons I bounced of Isabelle the first time I gave it a go. Found Lean+VS Code much nicer on my CPU, and a better editor experience than jEdit.
2