Auto-fixing files

Stream: mathlib4

[Mario Carneiro]

Now that I have gotten my feet wet in doing syntax rewriting, I would like to discuss how we should handle whole-file rewrites, thinking in particular about porting file cleanup activities. For concreteness, let's consider replacing unused variables marked by the linter with _ or _x.

1. We could have a code action that triggers when your cursor is on the warning, and adds the underscore. I checked what rust-analyzer does here, and it appears to read the error message (which has a mechanism for giving auto-applicable fixes) and apply the suggestion to insert _ at the start of the variable name. (Replacing with _ is not a suggested option.) This seems like something we should have anyway. (When there are multiple warnings within the span of the selection, it gives several code actions, one for each warning. So it's not really suitable for auto-fixing the whole file.)

2. For more large scale cleanups, rust has a cargo fix command which applies all auto-applicable fixes. I think this is also the interface we might want for porting changes: a standalone tool which reads the file and applies all rewrites of a certain kind.

3. We also have the option of a #lint like interface, where the user writes a command at the bottom of the file and it has a code action on it which applies some changes to the whole file. In the case of linter warnings, we might be able to get away with this because warnings are cumulative across the file, but many code actions use the info tree and this is cleared after every command, so it's probably not the best option for other things.

4. We could have a whole-file code action, where you select a large region or the whole file and then apply the code action. I don't think the code actions API is set up to handle this though, it will just give you a snapshot from the beginning of the file and you still don't get the rest of the info tree.

[Mario Carneiro]

Some other auto-fixes we might want to consider for post-port mathlib files:

• replacing fun x => e with fun x ↦ e
• replacing induction' e with a b c with induction e with | foo a => ... | bar b c => ...
• auto applying the <;> linter suggestion
• whole file formatting (I'm not sure what we have is good enough for this); this is also potentially a "reformat" code action, although I would prefer to minimize code actions that are always applicable since then the lightbulb never goes away

[Yaël Dillies]

Do mass edits of declaration names fall under that category of auto-fixes?

[Mario Carneiro]

I suppose it could. I think we might want to use a slightly different mechanism for that though, since we don't want to have to compile all of mathlib to get all the ASTs we need to do that. I wonder if the .ilean files have enough info to identify all uses of a constant?

[Yaël Dillies]

You know more than me, but I'm expecting the point of such a mass-edit to precisely be that it has access to more information than is available with regex. I do wonder how to handle docstrings, though...

[Mario Carneiro]

I am not suggesting a regex, but I was thinking mainly about whole-file edits for my original post, while global renaming is a whole-project edit

[Mario Carneiro]

For single-file edits it is reasonable to have the info tree available with some work, but for multiple-file edits if you need the info tree then that equates to compiling the whole project, because the info tree is not persisted as a build artifact

[Mario Carneiro]

The .ilean files have a watered down version of the info tree which is likely sufficient for the specific case of global renames (it is already sufficient for doing "find all references", and I think we could implement global rename today with just a bit of extra server code)

[Mario Carneiro]

honestly I'm not sure why local rename doesn't work already, it would be easy enough to use the local references information used for go-to-def/references requests for renames as well

[Sebastian Ullrich]

It's not completely trivial around namespaces and dot notation I think. And I don't know if it wouldn't be better to strive for global rename immediately

[Sebastian Ullrich]

whole file formatting (I'm not sure what we have is good enough for this)

If the current pretty printer was up to that task, I would have implemented auto-formatting a long time ago :) . I also still believe that doing structural, whitespace-unaware modifications to the syntax tree and then reformatting that part/the entire declaration would be the most robust way to implement more complex refactorings, but it's great to see that simple string editing works well for the refactorings you've been working on

[Mario Carneiro]

One reason I am sticking to string manipulation is because I am scared to delete comments or disturb other existing formatting with a more AST centric approach

[Sebastian Ullrich]

If there is a code formatter that's good enough so that the entire project is formatted with it, there is no formatting to disturb anymore. Making sure no comments vanish would also be simple by comparing the old and new CST, but giving them a reasonable position if they are within the affected region is harder, yeah.