Publish a downloadable build cache (Physlib + PhyslibAlpha)

.github/workflows/alphaBuild.yml

@@ -13,6 +13,9 @@ jobs:
   alpha_build:
     name: Lean based style linters
     runs-on: ubuntu-latest
+    env:
+      LAKE_CACHE_DIR: .lake/cache
+      HAVE_CACHE_KEY: ${{ secrets.LAKE_CACHE_KEY != '' }}
     steps:
 
       - uses: actions/checkout@v4
@@ -41,6 +44,44 @@ jobs:
           run: |
             bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build -KCI PhyslibAlpha | tee stdout.log"
 
+      # PhyslibAlpha is not a default target, so build.yml never builds or
+      # publishes it. Same R2 bucket and scope as build.yml -- artifacts are
+      # content-addressed by hash, so the two workflows' uploads coexist
+      # without needing separate scopes.
+      - name: stage build outputs for the cache
+        id: stage
+        if: github.event_name == 'push' && env.HAVE_CACHE_KEY == 'true'
+        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: github.event_name == 'push' && env.HAVE_CACHE_KEY == 'true' && 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=physlib-master \
+            --rev="${{ github.sha }}" \
+            --toolchain="$(cat lean-toolchain)"
+
+      - name: warn if cache publish failed
+        if: github.event_name == 'push' && env.HAVE_CACHE_KEY == 'true' && (steps.stage.outcome == 'failure' || steps.publish.outcome == 'failure')
+        run: echo "::warning::PhyslibAlpha build cache was not published this run."
+
       - name: runLinter on PhyslibAlpha
         if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
         id: lint
@@ -53,6 +94,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 +121,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,6 +13,13 @@ jobs:
   doc_lint:
     name: Lean based style linters
     runs-on: ubuntu-latest
+    env:
+      # Keep Lake's artifact cache inside the workspace rather than the
+      # toolchain directory, so it is scoped to this run and easy to stage.
+      LAKE_CACHE_DIR: .lake/cache
+      # Job-level so the cache steps can gate on it: a step's own `env:` block
+      # is not visible to that step's `if:` condition.
+      HAVE_CACHE_KEY: ${{ secrets.LAKE_CACHE_KEY != '' }}
     steps:
 
       - uses: actions/checkout@v4
@@ -41,6 +48,52 @@ jobs:
           run: |
             bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build -KCI | tee stdout.log"
 
+      # Publish to the R2 bucket via Lake's own content-addressed cache.
+      # Skipped entirely until LAKE_CACHE_KEY exists, so CI keeps working
+      # before the bucket is provisioned. See docs/cache-setup.md.
+      #
+      # continue-on-error on both steps: a stale or unreachable cache is an
+      # inconvenience, not a correctness problem, and must never block a
+      # merge. A failure here is surfaced via the warning step below instead.
+      - name: stage build outputs for the cache
+        id: stage
+        if: github.event_name == 'push' && env.HAVE_CACHE_KEY == 'true'
+        continue-on-error: true
+        run: |
+          set -euo pipefail
+          mkdir -p ../lake-cache-staging
+          # `--no-build` here does not build anything; it emits the
+          # input-to-output mappings for what was just built.
+          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: github.event_name == 'push' && env.HAVE_CACHE_KEY == 'true' && 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=physlib-master \
+            --rev="${{ github.sha }}" \
+            --toolchain="$(cat lean-toolchain)"
+
+      - name: warn if cache publish failed
+        if: github.event_name == 'push' && env.HAVE_CACHE_KEY == 'true' && (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."
+
       - name: check file imports
         run: |
           bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake exe check_file_imports"

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,10 @@ 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.LiftInvariance
 public import Physlib.ClassicalMechanics.Pendulum.SlidingPendulum
 public import Physlib.ClassicalMechanics.RigidBody.AngularMomentum
 public import Physlib.ClassicalMechanics.RigidBody.AngularVelocity
@@ -99,6 +103,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 +142,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 +343,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
@@ -441,11 +452,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 +549,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

Physlib/ClassicalMechanics/HarmonicOscillator/Basic.lean

@@ -7,6 +7,7 @@ module
 
 public import Physlib.ClassicalMechanics.EulerLagrange
 public import Physlib.ClassicalMechanics.HamiltonsEquations
+public import Physlib.Mathematics.Calculus.Gradient
 public import Mathlib.Algebra.Order.Archimedean.Real.Hom
 /-!
 
@@ -337,25 +338,6 @@ lemma contDiff_lagrangian (n : WithTop ℕ∞) : ContDiff ℝ n ↿S.lagrangian
   rw [lagrangian_eq]
   fun_prop
 
-lemma toDual_symm_innerSL (x : EuclideanSpace ℝ (Fin 1)) :
-    (InnerProductSpace.toDual ℝ (EuclideanSpace ℝ (Fin 1))).symm (innerSL ℝ x) = x :=
-  (InnerProductSpace.toDual ℝ (EuclideanSpace ℝ (Fin 1))).symm_apply_apply x
-
-lemma gradient_inner_self (x : EuclideanSpace ℝ (Fin 1)) :
-    gradient (fun y : EuclideanSpace ℝ (Fin 1) => ⟪y, y⟫_ℝ) x = (2 : ℝ) • x := by
-  refine ext_inner_right (𝕜 := ℝ) fun y => ?_
-  unfold gradient
-  rw [InnerProductSpace.toDual_symm_apply,
-    fderiv_inner_apply (𝕜 := ℝ) differentiableAt_fun_id differentiableAt_fun_id]
-  simp [real_inner_comm, inner_smul_right, two_mul]
-
-lemma gradient_const_mul_inner_self (c : ℝ) (x : EuclideanSpace ℝ (Fin 1)) :
-    gradient (fun y : EuclideanSpace ℝ (Fin 1) => c * ⟪y, y⟫_ℝ) x = (2 * c) • x := by
-  unfold gradient
-  rw [fderiv_const_mul (by fun_prop) c, map_smul]
-  show c • gradient (fun y : EuclideanSpace ℝ (Fin 1) => ⟪y, y⟫_ℝ) x = (2 * c) • x
-  rw [gradient_inner_self, smul_smul, mul_comm]
-
 /-!
 
 #### D.1.3. Gradients of the lagrangian
@@ -365,18 +347,13 @@ position and velocity.
 
 -/
 
-private lemma gradient_add_const' {f : EuclideanSpace ℝ (Fin 1) → ℝ} {c : ℝ}
-    (x : EuclideanSpace ℝ (Fin 1)) :
-    gradient (fun y => f y + c) x = gradient f x :=
-  congrArg (InnerProductSpace.toDual ℝ (EuclideanSpace ℝ (Fin 1))).symm (fderiv_add_const c)
-
 lemma gradient_lagrangian_position_eq (t : Time) (x : EuclideanSpace ℝ (Fin 1))
     (v : EuclideanSpace ℝ (Fin 1)) :
     gradient (fun x => lagrangian S t x v) x = - S.k • x := by
   have h_eq : (fun y : EuclideanSpace ℝ (Fin 1) => lagrangian S t y v) =
       fun y => (-(1 / (2 : ℝ)) * S.k) * ⟪y, y⟫_ℝ + (1 / (2 : ℝ) * S.m * ⟪v, v⟫_ℝ) := by
     funext y; simp only [lagrangian_eq]; ring
-  rw [h_eq, gradient_add_const', gradient_const_mul_inner_self]
+  rw [h_eq, gradient_add_const, gradient_const_mul_inner_self]
   module
 
 lemma gradient_lagrangian_velocity_eq (t : Time) (x : EuclideanSpace ℝ (Fin 1))
@@ -386,7 +363,7 @@ lemma gradient_lagrangian_velocity_eq (t : Time) (x : EuclideanSpace ℝ (Fin 1)
       fun y => ((1 / (2 : ℝ)) * S.m) * ⟪y, y⟫_ℝ + (-(1 / (2 : ℝ)) * S.k * ⟪x, x⟫_ℝ) := by
     funext y; simp only [lagrangian_eq]; ring
   change gradient (fun y : EuclideanSpace ℝ (Fin 1) => lagrangian S t x y) v = S.m • v
-  rw [h_eq, gradient_add_const', gradient_const_mul_inner_self]
+  rw [h_eq, gradient_add_const, gradient_const_mul_inner_self]
   module
 
 /-!
@@ -679,7 +656,7 @@ lemma gradient_hamiltonian_position_eq (t : Time) (x : EuclideanSpace ℝ (Fin 1
     simp only [hamiltonian_eq]
     ring
   change gradient (fun y : EuclideanSpace ℝ (Fin 1) => hamiltonian S t p y) x = S.k • x
-  rw [h_eq, gradient_add_const', gradient_const_mul_inner_self]
+  rw [h_eq, gradient_add_const, gradient_const_mul_inner_self]
   module
 
 lemma gradient_hamiltonian_momentum_eq (t : Time) (x : EuclideanSpace ℝ (Fin 1))
@@ -691,7 +668,7 @@ lemma gradient_hamiltonian_momentum_eq (t : Time) (x : EuclideanSpace ℝ (Fin 1
     funext y
     simp only [hamiltonian_eq]
   change gradient (fun y : EuclideanSpace ℝ (Fin 1) => hamiltonian S t y x) p = (1 / S.m) • p
-  rw [h_eq, gradient_add_const', gradient_const_mul_inner_self]
+  rw [h_eq, gradient_add_const, gradient_const_mul_inner_self]
   module
 
 /-!

Physlib/ClassicalMechanics/Pendulum/API-map.yaml

@@ -9,13 +9,15 @@ Overview: |
     covers the pendulum problems of Landau and Lifshitz, Mechanics, 3rd ed.,
     Chapter 1, Section 5.
 
-    At present only the sliding pendulum has a defined configuration space, with
-    the horizontal support position and the string angle as its generalized
-    coordinates. The coplanar double pendulum's configuration space is declared but
-    not yet defined, and the miscellaneous pivot-motion problems have documentation
-    only. The remaining requirements, a manifold structure on the configuration
-    space, a map into real space, trajectories, and the lagrangian, are open and
-    recorded below with location N/A.
+    The sliding pendulum has a defined configuration space in the generalized coordinates of the
+    support position and the string angle. The simple pendulum's configuration space, an angle
+    modulo a full turn, carries the manifold structure and the map into `Space`; it has its own API
+    map in `Physlib/ClassicalMechanics/Pendulum/SimplePendulum`. The coplanar double pendulum's
+    configuration space is declared but not yet defined, and the miscellaneous pivot-motion problems
+    have documentation only. The simple pendulum's Lagrangian and equation of motion on the
+    Euclidean lift are recorded in its own API map; the trajectory based on the configuration
+    space, and the Lagrangian derived from it, remain open and are recorded below with location
+    N/A.
 
 ParentAPIs:
   - Classical mechanics Lagrangian (Physlib/ClassicalMechanics/Lagrangian)
@@ -33,15 +35,13 @@ Requirements:
     done: true
     location: Physlib/ClassicalMechanics/Pendulum/SlidingPendulum.lean (ConfigurationSpace)
 
-  - description: The API shall contain the structure of a manifold on the configuration space.
-    done: false
-    location: "N/A"
+  - description: The API contains the structure of a manifold on the configuration space (for the simple pendulum).
+    done: true
+    location: Physlib/ClassicalMechanics/Pendulum/SimplePendulum/Geometric/Basic.lean (SimplePendulum.ConfigurationSpace.instIsManifold)
 
-  - description: >
-      The API shall contain a map from the configuration space to `Space`, giving the
-      position of the pendulum in real space.
-    done: false
-    location: "N/A"
+  - description: The API contains a map from the configuration space to `Space`, giving the position of the pendulum in real space (for the simple pendulum).
+    done: true
+    location: Physlib/ClassicalMechanics/Pendulum/SimplePendulum/Geometric/Basic.lean (SimplePendulum.ConfigurationSpace.toSpace)
 
   - description: The API shall contain the definition of a trajectory based on the configuration space.
     done: false