Sort lines by import order of files

Stream: general

[Anne Baanen]

So I have been cleaning up porting notes by searching for them in all files and testing each occurrence one by one, using commands like:

rg -i '10618' --vimgrep | sort | nvim -

which outputs a list of file of the form:

Mathlib/Algebra/Algebra/Hom.lean:51:19:-- Porting note (#10618): simp can prove this
Mathlib/Algebra/GCDMonoid/Basic.lean:123:19:-- Porting note (#10618): `simp` can prove this
Mathlib/Algebra/GCDMonoid/Basic.lean:128:19:-- Porting note (#10618): `simp` can prove this
Mathlib/Algebra/GCDMonoid/Basic.lean:869:19:-- Porting note (#10618): `simp` can prove this
Mathlib/Algebra/Group/Equiv/Basic.lean:474:19:-- Porting note (#10618): `simp` can prove this but it is a valid `dsimp` lemma.
Mathlib/Algebra/Group/Equiv/Basic.lean:479:19:-- Porting note (#10618): `simp` can prove this but it is a valid `dsimp` lemma.
Mathlib/Algebra/MonoidAlgebra/Defs.lean:1421:30:-- @[simp] -- Porting note (#10618): simp can prove this.
Mathlib/Algebra/MonoidAlgebra/Defs.lean:762:30:-- @[simp] -- Porting note (#10618): simp can prove this.
Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean:371:19:-- Porting note (#10618): simp can already prove this.

A big annoyance is that I finish editing one file, go to the next one on the list and have to wait for a few hundred intermediate files to compile because I touched a deep dependency.

One solution would be to have a little program that could sort a list of files in the above format by place in the import order (with leaves coming before roots). That way I shouldn't have to wait for any imports when I switch to the next file. Is anyone interested in building a command like this?

[Matthew Ballard]

I have wanted something like this also for the linter outputs.

[Ruben Van de Velde]

What I do is I make changes in vs code without saving - I just leave all changed files open until I'm done (or run out of memory). That means more dependent files will still compile using cached dependencies

[Ruben Van de Velde]

That only works as long as you don't change any signatures, of course

[Damiano Testa]

If we had a switch that makes a linter flag them, then "import order" is also lake build-output order.

[Damiano Testa]

This is what I do with fixing up linters, walk in reverse order of what lake build reports. It does require having full oleans for the chatty version, though.

[Damiano Testa]

I use this script to parse the lake build output with linter warnings:

    lake build | awk -F: -v regex="warning" 'BEGIN{ OFS=":"; print "(code ." }
      # on warnings, we set ourselves up for using a targeted `code`
      ($0 ~ regex) { print "code -r -g "$2, $3; }
      # to get an idea of progress, whenever 10 files have been built, we print a comment
      /0\// { printf("# %s\n", $0) } END{ print ")" }' )

[Damiano Testa]

Here is a prototype:

import ImportGraph.Imports

namespace SortImports

open Lean

/-- The `<` partial order on modules: `importLT env mod₁ mod₂` means that `mod₂` imports `mod₁`. -/
def importLT (env : Environment) (f1 f2 : Name) : Bool :=
  (env.findRedundantImports #[f1, f2]).contains f1

/--
`sort_imports mod₁ mod₂ ... modₙ` sorts `mod₁ mod₂ ... modₙ` so that in the resulting
list a module that appears somewhere can only import modules that appear before it.

It removes repetitions in the given list.
-/
elab "sort_imports " ids:ident* : command => do
  let fs := ids.map (·.getId)
  let env ← importModules (fs.map ({module := ·})) (← getOptions)
  let rip := (Std.HashSet.ofArray fs).toArray.qsort (importLT env)
  logInfo <| .joinSep (rip.toList.map (m!"{·}")) "\n"

end SortImports

[Damiano Testa]

Using that command on the imports that Anne mentioned, I get:

/--
info: Mathlib.Algebra.Group.Equiv.Basic
Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Mathlib.Algebra.Algebra.Hom
Mathlib.Algebra.GCDMonoid.Basic
Mathlib.Algebra.MonoidAlgebra.Defs
-/
#guard_msgs in
sort_imports
  Mathlib.Algebra.Algebra.Hom
  Mathlib.Algebra.GCDMonoid.Basic
  Mathlib.Algebra.GCDMonoid.Basic
  Mathlib.Algebra.GCDMonoid.Basic
  Mathlib.Algebra.Group.Equiv.Basic
  Mathlib.Algebra.Group.Equiv.Basic
  Mathlib.Algebra.MonoidAlgebra.Defs
  Mathlib.Algebra.MonoidAlgebra.Defs
  Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

[Damiano Testa]

If this works well, then preprocessing the input modules by splitting at :, converting a filename to a module name and processing that should be completely straightforward.

[Damiano Testa]

Note that this uses that the oleans for the files that you pass are present (and I think that it would start compiling them otherwise).

[Kyle Miller]

Ruben Van de Velde said:

What I do is I make changes in vs code without saving

Another way is to make use of git stash. Sometimes I do git stash after each change, and then do a sufficient number of git stash pops at the end.

[Eric Wieser]

Don't you risk polluting your cache in between?

[Kevin Buzzard]

In my experience you can usually get away with changing a file and then reverting the changes, especially if you don't start hammering the blue "imports are out of date, click here" button on other tabs