Merge branch 'master' into master

Author: YanYablonovskiy

.github/build.in.yml

@@ -501,7 +501,7 @@ jobs:
         id: lint
         run: |
           cd pr-branch
-          env LEAN_ABORT_ON_PANIC=1 ../master-branch/scripts/lake-build-wrapper.py .lake/build_summary_lint.json lake exe runLinter --trace Mathlib
+          env LEAN_ABORT_ON_PANIC=1 lake exe runLinter --trace Mathlib
 
       - name: end gh-problem-match-wrap for shake and lint steps
         uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23

.github/workflows/bors.yml

@@ -511,7 +511,7 @@ jobs:
         id: lint
         run: |
           cd pr-branch
-          env LEAN_ABORT_ON_PANIC=1 ../master-branch/scripts/lake-build-wrapper.py .lake/build_summary_lint.json lake exe runLinter --trace Mathlib
+          env LEAN_ABORT_ON_PANIC=1 lake exe runLinter --trace Mathlib
 
       - name: end gh-problem-match-wrap for shake and lint steps
         uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23

.github/workflows/build.yml

@@ -517,7 +517,7 @@ jobs:
         id: lint
         run: |
           cd pr-branch
-          env LEAN_ABORT_ON_PANIC=1 ../master-branch/scripts/lake-build-wrapper.py .lake/build_summary_lint.json lake exe runLinter --trace Mathlib
+          env LEAN_ABORT_ON_PANIC=1 lake exe runLinter --trace Mathlib
 
       - name: end gh-problem-match-wrap for shake and lint steps
         uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23

.github/workflows/build_fork.yml

@@ -515,7 +515,7 @@ jobs:
         id: lint
         run: |
           cd pr-branch
-          env LEAN_ABORT_ON_PANIC=1 ../master-branch/scripts/lake-build-wrapper.py .lake/build_summary_lint.json lake exe runLinter --trace Mathlib
+          env LEAN_ABORT_ON_PANIC=1 lake exe runLinter --trace Mathlib
 
       - name: end gh-problem-match-wrap for shake and lint steps
         uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23

.github/workflows/daily.yml

@@ -283,3 +283,164 @@ jobs:
           topic: 'mathlib test executable failure'
           content: |
             ❌ mathlib_test_executable [${{ needs.check-mathlib_test_executable.result }}](${{ steps.get-status.outputs.mathlib_test_executable_url }}) on ${{ github.sha }} (branch: ${{ env.BRANCH_REF }})
+
+  check-nanoda:
+    runs-on: ubuntu-latest
+    if: github.repository == 'leanprover-community/mathlib4'
+    strategy:
+      fail-fast: false
+      matrix:
+        branch_type: [master, nightly]
+    steps:
+      # Checkout repository, so that we can fetch tags to decide which branch we want.
+      - name: Checkout branch or tag
+        uses: actions/checkout@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1
+
+      - name: Fetch latest tags (if nightly)
+        if: matrix.branch_type == 'nightly'
+        run: |
+          # When in nightly mode, fetch tags from the nightly-testing repository
+          git remote add nightly-testing https://github.com/leanprover-community/mathlib4-nightly-testing.git
+          git fetch nightly-testing --tags
+          LATEST_TAG=$(git tag | grep -E "${{ env.TAG_PATTERN }}" | sort -r | head -n 1)
+          echo "LATEST_TAG=${LATEST_TAG}" >> "$GITHUB_ENV"
+
+      - name: Set branch ref
+        run: |
+          if [ "${{ matrix.branch_type }}" == "master" ]; then
+            echo "BRANCH_REF=${{ env.DEFAULT_BRANCH }}" >> "$GITHUB_ENV"
+          else
+            echo "BRANCH_REF=${{ env.LATEST_TAG }}" >> "$GITHUB_ENV"
+          fi
+
+      # Checkout the branch or tag we want to test.
+      - name: Checkout branch or tag
+        uses: actions/checkout@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1
+        with:
+          repository: ${{ matrix.branch_type == 'nightly' && 'leanprover-community/mathlib4-nightly-testing' || github.repository }}
+          ref: ${{ env.BRANCH_REF }}
+
+      - name: Configure Lean
+        uses: leanprover/lean-action@434f25c2f80ded67bba02502ad3a86f25db50709 # v1.3.0
+        with:
+          auto-config: false
+          use-github-cache: false
+          use-mathlib-cache: true
+          reinstall-transient-toolchain: true
+
+      - name: Install Rust
+        uses: dtolnay/rust-toolchain@stable
+
+      - name: Check Mathlib using nanoda # make sure this name is consistent with "Get job status and URLs" in the notify job
+        id: nanoda
+        continue-on-error: true
+        run: |
+          # Clone and build lean4export
+          # TODO: Once https://github.com/leanprover/lean4export/pull/11 is merged,
+          # switch to leanprover/lean4export and remove the `git checkout` line below.
+          git clone https://github.com/kim-em/lean4export
+          cd lean4export
+          git checkout fix-nondep-normalization
+          # Match toolchain to mathlib
+          cp ../lean-toolchain .
+          lake build
+          cd ..
+
+          # Clone and build nanoda_lib
+          git clone https://github.com/ammkrn/nanoda_lib
+          cd nanoda_lib
+          git checkout debug
+          cargo build --release
+          cd ..
+
+          # Export Mathlib
+          lake env lean4export/.lake/build/bin/lean4export Mathlib > mathlib_export.txt
+
+          # Create config
+          cat > nanoda_config.json << 'EOF'
+          {
+              "export_file_path": "mathlib_export.txt",
+              "permitted_axioms": [
+                  "propext",
+                  "Classical.choice",
+                  "Quot.sound",
+                  "Lean.trustCompiler"
+              ],
+              "unpermitted_axiom_hard_error": false,
+              "nat_extension": true,
+              "string_extension": true,
+              "print_success_message": true
+          }
+          EOF
+
+          # Run nanoda
+          nanoda_lib/target/release/nanoda_bin nanoda_config.json
+
+  notify-nanoda:
+    runs-on: ubuntu-latest
+    needs: check-nanoda
+    if: github.repository == 'leanprover-community/mathlib4' && always()
+    strategy:
+      fail-fast: false
+      matrix:
+        branch_type: [master, nightly]
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1
+
+      - name: Get job status and URLs
+        id: get-status
+        env:
+          GH_TOKEN: ${{ github.token }}
+        run: |
+          JOB_NAME="check-nanoda (${{ matrix.branch_type }})"
+
+          # Get URL to the specific step
+          NANODA_URL=$(gh run view ${{ github.run_id }} --json jobs --jq \
+            ".jobs[] | select(.name == \"$JOB_NAME\") \
+            | (.url + (.steps[] | select(.name == \"Check Mathlib using nanoda\") \
+              | \"#step:\(.number):1\"))")
+
+          echo "nanoda_url=${NANODA_URL}" | tee -a "$GITHUB_OUTPUT"
+
+      - name: Fetch latest tags (if nightly)
+        if: matrix.branch_type == 'nightly'
+        run: |
+          git remote add nightly-testing https://github.com/leanprover-community/mathlib4-nightly-testing.git
+          git fetch nightly-testing --tags
+          LATEST_TAG=$(git tag | grep -E "${{ env.TAG_PATTERN }}" | sort -r | head -n 1)
+          echo "LATEST_TAG=${LATEST_TAG}" | tee -a "$GITHUB_ENV"
+
+      - name: Set branch ref
+        run: |
+          if [ "${{ matrix.branch_type }}" == "master" ]; then
+            echo "BRANCH_REF=${{ env.DEFAULT_BRANCH }}" >> "$GITHUB_ENV"
+          else
+            echo "BRANCH_REF=${{ env.LATEST_TAG }}" >> "$GITHUB_ENV"
+          fi
+
+      - name: Post success message for nanoda on Zulip
+        if: needs.check-nanoda.result == 'success'
+        uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5 # v1.0.2
+        with:
+          api-key: ${{ secrets.ZULIP_API_KEY }}
+          email: 'github-mathlib4-bot@leanprover.zulipchat.com'
+          organization-url: 'https://leanprover.zulipchat.com'
+          to: 'nightly-testing'
+          type: 'stream'
+          topic: 'nanoda'
+          content: |
+            ✅ nanoda [succeeded](${{ steps.get-status.outputs.nanoda_url }}) on ${{ github.sha }} (branch: ${{ env.BRANCH_REF }})
+
+      - name: Post failure / cancelled message for nanoda on Zulip
+        if: needs.check-nanoda.result != 'success'
+        uses: zulip/github-actions-zulip/send-message@e4c8f27c732ba9bd98ac6be0583096dea82feea5 # v1.0.2
+        with:
+          api-key: ${{ secrets.ZULIP_API_KEY }}
+          email: 'github-mathlib4-bot@leanprover.zulipchat.com'
+          organization-url: 'https://leanprover.zulipchat.com'
+          to: 'nightly-testing'
+          type: 'stream'
+          topic: 'nanoda failure'
+          content: |
+            ❌ nanoda [${{ needs.check-nanoda.result }}](${{ steps.get-status.outputs.nanoda_url }}) on ${{ github.sha }} (branch: ${{ env.BRANCH_REF }})

Cache/Init.lean

@@ -0,0 +1,16 @@
+/-
+Copyright (c) 2023 Arthur Paulino. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Arthur Paulino
+-/
+
+namespace Cache.Requests
+
+open System (FilePath)
+
+-- FRO cache may be flaky: https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/The.20cache.20doesn't.20work/near/411058849
+-- This is defined in a separate file because it is used in the definition of `URL` and `UPLOAD_URL`
+-- and Lean does not allow one `initialize` to use another `initialize` defined in the same file
+initialize useFROCache : Bool ← do
+  let froCache ← IO.getEnv "USE_FRO_CACHE"
+  return froCache == some "1" || froCache == some "true"

Cache/Requests.lean

@@ -6,16 +6,12 @@ Authors: Arthur Paulino
 
 import Batteries.Data.String.Matcher
 import Cache.Hashing
+import Cache.Init
 
 namespace Cache.Requests
 
 open System (FilePath)
 
--- FRO cache may be flaky: https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/The.20cache.20doesn't.20work/near/411058849
-initialize useFROCache : Bool ← do
-  let froCache ← IO.getEnv "USE_FRO_CACHE"
-  return froCache == some "1" || froCache == some "true"
-
 /--
 Structure to hold repository information with priority ordering
 -/
@@ -244,11 +240,14 @@ def getRemoteRepo (mathlibDepPath : FilePath) : IO RepoInfo := do
   return {repo := repo, useFirst := false}
 
 /-- Public URL for mathlib cache -/
-def URL : String :=
-  if useFROCache then
-    "https://mathlib4.lean-cache.cloud"
-  else
-    "https://lakecache.blob.core.windows.net/mathlib4"
+initialize URL : String ← do
+  let url? ← IO.getEnv "MATHLIB_CACHE_GET_URL"
+  let defaultUrl :=
+    if useFROCache then
+      "https://mathlib4.lean-cache.cloud"
+    else
+      "https://lakecache.blob.core.windows.net/mathlib4"
+  return url?.getD defaultUrl
 
 /-- Retrieves the azure token from the environment -/
 def getToken : IO String := do
@@ -467,7 +466,7 @@ where
   printLakeOutput out := do
     unless out.stdout.isEmpty do
       IO.eprintln "lake stdout:"
-      IO.eprint out.stderr
+      IO.eprint out.stdout
     unless out.stderr.isEmpty do
       IO.eprintln "lake stderr:"
       IO.eprint out.stderr
@@ -508,11 +507,14 @@ end Get
 section Put
 
 /-- FRO cache S3 URL -/
-def UPLOAD_URL : String :=
-  if useFROCache then
-    "https://a09a7664adc082e00f294ac190827820.r2.cloudflarestorage.com/mathlib4"
-  else
-    URL
+initialize UPLOAD_URL : String ← do
+  let url? ← IO.getEnv "MATHLIB_CACHE_PUT_URL"
+  let defaultUrl :=
+    if useFROCache then
+      "https://a09a7664adc082e00f294ac190827820.r2.cloudflarestorage.com/mathlib4"
+    else
+      "https://lakecache.blob.core.windows.net/mathlib4"
+  return url?.getD defaultUrl
 
 /-- Formats the config file for `curl`, containing the list of files to be uploaded -/
 def mkPutConfigContent (repo : String) (fileNames : Array String) (token : String) : IO String := do

Mathlib.lean

@@ -546,6 +546,7 @@ public import Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
 public import Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
 public import Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass
 public import Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear
+public import Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
 public import Mathlib.Algebra.Homology.DerivedCategory.Ext.TStructure
 public import Mathlib.Algebra.Homology.DerivedCategory.Fractions
 public import Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful
@@ -852,6 +853,7 @@ public import Mathlib.Algebra.Order.BigOperators.Group.Finset
 public import Mathlib.Algebra.Order.BigOperators.Group.List
 public import Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
 public import Mathlib.Algebra.Order.BigOperators.Group.Multiset
+public import Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
 public import Mathlib.Algebra.Order.BigOperators.GroupWithZero.List
 public import Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset
 public import Mathlib.Algebra.Order.BigOperators.Ring.Finset
@@ -1665,6 +1667,7 @@ public import Mathlib.Analysis.Complex.CauchyIntegral
 public import Mathlib.Analysis.Complex.Circle
 public import Mathlib.Analysis.Complex.Conformal
 public import Mathlib.Analysis.Complex.Convex
+public import Mathlib.Analysis.Complex.CoveringMap
 public import Mathlib.Analysis.Complex.Exponential
 public import Mathlib.Analysis.Complex.ExponentialBounds
 public import Mathlib.Analysis.Complex.Hadamard
@@ -2767,6 +2770,7 @@ public import Mathlib.CategoryTheory.Localization.Trifunctor
 public import Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
 public import Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
 public import Mathlib.CategoryTheory.LocallyCartesianClosed.Over
+public import Mathlib.CategoryTheory.LocallyCartesianClosed.Sections
 public import Mathlib.CategoryTheory.LocallyDirected
 public import Mathlib.CategoryTheory.MarkovCategory.Basic
 public import Mathlib.CategoryTheory.Monad.Adjunction
@@ -4990,6 +4994,7 @@ public import Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
 public import Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
 public import Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
 public import Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm
+public import Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue
 public import Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
 public import Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope
 public import Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
@@ -5005,6 +5010,7 @@ public import Mathlib.MeasureTheory.Integral.Lebesgue.Sub
 public import Mathlib.MeasureTheory.Integral.LebesgueNormedSpace
 public import Mathlib.MeasureTheory.Integral.Marginal
 public import Mathlib.MeasureTheory.Integral.MeanInequalities
+public import Mathlib.MeasureTheory.Integral.MeanValue
 public import Mathlib.MeasureTheory.Integral.PeakFunction
 public import Mathlib.MeasureTheory.Integral.Pi
 public import Mathlib.MeasureTheory.Integral.Prod
@@ -5217,6 +5223,8 @@ public import Mathlib.NumberTheory.Harmonic.EulerMascheroni
 public import Mathlib.NumberTheory.Harmonic.GammaDeriv
 public import Mathlib.NumberTheory.Harmonic.Int
 public import Mathlib.NumberTheory.Harmonic.ZetaAsymp
+public import Mathlib.NumberTheory.Height.Basic
+public import Mathlib.NumberTheory.Height.Instances
 public import Mathlib.NumberTheory.JacobiSum.Basic
 public import Mathlib.NumberTheory.KummerDedekind
 public import Mathlib.NumberTheory.LSeries.AbstractFuncEq
@@ -7235,6 +7243,7 @@ public import Mathlib.Topology.MetricSpace.Pseudo.Real
 public import Mathlib.Topology.MetricSpace.Sequences
 public import Mathlib.Topology.MetricSpace.ShrinkingLemma
 public import Mathlib.Topology.MetricSpace.Similarity
+public import Mathlib.Topology.MetricSpace.Snowflaking
 public import Mathlib.Topology.MetricSpace.ThickenedIndicator
 public import Mathlib.Topology.MetricSpace.Thickening
 public import Mathlib.Topology.MetricSpace.TransferInstance