ssyram
ssyram
Yes, of course. Many tests are coming when the infrastructure is about to get done... Maybe we can focus on the implementation for now?
The original info is too messy, I reset everything and let it be the same as #796 and will start working on it from this point.
The base of this, which implements the first feature you mentioned, is in your PR #796 . I *reset* the PR to start from that branch. I've made the PR...
Thanks for the quick pinpointing! I spent an hour or two tracking this issue but was still not very clear about how this comes.
Thanks for the discussion. I think the bar should also show the progress of Cleanups to be made? BTW, I would focus on the vtable and DST restructuring on the...
The issue is still there?
BTW, in Eurydice, we now also like the idea of Builtin `Box` type: we can conveniently treat `Box` as just `T *`.
Thanks! Seems like a while away from fixing. To temporarily handle this bug, I've implemented a new pattern in my branch of Eurydice. At least now it functions as before.
Sure, the current priority for us is still to properly `drop`.
The sorting problem relates to #790 and should be resolved by AeneasVerif/hax#2.