bumps for other projects

Stream: nightly-testing

[Kim Morrison]

https://github.com/leanprover-community/import-graph/pull/37

is the adaptations PR for import-graph for nightly-2024-10-17. Entirely harmless I think, so I will merge myself sometime, but just pinging @Jon Eugster as the maintainer of import-graph. :-)

[Kim Morrison]

https://github.com/leanprover-community/quote4/pull/60

is the adaptations PR for quote4 for nightly-2024-10-17. Looks fine to me. Pinging @Eric Wieser as the maintainer.

[Kim Morrison]

https://github.com/leanprover-community/aesop/pull/168

is the adaptations PR for aesop for nightly-2024-10-17. This one still needs work: lake build is succeeding, but lake test has many failures.

@Jannis Limperg, would it be okay for me to hand this one off to you to take a further look at?

[Jannis Limperg]

I fixed Aesop's nightly-testing branch. :)

The only major change was an adaptation to lean4#4129 (from May). I'm not sure why this only surfaced now.

[Eric Wieser]

Kim Morrison said:

https://github.com/leanprover-community/quote4/pull/60

is the adaptations PR for quote4 for nightly-2024-10-17. Looks fine to me. Pinging Eric Wieser as the maintainer.

I'm struggling to review this as src#Lean.Meta.ReduceEval is undocumented...

[Eric Wieser]

Oh, I guess it's the opposite of toExpr?

[Eric Wieser]

Either way, patched and approved

[Eric Wieser]

@Kim Morrison , it looks like you pushed the bump to master; I'll force push to put it on the bump branch instead (edit: done. Your commit is still at https://github.com/leanprover-community/quote4/commit/0dc63701609247f3ef5c4227623c8811236dfe7e, but master no longer points at it)

[Kim Morrison]

Thank you. Sorry, I've got used to Johan's automation creating the Mathlib versions of these PRs automatically, and hence become less reliable at setting the base branch manually myself.