Stream: t-compiler/wg-polonius

Topic: meeting 2019.12.10


lqd (Dec 10 2019 at 20:00, on Zulip):

good evening :)

lqd (Dec 10 2019 at 20:01, on Zulip):

in case you haven't seen it, the great Mattew reviewed https://github.com/rust-lang/rust/pull/67016

lqd (Dec 10 2019 at 20:02, on Zulip):

and it landed, so we now have subset errors in rustc using -Zpolonius

nikomatsakis (Dec 10 2019 at 20:02, on Zulip):

:wave:

nikomatsakis (Dec 10 2019 at 20:03, on Zulip):

that's awesome!

nikomatsakis (Dec 10 2019 at 20:03, on Zulip):

I had not noticed, no

lqd (Dec 10 2019 at 20:03, on Zulip):

and (this one Albin has seen) I have been able to "replace" the work lokalmatador did on profiling, by adding a couple of new activities in -Z self-profile in https://github.com/rust-lang/rust/pull/67193

lqd (Dec 10 2019 at 20:03, on Zulip):

which the great Wesley has already reviewed

lqd (Dec 10 2019 at 20:04, on Zulip):

I was wondering if y'all thought we needed to differentiate profiling data (by def_id or something) right now ? or if this aggregation was already useful

nikomatsakis (Dec 10 2019 at 20:04, on Zulip):

hmm

nikomatsakis (Dec 10 2019 at 20:04, on Zulip):

IIRC

nikomatsakis (Dec 10 2019 at 20:04, on Zulip):

when I found hotspots

nikomatsakis (Dec 10 2019 at 20:05, on Zulip):

it was usually one function that dominated the time

nikomatsakis (Dec 10 2019 at 20:05, on Zulip):

which might argue for being able to differentiate

nikomatsakis (Dec 10 2019 at 20:05, on Zulip):

however, I feel like this is something that the timer would want to support more generically

lqd (Dec 10 2019 at 20:05, on Zulip):

@Albin Stjerna so yeah I remember you've been wanting to refactor more of fact generation, as mentioned in the PR, and this was mostly a cleanup of the existing one (in case you had conflicts in your existing PRs, or opinions about this one)

lqd (Dec 10 2019 at 20:05, on Zulip):

in fact it's going to yes

lqd (Dec 10 2019 at 20:05, on Zulip):

mw has been working on it apparently

nikomatsakis (Dec 10 2019 at 20:05, on Zulip):

also, what is the status of @Albin Stjerna's initialization work..? I see I have like 21 unread messages over in that topic

Albin Stjerna (Dec 10 2019 at 20:06, on Zulip):

Err

nikomatsakis (Dec 10 2019 at 20:06, on Zulip):

I want to land PRs!!

Albin Stjerna (Dec 10 2019 at 20:06, on Zulip):

/me has completely forgotten about those messages

Albin Stjerna (Dec 10 2019 at 20:06, on Zulip):

Oh those were off topic!

lqd (Dec 10 2019 at 20:06, on Zulip):

there's a WIP PR you can review niko, right Albin ? or did that need more work (beside testing, that is)

nikomatsakis (Dec 10 2019 at 20:06, on Zulip):

OK.

Albin Stjerna (Dec 10 2019 at 20:06, on Zulip):

Basically, we're waiting for me to get my behind in gear and rebase on @lqd's changes :)

Albin Stjerna (Dec 10 2019 at 20:06, on Zulip):

I think

nikomatsakis (Dec 10 2019 at 20:07, on Zulip):

I'm already getting back that feeling of "aaah can't remember where things were"

lqd (Dec 10 2019 at 20:07, on Zulip):

I think as well

nikomatsakis (Dec 10 2019 at 20:07, on Zulip):

it was nice when we did the sprint and I felt I had all the context at hand :)

Albin Stjerna (Dec 10 2019 at 20:07, on Zulip):

Yes, same

lqd (Dec 10 2019 at 20:07, on Zulip):

I'm hearing "polonius sprint 100% of the time"

nikomatsakis (Dec 10 2019 at 20:07, on Zulip):

lol YES

lqd (Dec 10 2019 at 20:07, on Zulip):

from now on :tada:

Albin Stjerna (Dec 10 2019 at 20:07, on Zulip):

It's even worse now because I write Scala now and it's similar enough to Rust to completely mess up my sense of both languages

nikomatsakis (Dec 10 2019 at 20:07, on Zulip):

there's a comment here that seems to summarize some state

nikomatsakis (Dec 10 2019 at 20:08, on Zulip):

I guess what I remember is

lqd (Dec 10 2019 at 20:08, on Zulip):

yes those were mostly for the parsing and testing

nikomatsakis (Dec 10 2019 at 20:08, on Zulip):

that over the sprint we kind of worked out what the rules "should be" in the hackmd

lqd (Dec 10 2019 at 20:08, on Zulip):

which can be seen as independent I feel

Albin Stjerna (Dec 10 2019 at 20:08, on Zulip):

I think so too

nikomatsakis (Dec 10 2019 at 20:08, on Zulip):

not sure how much that compared with what's in the PR

lqd (Dec 10 2019 at 20:08, on Zulip):

those new rules are in the PR right ?

Albin Stjerna (Dec 10 2019 at 20:08, on Zulip):

It should be the same now

nikomatsakis (Dec 10 2019 at 20:08, on Zulip):

there was that one sticking point about whether we had to track "any initialized subpath" or "just the variable" for the drop code

lqd (Dec 10 2019 at 20:08, on Zulip):

right, awesome

nikomatsakis (Dec 10 2019 at 20:08, on Zulip):

and I sort of remember that it probably didn't matter anyway

nikomatsakis (Dec 10 2019 at 20:09, on Zulip):

ok, great

Albin Stjerna (Dec 10 2019 at 20:09, on Zulip):

Yes, they should be the same, with the exception of the parent/child reverse relation

Albin Stjerna (Dec 10 2019 at 20:09, on Zulip):

That I insisted on :)

nikomatsakis (Dec 10 2019 at 20:09, on Zulip):

so I guess that in terms of review, I could try to compare the hackmd vs the PR and read that

nikomatsakis (Dec 10 2019 at 20:09, on Zulip):

ok :)

lqd (Dec 10 2019 at 20:09, on Zulip):

besides unit testing in polonius itself, as opposed to in rustc, this should be ready to review then ?

Albin Stjerna (Dec 10 2019 at 20:09, on Zulip):

and I sort of remember that it probably didn't matter anyway

You sort of convinced me to do the "less precise" one, but I'm still not fully convinced

Albin Stjerna (Dec 10 2019 at 20:09, on Zulip):

Anyway, that version is in the code now

Albin Stjerna (Dec 10 2019 at 20:10, on Zulip):

I'm really looking forward to the Christmas Holiday Sprint

lqd (Dec 10 2019 at 20:10, on Zulip):

@Albin Stjerna when you mention rebasing over my changes, you mean your init work on the rustc side, which goes with your open polonius PR ?

nikomatsakis (Dec 10 2019 at 20:11, on Zulip):

I feel the less precise one is "more correct", but I think I also convinced myself that it didn't matter in practice, because we of the limitations around how we allow initialization of subpaths etc

Albin Stjerna (Dec 10 2019 at 20:11, on Zulip):

@lqd Both really, also your work on polonius?

lqd (Dec 10 2019 at 20:11, on Zulip):

that is, there's no open PR for the rustc side yet, right ?

Albin Stjerna (Dec 10 2019 at 20:11, on Zulip):

Or maybe that isn't merged yet?

lqd (Dec 10 2019 at 20:11, on Zulip):

ah yes, right right

lqd (Dec 10 2019 at 20:11, on Zulip):

everything's merged now

Albin Stjerna (Dec 10 2019 at 20:11, on Zulip):

I don't even have an open PR for my rust changes yet I think

lqd (Dec 10 2019 at 20:12, on Zulip):

probably just in a branch yeah

lqd (Dec 10 2019 at 20:12, on Zulip):

at least you're not blocked on me so that's good

Albin Stjerna (Dec 10 2019 at 20:12, on Zulip):

Yes, and it's mostly a matter of emitting moves for variables at the start of each function

Albin Stjerna (Dec 10 2019 at 20:12, on Zulip):

No!

Albin Stjerna (Dec 10 2019 at 20:12, on Zulip):

I'm just blocked on time

lqd (Dec 10 2019 at 20:12, on Zulip):

a tough enemy

nikomatsakis (Dec 10 2019 at 20:13, on Zulip):

OK.

lqd (Dec 10 2019 at 20:14, on Zulip):

@nikomatsakis wrt to the WIP error, do you have thoughts on testing: would you rather we add all the missing facts in the parser and so on (possibly looking more like the old borrowck test syntax etc, to have paths etc etc) now ?

nikomatsakis (Dec 10 2019 at 20:14, on Zulip):

can we land the polonius PR?

nikomatsakis (Dec 10 2019 at 20:14, on Zulip):

what is the "WIP error"

lqd (Dec 10 2019 at 20:14, on Zulip):

dang

lqd (Dec 10 2019 at 20:14, on Zulip):

the WIP move errors PR I meant sorry

lqd (Dec 10 2019 at 20:15, on Zulip):

https://github.com/rust-lang/polonius/pull/135

nikomatsakis (Dec 10 2019 at 20:15, on Zulip):

yeah ok that's kind of what I was asking too

nikomatsakis (Dec 10 2019 at 20:15, on Zulip):

/me thinks

nikomatsakis (Dec 10 2019 at 20:15, on Zulip):

ok so there are sort of two things

nikomatsakis (Dec 10 2019 at 20:15, on Zulip):

first, creating tests that use facts generated by rustc

nikomatsakis (Dec 10 2019 at 20:16, on Zulip):

which I guess we can do with a WIP branch

nikomatsakis (Dec 10 2019 at 20:16, on Zulip):

second, being able to write tests that are standalone

nikomatsakis (Dec 10 2019 at 20:16, on Zulip):

which would involve adding things to the parser?

lqd (Dec 10 2019 at 20:16, on Zulip):

right

nikomatsakis (Dec 10 2019 at 20:16, on Zulip):

I do think we should create a better "unit test" language, more like the old thing

nikomatsakis (Dec 10 2019 at 20:16, on Zulip):

I'm not sure if you've put any thought into what it might look like, that could be a useful exercise

lqd (Dec 10 2019 at 20:17, on Zulip):

just adding those relations is relatively easy, the better unit test language is a bit more involved than just adding raw facts support to the parser

nikomatsakis (Dec 10 2019 at 20:17, on Zulip):

but it seems like we're going to want to be able to distill tests and patterns into something readable

nikomatsakis (Dec 10 2019 at 20:17, on Zulip):

right

Albin Stjerna (Dec 10 2019 at 20:17, on Zulip):

But I guess the more advanced language would still be syntactic sugar for the same thing?

lqd (Dec 10 2019 at 20:17, on Zulip):

yeah

nikomatsakis (Dec 10 2019 at 20:17, on Zulip):

we probably want both

Albin Stjerna (Dec 10 2019 at 20:17, on Zulip):

So it might not me completely wasted work to spend some time writing base facts

lqd (Dec 10 2019 at 20:17, on Zulip):

absolutely, to the both of you

nikomatsakis (Dec 10 2019 at 20:18, on Zulip):

that is, I'm sort of imagining it'd be nice to be able to "hand specify" the input facts in a precise way

nikomatsakis (Dec 10 2019 at 20:18, on Zulip):

but also have some short-hand

lqd (Dec 10 2019 at 20:18, on Zulip):

I'll try adding the quicker ones soon

lqd (Dec 10 2019 at 20:19, on Zulip):

as I haven't seen the others, say, the paths but maybe it's straightforward

nikomatsakis (Dec 10 2019 at 20:19, on Zulip):

we could take 10 minutes to sketch what it might look like

nikomatsakis (Dec 10 2019 at 20:19, on Zulip):

the nicer version, I mean

lqd (Dec 10 2019 at 20:19, on Zulip):

the better unit test language you mean

nikomatsakis (Dec 10 2019 at 20:19, on Zulip):

or maybe it's not a good use of this time

lqd (Dec 10 2019 at 20:19, on Zulip):

:)

lqd (Dec 10 2019 at 20:20, on Zulip):

so for reference your ~old~ prior syntax was https://github.com/nikomatsakis/borrowck/tree/master/test

nikomatsakis (Dec 10 2019 at 20:21, on Zulip):

yeah

nikomatsakis (Dec 10 2019 at 20:21, on Zulip):

one question mark would be how much of a "type system" we want

nikomatsakis (Dec 10 2019 at 20:21, on Zulip):

I remember wrestling with this

lqd (Dec 10 2019 at 20:22, on Zulip):

https://github.com/nikomatsakis/borrowck/blob/master/test/borrowck-write-struct-containing-mutable-ref-whose-referent-is-mutably-borrowed.nll seems representative

nikomatsakis (Dec 10 2019 at 20:23, on Zulip):

I think we probably do want the ability to declare "structs"

nikomatsakis (Dec 10 2019 at 20:23, on Zulip):

so that you can write things like a.b.c = foo and it can figure out the type relationships from that

lqd (Dec 10 2019 at 20:24, on Zulip):

albeit without assertions here but that reminds me, were those good ? would we want them in the "program" like this language has ?

nikomatsakis (Dec 10 2019 at 20:24, on Zulip):

hackmd for polonius mini input language

nikomatsakis (Dec 10 2019 at 20:24, on Zulip):

I don't think I liked the assertions that much in the end

nikomatsakis (Dec 10 2019 at 20:24, on Zulip):

well it may be useful to be able to add some of them

lqd (Dec 10 2019 at 20:24, on Zulip):

yeah

lqd (Dec 10 2019 at 20:25, on Zulip):

as long as we can do arbitrary assertions in the rust unit tests, the more common ones can be available in the language as well

nikomatsakis (Dec 10 2019 at 20:26, on Zulip):

maybe the 'one big function' setup was good

lqd (Dec 10 2019 at 20:26, on Zulip):

(especially here as sometimes we're testing "temporary" relations when we're checking a computation, and sometimes a blackbox-y "check only the output")

nikomatsakis (Dec 10 2019 at 20:27, on Zulip):

Yeah, I think in general "black-box" is better

Albin Stjerna (Dec 10 2019 at 20:27, on Zulip):

maybe the 'one big function' setup was good

I guess that depends on whether we want to test things that involve multiple functions?

nikomatsakis (Dec 10 2019 at 20:27, on Zulip):

Well, I think you want to be able to provide "prototypes" probably

nikomatsakis (Dec 10 2019 at 20:27, on Zulip):

for fns that could get called

nikomatsakis (Dec 10 2019 at 20:27, on Zulip):

but only one fn body

lqd (Dec 10 2019 at 20:28, on Zulip):

we mostly test one function body today

nikomatsakis (Dec 10 2019 at 20:29, on Zulip):

yeah I mean polonius is always testing one function at a time thus far

lqd (Dec 10 2019 at 20:29, on Zulip):

yeah

lqd (Dec 10 2019 at 20:30, on Zulip):

did y'all think about closures when talking about multiple functions or multiple prototypes ?

nikomatsakis (Dec 10 2019 at 20:31, on Zulip):

not really, closures are (at least right now...) mostly handled 'outside'

nikomatsakis (Dec 10 2019 at 20:31, on Zulip):

i.e., polonius doesn't have to know about them

nikomatsakis (Dec 10 2019 at 20:31, on Zulip):

right?

lqd (Dec 10 2019 at 20:31, on Zulip):

it's my understanding :)

lqd (Dec 10 2019 at 20:32, on Zulip):

I think the older syntax modeled variance ?

lqd (Dec 10 2019 at 20:33, on Zulip):

https://github.com/nikomatsakis/borrowck/blob/master/test/borrowck-walk-linked-list.nll is cute

nikomatsakis (Dec 10 2019 at 20:34, on Zulip):

I think the older syntax modeled variance ?

yes it did

nikomatsakis (Dec 10 2019 at 20:34, on Zulip):

it needed to in order to get T1 <: T2 correct

nikomatsakis (Dec 10 2019 at 20:34, on Zulip):

probably we need that too

nikomatsakis (Dec 10 2019 at 20:35, on Zulip):

well from this sketch it's pretty clear this is a "non-trivial" effort

nikomatsakis (Dec 10 2019 at 20:35, on Zulip):

not super hard

nikomatsakis (Dec 10 2019 at 20:35, on Zulip):

but it'll take some time

nikomatsakis (Dec 10 2019 at 20:35, on Zulip):

might be nice to try and write-up some tests for interesting scenarios

nikomatsakis (Dec 10 2019 at 20:36, on Zulip):

and see what's missing

lqd (Dec 10 2019 at 20:36, on Zulip):

do you happen to remember what you didn't like with it ? it seems likely we can reuse some/a lot from it

nikomatsakis (Dec 10 2019 at 20:36, on Zulip):

I'm trying to remember

lqd (Dec 10 2019 at 20:36, on Zulip):

yeah, agreed, seems like a bit of work :)

nikomatsakis (Dec 10 2019 at 20:36, on Zulip):

I remember having this feeling that it needed a bit more high-level stuff

nikomatsakis (Dec 10 2019 at 20:36, on Zulip):

e.g., it'd be nice to be able to write foo(a, b) and have it figure out the proper relations from that

nikomatsakis (Dec 10 2019 at 20:36, on Zulip):

also that I kind of started with something super minimal and glued a few things onto it and it was starting to feel hodge-podgy

lqd (Dec 10 2019 at 20:36, on Zulip):

question is how deep we need to go now

nikomatsakis (Dec 10 2019 at 20:36, on Zulip):

but I can't remember exactly why

lqd (Dec 10 2019 at 20:37, on Zulip):

as at the time you didn't have the NLL test corpus in rustc

nikomatsakis (Dec 10 2019 at 20:37, on Zulip):

yeah

lqd (Dec 10 2019 at 20:37, on Zulip):

I can probably start this with the basis of the older language and the hackmd (wow you've written a lot <3)

lqd (Dec 10 2019 at 20:37, on Zulip):

and then we can iterate as needed

nikomatsakis (Dec 10 2019 at 20:38, on Zulip):

I'm not sure how much to prioritize but

lqd (Dec 10 2019 at 20:38, on Zulip):

we don't need to block the PR on that tho

nikomatsakis (Dec 10 2019 at 20:38, on Zulip):

it does seem like if we want to write unit tests

nikomatsakis (Dec 10 2019 at 20:38, on Zulip):

we're going to want this

lqd (Dec 10 2019 at 20:38, on Zulip):

yeah

nikomatsakis (Dec 10 2019 at 20:38, on Zulip):

I wonder @lqd if you could start with some of the scenarios you wanted to write

nikomatsakis (Dec 10 2019 at 20:38, on Zulip):

and try to "model them" the way you'd want to write it so to speak

lqd (Dec 10 2019 at 20:38, on Zulip):

sure

nikomatsakis (Dec 10 2019 at 20:38, on Zulip):

one thing that's missing (e.g.) is that this doesn't have type parametesr on the function declaration

nikomatsakis (Dec 10 2019 at 20:38, on Zulip):

e.g. to model fn foo<'a, 'b: 'a> etc

lqd (Dec 10 2019 at 20:39, on Zulip):

(I think Albin had more use cases since we talked about it for the WIP PR)

lqd (Dec 10 2019 at 20:39, on Zulip):

we need rustc -Znll-facts !

nikomatsakis (Dec 10 2019 at 20:40, on Zulip):

don't we have that?

nikomatsakis (Dec 10 2019 at 20:40, on Zulip):

/me confused

lqd (Dec 10 2019 at 20:40, on Zulip):

not in a polonius unit test :)

nikomatsakis (Dec 10 2019 at 20:40, on Zulip):

I mean it is another option, as an aside

nikomatsakis (Dec 10 2019 at 20:40, on Zulip):

that we could invoke rustc to generate facts

nikomatsakis (Dec 10 2019 at 20:40, on Zulip):

and write the "unit tests" in pure rust

nikomatsakis (Dec 10 2019 at 20:40, on Zulip):

but I feel like there is some value in having this simplified model

nikomatsakis (Dec 10 2019 at 20:40, on Zulip):

maybe not that much though :)

lqd (Dec 10 2019 at 20:40, on Zulip):

it'd help with validation, but not really with new facts ofc

nikomatsakis (Dec 10 2019 at 20:41, on Zulip):

yeah, that's part of the problem

nikomatsakis (Dec 10 2019 at 20:41, on Zulip):

ok, I gotta go finish up a few other things

lqd (Dec 10 2019 at 20:41, on Zulip):

I don't expect us to add a million more, that being said

nikomatsakis (Dec 10 2019 at 20:41, on Zulip):

indeed, one hopes that this will slow down

lqd (Dec 10 2019 at 20:41, on Zulip):

oh right, it's 40mins in

lqd (Dec 10 2019 at 20:41, on Zulip):

thanks a lot @Albin Stjerna and @nikomatsakis :)

lqd (Dec 10 2019 at 20:42, on Zulip):

I'll try to work on this this week

lqd (Dec 10 2019 at 20:42, on Zulip):

(having "pure rust" unit tests would also help ensure the rustc driver has access to the facts, like Vytautas needed)

lqd (Dec 10 2019 at 20:43, on Zulip):

(for one of Niko's great ideas)

Last update: Jan 28 2020 at 01:15UTC