diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 111d9c89916d..c7a36f75a3fc 100644 --- a/.github/workflows/ci.yml +++ b/.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: diff --git a/.github/workflows/pr-release.yml b/.github/workflows/pr-release.yml index 8f4b31b3c663..63ee7e555cc7 100644 --- a/.github/workflows/pr-release.yml +++ b/.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' diff --git a/.github/workflows/pr-title.yml b/.github/workflows/pr-title.yml new file mode 100644 index 000000000000..40556c5c7bcc --- /dev/null +++ b/.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).'); + } diff --git a/.github/workflows/pr.yml b/.github/workflows/pr.yml deleted file mode 100644 index fc0463910a7e..000000000000 --- a/.github/workflows/pr.yml +++ /dev/null @@ -1,31 +0,0 @@ -name: sanity-check opened PRs - -on: - # needs read/write GH token, do *not* execute arbitrary code from PR - pull_request_target: - types: [opened] - -jobs: - check-pr: - runs-on: ubuntu-latest - steps: - - name: Check Commit Message - uses: actions/github-script@v6 - with: - github-token: ${{ secrets.GITHUB_TOKEN }} - script: | - const { data: commits } = await github.rest.pulls.listCommits({ - owner: context.repo.owner, - repo: context.repo.repo, - pull_number: context.issue.number, - }); - console.log(commits[0].commit.message); - // check first commit only (and only once) since later commits might be intended to be squashed away - if (!/^(feat|fix|doc|style|refactor|test|chore|perf): .*[^.]($|\n\n)/.test(commits[0].commit.message)) { - await github.rest.issues.createComment({ - owner: context.repo.owner, - repo: context.repo.repo, - issue_number: context.issue.number, - body: 'Thanks for your contribution! Please make sure to follow our [Commit Convention](https://leanprover.github.io/lean4/doc/dev/commit_convention.html).', - }); - } diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index fe89ca6149bd..3b4f722fc940 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/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 [] diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 1b203be23674..3d26bc852ef4 100644 --- a/src/Init/Prelude.lean +++ b/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) diff --git a/src/lake/Lake/CLI/Init.lean b/src/lake/Lake/CLI/Init.lean index 187e0fe53f01..3ebe1368de4d 100644 --- a/src/lake/Lake/CLI/Init.lean +++ b/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) := diff --git a/src/lake/README.md b/src/lake/README.md index 5c2d246b9c52..75a8b7f726b3 100644 --- a/src/lake/README.md +++ b/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`. diff --git a/src/lake/tests/llvm-bitcode-gen/lakefile.lean b/src/lake/tests/llvm-bitcode-gen/lakefile.lean index 5aacefe3a6ef..fe7d0c9a5c1c 100644 --- a/src/lake/tests/llvm-bitcode-gen/lakefile.lean +++ b/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 -