Is there any plan to make user-defined tactics usable on the UI?

[rbohrer]

When I use "tactic tacticName as ... " in my .kyx file and upload it, I can't type "tacticName" in the Web UI and call my tactic. Is there any plan to add this feature? This would be quite helpful for users who want to develop their own tactic libraries, in practice. Since it's common to do proofs in the Web UI, tactic definitions are less likely to get used if they can't get called from an interactive UI proof. I'm not particularly proposing to add any sort of fancy definition-management UI (like there is for function/predicate definitions). As long as there's a way to call the tactics that were in defined in the .kyx file, that would be impactful.

If I type "tactic tacticName as ...; tacticName" in the Web UI, it seems to partially work.

Of course, if I upload a finished proof, the user-defined tactics worked fine.

Priority: Non-urgent, but would be quite useful.