Skip to content

Bundle clang+lld+libc++ for Windows#736

Closed
Kha wants to merge 30 commits intoleanprover:masterfrom
Kha:bundle-llvm-windows
Closed

Bundle clang+lld+libc++ for Windows#736
Kha wants to merge 30 commits intoleanprover:masterfrom
Kha:bundle-llvm-windows

Conversation

@Kha
Copy link
Member

@Kha Kha commented Oct 22, 2021

Building on top of #733. There are no official LLVM tarball releases for Windows and we need the mingw headers anyway, so we simply copy everything from mingw.

@Kha Kha force-pushed the bundle-llvm-windows branch from dea52e1 to 5ce91d3 Compare October 22, 2021 12:37
@Kha
Copy link
Member Author

Kha commented Oct 22, 2021

The size increase is more modest on Windows than on Linux: 110MB -> 150MB. This is presumably due to clang and lld sharing some of their code via libLLVM.dll, which is pretty much a necessity on Windows since you can't e.g. symlink lld-link to lld.

@Kha
Copy link
Member Author

Kha commented Oct 22, 2021

Uncompressed breakdown from CI:

lean-4.0.0-windows
    ├── [190M]  bin
    │   ├── [150K]  clang.exe
    │   ├── [1.7M]  lake.exe
    │   ├── [4.9M]  ld.lld.exe
    │   ├── [ 84K]  lean.exe
    │   ├── [107K]  leanc.exe
    │   ├── [ 860]  leanmake
    │   ├── [284K]  leanpkg.exe
    │   ├── [1.2M]  libc++.dll
    │   ├── [ 45M]  libclang-cpp.dll
    │   ├── [ 34K]  libffi-7.dll
    │   ├── [572K]  libgmp-10.dll
    │   ├── [1022K]  libiconv-2.dll
    │   ├── [ 44M]  libleanshared.dll
    │   ├── [ 90M]  libLLVM.dll
    │   ├── [162K]  liblzma-5.dll
    │   ├── [ 36K]  libunwind.dll
    │   ├── [1.5M]  libxml2-2.dll
    │   └── [104K]  zlib1.dll
    ├── [119K]  include
    │   ├── [ 40K]  clang
    │   │   ├── [ 857]  __stddef_max_align_t.h
    │   │   ├── [2.8K]  limits.h
    │   │   ├── [ 583]  stdalign.h
    │   │   ├── [1.1K]  stdarg.h
    │   │   ├── [7.1K]  stdatomic.h
    │   │   ├── [ 897]  stdbool.h
    │   │   ├── [3.5K]  stddef.h
    │   │   ├── [ 22K]  stdint.h
    │   │   ├── [ 510]  stdnoreturn.h
    │   │   └── [ 218]  windows.h
    │   └── [ 80K]  lean
    │       ├── [ 271]  config.h
    │       ├── [ 79K]  lean.h
    │       ├── [ 575]  lean_gmp.h
    │       └── [ 399]  version.h
    ├── [340M]  lib
    │   ├── [136K]  clang
    │   │   └── [136K]  12.0.1
    │   │       └── [136K]  lib
    │   │           └── [136K]  windows
    │   │               └── [136K]  libclang_rt.builtins-x86_64.a
    │   ├── [ 24K]  crt2.o
    │   ├── [ 396]  crtbegin.o
    │   ├── [ 396]  crtend.o
    │   ├── [ 17K]  dllcrt2.o
    │   ├── [333M]  lean
    │   │   ├── [ 24M]  Init ...
    │   │   ├── [7.4K]  Init.olean
    │   │   ├── [7.7M]  Lake ...
    │   │   ├── [8.9K]  Lake.olean
    │   │   ├── [220M]  Lean ...
    │   │   ├── [9.0K]  Lean.olean
    │   │   ├── [1.4M]  Leanpkg ...
    │   │   ├── [492K]  Leanpkg.olean
    │   │   ├── [3.2M]  libInit.a
    │   │   ├── [ 50M]  libLean.a
    │   │   ├── [4.4M]  libleancpp.a
    │   │   ├── [516K]  libleanrt.a
    │   │   ├── [ 12M]  libleanshared.dll.a
    │   │   ├── [990K]  libStd.a
    │   │   ├── [3.4M]  src ...
    │   ├── [146K]  libadvapi32.a
    │   ├── [ 12K]  libbcrypt.a
    │   ├── [1.9M]  libc++.a
    │   ├── [679K]  libc++.dll.a
    │   ├── [930K]  libgmp.a
    │   ├── [ 96K]  libgmp.dll.a
    │   ├── [435K]  libkernel32.a
    │   ├── [ 620]  libm.a
    │   ├── [108K]  libmingw32.a
    │   ├── [1.8M]  libmingwex.a
    │   ├── [ 628]  libmoldname.a
    │   ├── [540K]  libmsvcrt.a
    │   ├── [ 72K]  libpthread.a
    │   ├── [ 25K]  libpthread.dll.a
    │   ├── [ 69K]  libshell32.a
    │   ├── [ 47K]  libunwind.a
    │   ├── [6.2K]  libunwind.dll.a
    │   ├── [151K]  libuser32.a
    │   └── [   0]  windows
    └── [2.9K]  share
        └── [2.9K]  lean
            └── [2.9K]  lean.mk

 531M used in 142 directories, 1095 files

@Kha Kha force-pushed the bundle-llvm-windows branch from 4b115e7 to 625066c Compare October 22, 2021 14:20
@tydeu
Copy link
Member

tydeu commented Oct 23, 2021

@Kha why does the Windows distro bundle libLLVM but the Linux distro does not (at least per the listing in #733? That seems like something that should be consistent across platforms.

@Kha
Copy link
Member Author

Kha commented Oct 23, 2021

@tydeu I reported my guess on that above. But other than potential file size savings it really shouldn't matter. As I said in the Linux thread, this all should be regarded as implementation details.

@Kha Kha force-pushed the bundle-llvm-windows branch from 625066c to bbe3697 Compare October 29, 2021 09:10
@Kha Kha force-pushed the bundle-llvm-windows branch 2 times, most recently from cf6d832 to ed2ca9a Compare November 9, 2021 13:02
@Kha Kha force-pushed the bundle-llvm-windows branch from ed2ca9a to 3f80452 Compare November 9, 2021 16:42
@Kha Kha force-pushed the bundle-llvm-windows branch 5 times, most recently from b6dd5ea to 4dd67cb Compare November 15, 2021 10:22
@Kha Kha force-pushed the bundle-llvm-windows branch from 4dd67cb to bc2e2bd Compare November 15, 2021 12:13
@Kha Kha mentioned this pull request Nov 15, 2021
@Kha
Copy link
Member Author

Kha commented Nov 15, 2021

Closing in favor of #795

@Kha Kha closed this Nov 15, 2021
ChrisHughes24 pushed a commit to ChrisHughes24/lean4 that referenced this pull request Dec 2, 2022
Mathlib SHA: 71ca477041bcd6d7c745fe555dc49735c12944b7

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
Co-authored-by: Scott Morrison <scott@tqft.net>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants