Merge branch 'nightly-with-mathlib' of https://github.com/leanprover/lean4 into joachim/issue10794

Author: nomeata

.github/workflows/build-template.yml

@@ -3,9 +3,6 @@ name: build-template
 on:
   workflow_call:
     inputs:
-      check-level:
-        type: string
-        required: true
       config:
         type: string
         required: true
@@ -230,7 +227,7 @@ jobs:
         run: |
           ulimit -c unlimited  # coredumps
           time ctest --preset ${{ matrix.CMAKE_PRESET || 'release' }} --test-dir build/$TARGET_STAGE -j$NPROC --output-junit test-results.xml ${{ matrix.CTEST_OPTIONS }}
-        if: (matrix.wasm || !matrix.cross) && (inputs.check-level >= 1 || matrix.test)
+        if: matrix.test
       - name: Test Summary
         uses: test-summary/action@v2
         with:

.github/workflows/ci.yml

@@ -31,10 +31,6 @@ jobs:
   configure:
     runs-on: ubuntu-latest
     outputs:
-      # 0: PRs without special label
-      # 1: PRs with `merge-ci` label, merge queue checks, master commits
-      # 2: PRs with `release-ci` label, releases (incl. nightlies)
-      check-level: ${{ steps.set-level.outputs.check-level }}
       # The build matrix, dynamically generated here
       matrix: ${{ steps.set-matrix.outputs.matrix }}
       # secondary build jobs that should not block the CI success/merge queue
@@ -110,6 +106,9 @@ jobs:
           TAG_NAME="${GITHUB_REF##*/}"
           echo "RELEASE_TAG=$TAG_NAME" >> "$GITHUB_OUTPUT"
 
+      # 0: PRs without special label
+      # 1: PRs with `merge-ci` label, merge queue checks, master commits
+      # 2: PRs with `release-ci` label, releases (incl. nightlies)
       - name: Set check level
         id: set-level
         # We do not use github.event.pull_request.labels.*.name here because
@@ -152,7 +151,8 @@ jobs:
                 "name": "Linux LLVM",
                 "os": "ubuntu-latest",
                 "release": false,
-                "check-level": 2,
+                "enabled": level >= 2,
+                "test": true,
                 "shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
                 "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-linux-gnu.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
@@ -168,14 +168,15 @@ jobs:
                 "os": "ubuntu-latest",
                 "release": true,
                 // Special handling for release jobs. We want:
-                // 1. To run it in PRs so developers get PR toolchains (so secondary is sufficient)
+                // 1. To run it in PRs so developers get PR toolchains (so secondary without tests is sufficient)
                 // 2. To skip it in merge queues as it takes longer than the
                 //    Linux lake build and adds little value in the merge queue
                 // 3. To run it in release (obviously)
                 // 4. To run it for pushes to master so that pushes to master have a Linux toolchain
                 //    available as an artifact for Grove to use.
-                "check-level": (isPr || isPushToMaster) ? 0 : 2,
-                "secondary": isPr,
+                "enabled": isPr || level != 1 || isPushToMaster,
+                "test": level >= 1,
+                "secondary": level == 0,
                 "shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
                 "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-linux-gnu.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
@@ -186,10 +187,9 @@ jobs:
               {
                 "name": "Linux Lake",
                 "os": large ? "nscloud-ubuntu-22.04-amd64-8x16-with-cache" : "ubuntu-latest",
-                "check-level": 0,
+                "enabled": true,
                 "check-rebootstrap": level >= 1,
                 "check-stage3": level >= 2,
-                // only check-level >= 1 opts into tests implicitly. TODO: Clean up this logic.
                 "test": true,
                 // NOTE: `test-speedcenter` currently seems to be broken on `ubuntu-latest`
                 "test-speedcenter": large && level >= 2,
@@ -199,14 +199,16 @@ jobs:
               {
                 "name": "Linux Reldebug",
                 "os": "ubuntu-latest",
-                "check-level": 2,
+                "enabled": level >= 2,
+                "test": true,
                 "CMAKE_PRESET": "reldebug",
               },
               // TODO: suddenly started failing in CI
               /*{
                 "name": "Linux fsanitize",
                 "os": "ubuntu-latest",
-                "check-level": 2,
+                "enabled": level >= 2,
+                "test": true,
                 // turn off custom allocator & symbolic functions to make LSAN do its magic
                 "CMAKE_PRESET": "sanitize",
                 // exclude seriously slow/problematic tests (laketests crash)
@@ -217,7 +219,7 @@ jobs:
                 "os": "macos-15-intel",
                 "release": true,
                 "test": false,  // Tier 2 platform
-                "check-level": 2,
+                "enabled": level >= 2,
                 "shell": "bash -euxo pipefail {0}",
                 "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-apple-darwin.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-macos.sh lean-llvm*",
@@ -228,23 +230,25 @@ jobs:
               {
                 "name": "macOS aarch64",
                 // standard GH runner only comes with 7GB so use large runner if possible when running tests
-                "os": large && !isPr ? "nscloud-macos-sequoia-arm64-6x14" : "macos-15",
+                "os": large && level >= 1 ? "nscloud-macos-sequoia-arm64-6x14" : "macos-15",
                 "CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-darwin_aarch64",
                 "release": true,
+                "test": true,
                 "shell": "bash -euxo pipefail {0}",
                 "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-aarch64-apple-darwin.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-macos.sh lean-llvm*",
                 "binary-check": "otool -L",
                 "tar": "gtar", // https://github.com/actions/runner-images/issues/2619
                 // See "Linux release" for release job levels; Grove is not a concern here
-                "check-level": isPr ? 0 : 2,
-                "secondary": isPr,
+                "enabled": isPr || level != 1,
+                "secondary": level == 0,
               },
               {
                 "name": "Windows",
                 "os": large && level == 2 ? "namespace-profile-windows-amd64-4x16" : "windows-2022",
                 "release": true,
-                "check-level": 2,
+                "enabled": level >= 2,
+                "test": true,
                 "shell": "msys2 {0}",
                 "CMAKE_OPTIONS": "-G \"Unix Makefiles\"",
                 "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-w64-windows-gnu.tar.zst",
@@ -256,7 +260,8 @@ jobs:
                 "os": "nscloud-ubuntu-22.04-arm64-4x16",
                 "CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-linux_aarch64",
                 "release": true,
-                "check-level": 2,
+                "enabled": level >= 2,
+                "test": true,
                 "shell": "nix develop .#oldGlibcAArch -c bash -euxo pipefail {0}",
                 "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-aarch64-linux-gnu.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
@@ -269,7 +274,7 @@ jobs:
               //  "CMAKE_OPTIONS": "-DSTAGE0_USE_GMP=OFF -DSTAGE0_LEAN_EXTRA_CXX_FLAGS='-m32' -DSTAGE0_LEANC_OPTS='-m32' -DSTAGE0_MMAP=OFF -DUSE_GMP=OFF -DLEAN_EXTRA_CXX_FLAGS='-m32' -DLEANC_OPTS='-m32' -DMMAP=OFF -DLEAN_INSTALL_SUFFIX=-linux_x86 -DCMAKE_LIBRARY_PATH=/usr/lib/i386-linux-gnu/ -DSTAGE0_CMAKE_LIBRARY_PATH=/usr/lib/i386-linux-gnu/ -DPKG_CONFIG_EXECUTABLE=/usr/bin/i386-linux-gnu-pkg-config",
               //  "cmultilib": true,
               //  "release": true,
-              //  "check-level": 2,
+              //  "enabled": level >= 2,
               //  "cross": true,
               //  "shell": "bash -euxo pipefail {0}"
               //}
@@ -281,7 +286,7 @@ jobs:
               //   "wasm": true,
               //   "cmultilib": true,
               //   "release": true,
-              //   "check-level": 2,
+              //   "enabled": level >= 2,
               //   "cross": true,
               //   "shell": "bash -euxo pipefail {0}",
               //   // Just a few selected tests because wasm is slow
@@ -295,7 +300,7 @@ jobs:
               }
             }
             console.log(`matrix:\n${JSON.stringify(matrix, null, 2)}`);
-            matrix = matrix.filter((job) => level >= job["check-level"]);
+            matrix = matrix.filter((job) => job["enabled"]);
             core.setOutput('matrix', matrix.filter((job) => !job["secondary"]));
             core.setOutput('matrix-secondary', matrix.filter((job) => job["secondary"]));
 
@@ -305,7 +310,6 @@ jobs:
     uses: ./.github/workflows/build-template.yml
     with:
       config: ${{needs.configure.outputs.matrix}}
-      check-level: ${{ needs.configure.outputs.check-level }}
       nightly: ${{ needs.configure.outputs.nightly }}
       LEAN_VERSION_MAJOR: ${{ needs.configure.outputs.LEAN_VERSION_MAJOR }}
       LEAN_VERSION_MINOR: ${{ needs.configure.outputs.LEAN_VERSION_MINOR }}
@@ -321,7 +325,6 @@ jobs:
     uses: ./.github/workflows/build-template.yml
     with:
       config: ${{needs.configure.outputs.matrix-secondary}}
-      check-level: ${{ needs.configure.outputs.check-level }}
       nightly: ${{ needs.configure.outputs.nightly }}
       LEAN_VERSION_MAJOR: ${{ needs.configure.outputs.LEAN_VERSION_MAJOR }}
       LEAN_VERSION_MINOR: ${{ needs.configure.outputs.LEAN_VERSION_MINOR }}

.gitignore

@@ -20,7 +20,6 @@ tasks.json
 settings.json
 .gdb_history
 .vscode/*
-!.vscode/settings.json
 script/__pycache__
 *.produced.out
 CMakeSettings.json

lean.code-workspace

@@ -15,7 +15,8 @@
 	],
 	"settings": {
 		// Open terminal at root, not current workspace folder
-		"terminal.integrated.cwd": "${workspaceFolder:.}",
+		// (there is not way to directly refer to the root folder included as `.` above)
+		"terminal.integrated.cwd": "${workspaceFolder:src}/..",
 		"files.insertFinalNewline": true,
 		"files.trimTrailingWhitespace": true,
 		"cmake.buildDirectory": "${workspaceFolder}/build/release",

src/Init/BinderNameHint.lean

@@ -7,7 +7,6 @@ Authors: Joachim Breitner
 module
 
 prelude
-public import Init.Prelude
 public import Init.Tactics
 
 public section

src/Init/Control/EState.lean

@@ -6,8 +6,6 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Init.Control.State
-public import Init.Control.Except
 public import Init.Data.ToString.Basic
 
 public section

src/Init/Control/Except.lean

@@ -10,7 +10,6 @@ module
 prelude
 public import Init.Control.Basic
 public import Init.Control.Id
-public import Init.Coe
 
 @[expose] public section
 

src/Init/Control/Lawful/Basic.lean

@@ -7,8 +7,6 @@ module
 
 prelude
 public import Init.Ext
-public import Init.SimpLemmas
-public import Init.Meta
 
 public section
 

src/Init/Control/Lawful/Instances.lean

@@ -7,14 +7,11 @@ module
 
 prelude
 public import Init.Control.Lawful.Basic
-public import Init.Control.Except
 import all Init.Control.Except
 public import Init.Control.Option
 import all Init.Control.Option
-public import Init.Control.State
 import all Init.Control.State
 public import Init.Control.StateRef
-public import Init.Ext
 
 public section
 

src/Init/Control/Lawful/Lemmas.lean

@@ -7,7 +7,6 @@ module
 
 prelude
 public import Init.Control.Lawful.Basic
-public import Init.RCases
 public import Init.ByCases
 
 public section