TEST: use cache in linter builds

.github/workflows/alphaBuild.yml

@@ -13,9 +13,14 @@ jobs:
   alpha_build:
     name: Lean based style linters
     runs-on: ubuntu-latest
+    env:
+      LAKE_CACHE_DIR: .lake/cache
     steps:
 
+      # Full history so lake can look back for a commit with a cache, see build.yml
       - uses: actions/checkout@v4
+        with:
+          fetch-depth: 0
 
       - name: Install elan
         run: |
@@ -33,6 +38,14 @@ jobs:
         run: |
           lake exe cache get
 
+      # PhyslibAlpha has its own cache in the bucket so we pull that one
+      - name: restore PhyslibAlpha's build cache
+        env:
+          LAKE_CONFIG: ${{ github.workspace }}/lake-cache.toml
+        run: |
+          lake cache get --scope="physlib-master/$(tr '/:' '--' < lean-toolchain | tr -d '[:space:]')/alpha" \
+            || echo "no existing cache to restore -- building from scratch"
+
       - name: build PhyslibAlpha
         id: build
         uses: liskin/gh-problem-matcher-wrap@v3
@@ -53,6 +66,10 @@ jobs:
       - name: Check no PhyslibAlpha in Physlib and QuantumInfo
         run: env LEAN_ABORT_ON_PANIC=1 lake exe noAlphaImports
 
+      - name: Check PhyslibAlpha imports
+        run: env LEAN_ABORT_ON_PANIC=1 lake exe alphaFileImports
+
+
   style_lint:
     name: Python based linters
     runs-on: ubuntu-latest
@@ -76,12 +93,6 @@ jobs:
         with:
           python-version: 3.8
 
-      - name: Check PhyslibAlpha imports
-        run: |
-          chmod u+x scripts/PhyslibAlpha/alphaFileImports.py
-          ./scripts/PhyslibAlpha/alphaFileImports.py
-
-
       - name: Python linters for PhyslibAlpha
         run: |
           chmod u+x scripts/PhyslibAlpha/alphaPythonLinters.sh

.github/workflows/build.yml

@@ -13,9 +13,15 @@ jobs:
   doc_lint:
     name: Lean based style linters
     runs-on: ubuntu-latest
+    env:
+      LAKE_CACHE_DIR: .lake/cache
     steps:
 
+      # Need the full history here, lake looks back through the commits to find
+      # one with a cache. A shallow clone only has one so it never finds anything.
       - uses: actions/checkout@v4
+        with:
+          fetch-depth: 0
 
       - name: Install elan
         run: |
@@ -33,6 +39,15 @@ jobs:
         run: |
           lake exe cache get
 
+      # Pulls the cache from the bucket so we only compile what the PR changed.
+      # No key needed as it is only reading. If it fails we just build from scratch.
+      - name: restore Physlib's build cache
+        env:
+          LAKE_CONFIG: ${{ github.workspace }}/lake-cache.toml
+        run: |
+          lake cache get --scope="physlib-master/$(tr '/:' '--' < lean-toolchain | tr -d '[:space:]')/physlib" \
+            || echo "no existing cache to restore -- building from scratch"
+
       - name: build Physlib
         id: build
         uses: liskin/gh-problem-matcher-wrap@v3

.github/workflows/publish-cache.yml

@@ -0,0 +1,187 @@
+on:
+  push:
+    branches:
+      - master
+
+name: Publish build cache
+
+# Pulls the cache from the bucket and then does a build with the new changes that are being merged
+# Then it creates a new cache which is pushed to the web bucket where they can be accessed
+# by `lake exe get_cache`.
+
+jobs:
+  # `secrets` is not allowed in a job-level `if:` -- GitHub rejects the whole
+  # file. Gating on a `needs` output instead skips the build jobs when the
+  # bucket is not set up yet.
+  gate:
+    name: Check for cache credentials
+    runs-on: ubuntu-latest
+    outputs:
+      has_key: ${{ steps.check.outputs.has_key }}
+    steps:
+      - name: look for LAKE_CACHE_KEY
+        id: check
+        env:
+          LAKE_CACHE_KEY: ${{ secrets.LAKE_CACHE_KEY }}
+        run: |
+          set -euo pipefail
+          if [ -n "$LAKE_CACHE_KEY" ]; then
+            echo "has_key=true" >> "$GITHUB_OUTPUT"
+          else
+            echo "::notice::LAKE_CACHE_KEY is not set, so the build cache will not be published. See docs/cache-setup.md."
+            echo "has_key=false" >> "$GITHUB_OUTPUT"
+          fi
+
+  physlib:
+    name: Physlib + QuantumInfo
+    needs: gate
+    if: needs.gate.outputs.has_key == 'true'
+    runs-on: ubuntu-latest
+    env:
+      LAKE_CACHE_DIR: .lake/cache
+    steps:
+      - uses: actions/checkout@v4
+
+      # Each job needs its own scope: Lake PUTs the revision mappings to
+      # <revisionEndpoint>/<scope>/<sha>.jsonl, so a shared scope would have
+      # one job overwrite the other's. The toolchain is in the scope because
+      # Lake ignores --toolchain for verbatim scopes.
+      # scripts/get_cache.lean builds the same strings -- keep them in step.
+      - name: compute cache scope
+        run: |
+          set -euo pipefail
+          TC="$(tr '/:' '--' < lean-toolchain | tr -d '[:space:]')"
+          echo "CACHE_SCOPE=physlib-master/$TC/physlib" >> "$GITHUB_ENV"
+
+      - name: Install elan
+        run: |
+          set -o pipefail
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
+          ~/.elan/bin/lean --version
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+
+      - name: build cache
+        run: |
+          lake exe cache get
+
+      # This reads the existing info in the bucket so that we only have to update whats changed
+      # If the bucket is empty we will have to build from scratch.
+      - name: restore Physlib's own cache
+        env:
+          LAKE_CONFIG: ${{ github.workspace }}/lake-cache.toml
+        run: |
+          lake cache get --scope="$CACHE_SCOPE" || echo "no existing cache to restore -- building from scratch"
+
+      - name: build Physlib
+        run: |
+          bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build -KCI | tee stdout.log"
+
+      # `--no-build` here does not build anything; it emits the
+      # input-to-output mappings for what was just built.
+      - name: stage build outputs for the cache
+        id: stage
+        continue-on-error: true
+        run: |
+          set -euo pipefail
+          mkdir -p ../lake-cache-staging
+          lake build --no-build -KCI -o .lake/outputs.jsonl
+          echo "mappings: $(wc -l < .lake/outputs.jsonl) entries"
+          lake cache stage .lake/outputs.jsonl ../lake-cache-staging
+          echo "staged: $(find ../lake-cache-staging -name '*.ltar' | wc -l) ltar files"
+
+      - name: publish to R2 cache
+        id: publish
+        if: steps.stage.outcome == 'success'
+        continue-on-error: true
+        env:
+          LAKE_CACHE_KEY_RAW: ${{ secrets.LAKE_CACHE_KEY }}
+          LAKE_CONFIG: ${{ github.workspace }}/lake-cache.toml
+        run: |
+          set -euo pipefail
+          # GitHub secrets commonly carry a trailing newline, which breaks the
+          # SigV4 signature. Trim it, and mask the value so it cannot surface
+          # in logs.
+          KEY="$(printf %s "$LAKE_CACHE_KEY_RAW" | sed -e 's/[[:space:]]*$//')"
+          echo "::add-mask::$KEY"
+          export LAKE_CACHE_KEY="$KEY"
+
+          lake cache put-staged ../lake-cache-staging \
+            --scope="$CACHE_SCOPE" \
+            --rev="${{ github.sha }}"
+
+      - name: warn if cache publish failed
+        if: steps.stage.outcome == 'failure' || steps.publish.outcome == 'failure'
+        run: echo "::warning::Physlib build cache was not published this run (staging or upload failed). Contributors will fall back to compiling from source until the next successful push."
+
+  physlib_alpha:
+    name: PhyslibAlpha
+    needs: gate
+    if: needs.gate.outputs.has_key == 'true'
+    runs-on: ubuntu-latest
+    env:
+      LAKE_CACHE_DIR: .lake/cache
+    steps:
+      - uses: actions/checkout@v4
+
+      # Own scope, so this job does not overwrite the physlib job's mappings.
+      - name: compute cache scope
+        run: |
+          set -euo pipefail
+          TC="$(tr '/:' '--' < lean-toolchain | tr -d '[:space:]')"
+          echo "CACHE_SCOPE=physlib-master/$TC/alpha" >> "$GITHUB_ENV"
+
+      - name: Install elan
+        run: |
+          set -o pipefail
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
+          ~/.elan/bin/lean --version
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+
+      - name: build cache
+        run: |
+          lake exe cache get
+
+      # See the physlib job's "restore Physlib's own cache" step -- same
+      # idea, seeding from this job's own scope before its build.
+      - name: restore PhyslibAlpha's own cache
+        env:
+          LAKE_CONFIG: ${{ github.workspace }}/lake-cache.toml
+        run: |
+          lake cache get --scope="$CACHE_SCOPE" || echo "no existing cache to restore -- building from scratch"
+
+      - name: build PhyslibAlpha
+        run: |
+          bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build -KCI PhyslibAlpha | tee stdout.log"
+
+      # Stage the cache so it can be pushed to the bucket
+      - name: stage build outputs for the cache
+        id: stage
+        continue-on-error: true
+        run: |
+          set -euo pipefail
+          mkdir -p ../lake-cache-staging
+          lake build --no-build -KCI PhyslibAlpha -o .lake/outputs.jsonl
+          echo "mappings: $(wc -l < .lake/outputs.jsonl) entries"
+          lake cache stage .lake/outputs.jsonl ../lake-cache-staging
+          echo "staged: $(find ../lake-cache-staging -name '*.ltar' | wc -l) ltar files"
+
+      - name: publish to R2 cache
+        id: publish
+        if: steps.stage.outcome == 'success'
+        continue-on-error: true
+        env:
+          LAKE_CACHE_KEY_RAW: ${{ secrets.LAKE_CACHE_KEY }}
+          LAKE_CONFIG: ${{ github.workspace }}/lake-cache.toml
+        run: |
+          set -euo pipefail
+          KEY="$(printf %s "$LAKE_CACHE_KEY_RAW" | sed -e 's/[[:space:]]*$//')"
+          echo "::add-mask::$KEY"
+          export LAKE_CACHE_KEY="$KEY"
+
+          lake cache put-staged ../lake-cache-staging \
+            --scope="$CACHE_SCOPE" \
+            --rev="${{ github.sha }}"
+
+      - name: warn if cache publish failed
+        if: steps.stage.outcome == 'failure' || steps.publish.outcome == 'failure'
+        run: echo "::warning::PhyslibAlpha build cache was not published this run."

AGENTS.md

@@ -59,7 +59,7 @@ When a long proof cannot be split, make sure it contains comments.
 - If edited a `PhyslibAlpha` file, check the following:
   - `lake exe runPhyslibAlphaLinters`
   - `lake exe noAlphaImports`
-  - `./scripts/PhyslibAlpha/alphaFileImports.py`
+  - `lake exe alphaFileImports`
   - `./scripts/PhyslibAlpha/alphaPythonLinters.sh`
 
 ## PR scope

Physlib.lean

@@ -17,6 +17,11 @@ public import Physlib.ClassicalMechanics.Mass.MassUnit
 public import Physlib.ClassicalMechanics.OrbitalMechanics.VisViva
 public import Physlib.ClassicalMechanics.Pendulum.CoplanarDoublePendulum
 public import Physlib.ClassicalMechanics.Pendulum.MiscellaneousPendulumPivotMotions
+public import Physlib.ClassicalMechanics.Pendulum.SimplePendulum.Basic
+public import Physlib.ClassicalMechanics.Pendulum.SimplePendulum.Equilibria
+public import Physlib.ClassicalMechanics.Pendulum.SimplePendulum.Geometric.Basic
+public import Physlib.ClassicalMechanics.Pendulum.SimplePendulum.Hamiltonian
+public import Physlib.ClassicalMechanics.Pendulum.SimplePendulum.LiftInvariance
 public import Physlib.ClassicalMechanics.Pendulum.SlidingPendulum
 public import Physlib.ClassicalMechanics.RigidBody.AngularMomentum
 public import Physlib.ClassicalMechanics.RigidBody.AngularVelocity
@@ -99,6 +104,7 @@ public import Physlib.FluidDynamics.ThermodynamicCauchyFlow.Bernoulli
 public import Physlib.FluidDynamics.ThermodynamicCauchyFlow.Isentropic
 public import Physlib.Mathematics.Calculus.AdjFDeriv
 public import Physlib.Mathematics.Calculus.Divergence
+public import Physlib.Mathematics.Calculus.Gradient
 public import Physlib.Mathematics.Calculus.ParametricIntegration
 public import Physlib.Mathematics.Calculus.Wirtinger.Basic
 public import Physlib.Mathematics.Calculus.Wirtinger.Coordinate
@@ -137,7 +143,9 @@ public import Physlib.Mathematics.RatComplexNum
 public import Physlib.Mathematics.Resolvent
 public import Physlib.Mathematics.SO3.Basic
 public import Physlib.Mathematics.SchurTriangulation
+public import Physlib.Mathematics.SpecialFunctions.EllipticIntegral
 public import Physlib.Mathematics.SpecialFunctions.PhysHermite
+public import Physlib.Mathematics.Trigonometry.SinSq
 public import Physlib.Mathematics.Trigonometry.Tanh
 public import Physlib.Mathematics.VariationalCalculus.Basic
 public import Physlib.Mathematics.VariationalCalculus.HasVarAdjDeriv
@@ -336,6 +344,10 @@ public import Physlib.QuantumMechanics.Hydrogen.Basic
 public import Physlib.QuantumMechanics.Hydrogen.LaplaceRungeLenzVector
 public import Physlib.QuantumMechanics.InfiniteSquareWell.Basic
 public import Physlib.QuantumMechanics.OperatorAlgebra.Basic
+public import Physlib.QuantumMechanics.OperatorAlgebra.Dynamics.Automorphism
+public import Physlib.QuantumMechanics.OperatorAlgebra.HilbertSpace
+public import Physlib.QuantumMechanics.OperatorAlgebra.Observables.Jordan
+public import Physlib.QuantumMechanics.OperatorAlgebra.Observables.Lie
 public import Physlib.QuantumMechanics.Operators.AngularMomentum
 public import Physlib.QuantumMechanics.Operators.Commutation
 public import Physlib.QuantumMechanics.Operators.Covariance
@@ -433,6 +445,7 @@ public import Physlib.Relativity.Tensors.Dual
 public import Physlib.Relativity.Tensors.Elab
 public import Physlib.Relativity.Tensors.Evaluation
 public import Physlib.Relativity.Tensors.LeviCivita.Basic
+public import Physlib.Relativity.Tensors.LeviCivita.Complex
 public import Physlib.Relativity.Tensors.LeviCivita.Contractions
 public import Physlib.Relativity.Tensors.MetricTensor
 public import Physlib.Relativity.Tensors.OfInt
@@ -441,11 +454,13 @@ public import Physlib.Relativity.Tensors.RealTensor.Basic
 public import Physlib.Relativity.Tensors.RealTensor.CoVector.Basic
 public import Physlib.Relativity.Tensors.RealTensor.CoVector.Representation
 public import Physlib.Relativity.Tensors.RealTensor.CoVector.Tensorial
+public import Physlib.Relativity.Tensors.RealTensor.Contraction.CrossToEnd
 public import Physlib.Relativity.Tensors.RealTensor.Matrix.Pre
 public import Physlib.Relativity.Tensors.RealTensor.Metrics.Basic
 public import Physlib.Relativity.Tensors.RealTensor.Metrics.Pre
 public import Physlib.Relativity.Tensors.RealTensor.Representation.Contraction
 public import Physlib.Relativity.Tensors.RealTensor.ToComplex
+public import Physlib.Relativity.Tensors.RealTensor.Units.Basic
 public import Physlib.Relativity.Tensors.RealTensor.Units.Pre
 public import Physlib.Relativity.Tensors.RealTensor.Vector.Basic
 public import Physlib.Relativity.Tensors.RealTensor.Vector.Causality.Basic
@@ -536,6 +551,7 @@ public import Physlib.Thermodynamics.Temperature.TemperatureUnits
 public import Physlib.Units.Basic
 public import Physlib.Units.Dimension
 public import Physlib.Units.Examples
+public import Physlib.Units.Exponent
 public import Physlib.Units.FDeriv
 public import Physlib.Units.ISQBridge
 public import Physlib.Units.ISQDimensionBase

Physlib/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean

@@ -504,11 +504,6 @@ lagrangian, using that the gradient scales with the constant `exp (γ/m * t)`.
 
 -/
 
-private lemma gradient_const_mul {f : EuclideanSpace ℝ (Fin 1) → ℝ} {x : EuclideanSpace ℝ (Fin 1)}
-    (c : ℝ) (hf : DifferentiableAt ℝ f x) :
-    gradient (fun y => c * f y) x = c • gradient f x := by
-  simp [gradient, fderiv_const_mul hf, map_smul]
-
 lemma gradient_lagrangian_position_eq (t : Time) (x v : EuclideanSpace ℝ (Fin 1)) :
     gradient (fun x => S.lagrangian t x v) x = -(exp (S.γ / S.m * t) * S.k) • x := by
   have hf : DifferentiableAt ℝ (fun y => S.toHarmonicOscillator.lagrangian t y v) x := by