Does Lean.Core.checkSystem expect a string or a name?

Stream: lean4

[Eric Wieser]

The function signature of docs#Lean.Core.checkSystem takes a String, but this is then coerced to a Name (by docs#Lean.Core.throwMaxHeartbeat) and then formatted back to a string, resulting in checkSystem "Foo.Bar" giving timeout at '«Foo.Bar»' in the error message.

[Joachim Breitner]

In master we removed that footgunning coercion from String to Name, maybe that has fixed this issue along the way?
https://github.com/leanprover/lean4/pull/3589

[Eric Wieser]

Ah you're right, now there's an explicit conversion here

[Eric Wieser]

But the question remains; is that conversion really supposed to happen?

[Joachim Breitner]

But probably the wrong one, if you expect to be able to pass a full module name there?

[Eric Wieser]

I'd argue that either throwMaxHeartbeat should take a String, or checkSystem should take a Name

[Joachim Breitner]

Yeah, the latter I'd assume