Stream: t-compiler/wg-polonius

Topic: meeting 2020.02.25


nikomatsakis (Feb 25 2020 at 19:59, on Zulip):

Hey @WG-polonius -- I'm going to go catch up with the notes from last week, but I wanted to raise the question of whether we can try to schedule the next "polonius sprint" (if we do indeed want to give this idea a spin).

lqd (Feb 25 2020 at 20:03, on Zulip):

scheduling already ? :)

lqd (Feb 25 2020 at 20:04, on Zulip):

would we need to prepare/update a roadmap to see what to do during this sprint ?

lqd (Feb 25 2020 at 20:06, on Zulip):

last week we mostly continued the work on move errors, and I think clarified a bit what was left to do

nikomatsakis (Feb 25 2020 at 20:08, on Zulip):

lqd said:

would we need to prepare/update a roadmap to see what to do during this sprint ?

not a bad idea :)

nikomatsakis (Feb 25 2020 at 20:08, on Zulip):

sorry, I got distracted, but the good news is I am down to inbox 0 in my rust-lang/rust gh notifications :P

lqd (Feb 25 2020 at 20:08, on Zulip):

there was a question from Aaron Weiss but I hadn't enough information to fully answer, I did my best but that'll likely require a few seconds of your time Niko

nikomatsakis (Feb 25 2020 at 20:08, on Zulip):

"feels like accomplishment"

nikomatsakis (Feb 25 2020 at 20:08, on Zulip):

"isn't really"

nikomatsakis (Feb 25 2020 at 20:08, on Zulip):

ok

nikomatsakis (Feb 25 2020 at 20:08, on Zulip):

let me now catch up on that thread

lqd (Feb 25 2020 at 20:10, on Zulip):

@Albin Stjerna I also wondered about another thing, correct me if I'm wrong but shouldn't we just stop the polonius process if we hit move errors (and would be able to bail, not needing to compute the borrowck and subset errors)

nikomatsakis (Feb 25 2020 at 20:10, on Zulip):

ok, so, in short you merged the work that @Albin Stjerna was doing, which is awesome

nikomatsakis (Feb 25 2020 at 20:10, on Zulip):

I am trying to remember...

nikomatsakis (Feb 25 2020 at 20:10, on Zulip):

...we had these "new versions of the polonius rules"

nikomatsakis (Feb 25 2020 at 20:10, on Zulip):

that we created at last sprint

nikomatsakis (Feb 25 2020 at 20:10, on Zulip):

and that also involved renamings and things

nikomatsakis (Feb 25 2020 at 20:10, on Zulip):

(a) where were we writing those rules up? some hackmd?

nikomatsakis (Feb 25 2020 at 20:10, on Zulip):

(b) have we moved them into the polonius book at all?

nikomatsakis (Feb 25 2020 at 20:11, on Zulip):

(c) have we merged the source code up to match those rules, and were we going to do a great renaming at some point?

Albin Stjerna (Feb 25 2020 at 20:11, on Zulip):

(a): yes, some hackmd, (b) not yet

lqd (Feb 25 2020 at 20:11, on Zulip):

(c) some of it, but maybe not everything

Albin Stjerna (Feb 25 2020 at 20:11, on Zulip):

(c) yes, in polonius!

nikomatsakis (Feb 25 2020 at 20:12, on Zulip):

@Albin Stjerna was that "yes" to both halves?

lqd (Feb 25 2020 at 20:12, on Zulip):

maybe not all of the existing rules though

lqd (Feb 25 2020 at 20:13, on Zulip):

for move errors at least it seems like it was

lqd (Feb 25 2020 at 20:13, on Zulip):

(the rustc PR is not merged yet)

Albin Stjerna (Feb 25 2020 at 20:14, on Zulip):

I'm planning to update the book with the new rules eventually

nikomatsakis (Feb 25 2020 at 20:15, on Zulip):

that would indeed be awesome

Albin Stjerna (Feb 25 2020 at 20:17, on Zulip):

It should be mostly copy + paste plus some verification

nikomatsakis (Feb 25 2020 at 20:17, on Zulip):

@lqd somewhere we have our kind of "master roadmap" hackmd, right?

lqd (Feb 25 2020 at 20:17, on Zulip):

yeah and we also clarified what needed to be done in addition to the rustc PR, to actually emit the move errors. still TBD on how to do that, but knowing is half the battle :)

nikomatsakis (Feb 25 2020 at 20:17, on Zulip):

side note

nikomatsakis (Feb 25 2020 at 20:17, on Zulip):

I wonder if we should move all these things to wiki pages on the polonius repo

nikomatsakis (Feb 25 2020 at 20:18, on Zulip):

so we don't have to keep fishing up these links

nikomatsakis (Feb 25 2020 at 20:18, on Zulip):

(also, I am tempted to try and port the roadmap to skill-tree, but that project still needs more work first probably)

lqd (Feb 25 2020 at 20:18, on Zulip):

nikomatsakis said:

lqd somewhere we have our kind of "master roadmap" hackmd, right?

yes, I can find the link, and it would need to be updated with the more recent work ofc

nikomatsakis (Feb 25 2020 at 20:18, on Zulip):

I'm mostly thinking that this would be helpful in determing a next sprint goal

nikomatsakis (Feb 25 2020 at 20:18, on Zulip):

i.e., are we now roughly at "feature parity" with borrow checker?

nikomatsakis (Feb 25 2020 at 20:19, on Zulip):

I guess that would be determined by looking at those test cases that don't match behavior

nikomatsakis (Feb 25 2020 at 20:19, on Zulip):

(I know some of them are due to OOM errors)

lqd (Feb 25 2020 at 20:19, on Zulip):

I think we're getting close

lqd (Feb 25 2020 at 20:19, on Zulip):

the polonius side has more parity than the rustc side

lqd (Feb 25 2020 at 20:19, on Zulip):

and there are those bugs indeed

lqd (Feb 25 2020 at 20:20, on Zulip):

(with the rustc PR as-is, we still won't emit the move errors that polonius computes)

nikomatsakis (Feb 25 2020 at 20:20, on Zulip):

ah

nikomatsakis (Feb 25 2020 at 20:20, on Zulip):

that seems imp't

lqd (Feb 25 2020 at 20:20, on Zulip):

right :upside_down:

lqd (Feb 25 2020 at 20:21, on Zulip):

I was looking into that but haven't made a lot of concrete progress yet, mostly looking around rustc

nikomatsakis (Feb 25 2020 at 20:21, on Zulip):

Polonius rules hackmd

nikomatsakis (Feb 25 2020 at 20:22, on Zulip):

Polonius mini input language hackmd -- I only vaguely remember what this was

lqd (Feb 25 2020 at 20:22, on Zulip):

we could put this rules doc in the book

nikomatsakis (Feb 25 2020 at 20:23, on Zulip):

I think we should, yes

nikomatsakis (Feb 25 2020 at 20:23, on Zulip):

maybe we should open an issue to add the rules doc into the book

lqd (Feb 25 2020 at 20:23, on Zulip):

yeah I'll do that

nikomatsakis (Feb 25 2020 at 20:23, on Zulip):

polonius roadmap dropbox paper

nikomatsakis (Feb 25 2020 at 20:24, on Zulip):

Ah, @lqd, so for placeholder loan support, how far did we get?

nikomatsakis (Feb 25 2020 at 20:24, on Zulip):

I see e.g. these notes

lqd (Feb 25 2020 at 20:24, on Zulip):

we did land those

lqd (Feb 25 2020 at 20:24, on Zulip):

both in polonius and rustc

nikomatsakis (Feb 25 2020 at 20:24, on Zulip):

I thought so, yeah

lqd (Feb 25 2020 at 20:25, on Zulip):

(in Polonius only in the Naive algo ofc)

nikomatsakis (Feb 25 2020 at 20:25, on Zulip):

hmm maybe I will try making a skill-tree for polonius :)

nikomatsakis (Feb 25 2020 at 20:25, on Zulip):

I feel like this is exactly the kind of context I wanted to capture and make easily visible

lqd (Feb 25 2020 at 20:25, on Zulip):

the latter hackmd is a document where we brainstormed how tests could look, to test more things in polonius itself, rather than mostly using rustc's tests

nikomatsakis (Feb 25 2020 at 20:25, on Zulip):

Ah, yes, right, there was this question around naive rules

nikomatsakis (Feb 25 2020 at 20:25, on Zulip):

lqd said:

the latter hackmd is a document where we brainstormed how tests could look, to test more things in polonius itself, rather than mostly using rustc's tests

right

nikomatsakis (Feb 25 2020 at 20:25, on Zulip):

nikomatsakis said:

Ah, yes, right, there was this question around naive rules

and in particular @lqd you had some optimizations that seemed to help a lot and be a lot simpler

nikomatsakis (Feb 25 2020 at 20:25, on Zulip):

it's all (well... some?) coming back to me now

nikomatsakis (Feb 25 2020 at 20:26, on Zulip):

and then there was the question of the "equivalence" relations

lqd (Feb 25 2020 at 20:26, on Zulip):

it did help but

nikomatsakis (Feb 25 2020 at 20:26, on Zulip):

seems like

Integrating move / overwrite analysis (a la Lark)

nikomatsakis (Feb 25 2020 at 20:26, on Zulip):

from the dropbox paper

nikomatsakis (Feb 25 2020 at 20:26, on Zulip):

is mostly checked

lqd (Feb 25 2020 at 20:26, on Zulip):
lqd (Feb 25 2020 at 20:26, on Zulip):
nikomatsakis (Feb 25 2020 at 20:26, on Zulip):

heh

lqd (Feb 25 2020 at 20:27, on Zulip):

but it's important in general

nikomatsakis (Feb 25 2020 at 20:27, on Zulip):

welll I still really want to work on completeness/correctness first

lqd (Feb 25 2020 at 20:27, on Zulip):

and will help move/init I think

lqd (Feb 25 2020 at 20:27, on Zulip):

right

nikomatsakis (Feb 25 2020 at 20:27, on Zulip):

but it does seem like we're getting quite close

nikomatsakis (Feb 25 2020 at 20:27, on Zulip):

outlives relations are basically...done?

nikomatsakis (Feb 25 2020 at 20:27, on Zulip):

do we report them from rustc?

lqd (Feb 25 2020 at 20:27, on Zulip):

and other work can still be done to compute which things we don't need to compute (heh) better

lqd (Feb 25 2020 at 20:28, on Zulip):

apart from the "equivalence" relations

lqd (Feb 25 2020 at 20:28, on Zulip):

regular outlives relations ?

lqd (Feb 25 2020 at 20:28, on Zulip):

(there's also the higher-rankedness which is huh interesting)

nikomatsakis (Feb 25 2020 at 20:29, on Zulip):

lqd said:

(there's also the higher-rankedness which is huh interesting)

yeah I'm ignoring that for the moment

nikomatsakis (Feb 25 2020 at 20:29, on Zulip):

I still think that should not be polonius's job

nikomatsakis (Feb 25 2020 at 20:29, on Zulip):

I think that chalk should handle it

lqd (Feb 25 2020 at 20:29, on Zulip):

yeah

nikomatsakis (Feb 25 2020 at 20:29, on Zulip):

I outlined some thoughts on that in #wg-traits at some point

lqd (Feb 25 2020 at 20:29, on Zulip):

yeah, with Matthew

nikomatsakis (Feb 25 2020 at 20:30, on Zulip):

#wg-traits > regions and universes

lqd (Feb 25 2020 at 20:30, on Zulip):

I think we're quite close, apart from emitting move errors which shouldn't be super hard, and unless I'm missing something it seems we did the first batch of what wanted to do wrt completeness goal

nikomatsakis (Feb 25 2020 at 20:31, on Zulip):

OK. Very exciting.

lqd (Feb 25 2020 at 20:31, on Zulip):

(+ various bugs/improvements apart from our other goals)

nikomatsakis (Feb 25 2020 at 20:31, on Zulip):

Well, maybe next meeting we can try to plan out our next sprint

nikomatsakis (Feb 25 2020 at 20:31, on Zulip):

I'd still like to get away from regular meetings

nikomatsakis (Feb 25 2020 at 20:31, on Zulip):

the context switch time is killing me

nikomatsakis (Feb 25 2020 at 20:31, on Zulip):

and try to have focused sprints instead at some frequency

lqd (Feb 25 2020 at 20:31, on Zulip):

we can also do that async if that's better

nikomatsakis (Feb 25 2020 at 20:31, on Zulip):

well, maybe, but then I sometimes wind up ignoring :)

lqd (Feb 25 2020 at 20:31, on Zulip):

where that = plan out the next sprint

nikomatsakis (Feb 25 2020 at 20:31, on Zulip):

but we can try

nikomatsakis (Feb 25 2020 at 20:32, on Zulip):

there's no perfect plan

nikomatsakis (Feb 25 2020 at 20:32, on Zulip):

anyway I am going to add a 'work item' to try making a skill-tree roadmap

nikomatsakis (Feb 25 2020 at 20:32, on Zulip):

just beacuse I want to try it and it'll help me to understand

nikomatsakis (Feb 25 2020 at 20:32, on Zulip):

though really the dropbox paper is good too

lqd (Feb 25 2020 at 20:32, on Zulip):

worst case you ignore till next meeting

nikomatsakis (Feb 25 2020 at 20:33, on Zulip):

do we have an up to date place listing the current discrepancies between polonius and rustc?

nikomatsakis (Feb 25 2020 at 20:33, on Zulip):

I guess I can run my own tests locally?

nikomatsakis (Feb 25 2020 at 20:34, on Zulip):

rustc tests: lqd has started an analysis of rustc’s test suite behaviour under -Zpolonius

nikomatsakis (Feb 25 2020 at 20:34, on Zulip):

:)

nikomatsakis (Feb 25 2020 at 20:34, on Zulip):

that's probably pretty old

nikomatsakis (Feb 25 2020 at 20:34, on Zulip):

I seem to recall you did that

lqd (Feb 25 2020 at 20:34, on Zulip):

yeah

nikomatsakis (Feb 25 2020 at 20:34, on Zulip):

(gotta run, I promised to sync with @pnkfelix 4 minutes ago :P)

lqd (Feb 25 2020 at 20:34, on Zulip):

so I had this document (I'm finding searching for hackmd links to be pretty difficult, with their titles sometimes missing)

lqd (Feb 25 2020 at 20:34, on Zulip):

I'll try to find those soon

nikomatsakis (Feb 25 2020 at 20:34, on Zulip):

yeah, it's important to give them titles

nikomatsakis (Feb 25 2020 at 20:35, on Zulip):

sometimes I search zulip

lqd (Feb 25 2020 at 20:35, on Zulip):

tests: we have one but I haven't updated since last time I updated rustc tests

lqd (Feb 25 2020 at 20:35, on Zulip):

I'll also look for it, but Albin has run those more recently, and seems like there were maybe 5 discrepancies

lqd (Feb 25 2020 at 20:38, on Zulip):

test discrepancies from October I'll update this soon with the most up to date results

lqd (Feb 25 2020 at 20:43, on Zulip):

slightly more recent roadmap/dump which I'll also need to update to include our more recent work e.g. on move errors — I feel it it has the information present in the dropbox paper and then some ?

lqd (Feb 25 2020 at 22:08, on Zulip):

@Albin Stjerna what do you want to with the rustc PR btw ? land as-is and then emit move errors in another PR ? or do both in the same PR ? (I'm not sure if I can push to it, but I have it built locally if that can save you a bit of time)

lqd (Feb 25 2020 at 22:18, on Zulip):

ah unfortunate, in the meantime someone re-did the same work to update to the new fact format in https://github.com/rust-lang/rust/pull/69470

Albin Stjerna (Feb 26 2020 at 07:30, on Zulip):

Except the new facts, but yes

Albin Stjerna (Feb 26 2020 at 07:31, on Zulip):

I think that more or less answers your question though; we should really Just Get It Merged

lqd (Feb 26 2020 at 09:25, on Zulip):

@Albin Stjerna I can rebase and format your commits in another PR (at lunch break)

Albin Stjerna (Feb 26 2020 at 09:35, on Zulip):

Excellent, please do!

Albin Stjerna (Feb 26 2020 at 09:36, on Zulip):

I expect to be pretty much swamped in the near future

lqd (Feb 26 2020 at 09:40, on Zulip):

alright, will do :)

lqd (Feb 26 2020 at 12:36, on Zulip):

@Albin Stjerna were you seeing 3 new test "failures" on the rustc PR (really, "unexpected pass" rather than failures per se) in the nll/maybe-initialized-drop-... tests: implicit-fragment-drop, with-fragment, with-uninitialized-fragment ?

lqd (Feb 26 2020 at 12:58, on Zulip):

I'll open the PR and we can talk about this later, I'll have to compare the tests in polonius under 0.11 and 0.12, but those new init/move facts might actually make those NLL maybe-initialized-drop tests "fixed by polonius" :thumbs_up:

lqd (Feb 26 2020 at 13:05, on Zulip):

https://github.com/rust-lang/rust/pull/69482

Albin Stjerna (Feb 26 2020 at 13:06, on Zulip):

I saw two unexpected passes according to the Zulip logs

Albin Stjerna (Feb 26 2020 at 13:06, on Zulip):

I’ll check when I’m home

lqd (Feb 26 2020 at 13:07, on Zulip):

ah https://rust-lang.zulipchat.com/#narrow/stream/186049-t-compiler.2Fwg-polonius/topic/meeting.202020.2E02.2E11/near/187949158 !

lqd (Feb 26 2020 at 13:08, on Zulip):

yes those 3:

[ui (polonius)] ui/nll/maybe-initialized-drop-implicit-fragment-drop.rs
[ui (polonius)] ui/nll/maybe-initialized-drop-with-fragment.rs
[ui (polonius)] ui/nll/maybe-initialized-drop-with-uninitialized-fragments.rs

are the 3 unexpected pass I'm seeing as well

lqd (Feb 26 2020 at 13:09, on Zulip):

of the other 4-5 failures, 99% are trivial diagnostics changes (like grammar or wording) which I'll bless in the future

lqd (Feb 28 2020 at 16:36, on Zulip):

yeah I was not present at the meeting where those :point_up: where discussed, so after checking them to update the test document, indeed it's only 2 unexpected pass bug fixes, and an unexpected pass bug which I'll need to investigate. In other news I've updated the test analysis document.

Aaron Weiss (Feb 28 2020 at 17:43, on Zulip):

The two unexpected passes (drop-implicit-fragment-drop and drop-with-unintialized-fragments) are both things that morally ought to be accepted, IMO.

lqd (Feb 28 2020 at 17:46, on Zulip):

yes that's why I was mentioning them as bug fixes -- that is, if the 3rd one is fixed, otherwise it's a bug in the move/init analysis hiding borrowck errors heh

lqd (Feb 28 2020 at 17:47, on Zulip):

since the 3 cases are so similar, it's a bit suspicious

Aaron Weiss (Feb 28 2020 at 17:50, on Zulip):

Ah, sorry, didn't quite understand what the phrase "unexpected pass bug fix" meant, but it makes sense now. :sweat_smile:

lqd (Feb 28 2020 at 17:50, on Zulip):

yeah sorry it wasn't super clear

Aaron Weiss (Feb 28 2020 at 17:52, on Zulip):

At least at a high level, I'm fairly sure Polonius _should_ be able to handle drop-with-fragment correctly (erroring) and the other two not. I recently finished (excepting issue 58053) getting all the borrowck and nll tests through my Oxide type checker implementation, and with provenances/origins, it works out on my end.

lqd (Feb 28 2020 at 17:52, on Zulip):

it's more likely a single bug (the 3rd one), which on such small similar test cases shows up as unexpected fixes

lqd (Feb 28 2020 at 17:53, on Zulip):

agreed

lqd (Feb 28 2020 at 17:53, on Zulip):

(whether this inconsistency is in our move/init analysis rules or input facts remains to be seen)

lqd (Feb 28 2020 at 17:55, on Zulip):

great news about oxide

lqd (Feb 28 2020 at 21:22, on Zulip):

my kingdom for why-not provenance

Last update: Apr 03 2020 at 18:10UTC