Stream: t-compiler/wg-polonius

Topic: sprint coordination Aug 3 to Aug 5


nikomatsakis (Aug 03 2020 at 13:29, on Zulip):

Let's use this stream to coordinate activities during the sprint?

lqd (Aug 03 2020 at 13:30, on Zulip):

yes :) cc @Albin Stjerna

nikomatsakis (Aug 03 2020 at 13:30, on Zulip):

lqd said:

as for agenda, what I had in mind was:

nikomatsakis (Aug 03 2020 at 13:30, on Zulip):

I'd be curious to get a bit of an update from @lqd on the status of things, I saw mention of "datapond" which I take it is the "datalog-to-datafrog" compiler you were hacking on?

lqd (Aug 03 2020 at 13:31, on Zulip):

exactly

lqd (Aug 03 2020 at 13:31, on Zulip):

so here goes

nikomatsakis (Aug 03 2020 at 13:31, on Zulip):

master hackmd with polonius rules -- is this still up to date?

lqd (Aug 03 2020 at 13:32, on Zulip):

I think so yes

lqd (Aug 03 2020 at 13:32, on Zulip):

although the code itself doesn't all have the new naming from the hackmd

nikomatsakis (Aug 03 2020 at 13:32, on Zulip):

(not to interrupt, I'm wondering if a good 1st step would be trying to create a skill-tree sort of thing for polonius)

nikomatsakis (Aug 03 2020 at 13:32, on Zulip):

anyway, carry on

lqd (Aug 03 2020 at 13:32, on Zulip):

status: all in all we're not far from a MVP of sorts, but some issues remain:

lqd (Aug 03 2020 at 13:33, on Zulip):

1) move errors: polonius emits them, but rustc doesn't read what polonius emits nor emits them

lqd (Aug 03 2020 at 13:34, on Zulip):
lqd (Aug 03 2020 at 13:35, on Zulip):
lqd (Aug 03 2020 at 13:36, on Zulip):
lqd (Aug 03 2020 at 13:37, on Zulip):

(- I remember while you and Albin were coming up with the rules for move errors last sprint, at some point you mentioned some possible mismatch between datalog and a regular dataflow computation for init/unit variables, so it may cause the inefficiency problem you had anticipated)

nikomatsakis (Aug 03 2020 at 13:38, on Zulip):

hmm ok :)

nikomatsakis (Aug 03 2020 at 13:38, on Zulip):

I'm sure it'll come back to me

lqd (Aug 03 2020 at 13:38, on Zulip):

I recall something about intersections of sets

lqd (Aug 03 2020 at 13:39, on Zulip):

but not important

lqd (Aug 03 2020 at 13:39, on Zulip):

2) subset errors: last time we did the implementation using placeholder loans

lqd (Aug 03 2020 at 13:40, on Zulip):
lqd (Aug 03 2020 at 13:40, on Zulip):
lqd (Aug 03 2020 at 13:40, on Zulip):

(- I have prototypes for both of these)

lqd (Aug 03 2020 at 13:41, on Zulip):
Albin Stjerna (Aug 03 2020 at 13:41, on Zulip):

I remember that we talked about the discrepancy on partial initialisation

lqd (Aug 03 2020 at 13:42, on Zulip):

oops I forgot that

Albin Stjerna (Aug 03 2020 at 13:42, on Zulip):

But Helpful Person I Forget Their Name Now submitted a patch for that, right?

nikomatsakis (Aug 03 2020 at 13:43, on Zulip):

lqd said:

I wonder if @Aaron Weiss is around

lqd (Aug 03 2020 at 13:43, on Zulip):

utaal definitely opened an issue, let me find it

lqd (Aug 03 2020 at 13:43, on Zulip):

https://github.com/rust-lang/polonius/issues/152

lqd (Aug 03 2020 at 13:44, on Zulip):

with their own prototype for that indeed (which I haven't had the time to look at)

nikomatsakis (Aug 03 2020 at 13:45, on Zulip):

sprint planning doc

lqd (Aug 03 2020 at 13:46, on Zulip):
lqd (Aug 03 2020 at 13:48, on Zulip):

3) OOMs during fact generation:

lqd (Aug 03 2020 at 13:49, on Zulip):
nikomatsakis (Aug 03 2020 at 13:50, on Zulip):

yeah, that's kind of a pain I imagine since it'll require some duplication of datalog rules

nikomatsakis (Aug 03 2020 at 13:50, on Zulip):

(I wonder if we could extend datafrog somewhat to avoid that...)

lqd (Aug 03 2020 at 13:50, on Zulip):
lqd (Aug 03 2020 at 13:51, on Zulip):

yes it's indeed duplicating some rules

lqd (Aug 03 2020 at 13:52, on Zulip):

the opt variant being the harder one and with the most duplication, the Naive one is less complicated, and the location insensitive one is of course trivial as this is just an outlives relation without points, which is what location insensitivity is all about :)

nikomatsakis (Aug 03 2020 at 13:52, on Zulip):

ah yes so that's another question I remember now

nikomatsakis (Aug 03 2020 at 13:53, on Zulip):

whether the opt variant "carries its weight", especially now

nikomatsakis (Aug 03 2020 at 13:53, on Zulip):

and whether it would be better replaced with location-insensitivity-based optimizations

nikomatsakis (Aug 03 2020 at 13:53, on Zulip):

(and/or, as you point out, perhaps a non-datalog based impl)

lqd (Aug 03 2020 at 13:53, on Zulip):

it's an interesting question

nikomatsakis (Aug 03 2020 at 13:54, on Zulip):

I'm somewhat inclined to remove it except if that means that we just can't run tests in practice, that'd be kind of a drag

lqd (Aug 03 2020 at 13:54, on Zulip):

I think it's obviously better than the naive one

lqd (Aug 03 2020 at 13:55, on Zulip):

I'm not sure we can afford to not limit the transitive closures like it does, but there may be different ways for that indeed

nikomatsakis (Aug 03 2020 at 13:55, on Zulip):

ok so I tried to take down the points you mentioned in the sprint tracking doc

nikomatsakis (Aug 03 2020 at 13:56, on Zulip):

I threw in a few notes at the end of my own :)

lqd (Aug 03 2020 at 13:56, on Zulip):

I'm sure we need location insensitivity at the very least the location insensitive analysis is important

nikomatsakis (Aug 03 2020 at 13:56, on Zulip):

right, I think the question is whether naive+insensitive is competitive with the opt variant

lqd (Aug 03 2020 at 13:56, on Zulip):

that being said, I've prototyped transforming the location insensitive analysis with a bunch of graph traversal queries and it is much faster

lqd (Aug 03 2020 at 13:57, on Zulip):

I'm not sure, and the problem is that there's a bit of uncertainty about benchmarks

nikomatsakis (Aug 03 2020 at 13:57, on Zulip):

ah, I rememeber some longer term questions as well

lqd (Aug 03 2020 at 13:57, on Zulip):

that is, clap is huge, and "accepted" by the pre-pass, that is, there are no potential errors

nikomatsakis (Aug 03 2020 at 13:57, on Zulip):

e.g we never settled the precise rules around invariance

nikomatsakis (Aug 03 2020 at 13:58, on Zulip):

nikomatsakis said:

right, I think the question is whether naive+insensitive is competitive with the opt variant

I guess when I ask this what I really mean is "can you run the rustc test suite in reasnable time"

nikomatsakis (Aug 03 2020 at 13:58, on Zulip):

that is to say, I'm sure it's not production quality

lqd (Aug 03 2020 at 13:58, on Zulip):

the problem right now is that move errors heavily skew that timing

nikomatsakis (Aug 03 2020 at 13:59, on Zulip):

I'm just concerned that maintaining multiple sets of rules is slowing us down on settling what the rules should be

lqd (Aug 03 2020 at 13:59, on Zulip):

right, and that's not even talking about the equality variant :)

nikomatsakis (Aug 03 2020 at 13:59, on Zulip):

yeah, so maybe the answer is that (a) we should get the move error reporting working and (b) see if we can do some simple optimizations (e.g., location insensitive) to optimize it

nikomatsakis (Aug 03 2020 at 13:59, on Zulip):

yes, it's that question thatI have in mind

nikomatsakis (Aug 03 2020 at 13:59, on Zulip):

I guess that before we get to optimizing I'd like to settle the equality variant, partial init, and other outstanding questions

nikomatsakis (Aug 03 2020 at 14:00, on Zulip):

and I think we all agree datalog is still a useful way to formulate the rules at least

nikomatsakis (Aug 03 2020 at 14:00, on Zulip):

(i.e., as a "reference impl")

lqd (Aug 03 2020 at 14:00, on Zulip):

at this point I'm wondering if we should even be computing move errors in datalog, rather than say using rustc dataflow framework, or even maybe computing them at all in polonius ?

nikomatsakis (Aug 03 2020 at 14:01, on Zulip):

I guess it's a fair question.

nikomatsakis (Aug 03 2020 at 14:01, on Zulip):

I wanted to have "all of the borrow checker" in polonius, but I'm not sure I can justify that

lqd (Aug 03 2020 at 14:01, on Zulip):

it's a nice idea and has many benefits

nikomatsakis (Aug 03 2020 at 14:02, on Zulip):

I guess I still believe that datalog can be made competitive, but that's not based on a lot of elbow grease :)

lqd (Aug 03 2020 at 14:02, on Zulip):

I do wonder about that as well

lqd (Aug 03 2020 at 14:02, on Zulip):

I remember Yannis not having a magic fix right ? :)

nikomatsakis (Aug 03 2020 at 14:03, on Zulip):

no, but tbh it's always been a bit hard to really "hand off" the question, I think in part because the rules were not written up in a way that let us easily communicate them to other researchers somehow

nikomatsakis (Aug 03 2020 at 14:03, on Zulip):

I do kind of feel like "hard to read datalog" is not obviously a win

lqd (Aug 03 2020 at 14:03, on Zulip):

sure

nikomatsakis (Aug 03 2020 at 14:04, on Zulip):

but if we're talking about a "reference implementation", I do see value in having it contain the entire borrow checker

nikomatsakis (Aug 03 2020 at 14:04, on Zulip):

still, in the interest of focusing on the most important things, I can see an argument for saying "ignore move errors"

lqd (Aug 03 2020 at 14:04, on Zulip):

there are quite a few frameworks using datalog points-to analyses, and there doesn't seem, to my recollection, to be one that is "fast"

nikomatsakis (Aug 03 2020 at 14:04, on Zulip):

there are many that claim to scale to very large codebases, but it's always hard to evaluate those claims

lqd (Aug 03 2020 at 14:05, on Zulip):

right that's what I wanted to mention as well, how can we carve a path to the answers we need most

lqd (Aug 03 2020 at 14:06, on Zulip):

which in my mind are:

Aaron Weiss (Aug 03 2020 at 14:06, on Zulip):

nikomatsakis said:

lqd said:

  • I'm not sure we should be using placeholder loans vs rules about subsets

I wonder if Aaron Weiss is around

I am now!
nikomatsakis (Aug 03 2020 at 14:06, on Zulip):

@lqd "those rules" refers to all of the rules?

nikomatsakis (Aug 03 2020 at 14:06, on Zulip):

I think my impression of the "move error" rules is that there aren't that many "open questions"

nikomatsakis (Aug 03 2020 at 14:07, on Zulip):

there is engineering effort

Albin Stjerna (Aug 03 2020 at 14:07, on Zulip):

I also remember talking to Yannis at SPLASH about my move error rules, and he said he'd look at them in case I could package something up, but I felt I never reached a state where I felt they wre "done enough" to talk to him about

nikomatsakis (Aug 03 2020 at 14:07, on Zulip):

it seems like there are more open questions around the lifetime phase of the analysis

lqd (Aug 03 2020 at 14:07, on Zulip):

yeah, sorry mostly the ones related to the polonius analysis, with the Naive variant we have, compared to the Equality variant

lqd (Aug 03 2020 at 14:08, on Zulip):

that is, the impact they have on rust code

nikomatsakis (Aug 03 2020 at 14:08, on Zulip):

right, it seems like the question of:

nikomatsakis (Aug 03 2020 at 14:08, on Zulip):

those are not entirely well understood

lqd (Aug 03 2020 at 14:08, on Zulip):

exactly

nikomatsakis (Aug 03 2020 at 14:09, on Zulip):

still I feel like I'm not ready to cut out the move errors yet -- we're kind of "so close" with them :P

lqd (Aug 03 2020 at 14:09, on Zulip):

and to then quantify the costs, both in our development time, but also the runtime of the analysis over whichever benchmarks

nikomatsakis (Aug 03 2020 at 14:11, on Zulip):

how hard would it be to have an option to not do the move computation

nikomatsakis (Aug 03 2020 at 14:11, on Zulip):

I'm trying to remember the interface, I remember we had some kind of hacks before that we were able to remove I guess

lqd (Aug 03 2020 at 14:11, on Zulip):

we did have such an implementation before the current PR

nikomatsakis (Aug 03 2020 at 14:12, on Zulip):

right

lqd (Aug 03 2020 at 14:12, on Zulip):

it was mostly temporary to prepare for the move errors computation in polonius, and I'm not sure how it performed but it's doable as Albin did do it :)

Aaron Weiss (Aug 03 2020 at 14:12, on Zulip):

Sorry took me a bit to install Zulip mobile app since the webapp on mobile is very hard to use. re: placeholder loans vs subsets, Oxide in its latest rendition (which I’m going to push to arXiv tomorrow when I have internet again) fell on what I think would count as rules about subsets.

nikomatsakis (Aug 03 2020 at 14:12, on Zulip):

interesting

nikomatsakis (Aug 03 2020 at 14:13, on Zulip):

maybe @lqd the right approach would be to focus on those two questions, and in general the subset analysis, but defer the question of the move analysis a bit

nikomatsakis (Aug 03 2020 at 14:14, on Zulip):

I guess the question is whether some action on move errors is blocking other progress

lqd (Aug 03 2020 at 14:14, on Zulip):

we can disable parts of the computation on the polonius side, so it's not super blocking

lqd (Aug 03 2020 at 14:14, on Zulip):

(it computes both move errors and some init/uninit state used for liveness)

nikomatsakis (Aug 03 2020 at 14:15, on Zulip):

there's definitely something appealing about having the entirety (or almost...) of the borrow check fit in one hackmd...

nikomatsakis (Aug 03 2020 at 14:15, on Zulip):

lqd said:

(it computes both move errors and some init/uninit state used for liveness)

right

nikomatsakis (Aug 03 2020 at 14:16, on Zulip):

I was just skimming over the rules to bring them back in mind

lqd (Aug 03 2020 at 14:16, on Zulip):

move errors aren't really borrow checking right ;)

nikomatsakis (Aug 03 2020 at 14:16, on Zulip):

debatable I guess :)

lqd (Aug 03 2020 at 14:16, on Zulip):

but yeah I totally understand

lqd (Aug 03 2020 at 14:17, on Zulip):

and as documentation/reference implementation etc it will always be valuable even if we had to not use datalog per se

lqd (Aug 03 2020 at 14:17, on Zulip):

I think I saw a minuscule, useless, inefficiency in rustc init/unit dataflow analyses thanks to our rules

nikomatsakis (Aug 03 2020 at 14:17, on Zulip):

do you have a sense for which parts of the rules are accounting for performance?

lqd (Aug 03 2020 at 14:18, on Zulip):

for move errors you mean ?

nikomatsakis (Aug 03 2020 at 14:18, on Zulip):

yeah, or is it just "computing all those tuples"

nikomatsakis (Aug 03 2020 at 14:18, on Zulip):

it does seem like they're probably ripe for a "location insensitive optimization"

lqd (Aug 03 2020 at 14:19, on Zulip):

I haven't profiled at all, but it seemed to to compute a lot of intermediary state and cloning it

nikomatsakis (Aug 03 2020 at 14:19, on Zulip):

though I have to thnk a bit about what that means ;)

lqd (Aug 03 2020 at 14:19, on Zulip):

which is expected

lqd (Aug 03 2020 at 14:19, on Zulip):

our CFGs are big, and such analyses are usually done per block

nikomatsakis (Aug 03 2020 at 14:19, on Zulip):

yeah, ok, so one thing we're not doing is doing the iteration at the block level

lqd (Aug 03 2020 at 14:19, on Zulip):

and optimizable when no cycles are present, etc etc

nikomatsakis (Aug 03 2020 at 14:20, on Zulip):

we're also computing transitive closures across paths at each node

nikomatsakis (Aug 03 2020 at 14:20, on Zulip):

i.e., if you access a.b.c, we also store tuples for accessing a, a.b, etc

lqd (Aug 03 2020 at 14:20, on Zulip):

right

nikomatsakis (Aug 03 2020 at 14:20, on Zulip):

you could imagine doing that differently

nikomatsakis (Aug 03 2020 at 14:20, on Zulip):

though I don't recall what rustc does

lqd (Aug 03 2020 at 14:21, on Zulip):

in any case we have multiple solutions for that situation

lqd (Aug 03 2020 at 14:21, on Zulip):

("move errors are slow" situation, not the transitive paths accesses)

nikomatsakis (Aug 03 2020 at 14:22, on Zulip):

regarding https://github.com/rust-lang/polonius/issues/152 (assignments to partially initialized paths), it's true that we intentionally made the borrow checker less precise here

nikomatsakis (Aug 03 2020 at 14:22, on Zulip):

I forget all the details of why, but probably we should make polonius match, seems like it wouldn't be hard to do

lqd (Aug 03 2020 at 14:23, on Zulip):

ah I found the issue I was looking for, https://github.com/rust-lang/rust/issues/70797 is the thing I was remembering when I was talking about the possible unintended consequence of the "move errors false positive fix" switching a fact location to the start point, and also fits in the theme "what rust code do our rules allow"

lqd (Aug 03 2020 at 14:23, on Zulip):

I haven't checked whether it was valid/expected, but it was at least a change

nikomatsakis (Aug 03 2020 at 14:24, on Zulip):

interesting

lqd (Aug 03 2020 at 14:25, on Zulip):

I don't remember how we ended up dealing with the same situation of user code expressiveness and limits during NLLs

nikomatsakis (Aug 03 2020 at 14:25, on Zulip):

OK, so, I'm wondering what we should try to do first? =)

One thing would be to start a different topic and talk over the status of subsets and the placeholder vs region relations question

nikomatsakis (Aug 03 2020 at 14:25, on Zulip):

Yeah, it'd be good to dig into that example and understand just what is going on

nikomatsakis (Aug 03 2020 at 14:26, on Zulip):

it may also inform the question of whether to "package" move errors and subsets

lqd (Aug 03 2020 at 14:26, on Zulip):

interesting

nikomatsakis (Aug 03 2020 at 14:26, on Zulip):

I could try investigating too... as a way to remember what the heck is going on :)

lqd (Aug 03 2020 at 14:26, on Zulip):

the status of subsets vs equality ?

nikomatsakis (Aug 03 2020 at 14:27, on Zulip):

no, actually, that's not what I meant

nikomatsakis (Aug 03 2020 at 14:27, on Zulip):

I guess I meant to go about the placeholder vs regions origins question,

nikomatsakis (Aug 03 2020 at 14:27, on Zulip):

but also review a bit the status of those rules in polonius

nikomatsakis (Aug 03 2020 at 14:27, on Zulip):

is https://hackmd.io/CGMNjt1hR_qYtsR9hgdGmw#Subset-and-contains-the-heart-of-the-borrow-check reflecting the current rules as implemented?

nikomatsakis (Aug 03 2020 at 14:28, on Zulip):

I am remembering our new terminology :)

lqd (Aug 03 2020 at 14:28, on Zulip):

besides the new terminology, which I still am not accustomed to, I think so yes :)

lqd (Aug 03 2020 at 14:30, on Zulip):

maybe those aren't finalized either, especially about "things that exist at all points" which we have hacked around in the data instead of the rules

nikomatsakis (Aug 03 2020 at 14:32, on Zulip):

yes, ok

lqd (Aug 03 2020 at 14:32, on Zulip):

(I mean I think we have updated the rules in the hackmd to be closer to what they used to be with souffé, but with new terminology, and not all those are completely finalized in the code)

lqd (Aug 03 2020 at 14:32, on Zulip):

but that's just refactoring and duplicating rules, the spirit is the same

lqd (Aug 03 2020 at 14:34, on Zulip):

about the "placeholder vs origins question" did you mean something like "placeholder loans vs origin subsets" ?

nikomatsakis (Aug 03 2020 at 14:34, on Zulip):

I think my feeling on move errors is that, ultimately, I would like them to be computed by polonius, in part because I want there to be some library that people can use to run and access borrow check results that is extracted from rustc (as part of the library-ification efforts). But I am not sure of the time-frame. And, furthermore, it's hard to imagine that -- in the fullness of time -- it really makes sense to "copy out" the CFG from MIR into a bunch of tuples versus operating directly on it in some way.

nikomatsakis (Aug 03 2020 at 14:35, on Zulip):

lqd said:

about the "placeholder vs origins question" did you mean something like "placeholder loans vs origin subsets" ?

yes.

nikomatsakis (Aug 03 2020 at 14:35, on Zulip):

so I think we should make the goal of this sprint being to have a definitive set of polonius rules

nikomatsakis (Aug 03 2020 at 14:35, on Zulip):

is that plausible?

nikomatsakis (Aug 03 2020 at 14:35, on Zulip):

I mean subject to a billion caveats ;)

lqd (Aug 03 2020 at 14:35, on Zulip):

:)

lqd (Aug 03 2020 at 14:36, on Zulip):

would definitive set imply knowing whether these rules as-is are to be preferred to the equality variant ones ?

nikomatsakis (Aug 03 2020 at 14:36, on Zulip):

but it feels like that would be really useful and would help us in future sprints to work on impl questions

nikomatsakis (Aug 03 2020 at 14:36, on Zulip):

lqd said:

would definitive set imply knowing whether these rules as-is are to be preferred to the equality variant ones ?

I do think we should talk about the equality vs subset question

lqd (Aug 03 2020 at 14:36, on Zulip):

note that I have an implementation of the equality variant which passed rustc tests except one

nikomatsakis (Aug 03 2020 at 14:37, on Zulip):

I still feel like the equality relation ought to be an optimization, as a side note, and it's more correct, so I guess I'm biased there, but open to being persuaded :)

nikomatsakis (Aug 03 2020 at 14:37, on Zulip):

where "correct" means "accepts more programs", I guess, but I think in particular accepts some programs rustc accepts today

nikomatsakis (Aug 03 2020 at 14:37, on Zulip):

but maybe I don't remember correctly

lqd (Aug 03 2020 at 14:38, on Zulip):

the equality variant being an optimization ?

lqd (Aug 03 2020 at 14:39, on Zulip):

I think it started that way, and fixed a polonius-as-is imprecision, and then it had some imprecision that polonius didn't have, and to fix that we had to propagate some equality facts, and then some rustc tests failed and I had to add another TC and then it wasn't much of an optimization any more :)

nikomatsakis (Aug 03 2020 at 14:41, on Zulip):

why don't we break some of these conversations out into a distinct topic at this point?

nikomatsakis (Aug 03 2020 at 14:41, on Zulip):

I'm not sure if @Albin Stjerna is still with us :)

lqd (Aug 03 2020 at 14:41, on Zulip):

right I was doing that :)

Albin Stjerna (Aug 03 2020 at 14:41, on Zulip):

I am! I just didn't have anything useful to add :)

nikomatsakis (Aug 03 2020 at 14:41, on Zulip):

that said, I think the equality should be an optimization just from "first principles", it has fewer relations to propagate

nikomatsakis (Aug 03 2020 at 14:41, on Zulip):

it's also bi-directional

nikomatsakis (Aug 03 2020 at 14:42, on Zulip):

we may not have figured out the right way to express those things yet, particularly not in datalog..

lqd (Aug 03 2020 at 14:42, on Zulip):

right, I didn't yet take any advatage of bidirectionality

nikomatsakis (Aug 03 2020 at 14:44, on Zulip):

@Albin Stjerna do you have some plans for what you want to be hacking on?

nikomatsakis (Aug 03 2020 at 14:44, on Zulip):

I am torn because I was going to say that I would be happy to help mentor a bit how to report move errors

nikomatsakis (Aug 03 2020 at 14:44, on Zulip):

but now @lqd is giving me second thoughts ;)

lqd (Aug 03 2020 at 14:44, on Zulip):

dang :)

Albin Stjerna (Aug 03 2020 at 14:44, on Zulip):

I started looking at reporting move errors in rustc, but I see what you mean

lqd (Aug 03 2020 at 14:45, on Zulip):

I need to do something for half an hour if you really want to talk about it though :)

nikomatsakis (Aug 03 2020 at 14:45, on Zulip):

though I think I would personally lean somewhat towards

nikomatsakis (Aug 03 2020 at 14:45, on Zulip):

I think it just would need to compute liveness?

lqd (Aug 03 2020 at 14:46, on Zulip):

it will not be wasted to validate our move errors rules

nikomatsakis (Aug 03 2020 at 14:46, on Zulip):

as I wrote above, I still feel the goal of polonius ought to ultimately be to be the borrow check library -- but I suspect that it may wind up depending on some "MIR library" and encapsulating fact generation as well

nikomatsakis (Aug 03 2020 at 14:46, on Zulip):

and perhaps that means that the optimized variants don't even use datalog

nikomatsakis (Aug 03 2020 at 14:46, on Zulip):

I still see a lot of value in having "reference implementations" we can test and publish

nikomatsakis (Aug 03 2020 at 14:46, on Zulip):

and, you know, actually read

lqd (Aug 03 2020 at 14:47, on Zulip):

that makes sense to me, I think we're all in agreement about that ?

Albin Stjerna (Aug 03 2020 at 14:47, on Zulip):

I had a look at how the fact generation code looks now, and it's still quite spaghetti

nikomatsakis (Aug 03 2020 at 14:47, on Zulip):

ok so maybe if @Albin Stjerna is interested we should push a bit more on that

nikomatsakis (Aug 03 2020 at 14:47, on Zulip):

yeah, true, not sure if we had plans for how to clean that up

lqd (Aug 03 2020 at 14:47, on Zulip):

Albin had some IIRC

nikomatsakis (Aug 03 2020 at 14:47, on Zulip):

that reminds me that another imp't goal I think is to document some more of this stuff

Albin Stjerna (Aug 03 2020 at 14:47, on Zulip):

I did, but I've forgotten everything

nikomatsakis (Aug 03 2020 at 14:47, on Zulip):

e.g., describing the input relations, and having some comments int he polonius book about what they are meant to represent

nikomatsakis (Aug 03 2020 at 14:48, on Zulip):

it bothers me a bit that e.g. we have this debate about "where this fact should go, on entry or mid point" etc

lqd (Aug 03 2020 at 14:48, on Zulip):

you had a nice chart at https://github.com/rust-lang/polonius/issues/117

Albin Stjerna (Aug 03 2020 at 14:48, on Zulip):

I also think the spaghettiness comes from the fact that it's piggy-backing off of different parts of the code doing the same analysis in rust

Albin Stjerna (Aug 03 2020 at 14:49, on Zulip):

nikomatsakis said:

ok so maybe if Albin Stjerna is interested we should push a bit more on that

I'm sorry, I'm not sure I followed what "that" is here?

lqd (Aug 03 2020 at 14:49, on Zulip):

(so I'll let you talk about move errors and will be back in 20-30 mins or so)

lqd (Aug 03 2020 at 14:53, on Zulip):

(@Albin Stjerna not that it matters much since you don't need it right now, but Mark has indeed found the fix to our x.py check earlier issue, we might have hit a recent cargo bug, but we can work around it by using the regular crates.io patching feature in the root Cargo.toml, so it's even easier than our previous way of doing it)

Albin Stjerna (Aug 03 2020 at 14:54, on Zulip):

Ok, that's great!

Albin Stjerna (Aug 03 2020 at 14:54, on Zulip):

I mean, we don't currently need the fix and I'm happy we found the bug

lqd (Aug 03 2020 at 14:55, on Zulip):

it does make my life easier rn :)

lqd (Aug 03 2020 at 14:55, on Zulip):

(bbl)

lqd (Aug 03 2020 at 16:02, on Zulip):

I will continue publishing the OOM-fix so y'all can take a look

nikomatsakis (Aug 05 2020 at 09:29, on Zulip):

Wow, this is going fast. I'm glad we're doing it regardless. I was thinking -- do you think we can schedule the next one? I'd like to start organizing my time in more "sprint-like" fashion, actually (e.g., chalk week, polonius week, etc).

lqd (Aug 05 2020 at 09:31, on Zulip):

once again my schedule is more easily manageable than both of yours for this, so I'd gladly do this again :)

lqd (Aug 05 2020 at 09:43, on Zulip):

what would be a reasonable period ? I'll assume we can't easily do polonius week ... every week, what did you have in mind, once every 3 months or something like that ?

lqd (Aug 05 2020 at 16:32, on Zulip):

I guess "what frequency" would have been the correct way to ask this question.

lqd (Aug 05 2020 at 16:35, on Zulip):

in any case I have to leave for a bit of the evening, so I wanted to thank you all for organizing and participating in the sprint, I'm enjoying it very much. Super fun and motivating as always.

nikomatsakis (Aug 05 2020 at 16:42, on Zulip):

Well, I don't know :)

nikomatsakis (Aug 05 2020 at 16:42, on Zulip):

but I was thinking maybe we can do something in september at least this time

nikomatsakis (Aug 05 2020 at 16:43, on Zulip):

every 3 months feels a bit too sparse to me

lqd (Aug 05 2020 at 17:05, on Zulip):

true; september could work, especially if I can prepare better so we have more, say, PRs to review, well-defined problems to discuss, etc. Using my time outside of the sprint to ensure your time inside the sprint is well spent

Albin Stjerna (Aug 06 2020 at 08:13, on Zulip):

I'll try to keep working a bit in order to even remember what I was doing again, but sure I'd be up for another sprint!

Albin Stjerna (Aug 06 2020 at 08:16, on Zulip):

I mean, I have to figure out where the move errors go wrong :)

nikomatsakis (Aug 06 2020 at 09:54, on Zulip):

nice, it went by way too fast

nikomatsakis (Aug 06 2020 at 09:54, on Zulip):

that said, I was checking off boxes in the hackmd and I realized we got quite a lot done

Albin Stjerna (Aug 06 2020 at 09:59, on Zulip):

Enough that I'll have to go through the things I wasn't involved with to figure out what you actually did :)

lqd (Aug 06 2020 at 09:59, on Zulip):

do you two think we should temporarily disable the move errors computation in polonius until this new work is done ? if it's super close to being finished there'd be no need to do so ofc

Albin Stjerna (Aug 06 2020 at 10:03, on Zulip):

Hmm. I think it makes sense given that we don't know what's broken and why

Albin Stjerna (Aug 06 2020 at 10:03, on Zulip):

So in the interest of having only something working in the repository, maybe disabling it would be a good idea, and it would also help with the OOMs

Albin Stjerna (Aug 06 2020 at 10:04, on Zulip):

Which I guess would also accelerate your work on the other parts?

lqd (Aug 06 2020 at 10:06, on Zulip):

it went by too fast for sure :) but it's an interesting process, that is, a seemingly nice way to batch up your time Niko (for polonius, chalk, and other projects) rather than cut into less useful 30mins bits weekly. In the meantime we can still work on it, that can help to have more work available in your next sprint, whether we can participate at the same time or not (with our TZ differences, there can still be overlap in late afternoon and evenings). Even if we weren't able to make much progress in-between sprints, there'd still be things to do for you during the sprint. That would allow it to be more frequent, like monthly, and so we can still have steady progress overall

lqd (Aug 06 2020 at 10:12, on Zulip):

Albin Stjerna said:

Which I guess would also accelerate your work on the other parts?

it could, but I can disable them locally whenever I need to do anything

Last update: Jun 20 2021 at 01:30UTC