Login

Verification run

Run 5

promachina/iut-lean branch master triggered via poller
failed commit eef13c1baa02 toolchain lean-v4-30-0 prover lean took 1h 59m · finished 6w ago

lake build :blueprint failed with exit code 1 (toolchain lean-v4-30-0, command: elan run leanprover/lean4:v4.30.0 -- lake build :blueprint)

Open project

Package inputs

This verification run did not include a theorem package lock. Its inputs depend only on repository, toolchain, image, and command inputs.

Trust verification

Recomputes trust checks from the recorded attestations, manifest, and command history.

(verification not run)

Manifest

Loads the published files manifest and location metadata for this job.

(manifest not loaded)

Verifier log excerpt

(no log excerpt)

Command runs

git_clone exit 0 duration 2s · created 
git clone --depth 1 --branch master --single-branch https://github.com/promachina/iut-lean.git /var/lib/apodeixis/repos/job-17-source
Cloning into '/var/lib/apodeixis/repos/job-17-source'...
git_checkout exit 0 duration 113 ms · created 
git checkout eef13c1baa0219ba8141b18917dffae8c6e07758
Note: switching to 'eef13c1baa0219ba8141b18917dffae8c6e07758'.

You are in 'detached HEAD' state. You can look around, make experimental
changes and commit them, and you can discard any commits you make in this
state without impacting any branches by switching back to a branch.

If you want to create a new branch to retain commits you create, you may
do so (now or later) by using -c with the switch command. Example:

  git switch -c <new-branch-name>

Or undo this operation with:

  git switch -

Turn off this advice by setting config variable advice.detachedHead to false

HEAD is now at eef13c1 Derive source chart calibration
lake_cache exit 1 duration 46s · created 
lake exe cache get
info: mathlib: cloning https://github.com/leanprover-community/mathlib4
info: mathlib: checking out revision 'c5ea00351c28e24afc9f0f84379aa41082b1188f'
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision 'a456461b368b71d2accd95234832cd9c174b5437'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient
info: LeanSearchClient: checking out revision 'c5d5b8fe6e5158def25cd28eb94e4141ad97c843'
info: importGraph: cloning https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision '515cf9d0c00ece5e661f6de4326a53dedc1e8ea1'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision 'a84b3e2475d5c5ab979567b1ad8aea21b764bcf8'
info: aesop: cloning https://github.com/leanprover-community/aesop
info: aesop: checking out revision '558915ae105bfd8074e22d597613d1961822adc2'
info: Qq: cloning https://github.com/leanprover-community/quote4
info: Qq: checking out revision 'a6e6c34c4ef182f83b219a3a5a385f51f44bdc4c'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision '32dc18cde3684679f3c003de608743b57498c56f'
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision '6b907cf12b2e445ccb7c24bc208ef04a1f39e84c'
✔ [3/25] Built Cache.Init (320ms)
✔ [4/25] Built Cache.Lean (455ms)
✔ [5/25] Built Cache.Init:c.o (74ms)
✔ [6/25] Built Cache.Lean:c.o (133ms)
✔ [14/25] Built Batteries.Data.String.Basic:c.o (99ms)
✔ [15/25] Built Batteries.Data.Array.Match:c.o (188ms)
✔ [16/25] Built Batteries.Data.String.Matcher:c.o (172ms)
✔ [17/25] Built Cache.IO (1.5s)
✖ [18/25] Building Cache.Hashing (420ms)
trace: .> LEAN_PATH=/apx/source/.lake/packages/Cli/.lake/build/lib/lean:/apx/source/.lake/packages/batteries/.lake/build/lib/lean:/apx/source/.lake/packages/Qq/.lake/build/lib/lean:/apx/source/.lake/packages/aesop/.lake/build/lib/lean:/apx/source/.lake/packages/proofwidgets/.lake/build/lib/lean:/apx/source/.lake/packages/importGraph/.lake/build/lib/lean:/apx/source/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/apx/source/.lake/packages/plausible/.lake/build/lib/lean:/apx/source/.lake/packages/mathlib/.lake/build/lib/lean:/apx/source/.lake/build/lib/lean /apx/elan/toolchains/leanprover--lean4---v4.30.0/bin/lean /apx/source/.lake/packages/mathlib/Cache/Hashing.lean -o /apx/source/.lake/packages/mathlib/.lake/build/lib/lean/Cache/Hashing.olean -i /apx/source/.lake/packages/mathlib/.lake/build/lib/lean/Cache/Hashing.ilean -c /apx/source/.lake/packages/mathlib/.lake/build/ir/Cache/Hashing.c --setup /apx/source/.lake/packages/mathlib/.lake/build/ir/Cache/Hashing.setup.json --json
error: Cache/Hashing.lean:7:0: leantar not found in Lean sysroot. This toolchain may predate nightly-2026-03-09.
error: Lean exited with code 1
✔ [24/25] Built Cache.IO:c.o (1.1s)
Some required targets logged failures:
- Cache.Hashing
error: build failed
lean_checker exit 0 duration 46m 30s · created 
lake build
ilt Mathlib.Analysis.Calculus.FDeriv.Basic (13s)
✔ [2453/2504] Built Mathlib.Algebra.Algebra.IsSimpleRing (1.0s)
✔ [2454/2504] Built Mathlib.Algebra.BigOperators.Balance (1.4s)
✔ [2455/2504] Built Mathlib.Analysis.Normed.Operator.Bilinear (18s)
✔ [2456/2504] Built Mathlib.Analysis.Complex.Norm (3.0s)
✔ [2457/2507] Built Mathlib.Analysis.Calculus.FDeriv.RestrictScalars (3.0s)
✔ [2458/2507] Built Mathlib.Algebra.Order.Module.Rat (1.6s)
✔ [2459/2507] Built Mathlib.Analysis.Calculus.FDeriv.Congr (4.2s)
✔ [2460/2507] Built Mathlib.Analysis.Calculus.FDeriv.Comp (6.2s)
✔ [2461/2507] Built Mathlib.Analysis.Complex.Order (2.6s)
✔ [2462/2508] Built Mathlib.Algebra.Order.Group.Opposite (1.6s)
✔ [2463/2508] Built Mathlib.Algebra.Star.StarProjection (2.2s)
✔ [2464/2508] Built Mathlib.Analysis.Normed.Operator.NormedSpace (7.4s)
✔ [2465/2509] Built Mathlib.Algebra.Order.BigOperators.Expect (4.6s)
✔ [2466/2509] Built Mathlib.Analysis.Calculus.FDeriv.Const (4.7s)
✔ [2467/2509] Built Mathlib.Analysis.Normed.Module.Completion (2.9s)
✔ [2468/2509] Built Mathlib.Algebra.Order.Star.Basic (4.7s)
✔ [2469/2509] Built Mathlib.Analysis.Normed.Group.Hom (6.4s)
✔ [2470/2514] Built Mathlib.Algebra.Star.Pi (1.2s)
✔ [2471/2514] Built Mathlib.Algebra.Star.Pointwise (1.6s)
✔ [2472/2515] Built Mathlib.Algebra.Star.Prod (1.4s)
✔ [2473/2517] Built Mathlib.Algebra.Star.Center (1.4s)
✔ [2474/2518] Built Mathlib.Analysis.Normed.Operator.Mul (7.8s)
✔ [2475/2518] Built Mathlib.Algebra.Algebra.Spectrum.Basic (5.3s)
✔ [2476/2520] Built Mathlib.Analysis.Calculus.Deriv.Basic (11s)
✔ [2477/2522] Built Mathlib.Data.Real.Star (1.2s)
✔ [2478/2522] Built Mathlib.Algebra.Star.MonoidHom (2.4s)
✔ [2479/2522] Built Mathlib.Analysis.Normed.Module.Multilinear.Basic (27s)
✔ [2480/2523] Built Mathlib.Analysis.Calculus.Deriv.Support (1.7s)
✔ [2481/2523] Built Mathlib.Topology.Algebra.Module.Star (2.5s)
✔ [2482/2523] Built Mathlib.Analysis.Normed.Ring.Finite (1.5s)
✔ [2483/2523] Built Mathlib.Analysis.Calculus.Deriv.Comp (9.3s)
✔ [2484/2523] Built Mathlib.Algebra.Star.Unitary (5.0s)
✔ [2485/2523] Built Mathlib.Algebra.Star.NonUnitalSubalgebra (22s)
✔ [2486/2527] Built Mathlib.Analysis.Normed.Module.Alternating.Basic (14s)
✔ [2487/2527] Built Mathlib.Data.Complex.BigOperators (1.6s)
✔ [2488/2529] Built Mathlib.Analysis.Normed.Operator.BoundedLinearMaps (9.9s)
✔ [2489/2529] Built Mathlib.Algebra.CharP.Invertible (1.5s)
✔ [2490/2529] Built Mathlib.Topology.Instances.RealVectorSpace (2.0s)
✔ [2491/2529] Built Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle (1.1s)
✔ [2492/2533] Built Mathlib.Analysis.Calculus.FDeriv.Linear (2.8s)
✔ [2493/2533] Built Mathlib.Analysis.Normed.Module.Multilinear.Curry (18s)
✔ [2494/2533] Built Mathlib.Algebra.Star.Subalgebra (11s)
✔ [2495/2533] Built Mathlib.LinearAlgebra.Complex.Module (8.3s)
✔ [2496/2533] Built Mathlib.Algebra.CharZero.Infinite (1.3s)
✔ [2497/2533] Built Mathlib.SetTheory.Cardinal.Continuum (1.5s)
✔ [2498/2533] Built Mathlib.Analysis.CStarAlgebra.Basic (3.8s)
✔ [2499/2536] Built Mathlib.Data.Rat.Cardinal (1.1s)
✔ [2500/2536] Built Mathlib.Analysis.Calculus.FormalMultilinearSeries (9.0s)
✔ [2501/2536] Built Mathlib.Analysis.Real.Cardinality (2.7s)
✔ [2502/2536] Built Mathlib.Analysis.Calculus.FDeriv.Prod (21s)
✔ [2503/2536] Built Mathlib.Order.Filter.Subsingleton (1.5s)
✔ [2504/2536] Built Mathlib.Analysis.Calculus.FDeriv.Add (17s)
✔ [2505/2536] Built Mathlib.Order.Filter.EventuallyConst (1.5s)
✔ [2506/2536] Built Mathlib.Analysis.Calculus.FDeriv.Bilinear (4.9s)
✔ [2507/2537] Built Mathlib.Analysis.RCLike.Basic (13s)
✔ [2508/2537] Built Mathlib.Analysis.Calculus.Deriv.Add (6.3s)
✔ [2509/2538] Built Mathlib.Analysis.Analytic.ConvergenceRadius (11s)
✔ [2510/2538] Built Mathlib.Algebra.Field.NegOnePow (1.4s)
✔ [2511/2539] Built Mathlib.Analysis.Complex.Basic (8.3s)
✔ [2512/2539] Built Mathlib.Analysis.Calculus.Deriv.Slope (4.4s)
✔ [2513/2539] Built Mathlib.Analysis.Calculus.FDeriv.Equiv (12s)
✔ [2514/2539] Built Mathlib.Algebra.Field.Periodic (2.3s)
✔ [2515/2539] Built Mathlib.Analysis.Analytic.OfScalars (5.0s)
✔ [2516/2540] Built Mathlib.Analysis.Complex.ReImTopology (2.4s)
✔ [2517/2540] Built Mathlib.Algebra.QuadraticDiscriminant (2.3s)
✔ [2518/2544] Built Mathlib.Analysis.Complex.Asymptotics (1.0s)
✔ [2519/2547] Built Mathlib.Analysis.Calculus.FDeriv.CompCLM (20s)
✔ [2520/2547] Built Mathlib.Tactic.NormNum.NatFactorial (2.1s)
✔ [2521/2548] Built Mathlib.Algebra.Order.CauSeq.BigOperators (5.4s)
✔ [2522/2549] Built Mathlib.Analysis.Complex.Exponential (8.4s)
✔ [2523/2549] Built Mathlib.Topology.Order.AtTopBotIxx (12s)
✔ [2524/2549] Built Mathlib.Analysis.Analytic.Basic (25s)
✔ [2525/2549] Built Mathlib.Analysis.Complex.Trigonometric (6.7s)
✔ [2526/2549] Built Mathlib.Analysis.Normed.Group.Quotient (7.2s)
✔ [2527/2551] Built Mathlib.Analysis.Normed.Module.Ball.Pointwise (5.9s)
✔ [2528/2552] Built Mathlib.Data.Int.SuccPred (1.5s)
✔ [2529/2554] Built Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries (28s)
✔ [2530/2556] Built Mathlib.Analysis.SpecialFunctions.Exp (3.9s)
✔ [2531/2556] Built Mathlib.Order.Circular (1.6s)
✔ [2532/2556] Built Mathlib.GroupTheory.QuotientGroup.ModEq (1.5s)
✔ [2533/2561] Built Mathlib.Algebra.Order.Interval.Set.Group (2.6s)
✔ [2534/2561] Built Mathlib.GroupTheory.Divisible (2.5s)
✔ [2535/2562] Built Mathlib.Analysis.Analytic.ChangeOrigin (8.7s)
✔ [2536/2562] Built Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas (2.2s)
✔ [2537/2564] Built Mathlib.Algebra.CharZero.Quotient (1.9s)
✔ [2538/2566] Built Mathlib.Topology.Instances.Sign (1.9s)
✔ [2539/2566] Built Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic (8.9s)
✔ [2540/2569] Built Mathlib.Topology.Instances.ZMultiples (1.7s)
✔ [2541/2569] Built Mathlib.Algebra.Order.Ring.Interval (1.4s)
✔ [2542/2576] Built Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse (4.6s)
✔ [2543/2576] Built Mathlib.Analysis.SpecialFunctions.Log.Basic (6.3s)
✔ [2544/2580] Built Mathlib.Algebra.Order.ToIntervalMod (15s)
✔ [2545/2580] Built Mathlib.Analysis.Calculus.Deriv.Linear (2.6s)
✔ [2546/2582] Built Mathlib.Analysis.Analytic.CPolynomialDef (12s)
✔ [2547/2582] Built Mathlib.Analysis.Normed.Group.AddTorsor (2.4s)
✔ [2548/2582] Built Mathlib.Analysis.Calculus.Deriv.AffineMap (2.4s)
✔ [2549/2582] Built Mathlib.Topology.Sets.Closeds (3.4s)
✔ [2550/2588] Built Mathlib.Topology.LocallyConstant.Basic (3.1s)
✔ [2551/2592] Built Mathlib.Analysis.Analytic.Linear (6.2s)
✔ [2552/2594] Built Mathlib.Topology.Instances.AddCircle.Defs (9.0s)
✔ [2553/2594] Built Mathlib.Topology.OpenPartialHomeomorph.IsImage (3.1s)
✔ [2554/2595] Built Mathlib.Analysis.Calculus.FDeriv.OfCompLeft (5.1s)
✔ [2555/2595] Built Mathlib.Topology.Instances.AddCircle.Real (1.9s)
✔ [2556/2600] Built Mathlib.Analysis.Calculus.Deriv.Inverse (3.3s)
✔ [2557/2600] Built Mathlib.Topology.Algebra.ContinuousAffineMap (11s)
✔ [2558/2600] Built Mathlib.Analysis.Analytic.Composition (16s)
✔ [2559/2601] Built Mathlib.Algebra.Algebra.TransferInstance (1.5s)
✔ [2560/2601] Built Mathlib.Analysis.Normed.Group.AddCircle (3.9s)
✔ [2561/2601] Built Mathlib.Topology.MetricSpace.CauSeqFilter (1.5s)
✔ [2562/2601] Built Mathlib.Analysis.Calculus.FDeriv.Affine (2.1s)
✔ [2563/2601] Built Mathlib.Analysis.Calculus.LocalExtr.Basic (4.2s)
✔ [2564/2607] Built Mathlib.Analysis.Normed.Algebra.Exponential (7.9s)
✔ [2565/2607] Built Mathlib.Topology.ExtendFrom (2.2s)
✔ [2566/2607] Built Mathlib.Topology.Order.ExtendFrom (2.2s)
✔ [2567/2608] Built Mathlib.Analysis.Analytic.Inverse (13s)
✔ [2568/2611] Built Mathlib.Topology.Order.Rolle (2.4s)
✔ [2569/2611] Built Mathlib.Analysis.Normed.Group.Lemmas (2.4s)
✔ [2570/2611] Built Mathlib.Analysis.Calculus.LocalExtr.Rolle (1.9s)
✔ [2571/2614] Built Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle (11s)
✔ [2572/2614] Built Mathlib.Topology.Algebra.AffineSubspace (1.8s)
✔ [2573/2615] Built Mathlib.Analysis.Normed.Module.RCLike.Basic (3.4s)
✔ [2574/2615] Built Mathlib.Topology.Algebra.Module.Determinant (2.1s)
✔ [2575/2615] Built Mathlib.Analysis.SpecialFunctions.Complex.Arg (5.8s)
✔ [2576/2616] Built Mathlib.Topology.Algebra.ContinuousAffineEquiv (6.0s)
✔ [2577/2616] Built Mathlib.Analysis.Normed.Module.RieszLemma (2.6s)
✔ [2578/2617] Built Mathlib.Analysis.SpecialFunctions.Complex.Log (3.2s)
✔ [2579/2617] Built Mathlib.Order.Atoms.Finite (1.4s)
✔ [2580/2617] Built Mathlib.Topology.Algebra.Module.ModuleTopology (5.2s)
✔ [2581/2622] Built Mathlib.Analysis.Analytic.Constructions (29s)
✔ [2582/2622] Built Mathlib.Order.CompactlyGenerated.Intervals (1.6s)
✔ [2583/2622] Built Mathlib.Analysis.SpecialFunctions.Complex.CircleMap (2.5s)
✔ [2584/2622] Built Mathlib.Analysis.Analytic.Within (2.7s)
✔ [2585/2625] Built Mathlib.Analysis.Analytic.Uniqueness (3.9s)
✔ [2586/2626] Built Mathlib.Control.Bifunctor (1.6s)
✔ [2587/2626] Built Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Quotient (1.9s)
✔ [2588/2626] Built Mathlib.Logic.Equiv.Functor (1.1s)
✔ [2589/2626] Built Mathlib.Analysis.Normed.Affine.Isometry (12s)
✔ [2590/2630] Built Mathlib.Topology.Algebra.SeparationQuotient.FiniteDimensional (1.2s)
✔ [2591/2632] Built Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent (5.3s)
✔ [2592/2632] Built Mathlib.Topology.Homeomorph.Quotient (1.4s)
✔ [2593/2632] Built Mathlib.Order.JordanHolder (3.7s)
✔ [2594/2632] Built Mathlib.Analysis.Analytic.CPolynomial (11s)
✔ [2595/2632] Built Mathlib.Topology.Instances.Matrix (3.5s)
✔ [2596/2632] Built Mathlib.Topology.Maps.Strict.Basic (1.4s)
✔ [2597/2634] Built Mathlib.LinearAlgebra.Dimension.LinearMap (2.5s)
✔ [2598/2634] Built Mathlib.Topology.Algebra.Module.Complement (5.2s)
✔ [2599/2638] Built Mathlib.Data.Finset.Update (1.7s)
✔ [2600/2642] Built Mathlib.Tactic.Measurability.Init (843ms)
✔ [2601/2642] Built Mathlib.Data.Prod.TProd (1.6s)
✔ [2602/2643] Built Mathlib.Tactic.Measurability (1.1s)
✔ [2603/2648] Built Mathlib.GroupTheory.GroupAction.IterateAct (855ms)
✔ [2604/2652] Built Mathlib.MeasureTheory.OuterMeasure.Defs (1.4s)
✔ [2605/2656] Built Mathlib.MeasureTheory.MeasurableSpace.Defs (2.6s)
✔ [2606/2660] Built Mathlib.RingTheory.SimpleModule.Basic (7.9s)
✔ [2607/2660] Built Mathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable (1.3s)
✔ [2608/2660] Built Mathlib.MeasureTheory.OuterMeasure.Basic (2.8s)
✔ [2609/2667] Built Mathlib.Data.Set.Dissipate (1.9s)
✔ [2610/2667] Built Mathlib.MeasureTheory.MeasurableSpace.Instances (1.4s)
✔ [2611/2667] Built Mathlib.Topology.Algebra.Module.Simple (1.7s)
✔ [2612/2667] Built Mathlib.MeasureTheory.MeasurableSpace.Basic (2.2s)
✔ [2613/2667] Built Mathlib.Order.Interval.Set.Monotone (2.0s)
✔ [2614/2668] Built Mathlib.MeasureTheory.OuterMeasure.AE (3.1s)
✔ [2615/2672] Built Mathlib.MeasureTheory.OuterMeasure.Operations (3.9s)
✔ [2616/2672] Built Mathlib.MeasureTheory.PiSystem (3.9s)
✔ [2617/2672] Built Mathlib.MeasureTheory.OuterMeasure.BorelCantelli (3.2s)
✔ [2618/2672] Built Mathlib.MeasureTheory.MeasurableSpace.Constructions (5.0s)
✔ [2619/2672] Built Mathlib.Data.Set.MemPartition (1.6s)
✔ [2620/2676] Built Mathlib.Order.Filter.CountableSeparatingOn (1.9s)
✔ [2621/2676] Built Mathlib.MeasureTheory.OuterMeasure.OfFunction (3.4s)
✔ [2622/2676] Built Mathlib.Analysis.Calculus.FDeriv.Analytic (22s)
✔ [2623/2676] Built Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated (2.0s)
✔ [2624/2676] Built Mathlib.Topology.Separation.GDelta (1.6s)
✔ [2625/2676] Built Mathlib.MeasureTheory.OuterMeasure.Caratheodory (2.6s)
✔ [2626/2676] Built Mathlib.MeasureTheory.MeasurableSpace.Embedding (5.3s)
✔ [2627/2676] Built Mathlib.Topology.Algebra.Module.FiniteDimension (15s)
✔ [2628/2676] Built Mathlib.Analysis.SpecialFunctions.Exponential (6.6s)
✔ [2629/2676] Built Mathlib.Topology.GDelta.MetrizableSpace (1.5s)
✔ [2630/2676] Built Mathlib.MeasureTheory.OuterMeasure.Induced (3.5s)
✔ [2631/2676] Built Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated (2.7s)
✔ [2632/2677] Built Mathlib.Analysis.Calculus.ContDiff.Defs (23s)
✔ [2633/2677] Built Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (22s)
✔ [2634/2680] Built Mathlib.MeasureTheory.Measure.MeasureSpaceDef (3.7s)
✔ [2635/2680] Built Mathlib.MeasureTheory.Function.AEMeasurableSequence (1.9s)
✔ [2636/2683] Built Mathlib.Analysis.Normed.Module.FiniteDimension (10s)
✔ [2637/2687] Built Mathlib.MeasureTheory.MeasurableSpace.Prod (1.6s)
✔ [2638/2693] Built Mathlib.MeasureTheory.Measure.AEDisjoint (1.9s)
✔ [2639/2693] Built Mathlib.Topology.Metrizable.Real (1.3s)
✔ [2640/2695] Built Mathlib.MeasureTheory.Measure.NullMeasurable (4.4s)
✔ [2641/2695] Built Mathlib.Algebra.Order.Monoid.Canonical.Basic (5.8s)
✔ [2642/2695] Built Mathlib.Analysis.Calculus.FDeriv.Mul (35s)
✔ [2643/2695] Built Mathlib.Topology.IndicatorConstPointwise (1.6s)
✔ [2644/2695] Built Mathlib.Analysis.Calculus.ContDiff.Basic (14s)
✔ [2645/2695] Built Mathlib.Topology.Algebra.Module.Spaces.WeakBilin (2.9s)
✔ [2646/2695] Built Mathlib.Topology.Instances.Real.Lemmas (2.0s)
✔ [2647/2695] Built Mathlib.Analysis.Calculus.DSlope (3.1s)
✔ [2648/2697] Built Mathlib.Analysis.Calculus.DiffContOnCl (3.5s)
✔ [2649/2697] Built Mathlib.MeasureTheory.Measure.MeasureSpace (7.0s)
✔ [2650/2697] Built Mathlib.Analysis.LocallyConvex.Polar (4.3s)
✔ [2651/2697] Built Mathlib.Analysis.Calculus.FDeriv.Pow (7.7s)
✔ [2652/2701] Built Mathlib.Analysis.Calculus.ContDiff.Comp (12s)
✔ [2653/2701] Built Mathlib.Geometry.Convex.Cone.Basic (7.1s)
✔ [2654/2701] Built Mathlib.Analysis.Analytic.IsolatedZeros (7.8s)
✔ [2655/2701] Built Mathlib.Analysis.Calculus.Deriv.Mul (17s)
✔ [2656/2701] Built Mathlib.MeasureTheory.Measure.Map (2.0s)
✔ [2657/2701] Built Mathlib.Analysis.Convex.Cone.Extension (3.0s)
✔ [2658/2701] Built Mathlib.Analysis.Calculus.Deriv.Pow (3.4s)
✔ [2659/2703] Built Mathlib.Analysis.Calculus.ContDiff.Deriv (3.2s)
✔ [2660/2703] Built Mathlib.Analysis.RCLike.Lemmas (3.1s)
✔ [2661/2703] Built Mathlib.Analysis.RCLike.Extend (5.1s)
✔ [2662/2703] Built Mathlib.Analysis.Calculus.Deriv.CompMul (2.3s)
✔ [2663/2703] Built Mathlib.Analysis.Calculus.Deriv.MeanValue (3.9s)
✔ [2664/2703] Built Mathlib.MeasureTheory.Measure.AbsolutelyContinuous (2.5s)
✔ [2665/2703] Built Mathlib.Analysis.Calculus.Deriv.Inv (4.0s)
✔ [2666/2703] Built Mathlib.Analysis.Calculus.MeanValue (8.3s)
✔ [2667/2703] Built Mathlib.Analysis.Calculus.Deriv.Polynomial (3.7s)
✔ [2668/2703] Built Mathlib.Analysis.Convex.TotallyBounded (1.9s)
✔ [2669/2703] Built Mathlib.Analysis.Calculus.IteratedDeriv.Defs (4.3s)
✔ [2670/2705] Built Mathlib.Analysis.Normed.Module.RCLike.Extend (2.6s)
✔ [2671/2705] Built Mathlib.Analysis.Calculus.Deriv.Shift (2.4s)
✔ [2672/2705] Built Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving (2.4s)
✔ [2673/2705] Built Mathlib.Analysis.LocallyConvex.AbsConvex (3.2s)
✔ [2674/2709] Built Mathlib.Analysis.Calculus.ContDiff.RCLike (3.7s)
✔ [2675/2709] Built Mathlib.Algebra.Central.Defs (1.3s)
✔ [2676/2709] Built Mathlib.Analysis.Normed.Module.HahnBanach (4.4s)
✔ [2677/2709] Built Mathlib.MeasureTheory.Measure.Comap (2.6s)
✔ [2678/2710] Built Mathlib.Analysis.Calculus.Deriv.ZPow (3.9s)
✔ [2679/2710] Built Mathlib.Algebra.Central.Basic (2.2s)
✔ [2680/2710] Built Mathlib.Analysis.Calculus.ContDiff.Operations (26s)
✔ [2681/2710] Built Mathlib.Analysis.Convex.Gauge (7.5s)
✔ [2682/2710] Built Mathlib.Analysis.Calculus.LogDeriv (5.1s)
✔ [2683/2710] Built Mathlib.MeasureTheory.Measure.Restrict (7.4s)
✔ [2684/2710] Built Mathlib.Combinatorics.Enumerative.InclusionExclusion (4.4s)
✔ [2685/2710] Built Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms (1.0s)
✔ [2686/2723] Built Mathlib.Analysis.Complex.RealDeriv (3.3s)
✔ [2687/2725] Built Mathlib.MeasureTheory.Measure.MutuallySingular (2.8s)
✔ [2688/2725] Built Mathlib.Analysis.LocallyConvex.Separation (6.8s)
✔ [2689/2725] Built Mathlib.MeasureTheory.Measure.Typeclasses.Finite (4.9s)
✔ [2690/2725] Built Mathlib.MeasureTheory.Group.Defs (2.0s)
✔ [2691/2727] Built Mathlib.MeasureTheory.Measure.Typeclasses.Probability (2.2s)
✔ [2692/2732] Built Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (4.6s)
✔ [2693/2732] Built Mathlib.Analysis.Normed.Group.FunctionSeries (3.1s)
✔ [2694/2732] Built Mathlib.Analysis.LocallyConvex.SeparatingDual (7.8s)
✔ [2695/2732] Built Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (2.5s)
✔ [2696/2735] Built Mathlib.MeasureTheory.Measure.Dirac (3.7s)
✔ [2697/2736] Built Mathlib.MeasureTheory.Measure.Trim (2.0s)
✔ [2698/2736] Built Mathlib.Topology.MetricSpace.Gluing (3.5s)
✔ [2699/2736] Built Mathlib.Analysis.Normed.Module.Dual (3.8s)
✔ [2700/2739] Built Mathlib.MeasureTheory.Measure.Count (2.7s)
✔ [2701/2739] Built Mathlib.Topology.Separation.CountableSeparatingOn (1.4s)
✔ [2702/2739] Built Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (23s)
✔ [2703/2739] Built Mathlib.Topology.MetricSpace.PiNat (6.4s)
✔ [2704/2739] Built Mathlib.Topology.Metrizable.CompletelyMetrizable (2.0s)
✔ [2705/2739] Built Mathlib.MeasureTheory.Measure.Doubling (2.0s)
✔ [2706/2740] Built Mathlib.MeasureTheory.Measure.AEMeasurable (2.0s)
✔ [2707/2740] Built Mathlib.Topology.MetricSpace.CantorScheme (1.9s)
✔ [2708/2740] Built Mathlib.Dynamics.Ergodic.MeasurePreserving (2.2s)
✔ [2709/2740] Built Mathlib.Topology.MetricSpace.Polish (2.5s)
✔ [2710/2741] Built Mathlib.Analysis.SpecialFunctions.ExpDeriv (4.3s)
✔ [2711/2742] Built Mathlib.MeasureTheory.Order.Lattice (2.1s)
✔ [2712/2742] Built Mathlib.Topology.MetricSpace.Perfect (1.7s)
✔ [2713/2748] Built Mathlib.Dynamics.Minimal (1.6s)
✔ [2714/2756] Built Mathlib.Topology.ContinuousMap.CocompactMap (2.2s)
✔ [2715/2756] Built Mathlib.MeasureTheory.Group.Arithmetic (7.0s)
✔ [2716/2761] Built Mathlib.GroupTheory.Complement (7.1s)
✔ [2717/2761] Built Mathlib.Data.Nat.NthRoot.Defs (461ms)
✔ [2718/2761] Built Mathlib.MeasureTheory.Group.Pointwise (1.8s)
✔ [2719/2761] Built Mathlib.Analysis.SpecialFunctions.Pow.Complex (3.2s)
✔ [2720/2761] Built Mathlib.Analysis.SpecialFunctions.Log.Deriv (8.1s)
✔ [2721/2761] Built Mathlib.Tactic.Qify (1.1s)
✔ [2722/2762] Built Mathlib.Tactic.Rify (1.5s)
✔ [2723/2766] Built Mathlib.MeasureTheory.Group.MeasurableEquiv (4.7s)
✔ [2724/2766] Built Mathlib.MeasureTheory.Constructions.BorelSpace.Basic (4.8s)
✔ [2725/2766] Built Mathlib.Topology.Compactness.CompactlyCoherentSpace (2.0s)
✔ [2726/2766] Built Mathlib.Analysis.SpecialFunctions.Pow.Real (6.7s)
✔ [2727/2766] Built Mathlib.Order.Filter.Germ.Basic (5.9s)
✔ [2728/2766] Built Mathlib.MeasureTheory.Measure.Regular (5.5s)
✔ [2729/2767] Built Mathlib.MeasureTheory.Measure.OpenPos (3.3s)
✔ [2730/2767] Built Mathlib.MeasureTheory.Constructions.BorelSpace.Metric (2.4s)
✔ [2731/2767] Built Mathlib.MeasureTheory.Constructions.BorelSpace.Order (7.7s)
✔ [2732/2767] Built Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap (3.1s)
✔ [2733/2768] Built Mathlib.Topology.UniformSpace.CompactConvergence (3.2s)
✔ [2734/2768] Built Mathlib.Order.Filter.ENNReal (2.8s)
✔ [2735/2768] Built Mathlib.MeasureTheory.Constructions.BorelSpace.Real (4.0s)
✔ [2736/2768] Built Mathlib.MeasureTheory.Group.Action (5.9s)
✔ [2737/2773] Built Mathlib.Analysis.SpecialFunctions.Pow.NNReal (8.4s)
✔ [2738/2773] Built Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable (1.9s)
✔ [2739/2773] Built Mathlib.Probability.ConditionalProbability (2.7s)
✔ [2740/2777] Built Mathlib.MeasureTheory.MeasurableSpace.Pi (1.4s)
✔ [2741/2777] Built Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics (3.6s)
✔ [2742/2777] Built Mathlib.MeasureTheory.Function.SimpleFunc (9.9s)
✔ [2743/2778] Built Mathlib.MeasureTheory.Constructions.BorelSpace.Complex (1.8s)
✔ [2744/2778] Built Mathlib.Topology.ContinuousMap.Algebra (8.5s)
✔ [2745/2778] Built Mathlib.MeasureTheory.Constructions.Polish.Basic (5.7s)
✔ [2746/2778] Built Mathlib.MeasureTheory.Function.SimpleFuncDense (2.7s)
✔ [2747/2780] Built Mathlib.Analysis.SpecialFunctions.Pow.Continuity (5.4s)
✔ [2748/2783] Built Mathlib.MeasureTheory.Function.SpecialFunctions.Basic (2.9s)
✔ [2749/2783] Built Mathlib.Data.ENNReal.Holder (1.8s)
✔ [2750/2787] Built Mathlib.MeasureTheory.Integral.Lebesgue.Basic (5.6s)
✔ [2751/2787] Built Mathlib.Algebra.BigOperators.Field (1.3s)
✔ [2752/2787] Built Mathlib.Analysis.Normed.Group.Indicator (1.4s)
✔ [2753/2787] Built Mathlib.MeasureTheory.Integral.Lebesgue.Norm (1.7s)
✔ [2754/2787] Built Mathlib.MeasureTheory.Integral.Lebesgue.Add (5.0s)
✔ [2755/2787] Built Mathlib.Analysis.Convex.Slope (5.6s)
✔ [2756/2787] Built Mathlib.Data.Real.ConjExponents (4.4s)
✔ [2757/2798] Built Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (7.0s)
✔ [2758/2798] Built Mathlib.MeasureTheory.Integral.Lebesgue.Map (2.5s)
✔ [2759/2798] Built Mathlib.MeasureTheory.Integral.Lebesgue.Sub (2.3s)
✔ [2760/2798] Built Mathlib.MeasureTheory.Integral.Lebesgue.Markov (2.0s)
✔ [2761/2800] Built Mathlib.Analysis.Convex.SpecificFunctions.Basic (3.1s)
✔ [2762/2800] Built Mathlib.MeasureTheory.Function.Egorov (2.7s)
✔ [2763/2800] Built Mathlib.Order.Monotone.Monovary (1.6s)
✔ [2764/2801] Built Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (2.2s)
✔ [2765/2805] Built Mathlib.MeasureTheory.Integral.Lebesgue.Countable (3.9s)
✔ [2766/2805] Built Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (6.9s)
✔ [2767/2805] Built Mathlib.MeasureTheory.Measure.Real (4.3s)
✔ [2768/2805] Built Mathlib.Algebra.Order.Monovary (6.0s)
✔ [2769/2805] Built Mathlib.MeasureTheory.Measure.GiryMonad (3.4s)
✔ [2770/2805] Built Mathlib.Analysis.MeanInequalities (8.8s)
✔ [2771/2805] Built Mathlib.Order.Filter.IndicatorFunction (1.6s)
✔ [2772/2813] Built Mathlib.MeasureTheory.Function.AEEqFun (6.0s)
✔ [2773/2813] Built Mathlib.Analysis.Convex.Mul (8.2s)
✔ [2774/2814] Built Mathlib.MeasureTheory.Measure.Prod (9.2s)
✔ [2775/2814] Built Mathlib.Analysis.Calculus.FDeriv.Measurable (12s)
✔ [2776/2814] Built Mathlib.Analysis.MeanInequalitiesPow (4.1s)
✔ [2777/2815] Built Mathlib.Algebra.Module.MinimalAxioms (800ms)
✔ [2778/2818] Built Mathlib.MeasureTheory.Group.Convolution (3.2s)
✔ [2779/2820] Built Mathlib.Topology.Algebra.Indicator (1.6s)
✔ [2780/2820] Built Mathlib.Analysis.Normed.Operator.Extend (9.7s)
✔ [2781/2827] Built Mathlib.MeasureTheory.Integral.MeanInequalities (3.8s)
✔ [2782/2829] Built Mathlib.MeasureTheory.Group.Measure (8.6s)
✔ [2783/2829] Built Mathlib.Topology.Bornology.BoundedOperation (2.4s)
✔ [2784/2829] Built Mathlib.Topology.NoetherianSpace (1.9s)
✔ [2785/2829] Built Mathlib.Topology.ContinuousMap.Star (2.2s)
✔ [2786/2829] Built Mathlib.Topology.QuasiSeparated (2.4s)
✔ [2787/2829] Built Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable (2.8s)
✔ [2788/2829] Built Mathlib.MeasureTheory.Group.LIntegral (2.4s)
✔ [2789/2830] Built Mathlib.MeasureTheory.Constructions.Pi (6.1s)
✔ [2790/2832] Built Mathlib.Topology.ContinuousMap.Bounded.Basic (6.5s)
✔ [2791/2832] Built Mathlib.MeasureTheory.Group.Prod (5.3s)
✔ [2792/2833] Built Mathlib.Probability.UniformOn (2.5s)
✔ [2793/2833] Built Mathlib.Topology.Sets.Compacts (3.9s)
✔ [2794/2833] Built Mathlib.Analysis.Normed.Operator.CompleteCodomain (3.1s)
✔ [2795/2834] Built Mathlib.Topology.MetricSpace.ThickenedIndicator (3.0s)
✔ [2796/2834] Built Mathlib.Analysis.LConvolution (2.6s)
✔ [2797/2836] Built Mathlib.MeasureTheory.Function.EssSup (3.3s)
✔ [2798/2836] Built Mathlib.LinearAlgebra.Matrix.Diagonal (2.4s)
✔ [2799/2836] Built Mathlib.MeasureTheory.Integral.Marginal (3.5s)
✔ [2800/2837] Built Mathlib.MeasureTheory.Function.LpSeminorm.Defs (2.3s)
✔ [2801/2839] Built Mathlib.Topology.ContinuousMap.Bounded.Normed (9.0s)
✔ [2802/2839] Built Mathlib.Topology.Order.LeftRightLim (3.9s)
✔ [2803/2839] Built Mathlib.MeasureTheory.Measure.WithDensity (6.5s)
✔ [2804/2839] Built Mathlib.Topology.Algebra.Group.Compact (1.7s)
✔ [2805/2839] Built Mathlib.MeasureTheory.Measure.Content (3.7s)
✔ [2806/2839] Built Mathlib.Topology.ContinuousMap.Bounded.Star (2.9s)
✔ [2807/2839] Built Mathlib.MeasureTheory.Function.LpSeminorm.Basic (8.4s)
✔ [2808/2839] Built Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas (2.9s)
✔ [2809/2839] Built Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (4.9s)
✔ [2810/2839] Built Mathlib.MeasureTheory.Measure.Stieltjes (5.0s)
✔ [2811/2839] Built Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality (2.8s)
✔ [2812/2842] Built Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (3.4s)
✔ [2813/2842] Built Mathlib.MeasureTheory.Measure.Haar.Basic (6.1s)
✔ [2814/2842] Built Mathlib.Topology.ContinuousMap.Compact (6.7s)
✔ [2815/2842] Built Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (2.7s)
✔ [2816/2848] Built Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov (2.2s)
✔ [2817/2853] Built Mathlib.MeasureTheory.Function.LpSeminorm.SMul (3.1s)
✔ [2818/2853] Built Mathlib.Topology.Baire.CompleteMetrizable (1.9s)
✔ [2819/2854] Built Mathlib.Analysis.InnerProductSpace.Defs (6.7s)
✔ [2820/2856] Built Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (4.8s)
✔ [2821/2856] Built Mathlib.Topology.Algebra.Module.ClosedSubmodule (4.9s)
✔ [2822/2856] Built Mathlib.Topology.ContinuousMap.ContinuousMapZero (7.9s)
✔ [2823/2860] Built Mathlib.Algebra.DirectSum.Decomposition (4.2s)
✔ [2824/2860] Built Mathlib.Analysis.Normed.Lp.WithLp (3.6s)
✔ [2825/2866] Built Mathlib.Analysis.InnerProductSpace.Basic (10s)
✔ [2826/2866] Built Mathlib.Analysis.InnerProductSpace.Continuous (2.0s)
✔ [2827/2866] Built Mathlib.Analysis.Normed.Operator.Banach (14s)
✔ [2828/2868] Built Mathlib.Data.Matrix.Reflection (2.1s)
✔ [2829/2870] Built Mathlib.Util.Superscript (1.8s)
✔ [2830/2870] Built Mathlib.Analysis.InnerProductSpace.Projection.Minimal (5.1s)
✔ [2831/2870] Built Mathlib.MeasureTheory.Function.LpSpace.Basic (17s)
✔ [2832/2873] Built Mathlib.MeasureTheory.Topology (1.5s)
✔ [2833/2873] Built Mathlib.Analysis.Normed.Lp.ProdLp (11s)
✔ [2834/2873] Built Mathlib.Topology.Algebra.IsUniformGroup.Order (1.5s)
✔ [2835/2873] Built Mathlib.LinearAlgebra.UnitaryGroup (4.1s)
✔ [2836/2874] Built Mathlib.Analysis.Calculus.TangentCone.Prod (2.2s)
✔ [2837/2880] Built Mathlib.MeasureTheory.Function.LpSpace.Indicator (4.6s)
✔ [2838/2880] Built Mathlib.MeasureTheory.Function.LpSpace.Complete (4.0s)
✔ [2839/2880] Built Mathlib.Order.Filter.AtTopBot.Floor (1.5s)
✔ [2840/2880] Built Mathlib.MeasureTheory.Function.ConvergenceInMeasure (3.0s)
✔ [2841/2882] Built Mathlib.Topology.Algebra.Order.Floor (3.5s)
✔ [2842/2887] Built Mathlib.Analysis.InnerProductSpace.LinearMap (12s)
✔ [2843/2889] Built Mathlib.MeasureTheory.Function.LpOrder (2.8s)
✔ [2844/2893] Built Mathlib.Analysis.BoxIntegral.Box.Basic (2.0s)
✔ [2845/2893] Built Mathlib.Analysis.InnerProductSpace.Orthonormal (5.8s)
✔ [2846/2893] Built Mathlib.Analysis.BoxIntegral.Partition.Basic (4.3s)
✔ [2847/2893] Built Mathlib.Analysis.BoxIntegral.Box.SubboxInduction (2.5s)
✔ [2848/2896] Built Mathlib.Analysis.Oscillation (2.2s)
✔ [2849/2896] Built Mathlib.Analysis.Normed.Lp.PiLp (16s)
✔ [2850/2896] Built Mathlib.Analysis.BoxIntegral.Partition.Split (2.4s)
✔ [2851/2896] Built Mathlib.Analysis.InnerProductSpace.Subspace (4.1s)
✔ [2852/2896] Built Mathlib.MeasureTheory.Function.LpSeminorm.Prod (2.2s)
✔ [2853/2896] Built Mathlib.Analysis.BoxIntegral.Partition.Tagged (3.3s)
✔ [2854/2897] Built Mathlib.MeasureTheory.Function.L1Space.Integrable (12s)
✔ [2855/2899] Built Mathlib.Analysis.BoxIntegral.Partition.Additive (2.6s)
✔ [2856/2900] Built Mathlib.Analysis.Normed.Lp.Matrix (3.5s)
✔ [2857/2900] Built Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction (1.0s)
✔ [2858/2905] Built Mathlib.MeasureTheory.Function.L1Space.AEEqFun (4.5s)
✔ [2859/2906] Built Mathlib.LinearAlgebra.Orientation (5.7s)
✔ [2860/2906] Built Mathlib.Analysis.InnerProductSpace.Orthogonal (8.8s)
✔ [2861/2906] Built Mathlib.MeasureTheory.Integral.IntegrableOn (6.7s)
✔ [2862/2908] Built Mathlib.Analysis.BoxIntegral.Partition.Filter (3.7s)
✔ [2863/2908] Built Mathlib.Analysis.Normed.Lp.MeasurableSpace (1.6s)
✔ [2864/2908] Built Mathlib.FieldTheory.PolynomialGaloisGroup (5.2s)
✔ [2865/2908] Built Mathlib.Analysis.Complex.Cardinality (1.7s)
✔ [2866/2910] Built Mathlib.Analysis.InnerProductSpace.Symmetric (6.0s)
✔ [2867/2914] Built Mathlib.MeasureTheory.Function.LocallyIntegrable (6.8s)
✔ [2868/2914] Built Mathlib.LinearAlgebra.Complex.FiniteDimensional (2.2s)
✔ [2869/2914] Built Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (11s)
✔ [2870/2915] Built Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (3.3s)
✔ [2871/2915] Built Mathlib.Topology.Maps.Proper.CompactlyGenerated (2.3s)
✔ [2872/2916] Built Mathlib.RingTheory.Finiteness.Quotient (2.5s)
✔ [2873/2917] Built Mathlib.RingTheory.Polynomial.Vieta (2.9s)
✔ [2874/2919] Built Mathlib.Algebra.CharP.Quotient (2.1s)
✔ [2875/2920] Built Mathlib.Analysis.InnerProductSpace.Projection.Basic (10s)
✔ [2876/2920] Built Mathlib.Topology.Algebra.Polynomial (3.2s)
✔ [2877/2920] Built Mathlib.Algebra.Field.ZMod (1.9s)
✔ [2878/2920] Built Mathlib.MeasureTheory.Integral.FinMeasAdditive (8.0s)
✔ [2879/2923] Built Mathlib.Data.ZMod.ValMinAbs (2.1s)
✔ [2880/2923] Built Mathlib.LinearAlgebra.FreeModule.Determinant (1.5s)
✔ [2881/2923] Built Mathlib.Analysis.InnerProductSpace.Projection.Submodule (4.5s)
✔ [2882/2923] Built Mathlib.Analysis.InnerProductSpace.Projection.Reflection (4.5s)
✔ [2883/2923] Built Mathlib.Data.Int.Associated (1.2s)
✔ [2884/2923] Built Mathlib.Data.Int.NatAbs (916ms)
✔ [2885/2927] Built Mathlib.FieldTheory.Finite.Basic (6.2s)
✔ [2886/2927] Built Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient (2.8s)
✔ [2887/2928] Built Mathlib.Data.SetLike.Fintype (1.2s)
✔ [2888/2928] Built Mathlib.RingTheory.Artinian.Defs (1.7s)
✔ [2889/2933] Built Mathlib.RingTheory.Ideal.Quotient.PowTransition (3.7s)
✔ [2890/2933] Built Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (7.4s)
✔ [2891/2933] Built Mathlib.RingTheory.Jacobson.Semiprimary (1.9s)
✔ [2892/2933] Built Mathlib.RingTheory.Spectrum.Maximal.Basic (1.4s)
✔ [2893/2933] Built Mathlib.RingTheory.LocalRing.RingHom.Basic (2.0s)
✔ [2894/2935] Built Mathlib.RingTheory.Artinian.Module (6.8s)
✔ [2895/2939] Built Mathlib.RingTheory.FiniteLength (2.8s)
✔ [2896/2939] Built Mathlib.Algebra.GroupWithZero.Submonoid.Instances (1.6s)
✔ [2897/2939] Built Mathlib.RingTheory.AdicCompletion.Basic (15s)
✔ [2898/2940] Built Mathlib.Algebra.Order.GroupWithZero.WithZero (2.6s)
✔ [2899/2943] Built Mathlib.RingTheory.Length (4.4s)
✔ [2900/2947] Built Mathlib.RingTheory.Bezout (1.5s)
✔ [2901/2949] Built Mathlib.MeasureTheory.Integral.SetToL1 (30s)
✔ [2902/2949] Built Mathlib.Algebra.GroupWithZero.Range (3.4s)
✔ [2903/2949] Built Mathlib.GroupTheory.PGroup (2.9s)
✔ [2904/2951] Built Mathlib.RingTheory.Coprime.Ideal (2.3s)
✔ [2905/2951] Built Mathlib.Algebra.Order.GroupWithZero.Range (2.1s)
✔ [2906/2952] Built Mathlib.GroupTheory.Torsion (3.7s)
✔ [2907/2952] Built Mathlib.Analysis.InnerProductSpace.PiL2 (27s)
✔ [2908/2954] Built Mathlib.GroupTheory.Sylow (5.4s)
✔ [2909/2954] Built Mathlib.MeasureTheory.Integral.Bochner.L1 (11s)
✔ [2910/2954] Built Mathlib.RingTheory.Finiteness.Nakayama (2.0s)
✔ [2911/2954] Built Mathlib.Algebra.Polynomial.Module.AEval (8.6s)
✔ [2912/2954] Built Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho (4.8s)
✔ [2913/2954] Built Mathlib.Analysis.InnerProductSpace.ProdL2 (6.1s)
✔ [2914/2956] Built Mathlib.Algebra.Module.ZMod (2.7s)
✔ [2915/2956] Built Mathlib.RingTheory.ReesAlgebra (2.2s)
✔ [2916/2956] Built Mathlib.MeasureTheory.Measure.Haar.OfBasis (7.7s)
✔ [2917/2958] Built Mathlib.RingTheory.Valuation.Basic (15s)
✔ [2918/2958] Built Mathlib.Algebra.Polynomial.Module.Basic (7.2s)
✔ [2919/2958] Built Mathlib.Analysis.InnerProductSpace.Orientation (5.5s)
✔ [2920/2958] Built Mathlib.RingTheory.LocalRing.ResidueField.Defs (2.5s)
✔ [2921/2958] Built Mathlib.MeasureTheory.Integral.Bochner.Basic (14s)
✔ [2922/2958] Built Mathlib.MeasureTheory.Measure.Lebesgue.Basic (6.0s)
✔ [2923/2958] Built Mathlib.Algebra.Module.Torsion.Basic (11s)
✔ [2924/2960] Built Mathlib.RingTheory.Valuation.PrimeMultiplicity (1.6s)
✔ [2925/2960] Built Mathlib.RingTheory.Valuation.Integers (5.8s)
✔ [2926/2960] Built Mathlib.RingTheory.LocalRing.ResidueField.Basic (3.0s)
✔ [2927/2960] Built Mathlib.RingTheory.Nakayama (4.0s)
✔ [2928/2960] Built Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory (3.0s)
✔ [2929/2960] Built Mathlib.RingTheory.Filtration (5.1s)
✔ [2930/2960] Built Mathlib.Analysis.BoxIntegral.Partition.Measure (2.1s)
✔ [2931/2961] Built Mathlib.MeasureTheory.Integral.Bochner.SumMeasure (3.2s)
✔ [2932/2962] Built Mathlib.RingTheory.Jacobson.Polynomial (2.2s)
✔ [2933/2962] Built Mathlib.RingTheory.Valuation.ValuationRing (4.8s)
✔ [2934/2962] Built Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (11s)
✔ [2935/2962] Built Mathlib.RingTheory.Ideal.Cotangent (10s)
✔ [2936/2963] Built Mathlib.Algebra.Order.Ring.Idempotent (2.0s)
✔ [2937/2963] Built Mathlib.Analysis.BoxIntegral.Basic (11s)
✔ [2938/2963] Built Mathlib.Order.Heyting.Hom (3.9s)
✔ [2939/2963] Built Mathlib.MeasureTheory.Integral.Bochner.Set (12s)
✔ [2940/2964] Built Mathlib.RingTheory.DiscreteValuationRing.Basic (4.0s)
✔ [2941/2964] Built Mathlib.RingTheory.Jacobson.Ring (7.8s)
✔ [2942/2964] Built Mathlib.RingTheory.Ideal.MinimalPrime.Localization (2.7s)
✔ [2943/2964] Built Mathlib.Analysis.BoxIntegral.Integrability (4.0s)
✔ [2944/2964] Built Mathlib.Analysis.BoxIntegral.DivergenceTheorem (4.6s)
✔ [2945/2964] Built Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace (7.3s)
✔ [2946/2968] Built Mathlib.MeasureTheory.Integral.Bochner.FundThmCalculus (2.1s)
✔ [2947/2968] Built Mathlib.RingTheory.Localization.AsSubring (2.8s)
✔ [2948/2969] Built Mathlib.MeasureTheory.Measure.Lebesgue.Complex (2.8s)
✔ [2949/2970] Built Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap (6.1s)
✔ [2950/2972] Built Mathlib.RingTheory.SurjectiveOnStalks (5.0s)
✔ [2951/2972] Built Mathlib.Topology.Sets.OpenCover (1.8s)
✔ [2952/2973] Built Mathlib.Order.BooleanSubalgebra (6.8s)
✔ [2953/2973] Built Mathlib.Topology.LocallyClosed (1.7s)
✔ [2954/2973] Built Mathlib.Topology.Spectral.Hom (2.0s)
✔ [2955/2973] Built Mathlib.RingTheory.LocalRing.ResidueField.Ideal (5.7s)
✔ [2956/2976] Built Mathlib.MeasureTheory.Group.FundamentalDomain (21s)
✔ [2957/2982] Built Mathlib.Topology.LocalAtTarget (3.3s)
✔ [2958/2982] Built Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (13s)
✔ [2959/2982] Built Mathlib.RingTheory.Spectrum.Prime.RingHom (4.1s)
✔ [2960/2984] Built Mathlib.Topology.Sober (1.0s)
✔ [2961/2984] Built Mathlib.Order.Ideal (3.3s)
✔ [2962/2984] Built Mathlib.RingTheory.Localization.Submodule (2.8s)
✔ [2963/2984] Built Mathlib.RingTheory.Spectrum.Maximal.Localization (4.4s)
✔ [2964/2985] Built Mathlib.Topology.KrullDimension (1.9s)
✔ [2965/2989] Built Mathlib.RingTheory.LocalProperties.Submodule (4.2s)
✔ [2966/2998] Built Mathlib.CategoryTheory.Category.Init (659ms)
✔ [2967/3003] Built Mathlib.MeasureTheory.Integral.DominatedConvergence (6.9s)
✔ [2968/3003] Built Mathlib.Data.Opposite (790ms)
✔ [2969/3003] Built Mathlib.Tactic.CategoryTheory.CategoryStar (541ms)
✔ [2970/3003] Built Mathlib.Topology.Spectral.Prespectral (2.2s)
✔ [2971/3003] Built Mathlib.Combinatorics.Quiver.Basic (818ms)
✔ [2972/3003] Built Mathlib.Topology.Spectral.Basic (1.6s)
✔ [2973/3003] Built Mathlib.Topology.Constructible (3.9s)
✔ [2974/3003] Built Mathlib.MeasureTheory.Integral.Prod (7.7s)
✔ [2975/3003] Built Mathlib.MeasureTheory.Measure.Haar.Quotient (8.1s)
✔ [2976/3005] Built Mathlib.Combinatorics.Quiver.Prefunctor (1.0s)
✔ [2977/3007] Built Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus (9.3s)
✔ [2978/3007] Built Mathlib.CategoryTheory.Category.Basic (2.7s)
✔ [2979/3007] Built Mathlib.Logic.Lemmas (920ms)
✔ [2980/3007] Built Mathlib.Analysis.SpecialFunctions.NonIntegrable (4.7s)
✔ [2981/3007] Built Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic (6.8s)
✔ [2982/3007] Built Mathlib.Combinatorics.Quiver.Push (1.0s)
✔ [2983/3010] Built Mathlib.MeasureTheory.Integral.DivergenceTheorem (7.7s)
✔ [2984/3010] Built Mathlib.RingTheory.Spectrum.Prime.Topology (8.0s)
✔ [2985/3010] Built Mathlib.CategoryTheory.Functor.Basic (1.6s)
✔ [2986/3010] Built Mathlib.Combinatorics.Quiver.Path (1.7s)
✔ [2987/3010] Built Mathlib.Tactic.CategoryTheory.Reassoc (1.5s)
✔ [2988/3010] Built Mathlib.RingTheory.KrullDimension.Zero (2.3s)
✔ [2989/3012] Built Mathlib.Combinatorics.Quiver.Symmetric (1.4s)
✔ [2990/3016] Built Mathlib.CategoryTheory.NatTrans (1.4s)
✔ [2991/3016] Built Mathlib.CategoryTheory.Iso (3.6s)
✔ [2992/3018] Built Mathlib.Tactic.CategoryTheory.Slice (2.2s)
✔ [2993/3018] Built Mathlib.RingTheory.DiscreteValuationRing.TFAE (3.7s)
✔ [2994/3018] Built Mathlib.MeasureTheory.Integral.CircleIntegral (7.6s)
✔ [2995/3047] Built Mathlib.Tactic.CategoryTheory.IsoReassoc (1.1s)
✔ [2996/3047] Built Mathlib.CategoryTheory.ObjectProperty.Basic (1.4s)
✔ [2997/3108] Built Mathlib.CategoryTheory.ConcreteCategory.Bundled (512ms)
✔ [2998/3108] Built Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms (1.1s)
✔ [2999/3146] Built Mathlib.Algebra.Ring.Shrink (1.1s)
✔ [3000/3146] Built Mathlib.CategoryTheory.Functor.Category (3.4s)
✔ [3001/3146] Built Mathlib.CategoryTheory.HomCongr (1.3s)
✔ [3002/3149] Built Mathlib.CategoryTheory.Thin (1.5s)
✔ [3003/3149] Built Mathlib.RingTheory.ChainOfDivisors (3.7s)
✔ [3004/3156] Built Mathlib.Analysis.Complex.CauchyIntegral (5.0s)
✔ [3005/3156] Built Mathlib.Algebra.Ring.Subsemiring.Pointwise (2.8s)
✔ [3006/3159] Built Mathlib.CategoryTheory.NatIso (4.3s)
✔ [3007/3159] Built Mathlib.RingTheory.Ideal.Basis (1.6s)
✔ [3008/3159] Built Mathlib.Analysis.Complex.Liouville (3.7s)
✔ [3009/3159] Built Mathlib.Algebra.Ring.Subring.Pointwise (2.4s)
✔ [3010/3159] Built Mathlib.RingTheory.Norm.Basic (3.5s)
✔ [3011/3162] Built Mathlib.RingTheory.FractionalIdeal.Basic (6.1s)
✔ [3012/3164] Built Mathlib.CategoryTheory.Functor.FullyFaithful (2.4s)
✔ [3013/3164] Built Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative (1.0s)
✔ [3014/3164] Built Mathlib.Algebra.Algebra.Subalgebra.Pointwise (1.0s)
✔ [3015/3164] Built Mathlib.Analysis.Complex.Polynomial.Basic (3.5s)
✔ [3016/3164] Built Mathlib.CategoryTheory.Bicategory.Basic (5.3s)
✔ [3017/3164] Built Mathlib.Algebra.GroupWithZero.Torsion (1.3s)
✔ [3018/3164] Built Mathlib.CategoryTheory.InducedCategory (1.6s)
✔ [3019/3165] Built Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp (1.9s)
✔ [3020/3168] Built Mathlib.CategoryTheory.ObjectProperty.FullSubcategory (1.8s)
✔ [3021/3168] Built Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings (4.6s)
✔ [3022/3168] Built Mathlib.CategoryTheory.EssentialImage (1.7s)
✔ [3023/3168] Built Mathlib.RingTheory.FractionalIdeal.Operations (11s)
✔ [3024/3168] Built Mathlib.CategoryTheory.Whiskering (9.0s)
✔ [3025/3169] Built Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (4.9s)
✔ [3026/3169] Built Mathlib.CategoryTheory.ConcreteCategory.Basic (1.4s)
✔ [3027/3169] Built Mathlib.Order.Interval.Finset.DenselyOrdered (1.2s)
✔ [3028/3170] Built Mathlib.CategoryTheory.Functor.ReflectsIso.Basic (1.1s)
✔ [3029/3170] Built Mathlib.Algebra.Order.Group.Cyclic (1.8s)
✔ [3030/3171] Built Mathlib.RingTheory.FractionalIdeal.Inverse (2.0s)
✔ [3031/3171] Built Mathlib.Tactic.CategoryTheory.Elementwise (1.6s)
✔ [3032/3172] Built Mathlib.Algebra.Order.Ring.IsNonarchimedean (2.9s)
✔ [3033/3172] Built Mathlib.CategoryTheory.Equivalence (6.5s)
✔ [3034/3172] Built Mathlib.Data.Int.WithZero (1.8s)
✔ [3035/3173] Built Mathlib.CategoryTheory.Elementwise (1.1s)
✔ [3036/3174] Built Mathlib.RingTheory.DedekindDomain.Ideal.Basic (6.3s)
✔ [3037/3174] Built Mathlib.RingTheory.Valuation.ExtendToLocalization (2.3s)
✔ [3038/3174] Built Mathlib.GroupTheory.ArchimedeanDensely (7.8s)
✔ [3039/3174] Built Mathlib.Algebra.Field.TransferInstance (1.3s)
✔ [3040/3174] Built Mathlib.RingTheory.Valuation.Archimedean (4.4s)
✔ [3041/3180] Built Mathlib.CategoryTheory.Opposites (8.0s)
✔ [3042/3184] Built Mathlib.Topology.Algebra.UniformFilterBasis (1.6s)
✔ [3043/3184] Built Mathlib.Topology.Algebra.OpenSubgroup (4.1s)
✔ [3044/3184] Built Mathlib.CategoryTheory.Functor.TwoSquare (2.2s)
✔ [3045/3184] Built Mathlib.RingTheory.Valuation.ValuativeRel.Basic (10s)
✔ [3046/3184] Built Mathlib.CategoryTheory.Functor.Const (1.9s)
✔ [3047/3184] Built Mathlib.CategoryTheory.EqToHom (2.2s)
✔ [3048/3187] Built Mathlib.Topology.Algebra.WithZeroTopology (2.0s)
✔ [3049/3187] Built Mathlib.Topology.Algebra.Nonarchimedean.Basic (2.1s)
✔ [3050/3187] Built Mathlib.CategoryTheory.Category.ULift (1.0s)
✔ [3051/3187] Built Mathlib.CategoryTheory.Bicategory.Strict.Basic (1.3s)
✔ [3052/3187] Built Mathlib.CategoryTheory.Products.Basic (4.8s)
✔ [3053/3190] Built Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (18s)
✔ [3054/3190] Built Mathlib.CategoryTheory.Category.Preorder (1.9s)
✔ [3055/3190] Built Mathlib.RingTheory.Ideal.Oka (1.5s)
✔ [3056/3190] Built Mathlib.RingTheory.Valuation.ValuationSubring (8.9s)
✔ [3057/3194] Built Mathlib.Topology.Algebra.Nonarchimedean.Bases (2.5s)
✔ [3058/3194] Built Mathlib.RingTheory.PrincipalIdealDomainOfPrime (1.8s)
✔ [3059/3194] Built Mathlib.Data.Real.Embedding (4.1s)
✔ [3060/3194] Built Mathlib.CategoryTheory.Pi.Basic (4.9s)
✔ [3061/3194] Built Mathlib.CategoryTheory.Functor.Currying (4.5s)
✔ [3062/3195] Built Mathlib.Topology.MetricSpace.Ultra.Basic (1.6s)
✔ [3063/3195] Built Mathlib.CategoryTheory.Discrete.Basic (2.8s)
✔ [3064/3199] Built Mathlib.Analysis.Normed.Field.TransferInstance (1.4s)
✔ [3065/3199] Built Mathlib.Analysis.Normed.Group.Ultra (3.4s)
✔ [3066/3199] Built Mathlib.RingTheory.Valuation.RankOne (5.4s)
✔ [3067/3199] Built Mathlib.CategoryTheory.Products.Unitor (1.7s)
✔ [3068/3199] Built Mathlib.CategoryTheory.FinCategory.Basic (1.3s)
✔ [3069/3199] Built Mathlib.Topology.Algebra.Valued.ValuationTopology (7.7s)
✔ [3070/3199] Built Mathlib.CategoryTheory.PEmpty (1.1s)
✔ [3071/3199] Built Mathlib.CategoryTheory.PUnit (1.6s)
✔ [3072/3199] Built Mathlib.Analysis.Normed.Ring.TransferInstance (1.3s)
✔ [3073/3203] Built Mathlib.CategoryTheory.FinCategory.AsType (1.4s)
✔ [3074/3204] Built Mathlib.Topology.Algebra.Valued.NormedValued (4.6s)
✔ [3075/3206] Built Mathlib.Analysis.Normed.Ring.WithAbs (3.8s)
✔ [3076/3206] Built Mathlib.CategoryTheory.Comma.Basic (10s)
✔ [3077/3206] Built Mathlib.RingTheory.Norm.Transitivity (5.3s)
✔ [3078/3206] Built Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (5.7s)
✔ [3079/3208] Built Mathlib.Topology.Instances.Complex (2.8s)
✔ [3080/3208] Built Mathlib.Analysis.Normed.Field.WithAbs (4.2s)
✔ [3081/3210] Built Mathlib.CategoryTheory.Comma.Arrow (3.1s)
✔ [3082/3211] Built Mathlib.Tactic.Algebra.Lemmas (2.3s)
✔ [3083/3211] Built Mathlib.RingTheory.Discriminant (4.2s)
✔ [3084/3211] Built Mathlib.CategoryTheory.CommSq (2.2s)
✔ [3085/3212] Built Mathlib.Tactic.ArithMult.Init (1.1s)
✔ [3086/3212] Built Mathlib.Analysis.AbsoluteValue.Equivalence (6.0s)
✔ [3087/3213] Built Mathlib.CategoryTheory.MorphismProperty.Basic (4.2s)
✔ [3088/3213] Built Mathlib.Topology.Algebra.Valued.ValuedField (20s)
✔ [3089/3213] Built Mathlib.Tactic.CancelDenoms (922ms)
✔ [3090/3213] Built Mathlib.Tactic.ArithMult (769ms)
✔ [3091/3213] Built Mathlib.RingTheory.Localization.NormTrace (2.2s)
✔ [3092/3213] Built Mathlib.Tactic.Cases (1.5s)
✔ [3093/3213] Built Mathlib.CategoryTheory.Groupoid (2.0s)
✔ [3094/3213] Built Mathlib.Tactic.Algebra.Basic (4.6s)
✔ [3095/3213] Built Mathlib.Tactic.CategoryTheory.BicategoricalComp (1.4s)
✔ [3096/3213] Built Mathlib.CategoryTheory.MorphismProperty.Composition (2.4s)
✔ [3097/3213] Built Mathlib.CategoryTheory.MorphismProperty.Factorization (2.5s)
✔ [3098/3213] Built Mathlib.CategoryTheory.Endomorphism (1.7s)
✔ [3099/3217] Built Mathlib.CategoryTheory.IsConnected (2.1s)
✔ [3100/3219] Built Mathlib.NumberTheory.NumberField.Norm (2.7s)
✔ [3101/3221] Built Mathlib.Tactic.CategoryTheory.Coherence.Datatypes (1.4s)
✔ [3102/3221] Built Mathlib.CategoryTheory.EpiMono (2.2s)
✔ [3103/3221] Built Mathlib.Tactic.CategoryTheory.Coherence.Normalize (4.6s)
✔ [3104/3221] Built Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (6.4s)
✔ [3105/3221] Built Mathlib.Tactic.CategoryTheory.Coherence.PureCoherence (5.5s)
✔ [3106/3221] Built Mathlib.Topology.Algebra.Valued.WithVal (11s)
✔ [3107/3221] Built Mathlib.CategoryTheory.Retract (1.9s)
✔ [3108/3221] Built Mathlib.CategoryTheory.Types.Basic (2.5s)
✔ [3109/3222] Built Mathlib.CategoryTheory.Balanced (1.3s)
✔ [3110/3222] Built Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes (3.7s)
✔ [3111/3222] Built Mathlib.Tactic.CategoryTheory.Coherence.Basic (1.4s)
✔ [3112/3222] Built Mathlib.CategoryTheory.Monad.Basic (3.8s)
✔ [3113/3222] Built Mathlib.CategoryTheory.LiftingProperties.Basic (1.8s)
✔ [3114/3224] Built Mathlib.CategoryTheory.Functor.Hom (1.2s)
✔ [3115/3228] Built Mathlib.CategoryTheory.Limits.Types.ColimitType (2.2s)
✔ [3116/3228] Built Mathlib.CategoryTheory.ConcreteCategory.Forget (1.7s)
✔ [3117/3228] Built Mathlib.CategoryTheory.Category.Cat (3.7s)
✔ [3118/3228] Built Mathlib.CategoryTheory.Bicategory.Functor.Prelax (2.1s)
✔ [3119/3230] Built Mathlib.CategoryTheory.Limits.Shapes.StrongEpi (1.5s)
✔ [3120/3230] Built Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence (2.9s)
✔ [3121/3230] Built Mathlib.CategoryTheory.ConcreteCategory.ReflectsIso (1.1s)
✔ [3122/3230] Built Mathlib.Tactic.CategoryTheory.Bicategory.Normalize (3.7s)
✔ [3123/3230] Built Mathlib.CategoryTheory.Category.Cat.AsSmall (1.1s)
✔ [3124/3230] Built Mathlib.Tactic.CategoryTheory.ToApp (1.7s)
✔ [3125/3230] Built Mathlib.CategoryTheory.IsomorphismClasses (1.2s)
✔ [3126/3230] Built Mathlib.Tactic.CategoryTheory.CancelIso (1.3s)
✔ [3127/3230] Built Mathlib.Algebra.Category.MonCat.Basic (4.4s)
✔ [3128/3230] Built Mathlib.Tactic.CategoryTheory.CheckCompositions (1.3s)
✔ [3129/3230] Built Mathlib.Tactic.CategoryTheory.Bicategory.Basic (3.2s)
✔ [3130/3236] Built Mathlib.CategoryTheory.Bicategory.Functor.Oplax (4.5s)
✔ [3131/3236] Built Mathlib.CategoryTheory.Bicategory.Functor.Lax (4.8s)
✔ [3132/3238] Built Mathlib.CategoryTheory.Yoneda (11s)
✔ [3133/3238] Built Mathlib.Algebra.Category.MonCat.ForgetCorepresentable (1.3s)
✔ [3134/3238] Built Mathlib.CategoryTheory.Functor.Trifunctor (3.1s)
✔ [3135/3240] Built Mathlib.Algebra.Category.Grp.Basic (5.3s)
✔ [3136/3240] Built Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor (7.0s)
✔ [3137/3242] Built Mathlib.CategoryTheory.Adjunction.Basic (6.4s)
✔ [3138/3242] Built Mathlib.CategoryTheory.Monoidal.Category (8.5s)
✔ [3139/3242] Built Mathlib.CategoryTheory.LiftingProperties.Adjunction (1.6s)
✔ [3140/3242] Built Mathlib.Algebra.Category.Ring.Basic (5.2s)
✔ [3141/3242] Built Mathlib.CategoryTheory.Bicategory.Free (5.9s)
✔ [3142/3242] Built Mathlib.CategoryTheory.Adjunction.FullyFaithful (2.6s)
✔ [3143/3243] Built Mathlib.CategoryTheory.Limits.Cones (14s)
✔ [3144/3244] Built Mathlib.Tactic.Change (949ms)
✔ [3145/3244] Built Mathlib.Tactic.Clean (667ms)
✔ [3146/3244] Built Mathlib.CategoryTheory.Skeletal (3.0s)
✔ [3147/3244] Built Mathlib.Tactic.CategoryTheory.MonoidalComp (1.6s)
✔ [3148/3244] Built Mathlib.CategoryTheory.Adjunction.Mates (5.8s)
✔ [3149/3244] Built Mathlib.CategoryTheory.Functor.EpiMono (2.1s)
✔ [3150/3244] Built Mathlib.Algebra.Category.Ring.Instances (1.7s)
✔ [3151/3244] Built Mathlib.Tactic.CategoryTheory.BicategoryCoherence (1.7s)
✔ [3152/3244] Built Mathlib.Tactic.ComputeAsymptotics.Lemmas (1.8s)
✔ [3153/3244] Built Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis (2.2s)
✔ [3154/3244] Built Mathlib.CategoryTheory.EssentiallySmall (1.9s)
✔ [3155/3246] Built Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes (3.7s)
✔ [3156/3246] Built Mathlib.CategoryTheory.Monad.Algebra (4.0s)
✔ [3157/3246] Built Mathlib.CategoryTheory.Limits.IsLimit (9.2s)
✔ [3158/3246] Built Mathlib.CategoryTheory.ShrinkYoneda (3.6s)
✔ [3159/3248] Built Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence (3.0s)
✔ [3160/3248] Built Mathlib.Order.CompleteLattice.Group (939ms)
✔ [3161/3248] Built Mathlib.CategoryTheory.Monoidal.Functor (13s)
✔ [3162/3248] Built Mathlib.Tactic.CategoryTheory.Monoidal.Normalize (4.3s)
✔ [3163/3248] Built Mathlib.Dynamics.FixedPoints.Topology (1.2s)
✔ [3164/3248] Built Mathlib.CategoryTheory.Limits.Shapes.IsTerminal (4.0s)
✔ [3165/3252] Built Mathlib.CategoryTheory.Monoidal.Free.Basic (3.7s)
✔ [3166/3252] Built Mathlib.Topology.MetricSpace.UniformConvergence (5.3s)
✔ [3167/3254] Built Mathlib.Tactic.CategoryTheory.Monoidal.Basic (3.8s)
✔ [3168/3254] Built Mathlib.CategoryTheory.Limits.HasLimits (7.0s)
✔ [3169/3254] Built Mathlib.Topology.MetricSpace.Contracting (2.4s)
✔ [3170/3254] Built Mathlib.Data.Stream.Defs (1.1s)
✔ [3171/3254] Built Mathlib.Tactic.CategoryTheory.Coherence (2.5s)
✔ [3172/3254] Built Mathlib.Tactic.ENatToNat (1.5s)
✔ [3173/3254] Built Mathlib.CategoryTheory.Limits.Shapes.Terminal (2.9s)
✔ [3174/3254] Built Mathlib.CategoryTheory.Limits.Types.Colimits (2.1s)
✔ [3175/3255] Built Mathlib.Algebra.Category.Ring.Colimits (4.1s)
✔ [3176/3255] Built Mathlib.CategoryTheory.Limits.Types.Limits (2.4s)
✔ [3177/3257] Built Mathlib.CategoryTheory.Limits.Preserves.Basic (3.4s)
✔ [3178/3257] Built Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks (6.8s)
✔ [3179/3257] Built Mathlib.Data.Stream.Init (2.8s)
✔ [3180/3257] Built Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects (1.7s)
✔ [3181/3257] Built Mathlib.CategoryTheory.Comma.StructuredArrow.Basic (14s)
✔ [3182/3257] Built Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal (1.7s)
✔ [3183/3257] Built Mathlib.CategoryTheory.Limits.Types.Yoneda (3.6s)
✔ [3184/3259] Built Mathlib.CategoryTheory.Limits.Preserves.Limits (1.8s)
✔ [3185/3260] Built Mathlib.CategoryTheory.Limits.Creates (3.5s)
✔ [3186/3260] Built Mathlib.CategoryTheory.Limits.Shapes.Products (12s)
✔ [3187/3260] Built Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized (2.1s)
✔ [3188/3260] Built Mathlib.Data.Seq.Computation (3.6s)
✔ [3189/3261] Built Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates (1.7s)
✔ [3190/3261] Built Mathlib.CategoryTheory.Elements (5.0s)
✔ [3191/3261] Built Mathlib.CategoryTheory.Limits.Preserves.Ulift (1.2s)
✔ [3192/3261] Built Mathlib.CategoryTheory.Limits.FunctorCategory.Basic (6.0s)
✔ [3193/3261] Built Mathlib.Tactic.DeriveCountable (2.3s)
✔ [3194/3261] Built Mathlib.CategoryTheory.EffectiveEpi.Basic (1.9s)
✔ [3195/3261] Built Mathlib.Algebra.Category.MonCat.Limits (4.6s)
✔ [3196/3264] Built Mathlib.Data.Seq.Defs (2.6s)
✔ [3197/3264] Built Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic (2.4s)
✔ [3198/3264] Built Mathlib.Control.Traversable.Lemmas (900ms)
✔ [3199/3264] Built Mathlib.Tactic.DeriveEncodable (3.3s)
✔ [3200/3264] Built Mathlib.CategoryTheory.Limits.Yoneda (2.4s)
✔ [3201/3265] Built Mathlib.Tactic.Eval (701ms)
✔ [3202/3267] Built Mathlib.Data.Seq.Basic (4.8s)
✔ [3203/3268] Built Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion (4.8s)
✔ [3204/3269] Built Mathlib.Tactic.DeriveTraversable (3.0s)
✔ [3205/3270] Built Mathlib.Tactic.Explode.Datatypes (599ms)
✔ [3206/3271] Built Mathlib.Tactic.Ext (506ms)
✔ [3207/3272] Built Mathlib.Tactic.Explode.Pretty (536ms)
✔ [3208/3272] Built Mathlib.Tactic.FindSyntax (829ms)
✔ [3209/3273] Built Mathlib.Tactic.GeneralizeProofs (486ms)
✔ [3210/3273] Built Mathlib.Tactic.Generalize (594ms)
✔ [3211/3274] Built Mathlib.Tactic.Have (980ms)
✔ [3212/3274] Built Mathlib.Tactic.Explode (1.2s)
✔ [3213/3278] Built Mathlib.Tactic.Linarith.NNRealPreprocessor (1.8s)
✔ [3215/3279] Built Mathlib.Tactic.ITauto (2.9s)
✔ [3216/3279] Built Mathlib.CategoryTheory.Comma.Over.Basic (22s)
✔ [3217/3280] Built Mathlib.Tactic.Linter.CommandRanges (566ms)
✔ [3218/3280] Built Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs (6.8s)
✔ [3219/3280] Built Mathlib.Tactic.LinearCombinationPrime (2.1s)
✔ [3220/3280] Built Mathlib.Tactic.Linter.CommandStart (520ms)
✔ [3221/3286] Built Mathlib.Tactic.Linarith.Oracle.FourierMotzkin (1.5s)
✔ [3224/3287] Built Mathlib.Tactic.Linter.FindDeprecations (1.2s)
✔ [3226/3287] Built Mathlib.Tactic.Linter.TextBased.UnicodeLinter (1.2s)
✔ [3227/3288] Built Mathlib.Tactic.Linter.ValidatePRTitle (864ms)
✔ [3228/3290] Built Mathlib.Tactic.ModCases (1.6s)
✔ [3229/3291] Built Mathlib.Tactic.Monotonicity.Basic (610ms)
✔ [3230/3292] Built Mathlib.Tactic.Monotonicity.Lemmas (880ms)
✔ [3231/3292] Built Mathlib.Tactic.Linter.TextBased (2.6s)
✔ [3232/3292] Built Mathlib.Tactic.Monotonicity (762ms)
✔ [3233/3296] Built Mathlib.Tactic.MoveAdd (1.6s)
✔ [3234/3297] Built Mathlib.Data.Rat.Sqrt (1.1s)
✔ [3235/3297] Built Mathlib.CategoryTheory.Grothendieck (7.7s)
✔ [3236/3297] Built Mathlib.Tactic.NormNum.IsCoprime (1.4s)
✔ [3237/3297] Built Mathlib.Tactic.NormNum.BigOperators (3.5s)
✔ [3238/3297] Built Mathlib.NumberTheory.Real.Irrational (3.0s)
✔ [3239/3297] Built Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (10s)
✔ [3240/3297] Built Mathlib.Tactic.NormNum.IsSquare (2.0s)
✔ [3241/3297] Built Mathlib.CategoryTheory.Limits.Shapes.Grothendieck (3.6s)
✔ [3242/3297] Built Mathlib.CategoryTheory.Monad.Products (2.5s)
✔ [3243/3302] Built Mathlib.Tactic.NormNum.Irrational (3.5s)
✔ [3244/3302] Built Mathlib.CategoryTheory.Limits.Types.Products (2.4s)
✔ [3245/3304] Built Mathlib.CategoryTheory.Limits.Shapes.StrictInitial (1.5s)
✔ [3246/3304] Built Mathlib.Data.Int.Range (899ms)
✔ [3247/3304] Built Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan (3.8s)
✔ [3248/3308] Built Mathlib.Data.PNat.Prime (1.5s)
✔ [3249/3308] Built Mathlib.Data.Nat.Factorization.PrimePow (1.7s)
✔ [3250/3308] Built Mathlib.NumberTheory.MulChar.Basic (3.7s)
✔ [3251/3316] Built Mathlib.RingTheory.Valuation.IsTrivialOn (2.2s)
✔ [3252/3316] Built Mathlib.FieldTheory.RatFunc.Defs (2.4s)
✔ [3253/3316] Built Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone (3.7s)
✔ [3254/3316] Built Mathlib.NumberTheory.LegendreSymbol.ZModChar (2.3s)
✔ [3255/3316] Built Mathlib.RingTheory.UniqueFactorizationDomain.Nat (1.5s)
✔ [3256/3321] Built Mathlib.RingTheory.RootsOfUnity.Complex (2.9s)
✔ [3257/3321] Built Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic (2.4s)
✔ [3258/3321] Built Mathlib.Data.Nat.Squarefree (3.2s)
✔ [3259/3322] Built Mathlib.RingTheory.Polynomial.Eisenstein.Criterion (2.6s)
✔ [3260/3323] Built Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (5.7s)
✔ [3261/3323] Built Mathlib.NumberTheory.LegendreSymbol.Basic (2.4s)
✔ [3262/3327] Built Mathlib.RingTheory.Polynomial.Eisenstein.Basic (2.3s)
✔ [3263/3327] Built Mathlib.NumberTheory.ArithmeticFunction.Defs (5.9s)
✔ [3264/3327] Built Mathlib.FieldTheory.KrullTopology (4.8s)
✔ [3265/3327] Built Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso (2.6s)
✔ [3266/3328] Built Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting (5.2s)
✔ [3267/3328] Built Mathlib.CategoryTheory.Limits.Shapes.Equalizers (9.9s)
✔ [3268/3328] Built Mathlib.Algebra.GCDMonoid.IntegrallyClosed (2.8s)
✔ [3269/3328] Built Mathlib.FieldTheory.Galois.GaloisClosure (4.3s)
✔ [3270/3328] Built Mathlib.Topology.Algebra.Group.ClosedSubgroup (1.9s)
✔ [3271/3328] Built Mathlib.FieldTheory.RatFunc.Basic (20s)
✔ [3272/3328] Built Mathlib.NumberTheory.ArithmeticFunction.Zeta (2.3s)
✔ [3273/3329] Built Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono (2.9s)
✔ [3274/3329] Built Mathlib.CategoryTheory.Limits.Connected (1.8s)
✔ [3275/3329] Built Mathlib.RingTheory.Adjoin.PowerBasis (3.7s)
✔ [3276/3329] Built Mathlib.CategoryTheory.Comma.Over.Pullback (5.3s)
✔ [3277/3329] Built Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits (1.6s)
✔ [3278/3329] Built Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc (5.3s)
✔ [3279/3329] Built Mathlib.RingTheory.RootsOfUnity.Minpoly (2.6s)
✔ [3280/3329] Built Mathlib.NumberTheory.ArithmeticFunction.Misc (3.0s)
✔ [3281/3329] Built Mathlib.FieldTheory.Galois.Infinite (5.5s)
✔ [3282/3329] Built Mathlib.NumberTheory.Padics.PadicVal.Basic (3.7s)
✔ [3283/3329] Built Mathlib.CategoryTheory.Limits.Shapes.Images (6.3s)
✔ [3284/3335] Built Mathlib.CategoryTheory.Limits.Opposites (4.0s)
✔ [3285/3335] Built Mathlib.NumberTheory.ArithmeticFunction.Moebius (3.1s)
✔ [3286/3338] Built Mathlib.CategoryTheory.Filtered.Basic (4.1s)
✔ [3287/3338] Built Mathlib.FieldTheory.Galois.Abelian (2.5s)
✔ [3288/3338] Built Mathlib.CategoryTheory.Limits.Types.Images (1.3s)
✔ [3289/3338] Built Mathlib.Analysis.Normed.Module.Ray (2.3s)
✔ [3290/3338] Built Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms (4.6s)
✔ [3291/3340] Built Mathlib.CategoryTheory.Limits.Types.Filtered (2.4s)
✔ [3292/3340] Built Mathlib.CategoryTheory.Filtered.Connected (1.2s)
✔ [3293/3340] Built Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks (5.0s)
✔ [3294/3340] Built Mathlib.Algebra.Algebra.ZMod (1.4s)
✔ [3295/3342] Built Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero (2.0s)
✔ [3296/3343] Built Mathlib.Analysis.Convex.StrictConvexSpace (2.8s)
✔ [3297/3343] Built Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic (2.0s)
✔ [3298/3343] Built Mathlib.CategoryTheory.Limits.Final (9.2s)
✔ [3299/3343] Built Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks (3.4s)
✔ [3300/3343] Built Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs (2.0s)
✔ [3301/3349] Built Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers (3.0s)
✔ [3302/3349] Built Mathlib.Data.ZMod.Units (1.8s)
✔ [3303/3350] Built Mathlib.Analysis.Convex.Uniform (2.0s)
✔ [3304/3350] Built Mathlib.FieldTheory.Finite.GaloisField (3.8s)
✔ [3305/3350] Built Mathlib.Algebra.CharP.CharAndCard (1.7s)
✔ [3306/3350] Built Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts (2.1s)
✔ [3307/3350] Built Mathlib.NumberTheory.MulChar.Lemmas (2.8s)
✔ [3308/3352] Built Mathlib.CategoryTheory.Limits.Shapes.RegularMono (3.8s)
✔ [3309/3352] Built Mathlib.Analysis.InnerProductSpace.Convex (1.9s)
✔ [3310/3353] Built Mathlib.Tactic.NormNum.ModEq (1.2s)
✔ [3311/3354] Built Mathlib.FieldTheory.Finite.Trace (1.9s)
✔ [3312/3354] Built Mathlib.CategoryTheory.Limits.Shapes.Kernels (9.2s)
✔ [3313/3355] Built Mathlib.Data.Nat.Fib.Basic (2.2s)
✔ [3314/3355] Built Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (3.7s)
✔ [3315/3355] Built Mathlib.Tactic.NormNum.NatLog (1.8s)
✔ [3316/3356] Built Mathlib.Analysis.Complex.Arg (2.0s)
✔ [3317/3356] Built Mathlib.Tactic.NormNum.NatSqrt (1.2s)
✔ [3318/3357] Built Mathlib.Tactic.NormNum.NatFib (1.6s)
✔ [3319/3358] Built Mathlib.CategoryTheory.Limits.Shapes.KernelPair (1.9s)
✔ [3320/3358] Built Mathlib.Tactic.NormNum.Ordinal (2.4s)
✔ [3321/3359] Built Mathlib.Tactic.NormNum.Parity (1.4s)
✔ [3322/3360] Built Mathlib.CategoryTheory.Preadditive.Basic (3.4s)
✔ [3323/3360] Built Mathlib.Tactic.NormNum.PowMod (1.3s)
✔ [3324/3361] Built Mathlib.Tactic.NormNum.Prime (1.7s)
✔ [3325/3362] Built Mathlib.Algebra.Category.Grp.Preadditive (1.9s)
✔ [3326/3362] Built Mathlib.Tactic.NormNum.RealSqrt (2.3s)
✔ [3327/3363] Built Mathlib.Tactic.Polyrith (520ms)
✔ [3328/3364] Built Mathlib.Tactic.PNatToNat (1.6s)
✔ [3329/3364] Built Mathlib.Tactic.Propose (441ms)
✔ [3330/3367] Built Mathlib.Tactic.ProdAssoc (924ms)
✔ [3331/3369] Built Mathlib.Algebra.Category.Grp.ForgetCorepresentable (1.7s)
✔ [3332/3369] Built Mathlib.Tactic.ReduceModChar.Ext (527ms)
✔ [3333/3369] Built Mathlib.Tactic.Recall (913ms)
✔ [3334/3370] Built Mathlib.Tactic.Relation.Symm (498ms)
✔ [3335/3370] Built Mathlib.Tactic.Replace (662ms)
✔ [3336/3370] Built Mathlib.Tactic.RewriteSearch (583ms)
✔ [3337/3370] Built Mathlib.CategoryTheory.Limits.Shapes.Diagonal (7.4s)
✔ [3338/3375] Built Mathlib.Tactic.ReduceModChar (2.8s)
✔ [3339/3376] Built Mathlib.Tactic.Ring.NamePolyVars (1.4s)
✔ [3340/3377] Built Mathlib.Algebra.Group.TypeTags.Pointwise (911ms)
✔ [3341/3377] Built Mathlib.Tactic.Sat.FromLRAT (1.0s)
✔ [3342/3378] Built Mathlib.Tactic.SetNotationForOrder (1.5s)
✔ [3343/3379] Built Mathlib.Tactic.Simproc.Divisors (1.5s)
✔ [3344/3380] Built Mathlib.CategoryTheory.MorphismProperty.Limits (5.3s)
✔ [3345/3381] Built Mathlib.Algebra.Category.Grp.Limits (7.5s)
✔ [3346/3381] Built Mathlib.Tactic.Simproc.Factors (1.7s)
✔ [3347/3382] Built Mathlib.Data.Finsupp.Weight (4.7s)
✔ [3348/3382] Built Mathlib.Tactic.Simproc.VecPerm (1.6s)
✔ [3349/3384] Built Mathlib.Tactic.TypeCheck (476ms)
✔ [3350/3385] Built Mathlib.Tactic.Simproc.FinsetInterval (2.9s)
✔ [3351/3385] Built ProofWidgets.Component.PenroseDiagram (731ms)
✔ [3352/3388] Built ProofWidgets.Presentation.Expr (921ms)
✔ [3353/3388] Built Mathlib.Tactic.Widget.GCongr (755ms)
✔ [3355/3405] Built ProofWidgets.Component.Panel.Basic (1.1s)
✔ [3356/3405] Built Mathlib.Tactic.Widget.CommDiag (1.6s)
✔ [3357/3405] Built ProofWidgets.Component.HtmlDisplay (778ms)
✔ [3358/3405] Built Mathlib.Tactic.WithoutCDot (669ms)
✔ [3359/3405] Built Iut.Stage1.PilotComparison (2.3s)
✔ [3360/3405] Built Iut.Foundations.AlgorithmicOutput (2.9s)
✔ [3361/3405] Built Mathlib.RingTheory.MvPowerSeries.Basic (7.4s)
✔ [3362/3405] Built Mathlib.Tactic.Ring.NamePowerVars (1.5s)
✔ [3363/3405] Built Iut.Foundations.AlgorithmicBridge (3.2s)
✔ [3364/3405] Built Mathlib.Tactic.Widget.StringDiagram (4.6s)
✔ [3365/3405] Built Mathlib.Algebra.Category.Ring.Limits (13s)
✔ [3366/3405] Built Mathlib.Algebra.Category.Ring.Constructions (6.3s)
✔ [3367/3405] Built Mathlib.RingTheory.RingHomProperties (2.1s)
✔ [3368/3405] Built Mathlib.RingTheory.LocalProperties.Basic (3.1s)
✔ [3369/3405] Built Mathlib.RingTheory.LocalProperties.IntegrallyClosed (2.5s)
✔ [3370/3405] Built Mathlib.RingTheory.DedekindDomain.Dvr (1.8s)
✔ [3371/3405] Built Mathlib.NumberTheory.RamificationInertia.Ramification (4.7s)
✔ [3372/3405] Built Mathlib.RingTheory.Ideal.Norm.AbsNorm (4.9s)
✔ [3373/3405] Built Mathlib.NumberTheory.RamificationInertia.Inertia (2.6s)
✔ [3374/3405] Built Mathlib.RingTheory.DedekindDomain.AdicValuation (11s)
✔ [3375/3405] Built Mathlib.FieldTheory.RatFunc.AsPolynomial (4.6s)
✔ [3376/3405] Built Mathlib.RingTheory.Valuation.Discrete.Basic (5.8s)
✔ [3377/3405] Built Mathlib.NumberTheory.RamificationInertia.Basic (9.7s)
✔ [3378/3405] Built Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (4.2s)
✔ [3379/3405] Built Mathlib.RingTheory.Valuation.Discrete.RankOne (3.5s)
✔ [3380/3405] Built Mathlib.RingTheory.Polynomial.Cyclotomic.Roots (3.1s)
✔ [3381/3405] Built Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (2.8s)
✔ [3382/3405] Built Mathlib.RingTheory.Polynomial.Cyclotomic.Eval (4.1s)
✔ [3383/3405] Built Mathlib.RingTheory.DedekindDomain.Factorization (12s)
✔ [3384/3405] Built Mathlib.NumberTheory.Cyclotomic.Basic (9.6s)
✔ [3385/3405] Built Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (4.1s)
✔ [3386/3405] Built Mathlib.NumberTheory.LegendreSymbol.AddCharacter (2.5s)
✔ [3387/3405] Built Mathlib.NumberTheory.NumberField.Completion.FinitePlace (10s)
✔ [3388/3405] Built Mathlib.NumberTheory.GaussSum (3.1s)
✔ [3389/3405] Built Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum (2.0s)
✔ [3390/3405] Built Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity (2.0s)
✔ [3391/3405] Built Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (2.7s)
✔ [3392/3405] Built Mathlib.Tactic.NormNum.LegendreSymbol (3.2s)
✔ [3393/3405] Built Mathlib.Tactic (1.7s)
✔ [3394/3405] Built Iut.Stage1.CorollarySchema (3.0s)
✔ [3395/3405] Built Iut.Stage1.SourceObligations (2.7s)
✔ [3396/3405] Built Iut.Stage1.IUTSourceScaffold (2.3s)
✔ [3397/3405] Built Iut.Stage1.IUTStage1Data (2.6s)
✔ [3398/3405] Built Iut.Foundations.InitialThetaData (18s)
✔ [3399/3405] Built Iut.Stage1.IUTStage1SourceCore (5.6s)
✔ [3400/3405] Built Iut.Stage1.IUTStage1Remark312Absorption (2.4s)
✔ [3401/3405] Built Iut.Stage1.IUTStage1Source (49s)
✔ [3402/3405] Built Iut.Stage1.IUTStage1Experiments (9.3s)
✔ [3403/3405] Built Iut.Basic (2.4s)
✔ [3404/3405] Built Iut (2.3s)
Build completed successfully (3405 jobs).
blueprint_build exit 1 duration 3s · created 
lake build :blueprint
error: unknown package facet `blueprint`
semantic_extract exit 0 duration 1h 11m · created 
./.apodeixis/tools/lean-semantic-extract.sh

Keyboard shortcuts