Enabling the next-generation trait solver on nightly

91 points by jana a day ago on lobsters | 20 comments

lonjil | a day ago

Woohoo

and enable us to fix the remaining type system unsoundnesses.

hell yeah

gignico | a day ago

Didn’t they recently enable the new borrow checker in nightly as well? The next few releases will be very interesting

[OP] jana | a day ago

Correct! Both experiments are going on simultaneously right now, and both are some very long standing projects (3+ years)!

gignico | a day ago

Seems awesome! :D

kevincox | 10 hours ago

Thanks for pointing this out! I had skipped the article thinking I'd already read it.

mond | a day ago

So... are there going to be any trait-related soundness issues left after this?

(I say trait-related, since I expect that llvm's handling of pointer provenance is still broken.)

[OP] jana | a day ago

The blog post references project 0, and the goal is that no, we won't. At least none of the currently known ones. Formally verifying the soundness is another step, which might at some point be happening too.

muvlon | 10 hours ago

I wonder whether this new solver will also finally fix https://github.com/rust-lang/rust/issues/25860. It's certainly not the most practically relevant soundness hole, but the most infamous and one of the oldest remaining ones at this point.

On one hand, it doesn't show up in the 200+ list linked in the post, because it doesn't have the necessary tag on GitHub. On the other hand, people in that issue mentioned that the new solver could fix this. So it's unclear to me.

[OP] jana | 9 hours ago

The goal is to eventually fix all these unsoundness issues, and for the majority of the known cases the new solver is a hard requirement.

briankung | 20 hours ago

As an underapproximation, we currently know of more than 200 issues on GitHub fixed by this change.

Wow, that's quite something.

polywolf | 11 hours ago

Awesome!!! Really appreciate the effort put into these posts, excited for all the new features it'll bring. Fantastic work

jado | a day ago

i wish the new solver performance plot showed 2x - 0.5x on the y axis so the perf change for those releases is easier to read (or it was another plot next to that 16x-0.125x plot).

otherwise awesome work!!

[OP] jana | a day ago

I'll make one for you! I'll put it in my blog post in an hour or two when I'm home at my computer :) I've got all the data ready!

jado | a day ago

thanks!!

[OP] jana | 15 hours ago

took a bit longer than 2 hours, laptop was dead so I did it in the morning, but here ya go!

https://donsz.nl/blog/new-solver-performance#zoomed

I hope this was what you meant. I can make more graphs based on the data I have, I have a lot at this point. Been meaning to make a visualization of all days of last week, since so much changed daily, and I pretty much have daily datapoints stored already.

moltonel | 13 hours ago

Interesting writeup. Sorted graph looks tidier, but I agree it's less informative. I wonder if a violin chart (same y axis, violin width is the number of crates in a y-axis range, one violin per measurement date) would work well for that data ?

Just to be clear, are these the times for "cargo check", or something narrower ?

[OP] jana | 11 hours ago

These are based on instruction counts (not wall times) of cargo check, after dependencies are built. In other words, we don't measure crates with large dependency trees as taking longer. The setup is to cargo check, then cargo clean -p leaf-package and then cargo check again.

addison | 23 hours ago

Awesome, awesome, awesome. I have projects which are intractable without next-solver. Incredible work, y'all.

rebound | 22 hours ago

Very excited for this. Great work!

junon | 7 hours ago

Wow, this is exciting. Thank you for the great writeup as always.