From 4f9e2e5979daf0b9934cc9d2ff9fe9909e7620c2 Mon Sep 17 00:00:00 2001 From: Batixx Date: Fri, 17 Jul 2026 16:07:28 +0200 Subject: [PATCH 1/7] . --- Cslib/Computability/Languages/OmegaLanguage.lean | 2 -- .../Machines/Turing/SingleTape/NonDeterministic.lean | 1 - Cslib/Crypto/Protocols/PerfectSecrecy/Basic.lean | 1 - Cslib/Crypto/Protocols/PerfectSecrecy/Defs.lean | 1 - .../Protocols/PerfectSecrecy/Internal/PerfectSecrecy.lean | 1 - Cslib/Crypto/Protocols/PerfectSecrecy/OneTimePad.lean | 1 - Cslib/Crypto/Protocols/SecretSharing/Scheme.lean | 1 - Cslib/Foundations/Data/HasFresh.lean | 1 - Cslib/Foundations/Logic/LogicalEquivalence.lean | 1 - Cslib/Foundations/Relation/Attr.lean | 1 - Cslib/Foundations/Relation/Restriction.lean | 1 - Cslib/Foundations/Semantics/LTS/Bisimulation.lean | 1 - Cslib/Foundations/Semantics/LTS/TraceEq.lean | 1 - .../LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean | 3 --- .../LambdaCalculus/LocallyNameless/Untyped/CallByName.lean | 1 - .../LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean | 1 - .../LocallyNameless/Untyped/FullBetaEtaConfluence.lean | 2 -- .../LambdaCalculus/LocallyNameless/Untyped/FullEta.lean | 1 - .../LambdaCalculus/LocallyNameless/Untyped/MultiSubst.lean | 1 - .../LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean | 2 -- Cslib/Logics/LinearLogic/CLL/Basic.lean | 1 - Cslib/Logics/LinearLogic/CLL/MLL.lean | 1 - Cslib/Logics/Modal/Basic.lean | 3 --- Cslib/Logics/Propositional/Defs.lean | 1 - Cslib/Logics/Propositional/NaturalDeduction/Basic.lean | 3 --- Cslib/MachineLearning/PACLearning/Defs.lean | 2 -- Cslib/MachineLearning/PACLearning/VersionSpace.lean | 2 -- Cslib/Probability/PMF.lean | 1 - CslibTests/FreeMonad.lean | 1 - CslibTests/LTS.lean | 1 - 30 files changed, 41 deletions(-) diff --git a/Cslib/Computability/Languages/OmegaLanguage.lean b/Cslib/Computability/Languages/OmegaLanguage.lean index cd17e2101..1cb015843 100644 --- a/Cslib/Computability/Languages/OmegaLanguage.lean +++ b/Cslib/Computability/Languages/OmegaLanguage.lean @@ -8,8 +8,6 @@ module public import Cslib.Computability.Languages.Language public import Cslib.Foundations.Data.OmegaSequence.Flatten -public import Mathlib.Computability.Language -public import Mathlib.Order.CompleteBooleanAlgebra public import Mathlib.Order.Filter.AtTopBot.Defs /-! diff --git a/Cslib/Computability/Machines/Turing/SingleTape/NonDeterministic.lean b/Cslib/Computability/Machines/Turing/SingleTape/NonDeterministic.lean index ffd15a590..6584ab358 100644 --- a/Cslib/Computability/Machines/Turing/SingleTape/NonDeterministic.lean +++ b/Cslib/Computability/Machines/Turing/SingleTape/NonDeterministic.lean @@ -10,7 +10,6 @@ public import Cslib.Foundations.Relation.Defs public import Cslib.Foundations.Data.RelatesInSteps public import Cslib.Computability.Automata.NA.Basic public import Cslib.Computability.Automata.Transducers.Transducer -public import Cslib.Foundations.Data.BiTape public import Cslib.Computability.Machines.Turing.SingleTape.Defs /-! # Single-Tape Nondeterministic Turing Machines (NTMs) diff --git a/Cslib/Crypto/Protocols/PerfectSecrecy/Basic.lean b/Cslib/Crypto/Protocols/PerfectSecrecy/Basic.lean index c5f5a29ef..a68c42ee7 100644 --- a/Cslib/Crypto/Protocols/PerfectSecrecy/Basic.lean +++ b/Cslib/Crypto/Protocols/PerfectSecrecy/Basic.lean @@ -6,7 +6,6 @@ Authors: Samuel Schlesinger module -public import Cslib.Crypto.Protocols.PerfectSecrecy.Defs public import Cslib.Crypto.Protocols.PerfectSecrecy.Internal.PerfectSecrecy /-! diff --git a/Cslib/Crypto/Protocols/PerfectSecrecy/Defs.lean b/Cslib/Crypto/Protocols/PerfectSecrecy/Defs.lean index e7d824dd6..38c03b2ec 100644 --- a/Cslib/Crypto/Protocols/PerfectSecrecy/Defs.lean +++ b/Cslib/Crypto/Protocols/PerfectSecrecy/Defs.lean @@ -8,7 +8,6 @@ module public import Cslib.Crypto.Protocols.PerfectSecrecy.Encryption public import Cslib.Probability.PMF -public import Mathlib.Probability.ProbabilityMassFunction.Constructions /-! # Perfect Secrecy: Definitions diff --git a/Cslib/Crypto/Protocols/PerfectSecrecy/Internal/PerfectSecrecy.lean b/Cslib/Crypto/Protocols/PerfectSecrecy/Internal/PerfectSecrecy.lean index 66656e8ba..310dfc4d7 100644 --- a/Cslib/Crypto/Protocols/PerfectSecrecy/Internal/PerfectSecrecy.lean +++ b/Cslib/Crypto/Protocols/PerfectSecrecy/Internal/PerfectSecrecy.lean @@ -7,7 +7,6 @@ Authors: Samuel Schlesinger module public import Cslib.Crypto.Protocols.PerfectSecrecy.Defs -public import Mathlib.Probability.Distributions.Uniform /-! # Perfect Secrecy: Internal proofs diff --git a/Cslib/Crypto/Protocols/PerfectSecrecy/OneTimePad.lean b/Cslib/Crypto/Protocols/PerfectSecrecy/OneTimePad.lean index ed53950f6..320d67800 100644 --- a/Cslib/Crypto/Protocols/PerfectSecrecy/OneTimePad.lean +++ b/Cslib/Crypto/Protocols/PerfectSecrecy/OneTimePad.lean @@ -8,7 +8,6 @@ module public import Cslib.Crypto.Protocols.PerfectSecrecy.Basic public import Cslib.Crypto.Protocols.PerfectSecrecy.Internal.OneTimePad -public import Mathlib.Probability.Distributions.Uniform /-! # One-Time Pad diff --git a/Cslib/Crypto/Protocols/SecretSharing/Scheme.lean b/Cslib/Crypto/Protocols/SecretSharing/Scheme.lean index 09e07ae2a..d1bdde4ea 100644 --- a/Cslib/Crypto/Protocols/SecretSharing/Scheme.lean +++ b/Cslib/Crypto/Protocols/SecretSharing/Scheme.lean @@ -7,7 +7,6 @@ Authors: Samuel Schlesinger module public import Cslib.Init -public import Mathlib.Data.Finset.Basic public import Mathlib.Probability.ProbabilityMassFunction.Constructions /-! diff --git a/Cslib/Foundations/Data/HasFresh.lean b/Cslib/Foundations/Data/HasFresh.lean index df3d980e0..8adfcbcb2 100644 --- a/Cslib/Foundations/Data/HasFresh.lean +++ b/Cslib/Foundations/Data/HasFresh.lean @@ -9,7 +9,6 @@ module -- shake: keep-downstream public import Cslib.Init public import Mathlib.Analysis.Normed.Field.Lemmas meta import Lean.Elab.ConfigEval -import Qq /-! Computable chacterization of infinite types. -/ diff --git a/Cslib/Foundations/Logic/LogicalEquivalence.lean b/Cslib/Foundations/Logic/LogicalEquivalence.lean index 7f6c0d332..ddfacf47f 100644 --- a/Cslib/Foundations/Logic/LogicalEquivalence.lean +++ b/Cslib/Foundations/Logic/LogicalEquivalence.lean @@ -6,7 +6,6 @@ Authors: Fabrizio Montesi module -public import Cslib.Foundations.Syntax.Context public import Cslib.Foundations.Syntax.Congruence /-! Typeclass and notation for logical equivalence. -/ diff --git a/Cslib/Foundations/Relation/Attr.lean b/Cslib/Foundations/Relation/Attr.lean index 0b2d03778..557084824 100644 --- a/Cslib/Foundations/Relation/Attr.lean +++ b/Cslib/Foundations/Relation/Attr.lean @@ -7,7 +7,6 @@ Authors: Fabrizio Montesi, Thomas Waring, Chris Henson module public import Cslib.Init -public import Lean.Elab.Command public import Mathlib.Util.Notation3 public import Mathlib.Logic.Relation diff --git a/Cslib/Foundations/Relation/Restriction.lean b/Cslib/Foundations/Relation/Restriction.lean index 9de7da6d5..885005ff1 100644 --- a/Cslib/Foundations/Relation/Restriction.lean +++ b/Cslib/Foundations/Relation/Restriction.lean @@ -6,7 +6,6 @@ Authors: Chris Henson module -public import Cslib.Foundations.Relation.Defs public import Cslib.Foundations.Relation.Domain /-! # Relations: Properties on set restrictions diff --git a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean index d49a11a04..24177ca1f 100644 --- a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean +++ b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean @@ -7,7 +7,6 @@ Authors: Fabrizio Montesi, Thomas Waring module public import Cslib.Foundations.Relation.Domain -public import Cslib.Foundations.Semantics.LTS.Simulation public import Cslib.Foundations.Semantics.LTS.TraceEq public import Mathlib.Tactic.TFAE diff --git a/Cslib/Foundations/Semantics/LTS/TraceEq.lean b/Cslib/Foundations/Semantics/LTS/TraceEq.lean index 45782b67a..6568c61aa 100644 --- a/Cslib/Foundations/Semantics/LTS/TraceEq.lean +++ b/Cslib/Foundations/Semantics/LTS/TraceEq.lean @@ -6,7 +6,6 @@ Authors: Fabrizio Montesi module -public import Cslib.Foundations.Semantics.LTS.Basic public import Cslib.Foundations.Semantics.LTS.Simulation /-! diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean index cb858529d..b3ede7379 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean @@ -7,10 +7,7 @@ Authors: David Wegmann module public import Cslib.Foundations.Data.HasFresh -public import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Basic -public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StrongNorm -public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LcAt public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiSubst /-! Strong normalization (termination) for full beta-reduction of simply typed lambda calculus. -/ diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/CallByName.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/CallByName.lean index a2be62e5a..1cff47bad 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/CallByName.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/CallByName.lean @@ -7,7 +7,6 @@ Authors: Maximiliano Onofre Martínez module public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta -public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties /-! # Call-by-Name Evaluation -/ diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean index bb064d21d..65595658c 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean @@ -7,7 +7,6 @@ Authors: Chris Henson module public import Cslib.Foundations.Relation.Attr -public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Congruence /-! # β-reduction for the λ-calculus diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaEtaConfluence.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaEtaConfluence.lean index 2412f2c10..c0b0cf3b8 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaEtaConfluence.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaEtaConfluence.lean @@ -6,8 +6,6 @@ Authors: Maximiliano Onofre Martínez module -public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaConfluence -public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullEtaConfluence public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaEta /-! # βη-Confluence for the λ-calculus diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean index 2231d2b08..b9edc0551 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean @@ -7,7 +7,6 @@ Authors: Maximiliano Onofre Martínez module public import Cslib.Foundations.Relation.Attr -public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Congruence /-! # η-reduction for the λ-calculus -/ diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiSubst.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiSubst.lean index 91deb0e11..6954cd664 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiSubst.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiSubst.lean @@ -8,7 +8,6 @@ Authors: David Wegmann module public import Cslib.Foundations.Data.HasFresh -public import Cslib.Foundations.Syntax.HasSubstitution public import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Basic public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean index ea45ee0e8..b808dcc23 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean @@ -6,9 +6,7 @@ Authors: David Wegmann module -public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiApp -public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LcAt public import Cslib.Foundations.Relation.Confluence /-! Strong normalization (termination) for full beta-reduction of untyped lambda calculus. -/ diff --git a/Cslib/Logics/LinearLogic/CLL/Basic.lean b/Cslib/Logics/LinearLogic/CLL/Basic.lean index c331ae2ae..a6b5f3d43 100644 --- a/Cslib/Logics/LinearLogic/CLL/Basic.lean +++ b/Cslib/Logics/LinearLogic/CLL/Basic.lean @@ -7,7 +7,6 @@ Authors: Fabrizio Montesi module public import Cslib.Init -public import Cslib.Foundations.Syntax.Context public import Cslib.Foundations.Logic.InferenceSystem public import Cslib.Foundations.Logic.LogicalEquivalence public import Mathlib.Data.Multiset.Fold diff --git a/Cslib/Logics/LinearLogic/CLL/MLL.lean b/Cslib/Logics/LinearLogic/CLL/MLL.lean index 0e3c39354..4f56285af 100644 --- a/Cslib/Logics/LinearLogic/CLL/MLL.lean +++ b/Cslib/Logics/LinearLogic/CLL/MLL.lean @@ -7,7 +7,6 @@ Authors: Fabrizio Montesi module public import Cslib.Logics.LinearLogic.CLL.Basic -public import Cslib.Foundations.Logic.InferenceSystem /-! # Multiplicative Classical Linear Logic (MLL) diff --git a/Cslib/Logics/Modal/Basic.lean b/Cslib/Logics/Modal/Basic.lean index fda217a1c..2a42e1ebd 100644 --- a/Cslib/Logics/Modal/Basic.lean +++ b/Cslib/Logics/Modal/Basic.lean @@ -8,10 +8,7 @@ module public import Cslib.Init public import Cslib.Foundations.Logic.InferenceSystem -public import Mathlib.Data.Set.Basic -public import Mathlib.Order.Defs.Unbundled public import Cslib.Foundations.Relation.Euclidean -public import Mathlib.Logic.Nonempty /-! # Modal Logic diff --git a/Cslib/Logics/Propositional/Defs.lean b/Cslib/Logics/Propositional/Defs.lean index e9c603d91..93868f98f 100644 --- a/Cslib/Logics/Propositional/Defs.lean +++ b/Cslib/Logics/Propositional/Defs.lean @@ -7,7 +7,6 @@ Authors: Thomas Waring module public import Cslib.Foundations.Logic.InferenceSystem -public import Mathlib.Data.FunLike.Basic public import Mathlib.Data.Set.Image public import Mathlib.Order.TypeTags diff --git a/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean b/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean index 560ecb69e..1fe01ead3 100644 --- a/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean +++ b/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean @@ -6,9 +6,6 @@ Authors: Thomas Waring module public import Cslib.Logics.Propositional.Defs -public import Cslib.Foundations.Logic.InferenceSystem -public import Mathlib.Data.Finset.Insert -public import Mathlib.Data.Finset.SDiff public import Mathlib.Data.Finset.Image /-! # Natural deduction for propositional logic diff --git a/Cslib/MachineLearning/PACLearning/Defs.lean b/Cslib/MachineLearning/PACLearning/Defs.lean index 084079f4b..6136db5b2 100644 --- a/Cslib/MachineLearning/PACLearning/Defs.lean +++ b/Cslib/MachineLearning/PACLearning/Defs.lean @@ -7,9 +7,7 @@ Authors: Samuel Schlesinger module public import Cslib.Init -public import Mathlib.MeasureTheory.Measure.MeasureSpace public import Mathlib.MeasureTheory.Constructions.Pi -public import Mathlib.Order.SymmDiff /-! # PAC Learning diff --git a/Cslib/MachineLearning/PACLearning/VersionSpace.lean b/Cslib/MachineLearning/PACLearning/VersionSpace.lean index 37f8072cf..209818a78 100644 --- a/Cslib/MachineLearning/PACLearning/VersionSpace.lean +++ b/Cslib/MachineLearning/PACLearning/VersionSpace.lean @@ -7,8 +7,6 @@ Authors: Dhruv Gupta module public import Cslib.MachineLearning.PACLearning.Defs -public import Mathlib.MeasureTheory.Measure.Dirac -public import Mathlib.MeasureTheory.Measure.Map /-! # Version Space diff --git a/Cslib/Probability/PMF.lean b/Cslib/Probability/PMF.lean index 8393eb229..4afefba49 100644 --- a/Cslib/Probability/PMF.lean +++ b/Cslib/Probability/PMF.lean @@ -7,7 +7,6 @@ Authors: Samuel Schlesinger module public import Cslib.Init -public import Mathlib.Probability.ProbabilityMassFunction.Monad public import Mathlib.Probability.Distributions.Uniform /-! diff --git a/CslibTests/FreeMonad.lean b/CslibTests/FreeMonad.lean index 6e6ce0359..64b4ed0ce 100644 --- a/CslibTests/FreeMonad.lean +++ b/CslibTests/FreeMonad.lean @@ -3,7 +3,6 @@ Copyright (c) 2025 Tanner Duve. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Tanner Duve -/ -import Cslib.Foundations.Control.Monad.Free import Mathlib.Tactic.Cases import Cslib.Foundations.Control.Monad.Free.Fold import Cslib.Languages.LambdaCalculus.LocallyNameless.Context diff --git a/CslibTests/LTS.lean b/CslibTests/LTS.lean index 34f3c3db9..730703a6b 100644 --- a/CslibTests/LTS.lean +++ b/CslibTests/LTS.lean @@ -6,7 +6,6 @@ Authors: Fabrizio Montesi import Cslib.Foundations.Semantics.LTS.Divergence import Cslib.Foundations.Semantics.LTS.Bisimulation -import Mathlib.Algebra.Group.Even import Mathlib.Algebra.Ring.Parity import Cslib.Foundations.Semantics.LTS.Notation From eab0bc8f94448f6ee6048097ed6278b9db71390b Mon Sep 17 00:00:00 2001 From: Batixx Date: Fri, 17 Jul 2026 17:38:34 +0200 Subject: [PATCH 2/7] sort --- Cslib/Algorithms/Lean/MergeSort/MergeSort.lean | 2 +- Cslib/Algorithms/Lean/TimeM.lean | 1 - Cslib/Computability/Automata/Acceptors/Acceptor.lean | 1 - Cslib/Computability/Automata/Transducers/Transducer.lean | 1 - .../Computability/Languages/Congruences/RightCongruence.lean | 1 - Cslib/Computability/Languages/Language.lean | 1 - Cslib/Computability/Languages/OmegaLanguage.lean | 1 + Cslib/Computability/Languages/OmegaRegularLanguage.lean | 2 +- .../Machines/Turing/SingleTape/NonDeterministic.lean | 3 +-- Cslib/Computability/URM/Defs.lean | 1 - Cslib/Crypto/Protocols/PerfectSecrecy/Encryption.lean | 1 - .../Crypto/Protocols/PerfectSecrecy/Internal/OneTimePad.lean | 1 - Cslib/Crypto/Protocols/SecretSharing/Defs.lean | 2 +- Cslib/Crypto/Protocols/SecretSharing/Scheme.lean | 1 - Cslib/Crypto/Protocols/SecretSharing/Shamir.lean | 3 ++- Cslib/Crypto/Protocols/SecretSharing/Shamir/Polynomial.lean | 1 - Cslib/Foundations/Combinatorics/InfiniteGraphRamsey.lean | 2 -- Cslib/Foundations/Data/BiTape.lean | 3 --- Cslib/Foundations/Data/FinFun/Basic.lean | 1 - Cslib/Foundations/Data/FinFun/Update.lean | 2 +- Cslib/Foundations/Data/HasFresh.lean | 1 + Cslib/Foundations/Data/Nat/Segment.lean | 2 -- Cslib/Foundations/Data/OmegaSequence/Defs.lean | 1 - Cslib/Foundations/Data/OmegaSequence/Init.lean | 1 - Cslib/Foundations/Data/PFunctor/Free.lean | 1 - Cslib/Foundations/Data/Set/Saturation.lean | 3 +-- Cslib/Foundations/Relation/Attr.lean | 3 +-- Cslib/Foundations/Relation/Defs.lean | 2 -- Cslib/Foundations/Semantics/LTS/Basic.lean | 1 - Cslib/Foundations/Semantics/LTS/LTSCat/Basic.lean | 3 +-- Cslib/Foundations/Syntax/HasAlphaEquiv.lean | 1 - Cslib/Foundations/Syntax/HasSubstitution.lean | 1 - Cslib/Foundations/Syntax/HasWellFormed.lean | 1 - Cslib/Languages/CCS/Basic.lean | 2 -- Cslib/Languages/CCS/Semantics.lean | 2 +- Cslib/Languages/CombinatoryLogic/Basic.lean | 1 + Cslib/Languages/CombinatoryLogic/Confluence.lean | 2 +- Cslib/Languages/CombinatoryLogic/Defs.lean | 2 +- .../Languages/LambdaCalculus/LocallyNameless/Stlc/Safety.lean | 2 +- .../LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean | 3 +-- .../LocallyNameless/Untyped/FullBetaConfluence.lean | 2 +- .../LocallyNameless/Untyped/FullEtaConfluence.lean | 2 +- .../LambdaCalculus/LocallyNameless/Untyped/MultiSubst.lean | 2 -- .../LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean | 2 +- Cslib/Logics/HML/LogicalEquivalence.lean | 2 +- Cslib/Logics/LinearLogic/CLL/Basic.lean | 1 - Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean | 4 ++-- Cslib/Logics/Modal/Basic.lean | 1 - Cslib/Logics/Modal/LogicalEquivalence.lean | 2 +- Cslib/Logics/Propositional/Defs.lean | 1 - Cslib/MachineLearning/PACLearning/Defs.lean | 1 - Cslib/Probability/PMF.lean | 1 - CslibTests/FreeMonad.lean | 1 - CslibTests/HML.lean | 2 +- CslibTests/ImportWithMathlib.lean | 2 +- CslibTests/LTS.lean | 3 +-- CslibTests/Reduction.lean | 1 + scripts/CheckInitImports.lean | 4 +--- 58 files changed, 30 insertions(+), 70 deletions(-) diff --git a/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean b/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean index bb9f9c8f1..15c5d70c5 100644 --- a/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean +++ b/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean @@ -8,8 +8,8 @@ module public import Cslib.Algorithms.Lean.TimeM public import Mathlib.Data.Nat.Cast.Order.Ring -public import Mathlib.Order.Lattice.Nat public import Mathlib.Data.Nat.Log +public import Mathlib.Order.Lattice.Nat /-! # MergeSort on a list diff --git a/Cslib/Algorithms/Lean/TimeM.lean b/Cslib/Algorithms/Lean/TimeM.lean index 389d6945b..7dda028e5 100644 --- a/Cslib/Algorithms/Lean/TimeM.lean +++ b/Cslib/Algorithms/Lean/TimeM.lean @@ -6,7 +6,6 @@ Authors: Sorrachai Yingchareonthawornhcai, Eric Wieser module -public import Cslib.Init public import Mathlib.Algebra.Group.Defs /-! diff --git a/Cslib/Computability/Automata/Acceptors/Acceptor.lean b/Cslib/Computability/Automata/Acceptors/Acceptor.lean index b9413b430..98579ceb2 100644 --- a/Cslib/Computability/Automata/Acceptors/Acceptor.lean +++ b/Cslib/Computability/Automata/Acceptors/Acceptor.lean @@ -6,7 +6,6 @@ Authors: Fabrizio Montesi module -public import Cslib.Init public import Mathlib.Computability.Language /-! -/ diff --git a/Cslib/Computability/Automata/Transducers/Transducer.lean b/Cslib/Computability/Automata/Transducers/Transducer.lean index e17942b64..57e281a59 100644 --- a/Cslib/Computability/Automata/Transducers/Transducer.lean +++ b/Cslib/Computability/Automata/Transducers/Transducer.lean @@ -6,7 +6,6 @@ Authors: Fabrizio Montesi module -public import Cslib.Init /-! # Transducers -/ diff --git a/Cslib/Computability/Languages/Congruences/RightCongruence.lean b/Cslib/Computability/Languages/Congruences/RightCongruence.lean index b1da41a95..d1d6fad4f 100644 --- a/Cslib/Computability/Languages/Congruences/RightCongruence.lean +++ b/Cslib/Computability/Languages/Congruences/RightCongruence.lean @@ -6,7 +6,6 @@ Authors: Ching-Tsun Chou module -public import Cslib.Init public import Mathlib.Computability.Language /-! diff --git a/Cslib/Computability/Languages/Language.lean b/Cslib/Computability/Languages/Language.lean index 2ff6f64ee..55be8e758 100644 --- a/Cslib/Computability/Languages/Language.lean +++ b/Cslib/Computability/Languages/Language.lean @@ -6,7 +6,6 @@ Authors: Ching-Tsun Chou module -public import Cslib.Init public import Mathlib.Computability.Language /-! diff --git a/Cslib/Computability/Languages/OmegaLanguage.lean b/Cslib/Computability/Languages/OmegaLanguage.lean index 1cb015843..a48fac2a4 100644 --- a/Cslib/Computability/Languages/OmegaLanguage.lean +++ b/Cslib/Computability/Languages/OmegaLanguage.lean @@ -8,6 +8,7 @@ module public import Cslib.Computability.Languages.Language public import Cslib.Foundations.Data.OmegaSequence.Flatten +public import Mathlib.Algebra.Order.Sub.Basic public import Mathlib.Order.Filter.AtTopBot.Defs /-! diff --git a/Cslib/Computability/Languages/OmegaRegularLanguage.lean b/Cslib/Computability/Languages/OmegaRegularLanguage.lean index 75e89deff..6153d6e16 100644 --- a/Cslib/Computability/Languages/OmegaRegularLanguage.lean +++ b/Cslib/Computability/Languages/OmegaRegularLanguage.lean @@ -12,9 +12,9 @@ public import Cslib.Computability.Automata.NA.BuchiInter public import Cslib.Computability.Automata.NA.Sum public import Cslib.Computability.Languages.Congruences.BuchiCongruence public import Cslib.Computability.Languages.ExampleEventuallyZero -public import Mathlib.SetTheory.Cardinal.NatCard public import Mathlib.Data.Finite.Sigma public import Mathlib.Logic.Equiv.Fin.Basic +public import Mathlib.SetTheory.Cardinal.NatCard /-! # ω-Regular languages diff --git a/Cslib/Computability/Machines/Turing/SingleTape/NonDeterministic.lean b/Cslib/Computability/Machines/Turing/SingleTape/NonDeterministic.lean index 6584ab358..30ec6463e 100644 --- a/Cslib/Computability/Machines/Turing/SingleTape/NonDeterministic.lean +++ b/Cslib/Computability/Machines/Turing/SingleTape/NonDeterministic.lean @@ -6,11 +6,10 @@ Authors: Fabrizio Montesi module -public import Cslib.Foundations.Relation.Defs -public import Cslib.Foundations.Data.RelatesInSteps public import Cslib.Computability.Automata.NA.Basic public import Cslib.Computability.Automata.Transducers.Transducer public import Cslib.Computability.Machines.Turing.SingleTape.Defs +public import Cslib.Foundations.Data.RelatesInSteps /-! # Single-Tape Nondeterministic Turing Machines (NTMs) diff --git a/Cslib/Computability/URM/Defs.lean b/Cslib/Computability/URM/Defs.lean index c5d91a615..804b31172 100644 --- a/Cslib/Computability/URM/Defs.lean +++ b/Cslib/Computability/URM/Defs.lean @@ -5,7 +5,6 @@ Authors: Jesse Alama -/ module -public import Cslib.Init public import Mathlib.Data.Finset.Insert /-! # URM Core Definitions diff --git a/Cslib/Crypto/Protocols/PerfectSecrecy/Encryption.lean b/Cslib/Crypto/Protocols/PerfectSecrecy/Encryption.lean index a6896bcdf..5a2732432 100644 --- a/Cslib/Crypto/Protocols/PerfectSecrecy/Encryption.lean +++ b/Cslib/Crypto/Protocols/PerfectSecrecy/Encryption.lean @@ -6,7 +6,6 @@ Authors: Samuel Schlesinger module -public import Cslib.Init public import Mathlib.Probability.ProbabilityMassFunction.Monad /-! diff --git a/Cslib/Crypto/Protocols/PerfectSecrecy/Internal/OneTimePad.lean b/Cslib/Crypto/Protocols/PerfectSecrecy/Internal/OneTimePad.lean index 451e3253a..585831f1b 100644 --- a/Cslib/Crypto/Protocols/PerfectSecrecy/Internal/OneTimePad.lean +++ b/Cslib/Crypto/Protocols/PerfectSecrecy/Internal/OneTimePad.lean @@ -6,7 +6,6 @@ Authors: Samuel Schlesinger module -public import Cslib.Init public import Mathlib.Probability.Distributions.Uniform /-! diff --git a/Cslib/Crypto/Protocols/SecretSharing/Defs.lean b/Cslib/Crypto/Protocols/SecretSharing/Defs.lean index e8788f08d..d9d278b8f 100644 --- a/Cslib/Crypto/Protocols/SecretSharing/Defs.lean +++ b/Cslib/Crypto/Protocols/SecretSharing/Defs.lean @@ -6,8 +6,8 @@ Authors: Samuel Schlesinger module -public import Cslib.Probability.PMF public import Cslib.Crypto.Protocols.SecretSharing.Scheme +public import Cslib.Probability.PMF /-! # Secret Sharing: Definitions diff --git a/Cslib/Crypto/Protocols/SecretSharing/Scheme.lean b/Cslib/Crypto/Protocols/SecretSharing/Scheme.lean index d1bdde4ea..62bd3668b 100644 --- a/Cslib/Crypto/Protocols/SecretSharing/Scheme.lean +++ b/Cslib/Crypto/Protocols/SecretSharing/Scheme.lean @@ -6,7 +6,6 @@ Authors: Samuel Schlesinger module -public import Cslib.Init public import Mathlib.Probability.ProbabilityMassFunction.Constructions /-! diff --git a/Cslib/Crypto/Protocols/SecretSharing/Shamir.lean b/Cslib/Crypto/Protocols/SecretSharing/Shamir.lean index bd0de00d3..b5845038b 100644 --- a/Cslib/Crypto/Protocols/SecretSharing/Shamir.lean +++ b/Cslib/Crypto/Protocols/SecretSharing/Shamir.lean @@ -7,8 +7,9 @@ Authors: Samuel Schlesinger module public import Cslib.Crypto.Protocols.SecretSharing.Scheme -public import Mathlib.Probability.Distributions.Uniform public import Cslib.Crypto.Protocols.SecretSharing.Shamir.Polynomial +public import Mathlib.Probability.Distributions.Uniform + import Cslib.Probability.PMF /-! diff --git a/Cslib/Crypto/Protocols/SecretSharing/Shamir/Polynomial.lean b/Cslib/Crypto/Protocols/SecretSharing/Shamir/Polynomial.lean index 4cb4ced4f..47d521961 100644 --- a/Cslib/Crypto/Protocols/SecretSharing/Shamir/Polynomial.lean +++ b/Cslib/Crypto/Protocols/SecretSharing/Shamir/Polynomial.lean @@ -6,7 +6,6 @@ Authors: Samuel Schlesinger module -public import Cslib.Init public import Mathlib.LinearAlgebra.Lagrange /-! diff --git a/Cslib/Foundations/Combinatorics/InfiniteGraphRamsey.lean b/Cslib/Foundations/Combinatorics/InfiniteGraphRamsey.lean index 17f1bb30f..78ebcc634 100644 --- a/Cslib/Foundations/Combinatorics/InfiniteGraphRamsey.lean +++ b/Cslib/Foundations/Combinatorics/InfiniteGraphRamsey.lean @@ -6,8 +6,6 @@ Authors: Ching-Tsun Chou module -public import Cslib.Init -public import Mathlib.Algebra.Order.Group.Nat public import Mathlib.Data.Fintype.Pigeonhole public import Mathlib.Data.Set.Finite.Basic public import Mathlib.Data.Set.Lattice diff --git a/Cslib/Foundations/Data/BiTape.lean b/Cslib/Foundations/Data/BiTape.lean index 8c57a4c11..879e07c9d 100644 --- a/Cslib/Foundations/Data/BiTape.lean +++ b/Cslib/Foundations/Data/BiTape.lean @@ -8,9 +8,6 @@ module public import Cslib.Foundations.Data.StackTape public import Mathlib.Computability.TuringMachine.Tape -public import Mathlib.Data.Finset.Attr -public import Mathlib.Tactic.SetLike -public import Mathlib.Algebra.Order.Group.Nat /-! # BiTape: Bidirectionally infinite TM tape representation using StackTape diff --git a/Cslib/Foundations/Data/FinFun/Basic.lean b/Cslib/Foundations/Data/FinFun/Basic.lean index 652b3d123..f6c0b3231 100644 --- a/Cslib/Foundations/Data/FinFun/Basic.lean +++ b/Cslib/Foundations/Data/FinFun/Basic.lean @@ -6,7 +6,6 @@ Authors: Fabrizio Montesi, Xueying Qin module -public import Cslib.Init public import Mathlib.Data.Finset.Filter public import Mathlib.Data.Finset.Lattice.Basic diff --git a/Cslib/Foundations/Data/FinFun/Update.lean b/Cslib/Foundations/Data/FinFun/Update.lean index d02941e77..220026b30 100644 --- a/Cslib/Foundations/Data/FinFun/Update.lean +++ b/Cslib/Foundations/Data/FinFun/Update.lean @@ -6,8 +6,8 @@ Authors: Fabrizio Montesi module -public import Cslib.Foundations.Data.FinFun.Basic public import Cslib.Foundations.Data.DecidableEqZero +public import Cslib.Foundations.Data.FinFun.Basic public import Mathlib.Data.Finset.SDiff /-! # Update for finite functions diff --git a/Cslib/Foundations/Data/HasFresh.lean b/Cslib/Foundations/Data/HasFresh.lean index 8adfcbcb2..49b7a4867 100644 --- a/Cslib/Foundations/Data/HasFresh.lean +++ b/Cslib/Foundations/Data/HasFresh.lean @@ -8,6 +8,7 @@ module -- shake: keep-downstream public import Cslib.Init public import Mathlib.Analysis.Normed.Field.Lemmas + meta import Lean.Elab.ConfigEval /-! Computable chacterization of infinite types. -/ diff --git a/Cslib/Foundations/Data/Nat/Segment.lean b/Cslib/Foundations/Data/Nat/Segment.lean index 01ec8fae8..9c2d4bde4 100644 --- a/Cslib/Foundations/Data/Nat/Segment.lean +++ b/Cslib/Foundations/Data/Nat/Segment.lean @@ -6,8 +6,6 @@ Authors: Ching-Tsun Chou module -public import Cslib.Init -public import Mathlib.Algebra.Order.Sub.Basic public import Mathlib.Data.Nat.Nth /-! diff --git a/Cslib/Foundations/Data/OmegaSequence/Defs.lean b/Cslib/Foundations/Data/OmegaSequence/Defs.lean index 6c5842a1c..aaf43765e 100644 --- a/Cslib/Foundations/Data/OmegaSequence/Defs.lean +++ b/Cslib/Foundations/Data/OmegaSequence/Defs.lean @@ -6,7 +6,6 @@ Authors: Ching-Tsun Chou, Fabrizio Montesi module -public import Cslib.Init public import Mathlib.Data.FunLike.Basic public import Mathlib.Logic.Function.Iterate diff --git a/Cslib/Foundations/Data/OmegaSequence/Init.lean b/Cslib/Foundations/Data/OmegaSequence/Init.lean index 0013a221a..b91de65f4 100644 --- a/Cslib/Foundations/Data/OmegaSequence/Init.lean +++ b/Cslib/Foundations/Data/OmegaSequence/Init.lean @@ -8,7 +8,6 @@ module public import Cslib.Foundations.Data.OmegaSequence.Defs public import Mathlib.Algebra.Order.Group.Nat -public import Mathlib.Algebra.Order.Sub.Basic public import Mathlib.Order.Lattice.Nat /-! diff --git a/Cslib/Foundations/Data/PFunctor/Free.lean b/Cslib/Foundations/Data/PFunctor/Free.lean index a29e97470..21bdd79cd 100644 --- a/Cslib/Foundations/Data/PFunctor/Free.lean +++ b/Cslib/Foundations/Data/PFunctor/Free.lean @@ -6,7 +6,6 @@ Authors: Quang Dao module -public import Cslib.Init public import Mathlib.Data.PFunctor.Univariate.Basic /-! diff --git a/Cslib/Foundations/Data/Set/Saturation.lean b/Cslib/Foundations/Data/Set/Saturation.lean index 32e9806db..689db482f 100644 --- a/Cslib/Foundations/Data/Set/Saturation.lean +++ b/Cslib/Foundations/Data/Set/Saturation.lean @@ -6,9 +6,8 @@ Authors: Ching-Tsun Chou module -public import Cslib.Init -public import Mathlib.Order.SetNotation public import Mathlib.Data.Set.Basic +public import Mathlib.Order.SetNotation /-! # Saturation diff --git a/Cslib/Foundations/Relation/Attr.lean b/Cslib/Foundations/Relation/Attr.lean index 557084824..a5bcbe34d 100644 --- a/Cslib/Foundations/Relation/Attr.lean +++ b/Cslib/Foundations/Relation/Attr.lean @@ -6,9 +6,8 @@ Authors: Fabrizio Montesi, Thomas Waring, Chris Henson module -public import Cslib.Init -public import Mathlib.Util.Notation3 public import Mathlib.Logic.Relation +public import Mathlib.Util.Notation3 /-! # Relations: Attributes diff --git a/Cslib/Foundations/Relation/Defs.lean b/Cslib/Foundations/Relation/Defs.lean index f649ed5dd..56c75c2d8 100644 --- a/Cslib/Foundations/Relation/Defs.lean +++ b/Cslib/Foundations/Relation/Defs.lean @@ -6,10 +6,8 @@ Authors: Fabrizio Montesi, Thomas Waring, Chris Henson module -public import Cslib.Init public import Mathlib.Data.Set.CoeSort public import Mathlib.Logic.Relation -public import Mathlib.Order.Basic /-! # Relations: Definitions diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean index b1f864f89..89b1ebee2 100644 --- a/Cslib/Foundations/Semantics/LTS/Basic.lean +++ b/Cslib/Foundations/Semantics/LTS/Basic.lean @@ -6,7 +6,6 @@ Authors: Fabrizio Montesi module -public import Cslib.Init public import Mathlib.Data.Set.Finite.Basic public import Mathlib.Order.SetNotation diff --git a/Cslib/Foundations/Semantics/LTS/LTSCat/Basic.lean b/Cslib/Foundations/Semantics/LTS/LTSCat/Basic.lean index d1e578db8..db6f92147 100644 --- a/Cslib/Foundations/Semantics/LTS/LTSCat/Basic.lean +++ b/Cslib/Foundations/Semantics/LTS/LTSCat/Basic.lean @@ -6,9 +6,8 @@ Authors: Ayberk Tosun module -public import Mathlib.CategoryTheory.Category.Basic public import Cslib.Foundations.Semantics.LTS.Basic -public import Mathlib.Control.Basic +public import Mathlib.CategoryTheory.Category.Basic /-! # Category of Labelled Transition Systems diff --git a/Cslib/Foundations/Syntax/HasAlphaEquiv.lean b/Cslib/Foundations/Syntax/HasAlphaEquiv.lean index c0faf8469..4e03a15bb 100644 --- a/Cslib/Foundations/Syntax/HasAlphaEquiv.lean +++ b/Cslib/Foundations/Syntax/HasAlphaEquiv.lean @@ -6,7 +6,6 @@ Authors: Fabrizio Montesi module -public import Cslib.Init /-! Notation typeclass for α-equivalence. -/ diff --git a/Cslib/Foundations/Syntax/HasSubstitution.lean b/Cslib/Foundations/Syntax/HasSubstitution.lean index b9b31470b..7e4a090af 100644 --- a/Cslib/Foundations/Syntax/HasSubstitution.lean +++ b/Cslib/Foundations/Syntax/HasSubstitution.lean @@ -6,7 +6,6 @@ Authors: Fabrizio Montesi module -public import Cslib.Init /-! Notation typeclass for substitution. -/ diff --git a/Cslib/Foundations/Syntax/HasWellFormed.lean b/Cslib/Foundations/Syntax/HasWellFormed.lean index 1dd2a6330..e440f04bd 100644 --- a/Cslib/Foundations/Syntax/HasWellFormed.lean +++ b/Cslib/Foundations/Syntax/HasWellFormed.lean @@ -6,7 +6,6 @@ Authors: Fabrizio Montesi module -public import Cslib.Init /-! Notation typeclass for well-formedness. -/ diff --git a/Cslib/Languages/CCS/Basic.lean b/Cslib/Languages/CCS/Basic.lean index c30c1849d..656b7dc9a 100644 --- a/Cslib/Languages/CCS/Basic.lean +++ b/Cslib/Languages/CCS/Basic.lean @@ -7,8 +7,6 @@ Authors: Fabrizio Montesi module public import Cslib.Foundations.Syntax.Context -public import Mathlib.Tactic.ToAdditive -public import Mathlib.Tactic.ToDual /-! # Calculus of Communicating Systems (CCS) diff --git a/Cslib/Languages/CCS/Semantics.lean b/Cslib/Languages/CCS/Semantics.lean index 7a5670fde..b4a113eae 100644 --- a/Cslib/Languages/CCS/Semantics.lean +++ b/Cslib/Languages/CCS/Semantics.lean @@ -6,8 +6,8 @@ Authors: Fabrizio Montesi module -public import Cslib.Foundations.Semantics.LTS.HasTau public meta import Cslib.Foundations.Semantics.LTS.Notation +public import Cslib.Foundations.Semantics.LTS.HasTau public import Cslib.Languages.CCS.Basic /-! # Semantics of CCS diff --git a/Cslib/Languages/CombinatoryLogic/Basic.lean b/Cslib/Languages/CombinatoryLogic/Basic.lean index 785d4223d..5c11d2925 100644 --- a/Cslib/Languages/CombinatoryLogic/Basic.lean +++ b/Cslib/Languages/CombinatoryLogic/Basic.lean @@ -7,6 +7,7 @@ Authors: Thomas Waring module public import Cslib.Languages.CombinatoryLogic.Defs +public import Mathlib.Tactic.SplitIfs /-! # Basic results for the SKI calculus diff --git a/Cslib/Languages/CombinatoryLogic/Confluence.lean b/Cslib/Languages/CombinatoryLogic/Confluence.lean index 9fc3c7d18..414a83e98 100644 --- a/Cslib/Languages/CombinatoryLogic/Confluence.lean +++ b/Cslib/Languages/CombinatoryLogic/Confluence.lean @@ -6,8 +6,8 @@ Authors: Thomas Waring module -public import Cslib.Languages.CombinatoryLogic.Defs public import Cslib.Foundations.Relation.Confluence +public import Cslib.Languages.CombinatoryLogic.Defs /-! # SKI reduction is confluent diff --git a/Cslib/Languages/CombinatoryLogic/Defs.lean b/Cslib/Languages/CombinatoryLogic/Defs.lean index 7d028d283..df76218fd 100644 --- a/Cslib/Languages/CombinatoryLogic/Defs.lean +++ b/Cslib/Languages/CombinatoryLogic/Defs.lean @@ -6,9 +6,9 @@ Authors: Thomas Waring module +public meta import Mathlib.Tactic.ToDual public import Cslib.Foundations.Relation.Attr public import Cslib.Foundations.Relation.Defs -public meta import Mathlib.Tactic.ToDual /-! # SKI Combinatory Logic diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/Safety.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/Safety.lean index 609e129a6..9878bb96e 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/Safety.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/Safety.lean @@ -6,9 +6,9 @@ Authors: Chris Henson module +public import Cslib.Foundations.Relation.Confluence public import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Basic public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta -public import Cslib.Foundations.Relation.Confluence /-! # λ-calculus diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean index b3ede7379..032703861 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/StrongNorm.lean @@ -6,9 +6,8 @@ Authors: David Wegmann module -public import Cslib.Foundations.Data.HasFresh -public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StrongNorm public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiSubst +public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StrongNorm /-! Strong normalization (termination) for full beta-reduction of simply typed lambda calculus. -/ diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaConfluence.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaConfluence.lean index 2f1f00360..d75752d6e 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaConfluence.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaConfluence.lean @@ -6,8 +6,8 @@ Authors: Chris Henson module -public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta public import Cslib.Foundations.Relation.Confluence +public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta /-! # β-confluence for the λ-calculus -/ diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEtaConfluence.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEtaConfluence.lean index 4defb563e..f97dad2d8 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEtaConfluence.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEtaConfluence.lean @@ -6,8 +6,8 @@ Authors: Maximiliano Onofre Martínez module -public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullEta public import Cslib.Foundations.Relation.Confluence +public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullEta /-! # η-confluence for the λ-calculus diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiSubst.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiSubst.lean index 6954cd664..995cb31a7 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiSubst.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/MultiSubst.lean @@ -7,9 +7,7 @@ Authors: David Wegmann module -public import Cslib.Foundations.Data.HasFresh public import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Basic -public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta /-! Multiple substitution for untyped lambda calculus. -/ diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean index b808dcc23..89f798460 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StrongNorm.lean @@ -6,8 +6,8 @@ Authors: David Wegmann module -public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiApp public import Cslib.Foundations.Relation.Confluence +public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiApp /-! Strong normalization (termination) for full beta-reduction of untyped lambda calculus. -/ diff --git a/Cslib/Logics/HML/LogicalEquivalence.lean b/Cslib/Logics/HML/LogicalEquivalence.lean index 5bad96e46..2391de9b1 100644 --- a/Cslib/Logics/HML/LogicalEquivalence.lean +++ b/Cslib/Logics/HML/LogicalEquivalence.lean @@ -6,8 +6,8 @@ Authors: Fabrizio Montesi module -public import Cslib.Logics.HML.Basic public import Cslib.Foundations.Logic.LogicalEquivalence +public import Cslib.Logics.HML.Basic /-! # Logical Equivalence in HML diff --git a/Cslib/Logics/LinearLogic/CLL/Basic.lean b/Cslib/Logics/LinearLogic/CLL/Basic.lean index a6b5f3d43..a208b5e3c 100644 --- a/Cslib/Logics/LinearLogic/CLL/Basic.lean +++ b/Cslib/Logics/LinearLogic/CLL/Basic.lean @@ -6,7 +6,6 @@ Authors: Fabrizio Montesi module -public import Cslib.Init public import Cslib.Foundations.Logic.InferenceSystem public import Cslib.Foundations.Logic.LogicalEquivalence public import Mathlib.Data.Multiset.Fold diff --git a/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean b/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean index fbb2fe840..9298488c0 100644 --- a/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean +++ b/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean @@ -6,10 +6,10 @@ Authors: Tanner Duve, Bhavik Mehta module -public import Mathlib.Algebra.Group.Pointwise.Set.Basic +public import Cslib.Logics.LinearLogic.CLL.Basic public import Mathlib.Algebra.Group.Idempotent +public import Mathlib.Algebra.Group.Pointwise.Set.Basic public import Mathlib.Order.Closure -public import Cslib.Logics.LinearLogic.CLL.Basic /-! # Phase semantics for Classical Linear Logic diff --git a/Cslib/Logics/Modal/Basic.lean b/Cslib/Logics/Modal/Basic.lean index 2a42e1ebd..51bfb4b3f 100644 --- a/Cslib/Logics/Modal/Basic.lean +++ b/Cslib/Logics/Modal/Basic.lean @@ -6,7 +6,6 @@ Authors: Fabrizio Montesi, Marianna Girlando module -public import Cslib.Init public import Cslib.Foundations.Logic.InferenceSystem public import Cslib.Foundations.Relation.Euclidean diff --git a/Cslib/Logics/Modal/LogicalEquivalence.lean b/Cslib/Logics/Modal/LogicalEquivalence.lean index 0fc089e4e..1c4c2368c 100644 --- a/Cslib/Logics/Modal/LogicalEquivalence.lean +++ b/Cslib/Logics/Modal/LogicalEquivalence.lean @@ -6,8 +6,8 @@ Authors: Fabrizio Montesi module -public import Cslib.Logics.Modal.Basic public import Cslib.Foundations.Logic.LogicalEquivalence +public import Cslib.Logics.Modal.Basic /-! # Logical Equivalence in Modal Logic diff --git a/Cslib/Logics/Propositional/Defs.lean b/Cslib/Logics/Propositional/Defs.lean index 93868f98f..45d25ea68 100644 --- a/Cslib/Logics/Propositional/Defs.lean +++ b/Cslib/Logics/Propositional/Defs.lean @@ -7,7 +7,6 @@ Authors: Thomas Waring module public import Cslib.Foundations.Logic.InferenceSystem -public import Mathlib.Data.Set.Image public import Mathlib.Order.TypeTags /-! # Propositions and theories diff --git a/Cslib/MachineLearning/PACLearning/Defs.lean b/Cslib/MachineLearning/PACLearning/Defs.lean index 6136db5b2..00c74f37c 100644 --- a/Cslib/MachineLearning/PACLearning/Defs.lean +++ b/Cslib/MachineLearning/PACLearning/Defs.lean @@ -6,7 +6,6 @@ Authors: Samuel Schlesinger module -public import Cslib.Init public import Mathlib.MeasureTheory.Constructions.Pi /-! # PAC Learning diff --git a/Cslib/Probability/PMF.lean b/Cslib/Probability/PMF.lean index 4afefba49..bb90539f5 100644 --- a/Cslib/Probability/PMF.lean +++ b/Cslib/Probability/PMF.lean @@ -6,7 +6,6 @@ Authors: Samuel Schlesinger module -public import Cslib.Init public import Mathlib.Probability.Distributions.Uniform /-! diff --git a/CslibTests/FreeMonad.lean b/CslibTests/FreeMonad.lean index 64b4ed0ce..a073470ca 100644 --- a/CslibTests/FreeMonad.lean +++ b/CslibTests/FreeMonad.lean @@ -3,7 +3,6 @@ Copyright (c) 2025 Tanner Duve. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Tanner Duve -/ -import Mathlib.Tactic.Cases import Cslib.Foundations.Control.Monad.Free.Fold import Cslib.Languages.LambdaCalculus.LocallyNameless.Context diff --git a/CslibTests/HML.lean b/CslibTests/HML.lean index 3e9346f2b..bdc13d02f 100644 --- a/CslibTests/HML.lean +++ b/CslibTests/HML.lean @@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi -/ -import Cslib.Logics.HML.Basic import Cslib.Languages.CCS.Semantics +import Cslib.Logics.HML.Basic namespace CslibTests diff --git a/CslibTests/ImportWithMathlib.lean b/CslibTests/ImportWithMathlib.lean index c68f3b0ba..2f31c4b8f 100644 --- a/CslibTests/ImportWithMathlib.lean +++ b/CslibTests/ImportWithMathlib.lean @@ -1,2 +1,2 @@ -import Mathlib import Cslib +import Mathlib diff --git a/CslibTests/LTS.lean b/CslibTests/LTS.lean index 730703a6b..ac9870e69 100644 --- a/CslibTests/LTS.lean +++ b/CslibTests/LTS.lean @@ -4,9 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi -/ -import Cslib.Foundations.Semantics.LTS.Divergence import Cslib.Foundations.Semantics.LTS.Bisimulation -import Mathlib.Algebra.Ring.Parity +import Cslib.Foundations.Semantics.LTS.Divergence import Cslib.Foundations.Semantics.LTS.Notation namespace CslibTests diff --git a/CslibTests/Reduction.lean b/CslibTests/Reduction.lean index fdd55a97a..41d3f5010 100644 --- a/CslibTests/Reduction.lean +++ b/CslibTests/Reduction.lean @@ -1,4 +1,5 @@ import Cslib.Foundations.Relation.Attr +import Cslib.Init namespace CslibTests diff --git a/scripts/CheckInitImports.lean b/scripts/CheckInitImports.lean index e3aca2ad4..13bea84b3 100644 --- a/scripts/CheckInitImports.lean +++ b/scripts/CheckInitImports.lean @@ -4,10 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Jesse Alama, Chris Henson -/ -import Lean -import Mathlib.Lean.CoreM import Batteries.Data.List.Basic -import ImportGraph +import Mathlib.Lean.CoreM open Lean Core Elab Command From 7688248763c4f916d043ff28158129f431e1033d Mon Sep 17 00:00:00 2001 From: Batixx Date: Fri, 17 Jul 2026 18:11:04 +0200 Subject: [PATCH 3/7] init --- Cslib/Algorithms/Lean/TimeM.lean | 1 + Cslib/Computability/Automata/Acceptors/Acceptor.lean | 1 + Cslib/Computability/Automata/Transducers/Transducer.lean | 1 + Cslib/Computability/Languages/Congruences/RightCongruence.lean | 1 + Cslib/Computability/Languages/Language.lean | 1 + Cslib/Computability/URM/Defs.lean | 1 + Cslib/Crypto/Protocols/PerfectSecrecy/Encryption.lean | 1 + Cslib/Crypto/Protocols/PerfectSecrecy/Internal/OneTimePad.lean | 1 + Cslib/Crypto/Protocols/SecretSharing/Scheme.lean | 1 + Cslib/Crypto/Protocols/SecretSharing/Shamir/Polynomial.lean | 1 + Cslib/Foundations/Combinatorics/InfiniteGraphRamsey.lean | 1 + Cslib/Foundations/Data/FinFun/Basic.lean | 1 + Cslib/Foundations/Data/Nat/Segment.lean | 1 + Cslib/Foundations/Data/OmegaSequence/Defs.lean | 1 + Cslib/Foundations/Data/PFunctor/Free.lean | 1 + Cslib/Foundations/Data/Set/Saturation.lean | 1 + Cslib/Foundations/Relation/Attr.lean | 1 + Cslib/Foundations/Relation/Defs.lean | 1 + Cslib/Foundations/Semantics/LTS/Basic.lean | 1 + Cslib/Foundations/Syntax/HasAlphaEquiv.lean | 1 + Cslib/Foundations/Syntax/HasSubstitution.lean | 1 + Cslib/Foundations/Syntax/HasWellFormed.lean | 1 + Cslib/MachineLearning/PACLearning/Defs.lean | 1 + Cslib/Probability/PMF.lean | 1 + 24 files changed, 24 insertions(+) diff --git a/Cslib/Algorithms/Lean/TimeM.lean b/Cslib/Algorithms/Lean/TimeM.lean index 7dda028e5..389d6945b 100644 --- a/Cslib/Algorithms/Lean/TimeM.lean +++ b/Cslib/Algorithms/Lean/TimeM.lean @@ -6,6 +6,7 @@ Authors: Sorrachai Yingchareonthawornhcai, Eric Wieser module +public import Cslib.Init public import Mathlib.Algebra.Group.Defs /-! diff --git a/Cslib/Computability/Automata/Acceptors/Acceptor.lean b/Cslib/Computability/Automata/Acceptors/Acceptor.lean index 98579ceb2..b9413b430 100644 --- a/Cslib/Computability/Automata/Acceptors/Acceptor.lean +++ b/Cslib/Computability/Automata/Acceptors/Acceptor.lean @@ -6,6 +6,7 @@ Authors: Fabrizio Montesi module +public import Cslib.Init public import Mathlib.Computability.Language /-! -/ diff --git a/Cslib/Computability/Automata/Transducers/Transducer.lean b/Cslib/Computability/Automata/Transducers/Transducer.lean index 57e281a59..4fec2a5e1 100644 --- a/Cslib/Computability/Automata/Transducers/Transducer.lean +++ b/Cslib/Computability/Automata/Transducers/Transducer.lean @@ -5,6 +5,7 @@ Authors: Fabrizio Montesi -/ module +public import Cslib.Init /-! # Transducers -/ diff --git a/Cslib/Computability/Languages/Congruences/RightCongruence.lean b/Cslib/Computability/Languages/Congruences/RightCongruence.lean index d1d6fad4f..b1da41a95 100644 --- a/Cslib/Computability/Languages/Congruences/RightCongruence.lean +++ b/Cslib/Computability/Languages/Congruences/RightCongruence.lean @@ -6,6 +6,7 @@ Authors: Ching-Tsun Chou module +public import Cslib.Init public import Mathlib.Computability.Language /-! diff --git a/Cslib/Computability/Languages/Language.lean b/Cslib/Computability/Languages/Language.lean index 55be8e758..2ff6f64ee 100644 --- a/Cslib/Computability/Languages/Language.lean +++ b/Cslib/Computability/Languages/Language.lean @@ -6,6 +6,7 @@ Authors: Ching-Tsun Chou module +public import Cslib.Init public import Mathlib.Computability.Language /-! diff --git a/Cslib/Computability/URM/Defs.lean b/Cslib/Computability/URM/Defs.lean index 804b31172..c5d91a615 100644 --- a/Cslib/Computability/URM/Defs.lean +++ b/Cslib/Computability/URM/Defs.lean @@ -5,6 +5,7 @@ Authors: Jesse Alama -/ module +public import Cslib.Init public import Mathlib.Data.Finset.Insert /-! # URM Core Definitions diff --git a/Cslib/Crypto/Protocols/PerfectSecrecy/Encryption.lean b/Cslib/Crypto/Protocols/PerfectSecrecy/Encryption.lean index 5a2732432..a6896bcdf 100644 --- a/Cslib/Crypto/Protocols/PerfectSecrecy/Encryption.lean +++ b/Cslib/Crypto/Protocols/PerfectSecrecy/Encryption.lean @@ -6,6 +6,7 @@ Authors: Samuel Schlesinger module +public import Cslib.Init public import Mathlib.Probability.ProbabilityMassFunction.Monad /-! diff --git a/Cslib/Crypto/Protocols/PerfectSecrecy/Internal/OneTimePad.lean b/Cslib/Crypto/Protocols/PerfectSecrecy/Internal/OneTimePad.lean index 585831f1b..451e3253a 100644 --- a/Cslib/Crypto/Protocols/PerfectSecrecy/Internal/OneTimePad.lean +++ b/Cslib/Crypto/Protocols/PerfectSecrecy/Internal/OneTimePad.lean @@ -6,6 +6,7 @@ Authors: Samuel Schlesinger module +public import Cslib.Init public import Mathlib.Probability.Distributions.Uniform /-! diff --git a/Cslib/Crypto/Protocols/SecretSharing/Scheme.lean b/Cslib/Crypto/Protocols/SecretSharing/Scheme.lean index 62bd3668b..d1bdde4ea 100644 --- a/Cslib/Crypto/Protocols/SecretSharing/Scheme.lean +++ b/Cslib/Crypto/Protocols/SecretSharing/Scheme.lean @@ -6,6 +6,7 @@ Authors: Samuel Schlesinger module +public import Cslib.Init public import Mathlib.Probability.ProbabilityMassFunction.Constructions /-! diff --git a/Cslib/Crypto/Protocols/SecretSharing/Shamir/Polynomial.lean b/Cslib/Crypto/Protocols/SecretSharing/Shamir/Polynomial.lean index 47d521961..4cb4ced4f 100644 --- a/Cslib/Crypto/Protocols/SecretSharing/Shamir/Polynomial.lean +++ b/Cslib/Crypto/Protocols/SecretSharing/Shamir/Polynomial.lean @@ -6,6 +6,7 @@ Authors: Samuel Schlesinger module +public import Cslib.Init public import Mathlib.LinearAlgebra.Lagrange /-! diff --git a/Cslib/Foundations/Combinatorics/InfiniteGraphRamsey.lean b/Cslib/Foundations/Combinatorics/InfiniteGraphRamsey.lean index 78ebcc634..6fa6501e7 100644 --- a/Cslib/Foundations/Combinatorics/InfiniteGraphRamsey.lean +++ b/Cslib/Foundations/Combinatorics/InfiniteGraphRamsey.lean @@ -6,6 +6,7 @@ Authors: Ching-Tsun Chou module +public import Cslib.Init public import Mathlib.Data.Fintype.Pigeonhole public import Mathlib.Data.Set.Finite.Basic public import Mathlib.Data.Set.Lattice diff --git a/Cslib/Foundations/Data/FinFun/Basic.lean b/Cslib/Foundations/Data/FinFun/Basic.lean index f6c0b3231..652b3d123 100644 --- a/Cslib/Foundations/Data/FinFun/Basic.lean +++ b/Cslib/Foundations/Data/FinFun/Basic.lean @@ -6,6 +6,7 @@ Authors: Fabrizio Montesi, Xueying Qin module +public import Cslib.Init public import Mathlib.Data.Finset.Filter public import Mathlib.Data.Finset.Lattice.Basic diff --git a/Cslib/Foundations/Data/Nat/Segment.lean b/Cslib/Foundations/Data/Nat/Segment.lean index 9c2d4bde4..236bb68ba 100644 --- a/Cslib/Foundations/Data/Nat/Segment.lean +++ b/Cslib/Foundations/Data/Nat/Segment.lean @@ -6,6 +6,7 @@ Authors: Ching-Tsun Chou module +public import Cslib.Init public import Mathlib.Data.Nat.Nth /-! diff --git a/Cslib/Foundations/Data/OmegaSequence/Defs.lean b/Cslib/Foundations/Data/OmegaSequence/Defs.lean index aaf43765e..6c5842a1c 100644 --- a/Cslib/Foundations/Data/OmegaSequence/Defs.lean +++ b/Cslib/Foundations/Data/OmegaSequence/Defs.lean @@ -6,6 +6,7 @@ Authors: Ching-Tsun Chou, Fabrizio Montesi module +public import Cslib.Init public import Mathlib.Data.FunLike.Basic public import Mathlib.Logic.Function.Iterate diff --git a/Cslib/Foundations/Data/PFunctor/Free.lean b/Cslib/Foundations/Data/PFunctor/Free.lean index 21bdd79cd..a29e97470 100644 --- a/Cslib/Foundations/Data/PFunctor/Free.lean +++ b/Cslib/Foundations/Data/PFunctor/Free.lean @@ -6,6 +6,7 @@ Authors: Quang Dao module +public import Cslib.Init public import Mathlib.Data.PFunctor.Univariate.Basic /-! diff --git a/Cslib/Foundations/Data/Set/Saturation.lean b/Cslib/Foundations/Data/Set/Saturation.lean index 689db482f..395d8c8e6 100644 --- a/Cslib/Foundations/Data/Set/Saturation.lean +++ b/Cslib/Foundations/Data/Set/Saturation.lean @@ -6,6 +6,7 @@ Authors: Ching-Tsun Chou module +public import Cslib.Init public import Mathlib.Data.Set.Basic public import Mathlib.Order.SetNotation diff --git a/Cslib/Foundations/Relation/Attr.lean b/Cslib/Foundations/Relation/Attr.lean index a5bcbe34d..49ad243d5 100644 --- a/Cslib/Foundations/Relation/Attr.lean +++ b/Cslib/Foundations/Relation/Attr.lean @@ -6,6 +6,7 @@ Authors: Fabrizio Montesi, Thomas Waring, Chris Henson module +public import Cslib.Init public import Mathlib.Logic.Relation public import Mathlib.Util.Notation3 diff --git a/Cslib/Foundations/Relation/Defs.lean b/Cslib/Foundations/Relation/Defs.lean index 56c75c2d8..fdb4a7b95 100644 --- a/Cslib/Foundations/Relation/Defs.lean +++ b/Cslib/Foundations/Relation/Defs.lean @@ -6,6 +6,7 @@ Authors: Fabrizio Montesi, Thomas Waring, Chris Henson module +public import Cslib.Init public import Mathlib.Data.Set.CoeSort public import Mathlib.Logic.Relation diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean index 89b1ebee2..b1f864f89 100644 --- a/Cslib/Foundations/Semantics/LTS/Basic.lean +++ b/Cslib/Foundations/Semantics/LTS/Basic.lean @@ -6,6 +6,7 @@ Authors: Fabrizio Montesi module +public import Cslib.Init public import Mathlib.Data.Set.Finite.Basic public import Mathlib.Order.SetNotation diff --git a/Cslib/Foundations/Syntax/HasAlphaEquiv.lean b/Cslib/Foundations/Syntax/HasAlphaEquiv.lean index 4e03a15bb..ae2624e3d 100644 --- a/Cslib/Foundations/Syntax/HasAlphaEquiv.lean +++ b/Cslib/Foundations/Syntax/HasAlphaEquiv.lean @@ -5,6 +5,7 @@ Authors: Fabrizio Montesi -/ module +public import Cslib.Init /-! Notation typeclass for α-equivalence. -/ diff --git a/Cslib/Foundations/Syntax/HasSubstitution.lean b/Cslib/Foundations/Syntax/HasSubstitution.lean index 7e4a090af..f9e2d5b2a 100644 --- a/Cslib/Foundations/Syntax/HasSubstitution.lean +++ b/Cslib/Foundations/Syntax/HasSubstitution.lean @@ -5,6 +5,7 @@ Authors: Fabrizio Montesi -/ module +public import Cslib.Init /-! Notation typeclass for substitution. -/ diff --git a/Cslib/Foundations/Syntax/HasWellFormed.lean b/Cslib/Foundations/Syntax/HasWellFormed.lean index e440f04bd..96f2e9000 100644 --- a/Cslib/Foundations/Syntax/HasWellFormed.lean +++ b/Cslib/Foundations/Syntax/HasWellFormed.lean @@ -5,6 +5,7 @@ Authors: Fabrizio Montesi -/ module +public import Cslib.Init /-! Notation typeclass for well-formedness. -/ diff --git a/Cslib/MachineLearning/PACLearning/Defs.lean b/Cslib/MachineLearning/PACLearning/Defs.lean index 00c74f37c..6136db5b2 100644 --- a/Cslib/MachineLearning/PACLearning/Defs.lean +++ b/Cslib/MachineLearning/PACLearning/Defs.lean @@ -6,6 +6,7 @@ Authors: Samuel Schlesinger module +public import Cslib.Init public import Mathlib.MeasureTheory.Constructions.Pi /-! # PAC Learning diff --git a/Cslib/Probability/PMF.lean b/Cslib/Probability/PMF.lean index bb90539f5..4afefba49 100644 --- a/Cslib/Probability/PMF.lean +++ b/Cslib/Probability/PMF.lean @@ -6,6 +6,7 @@ Authors: Samuel Schlesinger module +public import Cslib.Init public import Mathlib.Probability.Distributions.Uniform /-! From bc93c5e7128b7f46149b7060b49e241ad3d37413 Mon Sep 17 00:00:00 2001 From: Batixx Date: Fri, 17 Jul 2026 18:20:21 +0200 Subject: [PATCH 4/7] fix format --- Cslib/Computability/Automata/Transducers/Transducer.lean | 2 +- Cslib/Foundations/Syntax/HasAlphaEquiv.lean | 2 +- Cslib/Foundations/Syntax/HasSubstitution.lean | 2 +- Cslib/Foundations/Syntax/HasWellFormed.lean | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/Cslib/Computability/Automata/Transducers/Transducer.lean b/Cslib/Computability/Automata/Transducers/Transducer.lean index 4fec2a5e1..e17942b64 100644 --- a/Cslib/Computability/Automata/Transducers/Transducer.lean +++ b/Cslib/Computability/Automata/Transducers/Transducer.lean @@ -5,8 +5,8 @@ Authors: Fabrizio Montesi -/ module -public import Cslib.Init +public import Cslib.Init /-! # Transducers -/ diff --git a/Cslib/Foundations/Syntax/HasAlphaEquiv.lean b/Cslib/Foundations/Syntax/HasAlphaEquiv.lean index ae2624e3d..c0faf8469 100644 --- a/Cslib/Foundations/Syntax/HasAlphaEquiv.lean +++ b/Cslib/Foundations/Syntax/HasAlphaEquiv.lean @@ -5,8 +5,8 @@ Authors: Fabrizio Montesi -/ module -public import Cslib.Init +public import Cslib.Init /-! Notation typeclass for α-equivalence. -/ diff --git a/Cslib/Foundations/Syntax/HasSubstitution.lean b/Cslib/Foundations/Syntax/HasSubstitution.lean index f9e2d5b2a..b9b31470b 100644 --- a/Cslib/Foundations/Syntax/HasSubstitution.lean +++ b/Cslib/Foundations/Syntax/HasSubstitution.lean @@ -5,8 +5,8 @@ Authors: Fabrizio Montesi -/ module -public import Cslib.Init +public import Cslib.Init /-! Notation typeclass for substitution. -/ diff --git a/Cslib/Foundations/Syntax/HasWellFormed.lean b/Cslib/Foundations/Syntax/HasWellFormed.lean index 96f2e9000..1dd2a6330 100644 --- a/Cslib/Foundations/Syntax/HasWellFormed.lean +++ b/Cslib/Foundations/Syntax/HasWellFormed.lean @@ -5,8 +5,8 @@ Authors: Fabrizio Montesi -/ module -public import Cslib.Init +public import Cslib.Init /-! Notation typeclass for well-formedness. -/ From 57a406bea754bfffc7642d74c31615bd1b972a0a Mon Sep 17 00:00:00 2001 From: Batixx Date: Fri, 17 Jul 2026 18:56:14 +0200 Subject: [PATCH 5/7] include script --- .gitignore | 4 +- scripts/minimize.py | 581 ++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 584 insertions(+), 1 deletion(-) create mode 100755 scripts/minimize.py diff --git a/.gitignore b/.gitignore index 65cfbacbb..6d8033fb2 100644 --- a/.gitignore +++ b/.gitignore @@ -14,4 +14,6 @@ /docs/Std-manifest.json.hash /docs/Std-manifest.json.trace .DS_Store -.claude \ No newline at end of file +.claude +__pycache__ +/scripts/.minimize-state.json \ No newline at end of file diff --git a/scripts/minimize.py b/scripts/minimize.py new file mode 100755 index 000000000..f2af24d4c --- /dev/null +++ b/scripts/minimize.py @@ -0,0 +1,581 @@ +#!/usr/bin/env python3 +""" +minimize.py — minimize and normalize the imports of every CSLib module. + +Runs four phases, in this order: + + 1. Remove transitively-redundant imports. + If a file imports both B and C and B already (publicly) re-exports C, the import + of C is redundant and is dropped. This is provable from the import graph, so no + compilation is needed. + + 2. Empirically minimize the remaining imports. + Processing files in reverse-topological order (dependencies first), each unpinned + import is removed, the module is rebuilt with `lake build `, and the import + is kept out only if the module still compiles. If a file no longer builds even before + any removal (because an earlier file dropped an import it was inheriting), imports from + its original transitive closure are restored until it compiles again, then reduction + proceeds. + + 3. Restore `Cslib.Init` reachability, minimally. + `Cslib.Init` only installs linters / default tactics, so a build-based oracle happily + drops it — but `lake exe checkInitImports` requires every module to import it + (transitively). Phase 3 adds `public import Cslib.Init` to the smallest set of modules + needed so that all of them reach it again. + + 4. Sort the import block of every file into CSLib's canonical order: + + module[ -- annotations] + + public meta import + public import + + meta import + import + + + +Imports excluded from removal in phases 1 & 2 (never touched): + * meta imports (their elaboration-time closure differs from the regular one); + * imports carrying an inline `-- shake: keep` comment; + * every import inside a file whose `module` line has `-- shake: keep-all`; + * `shake: keep-downstream` modules other than `Cslib.Init` (currently: HasFresh). +`Cslib.Init` is deliberately *not* pinned here — phase 3 owns it. + +Usage: + scripts/minimize.py # run all four phases, then a final verification + scripts/minimize.py --dry-run # phases 1/3/4 report only; skips the phase-2 builds + scripts/minimize.py --phases 1,3,4 # run a subset of phases + scripts/minimize.py --resume # continue an interrupted phase-2 pass + scripts/minimize.py --limit N # phase 2: only process the first N eligible files + +The final `lake build` and `lake exe checkInitImports` are always run (unless --dry-run) +so the tree is left green. +""" +from __future__ import annotations +import argparse, json, os, re, subprocess, sys, time + +# --------------------------------------------------------------------------- paths +SCRIPT_DIR = os.path.dirname(os.path.abspath(__file__)) +ROOT = os.path.dirname(SCRIPT_DIR) +PKGS = os.path.join(ROOT, ".lake", "packages") +STATE_FILE = os.path.join(SCRIPT_DIR, ".minimize-state.json") + +# Modules exempt from the Cslib.Init requirement (see scripts/CheckInitImports.lean). +INIT_EXCEPTIONS = {"Cslib.Foundations.Lint.Basic", "Cslib.Init"} +INIT = "Cslib.Init" + + +def toolchain_src() -> str | None: + try: + tc = open(os.path.join(ROOT, "lean-toolchain")).read().strip() + except OSError: + return None + name = tc.replace("/", "--").replace(":", "---") # leanprover/lean4:v4.x -> ...---v4.x + elan = os.environ.get("ELAN_HOME", os.path.expanduser("~/.elan")) + path = os.path.join(elan, "toolchains", name, "src", "lean") + return path if os.path.isdir(path) else None + + +# --------------------------------------------------------------------------- indexing +def index_modules() -> dict[str, str]: + """Map every reachable module name to its .lean source file.""" + mod2file: dict[str, str] = {} + + def add_tree(base, subdirs=None): + for dp, dn, fns in os.walk(base): + dn[:] = [d for d in dn if d not in (".lake", ".git")] + for fn in fns: + if not fn.endswith(".lean"): + continue + full = os.path.join(dp, fn) + rel = os.path.relpath(full, base) + if subdirs is not None and rel.split(os.sep)[0].removesuffix(".lean") not in subdirs: + continue + mod2file.setdefault(rel.removesuffix(".lean").replace(os.sep, "."), full) + + add_tree(ROOT, ["Cslib", "CslibTests"]) + src = toolchain_src() + if src: + add_tree(src) + if os.path.isdir(PKGS): + for p in sorted(os.listdir(PKGS)): + add_tree(os.path.join(PKGS, p)) + return mod2file + + +IMPORT_RE = re.compile( + r"^(?P(?:public\s+|private\s+|meta\s+)*)import\s+(?Pall\s+)?" + r"(?P[A-Za-z_][\w.À-￿]*)\s*(?P--.*)?$") +MODULE_RE = re.compile(r"^module\b(?P.*)$") +DECL_RE = re.compile( + r"^\s*(@\[[^\]]*\]\s*)?((public|private|protected|meta|noncomputable|partial|unsafe|scoped" + r"|local)\s+)*(theorem|lemma|def|instance|structure|inductive|abbrev|class|opaque|axiom" + r"|example|macro|macro_rules|notation|syntax|elab|attribute|deriving|#guard|#check|#eval)\b", + re.M) + + +class Import: + __slots__ = ("name", "line", "pub", "meta", "keep", "cmt", "all") + + def __init__(self, name, line, pub, meta, keep, cmt, all=False): + self.name, self.line, self.pub, self.meta = name, line, pub, meta + self.keep, self.cmt, self.all = keep, cmt, all + + def rank(self): + return 0 if self.pub and self.meta else 1 if self.pub else 2 if self.meta else 3 + + def render(self): + kw = {0: "public meta import", 1: "public import", + 2: "meta import", 3: "import"}[self.rank()] + allkw = "all " if self.all else "" + return f"{kw} {allkw}{self.name}{self.cmt}\n" + + +class Model: + """Parsed import graph over all indexed modules, plus mutable in-repo state.""" + + def __init__(self): + self.mod2file = index_modules() + self.parsed: dict[str, tuple[bool, list[Import]]] = {} + self.keep_all: set[str] = set() + self.keep_downstream: set[str] = set() + self._pub: dict[str, set[str]] = {} # memoized public closures + self.targets = sorted( + m for m in self.mod2file + if (m == "Cslib" or m.startswith("Cslib.") or m == "CslibTests" + or m.startswith("CslibTests.")) + and self.mod2file[m].startswith(ROOT) + and os.sep + ".lake" + os.sep not in self.mod2file[m]) + self.target_set = set(self.targets) + for m in self.targets: + self.parse(m) + # pristine snapshot for the phase-2 restore rule + self.original_visible = {m: self.visible(m) for m in self.targets} + + # ---- parsing ----------------------------------------------------------- + def parse(self, mod): + if mod in self.parsed: + return self.parsed[mod] + f = self.mod2file.get(mod) + if f is None: + self.parsed[mod] = (True, []) + return self.parsed[mod] + imports, is_module, block = [], False, 0 + with open(f, encoding="utf-8") as fh: + for i, line in enumerate(fh, 1): + s = line.strip() + if block: + if "-/" in s: + block -= 1 + continue + if s.startswith("/-"): + if "-/" not in s: + block += 1 + continue + if s.startswith("--") or not s: + continue + mm = MODULE_RE.match(s) + if mm: + is_module = True + if "shake: keep-all" in mm.group("rest"): + self.keep_all.add(mod) + if "shake: keep-downstream" in mm.group("rest"): + self.keep_downstream.add(mod) + continue + code, _, comment = s.partition("--") + m = IMPORT_RE.match(code.strip() + (" --" + comment if comment else "")) + if m: + imports.append(Import( + name=m.group("name"), line=i, + pub="public" in (m.group("mods") or ""), + meta="meta" in (m.group("mods") or ""), + keep="shake: keep" in comment, + cmt=(" " + m.group("cmt")) if m.group("cmt") else "", + all=bool(m.group("all")))) + continue + if s.startswith(("prelude", "set_option", "open ")): + continue + break + self.parsed[mod] = (is_module, imports) + return self.parsed[mod] + + def imports(self, mod): + return self.parsed[mod][1] + + def is_module(self, mod): + return self.parsed[mod][0] + + def has_decls(self, mod): + return bool(DECL_RE.search(open(self.mod2file[mod], encoding="utf-8").read())) + + # ---- closures ---------------------------------------------------------- + def pub_closure(self, mod, _stack=None): + """Modules re-exported (transitively, publicly) by importing `mod`, incl. mod.""" + cached = self._pub.get(mod) + if cached is not None: + return cached + if _stack is None: + _stack = set() + if mod in _stack: + return {mod} # cycle guard: don't cache a partial result + _stack.add(mod) + is_mod, imps = self.parse(mod) + acc = {mod} + complete = True + for im in imps: + if im.meta: + continue + if im.pub or not is_mod: + if im.name in _stack: + complete = False + acc.add(im.name) + else: + acc |= self.pub_closure(im.name, _stack) + _stack.discard(mod) + if complete: + self._pub[mod] = acc + return acc + + def visible(self, mod): + acc = set() + for im in self.imports(mod): + if not im.meta: + acc |= self.pub_closure(im.name) + return acc + + def reaches_init(self, mod): + """True if `mod` transitively imports Cslib.Init (public or private edges).""" + seen, stack = set(), [im.name for im in self.imports(mod)] + while stack: + x = stack.pop() + if x == INIT: + return True + if x in seen: + continue + seen.add(x) + if x in self.parsed: + stack.extend(im.name for im in self.imports(x)) + # external modules never lead back to Cslib.Init + return False + + def topo(self): + """In-repo modules, dependencies before dependents.""" + order, mark = [], {} + + def visit(m): + if mark.get(m): + return + mark[m] = 1 + for im in self.imports(m): + if im.name in self.target_set: + visit(im.name) + order.append(m) + + for m in self.targets: + visit(m) + return order + + # ---- pinning ----------------------------------------------------------- + def pinned(self, mod, im: Import): + """True if `im` must never be removed in phases 1 & 2.""" + if im.meta or im.keep or im.all: + return True + if im.name in self.keep_downstream and im.name != INIT: + return True + return False + + # ---- file writing ------------------------------------------------------ + def write_block(self, mod, imports): + """Overwrite `mod`'s import block with `imports` (order preserved), keeping the + surrounding file intact. Blank lines around the block are left as-is here; phase 4 + normalizes them.""" + self._pub.clear() # graph is changing; drop memoized closures + path = self.mod2file[mod] + with open(path, encoding="utf-8") as fh: + lines = fh.readlines() + old = self.imports(mod) + if not old: + # no existing block: insert after `module` (or at file head for legacy files) + if imports: + mi = next((i for i, l in enumerate(lines) if MODULE_RE.match(l.strip())), None) + pos = (mi + 1) if mi is not None else 0 + ins = ["\n"] + [im.render() for im in imports] + ["\n"] + lines = lines[:pos] + ins + lines[pos:] + with open(path, "w", encoding="utf-8") as fh: + fh.writelines(lines) + return + first = min(im.line for im in old) + last = max(im.line for im in old) + # keep any non-import lines interleaved in the original block + orig_lines = {im.line for im in old} + interleaved = [lines[i - 1] for i in range(first, last + 1) if i not in orig_lines] + body = [im.render() for im in imports] + interleaved + lines = lines[:first - 1] + body + lines[last:] + with open(path, "w", encoding="utf-8") as fh: + fh.writelines(lines) + # re-parse so line numbers stay consistent + del self.parsed[mod] + self.parse(mod) + + +# --------------------------------------------------------------------------- build +def build(mod): + r = subprocess.run(["lake", "build", mod], cwd=ROOT, + capture_output=True, text=True, timeout=1800) + return r.returncode == 0 + + +def full_build(): + r = subprocess.run(["lake", "build"], cwd=ROOT) + return r.returncode == 0 + + +def check_init_imports(): + r = subprocess.run(["lake", "exe", "checkInitImports"], cwd=ROOT, + capture_output=True, text=True, timeout=1800) + return r.returncode == 0, r.stdout + r.stderr + + +def log(msg): + print(msg, flush=True) + + +# --------------------------------------------------------------------------- phase 1 +def phase1(model: Model, dry: bool): + log("\n=== phase 1: remove transitively-redundant imports ===") + removed = 0 + for A in model.targets: + if A in model.keep_all: + continue + is_mod = model.is_module(A) + imps = list(model.imports(A)) + keep = [] + for C in imps: + if C.meta or model.pinned(A, C): + keep.append(C) + continue + redundant = False + for B in imps: + if B is C or B.meta: + continue + # a public import of C needs a *public* carrier (or a legacy file) + if C.pub and not (B.pub or not is_mod): + continue + if C.name in model.pub_closure(B.name) and B.name != C.name: + redundant = True + break + if redundant: + removed += 1 + log(f" - {A}: {C.name} (implied by another import)") + else: + keep.append(C) + if len(keep) != len(imps) and not dry: + model.write_block(A, keep) + log(f"phase 1: removed {removed} redundant imports" + + (" (dry-run, nothing written)" if dry else "")) + return removed + + +# --------------------------------------------------------------------------- phase 2 +def restore_until_builds(model: Model, A): + """Add back imports from A's original closure until it compiles (the restore rule).""" + added = [] + for _ in range(50): + lost = model.original_visible[A] - model.visible(A) + if not lost: + break + maximal = [m for m in lost + if not any(m in model.pub_closure(o) for o in lost if o != m)] + maximal = maximal or sorted(lost) + cur = list(model.imports(A)) + for m in maximal: + cur.append(Import(m, line=-1, pub=model.is_module(A), meta=False, keep=False, cmt="")) + added.append(m) + model.write_block(A, cur) + if build(A): + break + return added + + +def phase2(model: Model, dry: bool, limit, resume): + log("\n=== phase 2: empirical per-import minimization ===") + if dry: + log("phase 2: skipped (--dry-run)") + return 0 + done = set() + if resume and os.path.exists(STATE_FILE): + done = set(json.load(open(STATE_FILE)).get("done", [])) + log(f" resuming: {len(done)} files already processed") + + order = [m for m in model.topo() + if m not in model.keep_all and model.imports(m) and model.has_decls(m)] + removed = processed = 0 + t0 = time.time() + for m in order: + if m in done: + continue + if limit and processed >= limit: + break + # baseline: make sure it builds before we start removing + if not build(m): + added = restore_until_builds(model, m) + if added: + log(f" [restore] {m}: added {added}") + if not build(m): + log(f" [skip] {m}: does not build even after restore") + done.add(m) + continue + # Snapshot the import objects up front; the loop tracks a `keep` list by value, + # never by identity, because write_block re-parses (new objects) after each write. + snapshot = list(model.imports(m)) + keep = list(snapshot) + for im in snapshot: + if model.pinned(m, im): + continue + trial = [x for x in keep if x.name != im.name] + model.write_block(m, trial) + if build(m): + keep = trial + removed += 1 + # on failure, `keep` is unchanged; the next write (or the final one) restores it + model.write_block(m, keep) # ensure the file matches the final keep set + processed += 1 + done.add(m) + json.dump({"done": sorted(done)}, open(STATE_FILE, "w")) + if processed % 10 == 0: + log(f" [{processed}/{len(order)}] removed {removed} so far " + f"({time.time() - t0:.0f}s)") + log(f"phase 2: removed {removed} imports across {processed} files") + if os.path.exists(STATE_FILE) and not limit: + os.remove(STATE_FILE) + return removed + + +# --------------------------------------------------------------------------- phase 3 +def phase3(model: Model, dry: bool): + log("\n=== phase 3: restore Cslib.Init reachability (minimal) ===") + order = model.topo() # dependencies first: adding Init to a root covers its dependents + added_to = [] + for m in order: + if m in INIT_EXCEPTIONS or m in model.keep_all: + continue + if model.reaches_init(m): + continue + # add `public import Cslib.Init` (or plain `import` for legacy files) + if not dry: + cur = list(model.imports(m)) + cur.append(Import(INIT, line=-1, pub=model.is_module(m), + meta=False, keep=False, cmt="")) + model.write_block(m, cur) + added_to.append(m) + log(f" + {m}") + log(f"phase 3: added Cslib.Init to {len(added_to)} modules" + + (" (dry-run)" if dry else "")) + return added_to + + +# --------------------------------------------------------------------------- phase 4 +def phase4(model: Model, dry: bool): + log("\n=== phase 4: sort import blocks into canonical order ===") + changed = 0 + for m in model.targets: + if m in model.keep_all: + continue + if sort_file(model.mod2file[m], dry): + changed += 1 + log(f"phase 4: normalized {changed} files" + (" (dry-run)" if dry else "")) + return changed + + +def sort_file(path, dry): + with open(path, encoding="utf-8") as fh: + lines = fh.readlines() + idx = [i for i, l in enumerate(lines) if IMPORT_RE.match(l.strip())] + if not idx: + return False + first, last = idx[0], idx[-1] + parsed = [] + for i in idx: + m = IMPORT_RE.match(lines[i].strip()) + parsed.append(Import( + name=m.group("name"), line=i, + pub="public" in (m.group("mods") or ""), + meta="meta" in (m.group("mods") or ""), + keep=bool(m.group("cmt") and "shake: keep" in m.group("cmt")), + cmt=(" " + m.group("cmt")) if m.group("cmt") else "", + all=bool(m.group("all")))) + parsed.sort(key=lambda im: (im.rank(), im.name)) + + block, prev_private = [], None + for im in parsed: + priv = im.rank() >= 2 + if prev_private is False and priv: + block.append("\n") # blank between exported and private groups + block.append(im.render()) + prev_private = priv + + # header: everything up to the first import; ensure exactly one blank before the block + head = lines[:first] + while head and head[-1].strip() == "": + head.pop() + # tail: everything after the last import; ensure exactly one blank after the block + tail = lines[last + 1:] + while tail and tail[0].strip() == "": + tail.pop(0) + # a separating blank only makes sense when there is something to separate from + new = (head + (["\n"] if head else []) + + block + + (["\n"] + tail if tail else [])) + if new != lines: + if not dry: + with open(path, "w", encoding="utf-8") as fh: + fh.writelines(new) + return True + return False + + +# --------------------------------------------------------------------------- main +def main(): + ap = argparse.ArgumentParser(description="Minimize and normalize CSLib imports.") + ap.add_argument("--phases", default="1,2,3,4", + help="comma-separated phases to run (default: 1,2,3,4)") + ap.add_argument("--dry-run", action="store_true", + help="report only; skip phase-2 builds and write nothing") + ap.add_argument("--limit", type=int, default=0, + help="phase 2: process at most N files (for testing)") + ap.add_argument("--resume", action="store_true", + help="phase 2: resume from the saved state file") + ap.add_argument("--no-verify", action="store_true", + help="skip the final lake build + checkInitImports") + args = ap.parse_args() + phases = {int(p) for p in args.phases.split(",") if p.strip()} + + model = Model() + log(f"indexed {len(model.mod2file)} modules; {len(model.targets)} CSLib targets") + log(f"keep-all files: {sorted(model.keep_all)}") + log(f"keep-downstream: {sorted(model.keep_downstream)}") + + if 1 in phases: + phase1(model, args.dry_run) + if 2 in phases: + phase2(model, args.dry_run, args.limit, args.resume) + if 3 in phases: + phase3(model, args.dry_run) + if 4 in phases: + phase4(model, args.dry_run) + + if args.dry_run or args.no_verify: + return + log("\n=== verification ===") + ok_build = full_build() + log(f"lake build: {'ok' if ok_build else 'FAILED'}") + ok_init, out = check_init_imports() + log(f"checkInitImports: {'ok' if ok_init else 'FAILED'}") + if not ok_init: + log(out.strip()[:2000]) + sys.exit(0 if ok_build and ok_init else 1) + + +if __name__ == "__main__": + main() From 3f41c002d5c1ac8728a5fb9426fd297f7c31b5a0 Mon Sep 17 00:00:00 2001 From: Batixx Date: Fri, 17 Jul 2026 19:01:05 +0200 Subject: [PATCH 6/7] exclude again --- .gitignore | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/.gitignore b/.gitignore index 6d8033fb2..65cfbacbb 100644 --- a/.gitignore +++ b/.gitignore @@ -14,6 +14,4 @@ /docs/Std-manifest.json.hash /docs/Std-manifest.json.trace .DS_Store -.claude -__pycache__ -/scripts/.minimize-state.json \ No newline at end of file +.claude \ No newline at end of file From 9a35cbc69adaed41a28a551217edf84e47f8fe64 Mon Sep 17 00:00:00 2001 From: Batixx Date: Fri, 17 Jul 2026 19:03:45 +0200 Subject: [PATCH 7/7] . --- scripts/minimize.py | 581 -------------------------------------------- 1 file changed, 581 deletions(-) delete mode 100755 scripts/minimize.py diff --git a/scripts/minimize.py b/scripts/minimize.py deleted file mode 100755 index f2af24d4c..000000000 --- a/scripts/minimize.py +++ /dev/null @@ -1,581 +0,0 @@ -#!/usr/bin/env python3 -""" -minimize.py — minimize and normalize the imports of every CSLib module. - -Runs four phases, in this order: - - 1. Remove transitively-redundant imports. - If a file imports both B and C and B already (publicly) re-exports C, the import - of C is redundant and is dropped. This is provable from the import graph, so no - compilation is needed. - - 2. Empirically minimize the remaining imports. - Processing files in reverse-topological order (dependencies first), each unpinned - import is removed, the module is rebuilt with `lake build `, and the import - is kept out only if the module still compiles. If a file no longer builds even before - any removal (because an earlier file dropped an import it was inheriting), imports from - its original transitive closure are restored until it compiles again, then reduction - proceeds. - - 3. Restore `Cslib.Init` reachability, minimally. - `Cslib.Init` only installs linters / default tactics, so a build-based oracle happily - drops it — but `lake exe checkInitImports` requires every module to import it - (transitively). Phase 3 adds `public import Cslib.Init` to the smallest set of modules - needed so that all of them reach it again. - - 4. Sort the import block of every file into CSLib's canonical order: - - module[ -- annotations] - - public meta import - public import - - meta import - import - - - -Imports excluded from removal in phases 1 & 2 (never touched): - * meta imports (their elaboration-time closure differs from the regular one); - * imports carrying an inline `-- shake: keep` comment; - * every import inside a file whose `module` line has `-- shake: keep-all`; - * `shake: keep-downstream` modules other than `Cslib.Init` (currently: HasFresh). -`Cslib.Init` is deliberately *not* pinned here — phase 3 owns it. - -Usage: - scripts/minimize.py # run all four phases, then a final verification - scripts/minimize.py --dry-run # phases 1/3/4 report only; skips the phase-2 builds - scripts/minimize.py --phases 1,3,4 # run a subset of phases - scripts/minimize.py --resume # continue an interrupted phase-2 pass - scripts/minimize.py --limit N # phase 2: only process the first N eligible files - -The final `lake build` and `lake exe checkInitImports` are always run (unless --dry-run) -so the tree is left green. -""" -from __future__ import annotations -import argparse, json, os, re, subprocess, sys, time - -# --------------------------------------------------------------------------- paths -SCRIPT_DIR = os.path.dirname(os.path.abspath(__file__)) -ROOT = os.path.dirname(SCRIPT_DIR) -PKGS = os.path.join(ROOT, ".lake", "packages") -STATE_FILE = os.path.join(SCRIPT_DIR, ".minimize-state.json") - -# Modules exempt from the Cslib.Init requirement (see scripts/CheckInitImports.lean). -INIT_EXCEPTIONS = {"Cslib.Foundations.Lint.Basic", "Cslib.Init"} -INIT = "Cslib.Init" - - -def toolchain_src() -> str | None: - try: - tc = open(os.path.join(ROOT, "lean-toolchain")).read().strip() - except OSError: - return None - name = tc.replace("/", "--").replace(":", "---") # leanprover/lean4:v4.x -> ...---v4.x - elan = os.environ.get("ELAN_HOME", os.path.expanduser("~/.elan")) - path = os.path.join(elan, "toolchains", name, "src", "lean") - return path if os.path.isdir(path) else None - - -# --------------------------------------------------------------------------- indexing -def index_modules() -> dict[str, str]: - """Map every reachable module name to its .lean source file.""" - mod2file: dict[str, str] = {} - - def add_tree(base, subdirs=None): - for dp, dn, fns in os.walk(base): - dn[:] = [d for d in dn if d not in (".lake", ".git")] - for fn in fns: - if not fn.endswith(".lean"): - continue - full = os.path.join(dp, fn) - rel = os.path.relpath(full, base) - if subdirs is not None and rel.split(os.sep)[0].removesuffix(".lean") not in subdirs: - continue - mod2file.setdefault(rel.removesuffix(".lean").replace(os.sep, "."), full) - - add_tree(ROOT, ["Cslib", "CslibTests"]) - src = toolchain_src() - if src: - add_tree(src) - if os.path.isdir(PKGS): - for p in sorted(os.listdir(PKGS)): - add_tree(os.path.join(PKGS, p)) - return mod2file - - -IMPORT_RE = re.compile( - r"^(?P(?:public\s+|private\s+|meta\s+)*)import\s+(?Pall\s+)?" - r"(?P[A-Za-z_][\w.À-￿]*)\s*(?P--.*)?$") -MODULE_RE = re.compile(r"^module\b(?P.*)$") -DECL_RE = re.compile( - r"^\s*(@\[[^\]]*\]\s*)?((public|private|protected|meta|noncomputable|partial|unsafe|scoped" - r"|local)\s+)*(theorem|lemma|def|instance|structure|inductive|abbrev|class|opaque|axiom" - r"|example|macro|macro_rules|notation|syntax|elab|attribute|deriving|#guard|#check|#eval)\b", - re.M) - - -class Import: - __slots__ = ("name", "line", "pub", "meta", "keep", "cmt", "all") - - def __init__(self, name, line, pub, meta, keep, cmt, all=False): - self.name, self.line, self.pub, self.meta = name, line, pub, meta - self.keep, self.cmt, self.all = keep, cmt, all - - def rank(self): - return 0 if self.pub and self.meta else 1 if self.pub else 2 if self.meta else 3 - - def render(self): - kw = {0: "public meta import", 1: "public import", - 2: "meta import", 3: "import"}[self.rank()] - allkw = "all " if self.all else "" - return f"{kw} {allkw}{self.name}{self.cmt}\n" - - -class Model: - """Parsed import graph over all indexed modules, plus mutable in-repo state.""" - - def __init__(self): - self.mod2file = index_modules() - self.parsed: dict[str, tuple[bool, list[Import]]] = {} - self.keep_all: set[str] = set() - self.keep_downstream: set[str] = set() - self._pub: dict[str, set[str]] = {} # memoized public closures - self.targets = sorted( - m for m in self.mod2file - if (m == "Cslib" or m.startswith("Cslib.") or m == "CslibTests" - or m.startswith("CslibTests.")) - and self.mod2file[m].startswith(ROOT) - and os.sep + ".lake" + os.sep not in self.mod2file[m]) - self.target_set = set(self.targets) - for m in self.targets: - self.parse(m) - # pristine snapshot for the phase-2 restore rule - self.original_visible = {m: self.visible(m) for m in self.targets} - - # ---- parsing ----------------------------------------------------------- - def parse(self, mod): - if mod in self.parsed: - return self.parsed[mod] - f = self.mod2file.get(mod) - if f is None: - self.parsed[mod] = (True, []) - return self.parsed[mod] - imports, is_module, block = [], False, 0 - with open(f, encoding="utf-8") as fh: - for i, line in enumerate(fh, 1): - s = line.strip() - if block: - if "-/" in s: - block -= 1 - continue - if s.startswith("/-"): - if "-/" not in s: - block += 1 - continue - if s.startswith("--") or not s: - continue - mm = MODULE_RE.match(s) - if mm: - is_module = True - if "shake: keep-all" in mm.group("rest"): - self.keep_all.add(mod) - if "shake: keep-downstream" in mm.group("rest"): - self.keep_downstream.add(mod) - continue - code, _, comment = s.partition("--") - m = IMPORT_RE.match(code.strip() + (" --" + comment if comment else "")) - if m: - imports.append(Import( - name=m.group("name"), line=i, - pub="public" in (m.group("mods") or ""), - meta="meta" in (m.group("mods") or ""), - keep="shake: keep" in comment, - cmt=(" " + m.group("cmt")) if m.group("cmt") else "", - all=bool(m.group("all")))) - continue - if s.startswith(("prelude", "set_option", "open ")): - continue - break - self.parsed[mod] = (is_module, imports) - return self.parsed[mod] - - def imports(self, mod): - return self.parsed[mod][1] - - def is_module(self, mod): - return self.parsed[mod][0] - - def has_decls(self, mod): - return bool(DECL_RE.search(open(self.mod2file[mod], encoding="utf-8").read())) - - # ---- closures ---------------------------------------------------------- - def pub_closure(self, mod, _stack=None): - """Modules re-exported (transitively, publicly) by importing `mod`, incl. mod.""" - cached = self._pub.get(mod) - if cached is not None: - return cached - if _stack is None: - _stack = set() - if mod in _stack: - return {mod} # cycle guard: don't cache a partial result - _stack.add(mod) - is_mod, imps = self.parse(mod) - acc = {mod} - complete = True - for im in imps: - if im.meta: - continue - if im.pub or not is_mod: - if im.name in _stack: - complete = False - acc.add(im.name) - else: - acc |= self.pub_closure(im.name, _stack) - _stack.discard(mod) - if complete: - self._pub[mod] = acc - return acc - - def visible(self, mod): - acc = set() - for im in self.imports(mod): - if not im.meta: - acc |= self.pub_closure(im.name) - return acc - - def reaches_init(self, mod): - """True if `mod` transitively imports Cslib.Init (public or private edges).""" - seen, stack = set(), [im.name for im in self.imports(mod)] - while stack: - x = stack.pop() - if x == INIT: - return True - if x in seen: - continue - seen.add(x) - if x in self.parsed: - stack.extend(im.name for im in self.imports(x)) - # external modules never lead back to Cslib.Init - return False - - def topo(self): - """In-repo modules, dependencies before dependents.""" - order, mark = [], {} - - def visit(m): - if mark.get(m): - return - mark[m] = 1 - for im in self.imports(m): - if im.name in self.target_set: - visit(im.name) - order.append(m) - - for m in self.targets: - visit(m) - return order - - # ---- pinning ----------------------------------------------------------- - def pinned(self, mod, im: Import): - """True if `im` must never be removed in phases 1 & 2.""" - if im.meta or im.keep or im.all: - return True - if im.name in self.keep_downstream and im.name != INIT: - return True - return False - - # ---- file writing ------------------------------------------------------ - def write_block(self, mod, imports): - """Overwrite `mod`'s import block with `imports` (order preserved), keeping the - surrounding file intact. Blank lines around the block are left as-is here; phase 4 - normalizes them.""" - self._pub.clear() # graph is changing; drop memoized closures - path = self.mod2file[mod] - with open(path, encoding="utf-8") as fh: - lines = fh.readlines() - old = self.imports(mod) - if not old: - # no existing block: insert after `module` (or at file head for legacy files) - if imports: - mi = next((i for i, l in enumerate(lines) if MODULE_RE.match(l.strip())), None) - pos = (mi + 1) if mi is not None else 0 - ins = ["\n"] + [im.render() for im in imports] + ["\n"] - lines = lines[:pos] + ins + lines[pos:] - with open(path, "w", encoding="utf-8") as fh: - fh.writelines(lines) - return - first = min(im.line for im in old) - last = max(im.line for im in old) - # keep any non-import lines interleaved in the original block - orig_lines = {im.line for im in old} - interleaved = [lines[i - 1] for i in range(first, last + 1) if i not in orig_lines] - body = [im.render() for im in imports] + interleaved - lines = lines[:first - 1] + body + lines[last:] - with open(path, "w", encoding="utf-8") as fh: - fh.writelines(lines) - # re-parse so line numbers stay consistent - del self.parsed[mod] - self.parse(mod) - - -# --------------------------------------------------------------------------- build -def build(mod): - r = subprocess.run(["lake", "build", mod], cwd=ROOT, - capture_output=True, text=True, timeout=1800) - return r.returncode == 0 - - -def full_build(): - r = subprocess.run(["lake", "build"], cwd=ROOT) - return r.returncode == 0 - - -def check_init_imports(): - r = subprocess.run(["lake", "exe", "checkInitImports"], cwd=ROOT, - capture_output=True, text=True, timeout=1800) - return r.returncode == 0, r.stdout + r.stderr - - -def log(msg): - print(msg, flush=True) - - -# --------------------------------------------------------------------------- phase 1 -def phase1(model: Model, dry: bool): - log("\n=== phase 1: remove transitively-redundant imports ===") - removed = 0 - for A in model.targets: - if A in model.keep_all: - continue - is_mod = model.is_module(A) - imps = list(model.imports(A)) - keep = [] - for C in imps: - if C.meta or model.pinned(A, C): - keep.append(C) - continue - redundant = False - for B in imps: - if B is C or B.meta: - continue - # a public import of C needs a *public* carrier (or a legacy file) - if C.pub and not (B.pub or not is_mod): - continue - if C.name in model.pub_closure(B.name) and B.name != C.name: - redundant = True - break - if redundant: - removed += 1 - log(f" - {A}: {C.name} (implied by another import)") - else: - keep.append(C) - if len(keep) != len(imps) and not dry: - model.write_block(A, keep) - log(f"phase 1: removed {removed} redundant imports" - + (" (dry-run, nothing written)" if dry else "")) - return removed - - -# --------------------------------------------------------------------------- phase 2 -def restore_until_builds(model: Model, A): - """Add back imports from A's original closure until it compiles (the restore rule).""" - added = [] - for _ in range(50): - lost = model.original_visible[A] - model.visible(A) - if not lost: - break - maximal = [m for m in lost - if not any(m in model.pub_closure(o) for o in lost if o != m)] - maximal = maximal or sorted(lost) - cur = list(model.imports(A)) - for m in maximal: - cur.append(Import(m, line=-1, pub=model.is_module(A), meta=False, keep=False, cmt="")) - added.append(m) - model.write_block(A, cur) - if build(A): - break - return added - - -def phase2(model: Model, dry: bool, limit, resume): - log("\n=== phase 2: empirical per-import minimization ===") - if dry: - log("phase 2: skipped (--dry-run)") - return 0 - done = set() - if resume and os.path.exists(STATE_FILE): - done = set(json.load(open(STATE_FILE)).get("done", [])) - log(f" resuming: {len(done)} files already processed") - - order = [m for m in model.topo() - if m not in model.keep_all and model.imports(m) and model.has_decls(m)] - removed = processed = 0 - t0 = time.time() - for m in order: - if m in done: - continue - if limit and processed >= limit: - break - # baseline: make sure it builds before we start removing - if not build(m): - added = restore_until_builds(model, m) - if added: - log(f" [restore] {m}: added {added}") - if not build(m): - log(f" [skip] {m}: does not build even after restore") - done.add(m) - continue - # Snapshot the import objects up front; the loop tracks a `keep` list by value, - # never by identity, because write_block re-parses (new objects) after each write. - snapshot = list(model.imports(m)) - keep = list(snapshot) - for im in snapshot: - if model.pinned(m, im): - continue - trial = [x for x in keep if x.name != im.name] - model.write_block(m, trial) - if build(m): - keep = trial - removed += 1 - # on failure, `keep` is unchanged; the next write (or the final one) restores it - model.write_block(m, keep) # ensure the file matches the final keep set - processed += 1 - done.add(m) - json.dump({"done": sorted(done)}, open(STATE_FILE, "w")) - if processed % 10 == 0: - log(f" [{processed}/{len(order)}] removed {removed} so far " - f"({time.time() - t0:.0f}s)") - log(f"phase 2: removed {removed} imports across {processed} files") - if os.path.exists(STATE_FILE) and not limit: - os.remove(STATE_FILE) - return removed - - -# --------------------------------------------------------------------------- phase 3 -def phase3(model: Model, dry: bool): - log("\n=== phase 3: restore Cslib.Init reachability (minimal) ===") - order = model.topo() # dependencies first: adding Init to a root covers its dependents - added_to = [] - for m in order: - if m in INIT_EXCEPTIONS or m in model.keep_all: - continue - if model.reaches_init(m): - continue - # add `public import Cslib.Init` (or plain `import` for legacy files) - if not dry: - cur = list(model.imports(m)) - cur.append(Import(INIT, line=-1, pub=model.is_module(m), - meta=False, keep=False, cmt="")) - model.write_block(m, cur) - added_to.append(m) - log(f" + {m}") - log(f"phase 3: added Cslib.Init to {len(added_to)} modules" - + (" (dry-run)" if dry else "")) - return added_to - - -# --------------------------------------------------------------------------- phase 4 -def phase4(model: Model, dry: bool): - log("\n=== phase 4: sort import blocks into canonical order ===") - changed = 0 - for m in model.targets: - if m in model.keep_all: - continue - if sort_file(model.mod2file[m], dry): - changed += 1 - log(f"phase 4: normalized {changed} files" + (" (dry-run)" if dry else "")) - return changed - - -def sort_file(path, dry): - with open(path, encoding="utf-8") as fh: - lines = fh.readlines() - idx = [i for i, l in enumerate(lines) if IMPORT_RE.match(l.strip())] - if not idx: - return False - first, last = idx[0], idx[-1] - parsed = [] - for i in idx: - m = IMPORT_RE.match(lines[i].strip()) - parsed.append(Import( - name=m.group("name"), line=i, - pub="public" in (m.group("mods") or ""), - meta="meta" in (m.group("mods") or ""), - keep=bool(m.group("cmt") and "shake: keep" in m.group("cmt")), - cmt=(" " + m.group("cmt")) if m.group("cmt") else "", - all=bool(m.group("all")))) - parsed.sort(key=lambda im: (im.rank(), im.name)) - - block, prev_private = [], None - for im in parsed: - priv = im.rank() >= 2 - if prev_private is False and priv: - block.append("\n") # blank between exported and private groups - block.append(im.render()) - prev_private = priv - - # header: everything up to the first import; ensure exactly one blank before the block - head = lines[:first] - while head and head[-1].strip() == "": - head.pop() - # tail: everything after the last import; ensure exactly one blank after the block - tail = lines[last + 1:] - while tail and tail[0].strip() == "": - tail.pop(0) - # a separating blank only makes sense when there is something to separate from - new = (head + (["\n"] if head else []) - + block - + (["\n"] + tail if tail else [])) - if new != lines: - if not dry: - with open(path, "w", encoding="utf-8") as fh: - fh.writelines(new) - return True - return False - - -# --------------------------------------------------------------------------- main -def main(): - ap = argparse.ArgumentParser(description="Minimize and normalize CSLib imports.") - ap.add_argument("--phases", default="1,2,3,4", - help="comma-separated phases to run (default: 1,2,3,4)") - ap.add_argument("--dry-run", action="store_true", - help="report only; skip phase-2 builds and write nothing") - ap.add_argument("--limit", type=int, default=0, - help="phase 2: process at most N files (for testing)") - ap.add_argument("--resume", action="store_true", - help="phase 2: resume from the saved state file") - ap.add_argument("--no-verify", action="store_true", - help="skip the final lake build + checkInitImports") - args = ap.parse_args() - phases = {int(p) for p in args.phases.split(",") if p.strip()} - - model = Model() - log(f"indexed {len(model.mod2file)} modules; {len(model.targets)} CSLib targets") - log(f"keep-all files: {sorted(model.keep_all)}") - log(f"keep-downstream: {sorted(model.keep_downstream)}") - - if 1 in phases: - phase1(model, args.dry_run) - if 2 in phases: - phase2(model, args.dry_run, args.limit, args.resume) - if 3 in phases: - phase3(model, args.dry_run) - if 4 in phases: - phase4(model, args.dry_run) - - if args.dry_run or args.no_verify: - return - log("\n=== verification ===") - ok_build = full_build() - log(f"lake build: {'ok' if ok_build else 'FAILED'}") - ok_init, out = check_init_imports() - log(f"checkInitImports: {'ok' if ok_init else 'FAILED'}") - if not ok_init: - log(out.strip()[:2000]) - sys.exit(0 if ok_build and ok_init else 1) - - -if __name__ == "__main__": - main()