Panic from making a name with an asterisk

Stream: lean4

[Michael Rothgang]

I just found the following panic, when trying to make a test-case for a mathlib linter I'm working on.
This causes a panic on the assertion failure, with an error mentioning (Inhabited.default for IO.Error).

import Mathlib.Tactic.Linter.TextBased

open Lean.Linter Mathlib.Linter.TextBased

def testModulesForbiddenWindows : IO Unit := do
  -- Explicitly enable the linter, although it is enabled by default.
  let opts : LinterOptions := {
    toOptions := linter.modulesUpperCamelCase.set {} true
    linterSets := {}
  }
  assert!((← modulesForbiddenWindows opts #[`Mathlib.Foo ++ "Foo*".toName]) == 1)

#eval testModulesForbiddenWindows -- panic

Changing the assertion to assert!((← modulesForbiddenWindows opts #[Mathlib.Foo.«Foo*»]) == 1)` works --- so this is arguably a user error. I would expect a better error message, though!

[Michael Rothgang]

(deleted)

[Michael Rothgang]

(deleted)

[Jovan Gerbscheid]

I think the panic just comes from the assert!, so maybe use something other than assert!

[Robin Arnez]

Well, assert! is non-monadic, so it will return default : IO Unit on failure

[Jovan Gerbscheid]

To be more precise, assert! throws a panic! message and then returns default : IO Unit