Skip to content

Commit

Permalink
merge master
Browse files Browse the repository at this point in the history
  • Loading branch information
Kha committed Nov 14, 2024
2 parents 0822d5a + e0d7c3a commit 4b17c42
Show file tree
Hide file tree
Showing 1,182 changed files with 1,025,662 additions and 912,923 deletions.
2 changes: 1 addition & 1 deletion .github/ISSUE_TEMPLATE/bug_report.md
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,7 @@ Please put an X between the brackets as you perform the following steps:

### Versions

[Output of `#eval Lean.versionString`]
[Output of `#version` or `#eval Lean.versionString`]
[OS version, if not using live.lean-lang.org.]

### Additional Information
Expand Down
8 changes: 7 additions & 1 deletion .github/PULL_REQUEST_TEMPLATE.md
Original file line number Diff line number Diff line change
Expand Up @@ -5,11 +5,17 @@
* Include the link to your `RFC` or `bug` issue in the description.
* If the issue does not already have approval from a developer, submit the PR as draft.
* The PR title/description will become the commit message. Keep it up-to-date as the PR evolves.
* For `feat/fix` PRs, the first paragraph starting with "This PR" must be present and will become a
changelog entry unless the PR is labeled with `no-changelog`. If the PR does not have this label,
it must instead be categorized with one of the `changelog-*` labels (which will be done by a
reviewer for external PRs).
* A toolchain of the form `leanprover/lean4-pr-releases:pr-release-NNNN` for Linux and M-series Macs will be generated upon build. To generate binaries for Windows and Intel-based Macs as well, write a comment containing `release-ci` on its own line.
* If you rebase your PR onto `nightly-with-mathlib` then CI will test Mathlib against your PR.
* You can manage the `awaiting-review`, `awaiting-author`, and `WIP` labels yourself, by writing a comment containing one of these labels on its own line.
* Remove this section, up to and including the `---` before submitting.

---

Closes #0000 (`RFC` or `bug` issue number fixed by this PR, if any)
This PR <short changelog summary for feat/fix, see above>.

Closes <`RFC` or `bug` issue number fixed by this PR, if any>
8 changes: 8 additions & 0 deletions .github/dependabot.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
version: 2
updates:
- package-ecosystem: "github-actions"
directory: "/"
schedule:
interval: "monthly"
commit-message:
prefix: "chore: CI"
2 changes: 1 addition & 1 deletion .github/workflows/actionlint.yml
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,6 @@ jobs:
- name: Checkout
uses: actions/checkout@v4
- name: actionlint
uses: raven-actions/actionlint@v1
uses: raven-actions/actionlint@v2
with:
pyflakes: false # we do not use python scripts
10 changes: 5 additions & 5 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -217,7 +217,7 @@ jobs:
"release": true,
"check-level": 2,
"shell": "msys2 {0}",
"CMAKE_OPTIONS": "-G \"Unix Makefiles\" -DUSE_GMP=OFF",
"CMAKE_OPTIONS": "-G \"Unix Makefiles\"",
// for reasons unknown, interactivetests are flaky on Windows
"CTEST_OPTIONS": "--repeat until-pass:2",
"llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-w64-windows-gnu.tar.zst",
Expand All @@ -227,7 +227,7 @@ jobs:
{
"name": "Linux aarch64",
"os": "nscloud-ubuntu-22.04-arm64-4x8",
"CMAKE_OPTIONS": "-DUSE_GMP=OFF -DLEAN_INSTALL_SUFFIX=-linux_aarch64",
"CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-linux_aarch64",
"release": true,
"check-level": 2,
"shell": "nix develop .#oldGlibcAArch -c bash -euxo pipefail {0}",
Expand Down Expand Up @@ -318,7 +318,7 @@ jobs:
if: github.event_name == 'pull_request'
# (needs to be after "Checkout" so files don't get overridden)
- name: Setup emsdk
uses: mymindstorm/setup-emsdk@v12
uses: mymindstorm/setup-emsdk@v14
with:
version: 3.1.44
actions-cache-folder: emsdk
Expand Down Expand Up @@ -492,7 +492,7 @@ jobs:
with:
path: artifacts
- name: Release
uses: softprops/action-gh-release@v1
uses: softprops/action-gh-release@v2
with:
files: artifacts/*/*
fail_on_unmatched_files: true
Expand Down Expand Up @@ -536,7 +536,7 @@ jobs:
echo -e "\n*Full commit log*\n" >> diff.md
git log --oneline "$last_tag"..HEAD | sed 's/^/* /' >> diff.md
- name: Release Nightly
uses: softprops/action-gh-release@v1
uses: softprops/action-gh-release@v2
with:
body_path: diff.md
prerelease: true
Expand Down
10 changes: 1 addition & 9 deletions .github/workflows/nix-ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -110,14 +110,6 @@ jobs:
# https://github.com/netlify/cli/issues/1809
cp -r --dereference ./result ./dist
if: matrix.name == 'Nix Linux'
- name: Check manual for broken links
id: lychee
uses: lycheeverse/[email protected]
with:
fail: false # report errors but do not block CI on temporary failures
# gmplib.org consistently times out from GH actions
# the GitHub token is to avoid rate limiting
args: --base './dist' --no-progress --github-token ${{ secrets.GITHUB_TOKEN }} --exclude 'gmplib.org' './dist/**/*.html'
- name: Rebuild Nix Store Cache
run: |
rm -rf nix-store-cache || true
Expand All @@ -129,7 +121,7 @@ jobs:
python3 -c 'import base64; print("alias="+base64.urlsafe_b64encode(bytes.fromhex("${{github.sha}}")).decode("utf-8").rstrip("="))' >> "$GITHUB_OUTPUT"
echo "message=`git log -1 --pretty=format:"%s"`" >> "$GITHUB_OUTPUT"
- name: Publish manual to Netlify
uses: nwtgck/actions-netlify@v2.0
uses: nwtgck/actions-netlify@v3.0
id: publish-manual
with:
publish-dir: ./dist
Expand Down
25 changes: 25 additions & 0 deletions .github/workflows/pr-body.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
name: Check PR body for changelog convention

on:
merge_group:
pull_request:
types: [opened, synchronize, reopened, edited, labeled, converted_to_draft, ready_for_review]

jobs:
check-pr-body:
runs-on: ubuntu-latest
steps:
- name: Check PR body
if: github.event_name == 'pull_request'
uses: actions/github-script@v7
with:
script: |
const { title, body, labels, draft } = context.payload.pull_request;
if (!draft && /^(feat|fix):/.test(title) && !labels.some(label => label.name == "changelog-no")) {
if (!labels.some(label => label.name.startsWith("changelog-"))) {
core.setFailed('feat/fix PR must have a `changelog-*` label');
}
if (!/^This PR [^<]/.test(body)) {
core.setFailed('feat/fix PR must have changelog summary starting with "This PR ..." as first line.');
}
}
10 changes: 5 additions & 5 deletions .github/workflows/pr-release.yml
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@ jobs:
- name: Download artifact from the previous workflow.
if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
id: download-artifact
uses: dawidd6/action-download-artifact@v2 # https://github.com/marketplace/actions/download-workflow-artifact
uses: dawidd6/action-download-artifact@v6 # https://github.com/marketplace/actions/download-workflow-artifact
with:
run_id: ${{ github.event.workflow_run.id }}
path: artifacts
Expand All @@ -60,7 +60,7 @@ jobs:
GH_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
- name: Release
if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
uses: softprops/action-gh-release@v1
uses: softprops/action-gh-release@v2
with:
name: Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }}
# There are coredumps files here as well, but all in deeper subdirectories.
Expand All @@ -75,7 +75,7 @@ jobs:

- name: Report release status
if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
uses: actions/github-script@v6
uses: actions/github-script@v7
with:
script: |
await github.rest.repos.createCommitStatus({
Expand Down Expand Up @@ -111,7 +111,7 @@ jobs:
- name: 'Setup jq'
if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
uses: dcarbone/install-jq-action@v1.0.1
uses: dcarbone/install-jq-action@v2.1.0

# Check that the most recently nightly coincides with 'git merge-base HEAD master'
- name: Check merge-base and nightly-testing-YYYY-MM-DD
Expand Down Expand Up @@ -208,7 +208,7 @@ jobs:
- name: Report mathlib base
if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true' }}
uses: actions/github-script@v6
uses: actions/github-script@v7
with:
script: |
const description =
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/stale.yml
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ jobs:
stale:
runs-on: ubuntu-latest
steps:
- uses: actions/stale@v8
- uses: actions/stale@v9
with:
days-before-stale: -1
days-before-pr-stale: 30
Expand Down
Loading

0 comments on commit 4b17c42

Please sign in to comment.