aesop tests failing on nightly-2024-01-19

Stream: lean4

[Kim Morrison]

@Jannis Limperg (or anyone else interested in jumping in)

aesop's nightly-testing branch is successfully building on nightly-2024-01-19, but the test suite is breaking in many places.

Might you be able to take a look? I'm running out of time for the day.

[Kim Morrison]

The two suspects should be

1. that simp is now doing something different with ground terms: lean4#3187.
2. that Std has reduced many of its imports, and so it may just be some missing imports

[Jannis Limperg]

I'm at a conference but will try to take a look later today.

[Jannis Limperg]

So this new simp option unfolds every def if it's applied only to ground terms? Or is there something else going on?

[Jannis Limperg]

nightly-testing tests should work again.

[Kim Morrison]

Thanks, @Jannis Limperg !