Merge branch 'master' into bug/macos-linker-failure

leanprover · Jun 28, 2024 · 527a65e · 527a65e
2 parents 7e5488e + 30a922a
commit 527a65e
Show file tree

Hide file tree

Showing 1,139 changed files with 790,624 additions and 211,825 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -122,9 +122,8 @@ jobs:
           script: |
             const level = ${{ steps.set-level.outputs.check-level }};
             console.log(`level: ${level}`);
-            // use large runners outside PRs where available (original repo)
-            // disabled for now as this mostly just speeds up the test suite which is not a bottleneck
-            // let large = ${{ github.event_name != 'pull_request' && github.repository == 'leanprover/lean4' }} ? "-large" : "";
+            // use large runners where available (original repo)
+            let large = ${{ github.repository == 'leanprover/lean4' }};
             let matrix = [
               {
                 // portable release build: use channel with older glibc (2.27)
@@ -143,7 +142,7 @@ jobs:
               },
               {
                 "name": "Linux release",
-                "os": "ubuntu-latest",
+                "os": large ? "nscloud-ubuntu-22.04-amd64-4x8" : "ubuntu-latest",
                 "release": true,
                 "check-level": 0,
                 "shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
@@ -155,7 +154,7 @@ jobs:
               },
               {
                 "name": "Linux",
-                "os": "ubuntu-latest",
+                "os": large ? "nscloud-ubuntu-22.04-amd64-4x8" : "ubuntu-latest",
                 "check-stage3": level >= 2,
                 "test-speedcenter": level >= 2,
                 "check-level": 1,
@@ -281,16 +280,8 @@ jobs:
       CXX: c++
       MACOSX_DEPLOYMENT_TARGET: 10.15
     steps:
-      - name: Checkout
-        uses: actions/checkout@v3
-        with:
-          submodules: true
-          # the default is to use a virtual merge commit between the PR and master: just use the PR
-          ref: ${{ github.event.pull_request.head.sha }}
       - name: Install Nix
-        uses: cachix/install-nix-action@v18
-        with:
-          install_url: https://releases.nixos.org/nix/nix-2.12.0/install
+        uses: DeterminateSystems/nix-installer-action@main
         if: runner.os == 'Linux' && !matrix.cmultilib
       - name: Install MSYS2
         uses: msys2/setup-msys2@v2
@@ -303,6 +294,20 @@ jobs:
         run: |
           brew install ccache tree zstd coreutils gmp
         if: runner.os == 'macOS'
+      - name: Checkout
+        uses: actions/checkout@v4
+        with:
+          # the default is to use a virtual merge commit between the PR and master: just use the PR
+          ref: ${{ github.event.pull_request.head.sha }}
+      # Do check out some CI-relevant files from virtual merge commit to accommodate CI changes on
+      # master (as the workflow files themselves are always taken from the merge)
+      # (needs to be after "Install *" to use the right shell)
+      - name: CI Merge Checkout
+        run: |
+          git fetch --depth=1 origin ${{ github.sha }}
+          git checkout FETCH_HEAD flake.nix flake.lock
+        if: github.event_name == 'pull_request'
+      # (needs to be after "Checkout" so files don't get overriden)
       - name: Setup emsdk
         uses: mymindstorm/setup-emsdk@v12
         with:
@@ -318,20 +323,14 @@ jobs:
         uses: actions/cache@v3
         with:
           path: .ccache
-          key: ${{ matrix.name }}-build-v3-${{ github.sha }}
+          key: ${{ matrix.name }}-build-v3-${{ github.event.pull_request.head.sha }}
           # fall back to (latest) previous cache
           restore-keys: |
             ${{ matrix.name }}-build-v3
+      # open nix-shell once for initial setup
       - name: Setup
         run: |
-          # open nix-shell once for initial setup
-          true
-        if: runner.os == 'Linux'
-      - name: Set up core dumps
-        run: |
-          mkdir -p $PWD/coredumps
-          # store in current directory, for easy uploading together with binary
-          echo $PWD/coredumps/%e.%p.%t | sudo tee /proc/sys/kernel/core_pattern
+          ccache --zero-stats
         if: runner.os == 'Linux'
       - name: Set up NPROC
         run: |
@@ -340,7 +339,6 @@ jobs:
         run: |
           mkdir build
           cd build
-          ulimit -c unlimited # coredumps
           # arguments passed to `cmake`
           # this also enables githash embedding into stage 1 library
           OPTIONS=(-DCHECK_OLEAN_VERSION=ON)
@@ -367,8 +365,10 @@ jobs:
           fi
           # contortion to support empty OPTIONS with old macOS bash
           cmake .. --preset ${{ matrix.CMAKE_PRESET || 'release' }} -B . ${{ matrix.CMAKE_OPTIONS }} ${OPTIONS[@]+"${OPTIONS[@]}"} -DLEAN_INSTALL_PREFIX=$PWD/..
-          make -j$NPROC
-          make install
+          time make -j$NPROC
+      - name: Install
+        run: |
+          make -C build install
       - name: Check Binaries
         run: ${{ matrix.binary-check }} lean-*/bin/* || true
       - name: List Install Tree
@@ -398,8 +398,7 @@ jobs:
       - name: Test
         id: test
         run: |
-          ulimit -c unlimited # coredumps
-          ctest --preset ${{ matrix.CMAKE_PRESET || 'release' }} --test-dir build/stage1 -j$NPROC --output-junit test-results.xml ${{ matrix.CTEST_OPTIONS }}
+          time ctest --preset ${{ matrix.CMAKE_PRESET || 'release' }} --test-dir build/stage1 -j$NPROC --output-junit test-results.xml ${{ matrix.CTEST_OPTIONS }}
         if: (matrix.wasm || !matrix.cross) && needs.configure.outputs.check-level >= 1
       - name: Test Summary
         uses: test-summary/action@v2
@@ -412,51 +411,28 @@ jobs:
         if: (!matrix.cross) && steps.test.conclusion != 'skipped'
       - name: Build Stage 2
         run: |
-          ulimit -c unlimited # coredumps
           make -C build -j$NPROC stage2
         if: matrix.test-speedcenter
       - name: Check Stage 3
         run: |
-          ulimit -c unlimited # coredumps
           make -C build -j$NPROC stage3
         if: matrix.test-speedcenter
       - name: Test Speedcenter Benchmarks
         run: |
-          echo -1 | sudo tee /proc/sys/kernel/perf_event_paranoid
+          # Necessary for some timing metrics but does not work on Namespace runners
+          # and we just want to test that the benchmarks run at all here
+          #echo -1 | sudo tee /proc/sys/kernel/perf_event_paranoid
           export BUILD=$PWD/build PATH=$PWD/build/stage1/bin:$PATH
           cd tests/bench
           nix shell .#temci -c temci exec --config speedcenter.yaml --included_blocks fast --runs 1
         if: matrix.test-speedcenter
       - name: Check rebootstrap
         run: |
-          ulimit -c unlimited # coredumps
           # clean rebuild in case of Makefile changes
           make -C build update-stage0 && rm -rf build/stage* && make -C build -j$NPROC
         if: matrix.name == 'Linux' && needs.configure.outputs.check-level >= 1
       - name: CCache stats
         run: ccache -s
-      - name: Show stacktrace for coredumps
-        if: ${{ failure() && runner.os == 'Linux' }}
-        run: |
-          for c in coredumps/*; do
-            progbin="$(file $c | sed "s/.*execfn: '\([^']*\)'.*/\1/")"
-            echo bt | $GDB/bin/gdb -q $progbin $c || true
-          done
-      # has not been used in a long while, would need to be adapted to new
-      # shared libs
-      #- name: Upload coredumps
-      #  uses: actions/upload-artifact@v3
-      #  if: ${{ failure() && runner.os == 'Linux' }}
-      #  with:
-      #    name: coredumps-${{ matrix.name }}
-      #    path: |
-      #      ./coredumps
-      #      ./build/stage0/bin/lean
-      #      ./build/stage0/lib/lean/libleanshared.so
-      #      ./build/stage1/bin/lean
-      #      ./build/stage1/lib/lean/libleanshared.so
-      #      ./build/stage2/bin/lean
-      #      ./build/stage2/lib/lean/libleanshared.so
 
   # This job collects results from all the matrix jobs
   # This can be made the “required” job, instead of listing each
@@ -491,6 +467,7 @@ jobs:
         with:
           files: artifacts/*/*
           fail_on_unmatched_files: true
+          prerelease: ${{ !startsWith(github.ref, 'refs/tags/v') || contains(github.ref, '-rc') }}
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
 

diff --git a/.github/workflows/nix-ci.yml b/.github/workflows/nix-ci.yml
@@ -13,18 +13,36 @@ concurrency:
   cancel-in-progress: true
 
 jobs:
+  # see ci.yml
+  configure:
+    runs-on: ubuntu-latest
+    outputs:
+      matrix: ${{ steps.set-matrix.outputs.result }}
+    steps:
+      - name: Configure build matrix
+        id: set-matrix
+        uses: actions/github-script@v7
+        with:
+          script: |
+            let large = ${{ github.repository == 'leanprover/lean4' }};
+            let matrix = [
+              {
+                "name": "Nix Linux",
+                "os": large ? "nscloud-ubuntu-22.04-amd64-8x8" : "ubuntu-latest",
+              }
+            ];
+            console.log(`matrix:\n${JSON.stringify(matrix, null, 2)}`);
+            return matrix;
+
   Build:
+    needs: [configure]
     runs-on: ${{ matrix.os }}
     defaults:
       run:
         shell: nix run .#ciShell -- bash -euxo pipefail {0}
     strategy:
       matrix:
-        include:
-          - name: Nix Linux
-            os: ubuntu-latest
-          #- name: Nix macOS
-          #  os: macos-latest
+        include: ${{fromJson(needs.configure.outputs.matrix)}}
       # complete all jobs
       fail-fast: false
     name: ${{ matrix.name }}

diff --git a/.gitignore b/.gitignore
@@ -4,8 +4,10 @@
 *.lock
 .lake
 lake-manifest.json
-build
-!/src/lake/Lake/Build
+/build
+/src/lakefile.toml
+/tests/lakefile.toml
+/lakefile.toml
 GPATH
 GRTAGS
 GSYMS

diff --git a/doc/char.md b/doc/char.md
@@ -1 +1,11 @@
 # Characters
+
+A value of type `Char`, also known as a character, is a [Unicode scalar value](https://www.unicode.org/glossary/#unicode_scalar_value). It is represented using an unsigned 32-bit integer and is statically guaranteed to be a valid Unicode scalar value.
+
+Syntactically, character literals are enclosed in single quotes.
+```lean
+#eval 'a' -- 'a'
+#eval '∀' -- '∀'
+```
+
+Characters are ordered and can be decidably compared using the relational operators `=`, `<`, `≤`, `>`, `≥`.
diff --git a/doc/examples/compiler/.gitignore b/doc/examples/compiler/.gitignore
@@ -0,0 +1 @@
+build
diff --git a/flake.nix b/flake.nix
@@ -35,26 +35,28 @@
       lean-packages = pkgs.callPackage (./nix/packages.nix) { src = ./.; inherit nix lean4-mode; };
 
       devShellWithDist = pkgsDist: pkgs.mkShell.override {
-	  stdenv = pkgs.overrideCC pkgs.stdenv lean-packages.llvmPackages.clang;
-	} ({
-	  buildInputs = with pkgs; [
-	    cmake gmp ccache
-	    lean-packages.llvmPackages.llvm  # llvm-symbolizer for asan/lsan
-	    # TODO: only add when proven to not affect the flakification
-	    #pkgs.python3
-	  ];
-	  # https://github.com/NixOS/nixpkgs/issues/60919
-	  hardeningDisable = [ "all" ];
-	  # more convenient `ctest` output
-	  CTEST_OUTPUT_ON_FAILURE = 1;
-	} // pkgs.lib.optionalAttrs pkgs.stdenv.isLinux {
-	  GMP = pkgsDist.gmp.override { withStatic = true; };
-	  GLIBC = pkgsDist.glibc;
-	  GLIBC_DEV = pkgsDist.glibc.dev;
-	  GCC_LIB = pkgsDist.gcc.cc.lib;
-	  ZLIB = pkgsDist.zlib;
-	  GDB = pkgsDist.gdb;
-	});
+          stdenv = pkgs.overrideCC pkgs.stdenv lean-packages.llvmPackages.clang;
+        } ({
+          buildInputs = with pkgs; [
+            cmake gmp ccache
+            lean-packages.llvmPackages.llvm  # llvm-symbolizer for asan/lsan
+            gdb
+            # TODO: only add when proven to not affect the flakification
+            #pkgs.python3
+            tree  # for CI
+          ];
+          # https://github.com/NixOS/nixpkgs/issues/60919
+          hardeningDisable = [ "all" ];
+          # more convenient `ctest` output
+          CTEST_OUTPUT_ON_FAILURE = 1;
+        } // pkgs.lib.optionalAttrs pkgs.stdenv.isLinux {
+          GMP = pkgsDist.gmp.override { withStatic = true; };
+          GLIBC = pkgsDist.glibc;
+          GLIBC_DEV = pkgsDist.glibc.dev;
+          GCC_LIB = pkgsDist.gcc.cc.lib;
+          ZLIB = pkgsDist.zlib;
+          GDB = pkgsDist.gdb;
+        });
     in {
       packages = lean-packages // rec {
         debug = lean-packages.override { debug = true; };

diff --git a/nix/bootstrap.nix b/nix/bootstrap.nix
@@ -87,15 +87,17 @@ rec {
         leanFlags = [ "-DwarningAsError=true" ];
       } // args);
       Init' = build { name = "Init"; deps = []; };
-      Lean' = build { name = "Lean"; deps = [ Init' ]; };
+      Std' = build { name = "Std"; deps = [ Init' ]; };
+      Lean' = build { name = "Lean"; deps = [ Std' ]; };
       attachSharedLib = sharedLib: pkg: pkg // {
         inherit sharedLib;
         mods = mapAttrs (_: m: m // { inherit sharedLib; propagatedLoadDynlibs = []; }) pkg.mods;
       };
     in (all: all // all.lean) rec {
       inherit (Lean) emacs-dev emacs-package vscode-dev vscode-package;
       Init = attachSharedLib leanshared Init';
-      Lean = attachSharedLib leanshared Lean' // { allExternalDeps = [ Init ]; };
+      Std = attachSharedLib leanshared Std' // { allExternalDeps = [ Init ]; };
+      Lean = attachSharedLib leanshared Lean' // { allExternalDeps = [ Std ]; };
       Lake = build {
         name = "Lake";
         src = src + "/src/lake";
@@ -109,29 +111,22 @@ rec {
         linkFlags = lib.optional stdenv.isLinux "-rdynamic";
         src = src + "/src/lake";
       };
-      stdlib = [ Init Lean Lake ];
+      stdlib = [ Init Std Lean Lake ];
       modDepsFiles = symlinkJoin { name = "modDepsFiles"; paths = map (l: l.modDepsFile) (stdlib ++ [ Leanc ]); };
       depRoots = symlinkJoin { name = "depRoots"; paths = map (l: l.depRoots) stdlib; };
       iTree = symlinkJoin { name = "ileans"; paths = map (l: l.iTree) stdlib; };
       Leanc = build { name = "Leanc"; src = lean-bin-tools-unwrapped.leanc_src; deps = stdlib; roots = [ "Leanc" ]; };
-      stdlibLinkFlags = "-L${Init.staticLib} -L${Lean.staticLib} -L${Lake.staticLib} -L${leancpp}/lib/lean";
+      stdlibLinkFlags = "${lib.concatMapStringsSep " " (l: "-L${l.staticLib}") stdlib} -L${leancpp}/lib/lean";
       libInit_shared = runCommand "libInit_shared" { buildInputs = [ stdenv.cc ]; libName = "libInit_shared${stdenv.hostPlatform.extensions.sharedLibrary}"; } ''
         mkdir $out
-        LEAN_CC=${stdenv.cc}/bin/cc ${lean-bin-tools-unwrapped}/bin/leanc -shared ${lib.optionalString stdenv.isLinux "-Wl,-Bsymbolic"} \
-          ${if stdenv.isDarwin
-            then "-Wl,-force_load,${Init.staticLib}/libInit.a -Wl,-force_load,${Lean.staticLib}/libLean.a -lleancpp -Wl,-force_load,${leancpp}/lib/lean/libleancpp.a ${leancpp}/lib/libleanrt_initial-exec.a -lc++"
-            else "-Wl,--whole-archive -lInit ${leancpp}/lib/libleanrt_initial-exec.a -Wl,--no-whole-archive -lstdc++"} \
-          -lm ${stdlibLinkFlags} \
-          $(${llvmPackages.libllvm.dev}/bin/llvm-config --ldflags --libs) \
-          -o $out/$libName
+        touch empty.c
+        ${stdenv.cc}/bin/cc -shared -o $out/$libName empty.c
       '';
       leanshared = runCommand "leanshared" { buildInputs = [ stdenv.cc ]; libName = "libleanshared${stdenv.hostPlatform.extensions.sharedLibrary}"; } ''
         mkdir $out
         LEAN_CC=${stdenv.cc}/bin/cc ${lean-bin-tools-unwrapped}/bin/leanc -shared ${lib.optionalString stdenv.isLinux "-Wl,-Bsymbolic"} \
-          ${if stdenv.isDarwin
-            then "-Wl,-force_load,${libInit_shared}/* -lLean -Wl,-force_load,${Lean.staticLib}/libLean.a -lleancpp -Wl,-force_load,${leancpp}/lib/lean/libleancpp.a ${leancpp}/lib/libleanrt_initial-exec.a -lc++"
-            else "${libInit_shared}/* -Wl,--whole-archive -lLean -lleancpp -Wl,--no-whole-archive -lstdc++"} \
-          -lm ${stdlibLinkFlags} \
+          ${if stdenv.isDarwin then "-Wl,-force_load,${Init.staticLib}/libInit.a -Wl,-force_load,${Lean.staticLib}/libLean.a -Wl,-force_load,${leancpp}/lib/lean/libleancpp.a ${leancpp}/lib/libleanrt_initial-exec.a -lc++"
+            else "-Wl,--whole-archive -lInit -lStd -lLean -lleancpp ${leancpp}/lib/libleanrt_initial-exec.a -Wl,--no-whole-archive -lstdc++"} -lm ${stdlibLinkFlags} \
           $(${llvmPackages.libllvm.dev}/bin/llvm-config --ldflags --libs) \
           -o $out/$libName
       '';
@@ -157,11 +152,9 @@ rec {
         '';
         meta.mainProgram = "lean";
       };
-      cacheRoots = linkFarmFromDrvs "cacheRoots" [
+      cacheRoots = linkFarmFromDrvs "cacheRoots" ([
         stage0 lean leanc lean-all iTree modDepsFiles depRoots Leanc.src
-        # .o files are not a runtime dependency on macOS because of lack of thin archives
-        Lean.oTree Lake.oTree
-      ];
+      ] ++ map (lib: lib.oTree) stdlib);
       test = buildCMake {
         name = "lean-test-${desc}";
         realSrc = lib.sourceByRegex src [ "src.*" "tests.*" ];
@@ -176,15 +169,15 @@ rec {
           ln -sf ${lean-all}/* .
         '';
         buildPhase = ''
-          ctest --output-junit test-results.xml --output-on-failure -E 'leancomptest_(doc_example|foreign)|leanlaketest_init' -j$NIX_BUILD_CORES
+          ctest --output-junit test-results.xml --output-on-failure -E 'leancomptest_(doc_example|foreign)' -j$NIX_BUILD_CORES
         '';
         installPhase = ''
           mkdir $out
           mv test-results.xml $out
         '';
       };
       update-stage0 =
-        let cTree = symlinkJoin { name = "cs"; paths = [ Init.cTree Lean.cTree ]; }; in
+        let cTree = symlinkJoin { name = "cs"; paths = map (lib: lib.cTree) stdlib; }; in
         writeShellScriptBin "update-stage0" ''
           CSRCS=${cTree} CP_C_PARAMS="--dereference --no-preserve=all" ${src + "/script/lib/update-stage0"}
         '';