Stream: wg-traits

Topic: meeting 2019-04-15


nikomatsakis (Apr 15 2019 at 18:02, on Zulip):

Hey @WG-traits -- shall we have a meeting? I had hoped to talk about the work I did on factoring the chalk crate and perhaps try to do a bit of a "take stock of next steps" meeting. I think the "sprint" hasn't quite worked out for a variety of reasons =)

nikomatsakis (Apr 15 2019 at 18:04, on Zulip):

(cc @Florian Diebold, @matklad, @detrumi -- this is all pretty related to integrating chalk into rls)

nikomatsakis (Apr 15 2019 at 18:05, on Zulip):

I spent .. a sort of embarassingly large amount of time trying to make a good diagram of the crates and kind of failed, but in the last hour I tried to write-up some notes on the general design here. It's not really that complicated.

nikomatsakis (Apr 15 2019 at 18:05, on Zulip):

Of course, writing up those notes also revealed to me a (relatively minor) problem around re-entrancy that will arise when we try to tackle specialization (and will require some altering of the design)

nikomatsakis (Apr 15 2019 at 18:06, on Zulip):

a sort of embarassingly large amount of time trying to make a good diagram of the crates and kind of failed

I blame the tooling =) I didn't find the right diagramming program yet I thnk :)

nikomatsakis (Apr 15 2019 at 18:07, on Zulip):

OK so how shall we do this.

nikomatsakis (Apr 15 2019 at 18:07, on Zulip):

Actually, give me 1 minute to grab a fresh cup of coffee ;)

detrumi (Apr 15 2019 at 18:09, on Zulip):

That's a good way to give us time to read the notes :slight_smile:

nikomatsakis (Apr 15 2019 at 18:10, on Zulip):

OK, back.

nikomatsakis (Apr 15 2019 at 18:10, on Zulip):

So yeah, feel free to skim the notes, but I'll reproduce a (shortened) version here

nikomatsakis (Apr 15 2019 at 18:10, on Zulip):

There are essentially three key components:

nikomatsakis (Apr 15 2019 at 18:11, on Zulip):

the solver and rules crate never talk directly to one another

nikomatsakis (Apr 15 2019 at 18:11, on Zulip):

all intercommunication is ultimately mediated by the integration crate

nikomatsakis (Apr 15 2019 at 18:12, on Zulip):

the solver/rules crates also do not know about chalk or anything like that. They each work against a "database" that fulfills a trait -- ChalkSolveDatabase or ChalkRulesDatabase respectively -- which defines the things they can ask of "their context"

nikomatsakis (Apr 15 2019 at 18:13, on Zulip):

Example of the ChalkSolveDatabase:

/// The trait for defining the program clauses that are in scope when
/// solving a goal.
pub trait ChalkSolveDatabase: Debug {
    /// Returns a set of program clauses that could possibly match
    /// `goal`. This can be any superset of the correct set, but the
    /// more precise you can make it, the more efficient solving will
    /// be.
    fn program_clauses_that_could_match(&self, goal: &DomainGoal, vec: &mut Vec<ProgramClause>);

    fn is_coinductive_trait(&self, trait_id: TraitId) -> bool;
}
nikomatsakis (Apr 15 2019 at 18:14, on Zulip):

the ChalkRulesDatabase trait is the other one, it's a bit bigger :)

nikomatsakis (Apr 15 2019 at 18:14, on Zulip):

I had this table I wound up cutting, but maybe it's helpful actually. It summarizes the intercommunication.

crate question answered by
chalk-solve program clauses for a given goal? chalk-rules
chalk-solve is a given trait coinductive? integration
chalk-rules solve a given goal chalk-solve
chalk-rules query the rust ir integration
nikomatsakis (Apr 15 2019 at 18:15, on Zulip):

Anyway, all of this setup I think it is sort of .. mostly correct, though as I mentioned I realized a problem (I'll get to it later).

nikomatsakis (Apr 15 2019 at 18:16, on Zulip):

But any questions on this part?

nikomatsakis (Apr 15 2019 at 18:17, on Zulip):

/me can't tell what people are doing :)

Aaron Turon (Apr 15 2019 at 18:17, on Zulip):

reading notes and listening :)

tmandry (Apr 15 2019 at 18:17, on Zulip):

trying to understand the table :)

detrumi (Apr 15 2019 at 18:17, on Zulip):

So the solver returns a superset, and you need to check those with rules?

Florian Diebold (Apr 15 2019 at 18:17, on Zulip):

it's very helpful already, I had looked at the PR and was quite confused as to who implements what :)

nikomatsakis (Apr 15 2019 at 18:18, on Zulip):

So the solver returns a superset, and you need to check those with rules?

not quite -- the solver asks for a superset

nikomatsakis (Apr 15 2019 at 18:18, on Zulip):

e.g., it might say, I need to prove that Vec<u32>: Clone -- give me any rules that I might use to do that

nikomatsakis (Apr 15 2019 at 18:18, on Zulip):

the more precise we can be, the better in some sense, because the solver will do less work

nikomatsakis (Apr 15 2019 at 18:19, on Zulip):

but it's also ok if we give it rules that don't apply, it will weed them out

nikomatsakis (Apr 15 2019 at 18:19, on Zulip):

it's actually a good place to dig a bit deeper -- but does that make sense so far? (And you do you know what I mean here by "rules"?)

Aaron Turon (Apr 15 2019 at 18:20, on Zulip):

it does, i recall talking through this part in one of our recorded video sessions (don't recall which)

nikomatsakis (Apr 15 2019 at 18:20, on Zulip):

yeah

nikomatsakis (Apr 15 2019 at 18:21, on Zulip):

by "rules" here I mean "Program clauses" in prolog terminology -- basically, the rules that we derive from rust IR. So e.g. if you had impl<T: Clone> Clone for Vec<T>, then that might be lowered to a program clause like

Implemented(Vec<T>: Clone) :- Implemented(T: Clone)

and that is (naturally) something we would want to return through this callback

nikomatsakis (Apr 15 2019 at 18:21, on Zulip):

(since it would apply to Vec<u32>)

nikomatsakis (Apr 15 2019 at 18:21, on Zulip):

but if there were some impl like impl<T: ?Sized> Clone for Arc<T>, that gives rise to a rule like Implemented(Arc<T>: Clone). -- and we might or might not return that

detrumi (Apr 15 2019 at 18:22, on Zulip):

Right, so mainly impl's, but also trait bounds in functions for example I'd imagine

nikomatsakis (Apr 15 2019 at 18:23, on Zulip):

so where-clauses (if that's what you mean) are actually part of the goals

detrumi (Apr 15 2019 at 18:23, on Zulip):

(where they originate I mean, I understand that Prolog rules are more general)

nikomatsakis (Apr 15 2019 at 18:23, on Zulip):

i.e., if you have

fn foo<T>(t: T)
where T: Clone,
{
   ...t.clone()...
}
nikomatsakis (Apr 15 2019 at 18:24, on Zulip):

when type-checking t.clone(), we might generate a goal for the solver like

forall<T> {
  if (T: Clone) { // from the where clause
    T: Clone // prove that `T: Clone`...
  }
}
nikomatsakis (Apr 15 2019 at 18:24, on Zulip):

(not quite right because of implied bounds, but that's the idea)

nikomatsakis (Apr 15 2019 at 18:24, on Zulip):

the solver internally knows how to handle this if (T: Clone) business

nikomatsakis (Apr 15 2019 at 18:24, on Zulip):

so really the callback is just about the global rules that come from impls and the rust semantics

nikomatsakis (Apr 15 2019 at 18:25, on Zulip):

anyway, so, the reason I said this was interesting to dig into a bit

nikomatsakis (Apr 15 2019 at 18:26, on Zulip):

it is interesting to think about how the "integration crate" will respond to this request, in terms of caching etc

nikomatsakis (Apr 15 2019 at 18:26, on Zulip):

in my branch that is in the PR, the main work I did was extracting the chalk-solve and chalk-rules crates

nikomatsakis (Apr 15 2019 at 18:26, on Zulip):

but the chalk crate itself (the "integration" crate) is still working in a kind of "global" fashion

nikomatsakis (Apr 15 2019 at 18:27, on Zulip):

so e.g. it has a query that just says "give me the rust-ir for the whole program"

nikomatsakis (Apr 15 2019 at 18:27, on Zulip):
 fn program_ir(&self) -> Result<Arc<Program>, ChalkError>;
matklad (Apr 15 2019 at 18:28, on Zulip):

/me joined, listens attentively

nikomatsakis (Apr 15 2019 at 18:28, on Zulip):

however, this Program type has been extracted from the chalk-rust-ir crate and now lives in the chalk crates

nikomatsakis (Apr 15 2019 at 18:28, on Zulip):

this is because -- e.g., in the RLS -- it is not something that we would want to have

nikomatsakis (Apr 15 2019 at 18:29, on Zulip):

(though it's ok in the chalk harness)

nikomatsakis (Apr 15 2019 at 18:29, on Zulip):

there is also a concept of ProgramEnvironment, which is the full set of lowered clauses -- this has also been confined to the chalk crate

nikomatsakis (Apr 15 2019 at 18:30, on Zulip):

and if you look at the code which answers the solver's "give me all possibly matching clauses" call, you will see it just iterates over a vector (link):

    fn program_clauses_that_could_match(&self, goal: &DomainGoal, vec: &mut Vec<ProgramClause>) {
        if let Ok(env) = self.environment() {
            vec.extend(
                env.program_clauses
                    .iter()
                    .filter(|&clause| clause.could_match(goal))
                    .cloned(),
            );
        }
}
nikomatsakis (Apr 15 2019 at 18:30, on Zulip):

this part is not really right, even for chalk

nikomatsakis (Apr 15 2019 at 18:30, on Zulip):

(because of specialization)

matklad (Apr 15 2019 at 18:30, on Zulip):

Quick question: what is the purpose of integration crate (chalk)? Should RLS use it directly, or should RLS be itself the "integration" crate?

In other words, why name it "integration", and not by name (chalk)

nikomatsakis (Apr 15 2019 at 18:31, on Zulip):

the RLS would be that crate

nikomatsakis (Apr 15 2019 at 18:31, on Zulip):

and it is named "chalk"

nikomatsakis (Apr 15 2019 at 18:31, on Zulip):

I am trying and maybe failing to use the term "integration crate" in order to be more generic

nikomatsakis (Apr 15 2019 at 18:31, on Zulip):

but i'm maybe using it more often than I should :)

nikomatsakis (Apr 15 2019 at 18:32, on Zulip):

but yeah I imagine that the RLS would implement the ChalkSolveDatabase and ChalkRulesDatabase traits

nikomatsakis (Apr 15 2019 at 18:32, on Zulip):

there is still a bit more refactoring within chalk I think to expose useful concepts before we do that

nikomatsakis (Apr 15 2019 at 18:32, on Zulip):

in particular around this callback I'm digging into now

nikomatsakis (Apr 15 2019 at 18:33, on Zulip):

basically, a big goal is that we should never 'iterate over the whole program' when solving a given goal

nikomatsakis (Apr 15 2019 at 18:33, on Zulip):

in an IDE, you can kind of clearly see why that would be --

nikomatsakis (Apr 15 2019 at 18:33, on Zulip):

you want to be as narrow as possible

nikomatsakis (Apr 15 2019 at 18:33, on Zulip):

in terms of what you "demand"

nikomatsakis (Apr 15 2019 at 18:34, on Zulip):

but also if you think of incremental compliation, where we are monitoring the bits of the program you looked at, it's the same. If you ask for "give me all the program clauses from the whole program" and then anything changes, you have to assume all your solving is outdated

nikomatsakis (Apr 15 2019 at 18:34, on Zulip):

Anyway so I think a bit of remaining work is to refine that callback from the solver.

tmandry (Apr 15 2019 at 18:35, on Zulip):

having taken an initial crack at salsaification, this is great and overall makes sense :)

tmandry (Apr 15 2019 at 18:35, on Zulip):

minor point, but I'm a little confused why GoalSolver is defined in chalk-rules

nikomatsakis (Apr 15 2019 at 18:35, on Zulip):

so e.g. if we get callback with a goal like Implemented(Vec<u32>: Clone), it should only access the rust-ir that might produce rules that answer this query -- i.e., impls of Clone, ideally

nikomatsakis (Apr 15 2019 at 18:35, on Zulip):

minor point, but I'm a little confused why GoalSolver is defined in chalk-rules

yes, that's a good question -- and I think it's actualy not quite right

nikomatsakis (Apr 15 2019 at 18:36, on Zulip):

so e.g. if we get callback with a goal like Implemented(Vec<u32>: Clone), it should only access the rust-ir that might produce rules that answer this query -- i.e., impls of Clone, ideally

I should say that @scalexm and I already took a crack at defining this logic in rustc

nikomatsakis (Apr 15 2019 at 18:36, on Zulip):

so we basically want to 'port over' that code from rustc back into chalk

nikomatsakis (Apr 15 2019 at 18:36, on Zulip):

i.e., knowing which bits of rust-ir might produce rules relevant to a given goal

nikomatsakis (Apr 15 2019 at 18:36, on Zulip):

and only lowering those

nikomatsakis (Apr 15 2019 at 18:37, on Zulip):

(I'm going to create a paper for this meeting actually to drop some notes in, then we can figure out where to move them to)

nikomatsakis (Apr 15 2019 at 18:38, on Zulip):

paper link

nikomatsakis (Apr 15 2019 at 18:39, on Zulip):

So before I take a shot at answering @tmandry's question about GoalSolver...

nikomatsakis (Apr 15 2019 at 18:40, on Zulip):

I guess, first off, any questions on what I wrote so far ?

matklad (Apr 15 2019 at 18:40, on Zulip):

I am not clear about needing two crates to integrate with

matklad (Apr 15 2019 at 18:40, on Zulip):

I guess, I understand why internally this makes sense (separating solving from lowering)

nikomatsakis (Apr 15 2019 at 18:40, on Zulip):

like, why separate chalk-solve and chalk-rules?

matklad (Apr 15 2019 at 18:41, on Zulip):

yeah

nikomatsakis (Apr 15 2019 at 18:41, on Zulip):

it's partly just an internal thing

matklad (Apr 15 2019 at 18:41, on Zulip):

from software engeneering perspective, I'd prefer to integrate RLS with a single crate :D

detrumi (Apr 15 2019 at 18:41, on Zulip):

Why can't one call the other?

detrumi (Apr 15 2019 at 18:41, on Zulip):

So that you only expose one of them

nikomatsakis (Apr 15 2019 at 18:41, on Zulip):

well

nikomatsakis (Apr 15 2019 at 18:42, on Zulip):

one of my motivations was that -- when I looked closely at the rules crate

nikomatsakis (Apr 15 2019 at 18:42, on Zulip):

I had the impression that, with some more work, it could probably be refactored such that it could be used from within rustc

nikomatsakis (Apr 15 2019 at 18:42, on Zulip):

but we'd have to do a bit of work on making the various bits of IR a bit more generic

nikomatsakis (Apr 15 2019 at 18:42, on Zulip):

we could certainly make an "end point" crate that rls can link against

nikomatsakis (Apr 15 2019 at 18:42, on Zulip):

or perhaps have chalk-solve know about chalk-rules

nikomatsakis (Apr 15 2019 at 18:42, on Zulip):

to be quite honest, the structure I'm presenting here is also something I sort of evolved a bit towards

nikomatsakis (Apr 15 2019 at 18:43, on Zulip):

so for some time I was just picking things apart

nikomatsakis (Apr 15 2019 at 18:43, on Zulip):

so that I could see all the pieces holding them together

nikomatsakis (Apr 15 2019 at 18:43, on Zulip):

and I think it may make sense to recombine them

nikomatsakis (Apr 15 2019 at 18:43, on Zulip):

which is partly why I wanted to talk it out

nikomatsakis (Apr 15 2019 at 18:43, on Zulip):

but we'd have to do a bit of work on making the various bits of IR a bit more generic

in particular, we'd want to make the rust-ir crate kind of generic over how types are represented etc. It might not be worth the trouble, but it might be.

matklad (Apr 15 2019 at 18:44, on Zulip):

"easy to integrate with rustc" makes sense! But chalk-facade would also be helpful: at least there will be a single point to start reading the code from :)

nikomatsakis (Apr 15 2019 at 18:44, on Zulip):

yeah.

nikomatsakis (Apr 15 2019 at 18:44, on Zulip):

I think there is probably an intermediate point that chalk would also integrate with

nikomatsakis (Apr 15 2019 at 18:45, on Zulip):

ok, so let me answer @tmandry's question

nikomatsakis (Apr 15 2019 at 18:45, on Zulip):

which was "why does chalk-rules have this GoalSolver trait"

nikomatsakis (Apr 15 2019 at 18:45, on Zulip):

GoalSolver has a single callback, solve, that lets you solve a given goal

nikomatsakis (Apr 15 2019 at 18:46, on Zulip):

(it is a supertrait of ChalkRulesDatabase, so it is meant to be implemented by the general database)

tmandry (Apr 15 2019 at 18:46, on Zulip):

(I think I just realized why btw)

tmandry (Apr 15 2019 at 18:46, on Zulip):

specialization?

nikomatsakis (Apr 15 2019 at 18:47, on Zulip):

Right now, the chalk-rules crate includes three things:

the latter two are basically Rust functions that return Result<(), ChalkError> <-- we should probably tweak those signatures

nikomatsakis (Apr 15 2019 at 18:48, on Zulip):

in order to do their work, they have to solve goals

nikomatsakis (Apr 15 2019 at 18:48, on Zulip):

specialization?

(yes, but I'm getting to it)

nikomatsakis (Apr 15 2019 at 18:48, on Zulip):

so they ask the database "hey solve this goal", and it has (internally) a cached solver that it delegates to, etc

nikomatsakis (Apr 15 2019 at 18:48, on Zulip):

they use the trait to do this

nikomatsakis (Apr 15 2019 at 18:50, on Zulip):

currently, the "solving" callback is not used when lowering from rust-ir to program clauses

nikomatsakis (Apr 15 2019 at 18:50, on Zulip):

however, I grouped them together because, to handle specialization, we do expect to have to solve goals and figure out the overlap between impls

nikomatsakis (Apr 15 2019 at 18:50, on Zulip):

and so creating the program clauses for a given impl (say, one that contains a default associated type) will require running coherence checks

nikomatsakis (Apr 15 2019 at 18:51, on Zulip):

this needs a bit more work to tease out, and this problem I keep hinting at is precisely here -- right now, the solver requires &mut self access. So if it invokes the callback to ask for program clauses, and that recursively invokes stuff in the solver, we have a cycle (what will happen in the code as it is today is a deadlock, because there is a Mutex involved)

nikomatsakis (Apr 15 2019 at 18:52, on Zulip):

(I think that what this means is that the "coherence checks" want to instantiate their own solver, which ironically is what the code used to do and I removed it)

nikomatsakis (Apr 15 2019 at 18:52, on Zulip):

But that's a relatively minor point

nikomatsakis (Apr 15 2019 at 18:53, on Zulip):

Anyway, to bring this back, since we're nearing on an hour here.

nikomatsakis (Apr 15 2019 at 18:54, on Zulip):

I think we should land my PR, first of all ;)

nikomatsakis (Apr 15 2019 at 18:54, on Zulip):

but there is still some refactoring to be done -- I think maybe now it is easier to define what that is

nikomatsakis (Apr 15 2019 at 18:55, on Zulip):

I wrote in the paper doc:

nikomatsakis (Apr 15 2019 at 18:55, on Zulip):

but I guess I left out "solve recursive solver setup"

nikomatsakis (Apr 15 2019 at 18:55, on Zulip):

at that point we're starting to be able to define specialization too

nikomatsakis (Apr 15 2019 at 18:56, on Zulip):

interestingly, this whole effort is in some sense a distraction ;) in that it doesn't really further the rustc-chalk integration we had intended to focus on. But I think it's important still -- and I also continue to have this nagging feeling that we should also push towards RLS integration.

nikomatsakis (Apr 15 2019 at 18:57, on Zulip):

Basically though this work serves two goals:

nikomatsakis (Apr 15 2019 at 18:57, on Zulip):

@Sunjay Varma you had mentioned wanting to do work on the latter, how much time do you think you have available? Similarly, @detrumi? I was thinking that maybe we should the 3 of us try to sync a bit

nikomatsakis (Apr 15 2019 at 18:57, on Zulip):

though others are welcome too :) but I wanted to bring up some other topics worth digging into

nikomatsakis (Apr 15 2019 at 18:58, on Zulip):

i.e., I want to try and create two sub-efforts. One focused on these steps towards refactoring chalk (which I hope I have now unblocked, though I expect we'll have to do a bit more sync'ing and mentoring to make clear what's the next steps)

nikomatsakis (Apr 15 2019 at 18:58, on Zulip):

and the other on some of the harder problems around built-in bounds, regions, etc

nikomatsakis (Apr 15 2019 at 18:59, on Zulip):

( which I am happy to go on discussing, but I want to hold off a bit to wrap this up )

nikomatsakis (Apr 15 2019 at 18:59, on Zulip):

and the other on some of the harder problems around built-in bounds, regions, etc

I guess harder isn't quite the right term, but there's a bit more unknowns in my mind about it

detrumi (Apr 15 2019 at 19:00, on Zulip):

It's also more a core issue, while the first sub-effort is more on the edge

nikomatsakis (Apr 15 2019 at 19:01, on Zulip):

yeah

nikomatsakis (Apr 15 2019 at 19:02, on Zulip):

So, we had talked about trying to organize "sprints". Strictly speaking, we are mid sprint =) though it ends in a few weeks.

nikomatsakis (Apr 15 2019 at 19:02, on Zulip):

(2019.03.18 - 2019.04.29)

nikomatsakis (Apr 15 2019 at 19:02, on Zulip):

I don't actually care about this per se

nikomatsakis (Apr 15 2019 at 19:02, on Zulip):

except that I think the concept of identifying some goals and working towards them is quite good

nikomatsakis (Apr 15 2019 at 19:02, on Zulip):

so I guess what I'm saying is, I think we can make a few clear sprint goals around this topic

Sunjay Varma (Apr 15 2019 at 19:03, on Zulip):

Sorry, I'm unable to take very much time for this meeting today. I am available to work on specialization and I will have a good amount of time to work on it in the coming weeks.

Sunjay Varma (Apr 15 2019 at 19:03, on Zulip):

Will try to catch up later

Sunjay Varma (Apr 15 2019 at 19:03, on Zulip):

Feel free to DM me about stuff if needed :)

nikomatsakis (Apr 15 2019 at 19:03, on Zulip):

@detrumi are you interested in pursuing the refactoring around queries and stuff we were talking about?

nikomatsakis (Apr 15 2019 at 19:03, on Zulip):

I was guessing you might be given how you jumped on the id stuff

nikomatsakis (Apr 15 2019 at 19:03, on Zulip):

and the connection to RLS

detrumi (Apr 15 2019 at 19:03, on Zulip):

Yeah I'm definitely interested

nikomatsakis (Apr 15 2019 at 19:04, on Zulip):

:+1: ok, so let's try to make some time to sync up on that more deeply in a bit, perhaps with @Sunjay Varma.

nikomatsakis (Apr 15 2019 at 19:05, on Zulip):

I'm not sure who's still around, I feel like this meeting is over

nikomatsakis (Apr 15 2019 at 19:05, on Zulip):

But I'm interested in starting another one to talk a bit more about the next steps on rustc-chalk integration :)

nikomatsakis (Apr 15 2019 at 19:06, on Zulip):

@Aaron Turon you around?

nikomatsakis (Apr 15 2019 at 19:07, on Zulip):

(cc @scalexm -- were you around today?)

nikomatsakis (Apr 15 2019 at 19:07, on Zulip):

I was looking over the current sprint document, and I guess it's still more-or-less ok.

scalexm (Apr 15 2019 at 19:07, on Zulip):

@nikomatsakis I wasn’t, just got out of work

scalexm (Apr 15 2019 at 19:07, on Zulip):

I’ll read over after dinner

nikomatsakis (Apr 15 2019 at 19:08, on Zulip):

No worries, the tl;dr is that I'm going to land my PR and try to write-up some concrete "next steps" as far as chalk query-ification goes

scalexm (Apr 15 2019 at 19:08, on Zulip):

Ok seems good, I skimmed through the PR already and it looked good

nikomatsakis (Apr 15 2019 at 19:08, on Zulip):

I was just thinking about the more general topic of rustc-chalk integration

nikomatsakis (Apr 15 2019 at 19:09, on Zulip):

I feel like there are two tricky topics:

nikomatsakis (Apr 15 2019 at 19:09, on Zulip):

and they are actually somewhat related

scalexm (Apr 15 2019 at 19:09, on Zulip):

Why do you think they are related?

nikomatsakis (Apr 15 2019 at 19:10, on Zulip):

not deeply related but

nikomatsakis (Apr 15 2019 at 19:10, on Zulip):

I think that when we encounter a ?T: Sized goal, we basically know that we want to defer it and try to do other work, and then come back to it later

nikomatsakis (Apr 15 2019 at 19:10, on Zulip):

right now that's not really what we are doing

nikomatsakis (Apr 15 2019 at 19:11, on Zulip):

(indeed, SLG solvers have a mechanism for doing this already, though its purpose is for handling negative cycles)

nikomatsakis (Apr 15 2019 at 19:11, on Zulip):

when you think about it, that's kind of what we are doing with region goals too

nikomatsakis (Apr 15 2019 at 19:11, on Zulip):

i.e., we're proving that "X is true modulo this subgoal G that we chose not to solve"

nikomatsakis (Apr 15 2019 at 19:12, on Zulip):

anyway, i'm not sure if we want to handle them through the same mechanism, but we might.

nikomatsakis (Apr 15 2019 at 19:13, on Zulip):

regardless, I thought it would be useful to try and spend some time talking about how the SLG solver works, both at a theoretical level and an actual level (like, how the chalk-engine crate is implementd)

nikomatsakis (Apr 15 2019 at 19:13, on Zulip):

and was going to propose that we try to schedule a (recorded) meeting to do that -- ideally this week, though that might be hard to schedule

scalexm (Apr 15 2019 at 19:14, on Zulip):

@nikomatsakis ok i like the idea of talking about the SLG solver

scalexm (Apr 15 2019 at 19:15, on Zulip):

This week might be tricky for me regarding scheduling

nikomatsakis (Apr 15 2019 at 19:15, on Zulip):

OK, here are some questions:

nikomatsakis (Apr 15 2019 at 19:16, on Zulip):
nikomatsakis (Apr 15 2019 at 19:16, on Zulip):

I'm thinking maybe next monday could be good

nikomatsakis (Apr 15 2019 at 19:16, on Zulip):

in terms of giving time to prepare and meeting scheduling constraints

scalexm (Apr 15 2019 at 19:17, on Zulip):

Yes next Monday is good, it’s an holiday here

nikomatsakis (Apr 15 2019 at 19:17, on Zulip):

I have to go review, I think what I would ideally do is to cover

nikomatsakis (Apr 15 2019 at 19:19, on Zulip):

the paper "A New Formulation of Tabled Resolution with Delay"

nikomatsakis (Apr 15 2019 at 19:19, on Zulip):

sorry, got lost hunting for a link and gave up

nikomatsakis (Apr 15 2019 at 19:19, on Zulip):

that's the more theoretical side, anyway

nikomatsakis (Apr 15 2019 at 19:19, on Zulip):

and try to map it to what the code does

nikomatsakis (Apr 15 2019 at 19:19, on Zulip):

it'd kind of be good for me to remember too

nikomatsakis (Apr 15 2019 at 19:20, on Zulip):

anyway, ok, so shall we schedule something for monday?

scalexm (Apr 15 2019 at 19:20, on Zulip):

Seems fine to me

nikomatsakis (Apr 15 2019 at 19:20, on Zulip):

I wonder if that's a holiday for me, too

nikomatsakis (Apr 15 2019 at 19:21, on Zulip):

(no)

nikomatsakis (Apr 15 2019 at 19:21, on Zulip):

Given that it's a holiday for you, @scalexm, would you rather do a bit earlier?

nikomatsakis (Apr 15 2019 at 19:22, on Zulip):

I'll just make a doodle

scalexm (Apr 15 2019 at 19:23, on Zulip):

Yeah earlier is even better

nikomatsakis (Apr 15 2019 at 19:23, on Zulip):

OK -- if you're interested in learning about the chalk-engine crate and SLG solving, doodle poll here

nikomatsakis (Apr 15 2019 at 19:27, on Zulip):

Looks like 12:00 noon is the winner

nikomatsakis (Apr 15 2019 at 19:28, on Zulip):

(Boston time)

nikomatsakis (Apr 15 2019 at 19:28, on Zulip):

I'll just go schedule that

nikomatsakis (Apr 15 2019 at 19:29, on Zulip):

Calendar event

Last update: Nov 18 2019 at 01:45UTC