Verification run
Run 26
failed commit
da43bbecb5da toolchain lean-v4-31-0 prover lean took 5h 37m · finished 4w ago ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-00000) failed with exit code none (process did not exit cleanly) (toolchain lean-v4-31-0, command: <command argv unavailable>)
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
8542 = 45%, 467 KB/s], Decompressed: 2509
Downloaded: 3925 file(s) [attempted 3934/8542 = 46%, 54 KB/s], Decompressed: 2509
Downloaded: 3959 file(s) [attempted 3968/8542 = 46%, 889 KB/s], Decompressed: 2509
Downloaded: 3997 file(s) [attempted 4006/8542 = 46%, 424 KB/s], Decompressed: 3150
Downloaded: 4034 file(s) [attempted 4043/8542 = 47%, 1117 KB/s], Decompressed: 3150
Downloaded: 4079 file(s) [attempted 4088/8542 = 47%, 4324 KB/s], Decompressed: 3150
Downloaded: 4119 file(s) [attempted 4129/8542 = 48%, 1075 KB/s], Decompressed: 3150
Downloaded: 4154 file(s) [attempted 4164/8542 = 48%, 336 KB/s], Decompressed: 3150
Downloaded: 4191 file(s) [attempted 4201/8542 = 49%, 195 KB/s], Decompressed: 3150
Downloaded: 4228 file(s) [attempted 4239/8542 = 49%, 1403 KB/s], Decompressed: 3150
Downloaded: 4269 file(s) [attempted 4280/8542 = 50%, 513 KB/s], Decompressed: 3150
Downloaded: 4306 file(s) [attempted 4317/8542 = 50%, 223 KB/s], Decompressed: 3150
Downloaded: 4347 file(s) [attempted 4358/8542 = 51%, 184 KB/s], Decompressed: 3150
Downloaded: 4385 file(s) [attempted 4396/8542 = 51%, 230 KB/s], Decompressed: 3150
Downloaded: 4429 file(s) [attempted 4440/8542 = 51%, 194 KB/s], Decompressed: 3150
Downloaded: 4464 file(s) [attempted 4475/8542 = 52%, 95 KB/s], Decompressed: 3150
Downloaded: 4508 file(s) [attempted 4519/8542 = 52%, 441 KB/s], Decompressed: 3150
Downloaded: 4549 file(s) [attempted 4560/8542 = 53%, 3694 KB/s], Decompressed: 3150
Downloaded: 4590 file(s) [attempted 4601/8542 = 53%, 72 KB/s], Decompressed: 3150
Downloaded: 4628 file(s) [attempted 4639/8542 = 54%, 90 KB/s], Decompressed: 3150
Downloaded: 4669 file(s) [attempted 4680/8542 = 54%, 66 KB/s], Decompressed: 3150
Downloaded: 4706 file(s) [attempted 4718/8542 = 55%, 464 KB/s], Decompressed: 3150
Downloaded: 4750 file(s) [attempted 4762/8542 = 55%, 124 KB/s], Decompressed: 3150
Downloaded: 4788 file(s) [attempted 4800/8542 = 56%, 132 KB/s], Decompressed: 3150
Downloaded: 4825 file(s) [attempted 4837/8542 = 56%, 1010 KB/s], Decompressed: 3150
Downloaded: 4863 file(s) [attempted 4875/8542 = 57%, 51 KB/s], Decompressed: 3150
Downloaded: 4904 file(s) [attempted 4916/8542 = 57%, 89 KB/s], Decompressed: 3150
Downloaded: 4949 file(s) [attempted 4961/8542 = 58%, 215 KB/s], Decompressed: 3150
Downloaded: 4992 file(s) [attempted 5005/8542 = 58%, 136 KB/s], Decompressed: 3966
Downloaded: 5030 file(s) [attempted 5043/8542 = 59%, 132 KB/s], Decompressed: 3966
Downloaded: 5071 file(s) [attempted 5084/8542 = 59%, 61 KB/s], Decompressed: 3966
Downloaded: 5109 file(s) [attempted 5122/8542 = 59%, 475 KB/s], Decompressed: 3966
Downloaded: 5146 file(s) [attempted 5159/8542 = 60%, 132 KB/s], Decompressed: 3966
Downloaded: 5194 file(s) [attempted 5207/8542 = 60%, 144 KB/s], Decompressed: 3966
Downloaded: 5235 file(s) [attempted 5248/8542 = 61%, 135 KB/s], Decompressed: 3966
Downloaded: 5276 file(s) [attempted 5289/8542 = 61%, 893 KB/s], Decompressed: 3966
Downloaded: 5310 file(s) [attempted 5323/8542 = 62%, 496 KB/s], Decompressed: 3966
Downloaded: 5352 file(s) [attempted 5365/8542 = 62%, 313 KB/s], Decompressed: 3966
Downloaded: 5396 file(s) [attempted 5409/8542 = 63%, 655 KB/s], Decompressed: 3966
Downloaded: 5444 file(s) [attempted 5457/8542 = 63%, 84 KB/s], Decompressed: 3966
Downloaded: 5492 file(s) [attempted 5505/8542 = 64%, 477 KB/s], Decompressed: 3966
Downloaded: 5534 file(s) [attempted 5547/8542 = 64%, 122 KB/s], Decompressed: 3966
Downloaded: 5571 file(s) [attempted 5584/8542 = 65%, 610 KB/s], Decompressed: 3966
Downloaded: 5605 file(s) [attempted 5618/8542 = 65%, 311 KB/s], Decompressed: 3966
Downloaded: 5646 file(s) [attempted 5659/8542 = 66%, 322 KB/s], Decompressed: 3966
Downloaded: 5692 file(s) [attempted 5705/8542 = 66%, 1389 KB/s], Decompressed: 3966
Downloaded: 5731 file(s) [attempted 5744/8542 = 67%, 436 KB/s], Decompressed: 3966
Downloaded: 5770 file(s) [attempted 5783/8542 = 67%, 291 KB/s], Decompressed: 3966
Downloaded: 5805 file(s) [attempted 5820/8542 = 68%, 376 KB/s], Decompressed: 3966
Downloaded: 5843 file(s) [attempted 5859/8542 = 68%, 731 KB/s], Decompressed: 3966
Downloaded: 5882 file(s) [attempted 5898/8542 = 69%, 626 KB/s], Decompressed: 3966
Downloaded: 5923 file(s) [attempted 5939/8542 = 69%, 166 KB/s], Decompressed: 3966
Downloaded: 5965 file(s) [attempted 5981/8542 = 70%, 394 KB/s], Decompressed: 3966
Downloaded: 6005 file(s) [attempted 6022/8542 = 70%, 73 KB/s], Decompressed: 3966
Downloaded: 6042 file(s) [attempted 6059/8542 = 70%, 52 KB/s], Decompressed: 3966
Downloaded: 6083 file(s) [attempted 6100/8542 = 71%, 59 KB/s], Decompressed: 3966
Downloaded: 6124 file(s) [attempted 6141/8542 = 71%, 235 KB/s], Decompressed: 3966
Downloaded: 6165 file(s) [attempted 6182/8542 = 72%, 417 KB/s], Decompressed: 3966
Downloaded: 6207 file(s) [attempted 6224/8542 = 72%, 42 KB/s], Decompressed: 3966
Downloaded: 6244 file(s) [attempted 6261/8542 = 73%, 61 KB/s], Decompressed: 3966
Downloaded: 6282 file(s) [attempted 6299/8542 = 73%, 1042 KB/s], Decompressed: 3966
Downloaded: 6323 file(s) [attempted 6340/8542 = 74%, 175 KB/s], Decompressed: 3966
Downloaded: 6364 file(s) [attempted 6381/8542 = 74%, 654 KB/s], Decompressed: 4969
Downloaded: 6401 file(s) [attempted 6419/8542 = 75%, 39 KB/s], Decompressed: 4969
Downloaded: 6435 file(s) [attempted 6453/8542 = 75%, 423 KB/s], Decompressed: 4969
Downloaded: 6478 file(s) [attempted 6497/8542 = 76%, 329 KB/s], Decompressed: 4969
Downloaded: 6523 file(s) [attempted 6542/8542 = 76%, 240 KB/s], Decompressed: 4969
Downloaded: 6563 file(s) [attempted 6583/8542 = 77%, 504 KB/s], Decompressed: 4969
Downloaded: 6604 file(s) [attempted 6624/8542 = 77%, 1222 KB/s], Decompressed: 4969
Downloaded: 6642 file(s) [attempted 6662/8542 = 77%, 58 KB/s], Decompressed: 4969
Downloaded: 6679 file(s) [attempted 6699/8542 = 78%, 57 KB/s], Decompressed: 4969
Downloaded: 6724 file(s) [attempted 6744/8542 = 78%, 138 KB/s], Decompressed: 4969
Downloaded: 6768 file(s) [attempted 6788/8542 = 79%, 20 KB/s], Decompressed: 4969
Downloaded: 6809 file(s) [attempted 6829/8542 = 79%, 255 KB/s], Decompressed: 4969
Downloaded: 6850 file(s) [attempted 6870/8542 = 80%, 140 KB/s], Decompressed: 4969
Downloaded: 6895 file(s) [attempted 6915/8542 = 80%, 230 KB/s], Decompressed: 4969
Downloaded: 6925 file(s) [attempted 6946/8542 = 81%, 205 KB/s], Decompressed: 4969
Downloaded: 6972 file(s) [attempted 6994/8542 = 81%, 178 KB/s], Decompressed: 4969
Downloaded: 7016 file(s) [attempted 7038/8542 = 82%, 54 KB/s], Decompressed: 4969
Downloaded: 7056 file(s) [attempted 7079/8542 = 82%, 490 KB/s], Decompressed: 4969
Downloaded: 7097 file(s) [attempted 7120/8542 = 83%, 564 KB/s], Decompressed: 4969
Downloaded: 7142 file(s) [attempted 7165/8542 = 83%, 535 KB/s], Decompressed: 4969
Downloaded: 7173 file(s) [attempted 7196/8542 = 84%, 48 KB/s], Decompressed: 4969
Downloaded: 7220 file(s) [attempted 7243/8542 = 84%, 37 KB/s], Decompressed: 4969
Downloaded: 7262 file(s) [attempted 7285/8542 = 85%, 40 KB/s], Decompressed: 4969
Downloaded: 7306 file(s) [attempted 7329/8542 = 85%, 110 KB/s], Decompressed: 4969
Downloaded: 7344 file(s) [attempted 7367/8542 = 86%, 106 KB/s], Decompressed: 4969
Downloaded: 7385 file(s) [attempted 7408/8542 = 86%, 389 KB/s], Decompressed: 4969
Downloaded: 7422 file(s) [attempted 7445/8542 = 87%, 260 KB/s], Decompressed: 4969
Downloaded: 7459 file(s) [attempted 7483/8542 = 87%, 105 KB/s], Decompressed: 4969
Downloaded: 7504 file(s) [attempted 7528/8542 = 88%, 950 KB/s], Decompressed: 4969
Downloaded: 7548 file(s) [attempted 7572/8542 = 88%, 26 KB/s], Decompressed: 4969
Downloaded: 7582 file(s) [attempted 7606/8542 = 89%, 121 KB/s], Decompressed: 4969
Downloaded: 7630 file(s) [attempted 7654/8542 = 89%, 156 KB/s], Decompressed: 4969
Downloaded: 7664 file(s) [attempted 7688/8542 = 90%, 43 KB/s], Decompressed: 4969
Downloaded: 7705 file(s) [attempted 7729/8542 = 90%, 211 KB/s], Decompressed: 4969
Downloaded: 7750 file(s) [attempted 7774/8542 = 91%, 348 KB/s], Decompressed: 4969
Downloaded: 7794 file(s) [attempted 7818/8542 = 91%, 772 KB/s], Decompressed: 4969
Downloaded: 7834 file(s) [attempted 7859/8542 = 92%, 325 KB/s], Decompressed: 4969
Downloaded: 7876 file(s) [attempted 7901/8542 = 92%, 681 KB/s], Decompressed: 4969
Downloaded: 7913 file(s) [attempted 7938/8542 = 92%, 454 KB/s], Decompressed: 4969
Downloaded: 7954 file(s) [attempted 7979/8542 = 93%, 407 KB/s], Decompressed: 4969
Downloaded: 7995 file(s) [attempted 8020/8542 = 93%, 86 KB/s], Decompressed: 4969
Downloaded: 8043 file(s) [attempted 8068/8542 = 94%, 228 KB/s], Decompressed: 4969
Downloaded: 8081 file(s) [attempted 8106/8542 = 94%, 445 KB/s], Decompressed: 4969
Downloaded: 8122 file(s) [attempted 8147/8542 = 95%, 1815 KB/s], Decompressed: 6330
Downloaded: 8156 file(s) [attempted 8181/8542 = 95%, 602 KB/s], Decompressed: 6330
Downloaded: 8197 file(s) [attempted 8222/8542 = 96%, 366 KB/s], Decompressed: 6330
Downloaded: 8238 file(s) [attempted 8263/8542 = 96%, 48 KB/s], Decompressed: 6330
Downloaded: 8282 file(s) [attempted 8307/8542 = 97%, 876 KB/s], Decompressed: 6330
Downloaded: 8320 file(s) [attempted 8345/8542 = 97%, 1133 KB/s], Decompressed: 6330
Downloaded: 8350 file(s) [attempted 8376/8542 = 98%, 566 KB/s], Decompressed: 6330
Downloaded: 8395 file(s) [attempted 8421/8542 = 98%, 75 KB/s], Decompressed: 6330
Downloaded: 8439 file(s) [attempted 8465/8542 = 99%, 81 KB/s], Decompressed: 6330
Downloaded: 8480 file(s) [attempted 8506/8542 = 99%, 663 KB/s], Decompressed: 6330
Downloaded: 8515 file(s) [attempted 8541/8542 = 99%, 488 KB/s], Decompressed: 6330
Downloaded: 8516 file(s) [attempted 8542/8542 = 100%, 488 KB/s], Decompressed: 6330
Warning: some files were not found in the cache.
This usually means that your local checkout of mathlib4 has diverged from upstream.
* If you push your commits to a PR to the mathlib4 repository
(use a draft PR if it is not ready for review),
then CI will build the oleans and they will be available later.
* If you have already opened a PR, this may mean
the CI build has failed part-way through building.
$ lake build
exit_code=Some(0) duration_ms=947821
stdout:
✔ [1/3] Built FLT.Assumptions.KnownIn1980s (480ms)
✔ [1953/1964] Built FLT.Assumptions.Mazur (21s)
✔ [2948/2955] Built FLT.Deformations.ContinuousRepresentation.IsTopologicalModule (4.6s)
✔ [2951/2956] Built FLT.Mathlib.Algebra.Algebra.Tower (2.0s)
✔ [2955/2958] Built FLT.Assumptions.Odlyzko (9.4s)
✔ [3222/3230] Built FLT.Mathlib.Algebra.FixedPoints.Basic (2.3s)
✔ [3228/3232] Built FLT.Mathlib.Topology.Algebra.Module.ModuleTopology (7.1s)
✔ [3229/3232] Built FLT.Hacks.RightActionInstances (3.9s)
✔ [3310/3327] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.RestrictedProduct (1.5s)
✔ [3311/3327] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Basic (3.0s)
✔ [3312/3327] Built FLT.Mathlib.Topology.Algebra.Module.Quotient (1.7s)
✔ [3313/3327] Built FLT.Mathlib.Topology.Algebra.Group.Units (1.2s)
✔ [3314/3327] Built FLT.Mathlib.Order.Filter.Cofinite (1.1s)
✔ [3316/3327] Built FLT.Mathlib.Topology.Bases (1.2s)
✔ [3318/3327] Built FLT.Mathlib.MeasureTheory.Group.Action (2.3s)
✔ [3319/3327] Built FLT.Mathlib.MeasureTheory.Measure.Typeclasses.Finite (1.5s)
✔ [3320/3327] Built FLT.DedekindDomain.FiniteAdeleRing.TensorPi (3.6s)
✔ [3321/3327] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Equiv (5.4s)
✔ [3323/3327] Built FLT.Mathlib.Topology.Algebra.ContinuousMonoidHom (1.8s)
✔ [3324/3327] Built FLT.Mathlib.MeasureTheory.Group.Measure (1.6s)
✔ [3325/3328] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (5.2s)
✔ [3326/3341] Built FLT.AutomorphicForm.QuaternionAlgebra.Defs (4.9s)
✔ [3332/3341] Built FLT.Mathlib.RingTheory.TensorProduct.Pi (1.4s)
✔ [3335/3348] Built FLT.Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing (10s)
✔ [3337/3349] Built FLT.Mathlib.LinearAlgebra.Dimension.Constructions (1.6s)
✔ [3339/3349] Built FLT.Mathlib.RingTheory.DedekindDomain.AdicValuation (1.9s)
✔ [3340/3349] Built FLT.Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic (1.3s)
✔ [3343/3349] Built FLT.Mathlib.RingTheory.Valuation.ValuationSubring (2.3s)
✔ [3345/3354] Built FLT.HaarMeasure.HaarChar.AddEquiv (6.3s)
✔ [3347/3355] Built FLT.HaarMeasure.HaarChar.Ring (3.2s)
✔ [3349/3355] Built FLT.Mathlib.RingTheory.Ideal.Quotient.Basic (1.1s)
✔ [3350/3356] Built FLT.Mathlib.LinearAlgebra.Countable (1.6s)
✔ [3354/3362] Built FLT.DedekindDomain.AdicValuation (8.6s)
✔ [3361/3382] Built FLT.Mathlib.Topology.Algebra.Valued.WithZeroMulInt (2.5s)
✔ [3371/3382] Built FLT.Mathlib.RingTheory.Localization.BaseChange (2.2s)
✔ [3373/3382] Built FLT.DedekindDomain.IntegralClosure (5.4s)
✔ [3377/3382] Built FLT.Mathlib.NumberTheory.NumberField.InfinitePlace.Completion (1.9s)
✔ [3379/3384] Built FLT.NumberField.HeightOneSpectrum (1.9s)
✔ [3380/3386] Built FLT.NumberField.Completion.Finite (2.6s)
✔ [3382/3391] Built FLT.Mathlib.NumberTheory.NumberField.FiniteAdeleRing (3.3s)
✔ [3387/3400] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.AdicCompletion (1.7s)
✔ [3388/3400] Built FLT.Mathlib.Algebra.Algebra.Hom (2.2s)
✔ [3389/3400] Built FLT.Mathlib.Algebra.Module.Submodule.Basic (1.1s)
✔ [3391/3410] Built FLT.Mathlib.RingTheory.TensorProduct.Basis (1.9s)
✔ [3392/3410] Built FLT.Mathlib.Topology.Algebra.UniformRing (1.4s)
✔ [3393/3410] Built FLT.Mathlib.Algebra.Algebra.Pi (1.5s)
✔ [3395/3410] Built FLT.Mathlib.Algebra.Algebra.Bilinear (2.1s)
✔ [3397/3410] Built FLT.Mathlib.Algebra.IsDirectLimit (2.1s)
✔ [3398/3410] Built FLT.Mathlib.Topology.Algebra.MulAction (1.3s)
✔ [3399/3410] Built FLT.Mathlib.Topology.Algebra.Algebra.Hom (1.8s)
✔ [3402/3414] Built FLT.Mathlib.LinearAlgebra.Pi (1.5s)
✔ [3403/3414] Built FLT.DedekindDomain.FiniteAdeleRing.IsDirectLimitRestricted (1.8s)
✔ [3405/3414] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Module (7.9s)
✔ [3407/3414] Built FLT.Mathlib.NumberTheory.NumberField.InfiniteAdeleRing (3.7s)
✔ [3409/3414] Built FLT.DedekindDomain.Completion.BaseChange (29s)
✔ [3410/3416] Built FLT.DedekindDomain.FiniteAdeleRing.TensorRestrictedProduct (7.6s)
✔ [3411/3429] Built FLT.Mathlib.NumberTheory.NumberField.AdeleRing (2.3s)
✔ [3414/3430] Built FLT.DedekindDomain.FiniteAdeleRing.BaseChange (80s)
✔ [3416/3430] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.FiniteAdeleRing (1.7s)
✔ [3417/3430] Built FLT.Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (1.7s)
✔ [3418/3430] Built FLT.Mathlib.Topology.Algebra.Group.Quotient (1.3s)
✔ [3419/3430] Built FLT.Mathlib.Topology.Algebra.ContinuousAlgEquiv (1.2s)
✔ [3420/3430] Built FLT.NumberField.InfinitePlace.Extension (2.8s)
✔ [3421/3430] Built FLT.Mathlib.Topology.Algebra.Module.FiniteDimension (1.5s)
✔ [3423/3430] Built FLT.Mathlib.Topology.Constructions (1.0s)
✔ [3425/3433] Built FLT.Mathlib.Topology.MetricSpace.Pseudo.Matrix (1.5s)
✔ [3428/3440] Built FLT.Mathlib.Topology.Algebra.Module.Equiv (1.9s)
✔ [3429/3442] Built FLT.Mathlib.Topology.MetricSpace.ProperSpace.InfinitePlace (1.9s)
✔ [3431/3442] Built FLT.NumberField.Padics.RestrictedProduct (2.7s)
✔ [3432/3442] Built FLT.Mathlib.Data.Real.Archimedean (1.1s)
✔ [3433/3442] Built FLT.Mathlib.LinearAlgebra.Matrix.Transvection (1.4s)
✔ [3434/3442] Built FLT.NumberField.Completion.Infinite (16s)
✔ [3435/3442] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.InfinitePlace (1.8s)
✔ [3438/3445] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.AdeleRing (1.8s)
✔ [3439/3445] Built FLT.Mathlib.RingTheory.SimpleRing.TensorProduct (5.9s)
✔ [3440/3445] Built FLT.NumberField.InfiniteAdeleRing (13s)
✔ [3442/3445] Built FLT.NumberField.AdeleRing (22s)
✔ [3449/3467] Built FLT.Mathlib.NumberTheory.Padics.PadicIntegers (1.0s)
✔ [3451/3467] Built FLT.Mathlib.NumberTheory.Padics.HeightOneSpectrum (3.1s)
✔ [3453/3470] Built FLT.HaarMeasure.MeasurableSpacePadics (1.0s)
✔ [3455/3470] Built FLT.Mathlib.LinearAlgebra.TensorProduct.FiniteFree (1.2s)
✔ [3456/3470] Built FLT.Mathlib.LinearAlgebra.TensorProduct.Algebra (1.7s)
✔ [3458/3473] Built FLT.HaarMeasure.HaarChar.RealComplex (2.8s)
✔ [3459/3473] Built FLT.HaarMeasure.HaarChar.Padic (2.8s)
✔ [3461/3473] Built FLT.Mathlib.Topology.Algebra.Module.TensorProduct (2.5s)
✔ [3464/3473] Built FLT.Mathlib.LinearAlgebra.TensorProduct.Basis (1.3s)
✔ [3465/3473] Built FLT.Mathlib.Algebra.Central.TensorProduct (2.3s)
✔ [3466/3473] Built FLT.DedekindDomain.FiniteAdeleRing.TensorProduct (9.2s)
✔ [3468/3473] Built FLT.Mathlib.GroupTheory.DoubleCoset (1.2s)
✔ [3469/3474] Built FLT.Mathlib.LinearAlgebra.Determinant (5.0s)
✔ [3470/3475] Built FLT.HaarMeasure.HaarChar.FiniteDimensional (6.0s)
✔ [3472/3478] Built FLT.HaarMeasure.HaarChar.FiniteAdeleRing (39s)
✔ [3473/3482] Built FLT.HaarMeasure.HaarChar.AdeleRing (22s)
✔ [3483/3492] Built FLT.Mathlib.Topology.HomToDiscrete (1.9s)
✔ [3484/3492] Built FLT.Mathlib.Topology.Polish (1.6s)
✔ [3488/3509] Built FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Abstract (2.4s)
✔ [3490/3509] Built FLT.Mathlib.Topology.Algebra.Valued.ValuationTopology (1.7s)
✔ [3491/3509] Built FLT.Mathlib.Topology.Instances.Matrix (1.5s)
✔ [3492/3509] Built FLT.Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs (1.9s)
✔ [3493/3509] Built FLT.DedekindDomain.FiniteAdeleRing.LocalUnits (3.8s)
✔ [3494/3509] Built FLT.Mathlib.MeasureTheory.Haar.Extension (2.6s)
✔ [3496/3509] Built FLT.Deformations.Algebra.InverseLimit.Basic (5.5s)
✔ [3498/3509] Built FLT.DivisionAlgebra.Finiteness (41s)
✔ [3499/3509] Built FLT.Data.QHat (6.7s)
✔ [3500/3509] Built FLT.Deformations.Algebra.InverseLimit.Topology (3.5s)
✔ [3502/3509] Built FLT.AutomorphicForm.QuaternionAlgebra.FiniteDimensional (3.8s)
✔ [3503/3515] Built FLT.Data.Hurwitz (4.3s)
✔ [3504/3516] Built FLT.Mathlib.Algebra.IsQuaternionAlgebra (2.1s)
✔ [3505/3516] Built FLT.Data.HurwitzRatHat (2.5s)
✔ [3507/3518] Built FLT.QuaternionAlgebra.NumberField (8.3s)
✔ [3510/3518] Built FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Local (6.2s)
✔ [3513/3521] Built FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Concrete (8.9s)
✔ [3515/3521] Built FLT.Patching.Utils.Lemmas (4.1s)
✔ [3519/3525] Built FLT.Patching.Utils.InverseLimit (1.4s)
✔ [3529/3539] Built FLT.Deformations.Lemmas (3.9s)
✔ [3531/3539] Built FLT.Mathlib.RingTheory.LocalRing.Defs (1.3s)
✔ [3533/3539] Built FLT.Deformations.RepresentationTheory.ContinuousSMulDiscrete (1.3s)
✔ [3534/3539] Built FLT.Deformations.IsResidueAlgebra (2.0s)
✔ [3535/3539] Built FLT.Patching.Utils.AdicTopology (3.7s)
✔ [3536/3540] Built FLT.Deformations.Subfunctor (1.0s)
✔ [3537/3540] Built FLT.Deformations.IsProartinian (1.0s)
✔ [3539/3540] Built FLT.Deformations.Categories (3.4s)
✔ [3586/3590] Built FLT.Deformations.RepresentationTheory.IntegralClosure (2.1s)
✔ [3587/3592] Built FLT.Deformations.RepresentationTheory.Frobenius (3.5s)
✔ [3607/3609] Built FLT.Deformations.RepresentationTheory.AbsoluteGaloisGroup (13s)
✔ [3618/3623] Built FLT.Deformations.RepresentationTheory.Etale (9.1s)
✔ [3635/3643] Built FLT.Deformations.RepresentationTheory.GaloisRep (12s)
✔ [3637/3643] Built FLT.Mathlib.RepresentationTheory.Basic (2.3s)
✔ [3640/3644] Built FLT.Deformations.RepresentationTheory.Irreducible (1.4s)
✔ [3642/3644] Built FLT.Deformations.LiftFunctor (3.0s)
✔ [3643/3655] Built FLT.Deformations.Representable (2.9s)
✔ [3653/3658] Built FLT.EllipticCurve.Torsion (2.5s)
✔ [3655/3662] Built FLT.Deformations.RepresentationTheory.GaloisRepFamily (2.1s)
✔ [3820/3833] Built FLT.Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (1.8s)
✔ [3821/3833] Built FLT.GaloisRepresentation.Automorphic (3.0s)
✔ [3823/3833] Built FLT.GaloisRepresentation.Cyclotomic (2.0s)
✔ [3824/3833] Built FLT.GaloisRepresentation.HardlyRamified.Defs (2.6s)
✔ [3826/3833] Built FLT.GaloisRepresentation.HardlyRamified.Threeadic (2.1s)
✔ [3827/3833] Built FLT.GaloisRepresentation.HardlyRamified.ModThree (2.1s)
✔ [3828/3833] Built FLT.GaloisRepresentation.HardlyRamified.Lift (2.1s)
✔ [3829/3833] Built FLT.GaloisRepresentation.HardlyRamified.Family (2.3s)
✔ [3830/3838] Built FLT.FreyCurve.FreyPackage (4.6s)
✔ [3831/3838] Built FLT.GaloisRepresentation.HardlyRamified.Frey (2.1s)
✔ [3833/3839] Built FLT.FreyCurve.Contradiction (1.0s)
✔ [3956/3975] Built FLT.GroupScheme.FiniteFlat (315ms)
✔ [3957/3975] Built FLT.Mathlib.Algebra.Order.AbsoluteValue.Basic (1.4s)
✔ [3958/3975] Built FLT.Mathlib.Analysis.Normed.Ring.WithAbs (1.4s)
✔ [3959/3975] Built FLT.Mathlib.Data.Fin.Basic (920ms)
✔ [3960/3975] Built FLT.Mathlib.Data.Set.Prod (630ms)
✔ [3961/3975] Built FLT.Mathlib.GroupTheory.Index (1.1s)
✔ [3962/3975] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.Padic (1.3s)
✔ [3963/3975] Built FLT.Mathlib.MeasureTheory.Measure.Regular (1.3s)
✔ [3964/3975] Built FLT.Mathlib.NumberTheory.NumberField.Completion (1.3s)
✔ [3966/3975] Built FLT.Mathlib.Topology.Algebra.Monoid (1.3s)
✔ [3972/3980] Built FLT.Mathlib.Topology.Algebra.Order.Field (2.3s)
✔ [3977/3985] Built FLT.GlobalLanglandsConjectures.GLnDefs (8.7s)
✔ [3979/3989] Built FLT.GlobalLanglandsConjectures.GLzero (2.2s)
✔ [3983/3992] Built FLT.Patching.Utils.TopologicallyFG (1.6s)
✔ [3985/3992] Built FLT.NumberField.DiscriminantBounds (2.6s)
✔ [3987/3994] Built FLT.Patching.Utils.StructureFiniteness (3.7s)
✔ [3988/3994] Built FLT.Patching.Ultraproduct (8.2s)
✔ [3990/3994] Built FLT.Patching.Module (11s)
✔ [3991/3994] Built FLT.Patching.Algebra (9.6s)
✔ [3993/4003] Built FLT.Patching.Over (11s)
✔ [4008/4018] Built FLT.Patching.VanishingFilter (2.7s)
✔ [4011/4018] Built FLT.TateCurve.TateCurve (305ms)
✔ [4012/4018] Built FLT.Patching.Utils.CompactHausdorffRings (2.2s)
✔ [4013/4018] Built FLT.Patching.Utils.Depth (2.0s)
✔ [4014/4018] Built FLT.Patching.System (9.6s)
✔ [4015/4018] Built FLT.Patching.REqualsT (3.9s)
✔ [4016/4018] Built FLT (1.9s)
✔ [4017/4018] Built FermatsLastTheorem (96s)
Build completed successfully (4018 jobs).
$ lake build :blueprint
exit_code=Some(1) duration_ms=9050
stderr:
error: unknown package facet `blueprint`
blueprint_build failed; continuing (non-fatal phase).
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-00000)
exit_code=None duration_ms=14400007
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":19329}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":748,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":25,"runner_cache_hit":false}
apx-semantic-phase {"phase":"runner_compile","duration_ms":42832,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache a214ed71bac59bbcc75754a09ff7bffe1dcc31fe1cd9e5b8f7918e5e64522625
/usr/bin/podman timed out after 14400s
podman cleanup removed verifier container apx-verifier-job-532-runtime-semantic_extract-1493713-1781827777936204779-3
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00000)
exit_code=Some(0) duration_ms=462420
stdout:
apx-semantic-phase {"duration_ms":23,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":1,"diagnostic_count":0,"duration_ms":115,"ok":true,"phase":"lean_declaration_extraction","target_module_count":3}
apx-semantic-phase {"declaration_count":1,"dependency_count":1,"diagnostic_count":5,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":376120,"module_count":3,"ok":true,"phase":"lean_module_facts","target_module_count":3}
apx-semantic-phase {"declaration_count":1,"dependency_count":1,"diagnostic_count":5,"duration_ms":64,"module_count":3,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":4845,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":5,"ok":true,"payload_bytes":4845,"phase":"lean_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":1350,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":24,"runner_cache_hit":false}
apx-semantic-phase {"phase":"runner_compile","duration_ms":79002,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 7e90b4e98157ffc2c3aee24cfbe0d24912d70b2489c2a5f1432d7ac4df4fe31d
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":380873,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00001)
exit_code=Some(0) duration_ms=348491
stdout:
apx-semantic-phase {"duration_ms":4,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":1,"duration_ms":151,"ok":true,"phase":"lean_declaration_extraction","target_module_count":2}
apx-semantic-phase {"declaration_count":3,"dependency_count":4,"diagnostic_count":12,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":337851,"module_count":2,"ok":true,"phase":"lean_module_facts","target_module_count":2}
apx-semantic-phase {"declaration_count":3,"dependency_count":4,"diagnostic_count":12,"duration_ms":63,"module_count":2,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":69761,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":69761,"phase":"lean_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":267,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":23,"runner_cache_hit":false}
apx-semantic-phase {"phase":"runner_compile","duration_ms":4650,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache ad6bd113eae3051161554b68ce84f22ffc8f48ab6411af8fad1d1c1a0a520801
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":342884,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00002)
exit_code=Some(0) duration_ms=516391
stdout:
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":177,"ok":true,"phase":"lean_declaration_extraction","target_module_count":2}
apx-semantic-phase {"declaration_count":3,"dependency_count":5,"diagnostic_count":13,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":502116,"module_count":2,"ok":true,"phase":"lean_module_facts","target_module_count":2}
apx-semantic-phase {"declaration_count":3,"dependency_count":5,"diagnostic_count":13,"duration_ms":51,"module_count":2,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":86203,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":86203,"phase":"lean_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":151,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":24,"runner_cache_hit":false}
apx-semantic-phase {"phase":"runner_compile","duration_ms":9187,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache fa0d1ef17bd9d5da728a7ae7abade55f2d75796ebeffd0bb356c9b30cd96f376
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":506303,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00003)
exit_code=Some(0) duration_ms=265396
stdout:
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":12,"diagnostic_count":6,"duration_ms":678,"ok":true,"phase":"lean_declaration_extraction","target_module_count":2}
apx-semantic-phase {"declaration_count":12,"dependency_count":26,"diagnostic_count":101,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":258054,"module_count":2,"ok":true,"phase":"lean_module_facts","target_module_count":2}
apx-semantic-phase {"declaration_count":12,"dependency_count":26,"diagnostic_count":101,"duration_ms":52,"module_count":2,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":178771,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":178771,"phase":"lean_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":12}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":123,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":27,"runner_cache_hit":false}
apx-semantic-phase {"phase":"runner_compile","duration_ms":2953,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 3f9b43e320631d0dd086f39e2658b002540d610d1c6f71ae043e064557bfc3cc
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":261741,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00004)
exit_code=Some(0) duration_ms=215459
stdout:
apx-semantic-phase {"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":4,"diagnostic_count":2,"duration_ms":124,"ok":true,"phase":"lean_declaration_extraction","target_module_count":2}
apx-semantic-phase {"declaration_count":4,"dependency_count":5,"diagnostic_count":19,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":209544,"module_count":2,"ok":true,"phase":"lean_module_facts","target_module_count":2}
apx-semantic-phase {"declaration_count":4,"dependency_count":5,"diagnostic_count":19,"duration_ms":58,"module_count":2,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":28943,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":28943,"phase":"lean_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":24}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":126,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":20,"runner_cache_hit":false}
apx-semantic-phase {"phase":"runner_compile","duration_ms":2528,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 394516ae786dad116689ad17d9acb6f99b38097e4896d88b86e53020dc7e9aa4
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":212203,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00005)
exit_code=Some(0) duration_ms=258674
stdout:
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":4,"diagnostic_count":1,"duration_ms":107,"ok":true,"phase":"lean_declaration_extraction","target_module_count":2}
apx-semantic-phase {"declaration_count":4,"dependency_count":5,"diagnostic_count":10,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":252721,"module_count":2,"ok":true,"phase":"lean_module_facts","target_module_count":2}
apx-semantic-phase {"declaration_count":4,"dependency_count":5,"diagnostic_count":10,"duration_ms":58,"module_count":2,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":117673,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":1,"ok":true,"payload_bytes":117673,"phase":"lean_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":18}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":114,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":23,"runner_cache_hit":false}
apx-semantic-phase {"phase":"runner_compile","duration_ms":2612,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 396d616fa0ca9e215587b67851fe30d2c6c914608c02e085f95d0df7b1dd4d28
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":255335,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00006)
exit_code=Some(0) duration_ms=407240
stdout:
apx-semantic-phase {"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":156,"ok":true,"phase":"lean_declaration_extraction","target_module_count":2}
apx-semantic-phase {"declaration_count":3,"dependency_count":2,"diagnostic_count":13,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":395629,"module_count":2,"ok":true,"phase":"lean_module_facts","target_module_count":2}
apx-semantic-phase {"declaration_count":3,"dependency_count":2,"diagnostic_count":13,"duration_ms":44,"module_count":2,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":59255,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":59255,"phase":"lean_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":25}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":132,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":27,"runner_cache_hit":false}
apx-semantic-phase {"phase":"runner_compile","duration_ms":7187,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache cffaad1d1e7cfe30c8d49d31822f15fc1dd0167038536ecc231d87674f3f4387
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":399231,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00007)
exit_code=Some(0) duration_ms=383346
stdout:
apx-semantic-phase {"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":19,"diagnostic_count":7,"duration_ms":820,"ok":true,"phase":"lean_declaration_extraction","target_module_count":2}
apx-semantic-phase {"declaration_count":19,"dependency_count":34,"diagnostic_count":47,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":375517,"module_count":2,"ok":true,"phase":"lean_module_facts","target_module_count":2}
apx-semantic-phase {"declaration_count":19,"dependency_count":34,"diagnostic_count":47,"duration_ms":101,"module_count":2,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":1330851,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":1,"ok":true,"payload_bytes":1330851,"phase":"lean_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":138,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":23,"runner_cache_hit":false}
apx-semantic-phase {"phase":"runner_compile","duration_ms":2990,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 6d0ed87a85be8855db2ae8513564e9b27f46b9d50cb78249ac5c5c7201dc5124
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":379572,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00008)
exit_code=Some(0) duration_ms=300525
stdout:
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":51,"diagnostic_count":27,"duration_ms":1817,"ok":true,"phase":"lean_declaration_extraction","target_module_count":2}
apx-semantic-phase {"declaration_count":51,"dependency_count":136,"diagnostic_count":249,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":291993,"module_count":2,"ok":true,"phase":"lean_module_facts","target_module_count":2}
apx-semantic-phase {"declaration_count":51,"dependency_count":136,"diagnostic_count":249,"duration_ms":94,"module_count":2,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":995985,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":995985,"phase":"lean_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":26}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":125,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":28,"runner_cache_hit":false}
apx-semantic-phase {"phase":"runner_compile","duration_ms":2847,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 7981a28a6d86a8db117687e32960fe1490babd291dc367302417a51b48b50402
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":296840,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00009)
exit_code=Some(0) duration_ms=236475
stdout:
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":105,"diagnostic_count":60,"duration_ms":3583,"ok":true,"phase":"lean_declaration_extraction","target_module_count":2}
apx-semantic-phase {"declaration_count":105,"dependency_count":236,"diagnostic_count":90,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":226947,"module_count":2,"ok":true,"phase":"lean_module_facts","target_module_count":2}
apx-semantic-phase {"declaration_count":105,"dependency_count":236,"diagnostic_count":90,"duration_ms":121,"module_count":2,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":1634320,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":1,"ok":true,"payload_bytes":1634320,"phase":"lean_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":21}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":132,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":21,"runner_cache_hit":false}
apx-semantic-phase {"phase":"runner_compile","duration_ms":2420,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache e9b1c83c8cc6c05bb8d095340ebf47607e20a2300835fa3e3f72f6a22e6a6964
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":233301,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00010)
exit_code=Some(0) duration_ms=473397
stdout:
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":108,"diagnostic_count":42,"duration_ms":4333,"ok":true,"phase":"lean_declaration_extraction","target_module_count":2}
apx-semantic-phase {"declaration_count":108,"dependency_count":338,"diagnostic_count":219,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":460585,"module_count":2,"ok":true,"phase":"lean_module_facts","target_module_count":2}
apx-semantic-phase {"declaration_count":108,"dependency_count":338,"diagnostic_count":219,"duration_ms":136,"module_count":2,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":1840480,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":2,"ok":true,"payload_bytes":1840480,"phase":"lean_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":148,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":24,"runner_cache_hit":false}
apx-semantic-phase {"phase":"runner_compile","duration_ms":4006,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache d26fa8fa5556b8c49f82fa59e90f6e05fbb1ce574cde3eacb3f0dde5e4b253f4
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":468546,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00011)
exit_code=Some(0) duration_ms=448701
stdout:
apx-semantic-phase {"duration_ms":22,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":1,"diagnostic_count":0,"duration_ms":127,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":1,"dependency_count":1,"diagnostic_count":2,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":417696,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":1,"dependency_count":1,"diagnostic_count":2,"duration_ms":64,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":4881,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":5,"ok":true,"payload_bytes":4881,"phase":"lean_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":111,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":22,"runner_cache_hit":false}
apx-semantic-phase {"phase":"runner_compile","duration_ms":24147,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 24c783e79ba0c36581546b5ab6a28d92330e9dc91b569bf18c093cc17b9b4806
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":423678,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00012)
exit_code=Some(0) duration_ms=193802
stdout:
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":2,"diagnostic_count":0,"duration_ms":141,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":2,"dependency_count":1,"diagnostic_count":0,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":185702,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":2,"dependency_count":1,"diagnostic_count":0,"duration_ms":53,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":7020,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":2,"ok":true,"payload_bytes":7020,"phase":"lean_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":24}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":250,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":25,"runner_cache_hit":false}
apx-semantic-phase {"phase":"runner_compile","duration_ms":3111,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 15a4c5adfd8bda418e61dc203baaedf8c0930b226feac8a3d515c9c4530db60c
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":189717,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00013)
exit_code=Some(1) duration_ms=5
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00014)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00015)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00016)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00017)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00018)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00019)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00020)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00021)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00022)
exit_code=Some(1) duration_ms=5
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00023)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00024)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00025)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00026)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00027)
exit_code=Some(1) duration_ms=3
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00028)
exit_code=Some(1) duration_ms=3
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00029)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00030)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00031)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00032)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00033)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00034)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00035)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00036)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00037)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00038)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00039)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00040)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00041)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00042)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00043)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00044)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00045)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00046)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00047)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00048)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00049)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00050)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00051)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00052)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00053)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00054)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00055)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00056)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00057)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00058)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00059)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00060)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00061)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00062)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00063)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00064)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00065)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00066)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00067)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00068)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00069)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00070)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00071)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00072)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00073)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00074)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00075)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00076)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00077)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00078)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00079)
exit_code=Some(1) duration_ms=5
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00080)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00081)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00082)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00083)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00084)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00085)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00086)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00087)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00088)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00089)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00090)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00091)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00092)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00093)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00094)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00095)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00096)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00097)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00098)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00099)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00100)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00101)
exit_code=Some(1) duration_ms=5
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00102)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00103)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00104)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00105)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00106)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00107)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00108)
exit_code=Some(1) duration_ms=5
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00109)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00110)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00111)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00112)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00113)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00114)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00115)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00116)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00117)
exit_code=Some(1) duration_ms=5
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00118)
exit_code=Some(1) duration_ms=5
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00119)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00120)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00121)
exit_code=Some(1) duration_ms=2
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00122)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00123)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00124)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00125)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00126)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00127)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00128)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00129)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00130)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00131)
exit_code=Some(1) duration_ms=4
stderr:
error getting current working directory: No such file or directory
Stored Lean workspace build cache
Mirrored 8 Lean dependency package snapshot(s)
Created 8 shared Lean git mirror(s)
Command runs
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00060)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00061)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00062)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00063)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00064)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00065)
error getting current working directory: No such file or directory
git_clone exit 0
git clone --depth 1 --branch main --single-branch https://github.com/ImperialCollegeLondon/FLT.git /var/lib/apodeixis/repos/job-532-source
Cloning into '/var/lib/apodeixis/repos/job-532-source'...
git_checkout exit 0
git checkout da43bbecb5dafc86686181188c69b16ef47895b5
Note: switching to 'da43bbecb5dafc86686181188c69b16ef47895b5'. 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 da43bbe chore: bump to v4.31 (#1026)
lake_cache exit 0
lake exe cache get
Current branch: HEAD Using cache (Azure) from origin: (some leanprover-community/mathlib4) Attempting to download 8542 file(s) from leanprover-community/mathlib4 cache Decompressed 8516 file(s) Already decompressed 8516 file(s)
info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git
info: mathlib: checking out revision 'fabf563a7c95a166b8d7b6efca11c8b4dc9d911f'
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision '63045536fe95024e6c18fc7b48e03f506701c5bc'
info: importGraph: cloning https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision '5c7542ed018c78194f1e2b903eaf6a792b74c03d'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision '24b0d9dc081c5423f8eec7e866c441e5184f29d9'
info: aesop: cloning https://github.com/leanprover-community/aesop
info: aesop: checking out revision 'e3cb2f741431ce31bf73549fb52316a57368b06f'
info: Qq: cloning https://github.com/leanprover-community/quote4
info: Qq: checking out revision 'f46324995fca5f0483b742e4eb4daec7f4ee50d2'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision 'fa08db58b30eb033edcdab331bba000827f9f785'
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision '92564e5770e4d09f2d86dfbf8ada1e9c715b384c'
✔ [3/6] Built Batteries.Data.Array.Match (1.7s)
✔ [4/6] Built Batteries.Data.String.Basic (417ms)
✔ [5/10] Built Batteries.Data.String.Matcher (545ms)
✔ [7/24] Built Cache.Lean (555ms)
✔ [8/24] Built Batteries.Tactic.OpenPrivate (1.2s)
✔ [9/24] Built Batteries.Data.Array.Match:c.o (1.8s)
✔ [10/24] Built Batteries.Data.String.Basic:c.o (130ms)
✔ [11/24] Built Batteries.Data.String.Matcher:c.o (181ms)
✔ [12/24] Built Cache.Lean:c.o (158ms)
✔ [13/24] Built Batteries.Tactic.OpenPrivate:c.o (941ms)
✔ [14/24] Built Cache.Init (396ms)
✔ [15/24] Built Cache.IO (1.8s)
✔ [16/24] Built Cache.Init:c.o (90ms)
✔ [17/24] Built Cache.IO:c.o (1.2s)
✔ [18/24] Built Cache.Hashing (1.0s)
✔ [19/24] Built Cache.Hashing:c.o (357ms)
✔ [20/24] Built Cache.Requests (2.1s)
✔ [21/24] Built Cache.Requests:c.o (1.8s)
✔ [22/24] Built Cache.Main (1.1s)
✔ [23/24] Built Cache.Main:c.o (525ms)
✔ [24/24] Built cache:exe (7.1s)
Downloaded: 1 file(s) [attempted 1/8542 = 0%, 9 KB/s], Decompressed: 0
Downloaded: 16 file(s) [attempted 16/8542 = 0%, 3 KB/s], Decompressed: 0
Downloaded: 37 file(s) [attempted 37/8542 = 0%, 123 KB/s], Decompressed: 0
Downloaded: 61 file(s) [attempted 61/8542 = 0%, 56 KB/s], Decompressed: 0
Downloaded: 85 file(s) [attempted 86/8542 = 1%, 50 KB/s], Decompressed: 0
Downloaded: 116 file(s) [attempted 117/8542 = 1%, 118 KB/s], Decompressed: 0
Downloaded: 150 file(s) [attempted 151/8542 = 1%, 120 KB/s], Decompressed: 0
Downloaded: 188 file(s) [attempted 189/8542 = 2%, 123 KB/s], Decompressed: 0
Downloaded: 222 file(s) [attempted 223/8542 = 2%, 1546 KB/s], Decompressed: 0
Downloaded: 260 file(s) [attempted 261/8542 = 3%, 191 KB/s], Decompressed: 1
Downloaded: 298 file(s) [attempted 299/8542 = 3%, 513 KB/s], Decompressed: 1
Downloaded: 335 file(s) [attempted 336/8542 = 3%, 167 KB/s], Decompressed: 1
Downloaded: 373 file(s) [attempted 374/8542 = 4%, 604 KB/s], Decompressed: 1
Downloaded: 414 file(s) [attempted 415/8542 = 4%, 462 KB/s], Decompressed: 1
Downloaded: 455 file(s) [attempted 456/8542 = 5%, 1217 KB/s], Decompressed: 1
Downloaded: 493 file(s) [attempted 494/8542 = 5%, 283 KB/s], Decompressed: 1
Downloaded: 534 file(s) [attempted 535/8542 = 6%, 245 KB/s], Decompressed: 1
Downloaded: 568 file(s) [attempted 569/8542 = 6%, 561 KB/s], Decompressed: 246
Downloaded: 609 file(s) [attempted 610/8542 = 7%, 213 KB/s], Decompressed: 246
Downloaded: 650 file(s) [attempted 651/8542 = 7%, 209 KB/s], Decompressed: 246
Downloaded: 688 file(s) [attempted 689/8542 = 8%, 55 KB/s], Decompressed: 246
Downloaded: 733 file(s) [attempted 734/8542 = 8%, 71 KB/s], Decompressed: 246
Downloaded: 767 file(s) [attempted 768/8542 = 8%, 50 KB/s], Decompressed: 246
Downloaded: 801 file(s) [attempted 802/8542 = 9%, 137 KB/s], Decompressed: 246
Downloaded: 839 file(s) [attempted 840/8542 = 9%, 208 KB/s], Decompressed: 246
Downloaded: 876 file(s) [attempted 878/8542 = 10%, 379 KB/s], Decompressed: 246
Downloaded: 913 file(s) [attempted 915/8542 = 10%, 104 KB/s], Decompressed: 246
Downloaded: 951 file(s) [attempted 953/8542 = 11%, 325 KB/s], Decompressed: 568
Downloaded: 982 file(s) [attempted 984/8542 = 11%, 582 KB/s], Decompressed: 568
Downloaded: 1019 file(s) [attempted 1021/8542 = 11%, 586 KB/s], Decompressed: 568
Downloaded: 1057 file(s) [attempted 1059/8542 = 12%, 184 KB/s], Decompressed: 568
Downloaded: 1102 file(s) [attempted 1104/8542 = 12%, 397 KB/s], Decompressed: 568
Downloaded: 1143 file(s) [attempted 1145/8542 = 13%, 104 KB/s], Decompressed: 568
Downloaded: 1180 file(s) [attempted 1182/8542 = 13%, 815 KB/s], Decompressed: 568
Downloaded: 1211 file(s) [attempted 1213/8542 = 14%, 549 KB/s], Decompressed: 568
Downloaded: 1245 file(s) [attempted 1247/8542 = 14%, 34 KB/s], Decompressed: 568
Downloaded: 1279 file(s) [attempted 1282/8542 = 15%, 319 KB/s], Decompressed: 568
Downloaded: 1313 file(s) [attempted 1316/8542 = 15%, 99 KB/s], Decompressed: 937
Downloaded: 1340 file(s) [attempted 1343/8542 = 15%, 217 KB/s], Decompressed: 937
Downloaded: 1361 file(s) [attempted 1364/8542 = 15%, 271 KB/s], Decompressed: 937
Downloaded: 1387 file(s) [attempted 1390/8542 = 16%, 100 KB/s], Decompressed: 937
Downloaded: 1405 file(s) [attempted 1408/8542 = 16%, 597 KB/s], Decompressed: 937
Downloaded: 1433 file(s) [attempted 1436/8542 = 16%, 125 KB/s], Decompressed: 937
Downloaded: 1467 file(s) [attempted 1470/8542 = 17%, 192 KB/s], Decompressed: 937
Downloaded: 1503 file(s) [attempted 1507/8542 = 17%, 1 KB/s], Decompressed: 937
Downloaded: 1543 file(s) [attempted 1548/8542 = 18%, 150 KB/s], Decompressed: 937
Downloaded: 1585 file(s) [attempted 1590/8542 = 18%, 264 KB/s], Decompressed: 937
Downloaded: 1626 file(s) [attempted 1631/8542 = 19%, 194 KB/s], Decompressed: 1299
Downloaded: 1663 file(s) [attempted 1668/8542 = 19%, 83 KB/s], Decompressed: 1299
Downloaded: 1701 file(s) [attempted 1706/8542 = 19%, 181 KB/s], Decompressed: 1299
Downloaded: 1742 file(s) [attempted 1747/8542 = 20%, 310 KB/s], Decompressed: 1299
Downloaded: 1780 file(s) [attempted 1785/8542 = 20%, 475 KB/s], Decompressed: 1299
Downloaded: 1824 file(s) [attempted 1829/8542 = 21%, 310 KB/s], Decompressed: 1299
Downloaded: 1865 file(s) [attempted 1870/8542 = 21%, 24 KB/s], Decompressed: 1299
Downloaded: 1906 file(s) [attempted 1911/8542 = 22%, 714 KB/s], Decompressed: 1299
Downloaded: 1944 file(s) [attempted 1949/8542 = 22%, 247 KB/s], Decompressed: 1299
Downloaded: 1982 file(s) [attempted 1987/8542 = 23%, 45 KB/s], Decompressed: 1299
Downloaded: 2023 file(s) [attempted 2028/8542 = 23%, 53 KB/s], Decompressed: 1622
Downloaded: 2067 file(s) [attempted 2072/8542 = 24%, 192 KB/s], Decompressed: 1622
Downloaded: 2112 file(s) [attempted 2117/8542 = 24%, 328 KB/s], Decompressed: 1622
Downloaded: 2149 file(s) [attempted 2154/8542 = 25%, 933 KB/s], Decompressed: 1622
Downloaded: 2187 file(s) [attempted 2192/8542 = 25%, 180 KB/s], Decompressed: 1622
Downloaded: 2225 file(s) [attempted 2230/8542 = 26%, 263 KB/s], Decompressed: 1622
Downloaded: 2268 file(s) [attempted 2273/8542 = 26%, 882 KB/s], Decompressed: 1622
Downloaded: 2307 file(s) [attempted 2312/8542 = 27%, 20 KB/s], Decompressed: 1622
Downloaded: 2348 file(s) [attempted 2353/8542 = 27%, 38 KB/s], Decompressed: 1622
Downloaded: 2385 file(s) [attempted 2390/8542 = 27%, 137 KB/s], Decompressed: 1622
Downloaded: 2433 file(s) [attempted 2438/8542 = 28%, 44 KB/s], Decompressed: 1622
Downloaded: 2478 file(s) [attempted 2483/8542 = 29%, 66 KB/s], Decompressed: 1622
Downloaded: 2522 file(s) [attempted 2527/8542 = 29%, 92 KB/s], Decompressed: 2016
Downloaded: 2560 file(s) [attempted 2565/8542 = 30%, 58 KB/s], Decompressed: 2016
Downloaded: 2598 file(s) [attempted 2603/8542 = 30%, 360 KB/s], Decompressed: 2016
Downloaded: 2635 file(s) [attempted 2640/8542 = 30%, 23 KB/s], Decompressed: 2016
Downloaded: 2680 file(s) [attempted 2685/8542 = 31%, 48 KB/s], Decompressed: 2016
Downloaded: 2721 file(s) [attempted 2726/8542 = 31%, 80 KB/s], Decompressed: 2016
Downloaded: 2758 file(s) [attempted 2763/8542 = 32%, 133 KB/s], Decompressed: 2016
Downloaded: 2806 file(s) [attempted 2811/8542 = 32%, 525 KB/s], Decompressed: 2016
Downloaded: 2854 file(s) [attempted 2859/8542 = 33%, 50 KB/s], Decompressed: 2016
Downloaded: 2895 file(s) [attempted 2900/8542 = 33%, 22 KB/s], Decompressed: 2016
Downloaded: 2930 file(s) [attempted 2935/8542 = 34%, 87 KB/s], Decompressed: 2016
Downloaded: 2966 file(s) [attempted 2972/8542 = 34%, 226 KB/s], Decompressed: 2016
Downloaded: 3007 file(s) [attempted 3013/8542 = 35%, 214 KB/s], Decompressed: 2016
Downloaded: 3051 file(s) [attempted 3058/8542 = 35%, 154 KB/s], Decompressed: 2016
Downloaded: 3095 file(s) [attempted 3102/8542 = 36%, 35 KB/s], Decompressed: 2016
Downloaded: 3134 file(s) [attempted 3141/8542 = 36%, 193 KB/s], Decompressed: 2016
Downloaded: 3171 file(s) [attempted 3178/8542 = 37%, 188 KB/s], Decompressed: 2509
Downloaded: 3212 file(s) [attempted 3219/8542 = 37%, 38 KB/s], Decompressed: 2509
Downloaded: 3249 file(s) [attempted 3256/8542 = 38%, 143 KB/s], Decompressed: 2509
Downloaded: 3297 file(s) [attempted 3304/8542 = 38%, 83 KB/s], Decompressed: 2509
Downloaded: 3344 file(s) [attempted 3352/8542 = 39%, 204 KB/s], Decompressed: 2509
Downloaded: 3385 file(s) [attempted 3393/8542 = 39%, 117 KB/s], Decompressed: 2509
Downloaded: 3423 file(s) [attempted 3431/8542 = 40%, 771 KB/s], Decompressed: 2509
Downloaded: 3460 file(s) [attempted 3468/8542 = 40%, 413 KB/s], Decompressed: 2509
Downloaded: 3498 file(s) [attempted 3506/8542 = 41%, 243 KB/s], Decompressed: 2509
Downloaded: 3543 file(s) [attempted 3551/8542 = 41%, 78 KB/s], Decompressed: 2509
Downloaded: 3589 file(s) [attempted 3598/8542 = 42%, 23 KB/s], Decompressed: 2509
Downloaded: 3631 file(s) [attempted 3640/8542 = 42%, 1341 KB/s], Decompressed: 2509
Downloaded: 3668 file(s) [attempted 3677/8542 = 43%, 380 KB/s], Decompressed: 2509
Downloaded: 3709 file(s) [attempted 3718/8542 = 43%, 196 KB/s], Decompressed: 2509
Downloaded: 3745 file(s) [attempted 3754/8542 = 43%, 238 KB/s], Decompressed: 2509
Downloaded: 3791 file(s) [attempted 3800/8542 = 44%, 483 KB/s], Decompressed: 2509
Downloaded: 3839 file(s) [attempted 3848/8542 = 45%, 402 KB/s], Decompressed: 2509
Downloaded: 3884 file(s) [attempted 3893/8542 = 45%, 467 KB/s], Decompressed: 2509
Downloaded: 3925 file(s) [attempted 3934/8542 = 46%, 54 KB/s], Decompressed: 2509
Downloaded: 3959 file(s) [attempted 3968/8542 = 46%, 889 KB/s], Decompressed: 2509
Downloaded: 3997 file(s) [attempted 4006/8542 = 46%, 424 KB/s], Decompressed: 3150
Downloaded: 4034 file(s) [attempted 4043/8542 = 47%, 1117 KB/s], Decompressed: 3150
Downloaded: 4079 file(s) [attempted 4088/8542 = 47%, 4324 KB/s], Decompressed: 3150
Downloaded: 4119 file(s) [attempted 4129/8542 = 48%, 1075 KB/s], Decompressed: 3150
Downloaded: 4154 file(s) [attempted 4164/8542 = 48%, 336 KB/s], Decompressed: 3150
Downloaded: 4191 file(s) [attempted 4201/8542 = 49%, 195 KB/s], Decompressed: 3150
Downloaded: 4228 file(s) [attempted 4239/8542 = 49%, 1403 KB/s], Decompressed: 3150
Downloaded: 4269 file(s) [attempted 4280/8542 = 50%, 513 KB/s], Decompressed: 3150
Downloaded: 4306 file(s) [attempted 4317/8542 = 50%, 223 KB/s], Decompressed: 3150
Downloaded: 4347 file(s) [attempted 4358/8542 = 51%, 184 KB/s], Decompressed: 3150
Downloaded: 4385 file(s) [attempted 4396/8542 = 51%, 230 KB/s], Decompressed: 3150
Downloaded: 4429 file(s) [attempted 4440/8542 = 51%, 194 KB/s], Decompressed: 3150
Downloaded: 4464 file(s) [attempted 4475/8542 = 52%, 95 KB/s], Decompressed: 3150
Downloaded: 4508 file(s) [attempted 4519/8542 = 52%, 441 KB/s], Decompressed: 3150
Downloaded: 4549 file(s) [attempted 4560/8542 = 53%, 3694 KB/s], Decompressed: 3150
Downloaded: 4590 file(s) [attempted 4601/8542 = 53%, 72 KB/s], Decompressed: 3150
Downloaded: 4628 file(s) [attempted 4639/8542 = 54%, 90 KB/s], Decompressed: 3150
Downloaded: 4669 file(s) [attempted 4680/8542 = 54%, 66 KB/s], Decompressed: 3150
Downloaded: 4706 file(s) [attempted 4718/8542 = 55%, 464 KB/s], Decompressed: 3150
Downloaded: 4750 file(s) [attempted 4762/8542 = 55%, 124 KB/s], Decompressed: 3150
Downloaded: 4788 file(s) [attempted 4800/8542 = 56%, 132 KB/s], Decompressed: 3150
Downloaded: 4825 file(s) [attempted 4837/8542 = 56%, 1010 KB/s], Decompressed: 3150
Downloaded: 4863 file(s) [attempted 4875/8542 = 57%, 51 KB/s], Decompressed: 3150
Downloaded: 4904 file(s) [attempted 4916/8542 = 57%, 89 KB/s], Decompressed: 3150
Downloaded: 4949 file(s) [attempted 4961/8542 = 58%, 215 KB/s], Decompressed: 3150
Downloaded: 4992 file(s) [attempted 5005/8542 = 58%, 136 KB/s], Decompressed: 3966
Downloaded: 5030 file(s) [attempted 5043/8542 = 59%, 132 KB/s], Decompressed: 3966
Downloaded: 5071 file(s) [attempted 5084/8542 = 59%, 61 KB/s], Decompressed: 3966
Downloaded: 5109 file(s) [attempted 5122/8542 = 59%, 475 KB/s], Decompressed: 3966
Downloaded: 5146 file(s) [attempted 5159/8542 = 60%, 132 KB/s], Decompressed: 3966
Downloaded: 5194 file(s) [attempted 5207/8542 = 60%, 144 KB/s], Decompressed: 3966
Downloaded: 5235 file(s) [attempted 5248/8542 = 61%, 135 KB/s], Decompressed: 3966
Downloaded: 5276 file(s) [attempted 5289/8542 = 61%, 893 KB/s], Decompressed: 3966
Downloaded: 5310 file(s) [attempted 5323/8542 = 62%, 496 KB/s], Decompressed: 3966
Downloaded: 5352 file(s) [attempted 5365/8542 = 62%, 313 KB/s], Decompressed: 3966
Downloaded: 5396 file(s) [attempted 5409/8542 = 63%, 655 KB/s], Decompressed: 3966
Downloaded: 5444 file(s) [attempted 5457/8542 = 63%, 84 KB/s], Decompressed: 3966
Downloaded: 5492 file(s) [attempted 5505/8542 = 64%, 477 KB/s], Decompressed: 3966
Downloaded: 5534 file(s) [attempted 5547/8542 = 64%, 122 KB/s], Decompressed: 3966
Downloaded: 5571 file(s) [attempted 5584/8542 = 65%, 610 KB/s], Decompressed: 3966
Downloaded: 5605 file(s) [attempted 5618/8542 = 65%, 311 KB/s], Decompressed: 3966
Downloaded: 5646 file(s) [attempted 5659/8542 = 66%, 322 KB/s], Decompressed: 3966
Downloaded: 5692 file(s) [attempted 5705/8542 = 66%, 1389 KB/s], Decompressed: 3966
Downloaded: 5731 file(s) [attempted 5744/8542 = 67%, 436 KB/s], Decompressed: 3966
Downloaded: 5770 file(s) [attempted 5783/8542 = 67%, 291 KB/s], Decompressed: 3966
Downloaded: 5805 file(s) [attempted 5820/8542 = 68%, 376 KB/s], Decompressed: 3966
Downloaded: 5843 file(s) [attempted 5859/8542 = 68%, 731 KB/s], Decompressed: 3966
Downloaded: 5882 file(s) [attempted 5898/8542 = 69%, 626 KB/s], Decompressed: 3966
Downloaded: 5923 file(s) [attempted 5939/8542 = 69%, 166 KB/s], Decompressed: 3966
Downloaded: 5965 file(s) [attempted 5981/8542 = 70%, 394 KB/s], Decompressed: 3966
Downloaded: 6005 file(s) [attempted 6022/8542 = 70%, 73 KB/s], Decompressed: 3966
Downloaded: 6042 file(s) [attempted 6059/8542 = 70%, 52 KB/s], Decompressed: 3966
Downloaded: 6083 file(s) [attempted 6100/8542 = 71%, 59 KB/s], Decompressed: 3966
Downloaded: 6124 file(s) [attempted 6141/8542 = 71%, 235 KB/s], Decompressed: 3966
Downloaded: 6165 file(s) [attempted 6182/8542 = 72%, 417 KB/s], Decompressed: 3966
Downloaded: 6207 file(s) [attempted 6224/8542 = 72%, 42 KB/s], Decompressed: 3966
Downloaded: 6244 file(s) [attempted 6261/8542 = 73%, 61 KB/s], Decompressed: 3966
Downloaded: 6282 file(s) [attempted 6299/8542 = 73%, 1042 KB/s], Decompressed: 3966
Downloaded: 6323 file(s) [attempted 6340/8542 = 74%, 175 KB/s], Decompressed: 3966
Downloaded: 6364 file(s) [attempted 6381/8542 = 74%, 654 KB/s], Decompressed: 4969
Downloaded: 6401 file(s) [attempted 6419/8542 = 75%, 39 KB/s], Decompressed: 4969
Downloaded: 6435 file(s) [attempted 6453/8542 = 75%, 423 KB/s], Decompressed: 4969
Downloaded: 6478 file(s) [attempted 6497/8542 = 76%, 329 KB/s], Decompressed: 4969
Downloaded: 6523 file(s) [attempted 6542/8542 = 76%, 240 KB/s], Decompressed: 4969
Downloaded: 6563 file(s) [attempted 6583/8542 = 77%, 504 KB/s], Decompressed: 4969
Downloaded: 6604 file(s) [attempted 6624/8542 = 77%, 1222 KB/s], Decompressed: 4969
Downloaded: 6642 file(s) [attempted 6662/8542 = 77%, 58 KB/s], Decompressed: 4969
Downloaded: 6679 file(s) [attempted 6699/8542 = 78%, 57 KB/s], Decompressed: 4969
Downloaded: 6724 file(s) [attempted 6744/8542 = 78%, 138 KB/s], Decompressed: 4969
Downloaded: 6768 file(s) [attempted 6788/8542 = 79%, 20 KB/s], Decompressed: 4969
Downloaded: 6809 file(s) [attempted 6829/8542 = 79%, 255 KB/s], Decompressed: 4969
Downloaded: 6850 file(s) [attempted 6870/8542 = 80%, 140 KB/s], Decompressed: 4969
Downloaded: 6895 file(s) [attempted 6915/8542 = 80%, 230 KB/s], Decompressed: 4969
Downloaded: 6925 file(s) [attempted 6946/8542 = 81%, 205 KB/s], Decompressed: 4969
Downloaded: 6972 file(s) [attempted 6994/8542 = 81%, 178 KB/s], Decompressed: 4969
Downloaded: 7016 file(s) [attempted 7038/8542 = 82%, 54 KB/s], Decompressed: 4969
Downloaded: 7056 file(s) [attempted 7079/8542 = 82%, 490 KB/s], Decompressed: 4969
Downloaded: 7097 file(s) [attempted 7120/8542 = 83%, 564 KB/s], Decompressed: 4969
Downloaded: 7142 file(s) [attempted 7165/8542 = 83%, 535 KB/s], Decompressed: 4969
Downloaded: 7173 file(s) [attempted 7196/8542 = 84%, 48 KB/s], Decompressed: 4969
Downloaded: 7220 file(s) [attempted 7243/8542 = 84%, 37 KB/s], Decompressed: 4969
Downloaded: 7262 file(s) [attempted 7285/8542 = 85%, 40 KB/s], Decompressed: 4969
Downloaded: 7306 file(s) [attempted 7329/8542 = 85%, 110 KB/s], Decompressed: 4969
Downloaded: 7344 file(s) [attempted 7367/8542 = 86%, 106 KB/s], Decompressed: 4969
Downloaded: 7385 file(s) [attempted 7408/8542 = 86%, 389 KB/s], Decompressed: 4969
Downloaded: 7422 file(s) [attempted 7445/8542 = 87%, 260 KB/s], Decompressed: 4969
Downloaded: 7459 file(s) [attempted 7483/8542 = 87%, 105 KB/s], Decompressed: 4969
Downloaded: 7504 file(s) [attempted 7528/8542 = 88%, 950 KB/s], Decompressed: 4969
Downloaded: 7548 file(s) [attempted 7572/8542 = 88%, 26 KB/s], Decompressed: 4969
Downloaded: 7582 file(s) [attempted 7606/8542 = 89%, 121 KB/s], Decompressed: 4969
Downloaded: 7630 file(s) [attempted 7654/8542 = 89%, 156 KB/s], Decompressed: 4969
Downloaded: 7664 file(s) [attempted 7688/8542 = 90%, 43 KB/s], Decompressed: 4969
Downloaded: 7705 file(s) [attempted 7729/8542 = 90%, 211 KB/s], Decompressed: 4969
Downloaded: 7750 file(s) [attempted 7774/8542 = 91%, 348 KB/s], Decompressed: 4969
Downloaded: 7794 file(s) [attempted 7818/8542 = 91%, 772 KB/s], Decompressed: 4969
Downloaded: 7834 file(s) [attempted 7859/8542 = 92%, 325 KB/s], Decompressed: 4969
Downloaded: 7876 file(s) [attempted 7901/8542 = 92%, 681 KB/s], Decompressed: 4969
Downloaded: 7913 file(s) [attempted 7938/8542 = 92%, 454 KB/s], Decompressed: 4969
Downloaded: 7954 file(s) [attempted 7979/8542 = 93%, 407 KB/s], Decompressed: 4969
Downloaded: 7995 file(s) [attempted 8020/8542 = 93%, 86 KB/s], Decompressed: 4969
Downloaded: 8043 file(s) [attempted 8068/8542 = 94%, 228 KB/s], Decompressed: 4969
Downloaded: 8081 file(s) [attempted 8106/8542 = 94%, 445 KB/s], Decompressed: 4969
Downloaded: 8122 file(s) [attempted 8147/8542 = 95%, 1815 KB/s], Decompressed: 6330
Downloaded: 8156 file(s) [attempted 8181/8542 = 95%, 602 KB/s], Decompressed: 6330
Downloaded: 8197 file(s) [attempted 8222/8542 = 96%, 366 KB/s], Decompressed: 6330
Downloaded: 8238 file(s) [attempted 8263/8542 = 96%, 48 KB/s], Decompressed: 6330
Downloaded: 8282 file(s) [attempted 8307/8542 = 97%, 876 KB/s], Decompressed: 6330
Downloaded: 8320 file(s) [attempted 8345/8542 = 97%, 1133 KB/s], Decompressed: 6330
Downloaded: 8350 file(s) [attempted 8376/8542 = 98%, 566 KB/s], Decompressed: 6330
Downloaded: 8395 file(s) [attempted 8421/8542 = 98%, 75 KB/s], Decompressed: 6330
Downloaded: 8439 file(s) [attempted 8465/8542 = 99%, 81 KB/s], Decompressed: 6330
Downloaded: 8480 file(s) [attempted 8506/8542 = 99%, 663 KB/s], Decompressed: 6330
Downloaded: 8515 file(s) [attempted 8541/8542 = 99%, 488 KB/s], Decompressed: 6330
Downloaded: 8516 file(s) [attempted 8542/8542 = 100%, 488 KB/s], Decompressed: 6330
Warning: some files were not found in the cache.
This usually means that your local checkout of mathlib4 has diverged from upstream.
* If you push your commits to a PR to the mathlib4 repository
(use a draft PR if it is not ready for review),
then CI will build the oleans and they will be available later.
* If you have already opened a PR, this may mean
the CI build has failed part-way through building.
lean_checker exit 0
lake build
✔ [1/3] Built FLT.Assumptions.KnownIn1980s (480ms) ✔ [1953/1964] Built FLT.Assumptions.Mazur (21s) ✔ [2948/2955] Built FLT.Deformations.ContinuousRepresentation.IsTopologicalModule (4.6s) ✔ [2951/2956] Built FLT.Mathlib.Algebra.Algebra.Tower (2.0s) ✔ [2955/2958] Built FLT.Assumptions.Odlyzko (9.4s) ✔ [3222/3230] Built FLT.Mathlib.Algebra.FixedPoints.Basic (2.3s) ✔ [3228/3232] Built FLT.Mathlib.Topology.Algebra.Module.ModuleTopology (7.1s) ✔ [3229/3232] Built FLT.Hacks.RightActionInstances (3.9s) ✔ [3310/3327] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.RestrictedProduct (1.5s) ✔ [3311/3327] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Basic (3.0s) ✔ [3312/3327] Built FLT.Mathlib.Topology.Algebra.Module.Quotient (1.7s) ✔ [3313/3327] Built FLT.Mathlib.Topology.Algebra.Group.Units (1.2s) ✔ [3314/3327] Built FLT.Mathlib.Order.Filter.Cofinite (1.1s) ✔ [3316/3327] Built FLT.Mathlib.Topology.Bases (1.2s) ✔ [3318/3327] Built FLT.Mathlib.MeasureTheory.Group.Action (2.3s) ✔ [3319/3327] Built FLT.Mathlib.MeasureTheory.Measure.Typeclasses.Finite (1.5s) ✔ [3320/3327] Built FLT.DedekindDomain.FiniteAdeleRing.TensorPi (3.6s) ✔ [3321/3327] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Equiv (5.4s) ✔ [3323/3327] Built FLT.Mathlib.Topology.Algebra.ContinuousMonoidHom (1.8s) ✔ [3324/3327] Built FLT.Mathlib.MeasureTheory.Group.Measure (1.6s) ✔ [3325/3328] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (5.2s) ✔ [3326/3341] Built FLT.AutomorphicForm.QuaternionAlgebra.Defs (4.9s) ✔ [3332/3341] Built FLT.Mathlib.RingTheory.TensorProduct.Pi (1.4s) ✔ [3335/3348] Built FLT.Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing (10s) ✔ [3337/3349] Built FLT.Mathlib.LinearAlgebra.Dimension.Constructions (1.6s) ✔ [3339/3349] Built FLT.Mathlib.RingTheory.DedekindDomain.AdicValuation (1.9s) ✔ [3340/3349] Built FLT.Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic (1.3s) ✔ [3343/3349] Built FLT.Mathlib.RingTheory.Valuation.ValuationSubring (2.3s) ✔ [3345/3354] Built FLT.HaarMeasure.HaarChar.AddEquiv (6.3s) ✔ [3347/3355] Built FLT.HaarMeasure.HaarChar.Ring (3.2s) ✔ [3349/3355] Built FLT.Mathlib.RingTheory.Ideal.Quotient.Basic (1.1s) ✔ [3350/3356] Built FLT.Mathlib.LinearAlgebra.Countable (1.6s) ✔ [3354/3362] Built FLT.DedekindDomain.AdicValuation (8.6s) ✔ [3361/3382] Built FLT.Mathlib.Topology.Algebra.Valued.WithZeroMulInt (2.5s) ✔ [3371/3382] Built FLT.Mathlib.RingTheory.Localization.BaseChange (2.2s) ✔ [3373/3382] Built FLT.DedekindDomain.IntegralClosure (5.4s) ✔ [3377/3382] Built FLT.Mathlib.NumberTheory.NumberField.InfinitePlace.Completion (1.9s) ✔ [3379/3384] Built FLT.NumberField.HeightOneSpectrum (1.9s) ✔ [3380/3386] Built FLT.NumberField.Completion.Finite (2.6s) ✔ [3382/3391] Built FLT.Mathlib.NumberTheory.NumberField.FiniteAdeleRing (3.3s) ✔ [3387/3400] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.AdicCompletion (1.7s) ✔ [3388/3400] Built FLT.Mathlib.Algebra.Algebra.Hom (2.2s) ✔ [3389/3400] Built FLT.Mathlib.Algebra.Module.Submodule.Basic (1.1s) ✔ [3391/3410] Built FLT.Mathlib.RingTheory.TensorProduct.Basis (1.9s) ✔ [3392/3410] Built FLT.Mathlib.Topology.Algebra.UniformRing (1.4s) ✔ [3393/3410] Built FLT.Mathlib.Algebra.Algebra.Pi (1.5s) ✔ [3395/3410] Built FLT.Mathlib.Algebra.Algebra.Bilinear (2.1s) ✔ [3397/3410] Built FLT.Mathlib.Algebra.IsDirectLimit (2.1s) ✔ [3398/3410] Built FLT.Mathlib.Topology.Algebra.MulAction (1.3s) ✔ [3399/3410] Built FLT.Mathlib.Topology.Algebra.Algebra.Hom (1.8s) ✔ [3402/3414] Built FLT.Mathlib.LinearAlgebra.Pi (1.5s) ✔ [3403/3414] Built FLT.DedekindDomain.FiniteAdeleRing.IsDirectLimitRestricted (1.8s) ✔ [3405/3414] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Module (7.9s) ✔ [3407/3414] Built FLT.Mathlib.NumberTheory.NumberField.InfiniteAdeleRing (3.7s) ✔ [3409/3414] Built FLT.DedekindDomain.Completion.BaseChange (29s) ✔ [3410/3416] Built FLT.DedekindDomain.FiniteAdeleRing.TensorRestrictedProduct (7.6s) ✔ [3411/3429] Built FLT.Mathlib.NumberTheory.NumberField.AdeleRing (2.3s) ✔ [3414/3430] Built FLT.DedekindDomain.FiniteAdeleRing.BaseChange (80s) ✔ [3416/3430] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.FiniteAdeleRing (1.7s) ✔ [3417/3430] Built FLT.Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (1.7s) ✔ [3418/3430] Built FLT.Mathlib.Topology.Algebra.Group.Quotient (1.3s) ✔ [3419/3430] Built FLT.Mathlib.Topology.Algebra.ContinuousAlgEquiv (1.2s) ✔ [3420/3430] Built FLT.NumberField.InfinitePlace.Extension (2.8s) ✔ [3421/3430] Built FLT.Mathlib.Topology.Algebra.Module.FiniteDimension (1.5s) ✔ [3423/3430] Built FLT.Mathlib.Topology.Constructions (1.0s) ✔ [3425/3433] Built FLT.Mathlib.Topology.MetricSpace.Pseudo.Matrix (1.5s) ✔ [3428/3440] Built FLT.Mathlib.Topology.Algebra.Module.Equiv (1.9s) ✔ [3429/3442] Built FLT.Mathlib.Topology.MetricSpace.ProperSpace.InfinitePlace (1.9s) ✔ [3431/3442] Built FLT.NumberField.Padics.RestrictedProduct (2.7s) ✔ [3432/3442] Built FLT.Mathlib.Data.Real.Archimedean (1.1s) ✔ [3433/3442] Built FLT.Mathlib.LinearAlgebra.Matrix.Transvection (1.4s) ✔ [3434/3442] Built FLT.NumberField.Completion.Infinite (16s) ✔ [3435/3442] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.InfinitePlace (1.8s) ✔ [3438/3445] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.AdeleRing (1.8s) ✔ [3439/3445] Built FLT.Mathlib.RingTheory.SimpleRing.TensorProduct (5.9s) ✔ [3440/3445] Built FLT.NumberField.InfiniteAdeleRing (13s) ✔ [3442/3445] Built FLT.NumberField.AdeleRing (22s) ✔ [3449/3467] Built FLT.Mathlib.NumberTheory.Padics.PadicIntegers (1.0s) ✔ [3451/3467] Built FLT.Mathlib.NumberTheory.Padics.HeightOneSpectrum (3.1s) ✔ [3453/3470] Built FLT.HaarMeasure.MeasurableSpacePadics (1.0s) ✔ [3455/3470] Built FLT.Mathlib.LinearAlgebra.TensorProduct.FiniteFree (1.2s) ✔ [3456/3470] Built FLT.Mathlib.LinearAlgebra.TensorProduct.Algebra (1.7s) ✔ [3458/3473] Built FLT.HaarMeasure.HaarChar.RealComplex (2.8s) ✔ [3459/3473] Built FLT.HaarMeasure.HaarChar.Padic (2.8s) ✔ [3461/3473] Built FLT.Mathlib.Topology.Algebra.Module.TensorProduct (2.5s) ✔ [3464/3473] Built FLT.Mathlib.LinearAlgebra.TensorProduct.Basis (1.3s) ✔ [3465/3473] Built FLT.Mathlib.Algebra.Central.TensorProduct (2.3s) ✔ [3466/3473] Built FLT.DedekindDomain.FiniteAdeleRing.TensorProduct (9.2s) ✔ [3468/3473] Built FLT.Mathlib.GroupTheory.DoubleCoset (1.2s) ✔ [3469/3474] Built FLT.Mathlib.LinearAlgebra.Determinant (5.0s) ✔ [3470/3475] Built FLT.HaarMeasure.HaarChar.FiniteDimensional (6.0s) ✔ [3472/3478] Built FLT.HaarMeasure.HaarChar.FiniteAdeleRing (39s) ✔ [3473/3482] Built FLT.HaarMeasure.HaarChar.AdeleRing (22s) ✔ [3483/3492] Built FLT.Mathlib.Topology.HomToDiscrete (1.9s) ✔ [3484/3492] Built FLT.Mathlib.Topology.Polish (1.6s) ✔ [3488/3509] Built FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Abstract (2.4s) ✔ [3490/3509] Built FLT.Mathlib.Topology.Algebra.Valued.ValuationTopology (1.7s) ✔ [3491/3509] Built FLT.Mathlib.Topology.Instances.Matrix (1.5s) ✔ [3492/3509] Built FLT.Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs (1.9s) ✔ [3493/3509] Built FLT.DedekindDomain.FiniteAdeleRing.LocalUnits (3.8s) ✔ [3494/3509] Built FLT.Mathlib.MeasureTheory.Haar.Extension (2.6s) ✔ [3496/3509] Built FLT.Deformations.Algebra.InverseLimit.Basic (5.5s) ✔ [3498/3509] Built FLT.DivisionAlgebra.Finiteness (41s) ✔ [3499/3509] Built FLT.Data.QHat (6.7s) ✔ [3500/3509] Built FLT.Deformations.Algebra.InverseLimit.Topology (3.5s) ✔ [3502/3509] Built FLT.AutomorphicForm.QuaternionAlgebra.FiniteDimensional (3.8s) ✔ [3503/3515] Built FLT.Data.Hurwitz (4.3s) ✔ [3504/3516] Built FLT.Mathlib.Algebra.IsQuaternionAlgebra (2.1s) ✔ [3505/3516] Built FLT.Data.HurwitzRatHat (2.5s) ✔ [3507/3518] Built FLT.QuaternionAlgebra.NumberField (8.3s) ✔ [3510/3518] Built FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Local (6.2s) ✔ [3513/3521] Built FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Concrete (8.9s) ✔ [3515/3521] Built FLT.Patching.Utils.Lemmas (4.1s) ✔ [3519/3525] Built FLT.Patching.Utils.InverseLimit (1.4s) ✔ [3529/3539] Built FLT.Deformations.Lemmas (3.9s) ✔ [3531/3539] Built FLT.Mathlib.RingTheory.LocalRing.Defs (1.3s) ✔ [3533/3539] Built FLT.Deformations.RepresentationTheory.ContinuousSMulDiscrete (1.3s) ✔ [3534/3539] Built FLT.Deformations.IsResidueAlgebra (2.0s) ✔ [3535/3539] Built FLT.Patching.Utils.AdicTopology (3.7s) ✔ [3536/3540] Built FLT.Deformations.Subfunctor (1.0s) ✔ [3537/3540] Built FLT.Deformations.IsProartinian (1.0s) ✔ [3539/3540] Built FLT.Deformations.Categories (3.4s) ✔ [3586/3590] Built FLT.Deformations.RepresentationTheory.IntegralClosure (2.1s) ✔ [3587/3592] Built FLT.Deformations.RepresentationTheory.Frobenius (3.5s) ✔ [3607/3609] Built FLT.Deformations.RepresentationTheory.AbsoluteGaloisGroup (13s) ✔ [3618/3623] Built FLT.Deformations.RepresentationTheory.Etale (9.1s) ✔ [3635/3643] Built FLT.Deformations.RepresentationTheory.GaloisRep (12s) ✔ [3637/3643] Built FLT.Mathlib.RepresentationTheory.Basic (2.3s) ✔ [3640/3644] Built FLT.Deformations.RepresentationTheory.Irreducible (1.4s) ✔ [3642/3644] Built FLT.Deformations.LiftFunctor (3.0s) ✔ [3643/3655] Built FLT.Deformations.Representable (2.9s) ✔ [3653/3658] Built FLT.EllipticCurve.Torsion (2.5s) ✔ [3655/3662] Built FLT.Deformations.RepresentationTheory.GaloisRepFamily (2.1s) ✔ [3820/3833] Built FLT.Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (1.8s) ✔ [3821/3833] Built FLT.GaloisRepresentation.Automorphic (3.0s) ✔ [3823/3833] Built FLT.GaloisRepresentation.Cyclotomic (2.0s) ✔ [3824/3833] Built FLT.GaloisRepresentation.HardlyRamified.Defs (2.6s) ✔ [3826/3833] Built FLT.GaloisRepresentation.HardlyRamified.Threeadic (2.1s) ✔ [3827/3833] Built FLT.GaloisRepresentation.HardlyRamified.ModThree (2.1s) ✔ [3828/3833] Built FLT.GaloisRepresentation.HardlyRamified.Lift (2.1s) ✔ [3829/3833] Built FLT.GaloisRepresentation.HardlyRamified.Family (2.3s) ✔ [3830/3838] Built FLT.FreyCurve.FreyPackage (4.6s) ✔ [3831/3838] Built FLT.GaloisRepresentation.HardlyRamified.Frey (2.1s) ✔ [3833/3839] Built FLT.FreyCurve.Contradiction (1.0s) ✔ [3956/3975] Built FLT.GroupScheme.FiniteFlat (315ms) ✔ [3957/3975] Built FLT.Mathlib.Algebra.Order.AbsoluteValue.Basic (1.4s) ✔ [3958/3975] Built FLT.Mathlib.Analysis.Normed.Ring.WithAbs (1.4s) ✔ [3959/3975] Built FLT.Mathlib.Data.Fin.Basic (920ms) ✔ [3960/3975] Built FLT.Mathlib.Data.Set.Prod (630ms) ✔ [3961/3975] Built FLT.Mathlib.GroupTheory.Index (1.1s) ✔ [3962/3975] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.Padic (1.3s) ✔ [3963/3975] Built FLT.Mathlib.MeasureTheory.Measure.Regular (1.3s) ✔ [3964/3975] Built FLT.Mathlib.NumberTheory.NumberField.Completion (1.3s) ✔ [3966/3975] Built FLT.Mathlib.Topology.Algebra.Monoid (1.3s) ✔ [3972/3980] Built FLT.Mathlib.Topology.Algebra.Order.Field (2.3s) ✔ [3977/3985] Built FLT.GlobalLanglandsConjectures.GLnDefs (8.7s) ✔ [3979/3989] Built FLT.GlobalLanglandsConjectures.GLzero (2.2s) ✔ [3983/3992] Built FLT.Patching.Utils.TopologicallyFG (1.6s) ✔ [3985/3992] Built FLT.NumberField.DiscriminantBounds (2.6s) ✔ [3987/3994] Built FLT.Patching.Utils.StructureFiniteness (3.7s) ✔ [3988/3994] Built FLT.Patching.Ultraproduct (8.2s) ✔ [3990/3994] Built FLT.Patching.Module (11s) ✔ [3991/3994] Built FLT.Patching.Algebra (9.6s) ✔ [3993/4003] Built FLT.Patching.Over (11s) ✔ [4008/4018] Built FLT.Patching.VanishingFilter (2.7s) ✔ [4011/4018] Built FLT.TateCurve.TateCurve (305ms) ✔ [4012/4018] Built FLT.Patching.Utils.CompactHausdorffRings (2.2s) ✔ [4013/4018] Built FLT.Patching.Utils.Depth (2.0s) ✔ [4014/4018] Built FLT.Patching.System (9.6s) ✔ [4015/4018] Built FLT.Patching.REqualsT (3.9s) ✔ [4016/4018] Built FLT (1.9s) ✔ [4017/4018] Built FermatsLastTheorem (96s) Build completed successfully (4018 jobs).
blueprint_build exit 1
lake build :blueprint
error: unknown package facet `blueprint`
semantic_extract exit -
./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-00000)
apx-semantic-phase {"phase":"core_compile","duration_ms":19329}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":748,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":25,"runner_cache_hit":false}
apx-semantic-phase {"phase":"runner_compile","duration_ms":42832,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache a214ed71bac59bbcc75754a09ff7bffe1dcc31fe1cd9e5b8f7918e5e64522625
/usr/bin/podman timed out after 14400s
podman cleanup removed verifier container apx-verifier-job-532-runtime-semantic_extract-1493713-1781827777936204779-3 semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00000)
apx-semantic-phase {"duration_ms":23,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":1,"diagnostic_count":0,"duration_ms":115,"ok":true,"phase":"lean_declaration_extraction","target_module_count":3}
apx-semantic-phase {"declaration_count":1,"dependency_count":1,"diagnostic_count":5,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":376120,"module_count":3,"ok":true,"phase":"lean_module_facts","target_module_count":3}
apx-semantic-phase {"declaration_count":1,"dependency_count":1,"diagnostic_count":5,"duration_ms":64,"module_count":3,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":4845,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":5,"ok":true,"payload_bytes":4845,"phase":"lean_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":1350,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":24,"runner_cache_hit":false}
apx-semantic-phase {"phase":"runner_compile","duration_ms":79002,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 7e90b4e98157ffc2c3aee24cfbe0d24912d70b2489c2a5f1432d7ac4df4fe31d
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":380873,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00001)
apx-semantic-phase {"duration_ms":4,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":1,"duration_ms":151,"ok":true,"phase":"lean_declaration_extraction","target_module_count":2}
apx-semantic-phase {"declaration_count":3,"dependency_count":4,"diagnostic_count":12,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":337851,"module_count":2,"ok":true,"phase":"lean_module_facts","target_module_count":2}
apx-semantic-phase {"declaration_count":3,"dependency_count":4,"diagnostic_count":12,"duration_ms":63,"module_count":2,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":69761,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":69761,"phase":"lean_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":267,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":23,"runner_cache_hit":false}
apx-semantic-phase {"phase":"runner_compile","duration_ms":4650,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache ad6bd113eae3051161554b68ce84f22ffc8f48ab6411af8fad1d1c1a0a520801
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":342884,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00002)
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":177,"ok":true,"phase":"lean_declaration_extraction","target_module_count":2}
apx-semantic-phase {"declaration_count":3,"dependency_count":5,"diagnostic_count":13,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":502116,"module_count":2,"ok":true,"phase":"lean_module_facts","target_module_count":2}
apx-semantic-phase {"declaration_count":3,"dependency_count":5,"diagnostic_count":13,"duration_ms":51,"module_count":2,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":86203,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":86203,"phase":"lean_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":151,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":24,"runner_cache_hit":false}
apx-semantic-phase {"phase":"runner_compile","duration_ms":9187,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache fa0d1ef17bd9d5da728a7ae7abade55f2d75796ebeffd0bb356c9b30cd96f376
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":506303,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00003)
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":12,"diagnostic_count":6,"duration_ms":678,"ok":true,"phase":"lean_declaration_extraction","target_module_count":2}
apx-semantic-phase {"declaration_count":12,"dependency_count":26,"diagnostic_count":101,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":258054,"module_count":2,"ok":true,"phase":"lean_module_facts","target_module_count":2}
apx-semantic-phase {"declaration_count":12,"dependency_count":26,"diagnostic_count":101,"duration_ms":52,"module_count":2,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":178771,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":178771,"phase":"lean_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":12}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":123,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":27,"runner_cache_hit":false}
apx-semantic-phase {"phase":"runner_compile","duration_ms":2953,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 3f9b43e320631d0dd086f39e2658b002540d610d1c6f71ae043e064557bfc3cc
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":261741,"ok":true}
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00042)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00043)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00044)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00045)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00046)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00047)
error getting current working directory: No such file or directory
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00004)
apx-semantic-phase {"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":4,"diagnostic_count":2,"duration_ms":124,"ok":true,"phase":"lean_declaration_extraction","target_module_count":2}
apx-semantic-phase {"declaration_count":4,"dependency_count":5,"diagnostic_count":19,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":209544,"module_count":2,"ok":true,"phase":"lean_module_facts","target_module_count":2}
apx-semantic-phase {"declaration_count":4,"dependency_count":5,"diagnostic_count":19,"duration_ms":58,"module_count":2,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":28943,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":28943,"phase":"lean_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":24}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":126,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":20,"runner_cache_hit":false}
apx-semantic-phase {"phase":"runner_compile","duration_ms":2528,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 394516ae786dad116689ad17d9acb6f99b38097e4896d88b86e53020dc7e9aa4
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":212203,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00005)
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":4,"diagnostic_count":1,"duration_ms":107,"ok":true,"phase":"lean_declaration_extraction","target_module_count":2}
apx-semantic-phase {"declaration_count":4,"dependency_count":5,"diagnostic_count":10,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":252721,"module_count":2,"ok":true,"phase":"lean_module_facts","target_module_count":2}
apx-semantic-phase {"declaration_count":4,"dependency_count":5,"diagnostic_count":10,"duration_ms":58,"module_count":2,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":117673,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":1,"ok":true,"payload_bytes":117673,"phase":"lean_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":18}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":114,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":23,"runner_cache_hit":false}
apx-semantic-phase {"phase":"runner_compile","duration_ms":2612,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 396d616fa0ca9e215587b67851fe30d2c6c914608c02e085f95d0df7b1dd4d28
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":255335,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00006)
apx-semantic-phase {"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":156,"ok":true,"phase":"lean_declaration_extraction","target_module_count":2}
apx-semantic-phase {"declaration_count":3,"dependency_count":2,"diagnostic_count":13,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":395629,"module_count":2,"ok":true,"phase":"lean_module_facts","target_module_count":2}
apx-semantic-phase {"declaration_count":3,"dependency_count":2,"diagnostic_count":13,"duration_ms":44,"module_count":2,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":59255,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":59255,"phase":"lean_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":25}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":132,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":27,"runner_cache_hit":false}
apx-semantic-phase {"phase":"runner_compile","duration_ms":7187,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache cffaad1d1e7cfe30c8d49d31822f15fc1dd0167038536ecc231d87674f3f4387
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":399231,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00007)
apx-semantic-phase {"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":19,"diagnostic_count":7,"duration_ms":820,"ok":true,"phase":"lean_declaration_extraction","target_module_count":2}
apx-semantic-phase {"declaration_count":19,"dependency_count":34,"diagnostic_count":47,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":375517,"module_count":2,"ok":true,"phase":"lean_module_facts","target_module_count":2}
apx-semantic-phase {"declaration_count":19,"dependency_count":34,"diagnostic_count":47,"duration_ms":101,"module_count":2,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":1330851,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":1,"ok":true,"payload_bytes":1330851,"phase":"lean_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":138,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":23,"runner_cache_hit":false}
apx-semantic-phase {"phase":"runner_compile","duration_ms":2990,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 6d0ed87a85be8855db2ae8513564e9b27f46b9d50cb78249ac5c5c7201dc5124
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":379572,"ok":true}
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00048)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00049)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00050)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00051)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00052)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00053)
error getting current working directory: No such file or directory
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00008)
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":51,"diagnostic_count":27,"duration_ms":1817,"ok":true,"phase":"lean_declaration_extraction","target_module_count":2}
apx-semantic-phase {"declaration_count":51,"dependency_count":136,"diagnostic_count":249,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":291993,"module_count":2,"ok":true,"phase":"lean_module_facts","target_module_count":2}
apx-semantic-phase {"declaration_count":51,"dependency_count":136,"diagnostic_count":249,"duration_ms":94,"module_count":2,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":995985,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":995985,"phase":"lean_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":26}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":125,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":28,"runner_cache_hit":false}
apx-semantic-phase {"phase":"runner_compile","duration_ms":2847,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 7981a28a6d86a8db117687e32960fe1490babd291dc367302417a51b48b50402
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":296840,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00009)
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":105,"diagnostic_count":60,"duration_ms":3583,"ok":true,"phase":"lean_declaration_extraction","target_module_count":2}
apx-semantic-phase {"declaration_count":105,"dependency_count":236,"diagnostic_count":90,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":226947,"module_count":2,"ok":true,"phase":"lean_module_facts","target_module_count":2}
apx-semantic-phase {"declaration_count":105,"dependency_count":236,"diagnostic_count":90,"duration_ms":121,"module_count":2,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":1634320,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":1,"ok":true,"payload_bytes":1634320,"phase":"lean_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":21}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":132,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":21,"runner_cache_hit":false}
apx-semantic-phase {"phase":"runner_compile","duration_ms":2420,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache e9b1c83c8cc6c05bb8d095340ebf47607e20a2300835fa3e3f72f6a22e6a6964
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":233301,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00010)
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":108,"diagnostic_count":42,"duration_ms":4333,"ok":true,"phase":"lean_declaration_extraction","target_module_count":2}
apx-semantic-phase {"declaration_count":108,"dependency_count":338,"diagnostic_count":219,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":460585,"module_count":2,"ok":true,"phase":"lean_module_facts","target_module_count":2}
apx-semantic-phase {"declaration_count":108,"dependency_count":338,"diagnostic_count":219,"duration_ms":136,"module_count":2,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":1840480,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":2,"ok":true,"payload_bytes":1840480,"phase":"lean_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":148,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":24,"runner_cache_hit":false}
apx-semantic-phase {"phase":"runner_compile","duration_ms":4006,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache d26fa8fa5556b8c49f82fa59e90f6e05fbb1ce574cde3eacb3f0dde5e4b253f4
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":468546,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00011)
apx-semantic-phase {"duration_ms":22,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":1,"diagnostic_count":0,"duration_ms":127,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":1,"dependency_count":1,"diagnostic_count":2,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":417696,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":1,"dependency_count":1,"diagnostic_count":2,"duration_ms":64,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":4881,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":5,"ok":true,"payload_bytes":4881,"phase":"lean_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":111,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":22,"runner_cache_hit":false}
apx-semantic-phase {"phase":"runner_compile","duration_ms":24147,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 24c783e79ba0c36581546b5ab6a28d92330e9dc91b569bf18c093cc17b9b4806
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":423678,"ok":true}
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00054)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00055)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00056)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00057)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00058)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00059)
error getting current working directory: No such file or directory
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00012)
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":2,"diagnostic_count":0,"duration_ms":141,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":2,"dependency_count":1,"diagnostic_count":0,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":185702,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":2,"dependency_count":1,"diagnostic_count":0,"duration_ms":53,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":7020,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":2,"ok":true,"payload_bytes":7020,"phase":"lean_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":24}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":250,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":25,"runner_cache_hit":false}
apx-semantic-phase {"phase":"runner_compile","duration_ms":3111,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 15a4c5adfd8bda418e61dc203baaedf8c0930b226feac8a3d515c9c4530db60c
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":189717,"ok":true}
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00013)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00014)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00015)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00016)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00017)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00018)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00019)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00020)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00021)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00022)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00023)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00024)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00025)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00026)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00027)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00028)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00029)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00030)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00031)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00032)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00033)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00034)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00035)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00036)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00037)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00038)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00039)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00040)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00041)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00066)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00067)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00068)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00069)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00070)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00071)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00072)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00073)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00074)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00075)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00076)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00077)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00078)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00079)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00080)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00081)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00082)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00083)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00084)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00085)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00086)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00087)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00088)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00089)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00090)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00091)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00092)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00093)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00094)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00095)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00096)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00097)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00098)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00099)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00100)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00101)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00102)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00103)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00104)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00105)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00106)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00107)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00108)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00109)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00110)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00111)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00112)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00113)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00114)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00115)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00116)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00117)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00118)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00119)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00120)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00121)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00122)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00123)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00124)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00125)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00126)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00127)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00128)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00129)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00130)
error getting current working directory: No such file or directory
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00131)
error getting current working directory: No such file or directory