!4#3162 variable!

Stream: PR reviews

[Scott Morrison]

@Kyle Miller, what would you like to do with variable!? It seems the options are:

• merge as is, as a tool that people can use but won't commit to mathlib
• wait, and you or someone else could add the ? mode discussed previously

There's also the question of what to do with the example @Eric Wieser found where it gets the answer wrong. I'm happy if the solution to that is "keep track of it". :-)

[Kyle Miller]

@Scott Morrison I tried getting the ? proposal to work in an ergonomic way, but there are a couple problems I ran into. Maybe I'll go check if anything in that work should be pushed into the PR and then we merge a first version without this feature?

[Scott Morrison]

Sounds good.

[Kyle Miller]

@Scott Morrison I've just pushed the changes, which includes turning it into the less-emphatic variable? command. It now always suggests a "try this".

I guess if you want a silent version in non-mathlib code, you could do

#guard_msgs (drop info) in variable? [Module R A]

or make a macro that expands to that.

[Kyle Miller]

The UI/ergonomics issues I had with the variable! [Module R M] => [Semiring R] [AddCommMonoid M] [Module R M] idea were that

1. ideally you'd also elaborate what's before the => otherwise you don't get any info when you hover in an IDE, but then you need to handle elaborating these at the same time as the corresponding binder on the RHS to do it in a similar context to avoid confusing situations when there's some shadowing (ideally there would be none, but you don't want to be more confused than you already are), and there's no good way to link up binders on the LHS with the RHS short of a lossy equality that tries to throw away whitespace differences;
2. figuring out how to get the unused variables linter to handle this more complicated syntax, given that I just copied the one for variable and the unused_variables_ignore_fn attribute is a dark art;
3. questions around checking that the cached expanded binders actually are the expansion of the LHS binders.

[Mario Carneiro]

(1) sounds solvable, you just need to use the same lctx for both elaborations and roll back the result

[Mario Carneiro]

the second part of (1) also sounds solvable, since you end up with two extended contexts and can compare them for expr equality (e.g. defeq)

[Mario Carneiro]

and I guess this is also (3)

[Kyle Miller]

for 1 the problem isn't the rolling back, it's the figuring out how the LHS is a subsequence of the RHS to line up the binders, and this didn't really seem worth pursuing, at least to me right now.

I'd considered a variant variable! +[Semiring R] +[AddCommMonoid M] [Module R M] to simplify the problem, but then it mixes all the added binders into the command, which goes against one of the goals of having a readable short version.

The complexity is all based on the assumption that the variable! command's algorithm can be slow, so it's worth avoiding running it when there's a => cache, but maybe it's not slow enough for anyone to care in the end.

[Scott Morrison]

Oh, what if we go for the middle ground:

• don't actually use the cache, just recompute every time
• people by default leave the full Try this: output with => in place
• but whenever that is annoyingly slow, replace it with the part to the right of =>.

(Perfect being the enemy of good.)

[Kyle Miller]

@Scott Morrison Ok, I think the middle ground is implemented now.