SHELL := /bin/sh
.DEFAULT_GOAL := all
.NOTPARALLEL:

export LEAN_NUM_THREADS := 1

.PHONY: all download setup check build audit clean

all: check

check: build audit
	@echo "Lean validation of all completed modules succeeded."

download setup:
	lake update
	lake exe cache get

build:
	lake build +GinibrePoincare.Endgame.SeriesDeficit:olean
	lake build +GinibrePoincare.Endgame.HilbertGeometry:olean
	lake build +GinibrePoincare.Endgame.GeneratorCompletion:olean
	lake build +GinibrePoincare.Endgame.TheoremOneNine:olean
	lake build +GinibrePoincare.Endgame.FiniteTheoremOneNine:olean
	lake build +GinibrePoincare.Endgame.ConcreteTheoremOneNine:olean
	lake build +GinibrePoincare.Concrete.Configuration:olean
	lake build +GinibrePoincare.Concrete.Vandermonde:olean
	lake build +GinibrePoincare.Concrete.Weights:olean
	lake build +GinibrePoincare.Concrete.GroundState:olean
	lake build +GinibrePoincare.Concrete.CenterOfMass:olean
	lake build +GinibrePoincare.Concrete.GaussianProbability:olean
	lake build +GinibrePoincare.Concrete.MeasureModel:olean
	lake build +GinibrePoincare.Concrete.NormalizedGroundState:olean
	lake build +GinibrePoincare.Concrete.SmoothTarget:olean
	lake build +GinibrePoincare.Concrete.Wirtinger:olean
	lake build +GinibrePoincare.Concrete.HolomorphicDistance:olean
	lake build +GinibrePoincare.Concrete.AnalyticStatements:olean
	lake build +GinibrePoincare.Concrete.MainProofReduction:olean
	lake build +GinibrePoincare.Concrete.ModeReduction:olean
	lake build +GinibrePoincare.Concrete.Generator:olean
	lake build +GinibrePoincare.Analysis.GaussianDensity:olean
	lake build +GinibrePoincare.Analysis.ComplexHermite:olean
	lake build +GinibrePoincare.Analysis.ComplexHermiteLowering:olean
	lake build +GinibrePoincare.Analysis.NormalizedComplexHermite:olean
	lake build +GinibrePoincare.Analysis.MultivariateComplexHermite:olean
	lake build +GinibrePoincare.Analysis.HermiteWirtinger:olean
	lake build +GinibrePoincare.Analysis.ComplexHermiteOrthogonality:olean
	lake build +GinibrePoincare.Analysis.MultivariateHermiteIntegrability:olean
	lake build +GinibrePoincare.Analysis.HermiteOrthogonalityCombinatorics:olean
	lake build +GinibrePoincare.Analysis.HermiteBinomialIdentity:olean
	lake build +GinibrePoincare.Analysis.GaussianPolynomialDensity:olean
	lake build +GinibrePoincare.Analysis.GaussianPolynomialCompleteness:olean
	lake build +GinibrePoincare.Analysis.HermiteMonomialSpan:olean
	lake build +GinibrePoincare.Analysis.MultivariateHermiteMonomialSpan:olean
	lake build +GinibrePoincare.Analysis.GaussianHermiteMoments:olean
	lake build +GinibrePoincare.Analysis.GaussianFourierCoordinates:olean
	lake build +GinibrePoincare.Analysis.GaussianFourierUniqueness:olean
	lake build +GinibrePoincare.Analysis.HermiteL2Family:olean
	lake build +GinibrePoincare.Analysis.HermiteParsevalModes:olean
	lake build +GinibrePoincare.Analysis.HermiteWeightedEnergy:olean
	lake build +GinibrePoincare.Analysis.VandermondeGroundStateZeroMode:olean
	lake build +GinibrePoincare.Analysis.WeightedSeriesTruncation:olean
	lake build +GinibrePoincare.Analysis.GaussianDbarParseval:olean
	lake build +GinibrePoincare.Analysis.RealGaussianIntegrationByParts:olean
	lake build +GinibrePoincare.Analysis.ComplexGaussianIntegrationByParts:olean
	lake build +GinibrePoincare.Analysis.ComplexGaussianProductIntegral:olean
	lake build +GinibrePoincare.Analysis.PolynomialCompactApproximation:olean
	lake build +GinibrePoincare.Analysis.HermiteEnergy:olean
	lake build +GinibrePoincare.Analysis.FiniteHermiteDeficit:olean
	lake build +GinibrePoincare.Analysis.L2RepresentativeBridges:olean
	lake build +GinibrePoincare.Analysis.GroundStateDbar:olean
	lake build +GinibrePoincare.Analysis.HolomorphicVandermondeDivision:olean
	lake build +GinibrePoincare.Analysis.HolomorphicVandermondeL2Closure:olean
	lake build +GinibrePoincare.Analysis.GinibreConjugationGeometry:olean
	lake build +GinibrePoincare.Analysis.GlobalPhaseAction:olean
	lake build +GinibrePoincare.Analysis.GinibreIntegrationByParts:olean
	lake build +GinibrePoincare.Analysis.GinibreGeneratorL2:olean
	lake build +GinibrePoincare.Analysis.FinitePiDensity:olean
	lake build +GinibrePoincare.Analysis.MeasureTransport:olean
	lake build +GinibrePoincare.Analysis.ComplexGaussianDensity:olean
	lake build +GinibrePoincare.Analysis.GinibreMassPositivity:olean
	lake build +GinibrePoincare.Analysis.GaussianPolynomialIntegrability:olean
	lake build +GinibrePoincare.Analysis.ComplexGaussianMoments:olean
	lake build +GinibrePoincare.Analysis.AngularMoments:olean
	lake build +GinibrePoincare.Analysis.RadialMoments:olean
	lake build +GinibrePoincare.Analysis.PolarGaussianMoments:olean
	lake build +GinibrePoincare.Analysis.GinibreMassFiniteness:olean
	lake build +GinibrePoincare.Analysis.CollisionNull:olean
	lake build +GinibrePoincare.Analysis.VandermondeL2:olean
	lake build +GinibrePoincare.Analysis.PermutationLp:olean
	lake build +GinibrePoincare.Analysis.VandermondeSymmetryL2:olean
	lake build +GinibrePoincare.Analysis.VandermondeL2Inverse:olean
	lake build +GinibrePoincare:olean

audit:
	lake env lean AxiomAudit.lean

clean:
	lake clean