ToExpr derive handler

Stream: std4

[Scott Morrison]

I'd like to upstream the ToExpr derive handler, and have PR'd this as https://github.com/leanprover/std4/pull/221. @Kyle Miller, we are missing some doc-strings here, as these files were added to Mathlib while we had the doc-string linter turned off. Is there any chance you would be able to write the missing doc-strings? If you don't have availability I will come up with something!

[Eric Wieser]

This will conflict with the #5952 from @Gabriel Ebner and me. Does Std4 take a Qq dependency?

[Mario Carneiro]

No, std has no dependencies. I think if we are considering that then Qq should perhaps be merged with either std or lean core

[Eric Wieser]

If there's some contention here, can we PR the docstrings to mathlib first so that we have them either way?

[Kyle Miller]

I'd written this as a comment to Eric on the std4 PR about #5952, and I'll copy it here:

I'd prefer if ToExpr were left alone and there be a completely new ToExprQ, mainly because ToExpr still exists in core. I know that you have this instance so deriving ToExprQ gives you a ToExpr instance, but still, I'd like to see ToExpr be deprecated in favor of ToExprQ rather than be replaced by it.

[Scott Morrison]

This sounds correct. ToExpr in core is not going to change, and the derive handler is useful for people who don't need Qq.

[Eric Wieser]

Can we avoid having two almost-duplicates of Kyle's derive handler?

[Mario Carneiro]

Do we need a ToExpr derive handler? We can just have an instance that derives it from ToExprQ

[Eric Wieser]

The claim is that people not using mathlib/Qq need the ToExpr handler

[Mario Carneiro]

why?

[Eric Wieser]

Because they don't have toExprQ available to them

[Mario Carneiro]

I think anyone using std will have ToExprQ if we are providing a derive handler for it

[Eric Wieser]

Are you arguing that std should depend on/absorb Qq?

[Mario Carneiro]

Mario Carneiro said:

No, std has no dependencies. I think if we are considering that then Qq should perhaps be merged with either std or lean core

[Eric Wieser]

Sorry, what I meant was "are you using that message to argue against Kyle's point above?"

[Mario Carneiro]

I think it's a pretty good candidate, I need Qq in any reasonably complicated tactic writing

[Mario Carneiro]

I think that for the purpose of this PR we need ToExprQ to be defined in std, but I guess the issue is that this class already exists and is defined in Qq?

[Mario Carneiro]

Maybe the least disruptive option would be to have std get a copy of Qq, just like it made a copy of Lean data structures

[Mario Carneiro]

and then people can migrate to Std.Qq if they are already depending on std and otherwise keep using Qq

[Mario Carneiro]

cc: @Gabriel Ebner

[Eric Wieser]

Eric Wieser said:

If there's some contention here, can we PR the docstrings to mathlib first so that we have them either way?

#6699, git applyd from the Std PR

[Eric Wieser]

Mario Carneiro said:

but I guess the issue is that this class already exists and is defined in Qq?

ToExprQ currently exists nowhere except #5952

[Mario Carneiro]

but ToExprQ has a type that needs Qq to state

[Eric Wieser]

So right now our choices are:

1. Merge std4#221, stranding #5952
2. Merge #5952, stranding std4#221
3. Duplicate Kyle's code for the toExpr handler (Std4) and the toExprQ handler (Mathlib 4)
4. Make Qq available inside Std4

[Mario Carneiro]

I think we should just not upstream this derive handler, and wait for the Qq situation to resolve

[Mario Carneiro]

merging #5952 SGTM

[Eric Wieser]

#5952 is blocked by #6699 for the same reason as the first message in this thread

[Scott Morrison]

Urgh, okay, I upstreamed the derive handler in order to make a project not depend on Mathlib, but now that is waiting on an indefinite project with no owner (migrating Qq into Std).

I guess I don't really care about not depending on Mathlib. :woman_shrugging:

[Kyle Miller]

Mario Carneiro said:

Maybe the least disruptive option would be to have std get a copy of Qq, just like it made a copy of Lean data structures

It seems to me that the least disruptive option is to merge std4#211, then once there's an owner for the project to migrate Qq into Std proceed to turn it into a ToExprQ handler.

[Eric Wieser]

What's the motivation for the migration to Std here? Is it to allow the derive handler to be used in a dependency of mathlib?

[Kyle Miller]

Eric Wieser said:

The claim is that people not using mathlib/Qq need the ToExpr handler

This isn't the point I was trying to make myself. I'm saying that we already have a ToExpr handler, so a reasonable way forward engineering-wise is to introduce a ToExprQ handler and deprecate the ToExpr one (and maybe delete the ToExpr one too; we can make a ToExpr handler that throws an error saying to derive ToExprQ instead). In the short term, it's true that since std doesn't have Qq then you'd need a ToExpr handler.

[Kyle Miller]

@Eric Wieser I think Scott explained it: "I upstreamed the derive handler in order to make a project not depend on Mathlib"

[Kyle Miller]

I'm also happy to see it be upstreamed because it really doesn't depend on mathlib in any way. It could even be in core in principle.

[Eric Wieser]

Sure, I guess my question was actually "what's the motivation for not depending on mathlib"?

[Scott Morrison]

It's a project that compiles other projects, extracting information at goal states, etc. I would like it to have minimal imports so people can use it by importing it into their project temporarily and running the scripts.

[Scott Morrison]

For the short term, where all I'm going to be running it on is mathlib itself, it is no particular problem to flip the dependency chain and depend on mathlib.

[Kyle Miller]

(Do we need to #xy this to determine whether it's appropriate to upstream this derive handler? For what it's worth, I only contributed the ToExpr handler to mathlib rather than std because it was a bit more convenient for me.)

[Scott Morrison]

But generally, I would really like to get generally useful programming stuff out of Mathlib --- it is a bad look for programming users if stuff they need is stuck in Mathlib.

[Scott Morrison]

(And I appreciate that a good long term solution is to move all this stuff, Qq and ToExprQ etc, into Std. But I like short term solutions with owners. :-)

[Eric Wieser]

Until we upstream Qq into Std, there's a tradeoff here between having more features, fewer dependencies, or duplicated code.

[Eric Wieser]

Maybe the compromise is just to have the code duplication, with an almost identical ToExprQin mathlib alongside ToExpr in Std4

[Scott Morrison]

I think not upstreaming something because we want to upstream more stuff is a recipe for not getting anything done, and unnecessary overhead.

[Scott Morrison]

The duplication is cheap to do, and hopefully motivates someone to do the work of migrating Qq and then upstreaming ToExprQ.

[Eric Wieser]

Will merging std4#221 force us to delete the toExpr handler from mathlib?

[Eric Wieser]

It will be easier to review #5952 if it can be left intact as a duplicate

[Kyle Miller]

Scott Morrison said:

I think not upstreaming something because we want to upstream more stuff is a recipe for not getting anything done, and unnecessary overhead.

Yeah, this is part of the subtext behind my original comment on the PR.

[Kyle Miller]

Eric Wieser said:

It will be easier to review #5952 if it can be left intact as a duplicate

Honestly, I'd be happier to review #5952 as a PR to a fresh file

I'm a little uncomfortable with this re-using-the-file-to-hatch-a-beautiful-butterfly, even if I like the butterfly

[Mario Carneiro]

the reason why my impression of this discussion is that we shouldn't upstream the ToExpr handler is that it seems it will soon be out of date, and I prefer not to put things in std4 which are going to change because I want to minimize churn for users of std

[Mario Carneiro]

mathlib is a better place to get something out quick and iterate on the design

[Kyle Miller]

@Mario Carneiro The problem is that it only might be soon, since it doesn't seem like anyone is really taking ownership to guarantee it will be soon.

The deprecation of the ToExpr derive handler could be done in a way that users never notice, since it could call the ToExprQ derive handler instead.

[Mario Carneiro]

Isn't the ToExpr class fundamentally broken? Like, it doesn't track levels properly

[Mario Carneiro]

std isn't in a hurry to grow though, so if no one takes charge to work on the prerequisites then it might just be a while and that's fine by me

[Mario Carneiro]

I'd rather not rush a poor design and have to back it out later or be stuck with it

[Kyle Miller]

Mario Carneiro said:

Isn't the ToExpr class fundamentally broken? Like, it doesn't track levels properly

I wouldn't say it's fundamentally broken. The class itself doesn't track levels, but instances can use the ToLevel class, and it can assemble expressions with the correct levels just fine.

[Kyle Miller]

There are some bad instances in core that don't track levels, but I added some instances that override these.

[Mario Carneiro]

Is it possible to build a ToExprQ instance on a ToExpr instance?

[Kyle Miller]

"Yes" in that you can get the universe level of the type if you have access to MetaM, but "no" in that the class is non-monadic.

It should be easy to write a function ToExpr X -> MetaM (ToExprQ X).

[Mario Carneiro]

yeah, that makes me want to just ignore ToExpr then, this is just some bootstrapping thing that no one else should need to care about

[Scott Morrison]

@Mario Carneiro, could you just summarize the plan? I'm left a little unsure what has been decided here.

[Mario Carneiro]

For now, nothing in std; we want to hunt down Gabriel and have a discussion about moving Qq and then we might move the ToExprQ version of the derive handler later. You should either depend on mathlib or copy that handler into your project in the meantime.

[Eric Wieser]

In the meantime we may as well merge #6699, right?

[Scott Morrison]

Okay, I have updated the compile_time_search_path% upstreaming PR std4#222 so that it doesn't rely on the ToExpr derive handler anymore. Review appreciated, as I'd like to reduce the steady duplication of this across projects! :-)