Codegen emits function declaration twice with different linkages

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

Start with the generated stage0/stdlib/Lean/Meta/ExprDefEq.c and LevelDefEq.c files, comparing the first declarations with the later LEAN_EXPORT declarations. Trace the code-generation entry point that produces these declarations and reproduce the build with Visual C++; done means the generated files compile without different-linkage redefinition errors.