awson

I've looked into (perhaps) relevant commits and noticed the following: the commit introducing `LEAN_EXPORT` looks as if `isExternal` is now used instead of `addExternForConsts`, [but `emitFnDeclAux` is now called with...

Ah, understood. Yes, VC++ requires other fixes, but they are more or less straightforward. I can build stage0 lean successfully with VC++ if grepping out these 2 offending lines.

Hmm, I've made a quick experiment and found that `__declspec(dllexport)` is absolutely harmless when we declare an external. It compiles and links with the truly external thing, regardless of how...

Yeah, and because of this I've made something like ``` #define LEAN_IMPORT __declspec(dllimport) ... #if defined LEAN_EXPORTING #define LEAN_SHARED LEAN_EXPORT #else #define LEAN_SHARED LEAN_IMPORT #endif ``` This is how things...

> In the latter case we have a small performance penalty (indirect data access) And `mingw` target **always does this**, and this is why it can seamlessly import data from...

In [your comment](https://github.com/leanprover/lean4/pull/670#issuecomment-920339420) you write: > *must* do so for imported data, e.g. 0-ary defs Are these cases covered exactly by [this ps.isEmpty and isExternal branch of `emitFnDeclAux`](https://github.com/leanprover/lean4/blob/d13fac6f458bd1efd772424066f2a85f8c8ba32a/src/Lean/Compiler/IR/EmitC.lean#L98)?

Is is possible to increase the priority of this task? Linking to `msvcrt` is becoming more and more problematic. Now it's virtually impossible to interop with C code built with...

> The only problem is that ucrt32 doesn't exist, so 32-bit julia is stuck using msvcrt. Strictly speaking, ucrt32 absolutely exists, but you are right in the sense that there...

> My two cents as somebody who just searched this in the issues page: a plugin api done via DLLs is not gonna end well, internal functions are (and should)...

> Far Manager is a clone of a file manager from the 1990s, so its not exactly a great example to point out when saying this is a good idea....