Move some tactics to separate package?

Stream: mathlib4

[Jannis Limperg]

I'm currently extending Aesop with the ability to generate proof scripts, which would make use of mathlib's on_goal tactic. This is a problem because I can't depend on mathlib. I think I can work around this by defining my own aesop_on_goal and using that instead of on_goal whenever on_goal is not available (which I can presumably detect).

But it made me think: many of the tactics in mathlib are quite general-purpose and will also be useful for people who don't use mathlib. So should they be split out into a separate package (maybe std, maybe a new std-tactics)?

[Heather Macbeth]

Just wondering, why can't you depend on mathlib? I'm sorry if I missed a previous discussion here.

[Jannis Limperg]

Because Aesop is supposed to be used in mathlib. So the alternative is really to move it into mathlib. That would also be fine with me, but if we want to move to a less monolithic ecosystem, it would be nice if tactics which are not intrinsically tied to mathlib aren't bundled with it.

[Heather Macbeth]

I see. Speaking just for myself, I'd certainly be happy to have it in mathlib.

In any case, during the current phase with mathlib4 changing very fast, it might be easier to keep a monolith ...

[Jannis Limperg]

That's fair. Splitting off a separate std-tactics, which would presumably depend on std, would be an issue with the current infrastructure.

Actually, now that I think about it, you can already use Aesop together with mathlib4 only if the two packages agree on which std commit they depend on.

[Johan Commelin]

I think we should first port mathlib, and then think about splitting things into packages. Doing both at once sounds like extra complications to me.

[Alex J. Best]

on_goal seems to fit nicely in std itself to me, its a tactic that shouldn't need mathematical background and is quite general purpose, maybe @Mario Carneiro should be the one to move it though

[Mario Carneiro]

Yes, on_goal should go in std. Feel free to open a thread on the #std4 stream whenever you have a request to move something from mathlib4 to std4.