Merge remote-tracking branch 'origin' into xfr_complex_measure_ishaar

leanprover-community · Sep 2, 2023 · 95b2f22 · 95b2f22
2 parents ed5dff2 + ab6dac9
commit 95b2f22
Show file tree

Hide file tree

Showing 173 changed files with 3,472 additions and 1,531 deletions.
diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml
@@ -100,6 +100,10 @@ jobs:
         run: |
           find . -name . -o -prune -exec rm -rf -- {} +
 
+      # The Hoskinson runners may not have jq installed, so do that now.
+      - name: 'Setup jq'
+        uses: dcarbone/[email protected]
+
       - name: install elan
         run: |
           set -o pipefail
@@ -115,12 +119,20 @@ jobs:
         run: |
           find Mathlib -name "*.lean" | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean
 
+      - name: If using a lean-pr-release toolchain, uninstall
+        run: |
+          if [[ `cat lean-toolchain` =~ ^leanprover/lean4-pr-releases:pr-release-[0-9]+$ ]]; then
+            echo "Uninstalling transient toolchain `cat lean-toolchain`"
+            elan toolchain uninstall `cat lean-toolchain`
+          fi
+
       - name: get cache
         run: |
           lake exe cache clean
           lake exe cache get
 
       - name: build mathlib
+        id: build
         uses: liskin/gh-problem-matcher-wrap@v2
         with:
           linters: gcc
@@ -154,14 +166,28 @@ jobs:
           build/bin/checkYaml
 
       - name: test mathlib
+        id: test
         run: make -j 8 test
 
       - name: lint mathlib
+        id: lint
         uses: liskin/gh-problem-matcher-wrap@v2
         with:
           linters: gcc
           run: env LEAN_ABORT_ON_PANIC=1 make lint
 
+      - name: Post comments for lean-pr-testing branch
+        if: always()
+        env:
+          TOKEN: ${{ secrets.LEAN_PR_TESTING }}
+          GITHUB_CONTEXT: ${{ toJson(github) }}
+          WORKFLOW_URL: https://github.com/${{ github.repository }}/actions/runs/${{ github.event.workflow_run.id }}
+          LINT_OUTCOME: ${{ steps.lint.outcome }}
+          TEST_OUTCOME: ${{ steps.test.outcome }}
+          BUILD_OUTCOME: ${{ steps.build.outcome }}
+        run: |
+          scripts/lean-pr-testing-comments.sh
+
   final:
     name: Post-CI job
     if: github.repository == 'leanprover-community/mathlib4'

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
@@ -106,6 +106,10 @@ jobs:
         run: |
           find . -name . -o -prune -exec rm -rf -- {} +
 
+      # The Hoskinson runners may not have jq installed, so do that now.
+      - name: 'Setup jq'
+        uses: dcarbone/[email protected]
+
       - name: install elan
         run: |
           set -o pipefail
@@ -121,12 +125,20 @@ jobs:
         run: |
           find Mathlib -name "*.lean" | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean
 
+      - name: If using a lean-pr-release toolchain, uninstall
+        run: |
+          if [[ `cat lean-toolchain` =~ ^leanprover/lean4-pr-releases:pr-release-[0-9]+$ ]]; then
+            echo "Uninstalling transient toolchain `cat lean-toolchain`"
+            elan toolchain uninstall `cat lean-toolchain`
+          fi
+
       - name: get cache
         run: |
           lake exe cache clean
           lake exe cache get
 
       - name: build mathlib
+        id: build
         uses: liskin/gh-problem-matcher-wrap@v2
         with:
           linters: gcc
@@ -160,14 +172,28 @@ jobs:
           build/bin/checkYaml
 
       - name: test mathlib
+        id: test
         run: make -j 8 test
 
       - name: lint mathlib
+        id: lint
         uses: liskin/gh-problem-matcher-wrap@v2
         with:
           linters: gcc
           run: env LEAN_ABORT_ON_PANIC=1 make lint
 
+      - name: Post comments for lean-pr-testing branch
+        if: always()
+        env:
+          TOKEN: ${{ secrets.LEAN_PR_TESTING }}
+          GITHUB_CONTEXT: ${{ toJson(github) }}
+          WORKFLOW_URL: https://github.com/${{ github.repository }}/actions/runs/${{ github.event.workflow_run.id }}
+          LINT_OUTCOME: ${{ steps.lint.outcome }}
+          TEST_OUTCOME: ${{ steps.test.outcome }}
+          BUILD_OUTCOME: ${{ steps.build.outcome }}
+        run: |
+          scripts/lean-pr-testing-comments.sh
+
   final:
     name: Post-CI job
     if: github.repository == 'leanprover-community/mathlib4'

diff --git a/.github/workflows/build.yml.in b/.github/workflows/build.yml.in
@@ -86,6 +86,10 @@ jobs:
         run: |
           find . -name . -o -prune -exec rm -rf -- {} +
 
+      # The Hoskinson runners may not have jq installed, so do that now.
+      - name: 'Setup jq'
+        uses: dcarbone/[email protected]
+
       - name: install elan
         run: |
           set -o pipefail
@@ -101,12 +105,20 @@ jobs:
         run: |
           find Mathlib -name "*.lean" | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean
 
+      - name: If using a lean-pr-release toolchain, uninstall
+        run: |
+          if [[ `cat lean-toolchain` =~ ^leanprover/lean4-pr-releases:pr-release-[0-9]+$ ]]; then
+            echo "Uninstalling transient toolchain `cat lean-toolchain`"
+            elan toolchain uninstall `cat lean-toolchain`
+          fi
+
       - name: get cache
         run: |
           lake exe cache clean
           lake exe cache get
 
       - name: build mathlib
+        id: build
         uses: liskin/gh-problem-matcher-wrap@v2
         with:
           linters: gcc
@@ -140,14 +152,28 @@ jobs:
           build/bin/checkYaml
 
       - name: test mathlib
+        id: test
         run: make -j 8 test
 
       - name: lint mathlib
+        id: lint
         uses: liskin/gh-problem-matcher-wrap@v2
         with:
           linters: gcc
           run: env LEAN_ABORT_ON_PANIC=1 make lint
 
+      - name: Post comments for lean-pr-testing branch
+        if: always()
+        env:
+          TOKEN: ${{ secrets.LEAN_PR_TESTING }}
+          GITHUB_CONTEXT: ${{ toJson(github) }}
+          WORKFLOW_URL: https://github.com/${{ github.repository }}/actions/runs/${{ github.event.workflow_run.id }}
+          LINT_OUTCOME: ${{ steps.lint.outcome }}
+          TEST_OUTCOME: ${{ steps.test.outcome }}
+          BUILD_OUTCOME: ${{ steps.build.outcome }}
+        run: |
+          scripts/lean-pr-testing-comments.sh
+
   final:
     name: Post-CI jobJOB_NAME
     if: github.repository MAIN_OR_FORK 'leanprover-community/mathlib4'

diff --git a/.github/workflows/build_fork.yml b/.github/workflows/build_fork.yml
@@ -104,6 +104,10 @@ jobs:
         run: |
           find . -name . -o -prune -exec rm -rf -- {} +
 
+      # The Hoskinson runners may not have jq installed, so do that now.
+      - name: 'Setup jq'
+        uses: dcarbone/[email protected]
+
       - name: install elan
         run: |
           set -o pipefail
@@ -119,12 +123,20 @@ jobs:
         run: |
           find Mathlib -name "*.lean" | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean
 
+      - name: If using a lean-pr-release toolchain, uninstall
+        run: |
+          if [[ `cat lean-toolchain` =~ ^leanprover/lean4-pr-releases:pr-release-[0-9]+$ ]]; then
+            echo "Uninstalling transient toolchain `cat lean-toolchain`"
+            elan toolchain uninstall `cat lean-toolchain`
+          fi
+
       - name: get cache
         run: |
           lake exe cache clean
           lake exe cache get
 
       - name: build mathlib
+        id: build
         uses: liskin/gh-problem-matcher-wrap@v2
         with:
           linters: gcc
@@ -158,14 +170,28 @@ jobs:
           build/bin/checkYaml
 
       - name: test mathlib
+        id: test
         run: make -j 8 test
 
       - name: lint mathlib
+        id: lint
         uses: liskin/gh-problem-matcher-wrap@v2
         with:
           linters: gcc
           run: env LEAN_ABORT_ON_PANIC=1 make lint
 
+      - name: Post comments for lean-pr-testing branch
+        if: always()
+        env:
+          TOKEN: ${{ secrets.LEAN_PR_TESTING }}
+          GITHUB_CONTEXT: ${{ toJson(github) }}
+          WORKFLOW_URL: https://github.com/${{ github.repository }}/actions/runs/${{ github.event.workflow_run.id }}
+          LINT_OUTCOME: ${{ steps.lint.outcome }}
+          TEST_OUTCOME: ${{ steps.test.outcome }}
+          BUILD_OUTCOME: ${{ steps.build.outcome }}
+        run: |
+          scripts/lean-pr-testing-comments.sh
+
   final:
     name: Post-CI job (fork)
     if: github.repository != 'leanprover-community/mathlib4'

diff --git a/.github/workflows/nightly_bump_toolchain.yml b/.github/workflows/nightly_bump_toolchain.yml
@@ -0,0 +1,34 @@
+name: Bump lean-toolchain on nightly-testing
+
+on:
+  schedule:
+    - cron: '0 10 * * *'  # 11AM CET/2AM PT, 3 hours after lean4 starts building the nightly.
+
+jobs:
+  update-toolchain:
+    runs-on: ubuntu-latest
+
+    steps:
+    - name: Checkout code
+      uses: actions/checkout@v2
+      with:
+        ref: nightly-testing # checkout nightly-testing branch
+        token: ${{ secrets.NIGHTLY_TESTING }}
+
+    - name: Get latest release tag from leanprover/lean4-nightly
+      id: get-latest-release
+      run: |
+        RELEASE_TAG=$(curl -s "https://api.github.com/repos/leanprover/lean4-nightly/releases" | jq -r '.[0].tag_name')
+        echo "RELEASE_TAG=$RELEASE_TAG" >> $GITHUB_ENV
+
+    - name: Update lean-toolchain file
+      run: |
+        echo "leanprover/lean4:${RELEASE_TAG}" > lean-toolchain
+
+    - name: Commit and push changes
+      run: |
+        git config user.name "leanprover-community-mathlib4-bot"
+        git config user.email "[email protected]"
+        git add lean-toolchain
+        git commit -m "chore: bump to ${RELEASE_TAG}"
+        git push origin nightly-testing
diff --git a/.github/workflows/nightly_detect_failure.yml b/.github/workflows/nightly_detect_failure.yml
@@ -0,0 +1,25 @@
+name: Post to zulip if the nightly-testing branch is failing.
+
+on:
+  workflow_run:
+    workflows: ["continuous integration"]
+    types:
+      - completed
+
+jobs:
+  handle_failure:
+    if: ${{ github.event.workflow_run.conclusion == 'failure' && github.event.workflow_run.head_branch == 'nightly-testing' }}
+    runs-on: ubuntu-latest
+
+    steps:
+    - name: Send message on Zulip
+      uses: zulip/github-actions-zulip/send-message@v1
+      with:
+        api-key: ${{ secrets.ZULIP_API_KEY }}
+        email: '[email protected]'
+        organization-url: 'https://leanprover.zulipchat.com'
+        to: 'mathlib reviewers'
+        type: 'stream'
+        topic: 'CI failure on the nightly-testing branch'
+        content: |
+          The latest CI for branch#nightly-testing has [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.event.workflow_run.id }}).
diff --git a/.github/workflows/nightly_merge_master.yml b/.github/workflows/nightly_merge_master.yml
@@ -0,0 +1,30 @@
+# This job merges every commit to `master` into `nightly-testing`, resolving merge conflicts in favor of `nightly-testing`.
+
+name: Merge master to nightly
+
+on:
+  push:
+    branches:
+      - master
+
+jobs:
+  merge-to-nightly:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v2
+        with:
+          fetch-depth: 0
+          token: ${{ secrets.NIGHTLY_TESTING }}
+
+      - name: Configure Git User
+        run: |
+          git config user.name "leanprover-community-mathlib4-bot"
+          git config user.email "[email protected]"
+
+      - name: Merge master to nightly favoring nightly changes
+        run: |
+          git checkout nightly-testing
+          git merge master --strategy-option ours --no-commit --allow-unrelated-histories
+          git commit -m "Merge master into nightly-testing"
+          git push origin nightly-testing
diff --git a/Card b/Card
diff --git a/Counterexamples/SorgenfreyLine.lean b/Counterexamples/SorgenfreyLine.lean
@@ -7,7 +7,7 @@ import Mathlib.Topology.Instances.Irrational
 import Mathlib.Topology.Algebra.Order.Archimedean
 import Mathlib.Topology.Paracompact
 import Mathlib.Topology.MetricSpace.Metrizable
-import Mathlib.Topology.MetricSpace.EMetricParacompact
+import Mathlib.Topology.EMetricSpace.Paracompact
 import Mathlib.Data.Set.Intervals.Monotone
 import Mathlib.Topology.Separation.NotNormal