search

rust-lang / chalk

An implementation and definition of the Rust trait system using a PROLOG-like logic solver
https://rust-lang.github.io/chalk/book/
Other
1.84k stars 182 forks source link

we only need to prove things one way #754

Closed nikomatsakis closed 2 years ago

nikomatsakis commented 2 years ago

Partially addresses #727 (some work is left for future work).

flodiebold commented 2 years ago

I tried out this patch with rust-analyzer on the rust-analyzer codebase:

> $ ./ra-chalk-master -q analysis-stats . 
Database loaded:     1.23s, 246minstr (metadata 747.44ms, 24minstr; build 266.50ms, 9338kinstr)
  crates: 39, mods: 857, decls: 19554, fns: 14566
Item Collection:     17.80s, 78ginstr
  exprs: 400526, ??ty: 342 (0%), ?ty: 514 (0%), !ty: 155
Inference:           102.34s, 375ginstr
Total:               120.14s, 453ginstr

> $ ./ra-chalk-niko -q analysis-stats . 
Database loaded:     1.14s, 245minstr (metadata 720.16ms, 24minstr; build 222.83ms, 9060kinstr)
  crates: 39, mods: 857, decls: 19554, fns: 14566
Item Collection:     17.82s, 78ginstr
  exprs: 400526, ??ty: 342 (0%), ?ty: 514 (0%), !ty: 17
Inference:           96.19s, 361ginstr
Total:               114.01s, 439ginstr

> $ ./ra-chalk-niko-early-exit -q analysis-stats .
Database loaded:     1.15s, 245minstr (metadata 711.23ms, 24minstr; build 206.14ms, 9085kinstr)
  crates: 39, mods: 857, decls: 19554, fns: 14566
Item Collection:     16.40s, 78ginstr
  exprs: 400526, ??ty: 342 (0%), ?ty: 514 (0%), !ty: 17
Inference:           75.01s, 318ginstr
Total:               91.41s, 396ginstr

So this patch fixes almost all remaining type mismatches (that's the !ty) we have on our codebase, and with the early exit I mentioned it actually improves inference time by 25%!

nikomatsakis commented 2 years ago

@flodiebold ready to merge, I think

nikomatsakis commented 2 years ago

I reverted the last commit

nikomatsakis commented 2 years ago

@bors r+

bors commented 2 years ago

:pushpin: Commit 70b2fdbd7a172c07e0dabaa7c275f4ab94e033a1 has been approved by nikomatsakis

bors commented 2 years ago

:hourglass: Testing commit 70b2fdbd7a172c07e0dabaa7c275f4ab94e033a1 with merge 3e3f76a28a6373e733ffdccf84802781f83a293a...

nikomatsakis commented 2 years ago

Filed https://github.com/rust-lang/chalk/issues/760

lnicola commented 2 years ago

Would it be possible to trigger an early publish? We want to get our hands on this in RA, and upgrading sooner will let us find any issues before the next release.

jackh726 commented 2 years ago

I can kick off a release later today.

bors commented 2 years ago

:sunny: Test successful - checks-actions Approved by: nikomatsakis Pushing 3e3f76a28a6373e733ffdccf84802781f83a293a to master...

jackh726 commented 2 years ago

0.82.0 released

lnicola commented 2 years ago

with the early exit I mentioned it actually improves inference time by 25%!

Strangely, I'm not seeing that large of a difference:

baseline
Database loaded:     1.79s, 244minstr (metadata 420.87ms, 24minstr; build 1.29s, 8944kinstr)
  crates: 39, mods: 878, decls: 20758, fns: 15517
Item Collection:     9.90s, 79ginstr
58  exprs: 425364, ??ty: 325 (0%), ?ty: 145 (0%), !ty: 142                                                                                                         
Inference:           53.36s, 405ginstr
Total:               63.25s, 484ginstr

chalk-0.82
Database loaded:     1.22s, 244minstr (metadata 413.94ms, 24minstr; build 727.46ms, 8602kinstr)
  crates: 39, mods: 878, decls: 20758, fns: 15517
Item Collection:     9.87s, 79ginstr
  exprs: 425364, ??ty: 325 (0%), ?ty: 145 (0%), !ty: 1                                                                                                             
Inference:           48.90s, 373ginstr
Total:               58.77s, 452ginstr
lnicola commented 2 years ago

Sure, but flodiebold reported a 25% speed-up vs. the 8% I got. Still good, but a bit unexpected.