fix: Tactic failure on synthesizing placeholder #139

    let descendants ←  Meta.getMVars $ ← instantiateMVars (.mvar goal)

    if (← Elab.Term.logUnassignedUsingErrorInfos descendants) then
      return .failure #["something is wrong"]

but it causes a couple existing tests to break. This is strange behaviour.

Adding this snippet to `GoalState.tryTacticM` fixes the test ```lean let descendants ← Meta.getMVars $ ← instantiateMVars (.mvar goal) if (← Elab.Term.logUnassignedUsingErrorInfos descendants) then return .failure #["something is wrong"] ``` but it causes a couple existing tests to break. This is strange behaviour.

aniva added 1 commit 2024-12-09 17:30:56 -08:00

47d26badc8

feat: Capture mvar errors

aniva commented

2024-12-09 17:34:54 -08:00

Introduced regression. Waiting on decision of issue author to pick a solution.

aniva added 1 commit 2024-12-09 17:58:32 -08:00

d040d2006c

fix: Do not guard mvar errors in other tactics

aniva commented

2024-12-09 21:44:59 -08:00

Should be ready to go

aniva added 1 commit 2024-12-10 23:16:57 -08:00

1d10cd2b20

fix: Collect errored mvars by iterating errorInfo

aniva added 1 commit 2024-12-10 23:49:49 -08:00

755ba13c1b

fix: Set `synthesizeSyntheticMVarsNoPostponing`

aniva added 1 commit 2024-12-10 23:51:54 -08:00

e0e5c9ec68

chore: Code cleanup

aniva added 1 commit 2024-12-11 00:17:08 -08:00

cb87fcd9dd

fix: Insert `mvarDeps`

aniva added 1 commit 2024-12-11 00:21:37 -08:00

58956d33fe

doc: Update behaviour rationale

aniva added 1 commit 2024-12-11 00:25:05 -08:00

aa122b2bb9

doc: Update rationale link

aniva commented

2024-12-11 00:49:13 -08:00

Fixed some more problems. Two test cases in Mathlib:

To reproduce, use these files and pipe them into pantograph-repl's stdin.

frontend.process {"file": "theorem amc12a_2021_p12 (a b c d : ℝ) (f : ℂ → ℂ) (h₀ : ∀ z, f z = z^6 - 10 * z^5 + a * z^4 + b * z^3 + c * z^2 + d * z + 16) (h₁ : ∀ z, f z = 0 → (z.im = 0 ∧ 0 < z.re ∧ ↑(Int.floor z.re) = z.re)) : b = -88 := sorry", "invocations": false, "sorrys": true}
goal.tactic {"stateId": 0, "goalId": 0, "tactic": "specialize h₁ (Complex.I * 3)"}
goal.tactic {"stateId": 1, "goalId": 0, "tactic": "norm_cast at h₁"}
goal.tactic {"stateId": 2, "goalId": 0, "tactic": "norm_cast at h₀"}
goal.tactic {"stateId": 3, "goalId": 0, "tactic": "simpa using h₁ (by simp [h₀])"}

(throws error, which is the correct behaviour)

frontend.process {"file": "theorem imo_1978_p5 (n : ℕ) (a : ℕ → ℕ) (h₀ : Function.Injective a) (h₁ : a 0 = 0) (h₂ : 0 < n) : (∑ k in Finset.Icc 1 n, (1 : ℝ)/k) ≤ ∑ k in Finset.Icc 1 n, (a k)/k^2 := sorry", "invocations": false, "sorrys": true}
goal.tactic {"stateId": 0, "goalId": 0, "tactic": "simp only [Finset.sum_range_one, Finset.sum_range_zero, h₁, Nat.cast_one, div_one] at *"}
goal.tactic {"stateId": 1, "goalId": 0, "tactic": "norm_cast"}
goal.tactic {"stateId": 2, "goalId": 0, "tactic": "simp_all only [Finset.sum_range_succ]"}
goal.tactic {"stateId": 3, "goalId": 0, "tactic": "norm_cast"}
goal.tactic {"stateId": 4, "goalId": 0, "tactic": "simpa [h₀] using Finset.sum_le_sum fun x hx => _"}

(generates 1 goal, which is the correct behaviour)

Fixed some more problems. Two test cases in Mathlib: To reproduce, use these files and pipe them into `pantograph-repl`'s stdin. ``` frontend.process {"file": "theorem amc12a_2021_p12 (a b c d : ℝ) (f : ℂ → ℂ) (h₀ : ∀ z, f z = z^6 - 10 * z^5 + a * z^4 + b * z^3 + c * z^2 + d * z + 16) (h₁ : ∀ z, f z = 0 → (z.im = 0 ∧ 0 < z.re ∧ ↑(Int.floor z.re) = z.re)) : b = -88 := sorry", "invocations": false, "sorrys": true} goal.tactic {"stateId": 0, "goalId": 0, "tactic": "specialize h₁ (Complex.I * 3)"} goal.tactic {"stateId": 1, "goalId": 0, "tactic": "norm_cast at h₁"} goal.tactic {"stateId": 2, "goalId": 0, "tactic": "norm_cast at h₀"} goal.tactic {"stateId": 3, "goalId": 0, "tactic": "simpa using h₁ (by simp [h₀])"} ``` (throws error, which is the correct behaviour) ``` frontend.process {"file": "theorem imo_1978_p5 (n : ℕ) (a : ℕ → ℕ) (h₀ : Function.Injective a) (h₁ : a 0 = 0) (h₂ : 0 < n) : (∑ k in Finset.Icc 1 n, (1 : ℝ)/k) ≤ ∑ k in Finset.Icc 1 n, (a k)/k^2 := sorry", "invocations": false, "sorrys": true} goal.tactic {"stateId": 0, "goalId": 0, "tactic": "simp only [Finset.sum_range_one, Finset.sum_range_zero, h₁, Nat.cast_one, div_one] at *"} goal.tactic {"stateId": 1, "goalId": 0, "tactic": "norm_cast"} goal.tactic {"stateId": 2, "goalId": 0, "tactic": "simp_all only [Finset.sum_range_succ]"} goal.tactic {"stateId": 3, "goalId": 0, "tactic": "norm_cast"} goal.tactic {"stateId": 4, "goalId": 0, "tactic": "simpa [h₀] using Finset.sum_le_sum fun x hx => _"} ``` (generates 1 goal, which is the correct behaviour)

aniva added 1 commit 2024-12-11 01:08:53 -08:00

4217dbcf80

Merge branch 'dev' into bug/tactic-failure-placeholder

aniva merged commit e9fbce7b4d into dev

2024-12-11 01:13:15 -08:00

aniva deleted branch bug/tactic-failure-placeholder

2024-12-11 01:13:15 -08:00

aniva referenced this issue from a commit

2024-12-11 01:13:16 -08:00

Merge pull request 'fix: Tactic failure on synthesizing placeholder' (#139) from bug/tactic-failure-placeholder into dev

Sign in to join this conversation.

No reviewers