leanprover-community / aesop

White-box automation for Lean 4
Apache License 2.0
192 stars 26 forks source link

traceScript is ignored when the maximum rule application depth is reached #74

Closed kim-em closed 11 months ago

kim-em commented 11 months ago

This would be helpful for user friendly debugging.

JLimperg commented 11 months ago

This is part of the bigger issue that script tracing currently only works for finished proofs. I'm working on this.