Could not find native implementation of external declaration

Stream: mathlib4

[Antoine Chambert-Loir]

In the compilation of #35830, we get the following error message:

Error: error: Mathlib/Data/Nat/Choose/Plurinomial.lean:132:0: Could not find native implementation of external declaration 'Multiset.filter._redArg' (symbols 'lp_mathlib_Multiset_filter___redArg___boxed' or 'lp_mathlib_Multiset_filter___redArg').

For declarations from `Init`, `Std`, or `Lean`, you need to set `supportInterpreter := true` in the relevant `lean_exe` statement in your `lakefile.lean`.

error: Lean exited with code 1

which I don't understand and do not know how to address.
Thank you in advance for any help!

[Anne Baanen]

Does it help to mark things as noncomputable?

[Antoine Chambert-Loir]

I can try, but it should be computable because it is. Moreover it compiles at home, so that's really something involving CI.

[Anne Baanen]

Does lake build work for you?

I expect this is something like: the induction tactic makes a term that doesn't get picked up correctly by the compiler, compared to hand-written induction. And then when we want to link everything together in one big Mathlib library, the expected output of the compiler is missing some bits.

[Anne Baanen]

I would say this is reportable as a Lean bug: at the very least the error message should be clearer.

[Robin Arnez]

Yeah, you'd need to meta import to have the code available at build time, i.e.

meta import Mathlib.Data.Nat.Choose.Multinomial
public import Mathlib.Data.Nat.Choose.Multinomial
public import Mathlib.Data.List.ToFinsupp

but presumably you don't want that #eval to stick around so you should be able to instead just remove it. I agree though that there should be a better error message that indicates this has to do with the meta separation.

[Antoine Chambert-Loir]

Removing the #evalline (that was just an example) was enough, thank you!

[Antoine Chambert-Loir]

Your messages suggest that during CI or when one orders lake build, the compiler is in a different state than when it compiles the given open file. Is that somewhat true?

[Robin Arnez]

Yeah, I think the language server loads compiled IR for more functions than the build does (to reduce build dependencies). In particular, #eval in the language server is (almost) unconstrainted but during build it is limited to meta imported functions or actual meta functions.