Fixing error message of unknown declaration on IR checking

Stream: lean4

[Shuhao Song]

Consider the following code at the current Lean nightly version on https://live.lean-lang.org/:

axiom f : Nat → Nat
set_option compiler.extract_closed false in
def a := f 1 + 1

It will report an error:

compiler IR check failed at 'a', error: unknown declaration 'f'

But we may want an error message like this:

failed to compile definition, consider marking it as 'noncomputable' because it depends on 'f', and it does not have executable code

I read the source code, and in the else block of function infer_constant of file library/compiler/ll_infer_type.cpp, when we can't find the constant in both the environment and m_new_decl_names, we will prompt the user to mark it as noncomputable. However, in the function getDecl of Lean/Compiler/IR/Checker.lean, we just prompt "unknown declaration '{c}'" when we can't find the constant in the environment, and it's may be not so informative.
Could I make a pull request for this? We could change it to "The definition depends on '{c}' but its executable code can't be found, consider marking the definition as 'noncomputable'".

[Kevin Buzzard]

There is an old lean 4 issue for this: https://github.com/leanprover/lean4/issues/1785

[Shuhao Song]

OK, thanks. I cited this issue in my PR.

[Kevin Buzzard]

Oh there is also https://github.com/leanprover/lean4/pull/4729 which seems to fix the same thing.