leanprover · Kha · Oct 11, 2021 · Oct 13, 2021 · Oct 18, 2021 · Sep 8, 2021
@@ -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}"
+            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
             check-stage3: true
@@ -73,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 zip unzip diffutils binutils tree mingw-w64-x86_64-zstd
         if: matrix.os == 'windows-2022'
       - name: Install Brew Packages
         run: |
-          brew install ccache
+          brew install ccache tree zstd
         if: matrix.os == 'macos-latest'
       - name: Cache
         uses: actions/cache@v2
@@ -100,35 +101,29 @@ 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 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
             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[@]}"} -DLEAN_INSTALL_PREFIX=$PWD/..
           make -j4
-      # de-Nix-ify binaries
-      - name: Patch
+          make install
+      - 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 lean-*/bin/* || true
       - name: Patch
         if: matrix.name == 'macOS'
         run: |
@@ -150,17 +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 '\.o?lean'
       - name: Pack
-        run: cd build/stage1; cpack
+        if: ${{ startsWith(github.ref, 'refs/tags/v') && matrix.release }}
+        run: |
+          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/LICENSE b/LICENSE
@@ -1,3 +1,8 @@
+==============================================================================
+See LICENSES for licenses of redistributed projects.
+The Lean project is under the Apache License 2.0:
+==============================================================================
+
 Apache License 2.0 (Apache)
 Apache License
 Version 2.0, January 2004
@@ -68,4 +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.
-
diff --git 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
@@ -0,0 +1,40 @@
+#!/usr/bin/env bash
+set -uo pipefail
+
+# 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)
+# ```
+
+# 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/{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`
+$CP $GLIBC/lib/crt* llvm/lib/
+$CP $GLIBC/lib/crt* stage1/lib/
+# runtime
+(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
+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_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 -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 -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/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, pkgsDist ? pkgs, llvmPackages ? null }:
 # use `shell` as default
 (attribs: attribs.shell // attribs) rec {
   shell = pkgs.mkShell.override {
@@ -13,6 +13,9 @@ in { pkgs ? flakePkgs.nixpkgs, llvmPackages ? null }:
     hardeningDisable = [ "all" ];
     # more convenient `ctest` output
     CTEST_OUTPUT_ON_FAILURE = 1;
+    GMP = pkgsDist.gmp.override { withStatic = true; };
+    GLIBC = pkgsDist.glibc;
+    ZLIB = pkgsDist.zlib;
     shellHook = ''
       export LEAN_SRC_PATH="$PWD/src"
     '';

diff --git 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,12 +277,20 @@ else()
   set(LEANC_STATIC_LINKER_FLAGS "-Wl,--start-group -lleancpp -lLean -Wl,--end-group -Wl,--start-group -lInit -lStd -lleanrt -Wl,--end-group")
 endif()
 
+set(LEAN_CXX_STDLIB "-lstdc++" CACHE STRING "C++ stdlib linker flags")
+
 if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
-  set(LEANC_STATIC_LINKER_FLAGS "${LEANC_STATIC_LINKER_FLAGS} -lc++")
-  set(LEANSHARED_LINKER_FLAGS "${LEANSHARED_LINKER_FLAGS} -lc++")
+  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}")
+
+# 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(LEANC_STATIC_LINKER_FLAGS "${LEANC_STATIC_LINKER_FLAGS} -lstdc++")
-  set(LEANSHARED_LINKER_FLAGS "${LEANSHARED_LINKER_FLAGS} -lstdc++")
+  set(LEANSHARED_LINKER_FLAGS "${LEANSHARED_LINKER_FLAGS} -Wl,--gc-sections")
 endif()
 
 set(LEANC_STATIC_LINKER_FLAGS "${LEANC_STATIC_LINKER_FLAGS} -lm")
@@ -294,15 +303,16 @@ 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")
-  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"))
@@ -375,9 +385,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
@@ -386,7 +396,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()
@@ -516,7 +526,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\")")
 
@@ -526,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")
 
@@ -544,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)
@@ -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⟩