aniva/Pantograph

Fork 0

fix: Tactic failure on synthesizing placeholder #139

Merged

aniva merged 10 commits from bug/tactic-failure-placeholder into dev

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

aniva commented

2024-12-09 08:15:52 -08:00

Owner

AFAIK This problem also exists in LeanDojo/REPL

https://github.com/lenianiva/Pantograph/issues/1

AFAIK This problem also exists in LeanDojo/REPL https://github.com/lenianiva/Pantograph/issues/1

aniva added this to the v0.2.22 milestone

2024-12-09 08:15:52 -08:00

aniva added the

labels

2024-12-09 08:15:52 -08:00

aniva self-assigned this

2024-12-09 08:15:52 -08:00

aniva added 1 commit

2024-12-09 08:15:53 -08:00

test: Tactic failure on synthesizing placeholder 7fc2bd0d0f

aniva commented

2024-12-09 17:22:00 -08:00

Author

Owner

Adding this snippet to GoalState.tryTacticM fixes the test

    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

feat: Capture mvar errors 47d26badc8

aniva commented

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

Author

Owner

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

aniva added 1 commit

2024-12-09 17:58:32 -08:00

fix: Do not guard mvar errors in other tactics d040d2006c

aniva commented

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

Author

Owner

Should be ready to go

aniva added 1 commit

2024-12-10 23:16:57 -08:00

fix: Collect errored mvars by iterating errorInfo 1d10cd2b20

aniva added 1 commit

2024-12-10 23:49:49 -08:00

fix: Set synthesizeSyntheticMVarsNoPostponing 755ba13c1b

aniva added 1 commit

2024-12-10 23:51:54 -08:00

chore: Code cleanup e0e5c9ec68

aniva added 1 commit

2024-12-11 00:17:08 -08:00

fix: Insert mvarDeps cb87fcd9dd

aniva added 1 commit

2024-12-11 00:21:37 -08:00

doc: Update behaviour rationale 58956d33fe

aniva added 1 commit

2024-12-11 00:25:05 -08:00

doc: Update rationale link aa122b2bb9

aniva commented

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

Author

Owner

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

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