Move `sorry` extraction to a separate command #263

New issue

Closed

opened 2025-08-01 11:55:39 -07:00 by aniva · 1 comment

aniva commented

2025-08-01 11:55:39 -07:00

Owner

The problem with the existing frontend.refactor command is that it produces source code nobody wants to read, and it relies on the delaborator, which is in a permanent whack-a-mole situation. Preliminary trials on PutnamBench shows that about 1 in 5 data points fail to roundtrip.

Given the distinct nature of search target extraction, we should have a command to turn sorrys directly into a search target with multiple mvars. For example, given the mystery example here:

def f : Nat -> Nat := sorry
theorem mystery_p : p f := sorry

We produce a target of the type

|- { f : Nat -> Nat // p f }

If this is the type of mvar ?root, then we can easily extract f and mystery from ?root.val and ?root.p.

The problem with the existing `frontend.refactor `command is that it produces source code nobody wants to read, and it relies on the delaborator, which is in a permanent whack-a-mole situation. Preliminary trials on PutnamBench shows that about 1 in 5 data points fail to roundtrip. Given the distinct nature of search target extraction, we should have a command to turn `sorry`s directly into a search target with multiple mvars. For example, given the mystery example here: ``` def f : Nat -> Nat := sorry theorem mystery_p : p f := sorry ``` We produce a target of the type ``` |- { f : Nat -> Nat // p f } ``` If this is the type of mvar `?root`, then we can easily extract `f` and `mystery` from `?root.val` and `?root.p`.