Merge remote-tracking branch 'origin/master' into joachim/guess-lex-b…

…adCassOn

.github/workflows/ci.yml

@@ -364,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).');
+            }

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/lake/Lake/CLI/Init.lean

@@ -56,10 +56,6 @@ lean_lib {libRoot} where
 @[default_target]
 lean_exe {exeName} where
   root := `Main
-  -- Enables the use of the Lean interpreter by the executable (e.g.,
-  -- `runFrontend`) at the expense of increased binary size on Linux.
-  -- Remove this line if you do not need such functionality.
-  supportInterpreter := true
 "
 
 def exeConfigFileContents (pkgName exeRoot : String) :=

src/lake/README.md

@@ -104,10 +104,6 @@ lean_lib «Hello» where
 @[default_target]
 lean_exe «hello» where
   root := `Main
-  -- Enables the use of the Lean interpreter by the executable (e.g.,
-  -- `runFrontend`) at the expense of increased binary size on Linux.
-  -- Remove this line if you do not need such functionality.
-  supportInterpreter := true
 ```
 
 The command `lake build` is used to build the package (and its [dependencies](#adding-dependencies), if it has them) into a native executable. The result will be placed in `.lake/build/bin`. The command `lake clean` deletes `build`.

src/lake/tests/llvm-bitcode-gen/lakefile.lean

@@ -13,12 +13,10 @@ lean_lib «LlvmBitcodeGen» where
 @[default_target]
 lean_exe «llvm-bitcode-gen» where
   root := `Main
-  -- Enables the use of the Lean interpreter by the executable (e.g.,
-  -- `runFrontend`) at the expense of increased binary size on Linux.
-  -- Remove this line if you do not need such functionality.
+  -- Enables the use of the Lean interpreter by the executable.
+  -- We need this to access `Lean.Internal.hasLLVMBackend`.
   supportInterpreter := true
 
 script hasLLVMBackend do
   IO.println s!"Lake Lean.Internal.hasLLVMBackend: {Lean.Internal.hasLLVMBackend ()}"
   return 0
-