Unname some unused variables

[Kha]

The following quick script takes as stdin a Lean build log and replaces reportedly unused variables with _ in the following two cases where formatting isn't too much of an issue:

• single-letter variables
• something that looks like a top-level pattern variable, in which case we pad with an appropriate number of spaces after the , (if any)

def main : IO Unit := do
  let stdin ← IO.getStdin
  while !(← stdin.isEof) do
    match (← (← IO.getStdin).getLine).trim.splitOn with
    | [loc, "warning:", "unused", "variable", var] =>
      let [file, lineNo, col, ""] := loc.splitOn ":" | throw <| IO.userError loc
      let lineNo := lineNo.toNat! - 1
      let col := col.toNat!
      let var := var.extract ⟨1⟩ (var.prev var.endPos)  -- remove ``
      let lines := (← IO.FS.readFile file).splitOn "\n" |>.toArray
      let line := lines[lineNo]
      if (line.contains '|' && !line.contains '(') || var.length == 1 then  -- then
        IO.println loc
        IO.println line
        let mut line := line.take col ++ "_" ++ "".pushn ' ' (var.length - "_".length) ++ line.drop (col + var.length)
        -- adjust trailing comma
        if var.length > 1 && (line.mkIterator.nextn (col + var.length) |>.curr) == ',' then
          line := line.mkIterator.nextn (col + 1) |>.setCurr ',' |>.nextn (var.length - 1) |>.setCurr ' ' |>.toString
        IO.println line
        let lines := lines.set! lineNo line
        IO.FS.writeFile file (String.join <| lines.toList.intersperse "\n")
    | _ => continue

It looks like the linter sometimes reports the same variable multiple times, which confuses the script, so I filtered the input through sort -u first. Then I post-processed the result using sed -i 's![_ : ![!g' to fix instance implicits. And then I did some more manual cleanups as in the commits below.

[Kha]

@larsk21 I wonder if we should exclude class signatures by default

[larsk21]

After seeing this use case, yes, probably. But the same issue occurs with structure and inductive signatures as well, doesn't it?

[larsk21]

see #1191

[Kha]

But the same issue occurs with structure and inductive signatures as well, doesn't it?

That's a good question. It could be argued that it is likelier for classes where parameters that are exclusively for directing typeclass resolution sounds quite reasonable, whereas "faux-typed" structures such as the single KeyedDeclsAttribute.Def from this PR seem more edge case (and often may as well be defs, in which case we can't exclude them anyway).

[Kha]

@leodemoura

[Kha]

Apparently not, the change breaks run/diamond{3,4}.lean

[leodemoura]

Thanks for catching this. I pushed a fix for this.

      let r := if e.isAppOfArity ``id 2 then e.appArg! else e
      return some (← reduceProjs (← instantiateMVars r) expandedStructNames)

[Kha]

@leodemoura correct?

[leodemoura]

Thanks for catching this. I pushed a fix for it.

[gebner]

I really dislike that this disables the (s := ...) syntax to specify implicit arguments (for no good reason). (Not that s is a great name, inst or something would certainly be better.)

[Kha]

Ugh, I dislike the counter-intuitive implicit-as-inst-implicit pattern in general. Not sure what would be a good general solution here.

[gebner]

implicit-as-inst-implicit pattern

Do you mean {_ : Decidable p} instead of [Decidable p]? (Not sure I understood you correctly. I would have named it the way around: inst-implicit-as-implicit pattern.)

[Kha]

Yes, I was thinking of it the other way around - an implicit parameter that becomes an inst-implicit argument in an application

[Kha]

I just noticed that the {_ : style is prevalent in e.g. Std.Data.PersistentHashMap, so this really is a pre-existing style issue that should be discussed at a larger scope.

[Kha]

Just a quick idea, but a "nicer" way could be to allow selecting parameters by type as in eq_false_of_decide (‹Decidable p› := ...). One slight downside would be a larger parser overlap.

[Kha]

@gebner Thanks, I definitely didn't look at every line in detail!

[Kha]

An unexpected consequence from renaming a pattern variable, but I can't say I've every done such a refold myself so far.