Questions about `grind`

Stream: lean4

[Ching-Tsun Chou]

Yesterday, after a bump to toolchain v4.29.0-rc1 in cslib, I had to change a proof from one that was originally just four invocations of grind for the four conjuncts of the goal, to one in which I had to spell out a lot of nitty-gritty details including a separate lemma:
https://github.com/leanprover/cslib/pull/325/changes/f31b889c981566e5244f507ab3f8409390ce40d1
I have several questions:
(1) Why did I have to do that? What happened in the v4.29.0-rc1 bump that necessitated such a change?
(2) In my attempt at avoiding doing a painful proof, I went to the pre-bump version and tried to use grind? to find out which lemmas were actually used by each grind. But I found out that once I added the ?, the grind proof blows up (in the sense of exceeding maxHeartbeats). Even after 5x maxHeartbeats, the grind?still could not solve the goal. Why?

[Chris Henson]

I can take a closer look, but I think it would be nice to first discuss in #CSLib and try to minimize before asking in this channel.

[Ching-Tsun Chou]

It seems to me that generating BKMs for grind would be of general interest for the Lean4 community. Proof instability would be a serious obstacle for the wider adoption of grind.