Windows: explicitly export Lean functions only #670

Kha · 2021-09-15T16:29:32Z

Saves us some more symbols by not exporting our C++ functions and avoids the --export-all-symbols flag not supported by Zig

Kha · 2021-09-15T20:07:09Z

ld.exe: ../build/stage1/lib/temp/Leanpkg.o:Leanpkg.c:(.text+0xb59c): undefined reference to `lean_dec_ref_cold'

Ah-ha, that's how we knows it's working! So we should mark runtime functions with dllexport as well. Unfortunately, it gets worse. According to https://web.archive.org/web/20140808231508/http://blogs.msdn.com/b/russellk/archive/2005/03/20/399465.aspx, we should mark functions imported from DLLs with __declspec(dllimport) for performance and must do so for imported data, e.g. 0-ary defs. So when emitting C code, we would need to know which imports are/will be compiled into separate DLLs and which won't 😱 . That would be a pretty significant change, but note that it is mandatory if we want back MSVC support (/cc @lovettchris), and perhaps to support Zig's future custom linker in case they don't want to implement the MinGW semantics.

lovettchris · 2021-09-15T21:24:46Z

I'd love to get back MSVC support :-) I played with it but kept running into bash shell invocations and custom make files... (leanc.in, stdlib.make.in, etc). but I'm happy to test what you are trying to do with this PR if you don't have msys handy.

lovettchris

couple questions...

lovettchris · 2021-09-15T21:25:09Z

src/shell/lean.cpp

@@ -644,7 +644,7 @@ int main(int argc, char ** argv) {
        }

        if (c_output && ok) {
-            std::ofstream out(*c_output);
+            std::ofstream out(*c_output, std::ios_base::binary);


what is this fixing?

See commit message, we should produce the same stage0/ on every platform. EmitC already uses \n explicitly, but the ofstream mangled it into \r\n.

lovettchris · 2021-09-15T21:25:50Z

stage0/src/Lean/Data/Rat.lean

@@ -0,0 +1,125 @@
+/-


this appears to be a new file about rational numbers, what does that have to do with this PR ?

Please ignore all changes in stage0/ :) . I couldn't even find your comment at first in order to respond because they are all collapsed by default.

lovettchris · 2021-09-15T21:26:50Z

stage0/stdlib/Lean/Compiler/IR/EmitC.c

@@ -585,6 +585,7 @@ lean_object* l_Lean_IR_EmitC_emitDeclAux___lambda__1(lean_object*, lean_object*,
 static lean_object* l_Nat_forM_loop___at_Lean_IR_EmitC_emitDeclAux___spec__1___closed__2;
 lean_object* l_Nat_forM_loop___at_Lean_IR_EmitC_emitDeclAux___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_IR_EmitC_toCType(lean_object*);
+static lean_object* l_Lean_IR_EmitC_emitDeclAux___closed__1;


I'd love to move stage0 to a git submodule so we can prune it's history from time to time... hate seeing this code generated cruft mingled with real changes like this...

Leo and I talked about doing this, but it would introduce more coordination headaches, especially around PRs. We'll gather some first experience with a Lake submodule (which shouldn't change as much) soon, then we can reevaluate this.

Kha · 2021-09-16T07:44:05Z

I'd love to get back MSVC support :-) I played with it but kept running into bash shell invocations and custom make files... (leanc.in, stdlib.make.in, etc). but I'm happy to test what you are trying to do with this PR if you don't have msys handy.

Oh right, the Makefile... the only way we could get rid of it that I can see is to bootstrap with Lake, which I don't see happening in the near future.

Kha · 2021-09-16T07:44:47Z

Same goes for this PR, it might be easier to add support for --export-all to Zig than to land this one...

lovettchris · 2021-09-16T18:54:56Z

I'd love to get back MSVC support :-) I played with it but kept running into bash shell invocations and custom make files... (leanc.in, stdlib.make.in, etc). but I'm happy to test what you are trying to do with this PR if you don't have msys handy.

Oh right, the Makefile... the only way we could get rid of it that I can see is to bootstrap with Lake, which I don't see happening in the near future.

On the ELL compiler project we have a build process that produces new cmake files. You just have configure_file(foo.cmake.in) instead off "foo.make.in") Any reason we could not do that? Instead of using Make files. Just go one step meta, generate a cmake instead. On linux that will generate Make files and on MSVC that will generate msbuild files.

Kha · 2021-09-16T19:07:26Z

When would this file be regenerated? The build graph potentially changes any time a .lean file is touched, we probably don't want to re-run cmake that often?

Kha · 2021-09-17T11:46:09Z

Nice, looks like I got all relevant symbols now. In my previous message I forgot that dllexport and dllimport are somewhat orthogonal, so if we add only the former, we still reap all the benefits mentioned in the original message. While dllimport would still be necessary for MVSC support, this is far from the only hurdle for that as mentioned.

@leodemoura Are you happy with these changes?

src/runtime/object.h

leodemoura · 2021-09-17T15:01:28Z

@leodemoura Are you happy with these changes?

Yeah, I am happy with the changes. I had just a small question (above).

Kha · 2021-09-17T15:02:41Z

I found out that clang doesn't like this version, will move the annotations from .cpp to .h soon

Kha

Ok, final revision hopefully. Clang's requirement that the (first) declaration needs to be annotated means that we now have some annotations in headers and some (when there are no header decls) in .cpps. But it shouldn't matter when applying the natural "implement new runtime function by copying existing function from same file" approach.

Kha · 2021-09-18T11:49:51Z

src/Lean/Compiler/IR/EmitC.lean


 def emitExternDeclAux (decl : Decl) (cNameStr : String) : M Unit := do
  let cName := Name.mkSimple cNameStr
  let env ← getEnv
  let extC := isExternC env decl.name
-  emitFnDeclAux decl cNameStr (!extC)
+  emitFnDeclAux decl cNameStr extC


@leodemoura It makes more sense this way around, right? We want to annotate [extern "..."] constants with extern, but not [extern inline ...] ones. It doesn't look like this was used before, but now that I extended the parameter to functions, it is.

It was calling into WSL bash on my machine...

… lean.h

mathlib3 SHA: 39af7d3bf61a98e928812dbc3e16f4ea8b795ca3 Porting notes: 1. Some lemmas were transferred from `Data.Int.Cast.Defs` in order to match mathlib3 (I accidentally put them in the wrong place when I had ported that file because those lemmas were already present in mathlib4.) 2. The lemmas just mentioned have retained their `simp` attribute for the reason Gabriel mentioned on that PR (leanprover#641), even though that attribute isn't present on the mathlib3 version. 3. The `bit0` and `bit1` lemmas have been marked as deprecated. 4. There were many dubious translation errors, I believe primarily because of the difference in the way coercions are handled, so I have `#align`ed all of these with `ₓ`. I believe this is the correct thing to do, but confirmation would be nice.

lovettchris suggested changes Sep 15, 2021

View reviewed changes

Kha force-pushed the dllexport branch 2 times, most recently from 376171a to 8c547ed Compare September 16, 2021 16:12

Kha force-pushed the dllexport branch 2 times, most recently from 224c556 to 2f778e1 Compare September 17, 2021 09:35

Kha marked this pull request as draft September 17, 2021 14:38

leodemoura reviewed Sep 17, 2021

View reviewed changes

src/runtime/object.h Outdated Show resolved Hide resolved

Kha force-pushed the dllexport branch 5 times, most recently from dde83c1 to 655525f Compare September 18, 2021 10:30

Kha commented Sep 18, 2021

View reviewed changes

Kha force-pushed the dllexport branch from 78679a2 to 655525f Compare September 18, 2021 12:24

Kha marked this pull request as ready for review September 18, 2021 12:24

Kha added 6 commits September 20, 2021 11:20

feat: Windows: explicitly export Lean functions only

8949289

chore: update stage0

1367027

chore: remove --export-all

7439afd

chore: avoid cmake -E env

f2247e8

It was calling into WSL bash on my machine...

fix: write .c output file in binary mode for reproducibility

7d10876

fix: annotate lean.h functions with LEAN_SHARED

2d866b8

Kha added 3 commits September 20, 2021 11:28

fix: dllexport functions not already annotated in header

87faceb

fix: include exported declarations in defining file

7711206

chore: silence clang warning when exporting Lean function declared in…

f5c8141

… lean.h

Kha force-pushed the dllexport branch from d0914d2 to f5c8141 Compare September 20, 2021 09:28

Kha merged commit 0a6778d into leanprover:master Sep 20, 2021

Kha mentioned this pull request Sep 22, 2021

feat: hide non-exported symbols on Unix #684

Merged

Kha mentioned this pull request May 18, 2022

Codegen emits function declaration twice with different linkages #1148

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Windows: explicitly export Lean functions only #670

Windows: explicitly export Lean functions only #670

Kha commented Sep 15, 2021

Kha commented Sep 15, 2021

lovettchris commented Sep 15, 2021

lovettchris left a comment

lovettchris Sep 15, 2021

Kha Sep 16, 2021

lovettchris Sep 15, 2021

Kha Sep 16, 2021

lovettchris Sep 15, 2021

Kha Sep 16, 2021

Kha commented Sep 16, 2021

Kha commented Sep 16, 2021

lovettchris commented Sep 16, 2021

Kha commented Sep 16, 2021 •

edited

Loading

Kha commented Sep 17, 2021 •

edited

Loading

leodemoura commented Sep 17, 2021

Kha commented Sep 17, 2021

Kha left a comment

Kha Sep 18, 2021

Windows: explicitly export Lean functions only #670

Windows: explicitly export Lean functions only #670

Conversation

Kha commented Sep 15, 2021

Kha commented Sep 15, 2021

lovettchris commented Sep 15, 2021

lovettchris left a comment

Choose a reason for hiding this comment

lovettchris Sep 15, 2021

Choose a reason for hiding this comment

Kha Sep 16, 2021

Choose a reason for hiding this comment

lovettchris Sep 15, 2021

Choose a reason for hiding this comment

Kha Sep 16, 2021

Choose a reason for hiding this comment

lovettchris Sep 15, 2021

Choose a reason for hiding this comment

Kha Sep 16, 2021

Choose a reason for hiding this comment

Kha commented Sep 16, 2021

Kha commented Sep 16, 2021

lovettchris commented Sep 16, 2021

Kha commented Sep 16, 2021 • edited Loading

Kha commented Sep 17, 2021 • edited Loading

leodemoura commented Sep 17, 2021

Kha commented Sep 17, 2021

Kha left a comment

Choose a reason for hiding this comment

Kha Sep 18, 2021

Choose a reason for hiding this comment

Kha commented Sep 16, 2021 •

edited

Loading

Kha commented Sep 17, 2021 •

edited

Loading