Self-correcting code

Stream: mathlib4

[Damiano Testa]

This post is a short summary with some ideas about self-correcting Lean code.

Since Mathlib changes so quickly, I think that it is important that Mathlib itself, and the projects that depend on it, can be automatically updated as much as possible.

[Damiano Testa]

My experience so far is limited, but promising:

• replacement of refine' with refine, where simply adding ? in the right places was enough;
• removal of unnecessary set_option ... in;
• adding (since "YYYY-MM-DD") to deprecated that were missing it;
• renames after a deprecation.

[Damiano Testa]

In all of these cases, this is what the workflow has been.

• Plant code in Mathlib that guides where the changes are supposed to take place and what the change should be (e.g. a line/column number, some old-name/new-name pair, the more specific the better) -- this has been a linter in the cases above.
• Run lake build to retrieve all the information about the replacements.
• Write a parser for the output of lake build that takes the information that was planted and acts on it.

[Damiano Testa]

For this to work, the simplest is to have "atomic" changes: add since ..., shorten long lines, remove a set_option ... in. The simplest the change, the higher the success rate.

[Damiano Testa]

Ideally, another tool (probably human for quite some time!), would compute something like the "edit distance" for a PR, that fragments it into a sequence of elementary changes that ideally fit well with the program above. Such a tool could be an evolution of Alex Best's leaff (of which move-decls is a very primitive, text-based butchering).

[Johan Commelin]

@Mario Carneiro Had similar ideas for a lake exe refactor. I think it would be really great to have such a tool!

[Damiano Testa]

I also just remembered about the replacement of theorem with lemma, whenever theorem does not have a doc-string.

[Damiano Testa]

In case anyone is feeling adventurous and wants to automate some deprecations, I would be very happy if they used lake exe update_deprecations (instructions in the repo) and reported back any short-comings/bugs!

[Mario Carneiro]

@Johan Commelin An initial draft of lake exe refactor is ready at #13973 . It would be good to try using this to do one of those back burner refactorings like (what is left of) refine -> refine', and refine the interface a bit before merging.

[Mario Carneiro]

also cc: @Damiano Testa , maybe you have some linter ideas in the pipeline that can be expressed as refactors instead / in addition

[Damiano Testa]

Yes, the "unnecessary set_option ... in" linter is a good candidate (and I already wrote a self-corrector for it).

[Damiano Testa]

Btw, in the code that I was using, the analogue of your Edit also had a field for the current syntax, as a check and would perform the substitution only if the current syntax matches the expectation. I could not see this in your code: have I not seen it? Do you think that it would be useful?

[Mario Carneiro]

We talked about having some constructors for Edit, which could do that kind of sanitization. I think that any Edit returned from runRefactoring should be considered as real edits, so that the edit application logic doesn't have to do parsing

[Damiano Testa]

More generally, any "unnecessary/unused syntax" linter is a good candidate.

[Damiano Testa]

Also, if you want to test your refactor tool, the have vs let linter has a lot of hits in mathlib.

[Damiano Testa]

(although it is silent by default.)

[Damiano Testa]

And the multigoal linter would be probably a good challenge!

[Mario Carneiro]

is the multigoal linter auto-fixable?

[Damiano Testa]

I am not sure that I tried to make it so, but I think that it could be made autofixable. I need to think a little bit about it, though.

[Mario Carneiro]

have / let sounds like the easiest one

[Damiano Testa]

I suspect that the same tracking logic for metavars that is used in the flexible vs rigid tactics can be used with the multigoal linter. But that would be quite a bit of extra code.

[Mario Carneiro]

you can import mathlib in Refactor.Main if you need

[Damiano Testa]

have / let is indeed easier, but not straightforward either if you want to have 100% success rate.

[Mario Carneiro]

hopefully the flexible vs rigid linter can share code with the refactoring

[Damiano Testa]

Also, the current "unnecessary simpNF" could be adapted -- at least the case in which there is nolint simpNF and no more linters are disabled in that call.

[Damiano Testa]

Ah, "theorem with no doc-string to lemma" should be really straightforward! I'm sure that you love this one...

[Damiano Testa]

For this one, there is also no need to worry about long lines: it is a simple translation.

[Mario Carneiro]

I'm not sure I like the polarity of that auto-fix

[Mario Carneiro]

I'd prefer the theorems get documentation

[Damiano Testa]

You mean that refactor should add doc-strings to undocumented theorems? :rofl:

[Mario Carneiro]

But I guess you could autofix and then review the changes to undo and document theorems that should have been documented

[Mario Carneiro]

or I suppose you could call chat-gpt or something

[Damiano Testa]

Anyway, that one is a really straightforward text trasliteration that could be a good test, whether you want to keep the result or not.

[Mario Carneiro]

and honestly a pretty cool / nontrivial application of a "refactoring"

[Damiano Testa]

That linter should be already ready.

[Damiano Testa]

Let me dig up the PR

[Damiano Testa]

#12869

[Damiano Testa]

The conflict is just the alphabetization of the "import all" files.

[Damiano Testa]

What about trying it with

def runRefactoring (cmd : TSyntax `command) : CommandElabM (List Edit) := do
  unless (cmd.raw.find? (·.isOfKind ``Lean.Parser.Command.docComment)).isNone do return []
  match (cmd.raw.find? (·.isOfKind ``Lean.Parser.Command.theorem)) with
    | none => return []
    | some thm => return [
      { replacement := "lemma"
        range := (thm.getHead?.getD default).getRange?.get! }]

[Damiano Testa]

(Assuming that I understood correctly the meaning of Edit.)

[Damiano Testa]

Also, I am not sure that I have a use for TSyntax instead of a plain Syntax: after all, a plain Syntax is what you get our of Linter.run as well.

[Damiano Testa]

I tested this: it replaced

import Mathlib.Tactic.Lemma

theorem replaceMe : True := .intro

/-- i have a doc-string -/
theorem doNotReplaceMe : True := .intro

lemma doNotReplaceMeEither : True := .intro

with

import Mathlib.Tactic.Lemma

lemma replaceMe : True := .intro

/-- i have a doc-string -/
theorem doNotReplaceMe : True := .intro

lemma doNotReplaceMeEither : True := .intro

Success!

[Damiano Testa]

I left lake exe refactor running in #13979 on all of Mathlib.

[Johan Commelin]

@Mario Carneiro wonderful! I will surely be playing with this a lot!

[Siddhartha Gadgil]

Mario Carneiro said:

I'd prefer the theorems get documentation

A reminder that a bunch of machine generated docs are available at https://math.iisc.ac.in/~gadgil/descs/ (and more have been recently generated).

[Damiano Testa]

At least one problem with the code above that I posted is that refactor climbs up in imports, so reaches quickly a file where lemma is not available. I wonder whether climbing down should have a flag, so that you can guarantee the existence of some syntax.

[Damiano Testa]

The "non-documented theorem to lemma" via refactor was successfully build by CI: #13979.

[Mario Carneiro]

Damiano Testa said:

At least one problem with the code above that I posted is that refactor climbs up in imports, so reaches quickly a file where lemma is not available. I wonder whether climbing down should have a flag, so that you can guarantee the existence of some syntax.

For tests like this, the easy thing to do is to check if the lemma declaration exists, or a module of interest is imported, and otherwise just return []

[Mario Carneiro]

I guess I should add a function which runs before any commands are processed since it might be possible to short-circuit before running the elaborator at all

[Damiano Testa]

Yes, this is what I ended up doing in the PR that successfully made the replacement.

[Damiano Testa]

In general, though, I still think that it is a fairly common situation where you want to refactor starting from a given module, rather than up to a given module.

[Mario Carneiro]

the walking up is a necessity, you should just think of it as running over the whole project

[Mario Carneiro]

it doesn't process the files in order

[Damiano Testa]

Ok, in any case, the workaround is simple enough.

[Mario Carneiro]

but I think what you want is to have that short circuit. There are two possible points at which it could be placed:

• Before running the subprocess: here we know only the name of the module and its direct imports
• After running the subprocess and processing the imports: here we know the module's recursive dependencies and also the list of declarations in the environment

[Mario Carneiro]

either one would save you a lot of elaboration cost

[Damiano Testa]

I am not too good with performance aspects, but I did find that with the (probably very inefficient) code that I wrote, it took quite a long time to replace all doc-less theorems by lemmas. Granted that it is a lot of operations, but I wonder whether maybe it might be a good test to perform "quickly".

[Mario Carneiro]

keep in mind that lake exe refactor is necessarily lower bounded by the cost of building mathlib

[Mario Carneiro]

even if you do nothing at all

[Mario Carneiro]

although this is not completely true if you use the aforementioned short-circuit

[Damiano Testa]

But it does use oleans, if they are available? Or not?

[Mario Carneiro]

it uses them, but it's still basically equivalent to a full build of every file

[Damiano Testa]

Ok, then it was probably not so bad, given that the refactor and the successful build took 1h20 (if I remember correctly).

[Damiano Testa]

Btw, is there a notion of just building the syntax trees? I imagine not, due to the very flexible extensibility of the language, but you never know... :smile:

[Mario Carneiro]

I've been asking for this for a very long time. This project is the result of deciding that I can't wait on that forever

[Damiano Testa]

Is it "theoretically" possible to just parse the syntax though? At least you should parse also syntax extensions, right?

[Mario Carneiro]

see also https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/quick.20and.20dirty.20mode

[Damiano Testa]

Ok, yes, I have seen these discussions. Let's hope that something happens along these lines!

[Damiano Testa]

I think that in the long run, it might make sense to abstract runRefactoring into an argument to lake exe refactor, so that we may then do lake exe refactor deprecations or lake exe refactor unnecessary_syntax or whatever and each calls refactor with the specialised runRefactoring function.

[Damiano Testa]

What would be the view of having certain "self-correcting" linters run on a schedule using refactor? For instance, a good candidate for this could be the "unused tactic" linter, flagging tactics that do not change any metavariable (note that this is different from the unreachable tactic linter). E.g., when I ran it several weeks ago it flagged a few congrs, some norm_nums maybe for which the list of metavariables before and after the tactic was unchanged.

The linter could produce the metaprogram that feeds into refactor and then refactor could perform the replacements.

[Damiano Testa]

In order to maximize self-referentiality, the linter could write a metaprogram that instructs refactor to modify runRefactoring inside its own file, in such a way that a second run of refactor would perform the removal of unused tactics.

[Mario Carneiro]

I don't think there is any need for self modifying code here (except insofar as any refactor is modifying code). The original idea was to have a small library of named refactors which can be selected either at the command line as you suggest, or via some easily editable script (i.e. runRefactoring is a one liner which calls a previously prepared refactoring function). For "unused tactic", we can just permanently have such a refactoring available but not called by default. There is no need for a linter to write the refactoring, they just share a common bit of code.