update to Lean 4.29.0

[AmosNico]

Update to Lean 4.29.0. Some rewrites which previously worked now failed (mostly using push_evaluate), so I had to rework some proofs.

[eshelyaron]

Hi @AmosNico, thanks for this!
I see you marked the PR as draft, so let me know if/when it is ready for review and if there's anything I can help with.

[AmosNico]

Hi @AmosNico, thanks for this! I see you marked the PR as draft, so let me know if/when it is ready for review and if there's anything I can help with.

Hi @eshelyaron, it is more or less ready now, with the exception of one instance in Sat.lean, where I had to manually increase the number of heartbeats. set_option pp.proofs true and set_option diagnostics true suggest that the issue is that the bounds proof in denotation is becomes very large and is reduced a lot. I am not sure how to fix it, so feel free to have a look if you want.
That being said, the file still compiles (it just takes a long time), and given that it is not part of the core library, I think this could still be merged to main. I will soon add another pull request for moving the repository to the new module system, it might make more sense to fix it there.

[AmosNico]

All problems in Sat.lean are solved now, I added a few congruence lemmas in BDD.lean which fix the problem.

Sorry for force pushes (here and on the other pull requests), I know it makes reviewing harder. In hindsight I should have waited longer to make the pull request (or at least keep it marked as draft until it was properly ready)

[eshelyaron]

Hi @AmosNico , sorry for the late response.
I've merged this PR after solving some merge conflicts due to the new Reduce implementation I pushed yesterday.
Oh, but I see you've just marked it as draft, are there additional changes we need to make here?
Thanks!

[AmosNico]

Oeps I was also solving the merge conflicts, so I guess we duplicated some work. I previously forgot to update the lean version in the docbuild, so I was fixing that as well. But given that there is v4.30 anyway, I don't think it matters much, and we can keep it this way