variable commands: splitting binder updates and new decls

Stream: general

[Michael Rothgang]

#15439 splits a few variable statements in Geometry/Manifold, separating binder updates and declaring new variables. Doing both at the same time can yield confusing errors (see lean4#2789).

If this is desired (my understanding is it is), #15400 proposes a linter against this. Currently, the linter only lints in some cases (when the binder update is for a variable from a previous scope), but this already finds quite some cases in mathlib. Help going over the errors and fixing them is very welcome.
I tried to make the error message very clear; let me know if you're stuck.

[Johan Commelin]

@Michael Rothgang this seems useful! what is the status here? Should we look at #15400 first?

[Michael Rothgang]

I just pushed three local commits to #15400, which are basically tweaks to the error message.

Current status is that the linter needs to be improved first: the current behaviour both has false negatives (missing variable commands which should be split) and false positives (complaining about variables which should not be linted (though they might be a code smell)).

[Michael Rothgang]

In a nutshell, the linter works by

• parsing the variable binders in a variable command (this is not hard and works well; the code could be cleaned up, but that can happen in parallel to fixing errors)
• comparing these to the previously declared variables, i.e. the current scope before the command took effect
• using this to find variable commands which should be split (this is also not hard and works)

The second step is not fully implemented, as I don't see a nice and clean was to do this. (I am using an approximation, which leads to the issue above.) The issue is described here, in essence: calling getScope when the linter is run on the variable command returns the scope after the command, which is not what I need.

[Michael Rothgang]

My current plan for a fix is to make the linter

• replace the command by a section temp command
• elaborate that, then get the current scopes (after the section command)
• the previous scope then has the information I want
  Actually, if the above works, something simpler also does: just replace the variable by some other command (such as open Nat; I only care about the variables in the current scope)

I will get to this, perhaps this week, but help with above (or suggesting an easier fix, if it exists), is certainly appreciated! (Also with fixing the offenders, once the linter works well.)

[Damiano Testa]

I wonder whether there should be a way of choosing whether a linter runs before or after a command is elaborated. Currently, it is after and I do not think that there is a choice. Sometimes, though, being able to run some code before a command is very useful.

[Michael Rothgang]

That certainly would solve my issue.

[Johan Commelin]

That requires a patch to the linter framework, right?

[Damiano Testa]

I think so: I would be happy to learn that there is a setting for this, but I do not think that there is.

[Damiano Testa]

This, combined with withoutModifyingEnv would also allow to parse a modification of the linted command, without having to jump through hoops to avoid creating two declarations with the same name.