Mac Malone

Revisiting this, I have since discovered that `@[default_instance]` can be used to get the best of both worlds: ```lean namespace Issue3128 #check show IO Unit from throw "hi" -- fails...

@FrederickPu You cannot define an `@[extern[` definition and then `#eval` it in the same environment. The `@[extern]` definition would need to be in a separate module that is compiled, loaded...

@FrederickPu > Also even when I put it into a compiled module it still fails The imported module itself has to be compiled into the dynlib, not just the FFI...

@semorrison > I'm a bit worried about adding a Lake import after seeing the troubles described at [leanprover-community/import-graph#20](https://github.com/leanprover-community/import-graph/issues/20) The problem there just appears to be that a shared library for...

FYI, a Lake shared library is now part of the standard Lean 4 release (since https://github.com/leanprover/lean4/pull/5143, which is in `v4.13.0`),

@digama0 Yes, this was intentionally designed this way. It is not necessarily the case that the module with a bad import is the problem, it can sometimes be its parents....

@kmill > Something I'm considering is also having `inductive` register types as being structures in the elaborator when it makes sense to do so, and use mkProjections. If this feature...

I think the best solution here is to eagerly print the log lines for dependency resolution.

@utensil > And this would not be noisy as long as such print is erased like the building progress bar, or erased and updated to the final print for the...

@kim-em I think the new version is a slightly different issue with the same effect. The previous issue did not print any log lines at all until everything was cloned....