Aesop search tree cycles

Stream: nightly-testing

[Jannis Limperg]

Per this message, Aesop is currently detecting cycles in its search trees. I use a somewhat tricky encoding of the search trees as an unsafe inductive type, to get pointers pointing up the tree. (Questionable value for sure.) Does that ring any bells? Any recent Lean changes that could be messing with this? cc @Sebastian Ullrich @Markus Himmel

[Sebastian Ullrich]

@Henrik Böving might be interested(/horrified) as well. I guess the BaseIO refactoring does fall in the date range in question but I'm not sure I want to even imagine how that could be relevant

[Jannis Limperg]

The unsafe construction in question is here: https://github.com/leanprover-community/aesop/blob/1fa48c6a63b4c4cda28be61e1037192776e77ac0/Aesop/Tree/Data.lean#L386

Maybe the answer is "well, don't do that!", but I feel like what I'm doing is not too crazy.

[Jannis Limperg]

@Henrik Böving @Sebastian Ullrich I've looked into this, but I can't find anything fishy in my code, so there might be an actual Lean bug. The function that checks for cycles is here. It traverses the tree, collects the IO.Refs that hold each node and checks that none of the Refs are pointer-equal to a previously visited node. Does this sound reasonable?

[Henrik Böving]

I know what it is

[Henrik Böving]

I overlooked to fix one in the hundreds of IO/ST functions and of course we don't actually test it anywhere so it went unnoticed

[Jannis Limperg]

Nice, happy to hear that! Thanks!

[Henrik Böving]

@Sebastian Ullrich I actually think lean_st_ref_ptr_eq was broken the entire time btw, check:

bool r = lean_to_ref(ref1)->m_value == lean_to_ref(ref2)->m_value;

This tests if the containing value if ptr eq, not if the cell is ptr eq, the documentation says:

Checks whether two reference cells are in fact aliases for the same cell.

Even if they contain the same value, two references allocated by different executions of IO.mkRef
or ST.mkRef are distinct. Modifying one has no effect on the other. Likewise, a single reference
cell may be aliased, and modifications to one alias also modify the other.

But if I currently have two IO.mkRef with the same 0 in them they are ptr_eq. I will change that.

[Henrik Böving]

@Jannis Limperg you can test aesop with the PR toolchain on https://github.com/leanprover/lean4/pull/11056 in a bit or when you wake up tomorrow.

[Kim Morrison]

Thanks @Henrik Böving! @Jannis Limperg, I've confirmed aesop works against that toolchain, so everything should come good by itself later today. (I need to restore the lake built AesopTest step in Mathlib CI, still.)