From eca7678a448bfe1b35474d5abf55e49dd86764f7 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 11 Oct 2021 18:03:45 +0200 Subject: [PATCH 01/27] refactor: avoid non-compiler headers in `lean.h` --- src/include/lean/lean.h | 27 +++++++++++++++++++-------- src/runtime/compact.cpp | 1 + src/runtime/object.cpp | 4 ++++ src/runtime/sharecommon.cpp | 1 + 4 files changed, 25 insertions(+), 8 deletions(-) diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h index a1212c8dad33..ac281f7b8b5e 100644 --- a/src/include/lean/lean.h +++ b/src/include/lean/lean.h @@ -5,18 +5,14 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include +#include #include #include -#include -#include #include -#if !defined(__APPLE__) -#include -#endif #ifdef __cplusplus #include +#include #define _Atomic(t) std::atomic #define LEAN_USING_STD using namespace std; /* NOLINT */ extern "C" { @@ -25,6 +21,13 @@ extern "C" { #endif #include +#ifdef NDEBUG +#define assert(expr) +#else +// TODO +#define assert(expr) +#endif + #define LEAN_CLOSURE_MAX_ARGS 16 #define LEAN_OBJECT_SIZE_DELTA 8 #define LEAN_MAX_SMALL_OBJECT_SIZE 4096 @@ -310,6 +313,10 @@ LEAN_SHARED void lean_free_small(void * p); LEAN_SHARED unsigned lean_small_mem_size(void * p); LEAN_SHARED void lean_inc_heartbeat(); +#ifndef __cplusplus +void * malloc(size_t); // avoid including big `stdlib.h` +#endif + static inline lean_object * lean_alloc_small_object(unsigned sz) { #ifdef LEAN_SMALL_ALLOCATOR sz = lean_align(sz, LEAN_OBJECT_SIZE_DELTA); @@ -358,6 +365,10 @@ static inline unsigned lean_small_object_size(lean_object * o) { #endif } +#ifndef __cplusplus +void free(void *); // avoid including big `stdlib.h` +#endif + static inline void lean_free_small_object(lean_object * o) { #ifdef LEAN_SMALL_ALLOCATOR lean_free_small(o); @@ -1008,9 +1019,9 @@ static inline uint8_t lean_string_utf8_at_end(b_lean_obj_arg s, b_lean_obj_arg i } LEAN_SHARED lean_obj_res lean_string_utf8_extract(b_lean_obj_arg s, b_lean_obj_arg b, b_lean_obj_arg e); static inline lean_obj_res lean_string_utf8_byte_size(b_lean_obj_arg s) { return lean_box(lean_string_size(s) - 1); } +LEAN_SHARED bool lean_string_eq_cold(b_lean_obj_arg s1, b_lean_obj_arg s2); static inline bool lean_string_eq(b_lean_obj_arg s1, b_lean_obj_arg s2) { - return s1 == s2 || - (lean_string_size(s1) == lean_string_size(s2) && memcmp(lean_string_cstr(s1), lean_string_cstr(s2), lean_string_size(s1)) == 0); + return s1 == s2 || (lean_string_size(s1) == lean_string_size(s2) && lean_string_eq_cold(s1, s2)); } static inline bool lean_string_ne(b_lean_obj_arg s1, b_lean_obj_arg s2) { return !lean_string_eq(s1, s2); } LEAN_SHARED bool lean_string_lt(b_lean_obj_arg s1, b_lean_obj_arg s2); diff --git a/src/runtime/compact.cpp b/src/runtime/compact.cpp index c3f0b9a7b3f8..5c32be133fe5 100644 --- a/src/runtime/compact.cpp +++ b/src/runtime/compact.cpp @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include #include #include +#include #include #include "runtime/hash.h" #include "runtime/compact.h" diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp index 7ad5e330f9a7..e2829175ee90 100644 --- a/src/runtime/object.cpp +++ b/src/runtime/object.cpp @@ -1649,6 +1649,10 @@ extern "C" LEAN_EXPORT object * lean_string_append(object * s1, object * s2) { return r; } +extern "C" bool lean_string_eq_cold(b_lean_obj_arg s1, b_lean_obj_arg s2) { + return std::memcmp(lean_string_cstr(s1), lean_string_cstr(s2), lean_string_size(s1)) == 0; +} + bool string_eq(object * s1, char const * s2) { if (lean_string_size(s1) != strlen(s2) + 1) return false; diff --git a/src/runtime/sharecommon.cpp b/src/runtime/sharecommon.cpp index eff5ac952cb1..5ec8aefef6f5 100644 --- a/src/runtime/sharecommon.cpp +++ b/src/runtime/sharecommon.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include +#include #include "runtime/object.h" #include "runtime/hash.h" From 1e179368942331f855910383eab083387b38df65 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 13 Oct 2021 15:18:04 +0200 Subject: [PATCH 02/27] fix: libleanshared.so needs rpath too --- src/CMakeLists.txt | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 12a5a5b6cd9e..0763b479dab2 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -294,11 +294,12 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Linux") endif() set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fPIC -ftls-model=initial-exec") set(LEANC_EXTRA_FLAGS "${LEANC_EXTRA_FLAGS} -fPIC") + set(LEANSHARED_LINKER_FLAGS "${LEANSHARED_LINKER_FLAGS} -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN") set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -Wl,-rpath=\\\$ORIGIN/../lib:\\\$ORIGIN/../lib/lean") elseif(${CMAKE_SYSTEM_NAME} MATCHES "Darwin") set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -ftls-model=initial-exec") - set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -Wl,-rpath,@executable_path/../lib -Wl,-rpath,@executable_path/../lib/lean") set(LEANSHARED_LINKER_FLAGS "${LEANSHARED_LINKER_FLAGS} -install_name @rpath/libleanshared.dylib") + set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -Wl,-rpath,@executable_path/../lib -Wl,-rpath,@executable_path/../lib/lean") endif() if(${CMAKE_SYSTEM_NAME} MATCHES "Linux") From 783719688c3f1954fd22924603ba1f18dbb1e900 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 18 Oct 2021 16:50:11 +0200 Subject: [PATCH 03/27] feat: String.replace --- src/Init/Data/String/Basic.lean | 41 ++++++++++++++++++++++----------- 1 file changed, 27 insertions(+), 14 deletions(-) diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean index 002d9641b7c2..8ab05886a8ab 100644 --- a/src/Init/Data/String/Basic.lean +++ b/src/Init/Data/String/Basic.lean @@ -244,11 +244,6 @@ def forward : Iterator → Nat → Iterator def remainingToString : Iterator → String | ⟨s, i⟩ => s.extract i s.bsize -/-- `(isPrefixOfRemaining it₁ it₂)` is `true` iff `it₁.remainingToString` is a prefix - of `it₂.remainingToString`. -/ -def isPrefixOfRemaining : Iterator → Iterator → Bool - | ⟨s₁, i₁⟩, ⟨s₂, i₂⟩ => s₁.extract i₁ s₁.bsize = s₂.extract i₂ (i₂ + (s₁.bsize - i₁)) - def nextn : Iterator → Nat → Iterator | it, 0 => it | it, i+1 => nextn it.next i @@ -320,15 +315,34 @@ def toNat? (s : String) : Option Nat := else none +/-- +Return `true` iff the substring of length `sz` starting at position `off1` in `s1` is equal to that starting at `off2` in `s2.`. +False if either substring of that length does not exist. -/ +partial def substrEq (s1 : String) (off1 : String.Pos) (s2 : String) (off2 : String.Pos) (sz : Nat) : Bool := + off1 + sz ≤ s1.bsize && off2 + sz ≤ s2.bsize && loop off1 off2 (off1 + sz) +where + loop (off1 off2 stop1 : Pos) := + if off1 >= stop1 then true + else + let c₁ := s1.get off1 + let c₂ := s2.get off2 + c₁ == c₂ && loop (off1 + csize c₁) (off2 + csize c₂) stop1 + /-- Return true iff `p` is a prefix of `s` -/ -partial def isPrefixOf (p : String) (s : String) : Bool := - let rec loop (i : Pos) := - if p.atEnd i then true +def isPrefixOf (p : String) (s : String) : Bool := + substrEq p 0 s 0 p.bsize + +/-- Replace all occurrences of `pattern` in `s` with `replacment`. -/ +partial def replace (s pattern replacement : String) : String := + loop "" 0 0 +where + loop (acc : String) (accStop pos : String.Pos) := + if pos + pattern.bsize > s.bsize then + acc ++ s.extract accStop s.bsize + else if s.substrEq pos pattern 0 pattern.bsize then + loop (acc ++ s.extract accStop pos ++ replacement) (pos + pattern.bsize) (pos + pattern.bsize) else - let c₁ := p.get i - let c₂ := s.get i - c₁ == c₂ && loop (s.next i) - p.length ≤ s.length && loop 0 + loop acc accStop (s.next pos) end String @@ -491,8 +505,7 @@ def toNat? (s : Substring) : Option Nat := none def beq (ss1 ss2 : Substring) : Bool := - -- TODO: should not allocate - ss1.bsize == ss2.bsize && ss1.toString == ss2.toString + ss1.bsize == ss2.bsize && ss1.str.substrEq ss1.startPos ss2.str ss2.startPos ss1.bsize instance hasBeq : BEq Substring := ⟨beq⟩ From a4663203ab0478585e55af5b2728d56ffc32ce9e Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 8 Sep 2021 18:56:19 +0200 Subject: [PATCH 04/27] feat: bundling LLVM on Linux --- .github/workflows/ci.yml | 14 +++++++++---- nix/bootstrap.nix | 4 ++-- script/prepare-llvm-linux.sh | 35 +++++++++++++++++++++++++++++++++ shell.nix | 4 ++++ src/CMakeLists.txt | 7 ++++--- src/Leanc.lean | 16 ++++++++------- src/bin/leanc.in | 9 ++++++--- src/shell/CMakeLists.txt | 38 +++++++++++++++++++----------------- 8 files changed, 90 insertions(+), 37 deletions(-) create mode 100755 script/prepare-llvm-linux.sh diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index cb8c5302ffef..3d8deaab0c6b 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -22,11 +22,12 @@ jobs: strategy: matrix: include: - # portable release build: link most libraries statically and use channel with older glibc (2.27; LLVM 7) + # portable release build: use channel with older glibc (2.27) - name: Linux release os: ubuntu-latest release: true shell: nix-shell --arg pkgs "import (fetchTarball \"channel:nixos-19.03\") {{}}" --argstr llvmPackages latest --run "bash -euxo pipefail {0}" + llvm-url: https://github.com/llvm/llvm-project/releases/download/llvmorg-13.0.0/clang+llvm-13.0.0-x86_64-linux-gnu-ubuntu-16.04.tar.xz - name: Linux os: ubuntu-latest check-stage3: true @@ -100,18 +101,23 @@ jobs: run: | mkdir build cd build - OPTIONS= + OPTIONS=() + if [[ '${{ matrix.llvm-url }}' && "${{ matrix.name }}" == "Linux release" ]]; then + wget -q ${{ matrix.llvm-url }} + eval "OPTIONS+=($(../script/prepare-llvm-linux.sh clang*.tar.*))" + fi if [[ $GITHUB_EVENT_NAME == 'schedule' && -n '${{ matrix.release }}' && -n '${{ secrets.PUSH_NIGHTLY_TOKEN }}' ]]; then git remote add nightly https://foo:'${{ secrets.PUSH_NIGHTLY_TOKEN }}'@github.com/${{ github.repository_owner }}/lean4-nightly.git git fetch nightly --tags LEAN_VERSION_STRING="nightly-$(date -u +%F)" # do nothing if commit already has a different tag if [[ $(git name-rev --name-only --tags --no-undefined HEAD 2> /dev/null || echo $LEAN_VERSION_STRING) == $LEAN_VERSION_STRING ]]; then - OPTIONS=-DLEAN_SPECIAL_VERSION_DESC=$LEAN_VERSION_STRING + OPTIONS+=(-DLEAN_SPECIAL_VERSION_DESC=$LEAN_VERSION_STRING) echo "LEAN_VERSION_STRING=$LEAN_VERSION_STRING" >> $GITHUB_ENV fi fi - cmake .. ${{ matrix.CMAKE_OPTIONS }} $OPTIONS + # contortion to support empty OPTIONS with old macOS bash + cmake .. ${{ matrix.CMAKE_OPTIONS }} ${OPTIONS[@]+"${OPTIONS[@]}"} make -j4 # de-Nix-ify binaries - name: Patch diff --git a/nix/bootstrap.nix b/nix/bootstrap.nix index 7fafcf4085c5..a951b97305aa 100644 --- a/nix/bootstrap.nix +++ b/nix/bootstrap.nix @@ -1,5 +1,5 @@ { debug ? false, stage0debug ? false, extraCMakeFlags ? [], - stdenv, lib, cmake, gmp, gnumake, bash, buildLeanPackage, writeShellScriptBin, runCommand, symlinkJoin, lndir, perl, + stdenv, lib, cmake, gmp, gnumake, bash, buildLeanPackage, writeShellScriptBin, runCommand, symlinkJoin, lndir, perl, gnused, ... } @ args: with builtins; rec { @@ -36,7 +36,7 @@ rec { mv bin/ include/ share/ $out/ mv leanc.sh $out/bin/leanc mv leanc/Leanc.lean $leanc_src/ - substituteInPlace $out/bin/leanc --replace '$root' "$out" + substituteInPlace $out/bin/leanc --replace '$root' "$out" --replace " sed " " ${gnused}/bin/sed " substituteInPlace $out/bin/leanmake --replace "make" "${gnumake}/bin/make" substituteInPlace $out/share/lean/lean.mk --replace "/usr/bin/env bash" "${bash}/bin/bash" ''; diff --git a/script/prepare-llvm-linux.sh b/script/prepare-llvm-linux.sh new file mode 100755 index 000000000000..74f1ee727685 --- /dev/null +++ b/script/prepare-llvm-linux.sh @@ -0,0 +1,35 @@ +#!/usr/bin/env bash +set -uo pipefail + +# run from root build directory (from inside nix-shell or otherwise defining GLIBC/GCC_DEV/GCC_LIBS/GMP) as in +# ``` +# eval cmake ../.. $(../../script/prepare-llvm-linux.sh ~/Downloads/clang+llvm-13.0.0-x86_64-linux-gnu-ubuntu-16.04.tar.xz) +# ``` + +# use full LLVM release for compiling C++ code, but subset for compiling C code and distribution + +[[ -d llvm ]] || (mkdir llvm; tar xf $1 --strip-components 1 --directory llvm) +mkdir -p stage1/{bin,lib,lib/glibc,include/clang} +CP="cp -d" # preserve symlinks +# a C compiler! +$CP $(realpath llvm/bin/clang) stage1/bin/clang +# a linker! +$CP llvm/bin/{lld,ld.lld} stage1/bin/ +# lean.h dependencies +$CP llvm/lib/clang/*/include/{std*,__std*,limits}.h stage1/include/clang +# ELF dependencies, must be put there for `--sysroot` +$CP $GLIBC/lib/crt* llvm/lib/ +$CP $GLIBC/lib/crt* stage1/lib/ +# further dependencies +# note that official LLVM releases are not built against compiler-rt, thus the GCC deps +$CP $GCC_ROOT/lib/gcc/*/*/libgcc.a $GCC_ROOT/lib/gcc/*/*/crt{begin,end}{,S}.o $GCC_LIBS/lib/libatomic.so* llvm/lib/libc++* $GMP/lib/libgmp.* stage1/lib/ +# glibc: use for linking (so Lean programs don't embed newer symbol versions), but not for running (because libc.so, librt.so, and ld.so must be compatible)! +$CP $GLIBC/lib/lib{c_nonshared,gcc_s}* stage1/lib/glibc +for f in $GLIBC/lib/lib{c,dl,m,rt,pthread}-*; do b=$(basename $f); cp $f stage1/lib/glibc/${b%-*}.so; done +OPTIONS=() +echo -n " -DCMAKE_C_COMPILER=$PWD/stage1/bin/clang -DCMAKE_CXX_COMPILER=$PWD/llvm/bin/clang++ -DLEAN_USE_LIBCXX=ON" +# allow C++ code to include /usr since it needs quite a few more headers +echo -n " -DLEAN_EXTRA_CXX_FLAGS='--sysroot $PWD/llvm --stdlib=libc++ -I/usr/include -I/usr/include/x86_64-linux-gnu'" +echo -n " -DLEANC_INTERNAL_FLAGS='--sysroot ROOT -I ROOT/include/clang' -DLEANC_CC=ROOT/bin/clang" +echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -L ROOT/lib/glibc ROOT/lib/glibc/libc_nonshared.a -fuse-ld=ROOT/bin/ld.lld'" +echo -n " -DLEAN_TEST_VARS='LD_LIBRARY_PATH=$PWD/stage1/lib:\${LD_LIBRARY_PATH:-}'" diff --git a/shell.nix b/shell.nix index 470d6a82ce0b..09d220f0899d 100644 --- a/shell.nix +++ b/shell.nix @@ -13,6 +13,10 @@ in { pkgs ? flakePkgs.nixpkgs, llvmPackages ? null }: hardeningDisable = [ "all" ]; # more convenient `ctest` output CTEST_OUTPUT_ON_FAILURE = 1; + GMP = pkgs.gmp; + GLIBC = pkgs.glibc; + GCC_ROOT = pkgs.gcc.cc; + GCC_LIBS = pkgs.gcc.cc.lib; shellHook = '' export LEAN_SRC_PATH="$PWD/src" ''; diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 0763b479dab2..3b65cb61e542 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -20,6 +20,7 @@ endif() set(LEAN_EXTRA_LINKER_FLAGS "" CACHE STRING "Additional flags used by the linker") set(LEAN_EXTRA_CXX_FLAGS "" CACHE STRING "Additional flags used by the C++ compiler") +set(LEAN_TEST_VARS "LEAN_CC=${CMAKE_C_COMPILER}" CACHE STRING "Additional environment variables used when running tests") if (NOT CMAKE_BUILD_TYPE) message(STATUS "No build type selected, default to Release") @@ -276,7 +277,7 @@ else() set(LEANC_STATIC_LINKER_FLAGS "-Wl,--start-group -lleancpp -lLean -Wl,--end-group -Wl,--start-group -lInit -lStd -lleanrt -Wl,--end-group") endif() -if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin") +if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin" OR "${LEAN_USE_LIBCXX}") set(LEANC_STATIC_LINKER_FLAGS "${LEANC_STATIC_LINKER_FLAGS} -lc++") set(LEANSHARED_LINKER_FLAGS "${LEANSHARED_LINKER_FLAGS} -lc++") else() @@ -303,7 +304,7 @@ elseif(${CMAKE_SYSTEM_NAME} MATCHES "Darwin") endif() if(${CMAKE_SYSTEM_NAME} MATCHES "Linux") - set(LEAN_EXTRA_LINKER_FLAGS "${LEAN_LINKER_FLAGS} -ldl") + set(LEAN_EXTRA_LINKER_FLAGS "${LEAN_EXTRA_LINKER_FLAGS} -ldl") endif() if(NOT(${CMAKE_SYSTEM_NAME} MATCHES "Windows")) @@ -387,7 +388,7 @@ include_directories(${CMAKE_BINARY_DIR}/include) # config.h etc., "public" head string(TOUPPER "${CMAKE_BUILD_TYPE}" uppercase_CMAKE_BUILD_TYPE) # These are used in lean.mk (and libleanrt) and passed through by stdlib.make # They are not embedded into `leanc` since they are build profile/machine specific -set(LEANC_OPTS "${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}}") +set(LEANC_OPTS "${LEANC_OPTS} ${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}}") if(CMAKE_OSX_SYSROOT) string(APPEND LEANC_OPTS " ${CMAKE_CXX_SYSROOT_FLAG}${CMAKE_OSX_SYSROOT}") endif() diff --git a/src/Leanc.lean b/src/Leanc.lean index 16c2b84bcbb8..34469aba41b2 100644 --- a/src/Leanc.lean +++ b/src/Leanc.lean @@ -17,10 +17,14 @@ Beware of the licensing consequences since GMP is LGPL." let root ← match (← IO.getEnv "LEAN_SYSROOT") with | some root => System.FilePath.mk root | none => (← IO.appDir).parent.get! + let rootify s := s.replace "ROOT" root.toString + -- We assume that the CMake variables do not contain escaped spaces let cflags := ["-I", (root / "include").toString] ++ "@LEANC_EXTRA_FLAGS@".trim.splitOn + let cflagsHidden := "@LEANC_INTERNAL_FLAGS@".trim.splitOn let mut ldflags := ["-L", (root / "lib").toString, "-L", (root / "lib" / "lean").toString, (← IO.getEnv "LEANC_GMP").getD "-lgmp"] ++ "@LEAN_EXTRA_LINKER_FLAGS@".trim.splitOn let mut ldflagsExt := "@LEANC_STATIC_LINKER_FLAGS@".trim.splitOn + let ldflagsHidden := "@LEANC_INTERNAL_LINKER_FLAGS@".trim.splitOn for arg in args do match arg with @@ -31,18 +35,16 @@ Beware of the licensing consequences since GMP is LGPL." ldflags := [] ldflagsExt := [] | "--print-cflags" => - IO.println <| " ".intercalate cflags + IO.println <| " ".intercalate (cflags.map rootify) return 0 | "--print-ldflags" => - IO.println <| " ".intercalate (cflags ++ ldflagsExt ++ ldflags) + IO.println <| " ".intercalate ((cflags ++ ldflagsExt ++ ldflags).map rootify) return 0 | _ => () - let mut cc := (← IO.getEnv "LEAN_CC").getD "@LEANC_CC@" - if cc.startsWith "." then - cc := (root / "bin" / cc).toString - - let args := cflags ++ args ++ ldflagsExt ++ ldflags ++ ["-Wno-unused-command-line-argument"] + let cc := rootify <| (← IO.getEnv "LEAN_CC").getD "@LEANC_CC@" + let args := cflags ++ cflagsHidden ++ args ++ ldflagsExt ++ ldflags ++ ldflagsHidden ++ ["-Wno-unused-command-line-argument"] + let args := args.map rootify if args.contains "-v" then IO.eprintln s!"{cc} {" ".intercalate args}" let child ← IO.Process.spawn { cmd := cc, args := args.toArray } diff --git a/src/bin/leanc.in b/src/bin/leanc.in index e6bb09797aff..cc7a6158b31d 100755 --- a/src/bin/leanc.in +++ b/src/bin/leanc.in @@ -1,10 +1,13 @@ #!/usr/bin/env bash # used only for building Lean itself root=$(dirname $0) -ldflags=("-L$root/lib/lean" "${LEANC_GMP:--lgmp}" @LEAN_EXTRA_LINKER_FLAGS@) +ldflags=("-L$root/lib" "-L$root/lib/lean" "${LEANC_GMP:--lgmp}" @LEAN_EXTRA_LINKER_FLAGS@ @LEANC_INTERNAL_LINKER_FLAGS@) for arg in "$@"; do # ccache doesn't like linker flags being passed here [[ "$arg" = "-c" ]] && ldflags=() - [[ "$arg" = "-v" ]] && set -x + [[ "$arg" = "-v" ]] && v=1 done -exec ${LEAN_CC:-@CMAKE_C_COMPILER@} "-I$root/include" @LEANC_EXTRA_FLAGS@ "$@" "${ldflags[@]}" -Wno-unused-command-line-argument +cmd=(${LEAN_CC:-@CMAKE_C_COMPILER@} "-I$root/include" @LEANC_EXTRA_FLAGS@ @LEANC_INTERNAL_FLAGS@ "$@" "${ldflags[@]}" -Wno-unused-command-line-argument) +cmd=$(printf '%q ' "${cmd[@]}" | sed "s!ROOT!$root!g") +[[ $v == 1 ]] && printf '%q ' $cmd +eval $cmd diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index c904abe9992f..85f33616e823 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -46,6 +46,8 @@ add_test(lean_ghash2 "${CMAKE_BINARY_DIR}/bin/lean" --githash) add_test(lean_unknown_option bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_BINARY_DIR}/bin/lean" "-z") add_test(lean_unknown_file1 bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_BINARY_DIR}/bin/lean" "boofoo.lean") +set(TEST_VARS "PATH=${LEAN_BIN}:$PATH ${LEAN_TEST_VARS}") + # LEAN TESTS file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.lean") FOREACH(T ${LEANTESTS}) @@ -53,7 +55,7 @@ FOREACH(T ${LEANTESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leantest_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean" - COMMAND bash -c "PATH=${LEAN_BIN}:$PATH ./test_single.sh ${T_NAME}") + COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}") endif() ENDFOREACH(T) @@ -64,7 +66,7 @@ FOREACH(T ${LEANRUNTESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leanruntest_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/run" - COMMAND bash -c "PATH=${LEAN_BIN}:$PATH ./test_single.sh ${T_NAME}") + COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}") endif() ENDFOREACH(T) @@ -74,7 +76,7 @@ FOREACH(T ${LEANCOMPTESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leancomptest_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/compiler" - COMMAND bash -c "PATH=${LEAN_BIN}:$PATH ./test_single.sh ${T_NAME}") + COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}") ENDFOREACH(T) add_test(NAME leancomptest_foreign @@ -82,7 +84,7 @@ add_test(NAME leancomptest_foreign COMMAND bash -c "${LEAN_BIN}/leanmake --always-make CXX='${CMAKE_CXX_COMPILER} ${LEANC_OPTS}'") add_test(NAME leancomptest_doc_example WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../doc/examples/compiler" - COMMAND bash -c "${LEAN_BIN}/leanmake --always-make bin && ./build/bin/test hello world") + COMMAND bash -c "export ${TEST_VARS}; leanmake --always-make bin && ./build/bin/test hello world") # LEAN INTERPRETER TESTS file(GLOB LEANINTERPTESTS "${LEAN_SOURCE_DIR}/../tests/compiler/*.lean") @@ -91,7 +93,7 @@ FOREACH(T ${LEANINTERPTESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leaninterptest_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/compiler" - COMMAND bash -c "PATH=${LEAN_BIN}:$PATH ./test_single_interpret.sh ${T_NAME}") + COMMAND bash -c "${TEST_VARS} ./test_single_interpret.sh ${T_NAME}") endif() ENDFOREACH(T) @@ -103,7 +105,7 @@ FOREACH(T_OUT ${LEANBENCHTESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leanbenchtest_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/bench" - COMMAND bash -c "PATH=${LEAN_BIN}:$PATH ./test_single.sh ${T_NAME}") + COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}") ENDFOREACH(T_OUT) file(GLOB LEANINTERPTESTS "${LEAN_SOURCE_DIR}/../tests/plugin/*.lean") @@ -111,7 +113,7 @@ FOREACH(T ${LEANINTERPTESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leanplugintest_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/plugin" - COMMAND bash -c "PATH=${LEAN_BIN}:$PATH ./test_single.sh ${T_NAME}") + COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}") ENDFOREACH(T) # LEAN TESTS using --trust=0 @@ -120,7 +122,7 @@ FOREACH(T ${LEANT0TESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leant0test_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/trust0" - COMMAND bash -c "PATH=${LEAN_BIN}:$PATH ./test_single.sh ${T_NAME}") + COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}") ENDFOREACH(T) # LEAN SERVER TESTS @@ -130,7 +132,7 @@ FOREACH(T ${LEANTESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leanservertest_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/server" - COMMAND bash -c "PATH=${LEAN_BIN}:$PATH ./test_single.sh ${T_NAME}") + COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}") endif() ENDFOREACH(T) @@ -141,7 +143,7 @@ FOREACH(T ${LEANTESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leaninteractivetest_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/interactive" - COMMAND bash -c "PATH=${LEAN_BIN}:$PATH ./test_single.sh ${T_NAME}") + COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}") endif() ENDFOREACH(T) @@ -149,7 +151,7 @@ add_test(NAME leanpkgtest WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/b" COMMAND bash -c " set -eu - export PATH=${LEAN_BIN}:$PATH + export ${TEST_VARS} leanpkg build # linking requires some manual steps (cd ../a; leanpkg build lib) @@ -160,14 +162,14 @@ add_test(NAME leanpkgtest_cyclic WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/cyclic" COMMAND bash -c " set -eu - export PATH=${LEAN_BIN}:$PATH + export ${TEST_VARS} leanpkg build 2>&1 | grep 'import cycle'") add_test(NAME leanpkgtest_user_ext WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/user_ext" COMMAND bash -c " set -eu - export PATH=${LEAN_BIN}:$PATH + export ${TEST_VARS} find . -name '*.olean' -delete leanmake | grep 'world, hello, test'") @@ -175,7 +177,7 @@ add_test(NAME leanpkgtest_user_attr WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/user_attr" COMMAND bash -c " set -eu - export PATH=${LEAN_BIN}:$PATH + export ${TEST_VARS} find . -name '*.olean' -delete leanmake") @@ -183,7 +185,7 @@ add_test(NAME leanpkgtest_user_opt WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/user_opt" COMMAND bash -c " set -eu - export PATH=${LEAN_BIN}:$PATH + export ${TEST_VARS} find . -name '*.olean' -delete leanmake") @@ -191,7 +193,7 @@ add_test(NAME leanpkgtest_prv WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/prv" COMMAND bash -c " set -eu - export PATH=${LEAN_BIN}:$PATH + export ${TEST_VARS} find . -name '*.olean' -delete leanmake 2>&1 | grep 'error: field.*private'") @@ -199,7 +201,7 @@ add_test(NAME leanpkgtest_user_attr_app WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/user_attr_app" COMMAND bash -c " set -eu - export PATH=${LEAN_BIN}:$PATH + export ${TEST_VARS} find . -name '*.olean' -delete leanmake bin LINK_OPTS='${LEAN_DYN_EXE_LINKER_FLAGS}' && build/bin/UserAttr") @@ -215,5 +217,5 @@ add_test(NAME laketest WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/lake/examples" COMMAND bash -c " set -eu - export PATH=${LEAN_BIN}:$PATH + export ${TEST_VARS} make LAKE=lake test") From 7f1e357543d70e694d4665bd3e22c31f66c44594 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 22 Oct 2021 10:40:22 +0200 Subject: [PATCH 05/27] fix: actually install all bundled files --- src/CMakeLists.txt | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 3b65cb61e542..20736c65390f 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -377,9 +377,9 @@ else() set(LEAN_IS_STAGE0 "#define LEAN_IS_STAGE0 0") endif() configure_file("${LEAN_SOURCE_DIR}/config.h.in" "${LEAN_BINARY_DIR}/include/lean/config.h") -install(DIRECTORY ${LEAN_BINARY_DIR}/include/lean DESTINATION include) +install(DIRECTORY ${LEAN_BINARY_DIR}/include/ DESTINATION include) configure_file(${LEAN_SOURCE_DIR}/lean.mk.in ${LEAN_BINARY_DIR}/share/lean/lean.mk) -install(DIRECTORY ${LEAN_BINARY_DIR}/share/lean DESTINATION share) +install(DIRECTORY ${LEAN_BINARY_DIR}/share/ DESTINATION share) include_directories(${LEAN_SOURCE_DIR}) include_directories(${CMAKE_BINARY_DIR}) # version.h etc., "private" headers @@ -518,7 +518,7 @@ add_custom_target(clean-stdlib add_custom_target(clean-olean DEPENDS clean-stdlib) -install(DIRECTORY "${CMAKE_BINARY_DIR}/lib/lean" DESTINATION lib) +install(DIRECTORY "${CMAKE_BINARY_DIR}/lib/" DESTINATION lib PATTERN temp EXCLUDE) install(CODE "execute_process(COMMAND sh -c \"cp ${CMAKE_BINARY_DIR}/lib/*.* \${CMAKE_INSTALL_PREFIX}/lib\")") From 48cf118b28b80fd328f78352c6b60cb1d48f8344 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 22 Oct 2021 10:43:25 +0200 Subject: [PATCH 06/27] fix: leanc: discard internal flag when using external compiler --- src/Leanc.lean | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/src/Leanc.lean b/src/Leanc.lean index 34469aba41b2..bd5099f0248e 100644 --- a/src/Leanc.lean +++ b/src/Leanc.lean @@ -21,10 +21,10 @@ Beware of the licensing consequences since GMP is LGPL." -- We assume that the CMake variables do not contain escaped spaces let cflags := ["-I", (root / "include").toString] ++ "@LEANC_EXTRA_FLAGS@".trim.splitOn - let cflagsHidden := "@LEANC_INTERNAL_FLAGS@".trim.splitOn + let mut cflagsInternal := "@LEANC_INTERNAL_FLAGS@".trim.splitOn let mut ldflags := ["-L", (root / "lib").toString, "-L", (root / "lib" / "lean").toString, (← IO.getEnv "LEANC_GMP").getD "-lgmp"] ++ "@LEAN_EXTRA_LINKER_FLAGS@".trim.splitOn let mut ldflagsExt := "@LEANC_STATIC_LINKER_FLAGS@".trim.splitOn - let ldflagsHidden := "@LEANC_INTERNAL_LINKER_FLAGS@".trim.splitOn + let mut ldflagsInternal := "@LEANC_INTERNAL_LINKER_FLAGS@".trim.splitOn for arg in args do match arg with @@ -42,8 +42,14 @@ Beware of the licensing consequences since GMP is LGPL." return 0 | _ => () - let cc := rootify <| (← IO.getEnv "LEAN_CC").getD "@LEANC_CC@" - let args := cflags ++ cflagsHidden ++ args ++ ldflagsExt ++ ldflags ++ ldflagsHidden ++ ["-Wno-unused-command-line-argument"] + let mut cc := "@LEANC_CC@" + if let some cc' ← IO.getEnv "LEAN_CC" then + cc := cc' + -- these are intended for the bundled compiler only + cflagsInternal := [] + ldflagsInternal := [] + cc := rootify cc + let args := cflags ++ cflagsInternal ++ args ++ ldflagsExt ++ ldflags ++ ldflagsInternal ++ ["-Wno-unused-command-line-argument"] let args := args.map rootify if args.contains "-v" then IO.eprintln s!"{cc} {" ".intercalate args}" From a8ea78201699c2247c334c9f637a32eed0441e20 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 22 Oct 2021 12:24:42 +0200 Subject: [PATCH 07/27] chore: CI: no more need for binary patching --- .github/workflows/ci.yml | 17 +++-------------- 1 file changed, 3 insertions(+), 14 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 3d8deaab0c6b..dc5723cde314 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -119,22 +119,11 @@ jobs: # contortion to support empty OPTIONS with old macOS bash cmake .. ${{ matrix.CMAKE_OPTIONS }} ${OPTIONS[@]+"${OPTIONS[@]}"} make -j4 - # de-Nix-ify binaries - - name: Patch + - name: Check binaries if: matrix.name == 'Linux release' run: | - cd build/stage1 - for f in lib/lean/libleanshared.so bin/lean bin/leanpkg bin/leanc bin/lake; do - cp -n $(ldd "$f" | cut -f3 -d' ' | grep -Ev 'libc|lean') lib/ || true - if [[ "$f" == bin/* ]]; then - patchelf --set-interpreter /lib64/ld-linux-x86-64.so.2 --set-rpath '$ORIGIN/../lib:$ORIGIN/../lib/lean' $f - else - # library: use executable RPATH - patchelf --remove-rpath $f - fi - ldd $f - done - ls -l lib/ + ldd -v build/stage1/bin/* || true + ls -l build/stage1/lib/ - name: Patch if: matrix.name == 'macOS' run: | From fc6cf90e0d78860eb6ce99de05e01d7a31069eab Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 22 Oct 2021 14:02:24 +0200 Subject: [PATCH 08/27] chore: CI: list archive contents & sizes --- .github/workflows/ci.yml | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index dc5723cde314..6efd5858125b 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -74,11 +74,11 @@ jobs: - name: Install MSYS2 uses: msys2/setup-msys2@v2 with: - install: make python mingw-w64-x86_64-cmake mingw-w64-x86_64-clang mingw-w64-x86_64-ccache git unzip diffutils binutils + install: make python mingw-w64-x86_64-cmake mingw-w64-x86_64-clang mingw-w64-x86_64-ccache git unzip diffutils binutils tree if: matrix.os == 'windows-2022' - name: Install Brew Packages run: | - brew install ccache + brew install ccache tree if: matrix.os == 'macos-latest' - name: Cache uses: actions/cache@v2 @@ -151,7 +151,12 @@ jobs: run: | build/stage1/bin/lean -h - name: Pack - run: cd build/stage1; cpack + run: | + cd build/stage1 + cpack + mkdir unpack + tar xf lean-* -C unpack || unzip lean-4 -d unpack + tree --du -h unpack - uses: actions/upload-artifact@v2 with: name: build-${{ matrix.name }} From 46f3c29ac76878d2ad67fcc9579ae5c2b20ca273 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 27 Oct 2021 15:42:08 +0200 Subject: [PATCH 09/27] feat: use custom, more minimal LLVM build --- .github/workflows/ci.yml | 4 ++-- script/prepare-llvm-linux.sh | 14 ++++++++++---- shell.nix | 2 -- 3 files changed, 12 insertions(+), 8 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 6efd5858125b..b42d18b674bd 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -27,7 +27,7 @@ jobs: os: ubuntu-latest release: true shell: nix-shell --arg pkgs "import (fetchTarball \"channel:nixos-19.03\") {{}}" --argstr llvmPackages latest --run "bash -euxo pipefail {0}" - llvm-url: https://github.com/llvm/llvm-project/releases/download/llvmorg-13.0.0/clang+llvm-13.0.0-x86_64-linux-gnu-ubuntu-16.04.tar.xz + llvm-url: https://github.com/leanprover/lean-llvm/releases/download/13.0.0/lean-llvm.tar.zst - name: Linux os: ubuntu-latest check-stage3: true @@ -104,7 +104,7 @@ jobs: OPTIONS=() if [[ '${{ matrix.llvm-url }}' && "${{ matrix.name }}" == "Linux release" ]]; then wget -q ${{ matrix.llvm-url }} - eval "OPTIONS+=($(../script/prepare-llvm-linux.sh clang*.tar.*))" + eval "OPTIONS+=($(../script/prepare-llvm-linux.sh *llvm*))" fi if [[ $GITHUB_EVENT_NAME == 'schedule' && -n '${{ matrix.release }}' && -n '${{ secrets.PUSH_NIGHTLY_TOKEN }}' ]]; then git remote add nightly https://foo:'${{ secrets.PUSH_NIGHTLY_TOKEN }}'@github.com/${{ github.repository_owner }}/lean4-nightly.git diff --git a/script/prepare-llvm-linux.sh b/script/prepare-llvm-linux.sh index 74f1ee727685..7c9c2ea117c3 100755 --- a/script/prepare-llvm-linux.sh +++ b/script/prepare-llvm-linux.sh @@ -1,7 +1,7 @@ #!/usr/bin/env bash set -uo pipefail -# run from root build directory (from inside nix-shell or otherwise defining GLIBC/GCC_DEV/GCC_LIBS/GMP) as in +# run from root build directory (from inside nix-shell or otherwise defining GLIBC/GMP) as in # ``` # eval cmake ../.. $(../../script/prepare-llvm-linux.sh ~/Downloads/clang+llvm-13.0.0-x86_64-linux-gnu-ubuntu-16.04.tar.xz) # ``` @@ -15,14 +15,20 @@ CP="cp -d" # preserve symlinks $CP $(realpath llvm/bin/clang) stage1/bin/clang # a linker! $CP llvm/bin/{lld,ld.lld} stage1/bin/ +# dependencies of the above +$CP llvm/lib/lib{clang-cpp,LLVM}*.so* stage1/lib/ +# clang can't even find its own deps in a standard build? ¯\_(ツ)_/¯ +ln llvm/lib/x86*/* llvm/lib +# ...nor are the rpaths sensible +patchelf --set-rpath '$ORIGIN' llvm/lib/libc++.so.* # lean.h dependencies $CP llvm/lib/clang/*/include/{std*,__std*,limits}.h stage1/include/clang # ELF dependencies, must be put there for `--sysroot` $CP $GLIBC/lib/crt* llvm/lib/ $CP $GLIBC/lib/crt* stage1/lib/ -# further dependencies -# note that official LLVM releases are not built against compiler-rt, thus the GCC deps -$CP $GCC_ROOT/lib/gcc/*/*/libgcc.a $GCC_ROOT/lib/gcc/*/*/crt{begin,end}{,S}.o $GCC_LIBS/lib/libatomic.so* llvm/lib/libc++* $GMP/lib/libgmp.* stage1/lib/ +# runtime +(cd llvm; $CP --parents lib/clang/*/lib/*/{*crt{begin,end}.o,libclang_rt.builtins*} ../stage1) +$CP llvm/lib/lib{c++,c++abi,unwind}.* $GMP/lib/libgmp.* stage1/lib/ # glibc: use for linking (so Lean programs don't embed newer symbol versions), but not for running (because libc.so, librt.so, and ld.so must be compatible)! $CP $GLIBC/lib/lib{c_nonshared,gcc_s}* stage1/lib/glibc for f in $GLIBC/lib/lib{c,dl,m,rt,pthread}-*; do b=$(basename $f); cp $f stage1/lib/glibc/${b%-*}.so; done diff --git a/shell.nix b/shell.nix index 09d220f0899d..1c7d397242e3 100644 --- a/shell.nix +++ b/shell.nix @@ -15,8 +15,6 @@ in { pkgs ? flakePkgs.nixpkgs, llvmPackages ? null }: CTEST_OUTPUT_ON_FAILURE = 1; GMP = pkgs.gmp; GLIBC = pkgs.glibc; - GCC_ROOT = pkgs.gcc.cc; - GCC_LIBS = pkgs.gcc.cc.lib; shellHook = '' export LEAN_SRC_PATH="$PWD/src" ''; From 23b99c4639e232fccce582cf9c0a5c98d0f0b220 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 28 Oct 2021 12:01:47 +0200 Subject: [PATCH 10/27] feat: link external dependencies statically again --- script/prepare-llvm-linux.sh | 11 ++++++----- shell.nix | 2 +- src/CMakeLists.txt | 13 +++++++------ src/Leanc.lean | 2 +- 4 files changed, 15 insertions(+), 13 deletions(-) diff --git a/script/prepare-llvm-linux.sh b/script/prepare-llvm-linux.sh index 7c9c2ea117c3..e1b943c580a2 100755 --- a/script/prepare-llvm-linux.sh +++ b/script/prepare-llvm-linux.sh @@ -28,14 +28,15 @@ $CP $GLIBC/lib/crt* llvm/lib/ $CP $GLIBC/lib/crt* stage1/lib/ # runtime (cd llvm; $CP --parents lib/clang/*/lib/*/{*crt{begin,end}.o,libclang_rt.builtins*} ../stage1) -$CP llvm/lib/lib{c++,c++abi,unwind}.* $GMP/lib/libgmp.* stage1/lib/ +$CP llvm/lib/lib{c++,c++abi,unwind}.* $GMP/lib/libgmp.a stage1/lib/ # glibc: use for linking (so Lean programs don't embed newer symbol versions), but not for running (because libc.so, librt.so, and ld.so must be compatible)! -$CP $GLIBC/lib/lib{c_nonshared,gcc_s}* stage1/lib/glibc +$CP $GLIBC/lib/libc_nonshared.a stage1/lib/glibc for f in $GLIBC/lib/lib{c,dl,m,rt,pthread}-*; do b=$(basename $f); cp $f stage1/lib/glibc/${b%-*}.so; done OPTIONS=() -echo -n " -DCMAKE_C_COMPILER=$PWD/stage1/bin/clang -DCMAKE_CXX_COMPILER=$PWD/llvm/bin/clang++ -DLEAN_USE_LIBCXX=ON" +echo -n " -DCMAKE_C_COMPILER=$PWD/stage1/bin/clang -DCMAKE_CXX_COMPILER=$PWD/llvm/bin/clang++ -DLEAN_CXX_STDLIB='-Wl,-Bstatic -lc++ -lc++abi -Wl,-Bdynamic'" # allow C++ code to include /usr since it needs quite a few more headers echo -n " -DLEAN_EXTRA_CXX_FLAGS='--sysroot $PWD/llvm --stdlib=libc++ -I/usr/include -I/usr/include/x86_64-linux-gnu'" echo -n " -DLEANC_INTERNAL_FLAGS='--sysroot ROOT -I ROOT/include/clang' -DLEANC_CC=ROOT/bin/clang" -echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -L ROOT/lib/glibc ROOT/lib/glibc/libc_nonshared.a -fuse-ld=ROOT/bin/ld.lld'" -echo -n " -DLEAN_TEST_VARS='LD_LIBRARY_PATH=$PWD/stage1/lib:\${LD_LIBRARY_PATH:-}'" +echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -L ROOT/lib/glibc ROOT/lib/glibc/libc_nonshared.a --rtlib=compiler-rt -static-libgcc -Wl,-Bstatic -lgmp -lunwind -Wl,-Bdynamic -fuse-ld=lld'" +# do not set `LEAN_CC` for tests +echo -n " -DLEAN_TEST_VARS=''" diff --git a/shell.nix b/shell.nix index 1c7d397242e3..152d04c65305 100644 --- a/shell.nix +++ b/shell.nix @@ -13,7 +13,7 @@ in { pkgs ? flakePkgs.nixpkgs, llvmPackages ? null }: hardeningDisable = [ "all" ]; # more convenient `ctest` output CTEST_OUTPUT_ON_FAILURE = 1; - GMP = pkgs.gmp; + GMP = pkgs.gmp.override { withStatic = true; }; GLIBC = pkgs.glibc; shellHook = '' export LEAN_SRC_PATH="$PWD/src" diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 20736c65390f..7702531bc3ab 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -277,14 +277,15 @@ else() set(LEANC_STATIC_LINKER_FLAGS "-Wl,--start-group -lleancpp -lLean -Wl,--end-group -Wl,--start-group -lInit -lStd -lleanrt -Wl,--end-group") endif() -if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin" OR "${LEAN_USE_LIBCXX}") - set(LEANC_STATIC_LINKER_FLAGS "${LEANC_STATIC_LINKER_FLAGS} -lc++") - set(LEANSHARED_LINKER_FLAGS "${LEANSHARED_LINKER_FLAGS} -lc++") -else() - set(LEANC_STATIC_LINKER_FLAGS "${LEANC_STATIC_LINKER_FLAGS} -lstdc++") - set(LEANSHARED_LINKER_FLAGS "${LEANSHARED_LINKER_FLAGS} -lstdc++") +set(LEAN_CXX_STDLIB "-lstdc++" CACHE STRING "C++ stdlib linker flags") + +if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin") + set(LEAN_CXX_STDLIB "-lc++") endif() +set(LEANC_STATIC_LINKER_FLAGS "${LEANC_STATIC_LINKER_FLAGS} ${LEAN_CXX_STDLIB}") +set(LEANSHARED_LINKER_FLAGS "${LEANSHARED_LINKER_FLAGS} ${LEAN_CXX_STDLIB}") + set(LEANC_STATIC_LINKER_FLAGS "${LEANC_STATIC_LINKER_FLAGS} -lm") set(LEANSHARED_LINKER_FLAGS "${LEANSHARED_LINKER_FLAGS} -lm") diff --git a/src/Leanc.lean b/src/Leanc.lean index bd5099f0248e..4205a4542682 100644 --- a/src/Leanc.lean +++ b/src/Leanc.lean @@ -22,7 +22,7 @@ Beware of the licensing consequences since GMP is LGPL." -- We assume that the CMake variables do not contain escaped spaces let cflags := ["-I", (root / "include").toString] ++ "@LEANC_EXTRA_FLAGS@".trim.splitOn let mut cflagsInternal := "@LEANC_INTERNAL_FLAGS@".trim.splitOn - let mut ldflags := ["-L", (root / "lib").toString, "-L", (root / "lib" / "lean").toString, (← IO.getEnv "LEANC_GMP").getD "-lgmp"] ++ "@LEAN_EXTRA_LINKER_FLAGS@".trim.splitOn + let mut ldflags := ["-L", (root / "lib" / "lean").toString, "-lgmp"] ++ "@LEAN_EXTRA_LINKER_FLAGS@".trim.splitOn let mut ldflagsExt := "@LEANC_STATIC_LINKER_FLAGS@".trim.splitOn let mut ldflagsInternal := "@LEANC_INTERNAL_LINKER_FLAGS@".trim.splitOn From 6f537394f3b44c3b2366a4a318beb6577602bc0c Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 28 Oct 2021 16:29:25 +0200 Subject: [PATCH 11/27] chore: gc libleanshared sections --- src/CMakeLists.txt | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 7702531bc3ab..01b977013a84 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -286,6 +286,13 @@ endif() set(LEANC_STATIC_LINKER_FLAGS "${LEANC_STATIC_LINKER_FLAGS} ${LEAN_CXX_STDLIB}") set(LEANSHARED_LINKER_FLAGS "${LEANSHARED_LINKER_FLAGS} ${LEAN_CXX_STDLIB}") +# get rid of unused parts of C++ stdlib +if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin") + set(LEANSHARED_LINKER_FLAGS "${LEANSHARED_LINKER_FLAGS} -Wl,-dead_strip") +else() + set(LEANSHARED_LINKER_FLAGS "${LEANSHARED_LINKER_FLAGS} -Wl,--gc-sections") +endif() + set(LEANC_STATIC_LINKER_FLAGS "${LEANC_STATIC_LINKER_FLAGS} -lm") set(LEANSHARED_LINKER_FLAGS "${LEANSHARED_LINKER_FLAGS} -lm") From f8ccdabdaf6387d2fdd7d9baf5fa93a9b1af0a5b Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 28 Oct 2021 16:46:19 +0200 Subject: [PATCH 12/27] chore: append licenses of LLVM & glibc --- LICENSE | 1174 +++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 1174 insertions(+) diff --git a/LICENSE b/LICENSE index 813da2975673..c0f2b9d8d7d7 100644 --- a/LICENSE +++ b/LICENSE @@ -1,3 +1,7 @@ +============================================================================== +The Lean project is under the Apache License 2.0: +============================================================================== + Apache License 2.0 (Apache) Apache License Version 2.0, January 2004 @@ -69,3 +73,1173 @@ In no event and under no legal theory, whether in tort (including negligence), c While redistributing the Work or Derivative Works thereof, You may choose to offer, and charge a fee for, acceptance of support, warranty, indemnity, or other liability obligations and/or rights consistent with this License. However, in accepting such obligations, You may act only on Your own behalf and on Your sole responsibility, not on behalf of any other Contributor, and only if You agree to indemnify, defend, and hold each Contributor harmless for any liability incurred by, or claims asserted against, such Contributor by reason of your accepting any such warranty or additional liability. +============================================================================== +The LLVM Project is under the Apache License v2.0 with LLVM Exceptions: +============================================================================== + + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright [yyyy] [name of copyright owner] + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. + + +---- LLVM Exceptions to the Apache 2.0 License ---- + +As an exception, if, as a result of your compiling your source code, portions +of this Software are embedded into an Object form of such source code, you +may redistribute such embedded portions in such Object form without complying +with the conditions of Sections 4(a), 4(b) and 4(d) of the License. + +In addition, if you combine or link compiled forms of this Software with +software that is licensed under the GPLv2 ("Combined Software") and if a +court of competent jurisdiction determines that the patent provision (Section +3), the indemnity provision (Section 9) or other Section of the License +conflicts with the conditions of the GPLv2, you may retroactively and +prospectively choose to deem waived or otherwise exclude such Section(s) of +the License, but only in their entirety and only with respect to the Combined +Software. + +============================================================================== +Software from third parties included in the LLVM Project: +============================================================================== +The LLVM Project contains third party software which is under different license +terms. All such code will be identified clearly using at least one of two +mechanisms: +1) It will be in a separate directory tree with its own `LICENSE.txt` or + `LICENSE` file at the top containing the specific license and restrictions + which apply to that software, or +2) It will contain specific license and restriction terms at the top of every + file. + +============================================================================== +Legacy LLVM License (https://llvm.org/docs/DeveloperPolicy.html#legacy): +============================================================================== +University of Illinois/NCSA +Open Source License + +Copyright (c) 2003-2019 University of Illinois at Urbana-Champaign. +All rights reserved. + +Developed by: + + LLVM Team + + University of Illinois at Urbana-Champaign + + http://llvm.org + +Permission is hereby granted, free of charge, to any person obtaining a copy of +this software and associated documentation files (the "Software"), to deal with +the Software without restriction, including without limitation the rights to +use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies +of the Software, and to permit persons to whom the Software is furnished to do +so, subject to the following conditions: + + * Redistributions of source code must retain the above copyright notice, + this list of conditions and the following disclaimers. + + * Redistributions in binary form must reproduce the above copyright notice, + this list of conditions and the following disclaimers in the + documentation and/or other materials provided with the distribution. + + * Neither the names of the LLVM Team, University of Illinois at + Urbana-Champaign, nor the names of its contributors may be used to + endorse or promote products derived from this Software without specific + prior written permission. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS +FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +CONTRIBUTORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS WITH THE +SOFTWARE. + +============================================================================= +The GNU C Library is distributed under the GNU Lesser General Public License, +with parts distributed under various other licenses: +============================================================================= + + GNU LESSER GENERAL PUBLIC LICENSE + Version 2.1, February 1999 + + Copyright (C) 1991, 1999 Free Software Foundation, Inc. + 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA + Everyone is permitted to copy and distribute verbatim copies + of this license document, but changing it is not allowed. + +[This is the first released version of the Lesser GPL. It also counts + as the successor of the GNU Library Public License, version 2, hence + the version number 2.1.] + + Preamble + + The licenses for most software are designed to take away your +freedom to share and change it. By contrast, the GNU General Public +Licenses are intended to guarantee your freedom to share and change +free software--to make sure the software is free for all its users. + + This license, the Lesser General Public License, applies to some +specially designated software packages--typically libraries--of the +Free Software Foundation and other authors who decide to use it. You +can use it too, but we suggest you first think carefully about whether +this license or the ordinary General Public License is the better +strategy to use in any particular case, based on the explanations below. + + When we speak of free software, we are referring to freedom of use, +not price. Our General Public Licenses are designed to make sure that +you have the freedom to distribute copies of free software (and charge +for this service if you wish); that you receive source code or can get +it if you want it; that you can change the software and use pieces of +it in new free programs; and that you are informed that you can do +these things. + + To protect your rights, we need to make restrictions that forbid +distributors to deny you these rights or to ask you to surrender these +rights. These restrictions translate to certain responsibilities for +you if you distribute copies of the library or if you modify it. + + For example, if you distribute copies of the library, whether gratis +or for a fee, you must give the recipients all the rights that we gave +you. You must make sure that they, too, receive or can get the source +code. If you link other code with the library, you must provide +complete object files to the recipients, so that they can relink them +with the library after making changes to the library and recompiling +it. And you must show them these terms so they know their rights. + + We protect your rights with a two-step method: (1) we copyright the +library, and (2) we offer you this license, which gives you legal +permission to copy, distribute and/or modify the library. + + To protect each distributor, we want to make it very clear that +there is no warranty for the free library. Also, if the library is +modified by someone else and passed on, the recipients should know +that what they have is not the original version, so that the original +author's reputation will not be affected by problems that might be +introduced by others. + + Finally, software patents pose a constant threat to the existence of +any free program. We wish to make sure that a company cannot +effectively restrict the users of a free program by obtaining a +restrictive license from a patent holder. Therefore, we insist that +any patent license obtained for a version of the library must be +consistent with the full freedom of use specified in this license. + + Most GNU software, including some libraries, is covered by the +ordinary GNU General Public License. This license, the GNU Lesser +General Public License, applies to certain designated libraries, and +is quite different from the ordinary General Public License. We use +this license for certain libraries in order to permit linking those +libraries into non-free programs. + + When a program is linked with a library, whether statically or using +a shared library, the combination of the two is legally speaking a +combined work, a derivative of the original library. The ordinary +General Public License therefore permits such linking only if the +entire combination fits its criteria of freedom. The Lesser General +Public License permits more lax criteria for linking other code with +the library. + + We call this license the "Lesser" General Public License because it +does Less to protect the user's freedom than the ordinary General +Public License. It also provides other free software developers Less +of an advantage over competing non-free programs. These disadvantages +are the reason we use the ordinary General Public License for many +libraries. However, the Lesser license provides advantages in certain +special circumstances. + + For example, on rare occasions, there may be a special need to +encourage the widest possible use of a certain library, so that it becomes +a de-facto standard. To achieve this, non-free programs must be +allowed to use the library. A more frequent case is that a free +library does the same job as widely used non-free libraries. In this +case, there is little to gain by limiting the free library to free +software only, so we use the Lesser General Public License. + + In other cases, permission to use a particular library in non-free +programs enables a greater number of people to use a large body of +free software. For example, permission to use the GNU C Library in +non-free programs enables many more people to use the whole GNU +operating system, as well as its variant, the GNU/Linux operating +system. + + Although the Lesser General Public License is Less protective of the +users' freedom, it does ensure that the user of a program that is +linked with the Library has the freedom and the wherewithal to run +that program using a modified version of the Library. + + The precise terms and conditions for copying, distribution and +modification follow. Pay close attention to the difference between a +"work based on the library" and a "work that uses the library". The +former contains code derived from the library, whereas the latter must +be combined with the library in order to run. + + GNU LESSER GENERAL PUBLIC LICENSE + TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION + + 0. This License Agreement applies to any software library or other +program which contains a notice placed by the copyright holder or +other authorized party saying it may be distributed under the terms of +this Lesser General Public License (also called "this License"). +Each licensee is addressed as "you". + + A "library" means a collection of software functions and/or data +prepared so as to be conveniently linked with application programs +(which use some of those functions and data) to form executables. + + The "Library", below, refers to any such software library or work +which has been distributed under these terms. A "work based on the +Library" means either the Library or any derivative work under +copyright law: that is to say, a work containing the Library or a +portion of it, either verbatim or with modifications and/or translated +straightforwardly into another language. (Hereinafter, translation is +included without limitation in the term "modification".) + + "Source code" for a work means the preferred form of the work for +making modifications to it. For a library, complete source code means +all the source code for all modules it contains, plus any associated +interface definition files, plus the scripts used to control compilation +and installation of the library. + + Activities other than copying, distribution and modification are not +covered by this License; they are outside its scope. The act of +running a program using the Library is not restricted, and output from +such a program is covered only if its contents constitute a work based +on the Library (independent of the use of the Library in a tool for +writing it). Whether that is true depends on what the Library does +and what the program that uses the Library does. + + 1. You may copy and distribute verbatim copies of the Library's +complete source code as you receive it, in any medium, provided that +you conspicuously and appropriately publish on each copy an +appropriate copyright notice and disclaimer of warranty; keep intact +all the notices that refer to this License and to the absence of any +warranty; and distribute a copy of this License along with the +Library. + + You may charge a fee for the physical act of transferring a copy, +and you may at your option offer warranty protection in exchange for a +fee. + + 2. You may modify your copy or copies of the Library or any portion +of it, thus forming a work based on the Library, and copy and +distribute such modifications or work under the terms of Section 1 +above, provided that you also meet all of these conditions: + + a) The modified work must itself be a software library. + + b) You must cause the files modified to carry prominent notices + stating that you changed the files and the date of any change. + + c) You must cause the whole of the work to be licensed at no + charge to all third parties under the terms of this License. + + d) If a facility in the modified Library refers to a function or a + table of data to be supplied by an application program that uses + the facility, other than as an argument passed when the facility + is invoked, then you must make a good faith effort to ensure that, + in the event an application does not supply such function or + table, the facility still operates, and performs whatever part of + its purpose remains meaningful. + + (For example, a function in a library to compute square roots has + a purpose that is entirely well-defined independent of the + application. Therefore, Subsection 2d requires that any + application-supplied function or table used by this function must + be optional: if the application does not supply it, the square + root function must still compute square roots.) + +These requirements apply to the modified work as a whole. If +identifiable sections of that work are not derived from the Library, +and can be reasonably considered independent and separate works in +themselves, then this License, and its terms, do not apply to those +sections when you distribute them as separate works. But when you +distribute the same sections as part of a whole which is a work based +on the Library, the distribution of the whole must be on the terms of +this License, whose permissions for other licensees extend to the +entire whole, and thus to each and every part regardless of who wrote +it. + +Thus, it is not the intent of this section to claim rights or contest +your rights to work written entirely by you; rather, the intent is to +exercise the right to control the distribution of derivative or +collective works based on the Library. + +In addition, mere aggregation of another work not based on the Library +with the Library (or with a work based on the Library) on a volume of +a storage or distribution medium does not bring the other work under +the scope of this License. + + 3. You may opt to apply the terms of the ordinary GNU General Public +License instead of this License to a given copy of the Library. To do +this, you must alter all the notices that refer to this License, so +that they refer to the ordinary GNU General Public License, version 2, +instead of to this License. (If a newer version than version 2 of the +ordinary GNU General Public License has appeared, then you can specify +that version instead if you wish.) Do not make any other change in +these notices. + + Once this change is made in a given copy, it is irreversible for +that copy, so the ordinary GNU General Public License applies to all +subsequent copies and derivative works made from that copy. + + This option is useful when you wish to copy part of the code of +the Library into a program that is not a library. + + 4. You may copy and distribute the Library (or a portion or +derivative of it, under Section 2) in object code or executable form +under the terms of Sections 1 and 2 above provided that you accompany +it with the complete corresponding machine-readable source code, which +must be distributed under the terms of Sections 1 and 2 above on a +medium customarily used for software interchange. + + If distribution of object code is made by offering access to copy +from a designated place, then offering equivalent access to copy the +source code from the same place satisfies the requirement to +distribute the source code, even though third parties are not +compelled to copy the source along with the object code. + + 5. A program that contains no derivative of any portion of the +Library, but is designed to work with the Library by being compiled or +linked with it, is called a "work that uses the Library". Such a +work, in isolation, is not a derivative work of the Library, and +therefore falls outside the scope of this License. + + However, linking a "work that uses the Library" with the Library +creates an executable that is a derivative of the Library (because it +contains portions of the Library), rather than a "work that uses the +library". The executable is therefore covered by this License. +Section 6 states terms for distribution of such executables. + + When a "work that uses the Library" uses material from a header file +that is part of the Library, the object code for the work may be a +derivative work of the Library even though the source code is not. +Whether this is true is especially significant if the work can be +linked without the Library, or if the work is itself a library. The +threshold for this to be true is not precisely defined by law. + + If such an object file uses only numerical parameters, data +structure layouts and accessors, and small macros and small inline +functions (ten lines or less in length), then the use of the object +file is unrestricted, regardless of whether it is legally a derivative +work. (Executables containing this object code plus portions of the +Library will still fall under Section 6.) + + Otherwise, if the work is a derivative of the Library, you may +distribute the object code for the work under the terms of Section 6. +Any executables containing that work also fall under Section 6, +whether or not they are linked directly with the Library itself. + + 6. As an exception to the Sections above, you may also combine or +link a "work that uses the Library" with the Library to produce a +work containing portions of the Library, and distribute that work +under terms of your choice, provided that the terms permit +modification of the work for the customer's own use and reverse +engineering for debugging such modifications. + + You must give prominent notice with each copy of the work that the +Library is used in it and that the Library and its use are covered by +this License. You must supply a copy of this License. If the work +during execution displays copyright notices, you must include the +copyright notice for the Library among them, as well as a reference +directing the user to the copy of this License. Also, you must do one +of these things: + + a) Accompany the work with the complete corresponding + machine-readable source code for the Library including whatever + changes were used in the work (which must be distributed under + Sections 1 and 2 above); and, if the work is an executable linked + with the Library, with the complete machine-readable "work that + uses the Library", as object code and/or source code, so that the + user can modify the Library and then relink to produce a modified + executable containing the modified Library. (It is understood + that the user who changes the contents of definitions files in the + Library will not necessarily be able to recompile the application + to use the modified definitions.) + + b) Use a suitable shared library mechanism for linking with the + Library. A suitable mechanism is one that (1) uses at run time a + copy of the library already present on the user's computer system, + rather than copying library functions into the executable, and (2) + will operate properly with a modified version of the library, if + the user installs one, as long as the modified version is + interface-compatible with the version that the work was made with. + + c) Accompany the work with a written offer, valid for at + least three years, to give the same user the materials + specified in Subsection 6a, above, for a charge no more + than the cost of performing this distribution. + + d) If distribution of the work is made by offering access to copy + from a designated place, offer equivalent access to copy the above + specified materials from the same place. + + e) Verify that the user has already received a copy of these + materials or that you have already sent this user a copy. + + For an executable, the required form of the "work that uses the +Library" must include any data and utility programs needed for +reproducing the executable from it. However, as a special exception, +the materials to be distributed need not include anything that is +normally distributed (in either source or binary form) with the major +components (compiler, kernel, and so on) of the operating system on +which the executable runs, unless that component itself accompanies +the executable. + + It may happen that this requirement contradicts the license +restrictions of other proprietary libraries that do not normally +accompany the operating system. Such a contradiction means you cannot +use both them and the Library together in an executable that you +distribute. + + 7. You may place library facilities that are a work based on the +Library side-by-side in a single library together with other library +facilities not covered by this License, and distribute such a combined +library, provided that the separate distribution of the work based on +the Library and of the other library facilities is otherwise +permitted, and provided that you do these two things: + + a) Accompany the combined library with a copy of the same work + based on the Library, uncombined with any other library + facilities. This must be distributed under the terms of the + Sections above. + + b) Give prominent notice with the combined library of the fact + that part of it is a work based on the Library, and explaining + where to find the accompanying uncombined form of the same work. + + 8. You may not copy, modify, sublicense, link with, or distribute +the Library except as expressly provided under this License. Any +attempt otherwise to copy, modify, sublicense, link with, or +distribute the Library is void, and will automatically terminate your +rights under this License. However, parties who have received copies, +or rights, from you under this License will not have their licenses +terminated so long as such parties remain in full compliance. + + 9. You are not required to accept this License, since you have not +signed it. However, nothing else grants you permission to modify or +distribute the Library or its derivative works. These actions are +prohibited by law if you do not accept this License. Therefore, by +modifying or distributing the Library (or any work based on the +Library), you indicate your acceptance of this License to do so, and +all its terms and conditions for copying, distributing or modifying +the Library or works based on it. + + 10. Each time you redistribute the Library (or any work based on the +Library), the recipient automatically receives a license from the +original licensor to copy, distribute, link with or modify the Library +subject to these terms and conditions. You may not impose any further +restrictions on the recipients' exercise of the rights granted herein. +You are not responsible for enforcing compliance by third parties with +this License. + + 11. If, as a consequence of a court judgment or allegation of patent +infringement or for any other reason (not limited to patent issues), +conditions are imposed on you (whether by court order, agreement or +otherwise) that contradict the conditions of this License, they do not +excuse you from the conditions of this License. If you cannot +distribute so as to satisfy simultaneously your obligations under this +License and any other pertinent obligations, then as a consequence you +may not distribute the Library at all. For example, if a patent +license would not permit royalty-free redistribution of the Library by +all those who receive copies directly or indirectly through you, then +the only way you could satisfy both it and this License would be to +refrain entirely from distribution of the Library. + +If any portion of this section is held invalid or unenforceable under any +particular circumstance, the balance of the section is intended to apply, +and the section as a whole is intended to apply in other circumstances. + +It is not the purpose of this section to induce you to infringe any +patents or other property right claims or to contest validity of any +such claims; this section has the sole purpose of protecting the +integrity of the free software distribution system which is +implemented by public license practices. Many people have made +generous contributions to the wide range of software distributed +through that system in reliance on consistent application of that +system; it is up to the author/donor to decide if he or she is willing +to distribute software through any other system and a licensee cannot +impose that choice. + +This section is intended to make thoroughly clear what is believed to +be a consequence of the rest of this License. + + 12. If the distribution and/or use of the Library is restricted in +certain countries either by patents or by copyrighted interfaces, the +original copyright holder who places the Library under this License may add +an explicit geographical distribution limitation excluding those countries, +so that distribution is permitted only in or among countries not thus +excluded. In such case, this License incorporates the limitation as if +written in the body of this License. + + 13. The Free Software Foundation may publish revised and/or new +versions of the Lesser General Public License from time to time. +Such new versions will be similar in spirit to the present version, +but may differ in detail to address new problems or concerns. + +Each version is given a distinguishing version number. If the Library +specifies a version number of this License which applies to it and +"any later version", you have the option of following the terms and +conditions either of that version or of any later version published by +the Free Software Foundation. If the Library does not specify a +license version number, you may choose any version ever published by +the Free Software Foundation. + + 14. If you wish to incorporate parts of the Library into other free +programs whose distribution conditions are incompatible with these, +write to the author to ask for permission. For software which is +copyrighted by the Free Software Foundation, write to the Free +Software Foundation; we sometimes make exceptions for this. Our +decision will be guided by the two goals of preserving the free status +of all derivatives of our free software and of promoting the sharing +and reuse of software generally. + + NO WARRANTY + + 15. BECAUSE THE LIBRARY IS LICENSED FREE OF CHARGE, THERE IS NO +WARRANTY FOR THE LIBRARY, TO THE EXTENT PERMITTED BY APPLICABLE LAW. +EXCEPT WHEN OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR +OTHER PARTIES PROVIDE THE LIBRARY "AS IS" WITHOUT WARRANTY OF ANY +KIND, EITHER EXPRESSED OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE +IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR +PURPOSE. THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE +LIBRARY IS WITH YOU. SHOULD THE LIBRARY PROVE DEFECTIVE, YOU ASSUME +THE COST OF ALL NECESSARY SERVICING, REPAIR OR CORRECTION. + + 16. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN +WRITING WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY +AND/OR REDISTRIBUTE THE LIBRARY AS PERMITTED ABOVE, BE LIABLE TO YOU +FOR DAMAGES, INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR +CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE THE +LIBRARY (INCLUDING BUT NOT LIMITED TO LOSS OF DATA OR DATA BEING +RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD PARTIES OR A +FAILURE OF THE LIBRARY TO OPERATE WITH ANY OTHER SOFTWARE), EVEN IF +SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH +DAMAGES. + + END OF TERMS AND CONDITIONS + + How to Apply These Terms to Your New Libraries + + If you develop a new library, and you want it to be of the greatest +possible use to the public, we recommend making it free software that +everyone can redistribute and change. You can do so by permitting +redistribution under these terms (or, alternatively, under the terms of the +ordinary General Public License). + + To apply these terms, attach the following notices to the library. It is +safest to attach them to the start of each source file to most effectively +convey the exclusion of warranty; and each file should have at least the +"copyright" line and a pointer to where the full notice is found. + + + Copyright (C) + + This library is free software; you can redistribute it and/or + modify it under the terms of the GNU Lesser General Public + License as published by the Free Software Foundation; either + version 2.1 of the License, or (at your option) any later version. + + This library is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU + Lesser General Public License for more details. + + You should have received a copy of the GNU Lesser General Public + License along with this library; if not, write to the Free Software + Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA + +Also add information on how to contact you by electronic and paper mail. + +You should also get your employer (if you work as a programmer) or your +school, if any, to sign a "copyright disclaimer" for the library, if +necessary. Here is a sample; alter the names: + + Yoyodyne, Inc., hereby disclaims all copyright interest in the + library `Frob' (a library for tweaking knobs) written by James Random Hacker. + + , 1 April 1990 + Ty Coon, President of Vice + +That's all there is to it! + +All code incorporated from 4.4 BSD is distributed under the following +license: + +Copyright (C) 1991 Regents of the University of California. +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions +are met: + +1. Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. +2. Redistributions in binary form must reproduce the above copyright + notice, this list of conditions and the following disclaimer in the + documentation and/or other materials provided with the distribution. +3. [This condition was removed.] +4. Neither the name of the University nor the names of its contributors + may be used to endorse or promote products derived from this software + without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE REGENTS AND CONTRIBUTORS ``AS IS'' AND +ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE +IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE +ARE DISCLAIMED. IN NO EVENT SHALL THE REGENTS OR CONTRIBUTORS BE LIABLE +FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL +DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS +OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) +HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT +LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY +OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF +SUCH DAMAGE. + +The DNS resolver code, taken from BIND 4.9.5, is copyrighted by UC +Berkeley, by Digital Equipment Corporation and by Internet Software +Consortium. The DEC portions are under the following license: + +Portions Copyright (C) 1993 by Digital Equipment Corporation. + +Permission to use, copy, modify, and distribute this software for any +purpose with or without fee is hereby granted, provided that the above +copyright notice and this permission notice appear in all copies, and +that the name of Digital Equipment Corporation not be used in +advertising or publicity pertaining to distribution of the document or +software without specific, written prior permission. + +THE SOFTWARE IS PROVIDED ``AS IS'' AND DIGITAL EQUIPMENT CORP. +DISCLAIMS ALL WARRANTIES WITH REGARD TO THIS SOFTWARE, INCLUDING ALL +IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL +DIGITAL EQUIPMENT CORPORATION BE LIABLE FOR ANY SPECIAL, DIRECT, +INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING +FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN ACTION OF CONTRACT, +NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION +WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. + +The ISC portions are under the following license: + +Portions Copyright (c) 1996-1999 by Internet Software Consortium. + +Permission to use, copy, modify, and distribute this software for any +purpose with or without fee is hereby granted, provided that the above +copyright notice and this permission notice appear in all copies. + +THE SOFTWARE IS PROVIDED "AS IS" AND INTERNET SOFTWARE CONSORTIUM DISCLAIMS +ALL WARRANTIES WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES +OF MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL INTERNET SOFTWARE +CONSORTIUM BE LIABLE FOR ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL +DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR +PROFITS, WHETHER IN AN ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS +ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS +SOFTWARE. + +The Sun RPC support (from rpcsrc-4.0) is covered by the following +license: + +Copyright (c) 2010, Oracle America, Inc. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are +met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials + provided with the distribution. + * Neither the name of the "Oracle America, Inc." nor the names of its + contributors may be used to endorse or promote products derived + from this software without specific prior written permission. + + THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS + "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT + LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS + FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE + COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, + INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE + GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS + INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, + WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING + NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + + +The following CMU license covers some of the support code for Mach, +derived from Mach 3.0: + +Mach Operating System +Copyright (C) 1991,1990,1989 Carnegie Mellon University +All Rights Reserved. + +Permission to use, copy, modify and distribute this software and its +documentation is hereby granted, provided that both the copyright +notice and this permission notice appear in all copies of the +software, derivative works or modified versions, and any portions +thereof, and that both notices appear in supporting documentation. + +CARNEGIE MELLON ALLOWS FREE USE OF THIS SOFTWARE IN ITS ``AS IS'' +CONDITION. CARNEGIE MELLON DISCLAIMS ANY LIABILITY OF ANY KIND FOR +ANY DAMAGES WHATSOEVER RESULTING FROM THE USE OF THIS SOFTWARE. + +Carnegie Mellon requests users of this software to return to + + Software Distribution Coordinator + School of Computer Science + Carnegie Mellon University + Pittsburgh PA 15213-3890 + +or Software.Distribution@CS.CMU.EDU any improvements or +extensions that they make and grant Carnegie Mellon the rights to +redistribute these changes. + +The file if_ppp.h is under the following CMU license: + + Redistribution and use in source and binary forms, with or without + modification, are permitted provided that the following conditions + are met: + 1. Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + 2. Redistributions in binary form must reproduce the above copyright + notice, this list of conditions and the following disclaimer in the + documentation and/or other materials provided with the distribution. + 3. Neither the name of the University nor the names of its contributors + may be used to endorse or promote products derived from this software + without specific prior written permission. + + THIS SOFTWARE IS PROVIDED BY CARNEGIE MELLON UNIVERSITY AND + CONTRIBUTORS ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, + INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF + MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. + IN NO EVENT SHALL THE UNIVERSITY OR CONTRIBUTORS BE LIABLE FOR ANY + DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE + GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS + INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER + IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR + OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN + IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + +The following license covers the files from Intel's "Highly Optimized +Mathematical Functions for Itanium" collection: + +Intel License Agreement + +Copyright (c) 2000, Intel Corporation + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are +met: + +* Redistributions of source code must retain the above copyright +notice, this list of conditions and the following disclaimer. + +* Redistributions in binary form must reproduce the above copyright +notice, this list of conditions and the following disclaimer in the +documentation and/or other materials provided with the distribution. + +* The name of Intel Corporation may not be used to endorse or promote +products derived from this software without specific prior written +permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL INTEL OR +CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + +The files inet/getnameinfo.c and sysdeps/posix/getaddrinfo.c are copyright +(C) by Craig Metz and are distributed under the following license: + +/* The Inner Net License, Version 2.00 + + The author(s) grant permission for redistribution and use in source and +binary forms, with or without modification, of the software and documentation +provided that the following conditions are met: + +0. If you receive a version of the software that is specifically labelled + as not being for redistribution (check the version message and/or README), + you are not permitted to redistribute that version of the software in any + way or form. +1. All terms of the all other applicable copyrights and licenses must be + followed. +2. Redistributions of source code must retain the authors' copyright + notice(s), this list of conditions, and the following disclaimer. +3. Redistributions in binary form must reproduce the authors' copyright + notice(s), this list of conditions, and the following disclaimer in the + documentation and/or other materials provided with the distribution. +4. [The copyright holder has authorized the removal of this clause.] +5. Neither the name(s) of the author(s) nor the names of its contributors + may be used to endorse or promote products derived from this software + without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY ITS AUTHORS AND CONTRIBUTORS ``AS IS'' AND ANY +EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED +WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE +DISCLAIMED. IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE FOR ANY +DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES +(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; +LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON +ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + + If these license terms cause you a real problem, contact the author. */ + +The file sunrpc/des_impl.c is copyright Eric Young: + +Copyright (C) 1992 Eric Young +Collected from libdes and modified for SECURE RPC by Martin Kuck 1994 +This file is distributed under the terms of the GNU Lesser General +Public License, version 2.1 or later - see the file COPYING.LIB for details. +If you did not receive a copy of the license with this program, please +see to obtain a copy. + +The file inet/rcmd.c is under a UCB copyright and the following: + +Copyright (C) 1998 WIDE Project. +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions +are met: +1. Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. +2. Redistributions in binary form must reproduce the above copyright + notice, this list of conditions and the following disclaimer in the + documentation and/or other materials provided with the distribution. +3. Neither the name of the project nor the names of its contributors + may be used to endorse or promote products derived from this software + without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE PROJECT AND CONTRIBUTORS ``AS IS'' AND +ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE +IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE +ARE DISCLAIMED. IN NO EVENT SHALL THE PROJECT OR CONTRIBUTORS BE LIABLE +FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL +DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS +OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) +HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT +LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY +OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF +SUCH DAMAGE. + +The file posix/runtests.c is copyright Tom Lord: + +Copyright 1995 by Tom Lord + + All Rights Reserved + +Permission to use, copy, modify, and distribute this software and its +documentation for any purpose and without fee is hereby granted, +provided that the above copyright notice appear in all copies and that +both that copyright notice and this permission notice appear in +supporting documentation, and that the name of the copyright holder not be +used in advertising or publicity pertaining to distribution of the +software without specific, written prior permission. + +Tom Lord DISCLAIMS ALL WARRANTIES WITH REGARD TO THIS SOFTWARE, +INCLUDING ALL IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS, IN NO +EVENT SHALL TOM LORD BE LIABLE FOR ANY SPECIAL, INDIRECT OR +CONSEQUENTIAL DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM LOSS OF +USE, DATA OR PROFITS, WHETHER IN AN ACTION OF CONTRACT, NEGLIGENCE OR +OTHER TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR +PERFORMANCE OF THIS SOFTWARE. + +The posix/rxspencer tests are copyright Henry Spencer: + +Copyright 1992, 1993, 1994, 1997 Henry Spencer. All rights reserved. +This software is not subject to any license of the American Telephone +and Telegraph Company or of the Regents of the University of California. + +Permission is granted to anyone to use this software for any purpose on +any computer system, and to alter it and redistribute it, subject +to the following restrictions: + +1. The author is not responsible for the consequences of use of this + software, no matter how awful, even if they arise from flaws in it. + +2. The origin of this software must not be misrepresented, either by + explicit claim or by omission. Since few users ever read sources, + credits must appear in the documentation. + +3. Altered versions must be plainly marked as such, and must not be + misrepresented as being the original software. Since few users + ever read sources, credits must appear in the documentation. + +4. This notice may not be removed or altered. + +The file posix/PCRE.tests is copyright University of Cambridge: + +Copyright (c) 1997-2003 University of Cambridge + +Permission is granted to anyone to use this software for any purpose on any +computer system, and to redistribute it freely, subject to the following +restrictions: + +1. This software is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. + +2. The origin of this software must not be misrepresented, either by + explicit claim or by omission. In practice, this means that if you use + PCRE in software that you distribute to others, commercially or + otherwise, you must put a sentence like this + + Regular expression support is provided by the PCRE library package, + which is open source software, written by Philip Hazel, and copyright + by the University of Cambridge, England. + + somewhere reasonably visible in your documentation and in any relevant + files or online help data or similar. A reference to the ftp site for + the source, that is, to + + ftp://ftp.csx.cam.ac.uk/pub/software/programming/pcre/ + + should also be given in the documentation. However, this condition is not + intended to apply to whole chains of software. If package A includes PCRE, + it must acknowledge it, but if package B is software that includes package + A, the condition is not imposed on package B (unless it uses PCRE + independently). + +3. Altered versions must be plainly marked as such, and must not be + misrepresented as being the original software. + +4. If PCRE is embedded in any software that is released under the GNU + General Purpose Licence (GPL), or Lesser General Purpose Licence (LGPL), + then the terms of that licence shall supersede any condition above with + which it is incompatible. + +Files from Sun fdlibm are copyright Sun Microsystems, Inc.: + +Copyright (C) 1993 by Sun Microsystems, Inc. All rights reserved. + +Developed at SunPro, a Sun Microsystems, Inc. business. +Permission to use, copy, modify, and distribute this +software is freely granted, provided that this notice +is preserved. + +Various long double libm functions are copyright Stephen L. Moshier: + +Copyright 2001 by Stephen L. Moshier + + This library is free software; you can redistribute it and/or + modify it under the terms of the GNU Lesser General Public + License as published by the Free Software Foundation; either + version 2.1 of the License, or (at your option) any later version. + + This library is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU + Lesser General Public License for more details. + + You should have received a copy of the GNU Lesser General Public + License along with this library; if not, see + . */ From b72b04e25b48aa4e42661ea39dc64c6b7bfd63f0 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 5 Nov 2021 17:35:03 +0100 Subject: [PATCH 13/27] chore: update lean-llvm --- .github/workflows/ci.yml | 2 +- script/prepare-llvm-linux.sh | 6 ++---- 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index b42d18b674bd..46147af34bfc 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -27,7 +27,7 @@ jobs: os: ubuntu-latest release: true shell: nix-shell --arg pkgs "import (fetchTarball \"channel:nixos-19.03\") {{}}" --argstr llvmPackages latest --run "bash -euxo pipefail {0}" - llvm-url: https://github.com/leanprover/lean-llvm/releases/download/13.0.0/lean-llvm.tar.zst + llvm-url: https://github.com/leanprover/lean-llvm/releases/download/13.0.0/lean-llvm-x86_64-linux-gnu.tar.zst - name: Linux os: ubuntu-latest check-stage3: true diff --git a/script/prepare-llvm-linux.sh b/script/prepare-llvm-linux.sh index e1b943c580a2..8c2afb9195f6 100755 --- a/script/prepare-llvm-linux.sh +++ b/script/prepare-llvm-linux.sh @@ -17,9 +17,7 @@ $CP $(realpath llvm/bin/clang) stage1/bin/clang $CP llvm/bin/{lld,ld.lld} stage1/bin/ # dependencies of the above $CP llvm/lib/lib{clang-cpp,LLVM}*.so* stage1/lib/ -# clang can't even find its own deps in a standard build? ¯\_(ツ)_/¯ -ln llvm/lib/x86*/* llvm/lib -# ...nor are the rpaths sensible +# fix up some rpaths(...?) patchelf --set-rpath '$ORIGIN' llvm/lib/libc++.so.* # lean.h dependencies $CP llvm/lib/clang/*/include/{std*,__std*,limits}.h stage1/include/clang @@ -27,7 +25,7 @@ $CP llvm/lib/clang/*/include/{std*,__std*,limits}.h stage1/include/clang $CP $GLIBC/lib/crt* llvm/lib/ $CP $GLIBC/lib/crt* stage1/lib/ # runtime -(cd llvm; $CP --parents lib/clang/*/lib/*/{*crt{begin,end}.o,libclang_rt.builtins*} ../stage1) +(cd llvm; $CP --parents lib/clang/*/lib/*/{clang_rt.*.o,libclang_rt.builtins*} ../stage1) $CP llvm/lib/lib{c++,c++abi,unwind}.* $GMP/lib/libgmp.a stage1/lib/ # glibc: use for linking (so Lean programs don't embed newer symbol versions), but not for running (because libc.so, librt.so, and ld.so must be compatible)! $CP $GLIBC/lib/libc_nonshared.a stage1/lib/glibc From 4a8229b2de5357cc7860dde71722abb850e0b387 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 5 Nov 2021 16:47:19 +0100 Subject: [PATCH 14/27] chore: split LICENSE again --- LICENSE | 1172 +------------------------------------------------------ 1 file changed, 1 insertion(+), 1171 deletions(-) diff --git a/LICENSE b/LICENSE index c0f2b9d8d7d7..6ff2b2040c91 100644 --- a/LICENSE +++ b/LICENSE @@ -1,4 +1,5 @@ ============================================================================== +See LICENSES for licenses of redistributed projects. The Lean project is under the Apache License 2.0: ============================================================================== @@ -72,1174 +73,3 @@ In no event and under no legal theory, whether in tort (including negligence), c 9. Accepting Warranty or Additional Liability. While redistributing the Work or Derivative Works thereof, You may choose to offer, and charge a fee for, acceptance of support, warranty, indemnity, or other liability obligations and/or rights consistent with this License. However, in accepting such obligations, You may act only on Your own behalf and on Your sole responsibility, not on behalf of any other Contributor, and only if You agree to indemnify, defend, and hold each Contributor harmless for any liability incurred by, or claims asserted against, such Contributor by reason of your accepting any such warranty or additional liability. - -============================================================================== -The LLVM Project is under the Apache License v2.0 with LLVM Exceptions: -============================================================================== - - Apache License - Version 2.0, January 2004 - http://www.apache.org/licenses/ - - TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION - - 1. Definitions. - - "License" shall mean the terms and conditions for use, reproduction, - and distribution as defined by Sections 1 through 9 of this document. - - "Licensor" shall mean the copyright owner or entity authorized by - the copyright owner that is granting the License. - - "Legal Entity" shall mean the union of the acting entity and all - other entities that control, are controlled by, or are under common - control with that entity. For the purposes of this definition, - "control" means (i) the power, direct or indirect, to cause the - direction or management of such entity, whether by contract or - otherwise, or (ii) ownership of fifty percent (50%) or more of the - outstanding shares, or (iii) beneficial ownership of such entity. - - "You" (or "Your") shall mean an individual or Legal Entity - exercising permissions granted by this License. - - "Source" form shall mean the preferred form for making modifications, - including but not limited to software source code, documentation - source, and configuration files. - - "Object" form shall mean any form resulting from mechanical - transformation or translation of a Source form, including but - not limited to compiled object code, generated documentation, - and conversions to other media types. - - "Work" shall mean the work of authorship, whether in Source or - Object form, made available under the License, as indicated by a - copyright notice that is included in or attached to the work - (an example is provided in the Appendix below). - - "Derivative Works" shall mean any work, whether in Source or Object - form, that is based on (or derived from) the Work and for which the - editorial revisions, annotations, elaborations, or other modifications - represent, as a whole, an original work of authorship. For the purposes - of this License, Derivative Works shall not include works that remain - separable from, or merely link (or bind by name) to the interfaces of, - the Work and Derivative Works thereof. - - "Contribution" shall mean any work of authorship, including - the original version of the Work and any modifications or additions - to that Work or Derivative Works thereof, that is intentionally - submitted to Licensor for inclusion in the Work by the copyright owner - or by an individual or Legal Entity authorized to submit on behalf of - the copyright owner. For the purposes of this definition, "submitted" - means any form of electronic, verbal, or written communication sent - to the Licensor or its representatives, including but not limited to - communication on electronic mailing lists, source code control systems, - and issue tracking systems that are managed by, or on behalf of, the - Licensor for the purpose of discussing and improving the Work, but - excluding communication that is conspicuously marked or otherwise - designated in writing by the copyright owner as "Not a Contribution." - - "Contributor" shall mean Licensor and any individual or Legal Entity - on behalf of whom a Contribution has been received by Licensor and - subsequently incorporated within the Work. - - 2. Grant of Copyright License. Subject to the terms and conditions of - this License, each Contributor hereby grants to You a perpetual, - worldwide, non-exclusive, no-charge, royalty-free, irrevocable - copyright license to reproduce, prepare Derivative Works of, - publicly display, publicly perform, sublicense, and distribute the - Work and such Derivative Works in Source or Object form. - - 3. Grant of Patent License. Subject to the terms and conditions of - this License, each Contributor hereby grants to You a perpetual, - worldwide, non-exclusive, no-charge, royalty-free, irrevocable - (except as stated in this section) patent license to make, have made, - use, offer to sell, sell, import, and otherwise transfer the Work, - where such license applies only to those patent claims licensable - by such Contributor that are necessarily infringed by their - Contribution(s) alone or by combination of their Contribution(s) - with the Work to which such Contribution(s) was submitted. If You - institute patent litigation against any entity (including a - cross-claim or counterclaim in a lawsuit) alleging that the Work - or a Contribution incorporated within the Work constitutes direct - or contributory patent infringement, then any patent licenses - granted to You under this License for that Work shall terminate - as of the date such litigation is filed. - - 4. Redistribution. You may reproduce and distribute copies of the - Work or Derivative Works thereof in any medium, with or without - modifications, and in Source or Object form, provided that You - meet the following conditions: - - (a) You must give any other recipients of the Work or - Derivative Works a copy of this License; and - - (b) You must cause any modified files to carry prominent notices - stating that You changed the files; and - - (c) You must retain, in the Source form of any Derivative Works - that You distribute, all copyright, patent, trademark, and - attribution notices from the Source form of the Work, - excluding those notices that do not pertain to any part of - the Derivative Works; and - - (d) If the Work includes a "NOTICE" text file as part of its - distribution, then any Derivative Works that You distribute must - include a readable copy of the attribution notices contained - within such NOTICE file, excluding those notices that do not - pertain to any part of the Derivative Works, in at least one - of the following places: within a NOTICE text file distributed - as part of the Derivative Works; within the Source form or - documentation, if provided along with the Derivative Works; or, - within a display generated by the Derivative Works, if and - wherever such third-party notices normally appear. The contents - of the NOTICE file are for informational purposes only and - do not modify the License. You may add Your own attribution - notices within Derivative Works that You distribute, alongside - or as an addendum to the NOTICE text from the Work, provided - that such additional attribution notices cannot be construed - as modifying the License. - - You may add Your own copyright statement to Your modifications and - may provide additional or different license terms and conditions - for use, reproduction, or distribution of Your modifications, or - for any such Derivative Works as a whole, provided Your use, - reproduction, and distribution of the Work otherwise complies with - the conditions stated in this License. - - 5. Submission of Contributions. Unless You explicitly state otherwise, - any Contribution intentionally submitted for inclusion in the Work - by You to the Licensor shall be under the terms and conditions of - this License, without any additional terms or conditions. - Notwithstanding the above, nothing herein shall supersede or modify - the terms of any separate license agreement you may have executed - with Licensor regarding such Contributions. - - 6. Trademarks. This License does not grant permission to use the trade - names, trademarks, service marks, or product names of the Licensor, - except as required for reasonable and customary use in describing the - origin of the Work and reproducing the content of the NOTICE file. - - 7. Disclaimer of Warranty. Unless required by applicable law or - agreed to in writing, Licensor provides the Work (and each - Contributor provides its Contributions) on an "AS IS" BASIS, - WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or - implied, including, without limitation, any warranties or conditions - of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A - PARTICULAR PURPOSE. You are solely responsible for determining the - appropriateness of using or redistributing the Work and assume any - risks associated with Your exercise of permissions under this License. - - 8. Limitation of Liability. In no event and under no legal theory, - whether in tort (including negligence), contract, or otherwise, - unless required by applicable law (such as deliberate and grossly - negligent acts) or agreed to in writing, shall any Contributor be - liable to You for damages, including any direct, indirect, special, - incidental, or consequential damages of any character arising as a - result of this License or out of the use or inability to use the - Work (including but not limited to damages for loss of goodwill, - work stoppage, computer failure or malfunction, or any and all - other commercial damages or losses), even if such Contributor - has been advised of the possibility of such damages. - - 9. Accepting Warranty or Additional Liability. While redistributing - the Work or Derivative Works thereof, You may choose to offer, - and charge a fee for, acceptance of support, warranty, indemnity, - or other liability obligations and/or rights consistent with this - License. However, in accepting such obligations, You may act only - on Your own behalf and on Your sole responsibility, not on behalf - of any other Contributor, and only if You agree to indemnify, - defend, and hold each Contributor harmless for any liability - incurred by, or claims asserted against, such Contributor by reason - of your accepting any such warranty or additional liability. - - END OF TERMS AND CONDITIONS - - APPENDIX: How to apply the Apache License to your work. - - To apply the Apache License to your work, attach the following - boilerplate notice, with the fields enclosed by brackets "[]" - replaced with your own identifying information. (Don't include - the brackets!) The text should be enclosed in the appropriate - comment syntax for the file format. We also recommend that a - file or class name and description of purpose be included on the - same "printed page" as the copyright notice for easier - identification within third-party archives. - - Copyright [yyyy] [name of copyright owner] - - Licensed under the Apache License, Version 2.0 (the "License"); - you may not use this file except in compliance with the License. - You may obtain a copy of the License at - - http://www.apache.org/licenses/LICENSE-2.0 - - Unless required by applicable law or agreed to in writing, software - distributed under the License is distributed on an "AS IS" BASIS, - WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. - See the License for the specific language governing permissions and - limitations under the License. - - ----- LLVM Exceptions to the Apache 2.0 License ---- - -As an exception, if, as a result of your compiling your source code, portions -of this Software are embedded into an Object form of such source code, you -may redistribute such embedded portions in such Object form without complying -with the conditions of Sections 4(a), 4(b) and 4(d) of the License. - -In addition, if you combine or link compiled forms of this Software with -software that is licensed under the GPLv2 ("Combined Software") and if a -court of competent jurisdiction determines that the patent provision (Section -3), the indemnity provision (Section 9) or other Section of the License -conflicts with the conditions of the GPLv2, you may retroactively and -prospectively choose to deem waived or otherwise exclude such Section(s) of -the License, but only in their entirety and only with respect to the Combined -Software. - -============================================================================== -Software from third parties included in the LLVM Project: -============================================================================== -The LLVM Project contains third party software which is under different license -terms. All such code will be identified clearly using at least one of two -mechanisms: -1) It will be in a separate directory tree with its own `LICENSE.txt` or - `LICENSE` file at the top containing the specific license and restrictions - which apply to that software, or -2) It will contain specific license and restriction terms at the top of every - file. - -============================================================================== -Legacy LLVM License (https://llvm.org/docs/DeveloperPolicy.html#legacy): -============================================================================== -University of Illinois/NCSA -Open Source License - -Copyright (c) 2003-2019 University of Illinois at Urbana-Champaign. -All rights reserved. - -Developed by: - - LLVM Team - - University of Illinois at Urbana-Champaign - - http://llvm.org - -Permission is hereby granted, free of charge, to any person obtaining a copy of -this software and associated documentation files (the "Software"), to deal with -the Software without restriction, including without limitation the rights to -use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies -of the Software, and to permit persons to whom the Software is furnished to do -so, subject to the following conditions: - - * Redistributions of source code must retain the above copyright notice, - this list of conditions and the following disclaimers. - - * Redistributions in binary form must reproduce the above copyright notice, - this list of conditions and the following disclaimers in the - documentation and/or other materials provided with the distribution. - - * Neither the names of the LLVM Team, University of Illinois at - Urbana-Champaign, nor the names of its contributors may be used to - endorse or promote products derived from this Software without specific - prior written permission. - -THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR -IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS -FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE -CONTRIBUTORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER -LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, -OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS WITH THE -SOFTWARE. - -============================================================================= -The GNU C Library is distributed under the GNU Lesser General Public License, -with parts distributed under various other licenses: -============================================================================= - - GNU LESSER GENERAL PUBLIC LICENSE - Version 2.1, February 1999 - - Copyright (C) 1991, 1999 Free Software Foundation, Inc. - 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA - Everyone is permitted to copy and distribute verbatim copies - of this license document, but changing it is not allowed. - -[This is the first released version of the Lesser GPL. It also counts - as the successor of the GNU Library Public License, version 2, hence - the version number 2.1.] - - Preamble - - The licenses for most software are designed to take away your -freedom to share and change it. By contrast, the GNU General Public -Licenses are intended to guarantee your freedom to share and change -free software--to make sure the software is free for all its users. - - This license, the Lesser General Public License, applies to some -specially designated software packages--typically libraries--of the -Free Software Foundation and other authors who decide to use it. You -can use it too, but we suggest you first think carefully about whether -this license or the ordinary General Public License is the better -strategy to use in any particular case, based on the explanations below. - - When we speak of free software, we are referring to freedom of use, -not price. Our General Public Licenses are designed to make sure that -you have the freedom to distribute copies of free software (and charge -for this service if you wish); that you receive source code or can get -it if you want it; that you can change the software and use pieces of -it in new free programs; and that you are informed that you can do -these things. - - To protect your rights, we need to make restrictions that forbid -distributors to deny you these rights or to ask you to surrender these -rights. These restrictions translate to certain responsibilities for -you if you distribute copies of the library or if you modify it. - - For example, if you distribute copies of the library, whether gratis -or for a fee, you must give the recipients all the rights that we gave -you. You must make sure that they, too, receive or can get the source -code. If you link other code with the library, you must provide -complete object files to the recipients, so that they can relink them -with the library after making changes to the library and recompiling -it. And you must show them these terms so they know their rights. - - We protect your rights with a two-step method: (1) we copyright the -library, and (2) we offer you this license, which gives you legal -permission to copy, distribute and/or modify the library. - - To protect each distributor, we want to make it very clear that -there is no warranty for the free library. Also, if the library is -modified by someone else and passed on, the recipients should know -that what they have is not the original version, so that the original -author's reputation will not be affected by problems that might be -introduced by others. - - Finally, software patents pose a constant threat to the existence of -any free program. We wish to make sure that a company cannot -effectively restrict the users of a free program by obtaining a -restrictive license from a patent holder. Therefore, we insist that -any patent license obtained for a version of the library must be -consistent with the full freedom of use specified in this license. - - Most GNU software, including some libraries, is covered by the -ordinary GNU General Public License. This license, the GNU Lesser -General Public License, applies to certain designated libraries, and -is quite different from the ordinary General Public License. We use -this license for certain libraries in order to permit linking those -libraries into non-free programs. - - When a program is linked with a library, whether statically or using -a shared library, the combination of the two is legally speaking a -combined work, a derivative of the original library. The ordinary -General Public License therefore permits such linking only if the -entire combination fits its criteria of freedom. The Lesser General -Public License permits more lax criteria for linking other code with -the library. - - We call this license the "Lesser" General Public License because it -does Less to protect the user's freedom than the ordinary General -Public License. It also provides other free software developers Less -of an advantage over competing non-free programs. These disadvantages -are the reason we use the ordinary General Public License for many -libraries. However, the Lesser license provides advantages in certain -special circumstances. - - For example, on rare occasions, there may be a special need to -encourage the widest possible use of a certain library, so that it becomes -a de-facto standard. To achieve this, non-free programs must be -allowed to use the library. A more frequent case is that a free -library does the same job as widely used non-free libraries. In this -case, there is little to gain by limiting the free library to free -software only, so we use the Lesser General Public License. - - In other cases, permission to use a particular library in non-free -programs enables a greater number of people to use a large body of -free software. For example, permission to use the GNU C Library in -non-free programs enables many more people to use the whole GNU -operating system, as well as its variant, the GNU/Linux operating -system. - - Although the Lesser General Public License is Less protective of the -users' freedom, it does ensure that the user of a program that is -linked with the Library has the freedom and the wherewithal to run -that program using a modified version of the Library. - - The precise terms and conditions for copying, distribution and -modification follow. Pay close attention to the difference between a -"work based on the library" and a "work that uses the library". The -former contains code derived from the library, whereas the latter must -be combined with the library in order to run. - - GNU LESSER GENERAL PUBLIC LICENSE - TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION - - 0. This License Agreement applies to any software library or other -program which contains a notice placed by the copyright holder or -other authorized party saying it may be distributed under the terms of -this Lesser General Public License (also called "this License"). -Each licensee is addressed as "you". - - A "library" means a collection of software functions and/or data -prepared so as to be conveniently linked with application programs -(which use some of those functions and data) to form executables. - - The "Library", below, refers to any such software library or work -which has been distributed under these terms. A "work based on the -Library" means either the Library or any derivative work under -copyright law: that is to say, a work containing the Library or a -portion of it, either verbatim or with modifications and/or translated -straightforwardly into another language. (Hereinafter, translation is -included without limitation in the term "modification".) - - "Source code" for a work means the preferred form of the work for -making modifications to it. For a library, complete source code means -all the source code for all modules it contains, plus any associated -interface definition files, plus the scripts used to control compilation -and installation of the library. - - Activities other than copying, distribution and modification are not -covered by this License; they are outside its scope. The act of -running a program using the Library is not restricted, and output from -such a program is covered only if its contents constitute a work based -on the Library (independent of the use of the Library in a tool for -writing it). Whether that is true depends on what the Library does -and what the program that uses the Library does. - - 1. You may copy and distribute verbatim copies of the Library's -complete source code as you receive it, in any medium, provided that -you conspicuously and appropriately publish on each copy an -appropriate copyright notice and disclaimer of warranty; keep intact -all the notices that refer to this License and to the absence of any -warranty; and distribute a copy of this License along with the -Library. - - You may charge a fee for the physical act of transferring a copy, -and you may at your option offer warranty protection in exchange for a -fee. - - 2. You may modify your copy or copies of the Library or any portion -of it, thus forming a work based on the Library, and copy and -distribute such modifications or work under the terms of Section 1 -above, provided that you also meet all of these conditions: - - a) The modified work must itself be a software library. - - b) You must cause the files modified to carry prominent notices - stating that you changed the files and the date of any change. - - c) You must cause the whole of the work to be licensed at no - charge to all third parties under the terms of this License. - - d) If a facility in the modified Library refers to a function or a - table of data to be supplied by an application program that uses - the facility, other than as an argument passed when the facility - is invoked, then you must make a good faith effort to ensure that, - in the event an application does not supply such function or - table, the facility still operates, and performs whatever part of - its purpose remains meaningful. - - (For example, a function in a library to compute square roots has - a purpose that is entirely well-defined independent of the - application. Therefore, Subsection 2d requires that any - application-supplied function or table used by this function must - be optional: if the application does not supply it, the square - root function must still compute square roots.) - -These requirements apply to the modified work as a whole. If -identifiable sections of that work are not derived from the Library, -and can be reasonably considered independent and separate works in -themselves, then this License, and its terms, do not apply to those -sections when you distribute them as separate works. But when you -distribute the same sections as part of a whole which is a work based -on the Library, the distribution of the whole must be on the terms of -this License, whose permissions for other licensees extend to the -entire whole, and thus to each and every part regardless of who wrote -it. - -Thus, it is not the intent of this section to claim rights or contest -your rights to work written entirely by you; rather, the intent is to -exercise the right to control the distribution of derivative or -collective works based on the Library. - -In addition, mere aggregation of another work not based on the Library -with the Library (or with a work based on the Library) on a volume of -a storage or distribution medium does not bring the other work under -the scope of this License. - - 3. You may opt to apply the terms of the ordinary GNU General Public -License instead of this License to a given copy of the Library. To do -this, you must alter all the notices that refer to this License, so -that they refer to the ordinary GNU General Public License, version 2, -instead of to this License. (If a newer version than version 2 of the -ordinary GNU General Public License has appeared, then you can specify -that version instead if you wish.) Do not make any other change in -these notices. - - Once this change is made in a given copy, it is irreversible for -that copy, so the ordinary GNU General Public License applies to all -subsequent copies and derivative works made from that copy. - - This option is useful when you wish to copy part of the code of -the Library into a program that is not a library. - - 4. You may copy and distribute the Library (or a portion or -derivative of it, under Section 2) in object code or executable form -under the terms of Sections 1 and 2 above provided that you accompany -it with the complete corresponding machine-readable source code, which -must be distributed under the terms of Sections 1 and 2 above on a -medium customarily used for software interchange. - - If distribution of object code is made by offering access to copy -from a designated place, then offering equivalent access to copy the -source code from the same place satisfies the requirement to -distribute the source code, even though third parties are not -compelled to copy the source along with the object code. - - 5. A program that contains no derivative of any portion of the -Library, but is designed to work with the Library by being compiled or -linked with it, is called a "work that uses the Library". Such a -work, in isolation, is not a derivative work of the Library, and -therefore falls outside the scope of this License. - - However, linking a "work that uses the Library" with the Library -creates an executable that is a derivative of the Library (because it -contains portions of the Library), rather than a "work that uses the -library". The executable is therefore covered by this License. -Section 6 states terms for distribution of such executables. - - When a "work that uses the Library" uses material from a header file -that is part of the Library, the object code for the work may be a -derivative work of the Library even though the source code is not. -Whether this is true is especially significant if the work can be -linked without the Library, or if the work is itself a library. The -threshold for this to be true is not precisely defined by law. - - If such an object file uses only numerical parameters, data -structure layouts and accessors, and small macros and small inline -functions (ten lines or less in length), then the use of the object -file is unrestricted, regardless of whether it is legally a derivative -work. (Executables containing this object code plus portions of the -Library will still fall under Section 6.) - - Otherwise, if the work is a derivative of the Library, you may -distribute the object code for the work under the terms of Section 6. -Any executables containing that work also fall under Section 6, -whether or not they are linked directly with the Library itself. - - 6. As an exception to the Sections above, you may also combine or -link a "work that uses the Library" with the Library to produce a -work containing portions of the Library, and distribute that work -under terms of your choice, provided that the terms permit -modification of the work for the customer's own use and reverse -engineering for debugging such modifications. - - You must give prominent notice with each copy of the work that the -Library is used in it and that the Library and its use are covered by -this License. You must supply a copy of this License. If the work -during execution displays copyright notices, you must include the -copyright notice for the Library among them, as well as a reference -directing the user to the copy of this License. Also, you must do one -of these things: - - a) Accompany the work with the complete corresponding - machine-readable source code for the Library including whatever - changes were used in the work (which must be distributed under - Sections 1 and 2 above); and, if the work is an executable linked - with the Library, with the complete machine-readable "work that - uses the Library", as object code and/or source code, so that the - user can modify the Library and then relink to produce a modified - executable containing the modified Library. (It is understood - that the user who changes the contents of definitions files in the - Library will not necessarily be able to recompile the application - to use the modified definitions.) - - b) Use a suitable shared library mechanism for linking with the - Library. A suitable mechanism is one that (1) uses at run time a - copy of the library already present on the user's computer system, - rather than copying library functions into the executable, and (2) - will operate properly with a modified version of the library, if - the user installs one, as long as the modified version is - interface-compatible with the version that the work was made with. - - c) Accompany the work with a written offer, valid for at - least three years, to give the same user the materials - specified in Subsection 6a, above, for a charge no more - than the cost of performing this distribution. - - d) If distribution of the work is made by offering access to copy - from a designated place, offer equivalent access to copy the above - specified materials from the same place. - - e) Verify that the user has already received a copy of these - materials or that you have already sent this user a copy. - - For an executable, the required form of the "work that uses the -Library" must include any data and utility programs needed for -reproducing the executable from it. However, as a special exception, -the materials to be distributed need not include anything that is -normally distributed (in either source or binary form) with the major -components (compiler, kernel, and so on) of the operating system on -which the executable runs, unless that component itself accompanies -the executable. - - It may happen that this requirement contradicts the license -restrictions of other proprietary libraries that do not normally -accompany the operating system. Such a contradiction means you cannot -use both them and the Library together in an executable that you -distribute. - - 7. You may place library facilities that are a work based on the -Library side-by-side in a single library together with other library -facilities not covered by this License, and distribute such a combined -library, provided that the separate distribution of the work based on -the Library and of the other library facilities is otherwise -permitted, and provided that you do these two things: - - a) Accompany the combined library with a copy of the same work - based on the Library, uncombined with any other library - facilities. This must be distributed under the terms of the - Sections above. - - b) Give prominent notice with the combined library of the fact - that part of it is a work based on the Library, and explaining - where to find the accompanying uncombined form of the same work. - - 8. You may not copy, modify, sublicense, link with, or distribute -the Library except as expressly provided under this License. Any -attempt otherwise to copy, modify, sublicense, link with, or -distribute the Library is void, and will automatically terminate your -rights under this License. However, parties who have received copies, -or rights, from you under this License will not have their licenses -terminated so long as such parties remain in full compliance. - - 9. You are not required to accept this License, since you have not -signed it. However, nothing else grants you permission to modify or -distribute the Library or its derivative works. These actions are -prohibited by law if you do not accept this License. Therefore, by -modifying or distributing the Library (or any work based on the -Library), you indicate your acceptance of this License to do so, and -all its terms and conditions for copying, distributing or modifying -the Library or works based on it. - - 10. Each time you redistribute the Library (or any work based on the -Library), the recipient automatically receives a license from the -original licensor to copy, distribute, link with or modify the Library -subject to these terms and conditions. You may not impose any further -restrictions on the recipients' exercise of the rights granted herein. -You are not responsible for enforcing compliance by third parties with -this License. - - 11. If, as a consequence of a court judgment or allegation of patent -infringement or for any other reason (not limited to patent issues), -conditions are imposed on you (whether by court order, agreement or -otherwise) that contradict the conditions of this License, they do not -excuse you from the conditions of this License. If you cannot -distribute so as to satisfy simultaneously your obligations under this -License and any other pertinent obligations, then as a consequence you -may not distribute the Library at all. For example, if a patent -license would not permit royalty-free redistribution of the Library by -all those who receive copies directly or indirectly through you, then -the only way you could satisfy both it and this License would be to -refrain entirely from distribution of the Library. - -If any portion of this section is held invalid or unenforceable under any -particular circumstance, the balance of the section is intended to apply, -and the section as a whole is intended to apply in other circumstances. - -It is not the purpose of this section to induce you to infringe any -patents or other property right claims or to contest validity of any -such claims; this section has the sole purpose of protecting the -integrity of the free software distribution system which is -implemented by public license practices. Many people have made -generous contributions to the wide range of software distributed -through that system in reliance on consistent application of that -system; it is up to the author/donor to decide if he or she is willing -to distribute software through any other system and a licensee cannot -impose that choice. - -This section is intended to make thoroughly clear what is believed to -be a consequence of the rest of this License. - - 12. If the distribution and/or use of the Library is restricted in -certain countries either by patents or by copyrighted interfaces, the -original copyright holder who places the Library under this License may add -an explicit geographical distribution limitation excluding those countries, -so that distribution is permitted only in or among countries not thus -excluded. In such case, this License incorporates the limitation as if -written in the body of this License. - - 13. The Free Software Foundation may publish revised and/or new -versions of the Lesser General Public License from time to time. -Such new versions will be similar in spirit to the present version, -but may differ in detail to address new problems or concerns. - -Each version is given a distinguishing version number. If the Library -specifies a version number of this License which applies to it and -"any later version", you have the option of following the terms and -conditions either of that version or of any later version published by -the Free Software Foundation. If the Library does not specify a -license version number, you may choose any version ever published by -the Free Software Foundation. - - 14. If you wish to incorporate parts of the Library into other free -programs whose distribution conditions are incompatible with these, -write to the author to ask for permission. For software which is -copyrighted by the Free Software Foundation, write to the Free -Software Foundation; we sometimes make exceptions for this. Our -decision will be guided by the two goals of preserving the free status -of all derivatives of our free software and of promoting the sharing -and reuse of software generally. - - NO WARRANTY - - 15. BECAUSE THE LIBRARY IS LICENSED FREE OF CHARGE, THERE IS NO -WARRANTY FOR THE LIBRARY, TO THE EXTENT PERMITTED BY APPLICABLE LAW. -EXCEPT WHEN OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR -OTHER PARTIES PROVIDE THE LIBRARY "AS IS" WITHOUT WARRANTY OF ANY -KIND, EITHER EXPRESSED OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE -IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR -PURPOSE. THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE -LIBRARY IS WITH YOU. SHOULD THE LIBRARY PROVE DEFECTIVE, YOU ASSUME -THE COST OF ALL NECESSARY SERVICING, REPAIR OR CORRECTION. - - 16. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN -WRITING WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY -AND/OR REDISTRIBUTE THE LIBRARY AS PERMITTED ABOVE, BE LIABLE TO YOU -FOR DAMAGES, INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR -CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE THE -LIBRARY (INCLUDING BUT NOT LIMITED TO LOSS OF DATA OR DATA BEING -RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD PARTIES OR A -FAILURE OF THE LIBRARY TO OPERATE WITH ANY OTHER SOFTWARE), EVEN IF -SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH -DAMAGES. - - END OF TERMS AND CONDITIONS - - How to Apply These Terms to Your New Libraries - - If you develop a new library, and you want it to be of the greatest -possible use to the public, we recommend making it free software that -everyone can redistribute and change. You can do so by permitting -redistribution under these terms (or, alternatively, under the terms of the -ordinary General Public License). - - To apply these terms, attach the following notices to the library. It is -safest to attach them to the start of each source file to most effectively -convey the exclusion of warranty; and each file should have at least the -"copyright" line and a pointer to where the full notice is found. - - - Copyright (C) - - This library is free software; you can redistribute it and/or - modify it under the terms of the GNU Lesser General Public - License as published by the Free Software Foundation; either - version 2.1 of the License, or (at your option) any later version. - - This library is distributed in the hope that it will be useful, - but WITHOUT ANY WARRANTY; without even the implied warranty of - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU - Lesser General Public License for more details. - - You should have received a copy of the GNU Lesser General Public - License along with this library; if not, write to the Free Software - Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA - -Also add information on how to contact you by electronic and paper mail. - -You should also get your employer (if you work as a programmer) or your -school, if any, to sign a "copyright disclaimer" for the library, if -necessary. Here is a sample; alter the names: - - Yoyodyne, Inc., hereby disclaims all copyright interest in the - library `Frob' (a library for tweaking knobs) written by James Random Hacker. - - , 1 April 1990 - Ty Coon, President of Vice - -That's all there is to it! - -All code incorporated from 4.4 BSD is distributed under the following -license: - -Copyright (C) 1991 Regents of the University of California. -All rights reserved. - -Redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions -are met: - -1. Redistributions of source code must retain the above copyright - notice, this list of conditions and the following disclaimer. -2. Redistributions in binary form must reproduce the above copyright - notice, this list of conditions and the following disclaimer in the - documentation and/or other materials provided with the distribution. -3. [This condition was removed.] -4. Neither the name of the University nor the names of its contributors - may be used to endorse or promote products derived from this software - without specific prior written permission. - -THIS SOFTWARE IS PROVIDED BY THE REGENTS AND CONTRIBUTORS ``AS IS'' AND -ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE -IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE -ARE DISCLAIMED. IN NO EVENT SHALL THE REGENTS OR CONTRIBUTORS BE LIABLE -FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS -OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) -HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT -LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY -OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF -SUCH DAMAGE. - -The DNS resolver code, taken from BIND 4.9.5, is copyrighted by UC -Berkeley, by Digital Equipment Corporation and by Internet Software -Consortium. The DEC portions are under the following license: - -Portions Copyright (C) 1993 by Digital Equipment Corporation. - -Permission to use, copy, modify, and distribute this software for any -purpose with or without fee is hereby granted, provided that the above -copyright notice and this permission notice appear in all copies, and -that the name of Digital Equipment Corporation not be used in -advertising or publicity pertaining to distribution of the document or -software without specific, written prior permission. - -THE SOFTWARE IS PROVIDED ``AS IS'' AND DIGITAL EQUIPMENT CORP. -DISCLAIMS ALL WARRANTIES WITH REGARD TO THIS SOFTWARE, INCLUDING ALL -IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL -DIGITAL EQUIPMENT CORPORATION BE LIABLE FOR ANY SPECIAL, DIRECT, -INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING -FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN ACTION OF CONTRACT, -NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION -WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. - -The ISC portions are under the following license: - -Portions Copyright (c) 1996-1999 by Internet Software Consortium. - -Permission to use, copy, modify, and distribute this software for any -purpose with or without fee is hereby granted, provided that the above -copyright notice and this permission notice appear in all copies. - -THE SOFTWARE IS PROVIDED "AS IS" AND INTERNET SOFTWARE CONSORTIUM DISCLAIMS -ALL WARRANTIES WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES -OF MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL INTERNET SOFTWARE -CONSORTIUM BE LIABLE FOR ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL -DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR -PROFITS, WHETHER IN AN ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS -ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS -SOFTWARE. - -The Sun RPC support (from rpcsrc-4.0) is covered by the following -license: - -Copyright (c) 2010, Oracle America, Inc. - -Redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are -met: - - * Redistributions of source code must retain the above copyright - notice, this list of conditions and the following disclaimer. - * Redistributions in binary form must reproduce the above - copyright notice, this list of conditions and the following - disclaimer in the documentation and/or other materials - provided with the distribution. - * Neither the name of the "Oracle America, Inc." nor the names of its - contributors may be used to endorse or promote products derived - from this software without specific prior written permission. - - THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS - "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT - LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS - FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE - COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, - INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL - DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE - GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS - INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, - WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING - NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE - OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. - - -The following CMU license covers some of the support code for Mach, -derived from Mach 3.0: - -Mach Operating System -Copyright (C) 1991,1990,1989 Carnegie Mellon University -All Rights Reserved. - -Permission to use, copy, modify and distribute this software and its -documentation is hereby granted, provided that both the copyright -notice and this permission notice appear in all copies of the -software, derivative works or modified versions, and any portions -thereof, and that both notices appear in supporting documentation. - -CARNEGIE MELLON ALLOWS FREE USE OF THIS SOFTWARE IN ITS ``AS IS'' -CONDITION. CARNEGIE MELLON DISCLAIMS ANY LIABILITY OF ANY KIND FOR -ANY DAMAGES WHATSOEVER RESULTING FROM THE USE OF THIS SOFTWARE. - -Carnegie Mellon requests users of this software to return to - - Software Distribution Coordinator - School of Computer Science - Carnegie Mellon University - Pittsburgh PA 15213-3890 - -or Software.Distribution@CS.CMU.EDU any improvements or -extensions that they make and grant Carnegie Mellon the rights to -redistribute these changes. - -The file if_ppp.h is under the following CMU license: - - Redistribution and use in source and binary forms, with or without - modification, are permitted provided that the following conditions - are met: - 1. Redistributions of source code must retain the above copyright - notice, this list of conditions and the following disclaimer. - 2. Redistributions in binary form must reproduce the above copyright - notice, this list of conditions and the following disclaimer in the - documentation and/or other materials provided with the distribution. - 3. Neither the name of the University nor the names of its contributors - may be used to endorse or promote products derived from this software - without specific prior written permission. - - THIS SOFTWARE IS PROVIDED BY CARNEGIE MELLON UNIVERSITY AND - CONTRIBUTORS ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, - INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF - MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. - IN NO EVENT SHALL THE UNIVERSITY OR CONTRIBUTORS BE LIABLE FOR ANY - DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL - DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE - GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS - INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER - IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR - OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN - IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. - -The following license covers the files from Intel's "Highly Optimized -Mathematical Functions for Itanium" collection: - -Intel License Agreement - -Copyright (c) 2000, Intel Corporation - -All rights reserved. - -Redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are -met: - -* Redistributions of source code must retain the above copyright -notice, this list of conditions and the following disclaimer. - -* Redistributions in binary form must reproduce the above copyright -notice, this list of conditions and the following disclaimer in the -documentation and/or other materials provided with the distribution. - -* The name of Intel Corporation may not be used to endorse or promote -products derived from this software without specific prior written -permission. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS -"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT -LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR -A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL INTEL OR -CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, -EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, -PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR -PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF -LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING -NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS -SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. - -The files inet/getnameinfo.c and sysdeps/posix/getaddrinfo.c are copyright -(C) by Craig Metz and are distributed under the following license: - -/* The Inner Net License, Version 2.00 - - The author(s) grant permission for redistribution and use in source and -binary forms, with or without modification, of the software and documentation -provided that the following conditions are met: - -0. If you receive a version of the software that is specifically labelled - as not being for redistribution (check the version message and/or README), - you are not permitted to redistribute that version of the software in any - way or form. -1. All terms of the all other applicable copyrights and licenses must be - followed. -2. Redistributions of source code must retain the authors' copyright - notice(s), this list of conditions, and the following disclaimer. -3. Redistributions in binary form must reproduce the authors' copyright - notice(s), this list of conditions, and the following disclaimer in the - documentation and/or other materials provided with the distribution. -4. [The copyright holder has authorized the removal of this clause.] -5. Neither the name(s) of the author(s) nor the names of its contributors - may be used to endorse or promote products derived from this software - without specific prior written permission. - -THIS SOFTWARE IS PROVIDED BY ITS AUTHORS AND CONTRIBUTORS ``AS IS'' AND ANY -EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED -WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE -DISCLAIMED. IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE FOR ANY -DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES -(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; -LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON -ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT -(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS -SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. - - If these license terms cause you a real problem, contact the author. */ - -The file sunrpc/des_impl.c is copyright Eric Young: - -Copyright (C) 1992 Eric Young -Collected from libdes and modified for SECURE RPC by Martin Kuck 1994 -This file is distributed under the terms of the GNU Lesser General -Public License, version 2.1 or later - see the file COPYING.LIB for details. -If you did not receive a copy of the license with this program, please -see to obtain a copy. - -The file inet/rcmd.c is under a UCB copyright and the following: - -Copyright (C) 1998 WIDE Project. -All rights reserved. - -Redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions -are met: -1. Redistributions of source code must retain the above copyright - notice, this list of conditions and the following disclaimer. -2. Redistributions in binary form must reproduce the above copyright - notice, this list of conditions and the following disclaimer in the - documentation and/or other materials provided with the distribution. -3. Neither the name of the project nor the names of its contributors - may be used to endorse or promote products derived from this software - without specific prior written permission. - -THIS SOFTWARE IS PROVIDED BY THE PROJECT AND CONTRIBUTORS ``AS IS'' AND -ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE -IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE -ARE DISCLAIMED. IN NO EVENT SHALL THE PROJECT OR CONTRIBUTORS BE LIABLE -FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL -DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS -OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) -HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT -LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY -OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF -SUCH DAMAGE. - -The file posix/runtests.c is copyright Tom Lord: - -Copyright 1995 by Tom Lord - - All Rights Reserved - -Permission to use, copy, modify, and distribute this software and its -documentation for any purpose and without fee is hereby granted, -provided that the above copyright notice appear in all copies and that -both that copyright notice and this permission notice appear in -supporting documentation, and that the name of the copyright holder not be -used in advertising or publicity pertaining to distribution of the -software without specific, written prior permission. - -Tom Lord DISCLAIMS ALL WARRANTIES WITH REGARD TO THIS SOFTWARE, -INCLUDING ALL IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS, IN NO -EVENT SHALL TOM LORD BE LIABLE FOR ANY SPECIAL, INDIRECT OR -CONSEQUENTIAL DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM LOSS OF -USE, DATA OR PROFITS, WHETHER IN AN ACTION OF CONTRACT, NEGLIGENCE OR -OTHER TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR -PERFORMANCE OF THIS SOFTWARE. - -The posix/rxspencer tests are copyright Henry Spencer: - -Copyright 1992, 1993, 1994, 1997 Henry Spencer. All rights reserved. -This software is not subject to any license of the American Telephone -and Telegraph Company or of the Regents of the University of California. - -Permission is granted to anyone to use this software for any purpose on -any computer system, and to alter it and redistribute it, subject -to the following restrictions: - -1. The author is not responsible for the consequences of use of this - software, no matter how awful, even if they arise from flaws in it. - -2. The origin of this software must not be misrepresented, either by - explicit claim or by omission. Since few users ever read sources, - credits must appear in the documentation. - -3. Altered versions must be plainly marked as such, and must not be - misrepresented as being the original software. Since few users - ever read sources, credits must appear in the documentation. - -4. This notice may not be removed or altered. - -The file posix/PCRE.tests is copyright University of Cambridge: - -Copyright (c) 1997-2003 University of Cambridge - -Permission is granted to anyone to use this software for any purpose on any -computer system, and to redistribute it freely, subject to the following -restrictions: - -1. This software is distributed in the hope that it will be useful, - but WITHOUT ANY WARRANTY; without even the implied warranty of - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. - -2. The origin of this software must not be misrepresented, either by - explicit claim or by omission. In practice, this means that if you use - PCRE in software that you distribute to others, commercially or - otherwise, you must put a sentence like this - - Regular expression support is provided by the PCRE library package, - which is open source software, written by Philip Hazel, and copyright - by the University of Cambridge, England. - - somewhere reasonably visible in your documentation and in any relevant - files or online help data or similar. A reference to the ftp site for - the source, that is, to - - ftp://ftp.csx.cam.ac.uk/pub/software/programming/pcre/ - - should also be given in the documentation. However, this condition is not - intended to apply to whole chains of software. If package A includes PCRE, - it must acknowledge it, but if package B is software that includes package - A, the condition is not imposed on package B (unless it uses PCRE - independently). - -3. Altered versions must be plainly marked as such, and must not be - misrepresented as being the original software. - -4. If PCRE is embedded in any software that is released under the GNU - General Purpose Licence (GPL), or Lesser General Purpose Licence (LGPL), - then the terms of that licence shall supersede any condition above with - which it is incompatible. - -Files from Sun fdlibm are copyright Sun Microsystems, Inc.: - -Copyright (C) 1993 by Sun Microsystems, Inc. All rights reserved. - -Developed at SunPro, a Sun Microsystems, Inc. business. -Permission to use, copy, modify, and distribute this -software is freely granted, provided that this notice -is preserved. - -Various long double libm functions are copyright Stephen L. Moshier: - -Copyright 2001 by Stephen L. Moshier - - This library is free software; you can redistribute it and/or - modify it under the terms of the GNU Lesser General Public - License as published by the Free Software Foundation; either - version 2.1 of the License, or (at your option) any later version. - - This library is distributed in the hope that it will be useful, - but WITHOUT ANY WARRANTY; without even the implied warranty of - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU - Lesser General Public License for more details. - - You should have received a copy of the GNU Lesser General Public - License along with this library; if not, see - . */ From c906567dc7a65a4b6e6bb8494f84ce73d99447cb Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 5 Nov 2021 18:40:38 +0100 Subject: [PATCH 15/27] fix: leanc: drop empty arguments --- src/Leanc.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Leanc.lean b/src/Leanc.lean index 4205a4542682..0986e70a9106 100644 --- a/src/Leanc.lean +++ b/src/Leanc.lean @@ -50,7 +50,7 @@ Beware of the licensing consequences since GMP is LGPL." ldflagsInternal := [] cc := rootify cc let args := cflags ++ cflagsInternal ++ args ++ ldflagsExt ++ ldflags ++ ldflagsInternal ++ ["-Wno-unused-command-line-argument"] - let args := args.map rootify + let args := args.filter (!·.isEmpty) |>.map rootify if args.contains "-v" then IO.eprintln s!"{cc} {" ".intercalate args}" let child ← IO.Process.spawn { cmd := cc, args := args.toArray } From 9d67d4eb2dbbaa0579980ae9f27f0f38dfa3e4d7 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 5 Nov 2021 18:50:50 +0100 Subject: [PATCH 16/27] fix: use old nixpkgs for glibc only --- .github/workflows/ci.yml | 2 +- shell.nix | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 46147af34bfc..5d28daf1f255 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -26,7 +26,7 @@ jobs: - name: Linux release os: ubuntu-latest release: true - shell: nix-shell --arg pkgs "import (fetchTarball \"channel:nixos-19.03\") {{}}" --argstr llvmPackages latest --run "bash -euxo pipefail {0}" + shell: nix-shell --arg glibc "(import (fetchTarball \"channel:nixos-19.03\") {{}}).glibc" --run "bash -euxo pipefail {0}" llvm-url: https://github.com/leanprover/lean-llvm/releases/download/13.0.0/lean-llvm-x86_64-linux-gnu.tar.zst - name: Linux os: ubuntu-latest diff --git a/shell.nix b/shell.nix index 152d04c65305..73d2625e63f7 100644 --- a/shell.nix +++ b/shell.nix @@ -1,6 +1,6 @@ let flakePkgs = (import ./default.nix).packages.${builtins.currentSystem}; -in { pkgs ? flakePkgs.nixpkgs, llvmPackages ? null }: +in { pkgs ? flakePkgs.nixpkgs, llvmPackages ? null, glibc ? pkgs.glibc }: # use `shell` as default (attribs: attribs.shell // attribs) rec { shell = pkgs.mkShell.override { @@ -14,7 +14,7 @@ in { pkgs ? flakePkgs.nixpkgs, llvmPackages ? null }: # more convenient `ctest` output CTEST_OUTPUT_ON_FAILURE = 1; GMP = pkgs.gmp.override { withStatic = true; }; - GLIBC = pkgs.glibc; + GLIBC = glibc; shellHook = '' export LEAN_SRC_PATH="$PWD/src" ''; From 4f0166505d2928c18d325d9f4a4ccb0149dee6b7 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sun, 7 Nov 2021 09:53:46 +0100 Subject: [PATCH 17/27] chore: update lean-llvm --- script/prepare-llvm-linux.sh | 2 -- 1 file changed, 2 deletions(-) diff --git a/script/prepare-llvm-linux.sh b/script/prepare-llvm-linux.sh index 8c2afb9195f6..43086958a65f 100755 --- a/script/prepare-llvm-linux.sh +++ b/script/prepare-llvm-linux.sh @@ -17,8 +17,6 @@ $CP $(realpath llvm/bin/clang) stage1/bin/clang $CP llvm/bin/{lld,ld.lld} stage1/bin/ # dependencies of the above $CP llvm/lib/lib{clang-cpp,LLVM}*.so* stage1/lib/ -# fix up some rpaths(...?) -patchelf --set-rpath '$ORIGIN' llvm/lib/libc++.so.* # lean.h dependencies $CP llvm/lib/clang/*/include/{std*,__std*,limits}.h stage1/include/clang # ELF dependencies, must be put there for `--sysroot` From 73489c98feccb7839bcd6f21b9c89b85fa7f0d8d Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sun, 7 Nov 2021 12:06:52 +0100 Subject: [PATCH 18/27] chore: install license --- src/CMakeLists.txt | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 01b977013a84..241e329326f8 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -536,6 +536,10 @@ install(DIRECTORY "${CMAKE_SOURCE_DIR}" DESTINATION lib/lean PATTERN "*.md" PATTERN examples EXCLUDE) +if(${STAGE} GREATER 0) + install(FILES "${CMAKE_SOURCE_DIR}/../LICENSE" DESTINATION ".") +endif() + file(COPY ${CMAKE_SOURCE_DIR}/include/lean DESTINATION ${CMAKE_BINARY_DIR}/include FILES_MATCHING PATTERN "*.h") From 427cee6256349eca2d018f998ac8dfc44c45a984 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sun, 7 Nov 2021 12:36:06 +0100 Subject: [PATCH 19/27] feat: reimplement `assert` without system headers --- src/include/lean/lean.h | 14 +++++++------- src/runtime/debug.cpp | 6 ++++++ 2 files changed, 13 insertions(+), 7 deletions(-) diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h index ac281f7b8b5e..fbdc24c661b8 100644 --- a/src/include/lean/lean.h +++ b/src/include/lean/lean.h @@ -21,13 +21,6 @@ extern "C" { #endif #include -#ifdef NDEBUG -#define assert(expr) -#else -// TODO -#define assert(expr) -#endif - #define LEAN_CLOSURE_MAX_ARGS 16 #define LEAN_OBJECT_SIZE_DELTA 8 #define LEAN_MAX_SMALL_OBJECT_SIZE 4096 @@ -48,6 +41,13 @@ extern "C" { #define LEAN_ALWAYS_INLINE #endif +#ifdef NDEBUG +#define assert(expr) +#else +void lean_notify_assert(const char * fileName, int line, const char * condition); +#define assert(expr) { if (LEAN_UNLIKELY(!(expr))) lean_notify_assert(__FILE__, __LINE__, #expr); } +#endif + #ifdef _WIN32 #define LEAN_EXPORT __declspec(dllexport) #else diff --git a/src/runtime/debug.cpp b/src/runtime/debug.cpp index 7317464a326a..ee4f9171006a 100644 --- a/src/runtime/debug.cpp +++ b/src/runtime/debug.cpp @@ -17,6 +17,7 @@ Author: Leonardo de Moura // Support for pid #include #endif +#include #include "runtime/debug.h" namespace lean { @@ -133,4 +134,9 @@ void invoke_debugger() { #endif } // LCOV_EXCL_STOP + +extern "C" LEAN_EXPORT void lean_notify_assert(const char * fileName, int line, const char * condition) { + notify_assertion_violation(fileName, line, condition); + invoke_debugger(); +} } From c9fbac0fd319bdf2b48da34ac607cf59cb1cf0be Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sun, 7 Nov 2021 13:56:05 +0100 Subject: [PATCH 20/27] feat: upload .tar.zst and .zip for every platform Also, do so only for releases since `zstd -19` takes a while. Also, stop double-wrapping artifacts --- .github/workflows/ci.yml | 36 ++++++++++++++++++------------------ src/CMakeLists.txt | 7 +++++++ 2 files changed, 25 insertions(+), 18 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 5d28daf1f255..c1ede85eb2d2 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -74,11 +74,11 @@ jobs: - name: Install MSYS2 uses: msys2/setup-msys2@v2 with: - install: make python mingw-w64-x86_64-cmake mingw-w64-x86_64-clang mingw-w64-x86_64-ccache git unzip diffutils binutils tree + install: make python mingw-w64-x86_64-cmake mingw-w64-x86_64-clang mingw-w64-x86_64-ccache git zip unzip diffutils binutils tree mingw-w64-x86_64-zstd if: matrix.os == 'windows-2022' - name: Install Brew Packages run: | - brew install ccache tree + brew install ccache tree zstd if: matrix.os == 'macos-latest' - name: Cache uses: actions/cache@v2 @@ -104,7 +104,7 @@ jobs: OPTIONS=() if [[ '${{ matrix.llvm-url }}' && "${{ matrix.name }}" == "Linux release" ]]; then wget -q ${{ matrix.llvm-url }} - eval "OPTIONS+=($(../script/prepare-llvm-linux.sh *llvm*))" + eval "OPTIONS+=($(../script/prepare-llvm-linux.sh lean-llvm*))" fi if [[ $GITHUB_EVENT_NAME == 'schedule' && -n '${{ matrix.release }}' && -n '${{ secrets.PUSH_NIGHTLY_TOKEN }}' ]]; then git remote add nightly https://foo:'${{ secrets.PUSH_NIGHTLY_TOKEN }}'@github.com/${{ github.repository_owner }}/lean4-nightly.git @@ -117,13 +117,13 @@ jobs: fi fi # contortion to support empty OPTIONS with old macOS bash - cmake .. ${{ matrix.CMAKE_OPTIONS }} ${OPTIONS[@]+"${OPTIONS[@]}"} + cmake .. ${{ matrix.CMAKE_OPTIONS }} ${OPTIONS[@]+"${OPTIONS[@]}"} -DLEAN_INSTALL_PREFIX=$PWD/.. make -j4 + make install - name: Check binaries if: matrix.name == 'Linux release' run: | - ldd -v build/stage1/bin/* || true - ls -l build/stage1/lib/ + ldd -v lean-*/bin/* || true - name: Patch if: matrix.name == 'macOS' run: | @@ -145,22 +145,22 @@ jobs: cp $(ldd bin/lean.exe | cut -f3 -d' ' | grep mingw) bin/ ldd bin/lean.exe ls -l bin/ - - name: Test Binary without Nix Shell - if: matrix.name != 'Windows' - shell: bash {0} + - name: List Install Tree run: | - build/stage1/bin/lean -h + # omit contents of src/, Init/, ... + tree --du -h lean-* | grep -Ev '(│.*){3}' - name: Pack + if: ${{ startsWith(github.ref, 'refs/tags/v') && matrix.release }} run: | - cd build/stage1 - cpack - mkdir unpack - tar xf lean-* -C unpack || unzip lean-4 -d unpack - tree --du -h unpack + dir=$(echo lean-*) + mkdir pack + which zstd + tar cf - $dir | zstd -T0 --no-progress -19 -o pack/$dir.tar.zst + zip -r pack/$dir.zip $dir - uses: actions/upload-artifact@v2 with: name: build-${{ matrix.name }} - path: build/stage1/lean-* + path: lean-* - name: Lean stats run: | build/stage1/bin/lean --stats src/Lean.lean @@ -195,7 +195,7 @@ jobs: uses: softprops/action-gh-release@v1 if: ${{ startsWith(github.ref, 'refs/tags/v') && matrix.release }} with: - files: build/stage1/lean-* + files: pack/* env: GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} - name: Prepare Nightly Release @@ -223,7 +223,7 @@ jobs: with: body_path: diff.md prerelease: true - files: build/stage1/lean-* + files: pack/* tag_name: ${{ env.LEAN_VERSION_STRING }} repository: ${{ github.repository_owner }}/lean4-nightly env: diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 241e329326f8..7f413e0c78a0 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -558,4 +558,11 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Linux") else() SET(CPACK_GENERATOR ZIP) endif() + +set(LEAN_INSTALL_PREFIX "" CACHE STRING "If set, set CMAKE_INSTALL_PREFIX to this value + version name") +if(LEAN_INSTALL_PREFIX) + set(CMAKE_INSTALL_PREFIX "${LEAN_INSTALL_PREFIX}/${CPACK_PACKAGE_FILE_NAME}") +endif() + +# NOTE: modifies `CPACK_PACKAGE_FILE_NAME`(??) include(CPack) From c38a78923bfabac98fde9f5cb28228795171b160 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sun, 7 Nov 2021 23:07:44 +0100 Subject: [PATCH 21/27] fix: Linux: bundle zlib --- .github/workflows/ci.yml | 2 +- script/prepare-llvm-linux.sh | 5 +++-- shell.nix | 7 ++++--- 3 files changed, 8 insertions(+), 6 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index c1ede85eb2d2..512abe240c0b 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -26,7 +26,7 @@ jobs: - name: Linux release os: ubuntu-latest release: true - shell: nix-shell --arg glibc "(import (fetchTarball \"channel:nixos-19.03\") {{}}).glibc" --run "bash -euxo pipefail {0}" + shell: nix-shell --arg pkgsDist "import (fetchTarball \"channel:nixos-19.03\") {{}}" --run "bash -euxo pipefail {0}" llvm-url: https://github.com/leanprover/lean-llvm/releases/download/13.0.0/lean-llvm-x86_64-linux-gnu.tar.zst - name: Linux os: ubuntu-latest diff --git a/script/prepare-llvm-linux.sh b/script/prepare-llvm-linux.sh index 43086958a65f..c54c7f775925 100755 --- a/script/prepare-llvm-linux.sh +++ b/script/prepare-llvm-linux.sh @@ -1,7 +1,7 @@ #!/usr/bin/env bash set -uo pipefail -# run from root build directory (from inside nix-shell or otherwise defining GLIBC/GMP) as in +# run from root build directory (from inside nix-shell or otherwise defining GLIBC/ZLIB/GMP) as in # ``` # eval cmake ../.. $(../../script/prepare-llvm-linux.sh ~/Downloads/clang+llvm-13.0.0-x86_64-linux-gnu-ubuntu-16.04.tar.xz) # ``` @@ -14,9 +14,10 @@ CP="cp -d" # preserve symlinks # a C compiler! $CP $(realpath llvm/bin/clang) stage1/bin/clang # a linker! -$CP llvm/bin/{lld,ld.lld} stage1/bin/ +$CP llvm/bin/{ld.lld,lld} stage1/bin/ # dependencies of the above $CP llvm/lib/lib{clang-cpp,LLVM}*.so* stage1/lib/ +$CP $ZLIB/lib/libz.so* stage1/lib/ # lean.h dependencies $CP llvm/lib/clang/*/include/{std*,__std*,limits}.h stage1/include/clang # ELF dependencies, must be put there for `--sysroot` diff --git a/shell.nix b/shell.nix index 73d2625e63f7..6d5bb1de6ef9 100644 --- a/shell.nix +++ b/shell.nix @@ -1,6 +1,6 @@ let flakePkgs = (import ./default.nix).packages.${builtins.currentSystem}; -in { pkgs ? flakePkgs.nixpkgs, llvmPackages ? null, glibc ? pkgs.glibc }: +in { pkgs ? flakePkgs.nixpkgs, pkgsDist ? pkgs, llvmPackages ? null }: # use `shell` as default (attribs: attribs.shell // attribs) rec { shell = pkgs.mkShell.override { @@ -13,8 +13,9 @@ in { pkgs ? flakePkgs.nixpkgs, llvmPackages ? null, glibc ? pkgs.glibc }: hardeningDisable = [ "all" ]; # more convenient `ctest` output CTEST_OUTPUT_ON_FAILURE = 1; - GMP = pkgs.gmp.override { withStatic = true; }; - GLIBC = glibc; + GMP = pkgsDist.gmp.override { withStatic = true; }; + GLIBC = pkgsDist.glibc; + ZLIB = pkgsDist.zlib; shellHook = '' export LEAN_SRC_PATH="$PWD/src" ''; From f5e69bdbd47a9342628222615d9b68825e7328ef Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 8 Nov 2021 17:37:22 +0100 Subject: [PATCH 22/27] fix: actually link against GMP statically --- script/prepare-llvm-linux.sh | 4 ++-- src/Leanc.lean | 4 ++-- src/bin/leanc.in | 2 +- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/script/prepare-llvm-linux.sh b/script/prepare-llvm-linux.sh index c54c7f775925..29cbbffc89f1 100755 --- a/script/prepare-llvm-linux.sh +++ b/script/prepare-llvm-linux.sh @@ -32,8 +32,8 @@ for f in $GLIBC/lib/lib{c,dl,m,rt,pthread}-*; do b=$(basename $f); cp $f stage1/ OPTIONS=() echo -n " -DCMAKE_C_COMPILER=$PWD/stage1/bin/clang -DCMAKE_CXX_COMPILER=$PWD/llvm/bin/clang++ -DLEAN_CXX_STDLIB='-Wl,-Bstatic -lc++ -lc++abi -Wl,-Bdynamic'" # allow C++ code to include /usr since it needs quite a few more headers -echo -n " -DLEAN_EXTRA_CXX_FLAGS='--sysroot $PWD/llvm --stdlib=libc++ -I/usr/include -I/usr/include/x86_64-linux-gnu'" +echo -n " -DLEAN_EXTRA_CXX_FLAGS='--sysroot $PWD/llvm -I/usr/include -I/usr/include/x86_64-linux-gnu'" echo -n " -DLEANC_INTERNAL_FLAGS='--sysroot ROOT -I ROOT/include/clang' -DLEANC_CC=ROOT/bin/clang" -echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -L ROOT/lib/glibc ROOT/lib/glibc/libc_nonshared.a --rtlib=compiler-rt -static-libgcc -Wl,-Bstatic -lgmp -lunwind -Wl,-Bdynamic -fuse-ld=lld'" +echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -L ROOT/lib/glibc ROOT/lib/glibc/libc_nonshared.a -Wl,--as-needed -static-libgcc -Wl,-Bstatic -lgmp -lunwind -Wl,-Bdynamic -fuse-ld=lld'" # do not set `LEAN_CC` for tests echo -n " -DLEAN_TEST_VARS=''" diff --git a/src/Leanc.lean b/src/Leanc.lean index 0986e70a9106..ac4753942ffe 100644 --- a/src/Leanc.lean +++ b/src/Leanc.lean @@ -22,9 +22,9 @@ Beware of the licensing consequences since GMP is LGPL." -- We assume that the CMake variables do not contain escaped spaces let cflags := ["-I", (root / "include").toString] ++ "@LEANC_EXTRA_FLAGS@".trim.splitOn let mut cflagsInternal := "@LEANC_INTERNAL_FLAGS@".trim.splitOn + let mut ldflagsInternal := "@LEANC_INTERNAL_LINKER_FLAGS@".trim.splitOn let mut ldflags := ["-L", (root / "lib" / "lean").toString, "-lgmp"] ++ "@LEAN_EXTRA_LINKER_FLAGS@".trim.splitOn let mut ldflagsExt := "@LEANC_STATIC_LINKER_FLAGS@".trim.splitOn - let mut ldflagsInternal := "@LEANC_INTERNAL_LINKER_FLAGS@".trim.splitOn for arg in args do match arg with @@ -49,7 +49,7 @@ Beware of the licensing consequences since GMP is LGPL." cflagsInternal := [] ldflagsInternal := [] cc := rootify cc - let args := cflags ++ cflagsInternal ++ args ++ ldflagsExt ++ ldflags ++ ldflagsInternal ++ ["-Wno-unused-command-line-argument"] + let args := cflags ++ cflagsInternal ++ args ++ ldflagsInternal ++ ldflagsExt ++ ldflags ++ ["-Wno-unused-command-line-argument"] let args := args.filter (!·.isEmpty) |>.map rootify if args.contains "-v" then IO.eprintln s!"{cc} {" ".intercalate args}" diff --git a/src/bin/leanc.in b/src/bin/leanc.in index cc7a6158b31d..5cb9a1633de1 100755 --- a/src/bin/leanc.in +++ b/src/bin/leanc.in @@ -1,7 +1,7 @@ #!/usr/bin/env bash # used only for building Lean itself root=$(dirname $0) -ldflags=("-L$root/lib" "-L$root/lib/lean" "${LEANC_GMP:--lgmp}" @LEAN_EXTRA_LINKER_FLAGS@ @LEANC_INTERNAL_LINKER_FLAGS@) +ldflags=(@LEANC_INTERNAL_LINKER_FLAGS@ "-L$root/lib/lean" "${LEANC_GMP:--lgmp}" @LEAN_EXTRA_LINKER_FLAGS@) for arg in "$@"; do # ccache doesn't like linker flags being passed here [[ "$arg" = "-c" ]] && ldflags=() From d9e41116c8625fd8c2c564c259459f02663194e5 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 8 Nov 2021 17:53:09 +0100 Subject: [PATCH 23/27] perf: strip LLVM binaries --- script/prepare-llvm-linux.sh | 1 + 1 file changed, 1 insertion(+) diff --git a/script/prepare-llvm-linux.sh b/script/prepare-llvm-linux.sh index 29cbbffc89f1..693a75fd7d51 100755 --- a/script/prepare-llvm-linux.sh +++ b/script/prepare-llvm-linux.sh @@ -18,6 +18,7 @@ $CP llvm/bin/{ld.lld,lld} stage1/bin/ # dependencies of the above $CP llvm/lib/lib{clang-cpp,LLVM}*.so* stage1/lib/ $CP $ZLIB/lib/libz.so* stage1/lib/ +find stage1 -type f -exec strip --strip-unneeded '{}' \; 2> /dev/null # lean.h dependencies $CP llvm/lib/clang/*/include/{std*,__std*,limits}.h stage1/include/clang # ELF dependencies, must be put there for `--sysroot` From b36e253cdd078931d465e6e57e590d5d0a55f972 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 9 Nov 2021 13:40:13 +0100 Subject: [PATCH 24/27] chore: fix `leanc.sh -v` --- src/bin/leanc.in | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/bin/leanc.in b/src/bin/leanc.in index 5cb9a1633de1..60ae824f771b 100755 --- a/src/bin/leanc.in +++ b/src/bin/leanc.in @@ -9,5 +9,5 @@ for arg in "$@"; do done cmd=(${LEAN_CC:-@CMAKE_C_COMPILER@} "-I$root/include" @LEANC_EXTRA_FLAGS@ @LEANC_INTERNAL_FLAGS@ "$@" "${ldflags[@]}" -Wno-unused-command-line-argument) cmd=$(printf '%q ' "${cmd[@]}" | sed "s!ROOT!$root!g") -[[ $v == 1 ]] && printf '%q ' $cmd +[[ $v == 1 ]] && echo $cmd eval $cmd From 1d5c4789aa95096d684fae56c9b2d24248b92416 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 9 Nov 2021 17:24:41 +0100 Subject: [PATCH 25/27] chore: avoid C++ warning --- src/include/lean/lean.h | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h index fbdc24c661b8..559a7bc30ab3 100644 --- a/src/include/lean/lean.h +++ b/src/include/lean/lean.h @@ -41,12 +41,14 @@ extern "C" { #define LEAN_ALWAYS_INLINE #endif +#ifndef assert #ifdef NDEBUG #define assert(expr) #else void lean_notify_assert(const char * fileName, int line, const char * condition); #define assert(expr) { if (LEAN_UNLIKELY(!(expr))) lean_notify_assert(__FILE__, __LINE__, #expr); } #endif +#endif #ifdef _WIN32 #define LEAN_EXPORT __declspec(dllexport) From 7344f8c172f6e602fed68a52aae97f30783026b3 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 9 Nov 2021 17:34:00 +0100 Subject: [PATCH 26/27] chore: fix foreign test on macOS, again --- src/Leanc.lean | 2 +- src/shell/CMakeLists.txt | 3 ++- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/Leanc.lean b/src/Leanc.lean index ac4753942ffe..86609af40d06 100644 --- a/src/Leanc.lean +++ b/src/Leanc.lean @@ -23,7 +23,7 @@ Beware of the licensing consequences since GMP is LGPL." let cflags := ["-I", (root / "include").toString] ++ "@LEANC_EXTRA_FLAGS@".trim.splitOn let mut cflagsInternal := "@LEANC_INTERNAL_FLAGS@".trim.splitOn let mut ldflagsInternal := "@LEANC_INTERNAL_LINKER_FLAGS@".trim.splitOn - let mut ldflags := ["-L", (root / "lib" / "lean").toString, "-lgmp"] ++ "@LEAN_EXTRA_LINKER_FLAGS@".trim.splitOn + let mut ldflags := ["-L", (root / "lib" / "lean").toString, (← IO.getEnv "LEANC_GMP").getD "-lgmp"] ++ "@LEAN_EXTRA_LINKER_FLAGS@".trim.splitOn let mut ldflagsExt := "@LEANC_STATIC_LINKER_FLAGS@".trim.splitOn for arg in args do diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index 85f33616e823..ffcb0a178c32 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -81,7 +81,8 @@ ENDFOREACH(T) add_test(NAME leancomptest_foreign WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/compiler/foreign" - COMMAND bash -c "${LEAN_BIN}/leanmake --always-make CXX='${CMAKE_CXX_COMPILER} ${LEANC_OPTS}'") + # LEANC_OPTS is necessary for macOS c++ to find its headers, GMP will be removed soon + COMMAND bash -c "LEANC_GMP=${GMP_LIBRARIES} ${LEAN_BIN}/leanmake --always-make CXX='${CMAKE_CXX_COMPILER} ${LEANC_OPTS}'") add_test(NAME leancomptest_doc_example WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../doc/examples/compiler" COMMAND bash -c "export ${TEST_VARS}; leanmake --always-make bin && ./build/bin/test hello world") From 6a0938bfa68f312b6e595c29b40f025b0cc6b2d1 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 9 Nov 2021 17:42:47 +0100 Subject: [PATCH 27/27] chore: ci: fix List Install Tree --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 512abe240c0b..8d373ae08b4c 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -148,7 +148,7 @@ jobs: - name: List Install Tree run: | # omit contents of src/, Init/, ... - tree --du -h lean-* | grep -Ev '(│.*){3}' + tree --du -h lean-* | grep -Ev '\.o?lean' - name: Pack if: ${{ startsWith(github.ref, 'refs/tags/v') && matrix.release }} run: |