Codegen emits function declaration twice with different linkages

[awson]

Description

I tried to compile Lean from sources using Visual C++.

When compiling stage0 stdlib the compiler spits (among others) the following 2 error messages:

C:\G\sources2\LEAN\lean\lean4\stage0\stdlib\Lean\Meta\ExprDefEq.c(219): error C2375: 'lean_is_expr_def_eq': redefinition; different linkage
C:\G\sources2\LEAN\lean\lean4\stage0\stdlib\Lean\Meta\ExprDefEq.c(123): note: see declaration of 'lean_is_expr_def_eq'

and

C:\G\sources2\LEAN\lean\lean4\stage0\stdlib\Lean\Meta\LevelDefEq.c(53): error C2375: 'lean_is_level_def_eq': redefinition; different linkage
C:\G\sources2\LEAN\lean\lean4\stage0\stdlib\Lean\Meta\LevelDefEq.c(42): note: see declaration of 'lean_is_level_def_eq'

And indeed, lean_is_expr_def_eq is first declared as

lean_object* lean_is_expr_def_eq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);

and a bit later redeclared (in the same file) as

LEAN_EXPORT lean_object* lean_is_expr_def_eq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);

(same for lean_is_level_def_eq)

Versions

2022-05-09 GMT 05:15

[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 extC instead of !extC.

Is this OK?

[Kha]

Yes, that code assumes that any [extern] decl is truly external, i.e. defined in a different object file. However, Lean.Meta.ExprDefEq both exports lean_is_expr_def_eq and uses the previously defined @[extern 7 "lean_is_expr_def_eq"] constant isExprDefEqAux, which confuses the C emitter. I don't see a trivial solution/workaround here (and suspect that there may be other issues with compiling Lean with VC++).

[awson]

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.

[awson]

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 it's defined: with or without __declspec(dllexport).

But if it is a data declaration (not a function) clang wants it to be declared as an explicit extern, VC++ is happy regardless of this (my impression is that Lean always generates functions anyway).

[Kha]

That's good to hear. But I also just remembered this reservation about dllimport: https://github.com/leanprover/lean4/pull/670#issuecomment-920339420. stage0 might not be affected by this because no Lean code is shared across DLLs there yet.

[awson]

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 are usually made on Windows.

Btw, it's safe (and dirty) to dllimport any external data, even if this external is linked statically, not dynamically.

In the latter case we have a small performance penalty (indirect data access) and linker warning about locally defined symbol being imported (which may, perhaps, be silenced).

[awson]

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 dlls (runtime pseudo-relocs). Any extern data (not a function) is accessed through the variable stub.

[Kha]

I see, that makes sense. If you can make this work, I'm happy to review it.

[awson]

In your comment 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?

[Kha]

Yes, that sounds right