Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Bundle LLVM on all platforms #795

Merged
merged 39 commits into from
Nov 18, 2021
Merged

Bundle LLVM on all platforms #795

merged 39 commits into from
Nov 18, 2021

Conversation

Kha
Copy link
Member

@Kha Kha commented Nov 15, 2021

Building on top of #733 and #736, add support for macOS to complete the trio.

├── [9.2K]  LICENSE
├── [7.8M]  bin
│   ├── [166K]  clang
│   ├── [1.5M]  lake
│   ├── [5.9M]  ld64.lld
│   ├── [ 16K]  lean
│   ├── [ 43K]  leanc
│   ├── [ 839]  leanmake
│   └── [218K]  leanpkg
├── [118K]  include
│   ├── [ 40K]  clang
│   │   ├── [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
│   └── [ 78K]  lean
│       ├── [ 259]  config.h
│       ├── [ 77K]  lean.h
│       ├── [ 551]  lean_gmp.h
│       └── [ 387]  version.h
├── [467M]  lib
│   ├── [762K]  clang
│   │       └── [762K]  lib
│   │           └── [762K]  darwin
│   │               └── [761K]  libclang_rt.osx.a
│   ├── [355M]  lean
│   │   ├── [ 24M]  Init
│   │   ├── [8.3M]  Lake
│   │   ├── [220M]  Lean
│   │   ├── [1.4M]  Leanpkg
│   │   ├── [5.4M]  Std
│   │   ├── [3.2M]  libInit.a
│   │   ├── [ 46M]  libLean.a
│   │   ├── [865K]  libStd.a
│   │   ├── [3.6M]  libleancpp.a
│   │   ├── [447K]  libleanrt.a
│   │   ├── [ 39M]  libleanshared.dylib
│   │   └── [3.4M]  src
│   │       ├── [488K]  Init
│   │       ├── [2.6M]  Lean
│   │       ├── [ 15K]  Leanpkg
│   │       ├── [ 82K]  Std
│   │       ├── [  64]  bin
│   │       ├── [ 160]  cmake
│   │       ├── [ 160]  include
│   │       │   └── [  64]  lean
│   │       ├── [  64]  initialize
│   │       ├── [  64]  kernel
│   │       ├── [136K]  lake
│   │       │   ├── [126K]  Lake
│   │       ├── [ 256]  library
│   │       │   ├── [  64]  compiler
│   │       │   └── [  64]  constructions
│   │       ├── [  64]  runtime
│   │       ├── [  64]  shell
│   │       └── [  64]  util
│   ├── [ 55M]  libLLVM.dylib
│   ├── [1.5M]  libc
│   │   ├── [252K]  libSystem.tbd
│   │   ├── [832K]  libc++.dylib
│   │   ├── [310K]  libc++abi.dylib
│   │   └── [ 94K]  libunwind.dylib
│   ├── [ 54M]  libclang-cpp.dylib
│   └── [831K]  libgmp.a
└── [3.0K]  share
    └── [2.9K]  lean
        └── [2.8K]  lean.mk
 475M used in 124 directories, 1050 files

LICENSE Outdated Show resolved Hide resolved
@Kha
Copy link
Member Author

Kha commented Nov 16, 2021

Note, this currently always statically links GMP with the expectation that this dependency will be dropped soon

@Kha Kha merged commit fee052c into leanprover:master Nov 18, 2021
ChrisHughes24 pushed a commit to ChrisHughes24/lean4 that referenced this pull request Dec 2, 2022
mathlib SHA: 4e42a9d0a79d151ee359c270e498b1a00cc6fa4e

Porting Notes:
1. Basically no errors. Only needed to fix some lambdas having implicit arguments.
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