Merge pull request #977 from leanprover-community/module_system

chore: move to module system

Author: zhikaip

PhysLean.lean

@@ -3,11 +3,13 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
+module
+
 /-!
 
 # Classical mechanics
 
 This file is currently a stub.
 Please feel free to contribute!
 
--/
+-/@[expose] public section

PhysLean/ClassicalMechanics/Basic.lean

@@ -3,9 +3,11 @@ Copyright (c) 2025 Nicola Bernini. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Nicola Bernini
 -/
-import PhysLean.Meta.Informal.SemiFormal
-import PhysLean.ClassicalMechanics.EulerLagrange
-import PhysLean.ClassicalMechanics.HamiltonsEquations
+module
+
+public import PhysLean.Meta.Informal.SemiFormal
+public import PhysLean.ClassicalMechanics.EulerLagrange
+public import PhysLean.ClassicalMechanics.HamiltonsEquations
 /-!
 
 # The Damped Harmonic Oscillator
@@ -59,6 +61,8 @@ References for the damped harmonic oscillator include:
 
 -/
 
+@[expose] public section
+
 namespace ClassicalMechanics
 open Real
 open ContDiff

PhysLean/ClassicalMechanics/DampedHarmonicOscillator/Basic.lean

@@ -3,7 +3,9 @@ Copyright (c) 2025 Tomas Skrivan. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Tomas Skrivan, Joseph Tooby-Smith
 -/
-import PhysLean.Mathematics.VariationalCalculus.HasVarGradient
+module
+
+public import PhysLean.Mathematics.VariationalCalculus.HasVarGradient
 /-!
 
 # Euler-Lagrange equations
@@ -14,6 +16,8 @@ and prove the that the variational derivative of the action functional
 
 -/
 
+@[expose] public section
+
 open MeasureTheory ContDiff InnerProductSpace Time
 
 variable {X} [NormedAddCommGroup X] [InnerProductSpace ℝ X] [CompleteSpace X]

PhysLean/ClassicalMechanics/EulerLagrange.lean

@@ -3,7 +3,9 @@ Copyright (c) 2025 Tomas Skrivan. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Tomas Skrivan, Joseph Tooby-Smith
 -/
-import PhysLean.Mathematics.VariationalCalculus.HasVarGradient
+module
+
+public import PhysLean.Mathematics.VariationalCalculus.HasVarGradient
 /-!
 
 # Hamilton's equations
@@ -23,6 +25,8 @@ applied to `(p, q)`.
 
 -/
 
+@[expose] public section
+
 open MeasureTheory ContDiff InnerProductSpace Time
 
 namespace ClassicalMechanics

PhysLean/ClassicalMechanics/HamiltonsEquations.lean

@@ -3,10 +3,12 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith, Lode Vermeulen
 -/
-import PhysLean.Meta.Informal.SemiFormal
-import PhysLean.ClassicalMechanics.EulerLagrange
-import PhysLean.ClassicalMechanics.HamiltonsEquations
-import PhysLean.ClassicalMechanics.HarmonicOscillator.ConfigurationSpace
+module
+
+public import PhysLean.Meta.Informal.SemiFormal
+public import PhysLean.ClassicalMechanics.EulerLagrange
+public import PhysLean.ClassicalMechanics.HamiltonsEquations
+public import PhysLean.ClassicalMechanics.HarmonicOscillator.ConfigurationSpace
 /-!
 
 # The Classical Harmonic Oscillator
@@ -81,6 +83,8 @@ References for the classical harmonic oscillator include:
 
 -/
 
+@[expose] public section
+
 namespace ClassicalMechanics
 open Real
 open Space

PhysLean/ClassicalMechanics/HarmonicOscillator/Basic.lean

@@ -3,15 +3,19 @@ Copyright (c) 2026 Nicola Bernini. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Nicola Bernini
 -/
-import Mathlib.Geometry.Manifold.Diffeomorph
-import PhysLean.SpaceAndTime.Time.Basic
+module
+
+public import Mathlib.Geometry.Manifold.Diffeomorph
+public import PhysLean.SpaceAndTime.Time.Basic
 /-!
 # Configuration space of the harmonic oscillator
 
 The configuration space is defined as a one-dimensional smooth manifold,
 modeled on `ℝ`, with a chosen coordinate.
 -/
 
+@[expose] public section
+
 namespace ClassicalMechanics
 
 namespace HarmonicOscillator

PhysLean/ClassicalMechanics/HarmonicOscillator/ConfigurationSpace.lean

@@ -3,9 +3,11 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith, Lode Vermeulen
 -/
-import Mathlib.Analysis.CStarAlgebra.Classes
-import PhysLean.ClassicalMechanics.HarmonicOscillator.Basic
-import PhysLean.Units.Basic
+module
+
+public import Mathlib.Analysis.CStarAlgebra.Classes
+public import PhysLean.ClassicalMechanics.HarmonicOscillator.Basic
+public import PhysLean.Units.Basic
 /-!
 
 # Solutions to the classical harmonic oscillator
@@ -53,6 +55,8 @@ References for the classical harmonic oscillator include:
 
 -/
 
+@[expose] public section
+
 namespace ClassicalMechanics
 open Real Time ContDiff
 

PhysLean/ClassicalMechanics/HarmonicOscillator/Solution.lean

@@ -3,7 +3,9 @@ Copyright (c) 2025 Rein Zustand. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rein Zustand
 -/
-import PhysLean.Mathematics.VariationalCalculus.HasVarGradient
+module
+
+public import PhysLean.Mathematics.VariationalCalculus.HasVarGradient
 /-!
 
 # Equivalent Lagrangians under Total Derivatives
@@ -51,6 +53,8 @@ This is because:
 
 -/
 
+@[expose] public section
+
 namespace ClassicalMechanics
 
 open InnerProductSpace

PhysLean/ClassicalMechanics/Lagrangian/TotalDerivativeEquivalence.lean

@@ -3,8 +3,10 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import Mathlib.Geometry.Manifold.Diffeomorph
-import PhysLean.SpaceAndTime.Time.Basic
+module
+
+public import Mathlib.Geometry.Manifold.Diffeomorph
+public import PhysLean.SpaceAndTime.Time.Basic
 /-!
 
 # Units on Mass
@@ -24,6 +26,8 @@ existence of the mass unit of kilograms, and construct all other mass units from
 
 -/
 
+@[expose] public section
+
 open NNReal
 
 /-- The choices of translationally-invariant metrics on the mass-manifold.