diff --git a/.gitattributes b/.gitattributes index 1ea36cb79b..4daec97449 100644 --- a/.gitattributes +++ b/.gitattributes @@ -1,7 +1,7 @@ -# Generated root import aggregators are sorted lists of one-line imports. +# Generated root import aggregators are sorted lists of one-line imports. (The test library has +# no aggregator: Lake builds it from a glob, see `lakefile.toml`.) # Union merge avoids spurious 3-line context conflicts when concurrent PRs add # imports in the same alphabetical neighborhood; `lake exe mk_all --check` in # merge-queue CI still enforces canonical sort order. Complexity.lean merge=union -ComplexityTests.lean merge=union abstracts/ComplexityAbstracts.lean merge=union diff --git a/AGENTS.md b/AGENTS.md index 70b51efebf..fc1d93e35e 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -253,7 +253,7 @@ ambiguous change/import analysis fall back to all six gates. Run the default com submitting a PR; quick success does not satisfy that requirement. `lake exe mk_all` regenerates `Complexity.lean` after adding a file. New test files go in -`ComplexityTests/` and must be imported from `ComplexityTests.lean`. +`ComplexityTests/`; the test library is built from a Lake glob, so there is no aggregator to update. ## File rules @@ -393,10 +393,10 @@ and [API review with explicit nonblocking nits](https://github.com/leanprover/cs `abstracts/catalogue.json` selects the public headline results. Each selected group has a checked `*Abstract.lean` and `*Bridge.lean` under `abstracts/ComplexityAbstracts/`, imported by the -dedicated `ComplexityAbstracts` library. `ComplexityTests.lean` imports that library and its -regression tests. Existing declaration namespaces remain stable across the source relocation. -The Lean definitions and statements are the source of truth; PDFs are generated from them, with -proof bodies omitted. There is no separately maintained paper/TeX index. +dedicated `ComplexityAbstracts` library. `ComplexityTests/Abstracts/All.lean` imports that library, +and its regression tests sit beside it. Existing declaration namespaces remain stable across the +source relocation. The Lean definitions and statements are the source of truth; PDFs are generated +from them, with proof bodies omitted. There is no separately maintained paper/TeX index. Selection has a higher bar than inclusion in the library: a headline must be a substantial proved endpoint with conventional, inspectable semantics, hypotheses that are satisfiable or are standard diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index beb55bd81d..81b20cecaf 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -179,10 +179,10 @@ Keep incomplete endpoints in `ROADMAP.md` and credit mathematical and formalizat Every AI-authored PR must assess its final Lean changes against the selection. Update affected abstracts and scope notes, or explain why the catalogue is unaffected. Proof-only changes with -unchanged statements and scope can record that assessment without rewriting the abstract. Follow -the repository's `lean-abstract` skill, import new abstracts in `ComplexityTests.lean`, and run their -`#check_abstract` audits. Allow only narrow, explained foundational models; do not allowlist the -result's class definitions or construction to evade a self-contained statement. +unchanged statements and scope can record that assessment without rewriting the abstract. Follow the +repository's `lean-abstract` skill, import new abstracts in `ComplexityTests/Abstracts/All.lean`, +and run their `#check_abstract` audits. Allow only narrow, explained foundational models; do not +allowlist the result's class definitions or construction to evade a self-contained statement. Arrange independent API, correctness and abstract reviews against the final source revision. Reviewers must check quantifiers, semantics, encodings, bounds, nonvacuity and readability. Record diff --git a/ComplexityTests.lean b/ComplexityTests.lean deleted file mode 100644 index d195d5d491..0000000000 --- a/ComplexityTests.lean +++ /dev/null @@ -1,508 +0,0 @@ -import ComplexityTests.AKSCriterion -import ComplexityTests.AWPPAmplification -import ComplexityTests.AWPPLowness -import ComplexityTests.Abstracts.All -import ComplexityTests.Abstracts.CheckTests -import ComplexityTests.Abstracts.CommunicationTests -import ComplexityTests.Abstracts.ImmermanSzelepcsenyiTests -import ComplexityTests.Abstracts.InputLayouts -import ComplexityTests.Abstracts.SipserLautemannTests -import ComplexityTests.AdaptivePPT -import ComplexityTests.Advice -import ComplexityTests.AffineController -import ComplexityTests.AffineDisperser -import ComplexityTests.AffineDisperserCorollary -import ComplexityTests.AffineDisperserLowerBound -import ComplexityTests.AffineDisperserRuntime -import ComplexityTests.AlgebraicComplexity -import ComplexityTests.Alternation -import ComplexityTests.ApproximateCounting -import ComplexityTests.ArithmeticHessian -import ComplexityTests.ArithmeticHessianRelative -import ComplexityTests.ArithmeticWaring -import ComplexityTests.ArthurMerlin -import ComplexityTests.Axioms -import ComplexityTests.BalancedCode -import ComplexityTests.BasicClasses -import ComplexityTests.BatchLookup -import ComplexityTests.BatchOr -import ComplexityTests.BipartiteMatching -import ComplexityTests.BitString -import ComplexityTests.BitStringProjection -import ComplexityTests.BitStringRows -import ComplexityTests.BitonicSort -import ComplexityTests.BitonicTrace -import ComplexityTests.BooleanAnalysisDecisionTree -import ComplexityTests.BooleanAnalysisExamples -import ComplexityTests.BooleanHierarchyClosure -import ComplexityTests.BooleanHierarchyPH -import ComplexityTests.BoundedUniform -import ComplexityTests.Broadcast -import ComplexityTests.CNF -import ComplexityTests.CNFPolyTime -import ComplexityTests.CarryLookahead -import ComplexityTests.CarrySaveNative -import ComplexityTests.CircuitCertificate -import ComplexityTests.CircuitEvaluation -import ComplexityTests.CircuitHamming.Approximation -import ComplexityTests.CircuitHamming.Continuity -import ComplexityTests.CircuitHamming.Gates -import ComplexityTests.CircuitHamming.Parseval -import ComplexityTests.CircuitHamming.Pointwise -import ComplexityTests.CircuitLayerPadding -import ComplexityTests.CircuitLayering -import ComplexityTests.CircuitMaterialize -import ComplexityTests.CircuitMetric -import ComplexityTests.CircuitValueCompleteness -import ComplexityTests.ClassClosure -import ComplexityTests.ClassCorollaries -import ComplexityTests.Code -import ComplexityTests.Code.Concatenation -import ComplexityTests.Code.Johnson -import ComplexityTests.Code.M3 -import ComplexityTests.CodeComposition -import ComplexityTests.CodeSubstitution -import ComplexityTests.CoinTape -import ComplexityTests.CombinatorialBounds -import ComplexityTests.CombinatoricsExamples -import ComplexityTests.CommunicationComplexity -import ComplexityTests.CommunicationComplexity2 -import ComplexityTests.CommunicationComplexity3 -import ComplexityTests.CommunicationComplexity4 -import ComplexityTests.CompareSwap -import ComplexityTests.ComparisonCircuits -import ComplexityTests.Computability.Circuit.Boolean.ACC0 -import ComplexityTests.ComputationalCrypto -import ComplexityTests.ConditioningCollision -import ComplexityTests.ConfigurationGraph -import ComplexityTests.ConfigurationPolyTime -import ComplexityTests.Consolidation -import ComplexityTests.ContextualPower -import ComplexityTests.CookLevinPolyTime -import ComplexityTests.CountingAggregation -import ComplexityTests.CountingAmbiguity -import ComplexityTests.CountingBranches -import ComplexityTests.CountingCompleteness -import ComplexityTests.CountingComposition -import ComplexityTests.CountingExecution -import ComplexityTests.CountingGapMachine -import ComplexityTests.CountingGuess -import ComplexityTests.CountingMachine -import ComplexityTests.CountingOracle -import ComplexityTests.CountingOracleEquivalence -import ComplexityTests.CountingProducts -import ComplexityTests.CountingSpace -import ComplexityTests.CountingVerifier -import ComplexityTests.Crypto.Bootstrapping -import ComplexityTests.Crypto.CarterWegman -import ComplexityTests.Crypto.Commitment -import ComplexityTests.Crypto.DiffieHellman -import ComplexityTests.Crypto.Encryption -import ComplexityTests.Crypto.EvenMansour -import ComplexityTests.Crypto.FiatShamir -import ComplexityTests.Crypto.FixedKeySecurity -import ComplexityTests.Crypto.Forking -import ComplexityTests.Crypto.GMWPointwise -import ComplexityTests.Crypto.GSW -import ComplexityTests.Crypto.GSWDecryption -import ComplexityTests.Crypto.GSWDecryptionCircuit -import ComplexityTests.Crypto.GSWDepthParameters -import ComplexityTests.Crypto.GSWEvaluation -import ComplexityTests.Crypto.GSWHiding -import ComplexityTests.Crypto.GSWNative -import ComplexityTests.Crypto.GSWParameters -import ComplexityTests.Crypto.GSWSampling -import ComplexityTests.Crypto.GSWSecurity -import ComplexityTests.Crypto.GameBounds -import ComplexityTests.Crypto.HomomorphicEvaluation -import ComplexityTests.Crypto.HomomorphicExample -import ComplexityTests.Crypto.HomomorphicFixedKey -import ComplexityTests.Crypto.HomomorphicLayered -import ComplexityTests.Crypto.HomomorphicLeveled -import ComplexityTests.Crypto.HomomorphicRefresh -import ComplexityTests.Crypto.KeyChainSecurity -import ComplexityTests.Crypto.LeveledSecurity -import ComplexityTests.Crypto.LubyRackoff -import ComplexityTests.Crypto.Lyubashevsky -import ComplexityTests.Crypto.LyubashevskyNative -import ComplexityTests.Crypto.MAC -import ComplexityTests.Crypto.MerkleDamgard -import ComplexityTests.Crypto.PlainConstructors -import ComplexityTests.Crypto.SchnorrDiscreteLog -import ComplexityTests.Crypto.SigmaIdentification -import ComplexityTests.Crypto.SigmaProtocol -import ComplexityTests.Crypto.Signature -import ComplexityTests.Crypto.UntilBad -import ComplexityTests.Crypto.ZeroKnowledge -import ComplexityTests.CyclicFeedback -import ComplexityTests.DataStructure -import ComplexityTests.DataStructureQueue -import ComplexityTests.DataStructureRetroactive -import ComplexityTests.DecisionTree -import ComplexityTests.DenseMask -import ComplexityTests.DependentTable -import ComplexityTests.Derandomization -import ComplexityTests.DuplicateFlags -import ComplexityTests.DynamicArray -import ComplexityTests.ElementDistinctnessRAM -import ComplexityTests.EmpiricalProbability -import ComplexityTests.Encodings -import ComplexityTests.EntropyPseudoentropy -import ComplexityTests.Expander -import ComplexityTests.ExpanderContraction -import ComplexityTests.ExpanderFamily -import ComplexityTests.ExpanderHitting -import ComplexityTests.ExplicitExpanders -import ComplexityTests.ExponentialPadding -import ComplexityTests.Extractor -import ComplexityTests.FOLogSpace -import ComplexityTests.FOLogSpaceReduction -import ComplexityTests.Fagin -import ComplexityTests.FaginEncoding -import ComplexityTests.FaginNP -import ComplexityTests.FineGrained -import ComplexityTests.FineGrained.GraphProblems -import ComplexityTests.FineGrained.Sparsification -import ComplexityTests.FiniteControl -import ComplexityTests.FiniteCover -import ComplexityTests.FiniteFieldUnitSum -import ComplexityTests.FiniteMachine -import ComplexityTests.FiniteTables -import ComplexityTests.FirstOrderAutomation -import ComplexityTests.FirstOrderConstants -import ComplexityTests.FirstOrderProjection -import ComplexityTests.FirstOrderReductions -import ComplexityTests.FormulaDepth -import ComplexityTests.FoundationsExamples -import ComplexityTests.FourierLearning -import ComplexityTests.FrontierAverageCaseImports -import ComplexityTests.FrontierFiniteEdges -import ComplexityTests.FrontierRectangleImports -import ComplexityTests.FunctionalGraph -import ComplexityTests.FunctionalGraphSpectrum -import ComplexityTests.Fusion -import ComplexityTests.FusionBoolean -import ComplexityTests.FusionClosure -import ComplexityTests.FusionConondeterministic -import ComplexityTests.FusionConsistency -import ComplexityTests.FusionConverse -import ComplexityTests.FusionCyclic -import ComplexityTests.FusionDeMorgan -import ComplexityTests.FusionGraph -import ComplexityTests.FusionHomomorphism -import ComplexityTests.FusionQuadratic -import ComplexityTests.FusionRandom -import ComplexityTests.FusionSampling -import ComplexityTests.FusionSemifilter -import ComplexityTests.FusionTransport -import ComplexityTests.FusionTree -import ComplexityTests.FusionTreeHeight -import ComplexityTests.FusionTreeLayout -import ComplexityTests.FusionTreeQuery -import ComplexityTests.FusionTreeRAM -import ComplexityTests.GGM -import ComplexityTests.GapGraphsGeography -import ComplexityTests.GeneratorPadding -import ComplexityTests.GeneratorReindex -import ComplexityTests.GeneratorXor -import ComplexityTests.GenericRAM -import ComplexityTests.GenericRAMAlgebraic -import ComplexityTests.GenericRAMNative -import ComplexityTests.GenericRAMSigned -import ComplexityTests.GenericRAMSimulation -import ComplexityTests.GoldreichLevin -import ComplexityTests.Halting -import ComplexityTests.HardCore -import ComplexityTests.HardnessAmplification -import ComplexityTests.HashFamily -import ComplexityTests.HashedParity -import ComplexityTests.Hastad -import ComplexityTests.HastadSharp -import ComplexityTests.HessianSourceComplexity -import ComplexityTests.HierarchyTheorems -import ComplexityTests.Hypercontractivity -import ComplexityTests.InductiveCounting -import ComplexityTests.IntBinaryDecode -import ComplexityTests.IntBinaryDiv -import ComplexityTests.Interactive -import ComplexityTests.InteractiveProofs -import ComplexityTests.Isolation -import ComplexityTests.Iteration -import ComplexityTests.Iteration.Batch -import ComplexityTests.Iteration.Dynamics -import ComplexityTests.Iteration.SparseDisplacement -import ComplexityTests.Iteration.SparseTime -import ComplexityTests.IterationFoundations -import ComplexityTests.Kadin -import ComplexityTests.KahnKalaiLinialFriedgut -import ComplexityTests.Kannan -import ComplexityTests.KarpLipton -import ComplexityTests.KarpLipton2 -import ComplexityTests.KarpReductions -import ComplexityTests.KeyedSort -import ComplexityTests.KolmogorovCrypto -import ComplexityTests.KolmogorovTimeBounded -import ComplexityTests.Ladner -import ComplexityTests.LinearHash -import ComplexityTests.ListBasicImports -import ComplexityTests.ListEnumeration -import ComplexityTests.ListZipIdx -import ComplexityTests.LogSpace -import ComplexityTests.Logarithms -import ComplexityTests.MIP -import ComplexityTests.MachineClock -import ComplexityTests.MachineExtendTapes -import ComplexityTests.MachineIOBuffer -import ComplexityTests.MachinePrograms -import ComplexityTests.MachineSequential -import ComplexityTests.MachineStateMap -import ComplexityTests.ManyOne -import ComplexityTests.ManyOneKernel -import ComplexityTests.MassProduction -import ComplexityTests.MassProduction.Fine -import ComplexityTests.MassProduction.HighRate -import ComplexityTests.MassProduction.Menu -import ComplexityTests.MassProduction.Pipeline -import ComplexityTests.MassProduction.Scheduler -import ComplexityTests.MassProduction.Uhlig -import ComplexityTests.MathlibTM2 -import ComplexityTests.MathlibTM2Reverse -import ComplexityTests.MathlibTM2Space -import ComplexityTests.MemoizePPT -import ComplexityTests.ModularGap -import ComplexityTests.MonotoneCircuitValue -import ComplexityTests.MultiTapePolyTime -import ComplexityTests.NLComplement -import ComplexityTests.NPCompleteGraphs -import ComplexityTests.NPCompleteGraphs.Hamiltonian -import ComplexityTests.NPCompleteGraphs.TSP -import ComplexityTests.NPCompleteGraphs.Undirected -import ComplexityTests.NPCompleteNumbers -import ComplexityTests.NPCompleteness -import ComplexityTests.NPExistsAppend -import ComplexityTests.NPWitness -import ComplexityTests.NatBits -import ComplexityTests.NativeProducts -import ComplexityTests.NaturalProofs -import ComplexityTests.NegligibleSqrt -import ComplexityTests.NonVacuity -import ComplexityTests.NondeterministicVerifiers -import ComplexityTests.OneWayMetacomplexity -import ComplexityTests.OneWayNormalization -import ComplexityTests.OracleCircuits -import ComplexityTests.OracleComposition -import ComplexityTests.OracleComposition.Substitution -import ComplexityTests.OracleLowness -import ComplexityTests.OraclePPT -import ComplexityTests.OracleReplay -import ComplexityTests.OracleRepresentation -import ComplexityTests.OracleSemantics -import ComplexityTests.OracleSpecSum -import ComplexityTests.OrderedAddition -import ComplexityTests.OrderedBitSum -import ComplexityTests.OrderedComposition -import ComplexityTests.OrderedFOReduction -import ComplexityTests.OrderedFagin -import ComplexityTests.OrderedFirstOrder -import ComplexityTests.OrderedModelChecking -import ComplexityTests.OrderedMultiplication -import ComplexityTests.OrderedReduction -import ComplexityTests.OrderedSet -import ComplexityTests.OrderedSuccessor -import ComplexityTests.OrderedTupleBit -import ComplexityTests.OrderedTuples -import ComplexityTests.PCPAmplification -import ComplexityTests.PCPAmplifierIteration -import ComplexityTests.PCPApproximation -import ComplexityTests.PCPCompleteness -import ComplexityTests.PCPEncoded -import ComplexityTests.PCPEncodedAmplification -import ComplexityTests.PCPEncodedAmplificationIteration -import ComplexityTests.PCPEncodedArithmeticAmplification -import ComplexityTests.PCPEncodedAssignmentTester -import ComplexityTests.PCPEncodedComposition -import ComplexityTests.PCPEncodedCompositionEnumeration -import ComplexityTests.PCPEncodedConstraints -import ComplexityTests.PCPEncodedEnumeration -import ComplexityTests.PCPEncodedGap -import ComplexityTests.PCPEncodedGenericComposition -import ComplexityTests.PCPEncodedIteration -import ComplexityTests.PCPEncodedPreprocess -import ComplexityTests.PCPEncodedSize -import ComplexityTests.PCPEncodedThreeSAT -import ComplexityTests.PCPEncodedVerifier -import ComplexityTests.PCPExpander -import ComplexityTests.PCPGenericComposition -import ComplexityTests.PCPLocalTest -import ComplexityTests.PCPNP -import ComplexityTests.PCPNumbering -import ComplexityTests.PCPPreprocessPrograms -import ComplexityTests.PCPSelectedAssignmentTester -import ComplexityTests.PCPVerifierProbability -import ComplexityTests.PHClosure -import ComplexityTests.PPT -import ComplexityTests.PPTComposition -import ComplexityTests.PPTTactic -import ComplexityTests.PPTruthTable -import ComplexityTests.PRGStretch -import ComplexityTests.Parameterized -import ComplexityTests.PartialMCSP -import ComplexityTests.PlainAutomationSupport -import ComplexityTests.PlainCapturedMap -import ComplexityTests.PlainCleanPhase -import ComplexityTests.PlainIntMulOracleRun -import ComplexityTests.PlainLawfulBEq -import ComplexityTests.PlainPPTPreprocess -import ComplexityTests.PlainPurePPT -import ComplexityTests.PolySpaceFold -import ComplexityTests.PolyTimeBinaryWord -import ComplexityTests.PolyTimeContracts -import ComplexityTests.PolyTimeEncodedProjection -import ComplexityTests.PolyTimeMetadata -import ComplexityTests.PolyTimeMixes -import ComplexityTests.PolyTimePlain -import ComplexityTests.PolyTimePlainDriver -import ComplexityTests.PolyTimeScans -import ComplexityTests.PolyTimeSearch -import ComplexityTests.PolyTimeSum -import ComplexityTests.PolyTimeTactic -import ComplexityTests.PolynomialBound -import ComplexityTests.PolynomialClock -import ComplexityTests.PostTuringMachine -import ComplexityTests.Presample -import ComplexityTests.ProbabilisticComposition -import ComplexityTests.ProbabilisticSampling -import ComplexityTests.ProbabilityNotation -import ComplexityTests.ProbabilityToolkit -import ComplexityTests.ProbabilityToolkit2 -import ComplexityTests.ProbabilityToolkit3 -import ComplexityTests.ProgramCertificateDiagnostics -import ComplexityTests.Programs -import ComplexityTests.ProofComplexity -import ComplexityTests.ProofComplexity.Pigeonhole -import ComplexityTests.ProofComplexity.Resolution -import ComplexityTests.ProofComplexity.Tseitin -import ComplexityTests.Propagation -import ComplexityTests.PseudoentropyBoosting -import ComplexityTests.PseudoentropyExtraction -import ComplexityTests.PseudoentropyLearning -import ComplexityTests.PseudoentropyMasking -import ComplexityTests.PseudoentropySeed -import ComplexityTests.PseudoentropyThreeSource -import ComplexityTests.PseudoentropyTraining -import ComplexityTests.PseudorandomFunction -import ComplexityTests.PseudorandomObjects -import ComplexityTests.QBFProtocol -import ComplexityTests.Quantitative -import ComplexityTests.QuantitativeEncoding -import ComplexityTests.QueryComplexity -import ComplexityTests.QueryComplexity.Approximate -import ComplexityTests.QueryComplexity.Measures -import ComplexityTests.QueryComplexity.Randomized -import ComplexityTests.QueryComplexity.Sensitivity -import ComplexityTests.RAMInput -import ComplexityTests.Radix -import ComplexityTests.RandomOracle -import ComplexityTests.RandomizedDisjointness -import ComplexityTests.RationalHitting -import ComplexityTests.RationalHitting.Determinant -import ComplexityTests.RationalHitting.Encode -import ComplexityTests.RationalHitting.IntBinary -import ComplexityTests.RationalHitting.Lift -import ComplexityTests.RationalHitting.Parameters -import ComplexityTests.RationalHitting.Point -import ComplexityTests.RationalHitting.Runtime -import ComplexityTests.ReductionClasses -import ComplexityTests.Reingold -import ComplexityTests.RejectionSampling -import ComplexityTests.Relativization -import ComplexityTests.RelativizedCounting -import ComplexityTests.RepeatedTrials -import ComplexityTests.ResourceBoundsPlain -import ComplexityTests.ResourceClasses -import ComplexityTests.ResourceClasses2 -import ComplexityTests.ResourceClasses3 -import ComplexityTests.ResourceClasses4 -import ComplexityTests.RotationWalk -import ComplexityTests.Routing -import ComplexityTests.SATPolyTime -import ComplexityTests.SBPAmplification -import ComplexityTests.STCON -import ComplexityTests.SavedPrediction -import ComplexityTests.SearchTree -import ComplexityTests.SearchTreeErase -import ComplexityTests.SeedFixing -import ComplexityTests.SeededEvaluator -import ComplexityTests.SensitivitySeparation -import ComplexityTests.ShannonSynthesis -import ComplexityTests.SharpPLowness -import ComplexityTests.ShortWords -import ComplexityTests.SignQueries -import ComplexityTests.SipserLautemann -import ComplexityTests.SmallCountingClasses -import ComplexityTests.Smoke -import ComplexityTests.SortingTrace -import ComplexityTests.SourceComplexity -import ComplexityTests.Space -import ComplexityTests.Space.Machines -import ComplexityTests.Space.Savitch -import ComplexityTests.SpaceClasses -import ComplexityTests.SpaceHierarchy -import ComplexityTests.SparseLanguages -import ComplexityTests.SparseMemory -import ComplexityTests.StatefulRefinement -import ComplexityTests.SubbotovskayaAndreev -import ComplexityTests.Sumcheck -import ComplexityTests.SynthesisBuilder -import ComplexityTests.TFNP -import ComplexityTests.TFNPCompleteness -import ComplexityTests.TQBF -import ComplexityTests.TapePolyTime -import ComplexityTests.ThreeCNF -import ComplexityTests.ThreeCNFPolyTime -import ComplexityTests.ThresholdActivity -import ComplexityTests.ThresholdActivityLog -import ComplexityTests.ThresholdCapacity -import ComplexityTests.ThresholdCapacityCircuit -import ComplexityTests.ThresholdInnerProduct -import ComplexityTests.ThresholdInnerProductActivity -import ComplexityTests.ThresholdNC1 -import ComplexityTests.ThresholdRectangles -import ComplexityTests.ThresholdTranscript -import ComplexityTests.TimeHierarchy -import ComplexityTests.TimeReductions -import ComplexityTests.Toda -import ComplexityTests.TreeEval -import ComplexityTests.TreeEvalAry -import ComplexityTests.UnaryLength -import ComplexityTests.UniformCircuits -import ComplexityTests.UniformNat -import ComplexityTests.UniversalHash -import ComplexityTests.UniversalPolyTime -import ComplexityTests.UniversalResourceBound -import ComplexityTests.VanEmdeBoas -import ComplexityTests.VanEmdeBoasRAM -import ComplexityTests.VertexCoverKernel -import ComplexityTests.WPP -import ComplexityTests.WPPBounded -import ComplexityTests.WPPLowness -import ComplexityTests.WPPRobustness -import ComplexityTests.WPPTruthTable -import ComplexityTests.WPPTwoSided -import ComplexityTests.WaringCompilation -import ComplexityTests.WeightedThreshold -import ComplexityTests.WeightedThresholdBounds -import ComplexityTests.WordRAM -import ComplexityTests.WordRAMBasis -import ComplexityTests.WordRAMController -import ComplexityTests.WordRAMDigits -import ComplexityTests.WordRAMDynamic -import ComplexityTests.WordRAMFamilies -import ComplexityTests.WordRAMGeneric -import ComplexityTests.WordRAMMSB -import ComplexityTests.WordRAMMultiword -import ComplexityTests.WordRAMPrefixSums -import ComplexityTests.WordRAMQueue -import ComplexityTests.WordRAMRAM -import ComplexityTests.WorstCaseHardness -import ComplexityTests.ZooCountingHierarchy diff --git a/lakefile.toml b/lakefile.toml index 1c2605cef7..a986fad7d6 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -46,6 +46,8 @@ allowNonModules = true [[lean_lib]] name = "ComplexityTests" +roots = [] +globs = ["ComplexityTests.+"] leanOptions = {weak.linter.style.header = false} # The test files do not use the module system, but they import Mathlib, whose package sets # `requiresModuleSystem`. diff --git a/scripts/quality_report.py b/scripts/quality_report.py index e51f33a4c9..63fe5e80e4 100644 --- a/scripts/quality_report.py +++ b/scripts/quality_report.py @@ -46,6 +46,22 @@ from proof_lengths import masks, scan as scan_proofs # noqa: E402 ROOTS = ("Complexity", "ComplexityTests", "ComplexityAbstracts") +# Libraries that Lake builds from a glob (`lakefile.toml`) have no root aggregator file: their +# modules are exactly the source files under their directory. +GLOB_ROOTS = ("ComplexityTests",) + + +def glob_modules(root: str) -> list[str]: + """The modules of a glob-built library, from its source files.""" + return sorted(".".join(p.relative_to(ROOT).with_suffix("").parts) + for p in (ROOT / root).rglob("*.lean")) + + +def root_modules(glob=glob_modules) -> list[str]: + """Modules whose imports cover all three libraries: the aggregator roots and every module + of a glob-built library.""" + return [m for root in ROOTS + for m in (glob(root) if root in GLOB_ROOTS else [root])] # Documents outside module docstrings whose backquoted names count as intended API. EXTERNAL_DOCS = ("README.md", "abstracts/README.md") # The areas of #587: its table, completed by its assignment of the remaining paths @@ -411,13 +427,16 @@ def listed_modules(text: str) -> list[str]: return ROOT_IMPORT.findall(text) -def load_ileans(build_dir: Path, missing: list[str] | None = None) -> dict[str, dict]: +def load_ileans(build_dir: Path, missing: list[str] | None = None, + glob=glob_modules) -> dict[str, dict]: """The `.ilean` data of the modules the three libraries' roots import, by module name. A long-lived build directory keeps the outputs of modules that were since deleted or moved, and `lake build --no-build` does not notice them, so modules are found by following imports - from the roots rather than by listing files. Every root and every module they import must have - one; a missing file means the build is incomplete. The roots themselves are left out. + from the roots rather than by listing files. A glob-built library (`GLOB_ROOTS`) has no root + file, so its source files are the starting points instead. Every starting point and every + module they import must have one; a missing file means the build is incomplete. The aggregator + roots themselves are left out. Given a list `missing`, the build may be partial instead (for a tree that does not build completely): the modules are those the roots' source files import, and the ones without an @@ -425,14 +444,16 @@ def load_ileans(build_dir: Path, missing: list[str] | None = None) -> dict[str, if missing is not None: ileans = {} for root in ROOTS: - for module in listed_modules(source_path(root).read_text()): + modules = (glob(root) if root in GLOB_ROOTS + else listed_modules(source_path(root).read_text())) + for module in modules: path = build_dir / (module.replace(".", "/") + ".ilean") if path.is_file(): ileans[module] = json.loads(path.read_text()) else: missing.append(module) return ileans - ileans, todo = {}, [(root, None) for root in ROOTS] + ileans, todo = {}, [(module, None) for module in root_modules(glob)] while todo: module, importer = todo.pop() if module in ileans: @@ -445,7 +466,8 @@ def load_ileans(build_dir: Path, missing: list[str] | None = None) -> dict[str, todo.extend((i[0], module) for i in ileans[module]["directImports"] if i[0].split(".")[0] in ROOTS) for root in ROOTS: - del ileans[root] + if root not in GLOB_ROOTS: + del ileans[root] return ileans @@ -699,7 +721,8 @@ def tidy_usage_report(lib: Library, prefixes: tuple[str, ...] = TIDY_INTERNAL_PR keys = ("public_tidy_statements", "private_tidy_declarations", "local_tidy_fun_prop", "bridge_occurrences") source_hash = hashlib.sha256() - for path in [source_path(root) for root in ROOTS] + [p for _, p, _ in sources]: + for path in ([source_path(root) for root in ROOTS if root not in GLOB_ROOTS] + + [p for _, p, _ in sources]): source_hash.update(path.relative_to(ROOT).as_posix().encode() + b"\0") source_hash.update(path.read_bytes() + b"\0") provenance = {"revision": run(["git", "rev-parse", "HEAD"], capture_output=True).stdout.strip(), @@ -708,7 +731,7 @@ def tidy_usage_report(lib: Library, prefixes: tuple[str, ...] = TIDY_INTERNAL_PR capture_output=True).stdout.strip()), "source_dirty": bool(run(["git", "status", "--porcelain", "--", "Complexity", "ComplexityTests", "abstracts", "guide", - "Complexity.lean", "ComplexityTests.lean"], + "Complexity.lean"], capture_output=True).stdout.strip()), "scanned_source_sha256": source_hash.hexdigest(), "scanned_files": len(sources), "build_dir": str(lib.build_dir)} diff --git a/scripts/quick_check.py b/scripts/quick_check.py index fc456a8013..7769e0c824 100644 --- a/scripts/quick_check.py +++ b/scripts/quick_check.py @@ -69,10 +69,10 @@ def source_modules(root: Path) -> tuple[dict[str, str], set[str], set[str]]: physical_sources: set[Path] = set() aggregates: set[str] = set() roots: set[str] = set() - allowed = {"name", "srcDir", "leanOptions", "allowNonModules"} + allowed = {"name", "srcDir", "leanOptions", "allowNonModules", "roots", "globs"} for library in libraries: if not isinstance(library, dict) or set(library) - allowed: - raise FullCheck("custom Lake library roots/globs/options need full checks") + raise FullCheck("custom Lake library options need full checks") name = library.get("name", "") if not re.fullmatch(r"[A-Za-z_][A-Za-z_0-9]*(\.[A-Za-z_][A-Za-z_0-9]*)*", name): raise FullCheck("unsupported library name") @@ -82,15 +82,23 @@ def source_modules(root: Path) -> tuple[dict[str, str], set[str], set[str]]: relative = Path(*name.split(".")) aggregator = source / relative.with_suffix(".lean") directory = source / relative - if not aggregator.is_file() or not directory.is_dir(): + # The one supported glob layout: no roots and exactly the library's own submodules + # (`roots = []`, `globs = ["Name.+"]`), which Lake builds without an aggregator file. + globbed = "roots" in library or "globs" in library + if globbed and (library.get("roots") != [] or library.get("globs") != [f"{name}.+"]): + raise FullCheck("custom Lake library roots/globs need full checks") + if globbed and aggregator.exists(): + raise FullCheck(f"glob library {name} also has an aggregator file") + if (not globbed and not aggregator.is_file()) or not directory.is_dir(): raise FullCheck(f"missing library root {name}") # rglob does not descend through directory symlinks: reject them explicitly, # including the library root, before trusting the discovered import graph. if directory.is_symlink() or any(path.is_symlink() for path in directory.rglob("*")): raise FullCheck("symlinked source directories/files need full checks") roots.add(name) - aggregates.add(name) - for path in [aggregator, *sorted(directory.rglob("*.lean"))]: + if not globbed: + aggregates.add(name) + for path in [*([] if globbed else [aggregator]), *sorted(directory.rglob("*.lean"))]: if path.is_symlink() or not path.resolve().is_relative_to(source.resolve()): raise FullCheck("symlinked source file is outside quick-check scope") parts = path.relative_to(source).with_suffix("").parts diff --git a/scripts/test_quality_report.py b/scripts/test_quality_report.py index 63235188d8..e94909a4c8 100644 --- a/scripts/test_quality_report.py +++ b/scripts/test_quality_report.py @@ -212,23 +212,33 @@ def write_ileans(self, modules: dict[str, list[str]]) -> None: {"module": module, "directImports": [[i, False, False, False] for i in imports]})) def test_outputs_of_deleted_modules_are_ignored(self) -> None: - self.write_ileans({"Complexity": ["Complexity.A"], "ComplexityTests": [], - "ComplexityAbstracts": [], "Complexity.A": ["Mathlib.Init"], - "Complexity.Deleted": []}) - self.assertEqual(list(q.load_ileans(self.reference)), ["Complexity.A"]) + self.write_ileans({"Complexity": ["Complexity.A"], "ComplexityAbstracts": [], + "Complexity.A": ["Mathlib.Init"], "Complexity.Deleted": []}) + self.assertEqual(list(q.load_ileans(self.reference, glob=lambda root: [])), + ["Complexity.A"]) + + def test_glob_library_modules_are_read_from_sources(self) -> None: + self.write_ileans({"Complexity": [], "ComplexityAbstracts": [], + "ComplexityTests.T": ["Complexity.B"], "Complexity.B": [], + "ComplexityTests.Stale": []}) + glob = lambda root: ["ComplexityTests.T"] if root == "ComplexityTests" else [] + self.assertEqual(sorted(q.load_ileans(self.reference, glob=glob)), + ["Complexity.B", "ComplexityTests.T"]) + self.assertEqual(q.root_modules(glob), + ["Complexity", "ComplexityTests.T", "ComplexityAbstracts"]) def test_missing_reachable_output_is_refused(self) -> None: - self.write_ileans({"Complexity": ["Complexity.Live"], "ComplexityTests": [], - "ComplexityAbstracts": [], "Complexity.Live": ["Complexity.Missing"]}) + self.write_ileans({"Complexity": ["Complexity.Live"], "ComplexityAbstracts": [], + "Complexity.Live": ["Complexity.Missing"]}) with self.assertRaises(SystemExit) as error: - q.load_ileans(self.reference) + q.load_ileans(self.reference, glob=lambda root: []) self.assertIn("Missing.ilean is missing (imported by Complexity.Live)", str(error.exception.code)) def test_missing_root_output_is_refused(self) -> None: - self.write_ileans({"Complexity": [], "ComplexityTests": []}) + self.write_ileans({"Complexity": []}) with self.assertRaises(SystemExit) as error: - q.load_ileans(self.reference) + q.load_ileans(self.reference, glob=lambda root: []) self.assertIn("ComplexityAbstracts.ilean is missing (a root)", str(error.exception.code)) diff --git a/scripts/test_quick_check.py b/scripts/test_quick_check.py index 6cb66bf4e4..9dfcbfa968 100644 --- a/scripts/test_quick_check.py +++ b/scripts/test_quick_check.py @@ -64,6 +64,32 @@ def test_transitive_clients_and_clients_importing_aggregate(self): self.assertEqual(self.plan().targets, ["Demo.Base", "Demo.Middle", "DemoTests.AllClient", "DemoTests.Client"]) + def use_glob_test_library(self, globs='["DemoTests.+"]'): + """Switch the fixture's test library to the repository's glob layout: no aggregator.""" + self.write("lakefile.toml", 'name = "quickfixture"\n[[lean_lib]]\nname = "Demo"\n' + f'[[lean_lib]]\nname = "DemoTests"\nroots = []\nglobs = {globs}\n') + (self.root / "DemoTests.lean").unlink() + self.commit() + self.git("update-ref", "refs/remotes/origin/main", "HEAD") + + def test_glob_test_library_plans_affected_tests(self): + self.use_glob_test_library() + self.write("Demo/Base.lean", "def value : Nat := 2\n") + self.assertEqual(self.plan().targets, + ["Demo.Base", "Demo.Middle", "DemoTests.AllClient", "DemoTests.Client"]) + + def test_other_glob_layouts_fall_back(self): + self.use_glob_test_library('["DemoTests.*"]') + self.write("Demo/Base.lean", "def value : Nat := 2\n") + with self.assertRaises(quick.FullCheck): + self.plan() + + def test_glob_library_with_aggregator_falls_back(self): + self.use_glob_test_library() + self.write("DemoTests.lean", "import DemoTests.Client\n") + with self.assertRaises(quick.FullCheck): + self.plan() + def test_test_helper_and_diamond(self): self.write("DemoTests/Helper.lean", "import Demo.Middle\n") self.write("DemoTests/Client.lean", "import Demo.Base\nimport DemoTests.Helper\n") diff --git a/scripts/tidy_sweep.py b/scripts/tidy_sweep.py index 9e464c0ac7..8343ee4339 100644 --- a/scripts/tidy_sweep.py +++ b/scripts/tidy_sweep.py @@ -374,7 +374,7 @@ def __init__(self, build_dir: Path, allowlist: set[str], partial: bool = False, qr.collect_references(self.lib, self.decls, self.owners) qr.classify(self.decls) self.allowlist = allowlist - roots = sorted(self.lib.ileans) if partial else qr.ROOTS + roots = sorted(self.lib.ileans) if partial else qr.root_modules() out = qr.run(["lake", "env", "lean", "--run", "scripts/QualityReport.lean", "--names", *roots], capture_output=True).stdout names, _, tokens = out.partition("\n--tokens--\n")