From c1f6daf1acda8738dc97fe69cc323d5ad0ecdbdd Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Wed, 29 Nov 2023 00:18:20 +1100 Subject: [PATCH 1/6] fix: remove unnecessary step in pr-release.yml (#2976) This step was unnecessary, as the script uses an unauthenticated https URL anyway, and apparently was causing a [permissions problem](https://github.com/leanprover/lean4/actions/runs/7005903162/job/19094622187#step:8:7). --- .github/workflows/pr-release.yml | 1 - 1 file changed, 1 deletion(-) 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' From 6c7a765abb9d97ec881af386c337a514f7b82db1 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Tue, 28 Nov 2023 18:48:09 +0100 Subject: [PATCH 2/6] chore: Check PR title, not commit, for commit convention (#2978) Also turn this into a proper check, run when a PR is opened or edited. I took the liberty to rename the workflow file and name, so that one doesn't have to look inside to guess what the workflow is doing. --- .github/workflows/pr-title.yml | 17 +++++++++++++++++ .github/workflows/pr.yml | 31 ------------------------------- 2 files changed, 17 insertions(+), 31 deletions(-) create mode 100644 .github/workflows/pr-title.yml delete mode 100644 .github/workflows/pr.yml diff --git a/.github/workflows/pr-title.yml b/.github/workflows/pr-title.yml new file mode 100644 index 000000000000..dcb5dd5f8718 --- /dev/null +++ b/.github/workflows/pr-title.yml @@ -0,0 +1,17 @@ +name: Check PR title for commit convention + +on: + pull_request: + types: [opened, edited] + +jobs: + check-pr-title: + runs-on: ubuntu-latest + steps: + - name: Check PR title + uses: actions/github-script@v6 + with: + script: | + if (!/^(feat|fix|doc|style|refactor|test|chore|perf): .*[^.]($|\n\n)/.test(context.payload.pull_request.title)) { + 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).', - }); - } From 0a6aed61e9a1c5bfeb7b348ec6fc2f71028bb406 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 29 Nov 2023 01:10:11 +0100 Subject: [PATCH 3/6] chore: CI: Create an all-builds-ok job (#2983) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit there is a little dance with `if: success()` because otherwise a failed `build` job would make this new job skipped, not failed, and I fear skipped means ok when it is a required job. So let’s make sure this job actually fails. --- .github/workflows/ci.yml | 15 +++++++++++++++ 1 file changed, 15 insertions(+) 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: From 5d22145b8329f78c2bad372214c91b08a7f7766b Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Wed, 29 Nov 2023 17:16:34 +1100 Subject: [PATCH 4/6] chore: remove supportInterpreter from lake template (#2984) Now that there is a helpful message at the point of use when `supportInterpreter` is required, we don't need to clutter every `lakefile` with the advice. --- src/lake/Lake/CLI/Init.lean | 4 ---- src/lake/README.md | 4 ---- src/lake/tests/llvm-bitcode-gen/lakefile.lean | 6 ++---- 3 files changed, 2 insertions(+), 12 deletions(-) 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 - From 34264a4b1daf9ff61843f6eacc777108ad7e5d2e Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 29 Nov 2023 09:49:13 +0100 Subject: [PATCH 5/6] doc: Improve docstrings around Array.mk,.data,.toList (#2771) following a discussion at --------- Co-authored-by: Mario Carneiro --- src/Init/Data/Array/Basic.lean | 3 +++ src/Init/Prelude.lean | 26 ++++++++++++++++---------- 2 files changed, 19 insertions(+), 10 deletions(-) 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) From 4f2f704962f960c42ca2bc3ca81c4c43767b22f2 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 29 Nov 2023 13:03:20 +0100 Subject: [PATCH 6/6] chore: make PR title check work as a merge_group check (#2987) --- .github/workflows/pr-title.yml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/.github/workflows/pr-title.yml b/.github/workflows/pr-title.yml index dcb5dd5f8718..40556c5c7bcc 100644 --- a/.github/workflows/pr-title.yml +++ b/.github/workflows/pr-title.yml @@ -1,8 +1,9 @@ name: Check PR title for commit convention on: + merge_group: pull_request: - types: [opened, edited] + types: [opened, synchronize, reopened, edited] jobs: check-pr-title: @@ -12,6 +13,8 @@ jobs: uses: actions/github-script@v6 with: script: | - if (!/^(feat|fix|doc|style|refactor|test|chore|perf): .*[^.]($|\n\n)/.test(context.payload.pull_request.title)) { + 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).'); }