diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index cb8c5302ffef..8d373ae08b4c 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}" + 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 index 813da2975673..6ff2b2040c91 100644 --- 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 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..693a75fd7d51 --- /dev/null +++ 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 index 470d6a82ce0b..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 }: +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 index 12a5a5b6cd9e..7f413e0c78a0 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,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) 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⟩ diff --git a/src/Leanc.lean b/src/Leanc.lean index 16c2b84bcbb8..86609af40d06 100644 --- a/src/Leanc.lean +++ b/src/Leanc.lean @@ -17,9 +17,13 @@ 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 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 cflagsInternal := "@LEANC_INTERNAL_FLAGS@".trim.splitOn + let mut ldflagsInternal := "@LEANC_INTERNAL_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 @@ -31,18 +35,22 @@ 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 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 ++ 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}" let child ← IO.Process.spawn { cmd := cc, args := args.toArray } diff --git a/src/bin/leanc.in b/src/bin/leanc.in index e6bb09797aff..60ae824f771b 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=(@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=() - [[ "$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 ]] && echo $cmd +eval $cmd diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h index a1212c8dad33..559a7bc30ab3 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" { @@ -45,6 +41,15 @@ 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) #else @@ -310,6 +315,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 +367,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 +1021,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/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(); +} } 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" diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index c904abe9992f..ffcb0a178c32 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,15 +76,16 @@ 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 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 "${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 +94,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 +106,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 +114,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 +123,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 +133,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 +144,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 +152,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 +163,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 +178,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 +186,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 +194,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 +202,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 +218,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")