Merge branch 'master' of github.com:leanprover/lean4 into joachim/wf-…

…hint-elab

.github/workflows/ci.yml

@@ -132,15 +132,15 @@ jobs:
             # exclude seriously slow/problematic tests (laketests crash)
             CTEST_OPTIONS: -E 'interactivetest|leanpkgtest|laketest|benchtest'
           - name: macOS
-            os: macos-11
+            os: macos-latest
             release: true
             shell: bash -euxo pipefail {0}
             llvm-url: https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-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
           - name: macOS aarch64
-            os: macos-11
+            os: macos-latest
             release: true
             cross: true
             shell: bash -euxo pipefail {0}
@@ -223,7 +223,7 @@ jobs:
       - name: Install Brew Packages
         run: |
           brew install ccache tree zstd coreutils gmp
-        if: matrix.os == 'macos-11'
+        if: matrix.os == 'macos-latest'
       - name: Setup emsdk
         uses: mymindstorm/setup-emsdk@v12
         with:
@@ -259,7 +259,8 @@ jobs:
           mkdir build
           cd build
           ulimit -c unlimited # coredumps
-          OPTIONS=()
+          # this also enables githash embedding into stage 1 library
+          OPTIONS=(-DCHECK_OLEAN_VERSION=ON)
           if [[ -n '${{ matrix.prepare-llvm }}' ]]; then
             wget -q ${{ matrix.llvm-url }}
             PREPARE="$(${{ matrix.prepare-llvm }})"
@@ -363,6 +364,21 @@ jobs:
             ./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
+  # matrix job separately
+  all-done:
+    name: Build matrix complete
+    runs-on: ubuntu-latest
+    needs: build
+    if: ${{ always() }}
+    steps:
+    - if: contains(needs.*.result, 'failure') ||  contains(needs.*.result, 'cancelled')
+      uses: actions/github-script@v3
+      with:
+        script: |
+            core.setFailed('Some jobs failed')
+
   # This job creates releases from tags
   # (whether they are "unofficial" releases for experiments, or official releases when the tag is "v" followed by a semver string.)
   # We do not attempt to automatically construct a changelog here:

.github/workflows/pr-release.yml

@@ -84,7 +84,6 @@ jobs:
         id: most-recent-nightly-tag
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         run: |
-          git remote add nightly https://foo:'${{ secrets.PUSH_NIGHTLY_TOKEN }}'@github.com/${{ github.repository_owner }}/lean4-nightly.git
           echo "MOST_RECENT_NIGHTLY=$(script/most-recent-nightly-tag.sh)" >> $GITHUB_ENV
 
       - name: 'Setup jq'

.github/workflows/pr-title.yml

@@ -0,0 +1,20 @@
+name: Check PR title for commit convention
+
+on:
+  merge_group:
+  pull_request:
+    types: [opened, synchronize, reopened, edited]
+
+jobs:
+  check-pr-title:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Check PR title
+        uses: actions/github-script@v6
+        with:
+          script: |
+            const msg = context.payload.pull_request? context.payload.pull_request.title : context.payload.merge_group.head_commit.message;
+            console.log(`Message: ${msg}`)
+            if (!/^(feat|fix|doc|style|refactor|test|chore|perf): .*[^.]($|\n\n)/.test(msg)) {
+              core.setFailed('PR title does not follow the Commit Convention (https://leanprover.github.io/lean4/doc/dev/commit_convention.html).');
+            }

CMakeLists.txt

@@ -11,7 +11,7 @@ foreach(var ${vars})
     list(APPEND STAGE0_ARGS "-D${CMAKE_MATCH_1}=${${var}}")
   elseif("${currentHelpString}" MATCHES "No help, variable specified on the command line." OR "${currentHelpString}" STREQUAL "")
     list(APPEND CL_ARGS "-D${var}=${${var}}")
-    if("${var}" STREQUAL "USE_GMP")
+    if("${var}" MATCHES "USE_GMP|CHECK_OLEAN_VERSION")
       # must forward options that generate incompatible .olean format
       list(APPEND STAGE0_ARGS "-D${var}=${${var}}")
     endif()
@@ -35,6 +35,8 @@ ExternalProject_add(stage0
   SOURCE_SUBDIR src
   BINARY_DIR stage0
   # do not rebuild stage0 when git hash changes; it's not from this commit anyway
+  # (however, `CHECK_OLEAN_VERSION=ON` in CI will override this as we need to
+  # embed the githash into the stage 1 library built by stage 0)
   CMAKE_ARGS -DSTAGE=0 -DUSE_GITHASH=OFF ${PLATFORM_ARGS} ${STAGE0_ARGS}
   BUILD_ALWAYS ON  # cmake doesn't auto-detect changes without a download method
   INSTALL_COMMAND ""  # skip install

RELEASES.md

@@ -19,6 +19,13 @@ v4.4.0 (development in progress)
 * Lean and Lake now properly support non-identifier library names (e.g., `lake new 123-hello` and `import «123Hello»` now work correctly). See issue [#2865](https://github.com/leanprover/lean4/issue/2865) and PR [#2889](https://github.com/leanprover/lean4/pull/2888).
 * Lake now filters the environment extensions loaded from a compiled configuration (`lakefile.olean`) to include only those relevant to Lake's workspace loading process. This resolves segmentation faults caused by environment extension type mismatches (e.g., when defining custom elaborators via `elab` in configurations). See issue [#2632](https://github.com/leanprover/lean4/issue/2632) and PR [#2896](https://github.com/leanprover/lean4/pull/2896).
 
+* Cloud releases will now properly be re-unpacked if the build directory is removed. See PR [#2928](https://github.com/leanprover/lean4/pull/2928).
+* Lake's `math` template has been simplified. See PR [#2930](https://github.com/leanprover/lean4/pull/2930).
+* `lake exe <target>` now parses `target` like a build target (as the help text states it should) rather than as a basic name. For example, `lake exe @mathlib/runLinter` should now work. See PR [#2932](https://github.com/leanprover/lean4/pull/2932).
+* `lake new foo.bar [std]` now generates executables named `foo-bar` and `lake new foo.bar exe` properly creates `foo/bar.lean`. See PR [#2932](https://github.com/leanprover/lean4/pull/2932).
+* Later packages and libraries in the dependency tree are now preferred over earlier ones. That is, the later ones "shadow" the earlier ones. Such an ordering is more consistent with how declarations generally work in programming languages. This will break any package that relied on the previous ordering. See issue [#2548](https://github.com/leanprover/lean4/issues/2548) and PR [#2937](https://github.com/leanprover/lean4/pull/2937).
+* Executable roots are no longer mistakenly treated as importable. They will no longer be picked up by `findModule?`. See PR [#2937](https://github.com/leanprover/lean4/pull/2937).
+
 v4.3.0
 ---------
 

nix/lake-dev.in

@@ -10,7 +10,7 @@ function pebkac() {
 [[ $# -gt 0 ]] || pebkac
 case $1 in
     --version)
-        # minimum version for `lake server` with fallback
+        # minimum version for `lake serve` with fallback
         echo 3.1.0
         ;;
     print-paths)

src/CMakeLists.txt

@@ -64,7 +64,7 @@ option(BSYMBOLIC "Link with -Bsymbolic to reduce call overhead in shared librari
 option(USE_GMP "USE_GMP" ON)
 
 # development-specific options
-option(CHECK_OLEAN_VERSION "Only load .olean files compiled with the current version of Lean" ON)
+option(CHECK_OLEAN_VERSION "Only load .olean files compiled with the current version of Lean" OFF)
 
 set(LEAN_EXTRA_MAKE_OPTS  ""                           CACHE STRING "extra options to lean --make")
 set(LEANC_CC              ${CMAKE_C_COMPILER}          CACHE STRING "C compiler to use in `leanc`")
@@ -93,8 +93,9 @@ if ("${RUNTIME_STATS}" MATCHES "ON")
   string(APPEND LEAN_EXTRA_CXX_FLAGS " -D LEAN_RUNTIME_STATS")
 endif()
 
-if (NOT("${CHECK_OLEAN_VERSION}" MATCHES "ON"))
-  string(APPEND LEAN_EXTRA_CXX_FLAGS " -D LEAN_IGNORE_OLEAN_VERSION")
+if ("${CHECK_OLEAN_VERSION}" MATCHES "ON")
+  set(USE_GITHASH ON)
+  string(APPEND LEAN_EXTRA_CXX_FLAGS " -D LEAN_CHECK_OLEAN_VERSION")
 endif()
 
 if(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
@@ -401,26 +402,17 @@ if(MULTI_THREAD AND NOT MSVC AND (NOT ("${CMAKE_SYSTEM_NAME}" MATCHES "Darwin"))
 endif()
 
 # Git HASH
-set(LEAN_PACKAGE_VERSION "NOT-FOUND")
 if(USE_GITHASH)
   include(GetGitRevisionDescription)
   get_git_head_revision(GIT_REFSPEC GIT_SHA1)
   if(${GIT_SHA1} MATCHES "GITDIR-NOTFOUND")
     message(STATUS "Failed to read git_sha1")
     set(GIT_SHA1 "")
-    if(EXISTS "${LEAN_SOURCE_DIR}/bin/package_version")
-      file(STRINGS "${LEAN_SOURCE_DIR}/bin/package_version" LEAN_PACKAGE_VERSION)
-      message(STATUS "Package version detected: ${LEAN_PACKAGE_VERSION}")
-    endif()
   else()
     message(STATUS "git commit sha1: ${GIT_SHA1}")
   endif()
 else()
   set(GIT_SHA1 "")
-  if(EXISTS "${LEAN_SOURCE_DIR}/bin/package_version")
-    file(STRINGS "${LEAN_SOURCE_DIR}/bin/package_version" LEAN_PACKAGE_VERSION)
-    message(STATUS "Package version detected: ${LEAN_PACKAGE_VERSION}")
-  endif()
 endif()
 configure_file("${LEAN_SOURCE_DIR}/githash.h.in" "${LEAN_BINARY_DIR}/githash.h")
 

src/Init/Data/Array/Basic.lean

@@ -468,6 +468,9 @@ def elem [BEq α] (a : α) (as : Array α) : Bool :=
     else
       (true, r)
 
+/-- Convert a `Array α` into an `List α`. This is O(n) in the size of the array.  -/
+-- This function is exported to C, where it is called by `Array.data`
+-- (the projection) to implement this functionality.
 @[export lean_array_to_list]
 def toList (as : Array α) : List α :=
   as.foldr List.cons []

src/Init/Prelude.lean

@@ -2548,13 +2548,22 @@ is not observable from lean code. Arrays perform best when unshared; as long
 as they are used "linearly" all updates will be performed destructively on the
 array, so it has comparable performance to mutable arrays in imperative
 programming languages.
+
+From the point of view of proofs `Array α` is just a wrapper around `List α`.
 -/
 structure Array (α : Type u) where
-  /-- Convert a `List α` into an `Array α`. This function is overridden
-  to `List.toArray` and is O(n) in the length of the list. -/
+  /--
+  Converts a `List α` into an `Array α`.
+
+  At runtime, this constructor is implemented by `List.toArray` and is O(n) in the length of the
+  list.
+  -/
   mk ::
-  /-- Convert an `Array α` into a `List α`. This function is overridden
-  to `Array.toList` and is O(n) in the length of the list. -/
+  /--
+  Converts a `Array α` into an `List α`.
+
+  At runtime, this projection is implemented by `Array.toList` and is O(n) in the length of the
+  array. -/
   data : List α
 
 attribute [extern "lean_array_data"] Array.data
@@ -2702,12 +2711,9 @@ def List.redLength : List α → Nat
   | nil       => 0
   | cons _ as => as.redLength.succ
 
-/--
-Convert a `List α` into an `Array α`. This is O(n) in the length of the list.
-
-This function is exported to C, where it is called by `Array.mk`
-(the constructor) to implement this functionality.
--/
+/-- Convert a `List α` into an `Array α`. This is O(n) in the length of the list.  -/
+-- This function is exported to C, where it is called by `Array.mk`
+-- (the constructor) to implement this functionality.
 @[inline, match_pattern, export lean_list_to_array]
 def List.toArray (as : List α) : Array α :=
   as.toArrayAux (Array.mkEmpty as.redLength)

src/Lean/Data/KVMap.lean

@@ -190,6 +190,16 @@ def subsetAux : List (Name × DataValue) → KVMap → Bool
 def subset : KVMap → KVMap → Bool
   | ⟨m₁⟩, m₂ => subsetAux m₁ m₂
 
+def mergeBy (mergeFn : Name → DataValue → DataValue → DataValue) (l r : KVMap)
+    : KVMap := Id.run do
+  let mut result := l
+  for ⟨k, vᵣ⟩ in r do
+    if let some vₗ := result.find k then
+      result := result.insert k (mergeFn k vₗ vᵣ)
+    else
+      result := result.insert k vᵣ
+  return result
+
 def eqv (m₁ m₂ : KVMap) : Bool :=
   subset m₁ m₂ && subset m₂ m₁
 

src/Lean/Data/NameTrie.lean

@@ -69,4 +69,10 @@ def NameTrie.forMatchingM [Monad m] (t : NameTrie β) (k : Name) (f : β → m U
 def NameTrie.forM [Monad m] (t : NameTrie β) (f : β → m Unit) : m Unit :=
   t.forMatchingM Name.anonymous f
 
+def NameTrie.matchingToArray (t : NameTrie β) (k : Name) : Array β :=
+  Id.run <| t.foldMatchingM k #[] fun v acc => acc.push v
+
+def NameTrie.toArray (t : NameTrie β) : Array β :=
+  Id.run <| t.foldM #[] fun v acc => acc.push v
+
 end Lean