Syntax for attributes loaded by plugins

Stream: lean4

[Thomas Murrills]

Most often the fact that plugins do not load syntax is not an issue, but attribute syntax provides an example of where an interaction can occur.

Let's say I've loaded an attribute @[plugin_attr] via plugin (either defined in the plugin itself or one of its dependencies). The attribute is still initialized and its add field is applied to the attribute syntax. However, because the syntax (name := pluginAttr) "plugin_attr" : attr syntax was not added, the syntax fed to add is merely of kind Attr.simple, not plugin_attr. This means that a typical match stx with | `(attr| plugin_attr) => ... in add fails, yielding an internal exception when Elab.throwUnsupportedSyntax is used, as is typical. (Note: elabAttr has special handling for Attr.simple which identifies the relevant extension and feeds the syntax to its add in the first place.)

I'm not sure if the right approach here is to somehow load the meta phase of plugins (which might be more possible now than before thanks to the module system?), special-case attribute syntax when loading, modify attr antiquotations somehow, or, perhaps most likely...just deal with the internal exception messages, since plugins are not widespread (yet!). But thought I'd bring it up! :)

Here's an example package (OutletPkg 2.zip), and some code logging the differing attribute syntax between an attribute from a plugin and one loaded in the ordinary way:

module

import OutletPkg.Basic

/--
info: input syntax: (Attr.simple `plugin_attr [])
---
info: failed to match
-/
#guard_msgs in
@[plugin_attr]
def foo := 4

/--
info: input syntax: (regular_attr "regular_attr")
---
info: regular attr success!
-/
#guard_msgs in
@[regular_attr]
def bar := 4

[Sebastian Ullrich]

This looks like a misuse of plugins. If something is required for successful elaboration of a file, it should be an import. Could you un-XY?

[Thomas Murrills]

Sure! (I don't actually want to add attributes via plugin; I just want to avoid confusing errors.)

I'm experimenting with making Mathlib.Init (or at least the linter parts of it) a plugin. However, the new MathlibInit plugin requires Batteries, which means that batteries needs to be statically linked to the new plugin (see #lean4 > Load plugin during build?) (or dynamically linked in mathlib). However, this means that we see the internal exception on @[nolint _]s even when Batteries is not imported. I anticipate this would be a similar situation for any other plugin with dependencies—possibly for my actual, non-experimental use case as well (elaboration-aware refactoring utilities).

Maybe the solution is to somehow avoid feeding it to the plugin and have a typical unexpected attribute error, then? :thinking:

[Sebastian Ullrich]

What's wrong with importing linters?

[Thomas Murrills]

For one, we want them to apply library-wide, which means we need to make sure Mathlib.Init is imported in every file; plugins seem like a cleaner approach.

But this is just an experiment to stress-test plugins, ultimately; my actual use case is executing temporarily-active library-wide elaboration aware refactoring utilities via plugin. :)

[Thomas Murrills]

Also, I imagine this would be an issue for any plugin with dependencies, right?

[Sebastian Ullrich]

Thomas Murrills said:

For one, we want them to apply library-wide, which means we need to make sure Mathlib.Init is imported in every file; plugins seem like a cleaner approach.

But here "library-wide" means "anything not upstream of the linter definitions", right? So it's nontrivial either way and one viewpoint here could be that this should be a shake concern, like any other import management.

Also, I imagine this would be an issue for any plugin with dependencies, right?

Yes; one could expect that the meta initializes used to register attributes and so on should only be activated when building the plugin, not when running it. Separation of build-time and run-time generated code like this is the last remaining major goal of the module system that I will focus on next quarter.

[Thomas Murrills]

Sebastian Ullrich said:

But here "library-wide" means "anything not upstream of the linter definitions", right?

Only technically; we carefully bottleneck through Mathlib.Init, and have linters to ensure that Mathlib.Init is imported in every file that is not a dependency of Mathlib.Init. That is, it already more or less functions like a separate library used as a plugin for the rest of mathlib.

[Thomas Murrills]

Also, I'm a bit surprised that loading linters as plugins is (apparently?) not envisioned as a primary use for plugins! (Or is it?) What is the intended use of plugins, if not initializing linters and environment extensions?

[Thomas Murrills]

(By the way: downstream repos also take advantage of the mathlibStandardSet of linters. I imagine it would be easier for them to simply add a MathlibInit plugin to their library rather than making sure each of their files imports Mathlib.Init!)

[Thomas Murrills]

One more adjacent thought: a plugin model could hypothetically be useful in providing e.g. temporary, convenient, interactive hash commands everywhere in a library without needing imports. (Of course, this is not supported at the moment.) This conflicts a bit with the notion that file elaboration shouldn't depend on plugins, but having library-specific "development tools" at your fingertips without having to add imports would be really nice.

[Kim Morrison]

I think with plugins a barely-used, undocumented feature, we shouldn't bother trying to use them to do things that already work (e.g. Mathlib.Init) "better". If they are necessary for a new, signficant feature, sure, let's endure the cost of making plugins a viable tool.

[Thomas Murrills]

I totally agree. :) Pluginizing Mathlib.Init is (only) an experiment to assess the limitations (and pitfalls) of plugins themselves, which can otherwise be hard to encounter in simpler cases. In principle, it "makes sense" for Mathlib.Init to be a plugin, but for sure—actually making it one would only be a good idea if/once plugins are streamlined, predictable, and reliable.

P.S. There's a demo—not ergonomically at library scale yet—of what I'm working on that motivates this investigation into plugins at #mathlib4 > Demo (Skimmer): replacing deprecated declarations, plus some discussion of the requirements here that make plugins useful for, well, plugging in such tools. :)