Unused variable linter

Stream: mathlib4

[Gareth Ma]

Hi, I think I found a bug. Take a look at the following code:

import Mathlib.Analysis.Asymptotics.Asymptotics
import Mathlib.Data.Finset.Basic
import Mathlib.Data.Nat.Interval
import Mathlib.Data.Nat.Prime
import Mathlib.NumberTheory.ArithmeticFunction

open Nat Finset BigOperators ArithmeticFunction Real Asymptotics Filter

/- primes in Ico -/
def prime_Ico (a b : ℕ) := (Ico a b).filter Nat.Prime

/- Primorial of primes < z -/
def Pr (z : ℕ) := ∏ p in prime_Ico 1 z, p

theorem card_prod_primes (s : Finset ℕ) (hs : ∀ p ∈ s, p.Prime) :
    2 ^ s.card = σ 0 (∏ p in s, p) := by
  sorry

example : (fun (z : ℕ) ↦ ∑ d in (Pr z).divisors, (1 : ℝ)) =O[atTop] (fun (z : ℕ) ↦ (2 : ℝ) ^ z) := by
  rw [IsBigO]
  use 1
  rw [IsBigOWith]
  apply eventually_of_forall
  intro x
  rw [sum_const, one_mul, norm_eq_abs, norm_eq_abs, nsmul_one, abs_of_nonneg, abs_of_nonneg,
      ←sigma_zero_apply, Pr, ←card_prod_primes]
  · push_cast
    gcongr
    · linarith
    · rw [prime_Ico]
      apply (card_filter_le _ _).trans
      rw [card_Ico]
      apply sub_le
  · intro p hp
    exact (mem_filter.mp hp).right
  · exact pow_nonneg zero_le_two _
  · exact cast_nonneg (card _)

(The proof is necessary for the bug to appear.) On line 19 with example : ..., there is a linter warning

▶ 19:28-19:29: warning:
unused variable `d` [linter.unusedVariables]

However, if you replace d with _, Lean complains:

elaboration function for 'BigOperators.bigsumin' has not been implemented
  ∑ _ in (Pr z).divisors, (1 : ℝ)

[Gareth Ma]

Actually, replacing d with __ works i.e. gets rid of the error + compiles. Is that intended?

[Yakov Pechersky]

Doesn't solve your discovered bug of the elaboration function, but the unused var linter iirc ignores vars with leading underscores

[Gareth Ma]

Oh, that's interesting, thanks :)

[Kyle Miller]

_ is classified as a hole instead of a variable, and it's an oversight that summation notation cannot handle holes. I'm hoping to have this fixed soon-ish incidental to some other work on scoped notations like this.

[Gareth Ma]

I see, the fix will be appreciated since it works for e.g. fun _ => 1 :)