Skip to content

feat: Backreporters - #170

Draft
thorimur wants to merge 20 commits into
leanprover-community:mainfrom
thorimur:backreporters
Draft

thorimur wants to merge 20 commits into
leanprover-community:mainfrom
thorimur:backreporters

Conversation

@thorimur

@thorimur thorimur commented Oct 2, 2026 •

Copy link
Copy Markdown
Collaborator

This PR adds backreporters, which provide a means for command elaborators to request that certain actions are run at the end of the file.

We use this to implement #min_imports, which needs to be run in a ModuleLinter to see the current module's full array of parsed Syntax. This also enables it to be written anywhere in the file.

This PR takes care to allow command elaborators sending requests to backreporters to place a progress indicator (e.g. a yellow bar) at the requesting command until the request is fulfilled when in interactive contexts.


Backreporters are currently tested in the dependent PR #168 through their use in #min_imports.

@thorimur
thorimur marked this pull request as ready for review October 2, 2026 23:32
@JovanGerb

JovanGerb commented Oct 6, 2026 •

Copy link
Copy Markdown

It looks like this PR is actually doing much more than the PR description claims. The PR implements a general framework for backreporters, and then runLaterReporter which is an instance of a backreporter.

Because there is only one use case for this pair of frameworks, I think this is over-engineered for the task at hand. I know that you want to provide general infrastructure when you have the chance, but I think you should also consider the maintenance cost of having a bunch of code that is essentially redundant.

Though of course I'm not maintaining import-graph, so take this with a grain of salt.

@thorimur

thorimur commented Oct 7, 2026 •

Copy link
Copy Markdown
Collaborator Author

I think the maintenance costs are reversed. If you make n special-purpose approaches to n tasks, that forces refactoring and maintenance for each down the line. Whereas if you invest in general-purpose infrastructure up front, you do not need to maintain n special-purpose designs down the line, and the overall maintenance costs are lower.

@JovanGerb

Copy link
Copy Markdown

This PR provides two general frameworks (back reporters and runLaterReporter) and for both I don't see any other use cases, so it looks like n = 1?

@thorimur

thorimur commented Oct 7, 2026 •

Copy link
Copy Markdown
Collaborator Author

Yes, that's correct...currently. But I'd say maintenance (and designing for maintenance) is entirely about the future. :)

My response to this grew quite long, but here it is in a more abbreviated form. (As you can see by this being the abbreviated form, I have some thoughts on this matter! 🙃 )

  • Upstream interface design choices & availability shape downstream choices and maintenance costs.
  • Most often, you don't know what people are going to use an interface for.
  • If you only do what is necessary, you sooner or later incur friction at each point someone needs something slightly different.
    • Namely, depending on the precise way in which upstream is "too specific", people will either: work around things with hacks; build infrastructure downstream even though it is more generally useful adjacently, potentially resulting in duplicate work (upstream is "more available"); petition for an upstream change before moving on with their project; simply not do anything when they see it's not "blessed" by the interface; and/or generally be forced to put in more work each time they interact with the pared-back, specific interface, either through creating bespoke approaches each time or repeating boilerplate, meaning that all of them need more maintenance.
  • Whereas if you provide general interfaces and convenient entry points to those interfaces when you first need something, without molding the interfaces to the specificity of the problem you're solving immediately, you can avoid these future costs at a slightly higher up front cost.
  • This is ultimately the same reason I think code should be factored well and APIs should be fleshed out: by providing flexible reusable tools you reduce future costs/increase the things that get done.
  • This is not an argument for feature-maximilism, as providing and maintaining tons of features that are not necessarily used indeed may create too high a maintenance cost relative to their use, but may also create complexity downstream, since now we are not providing flexibility through generality (which may be simple to use on the outer side of the interface), but flexibility through complexity (which may actually make downstream interactions with the interface more difficult—there's too much to keep track of)

There is an alternative view (not saying this is yours necessarily) which says that all or most code should be motivated by current use cases; "you aren't gonna need it", I've seen it said. There's a balance, right? It's true that sometimes you don't need it. (This is also part of flexibility-through-generality rather than flexibility-through-complexity.) I worry that such an approach not only makes the aforementioned friction more likely and maintenance costs higher overall, but also changes the trajectory of what is made.

Since we're in an ecosystem with people that are bottlenecked on volunteer time (and as a consequence sometimes skill level and maintenance time), which interfaces already exist and how costly they are to use partially determines what gets made in the first place. And the thing is that if you don't provide these interfaces up front, you may simply never hear about what didn't get made. It may just silently not exist, and the "you're not gonna need it" reasoning appears unrefuted despite causing meaningfully different outcomes.

Anyway, that's a bit of my maintenance + library development philosophy more generally :) (Btw, I go into a couple of these themes in my LT2026 talk, but surely it's quite gauche to say "I refer you to this talk I've given on the matter" in a github comment! XD)

But yes, these are indeed interfaces that are factored to be more general than just the #min_imports needs, and that's deliberate :) I wrote the PR description in a bit of a rush the other night, so indeed I should update it.

@thorimur

thorimur commented Oct 7, 2026 •

Copy link
Copy Markdown
Collaborator Author

I'll also mention to anyone looking at this PR that Kim ran this through Fable and produced the linked gist of comments which I plan to respond to when I get back from PTO next week. As such I'll mark this as a draft PR until then.

(I should also say to anyone reading that Kim kindly offered to convert this into inline comments or digest them herself, but I said I was happy with the gist—Kim didn't simply throw a gist at me! :) )

@thorimur
thorimur marked this pull request as draft October 7, 2026 04:27
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants