Lean.Elab.admitGoal is not noisy

Stream: lean4

[Arthur Paulino]

In @Siddharth Bhat's example from the metaprogramming book I noticed that Lean.Elab.admitGoal doesn't trigger any alert that a theorem was accepted by the kernel without a proper proof. Is this intentional?

[Leonardo de Moura]

We have the following issue: https://github.com/leanprover/lean4/issues/1163
I will try to address it soon. Tactic support may provide better position information for the warning message.

[Arthur Paulino]

Glad to know it's already tracked, thanks!