Async running of tactics

Stream: lean4

[Siddhartha Gadgil]

Here is a demo of running tactics in the background as @Scott Morrison suggested. This is crude and buggy, so posted more as a proof of concept of what can be done fairly easily. The motivation is for long-running AI-powered tactics (and also conjectures).

bg-tactics.gif

I implemented a couple of variants. For the one in the demo:

• One types bg tactic to launch a tactic and then return a sorry (a variant is a noop instead).
• This runs in the background as a Task and caches results (in two ways) when done.
• There is a code action which replaces any successful bg tac with a tactic script
  - for most tactics this is just tac.
  - in the case of aesop? and library_search for example, the suggested tactic is pasted instead.

As I said this is still buggy and needs work. Suggestions are most welcome.

[Siddhartha Gadgil]

The source code for the above is at https://github.com/siddhartha-gadgil/LeanAide/blob/main/LeanCodePrompts/Async.lean and https://github.com/siddhartha-gadgil/LeanAide/blob/main/LeanCodePrompts/AsyncCodeAction.lean