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.
VSCode is experimentally supported by Isabelle but the prettify symbols mode is quite janky and slow, and I get even more lagging than jEdit.
1
1
Haha, yup, just remembered that there was a plugin! Would be nice if they figured out how to get it working more smoothly. Isabelle deserves a good editor experience.