non-finishing `aesop?`

Stream: general

[Damiano Testa]

Dear All,

is there a way to get aesop? to print the steps that it took, even when it does not close the goal?

For definiteness, here is an example where I may want to know what it is that aesop did: can I access it?

Thanks!

import Mathlib.Tactic

example {n : ℕ} (h : (n = 0 ∧ False) ∨ n = 1) : False := by
  aesop?  -- can I get `aesop` to show what it did to reach this state?
  sorry

[Jannis Limperg]

Not currently, but I should really fix this. There's no conceptual problem with this, just technical issues.

[Damiano Testa]

Ok, thanks! Of course, the reason for asking is that aesop works so well that I want to use it even when it does not close the goal, but then I would like to replace it with the steps that it took!

[Alex J. Best]

I wonder if there is a way to hackily get this on the user side by adding a super low priority "give up and sorry rule" that only runs when all other goals are exhausted, then aesop would always ("succeed")

[Damiano Testa]

Are you thinking of something like wrapping aesop in aesop <;> sorry? EDITED.

[Damiano Testa]

Ah, maybe this would backtrack, so I guess not this!

[Alex J. Best]

I mean like this

import Mathlib.Tactic
import Aesop

@[aesop 1% unsafe apply]
def sooryeh {A} : A := sorry
set_option trace.aesop true

example {n : ℕ} (h : (n = 0 ∧ False) ∨ n = 1) : False := by
  aesop? -- can I get `aesop` to show what it did to reach this state?
  sorry

[Damiano Testa]

@Alex J. Best this is a wonderful idea, thanks!

[Siddhartha Gadgil]

@Alex J. Best I agree this is brilliant. Maybe one can refine it with a variant of sorry that logs the goal state and then uses sorry.