feat: topology on ring of finite adeles.

.github/workflows/bors.yml

@@ -50,7 +50,14 @@ jobs:
         with:
           python-version: 3.8
 
-      - name: lint
+      - name: install elan
+        run: |
+          set -o pipefail
+          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+          ./elan-init -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
+
+      - name: "run style linters: Python ones and their Lean rewrite"
         run: |
           ./scripts/lint-style.sh
 
@@ -83,23 +90,6 @@ jobs:
       - name: check that workflows were consistent
         run: git diff --exit-code
 
-  summarize_declarations:
-    if: github.repository == 'leanprover-community/mathlib4'
-    name: summarize_declarations
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/checkout@v4
-        with:
-          ## fetch the whole repository, useful to find a common fork
-          fetch-depth: 0
-      - name: print_lost_declarations
-        run: |
-          ## back and forth to settle a "detached head" (maybe?)
-          git checkout -q master
-          git checkout -q -
-          printf '###  Summary\n\n' > "${GITHUB_STEP_SUMMARY}"
-          ./scripts/no_lost_declarations.sh >> "${GITHUB_STEP_SUMMARY}"
-
   build:
     if: github.repository == 'leanprover-community/mathlib4'
     name: Build
@@ -124,7 +114,7 @@ jobs:
       - name: install elan
         run: |
           set -o pipefail
-          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
           ./elan-init -y --default-toolchain none
           echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
 
@@ -142,8 +132,8 @@ jobs:
           lean --version
           lake --version
 
-      - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
-        run: lake exe mk_all
+      - name: check {Mathlib, Tactic, Counterexamples, Archive}.lean are up to date
+        run: lake exe mk_all --check
 
       - name: build cache
         run: |

.github/workflows/build.yml

@@ -57,7 +57,14 @@ jobs:
         with:
           python-version: 3.8
 
-      - name: lint
+      - name: install elan
+        run: |
+          set -o pipefail
+          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+          ./elan-init -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
+
+      - name: "run style linters: Python ones and their Lean rewrite"
         run: |
           ./scripts/lint-style.sh
 
@@ -90,23 +97,6 @@ jobs:
       - name: check that workflows were consistent
         run: git diff --exit-code
 
-  summarize_declarations:
-    if: github.repository == 'leanprover-community/mathlib4'
-    name: summarize_declarations
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/checkout@v4
-        with:
-          ## fetch the whole repository, useful to find a common fork
-          fetch-depth: 0
-      - name: print_lost_declarations
-        run: |
-          ## back and forth to settle a "detached head" (maybe?)
-          git checkout -q master
-          git checkout -q -
-          printf '###  Summary\n\n' > "${GITHUB_STEP_SUMMARY}"
-          ./scripts/no_lost_declarations.sh >> "${GITHUB_STEP_SUMMARY}"
-
   build:
     if: github.repository == 'leanprover-community/mathlib4'
     name: Build
@@ -131,7 +121,7 @@ jobs:
       - name: install elan
         run: |
           set -o pipefail
-          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
           ./elan-init -y --default-toolchain none
           echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
 
@@ -149,8 +139,8 @@ jobs:
           lean --version
           lake --version
 
-      - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
-        run: lake exe mk_all
+      - name: check {Mathlib, Tactic, Counterexamples, Archive}.lean are up to date
+        run: lake exe mk_all --check
 
       - name: build cache
         run: |

.github/workflows/build.yml.in

@@ -36,7 +36,14 @@ jobs:
         with:
           python-version: 3.8
 
-      - name: lint
+      - name: install elan
+        run: |
+          set -o pipefail
+          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+          ./elan-init -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
+
+      - name: "run style linters: Python ones and their Lean rewrite"
         run: |
           ./scripts/lint-style.sh
 
@@ -69,23 +76,6 @@ jobs:
       - name: check that workflows were consistent
         run: git diff --exit-code
 
-  summarize_declarations:
-    if: github.repository MAIN_OR_FORK 'leanprover-community/mathlib4'
-    name: summarize_declarations
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/checkout@v4
-        with:
-          ## fetch the whole repository, useful to find a common fork
-          fetch-depth: 0
-      - name: print_lost_declarations
-        run: |
-          ## back and forth to settle a "detached head" (maybe?)
-          git checkout -q master
-          git checkout -q -
-          printf '###  Summary\n\n' > "${GITHUB_STEP_SUMMARY}"
-          ./scripts/no_lost_declarations.sh >> "${GITHUB_STEP_SUMMARY}"
-
   build:
     if: github.repository MAIN_OR_FORK 'leanprover-community/mathlib4'
     name: BuildJOB_NAME
@@ -110,7 +100,7 @@ jobs:
       - name: install elan
         run: |
           set -o pipefail
-          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
           ./elan-init -y --default-toolchain none
           echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
 
@@ -128,8 +118,8 @@ jobs:
           lean --version
           lake --version
 
-      - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
-        run: lake exe mk_all
+      - name: check {Mathlib, Tactic, Counterexamples, Archive}.lean are up to date
+        run: lake exe mk_all --check
 
       - name: build cache
         run: |

.github/workflows/build_fork.yml

@@ -54,7 +54,14 @@ jobs:
         with:
           python-version: 3.8
 
-      - name: lint
+      - name: install elan
+        run: |
+          set -o pipefail
+          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+          ./elan-init -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
+
+      - name: "run style linters: Python ones and their Lean rewrite"
         run: |
           ./scripts/lint-style.sh
 
@@ -87,23 +94,6 @@ jobs:
       - name: check that workflows were consistent
         run: git diff --exit-code
 
-  summarize_declarations:
-    if: github.repository != 'leanprover-community/mathlib4'
-    name: summarize_declarations
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/checkout@v4
-        with:
-          ## fetch the whole repository, useful to find a common fork
-          fetch-depth: 0
-      - name: print_lost_declarations
-        run: |
-          ## back and forth to settle a "detached head" (maybe?)
-          git checkout -q master
-          git checkout -q -
-          printf '###  Summary\n\n' > "${GITHUB_STEP_SUMMARY}"
-          ./scripts/no_lost_declarations.sh >> "${GITHUB_STEP_SUMMARY}"
-
   build:
     if: github.repository != 'leanprover-community/mathlib4'
     name: Build (fork)
@@ -128,7 +118,7 @@ jobs:
       - name: install elan
         run: |
           set -o pipefail
-          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
           ./elan-init -y --default-toolchain none
           echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
 
@@ -146,8 +136,8 @@ jobs:
           lean --version
           lake --version
 
-      - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
-        run: lake exe mk_all
+      - name: check {Mathlib, Tactic, Counterexamples, Archive}.lean are up to date
+        run: lake exe mk_all --check
 
       - name: build cache
         run: |

.github/workflows/lean4checker.yml

@@ -29,7 +29,7 @@ jobs:
       - name: install elan
         run: |
           set -o pipefail
-          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
           ./elan-init -y --default-toolchain none
           echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
 

.github/workflows/lint_and_suggest_pr.yml

@@ -60,7 +60,7 @@ jobs:
       - name: install elan
         run: |
           set -o pipefail
-          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
           ./elan-init -y --default-toolchain none
           echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
 

.github/workflows/nightly_merge_master.yml

@@ -13,7 +13,7 @@ jobs:
       - name: install elan
         run: |
           set -o pipefail
-          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
           ./elan-init -y --default-toolchain none
           echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
 

.github/workflows/nolints.yml

@@ -20,7 +20,7 @@ jobs:
       - name: install elan
         run: |
           set -o pipefail
-          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
           ./elan-init -y --default-toolchain none
           echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
 

.github/workflows/technical_debt_counters.yml → .github/workflows/technical_debt_metrics.yml

@@ -11,11 +11,13 @@ jobs:
     steps:
     - name: Checkout code
       uses: actions/checkout@v4
+      with: # checkout all history so that we can compare across commits
+        fetch-depth: 0
 
     - name: Run script
       id: tech_debt
       run: |
-        printf $'summary<<EOF\n%s\nEOF' "$(./scripts/technical-debt-counters.sh)" >> "$GITHUB_OUTPUT"
+        printf $'summary<<EOF\n%s\nEOF' "$(./scripts/technical-debt-metrics.sh)" >> "$GITHUB_OUTPUT"
 
     - name: Post output to Zulip
       uses: zulip/github-actions-zulip/send-message@v1