Feature request: Extract goal ++

Stream: general

[Adam Topaz]

Idris has a nice feature where (in emacs) C-c C-e extracts a goal as a top-level definition, and replaces the current goal with a call to that new definition. We have something similar with extract_goal in mathlib. How hard would it be to extend extract_goal so that it automatically makes a top level def (with a sorry) and replaces the current goal with that def?

[Adam Topaz]

(I guess it would have to be a hole command?)

[Andrew Yang]

Is tactic.interactive.abstract what you want? The tactic description looks promising but I have never figured out how to make it work.

[Adam Topaz]

Maybe! I have never even heard of abstract...

[Adam Topaz]

I'll have to try it later.

[Rob Lewis]

I think Adam wants something that changes the source code, right? abstract can be useful but it just creates a new declaration under the hood. I think what you're describing is extract_goal plus VSCode support. This doesn't seem doable with the current Try this: or with hole commands.

[Adam Topaz]

So what is abstract actually useful for? For example, can it help with deterministic timeouts in long proofs?

[Eric Rodriguez]

I just tried this, and I think extract_goal uses pp instead of to_string so copy-pasting goals created by it doesn't usually work :/ is round-tripping easier in Lean4?