Stream: t-compiler/wg-polonius

Topic: meeting 2019.09.17


Albin Stjerna (Sep 17 2019 at 08:13, on Zulip):

Hi everyone! I am probably not going to be able to attend the meeting, but I figured I could write a quick report anyway. I'm mainly working on the presentation for my thesis and [non-Polonius stuff]. Once The Great Renaming and my Other Things have settled down, I figure I'll go into fixing Niko's concerns about initialisation to make the tracking of move paths precise. For that, I would need some way to do verification, for example the Rust unit tests with Polonius (that I don't know how to run).

After that comes move errors, which I have code for in pencil on a sheet of paper somewhere. To unblock that would also require some way of verifying it (passing the results on to rustc and running the compiler's unit tests?), and a decision on how to report errors that are not invalidation x live loans-errors (that is, the current set of errors). Of course, I can just make something up and fix it retroactively.

Other things I would like to work on in the reasonably near future is:

lqd (Sep 17 2019 at 11:30, on Zulip):

those are all of great interest and very useful :thumbs_up:

lqd (Sep 17 2019 at 11:30, on Zulip):

(also I like that The Great Renaming™ terminology is catching on ;)

lqd (Sep 17 2019 at 18:28, on Zulip):

@nikomatsakis I see you're firefighting some async issues, do you need to skip today's meeting ?

lqd (Sep 17 2019 at 19:01, on Zulip):

hello friends from @WG-polonius :wave: — Albin mentioned they might not attend so it's likely going to be fairly sparse in here :)

lqd (Sep 17 2019 at 19:02, on Zulip):

I'll give my update about this week so at least people can ready about it async

lqd (Sep 17 2019 at 19:03, on Zulip):

I was supposed to read Albin's thesis and give feedback but I didn't manage to do so

nikomatsakis (Sep 17 2019 at 19:03, on Zulip):

:wave:

lqd (Sep 17 2019 at 19:03, on Zulip):

hey niko :)

nikomatsakis (Sep 17 2019 at 19:03, on Zulip):

Yeah, I don't have a ton to report -- I talked to @lqd some last week and brought myself up to speed on what they'd done on equality -- I hope to put in a bit more time this week to look at subset errors

nikomatsakis (Sep 17 2019 at 19:03, on Zulip):

oh I forgot about my PR proposing names

nikomatsakis (Sep 17 2019 at 19:04, on Zulip):

I have some unread messages in this stream :)

lqd (Sep 17 2019 at 19:04, on Zulip):

one or two at most :)

lqd (Sep 17 2019 at 19:04, on Zulip):

so I'll continue, I have I think a good enough overview of inputs to be reviewed

lqd (Sep 17 2019 at 19:04, on Zulip):

as for naming I have started renaming regions to origins

lqd (Sep 17 2019 at 19:05, on Zulip):

(I'll add all the links later)

lqd (Sep 17 2019 at 19:05, on Zulip):

I've updated the current status of the rustc test suite, and opened a PR on the trivial cases

lqd (Sep 17 2019 at 19:05, on Zulip):

doing so I found there was a new OOM, which I also investigated

lqd (Sep 17 2019 at 19:06, on Zulip):

and it's very similar to the previous one, and also what we experienced with NLLs

lqd (Sep 17 2019 at 19:06, on Zulip):

e.g. here a lot of arguments/temporary variables coming from assert_eq! and the likes

lqd (Sep 17 2019 at 19:07, on Zulip):

and that's pretty much it :)

lqd (Sep 17 2019 at 19:07, on Zulip):

I plan to continue on The Great Renaming this week, adopting the new nomenclature in the "polonius inputs" doc and opening a PR for that

lqd (Sep 17 2019 at 19:08, on Zulip):

and read Albin's thesis

nikomatsakis (Sep 17 2019 at 19:11, on Zulip):

thanks @lqd :heart:

lqd (Sep 17 2019 at 19:11, on Zulip):

:)

nikomatsakis (Sep 17 2019 at 19:11, on Zulip):

Sounds like we should land https://github.com/rust-lang/polonius/pull/124 ?

lqd (Sep 17 2019 at 19:11, on Zulip):

(I've added links the previous messages in case)

lqd (Sep 17 2019 at 19:12, on Zulip):

yeah let's do it

lqd (Sep 17 2019 at 19:12, on Zulip):

I'll get used to Nodes vs Points ;)

nikomatsakis (Sep 17 2019 at 19:12, on Zulip):

done

nikomatsakis (Sep 17 2019 at 19:12, on Zulip):

yeah, hmm, we'll see if I can

nikomatsakis (Sep 17 2019 at 19:12, on Zulip):

that is probably the least important one, I'd be fine to revert it, as long as we avoid single-letter names

nikomatsakis (Sep 17 2019 at 19:12, on Zulip):

which I think we sort of agreed to do anyway

lqd (Sep 17 2019 at 19:13, on Zulip):

about thos single letter names

nikomatsakis (Sep 17 2019 at 19:13, on Zulip):

I see @lqd you opened polonius#125

lqd (Sep 17 2019 at 19:13, on Zulip):

was it about them in generic types ?

lqd (Sep 17 2019 at 19:13, on Zulip):

or variables as well

nikomatsakis (Sep 17 2019 at 19:13, on Zulip):

mm I don't know, I was thinking also in the book

nikomatsakis (Sep 17 2019 at 19:13, on Zulip):

e.g., in "datalog rules"

nikomatsakis (Sep 17 2019 at 19:13, on Zulip):

I guess everywhere :)

lqd (Sep 17 2019 at 19:14, on Zulip):

:)

nikomatsakis (Sep 17 2019 at 19:14, on Zulip):

was it about them in generic types ?

I'm always unsure about this -- single letters are sometimes kind of nice to clearly separate out "generics", but I can't see a good argument for it

lqd (Sep 17 2019 at 19:14, on Zulip):

so for L0 I should eg switch to Loan0 everywhere ? comments, datafrog closures, etc ?

nikomatsakis (Sep 17 2019 at 19:14, on Zulip):

yeah, like that

nikomatsakis (Sep 17 2019 at 19:14, on Zulip):

Loan0 seems sort of strictly better, no?

lqd (Sep 17 2019 at 19:15, on Zulip):

surely :)

lqd (Sep 17 2019 at 19:15, on Zulip):

alright I'll take care of this this week then

lqd (Sep 17 2019 at 19:16, on Zulip):

Albin also posted an interesting message at the top of this thread about possible tasks we'd need to do

lqd (Sep 17 2019 at 19:17, on Zulip):

but in general we can talk more about this async for sure

lqd (Sep 17 2019 at 19:17, on Zulip):

these and the other ongoing topics

lqd (Sep 17 2019 at 19:22, on Zulip):

looks like we're close to the end, if so thank you for your time everyone :) have a nice evening/afternoon :wave:

lqd (Sep 17 2019 at 19:23, on Zulip):

(I'll still be around)

Last update: Nov 15 2019 at 20:45UTC