feat(frontend): Move functionalities of sorry capture to `frontend.distil` #271

Merged

aniva merged 6 commits from frontend/distil into dev

2025-08-11 14:58:54 -07:00

aniva commented

2025-08-08 12:03:12 -07:00

Owner

Problems with `frontend.process`

This is related to the problem of sorry captures in PutnamBench's 2005/a2 data point.

frontend.distil works:

frontend.distil {"file": "open Nat Set\nabbrev putnam_2005_a2_solution : ℕ → ℕ := sorry\ntheorem putnam_2005_a2 (n : ℕ) (npos : n > 0) (S : Set (ℤ × ℤ)) (unit : ℤ × ℤ → ℤ × ℤ → Prop) (rooktour : (ℕ → ℤ × ℤ) → Prop) (hS : S = prod (Icc 1 (n : ℤ)) (Icc 1 3)) (hunit : unit = fun (a, b) (c, d) ↦ a = c ∧ |d - b| = 1 ∨ b = d ∧ |c - a| = 1) (hrooktour : rooktour = fun p ↦ (∀ P ∈ S, ∃! i, i ∈ Icc 1 (3 * n) ∧ p i = P) ∧ (∀ i ∈ Icc 1 (3 * n - 1), unit (p i) (p (i + 1))) ∧ p 0 = 0 ∧ ∀ i > 3 * n, p i = 0) : ({p : ℕ → ℤ × ℤ | rooktour p ∧ p 1 = (1, 1) ∧ p (3 * n) = ((n : ℤ), 1)}.encard = putnam_2005_a2_solution n) := sorry"}

frontend.process does not:

frontend.process {"file": "open Nat Set\nabbrev putnam_2005_a2_solution : ℕ → ℕ := sorry\ntheorem putnam_2005_a2 (n : ℕ) (npos : n > 0) (S : Set (ℤ × ℤ)) (unit : ℤ × ℤ → ℤ × ℤ → Prop) (rooktour : (ℕ → ℤ × ℤ) → Prop) (hS : S = prod (Icc 1 (n : ℤ)) (Icc 1 3)) (hunit : unit = fun (a, b) (c, d) ↦ a = c ∧ |d - b| = 1 ∨ b = d ∧ |c - a| = 1) (hrooktour : rooktour = fun p ↦ (∀ P ∈ S, ∃! i, i ∈ Icc 1 (3 * n) ∧ p i = P) ∧ (∀ i ∈ Icc 1 (3 * n - 1), unit (p i) (p (i + 1))) ∧ p 0 = 0 ∧ ∀ i > 3 * n, p i = 0) : ({p : ℕ → ℤ × ℤ | rooktour p ∧ p 1 = (1, 1) ∧ p (3 * n) = ((n : ℤ), 1)}.encard = putnam_2005_a2_solution n) := sorry", "readHeader": false, "inheritEnv": false, "sorrys": true, "typeErrorsAsGoals": false, "newConstants": false}

which gives

{"error":"exception","desc":"unknown constant 'putnam_2005_a2.match_1'"}

To me, this is a signal to deprecate drafting capabilities in frontend.process.

Proposal

Merge the sorry-capturing capabilities to frontend.distil. Remove the InfoTree based processing system since syntactic sorrys could correspond to multiple expression sorrys.

## Problems with `frontend.process` This is related to the problem of `sorry` captures in PutnamBench's 2005/a2 data point. `frontend.distil` works: ``` frontend.distil {"file": "open Nat Set\nabbrev putnam_2005_a2_solution : ℕ → ℕ := sorry\ntheorem putnam_2005_a2 (n : ℕ) (npos : n > 0) (S : Set (ℤ × ℤ)) (unit : ℤ × ℤ → ℤ × ℤ → Prop) (rooktour : (ℕ → ℤ × ℤ) → Prop) (hS : S = prod (Icc 1 (n : ℤ)) (Icc 1 3)) (hunit : unit = fun (a, b) (c, d) ↦ a = c ∧ |d - b| = 1 ∨ b = d ∧ |c - a| = 1) (hrooktour : rooktour = fun p ↦ (∀ P ∈ S, ∃! i, i ∈ Icc 1 (3 * n) ∧ p i = P) ∧ (∀ i ∈ Icc 1 (3 * n - 1), unit (p i) (p (i + 1))) ∧ p 0 = 0 ∧ ∀ i > 3 * n, p i = 0) : ({p : ℕ → ℤ × ℤ | rooktour p ∧ p 1 = (1, 1) ∧ p (3 * n) = ((n : ℤ), 1)}.encard = putnam_2005_a2_solution n) := sorry"} ``` `frontend.process` does not: ``` frontend.process {"file": "open Nat Set\nabbrev putnam_2005_a2_solution : ℕ → ℕ := sorry\ntheorem putnam_2005_a2 (n : ℕ) (npos : n > 0) (S : Set (ℤ × ℤ)) (unit : ℤ × ℤ → ℤ × ℤ → Prop) (rooktour : (ℕ → ℤ × ℤ) → Prop) (hS : S = prod (Icc 1 (n : ℤ)) (Icc 1 3)) (hunit : unit = fun (a, b) (c, d) ↦ a = c ∧ |d - b| = 1 ∨ b = d ∧ |c - a| = 1) (hrooktour : rooktour = fun p ↦ (∀ P ∈ S, ∃! i, i ∈ Icc 1 (3 * n) ∧ p i = P) ∧ (∀ i ∈ Icc 1 (3 * n - 1), unit (p i) (p (i + 1))) ∧ p 0 = 0 ∧ ∀ i > 3 * n, p i = 0) : ({p : ℕ → ℤ × ℤ | rooktour p ∧ p 1 = (1, 1) ∧ p (3 * n) = ((n : ℤ), 1)}.encard = putnam_2005_a2_solution n) := sorry", "readHeader": false, "inheritEnv": false, "sorrys": true, "typeErrorsAsGoals": false, "newConstants": false} ``` which gives ```json {"error":"exception","desc":"unknown constant 'putnam_2005_a2.match_1'"} ``` To me, this is a signal to deprecate drafting capabilities in `frontend.process`. ## Proposal Merge the sorry-capturing capabilities to `frontend.distil`. Remove the `InfoTree` based processing system since syntactic `sorry`s could correspond to multiple expression `sorry`s.

aniva added this to the v0.3.6 milestone

2025-08-08 12:03:12 -07:00

aniva added the

labels

2025-08-08 12:03:12 -07:00

aniva self-assigned this

2025-08-08 12:03:12 -07:00

aniva added the

part/REPL

label

2025-08-08 21:22:54 -07:00

aniva changed title from ~~fix(frontend): Handling of matchers in distil~~ to feat(frontend): Move functionalities of sorry capture to frontend.distil

2025-08-11 11:59:21 -07:00

aniva added 2 commits

2025-08-11 14:17:29 -07:00