Kernel error in Aesop

Stream: general

[Harry Goldstein]

Hi all, I raised this issue in the Aesop repo at the end of last year: https://github.com/leanprover-community/aesop/issues/186

At the time, it was just a curiosity, but now it's blocking a project that I'm working on. Does anyone have any immediate impressions about what could be going wrong?

[Shreyas Srinivas]

I don’t think this is a kernel error. This seems to be a case of Aesop unhygienically adding declarations into the environment. See : https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/aesop.20and.20bv_decide/near/514775125

[Shreyas Srinivas]

It’s best that we CC @Jannis Limperg to be sure.

[Sebastian Ullrich]

Does not reproduce on live.lean-lang.org (anymore)

[Jannis Limperg]

Yeah, this seems to have been solved by recent improvements to Aesop's handling of auxiliary lemmas. Please lmk if it doesn't work for you.

[Bhavik Mehta]

In all cases I had where aesop gave kernel errors, the recent improvements mentioned above fixed it

[Harry Goldstein]

OK, thanks for the help folks. My project was pinned to v4.20.0, but updating to v4.21.0-rc3 fixed my issue. Is it generally expected that folks just pin production code to the latest RC no matter what? In other language communities I've been a part of, there was a culture of back-porting bug fixes to the latest stable version, but it seems like that's not the case for Lean?

[Kevin Buzzard]

Right now nothing is back ported and no backwards compatibility is promised. In my project to prove FLT we are constantly bumping to current lean and mathlib (basically weekly). This might change as the software stabilises, I guess.

[Kim Morrison]

We're not yet ready to backport non-show-stopper bug fixes to previous stables. It's certainly fine to stay on stable releases, but do expect to have to move on to the next stable (approximately one month after the release candidate) to get further language changes.

[Sebastian Ullrich]

It wasn't even so much of a bugfix in this case as a new Lean API that then enabled Aesop to make its own implementation more robust

[Harry Goldstein]

OK, that's what I thought, and I think that makes sense for a language like Lean that's still in flux and with constrained developer resources.

I had been following the update cadence that Kim recommended, updating once a month, but this Aesop issue was seriously derailing our development. (Almost every file in my project with multiple definitions was crashing — my student was resorting to just moving everything into its own file.) In this case updating right away to the RC was fine, but if I'd had any external dependencies I could see that being a really tricky situation.