PR summary 931b42b075

Import changes for modified files

No significant changes to the import graph

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

@grunweg, this is a prototype for the "no whitespace linter"! I won't have time now to fix the spaces around explicit/implicit binders, but if you want to have a look at it, feel free to do so!

If you do and you can let me know the false positives, I'd be very grateful!

E.g., I'm already aware that the linter does not do the right thing with binders spanning more than one line, but I don't know what other issues it might have.

Thanks for asking! I took a look at the linter errors - the number is quite manageable (perhaps 50 warnings overall).

• A significant proportion are false positives.
• A number of them indicate real problems. After fixing these, usually some error persists (which is then off).

Here are some things I noticed, with some code examples (you can search the diff to find the relevant place) and what the linter prints for me.
0. Small issue, but: the suggestion always uses variable, even if the affected binder is in a theorem statement.

1. Often, the error message is off by two.
   Example: variable {X : Type u} prints j {U : Under ' should be printed as 'variable {U : Under X}; a similar issue occurred with variable {U : Under C}. (My hypothesis: the right hand side is multiple parts and not all of it is captured somehow?)

2. Another example, perhaps related: I get the linter output 'ble {D : Type u' should be printed as 'variable {D : Type u₂}' for the code variable {D : Type u₂} [Category.{v₂} D].

3. I wonder: is this one about nested binders?

def toOver (F : S ⥤ T) (X : T) (f : (Y : S) → F.obj Y ⟶ X)
    (h : ∀ {Y Z : S} (g : Y ⟶ Z), F.map g ≫ f Z = f Y) : S ⥤ Over X :=

prints '∀ {Y Z ' should be printed as 'variable {Y Z : S}'.

4. Is this one about composite notation? The linter prints '{ f : R →+* T' should be printed as 'variable {f : R →+* T}' on the code

irreducible_def preLift {r : R → R → Prop} {f : R →+* T} (h : ∀ ⦃x y⦄, r x y → f x = f y) :

5. Another interesting example, about the behaviour after correcting the error. Is this about incrementality, or some caching issue in the linter? The original code is variable [T2Space M] {α β γ : Type*}, the linter (rightly) prints '{α β γ : Type*}' should be printed as 'variable {α β γ : Type*}'.
   After correction and restarting the file, there is still an error, now saying '{α β γ : Type*' should be printed as 'variable {α β γ : Type*}'. That error is bogus, but looks like it's still using the old syntax (note the double space in the old message).

6. Perhaps this is the same as issue 5? In one example, correcting an issue makes the linter flag the next binders.
   Initial code was theorem countable_meas_pos_of_disjoint_iUnion₀ {ι : Type*} { _ : MeasurableSpace α} {μ : Measure α},
   the linter rightly printed '{ _ : MeasurableSpace α}' should be printed as 'variable {_ : MeasurableSpace α}'.
   Correct the error, now the code is theorem countable_meas_pos_of_disjoint_iUnion₀ {ι : Type*} {_ : MeasurableSpace α} {μ : Measure α}. Now the linter prints three errors!

• '{ _ : MeasurableSpace α' should be printed as 'variable {_ : MeasurableSpace α}'
• ' {μ : Measure α' should be printed as 'variable {μ : Measure α}'
• ' {As : ι → Set α' should be printed as 'variable {As : ι → Set α}'

I've pushed the ~10 true fixes to this PR.

Created #14662 as a by-product.

Quick, incomplete reply:

• using variable is a hack to produce valid syntax -- I'd like to not print it, but have not figured out how;
• the linter reads the file that is being modified, so caching and recent modifications in an unsaved file produce unexpected behaviour -- I found that saving and restarting the file works more reliably;
• one of the issues that you flagged seemed to have an extra space around a binder, so looked like a real case (maybe item 4?).

The shift in print I think boils down to what counts as a "character": some unicode symbols create some issues and I do not really know how to get consistent behaviour.

Quick, incomplete reply:

* using variable is a hack to produce valid syntax -- I'd like to not print it, but have not figured out how;

* the linter reads the file that is being modified, so caching and recent modifications in an unsaved file produce unexpected behaviour -- I found that saving and restarting the file works more reliably;

* one of the issues that you flagged seemed to have an extra space around a binder, so looked like a real case (maybe item 4?).

Ah, that explains. I wasn't saving the files - usually, that works (until it doesn't).

Michael, thank you so much for the complete report! Here is a more detailed answer.

0. I'd like to not print variable, but the binder alone is not valid syntax, so this is a hack to pretty-print something.

1+2. I think that these are mostly issues with unsaved changes in a file and using a cached version of the text.

3+4+5+6. These again seem to be caching-related.

Conclusions.

1. In its current form, the linter can only be reliably used in CI, since it gives often non-up-to-date information on modified files.
2. I did not find many false positives: in fact, after allowing a line break after a colon (:), I am hoping that all the warnings are correct (CI is still running).

This evolved into the ppRoundtrip linter.