min_import bug?

Stream: CSLib

[Sorrachai Yingchareonthawornchai]

#min_imports in the following code in https://github.com/leanprover/cslib/pull/165

gives a suggestion of

import Cslib.Algorithms.Lean.TimeM
import Mathlib.Data.Nat.Cast.Order.Ring
import Mathlib.Data.Nat.Lattice
import Mathlib.Data.Nat.Log

However, it misses this tactic.

import Mathlib.Tactic.Bound

Does anyone know a way to get around this?

[Chris Henson]

#min_imports and shake are not aware of when an import is required for tactics. You can add an entry to the ignore key in scripts/noshake.json to add this as an exception.