Verification run
Run 71
failed commit
5754873e8dae toolchain lean-v4-30-0 prover lean took 2h 51m · finished 4w ago ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00018) failed with exit code none (process did not exit cleanly) (toolchain lean-v4-30-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
have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3781:4: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.
Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3784:6: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.
Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3786:4: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.
Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3776:32: The following tactic starts with 2 goals and ends with 2 goals, 1 of which is not operated on.
ring
Please focus on the current goal, for instance using `·` (typed as "\.").
Note: This linter can be disabled with `set_option linter.style.multiGoal false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3827:4: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.
Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3830:8: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.
Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: `simp_all +decide [ επ_num, μ_num ]` is a flexible tactic modifying `⊢`. Try `simp_all?` and use the suggested `simp_all only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: Try this:
[apply] simp_all +decide only [ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3836:4: `have h63 :=
theorem_6_3 (by linarith : 14 ≤ x₁) x₂.toReal
(by
cases x₂ <;> norm_num at *; · linarith;
· exact absurd hc (by exact ne_of_lt (EReal.coe_lt_top _)))
x hx₁
(by
cases x₂ <;> norm_num at *; · linarith;
· exact absurd hc (by exact ne_of_lt (EReal.coe_lt_top _)))
(by
cases x₂ <;> norm_num at *; · exact_mod_cast hc;
· exact mul_nonneg (by linarith) (Real.log_nonneg (by linarith)))` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: `simp_all +decide [ επ_num, μ_num ]` is a flexible tactic modifying `⊢`. Try `simp_all?` and use the suggested `simp_all only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: Try this:
[apply] simp_all +decide only [ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3846:4: `unfold μ_num_1` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3847:35: `simp_all +decide [ mul_assoc, mul_comm, mul_left_comm ]` is a flexible tactic modifying `⊢`. Try `simp_all?` and use the suggested `simp_all only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3847:35: Try this:
[apply] simp_all +decide only [Fin.Iio_last_eq_map, Finset.sum_sub_distrib, Finset.sum_map, Fin.coe_castSuccEmb,
Fin.coeSucc_eq_succ, ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3849:6: `exact absurd (this y hy₁) (by norm_num [h]; linarith)` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: `simp_all +decide [ επ_num, μ_num ]` is a flexible tactic modifying `⊢`. Try `simp_all?` and use the suggested `simp_all only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: Try this:
[apply] simp_all +decide only [ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3858:6: `exact absurd ‹_› (not_le_of_gt hc)` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4652:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4679:8: declaration uses `sorry`
✔ [4201/4212] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows:blueprint (2.9s)
✔ [4204/4212] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2:blueprint (30s)
✔ [4206/4259] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_dispatch:blueprint (14s)
✔ [4223/4261] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtCore:blueprint (3.0s)
✔ [4241/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_00:blueprint (2.9s)
✔ [4242/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_01:blueprint (2.9s)
✔ [4243/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_02:blueprint (2.9s)
✔ [4244/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_03:blueprint (2.9s)
✔ [4245/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_04:blueprint (2.9s)
✔ [4246/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_05:blueprint (2.9s)
✔ [4247/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_06:blueprint (2.9s)
✔ [4248/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_07:blueprint (2.9s)
✔ [4249/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_08:blueprint (2.9s)
✔ [4250/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_09:blueprint (2.9s)
✔ [4251/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_10:blueprint (2.9s)
✔ [4252/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_11:blueprint (2.0s)
✔ [4253/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_12:blueprint (2.9s)
✔ [4254/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_13:blueprint (2.9s)
⚠ [4255/4262] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean:116:8: declaration uses `sorry`
✔ [4257/4264] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext:blueprint (2.9s)
⚠ [4258/4264] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:19:72: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.
Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:109:37: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.
Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:122:60: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.
Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
✔ [4261/4299] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor:blueprint (5.5s)
⚠ [4272/4299] Replayed PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting
warning: PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:2045:6: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.
Note: This linter can be disabled with `set_option linter.style.show false`
✔ [4279/4356] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower:blueprint (3.1s)
⚠ [4280/4356] Replayed PrimeNumberTheoremAnd.IEANTN.TMEEMT
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:93:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:104:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:117:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:146:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:154:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:179:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:187:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:195:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:333:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:341:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:470:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:515:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:530:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:564:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:573:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:582:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:591:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:600:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:616:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:625:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:634:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:643:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:678:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:687:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:696:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:722:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:745:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:756:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:767:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:778:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:788:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:796:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:805:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:814:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:937:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:957:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:987:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1013:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1027:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1035:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1050:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1065:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1074:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1089:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1107:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1119:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1136:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1147:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1169:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1183:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1197:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1227:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1243:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1254:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1278:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1292:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1306:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1320:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1334:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1369:8: declaration uses `sorry`
✔ [4299/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.TMEEMT:blueprint (43s)
⚠ [4300/4395] Replayed PrimeNumberTheoremAnd.IEANTN.SecondarySummary
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:61:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:204:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:214:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:228:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:243:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:256:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:338:8: declaration uses `sorry`
ℹ [4328/4395] Replayed PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations
info: PrimeNumberTheoremAnd/IEANTN/Ramanujan/RamanujanCalculations.lean:76:4: Try this:
[apply] ring_nf
The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
⚠ [4329/4395] Replayed PrimeNumberTheoremAnd.IwaniecKowalskiCh1
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:74:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:91:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:638:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:680:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:718:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:986:3: error: doc-strings should start with a single space or newline
Note: This linter can be disabled with `set_option linter.style.docString false`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1259:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1429:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1444:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1456:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1474:6: declaration uses `sorry`
✔ [4333/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondarySummary:blueprint (6.5s)
⚠ [4334/4395] Replayed PrimeNumberTheoremAnd.IEANTN.Goldbach
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
✔ [4344/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.DigammaSeries:blueprint (2.4s)
✔ [4354/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.MobiusLemma:blueprint (10s)
✔ [4356/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Goldbach:blueprint (5.8s)
✔ [4379/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.LaplaceInversion:blueprint (2.5s)
✔ [4380/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Lcm:blueprint (10s)
✔ [4381/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimarySummary:blueprint (2.8s)
✔ [4382/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan:blueprint (14s)
✔ [4384/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.PerronFormula:blueprint (20s)
⚠ [4390/4395] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:132:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:169:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:206:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:277:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:325:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:357:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1277:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1320:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1407:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1490:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2720:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2746:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:3352:8: declaration uses `sorry`
✔ [4391/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Kadiri:blueprint (42s)
✔ [4393/4396] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (3.2s)
ℹ [4394/4396] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (60ms)
info: Blueprint indexing
Build completed successfully (4396 jobs).
stderr:
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00000)
exit_code=Some(0) duration_ms=378520
stdout:
apx-semantic-phase {"duration_ms":4,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":20,"diagnostic_count":12,"duration_ms":1445,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":20,"dependency_count":29,"diagnostic_count":110,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":363804,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":20,"dependency_count":29,"diagnostic_count":110,"duration_ms":107,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":173726,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":3,"ok":true,"payload_bytes":173726,"phase":"lean_json_write"}
stderr:
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"core_compile","duration_ms":4304}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":168,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":25,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":4048,"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 5741e1a44ae06aad78a68854fd2e21d57fb81612889b2505612cab2fd9c44553
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":369119,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00001)
exit_code=Some(0) duration_ms=375027
stdout:
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":97,"diagnostic_count":49,"duration_ms":7409,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":97,"dependency_count":170,"diagnostic_count":1037,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":359054,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":97,"dependency_count":170,"diagnostic_count":1037,"duration_ms":232,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":1249897,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":1,"ok":true,"payload_bytes":1249897,"phase":"lean_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":22}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":191,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":24,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":3655,"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 5b77841087ccab3bcfb34d5a043c9fa5b17370b1dfa57d99f47ad48210893493
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":370464,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00002)
exit_code=Some(0) duration_ms=306155
stdout:
apx-semantic-phase {"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":209,"diagnostic_count":121,"duration_ms":12350,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":209,"dependency_count":112,"diagnostic_count":121,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":286194,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":209,"dependency_count":112,"diagnostic_count":121,"duration_ms":138,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":2085440,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":3,"ok":true,"payload_bytes":2085440,"phase":"lean_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":24}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":140,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":25,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":3225,"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 51b4d997b7ef0937d9360853ece8692b7955dcf8e72ba6aa1548224968760561
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":301879,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00003)
exit_code=Some(0) duration_ms=402903
stdout:
apx-semantic-phase {"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":320,"diagnostic_count":209,"duration_ms":23324,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":320,"dependency_count":576,"diagnostic_count":3709,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":369538,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":320,"dependency_count":576,"diagnostic_count":3709,"duration_ms":649,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":3206467,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":4,"ok":true,"payload_bytes":3206467,"phase":"lean_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":248,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":23,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":3942,"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 d203f7a84cac617a041c0c41d596da8a2cffed777b2b3d148400d0836b1525bd
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":397791,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00004)
exit_code=Some(0) duration_ms=292707
stdout:
apx-semantic-phase {"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":30,"diagnostic_count":8,"duration_ms":1978,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":30,"dependency_count":56,"diagnostic_count":328,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":282937,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":30,"dependency_count":56,"diagnostic_count":328,"duration_ms":120,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":430335,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":1,"ok":true,"payload_bytes":430335,"phase":"lean_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":210,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":25,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":3496,"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 4bc71e7804c1e324b3fac66104e45900b93c56607d510147ae600737b5556517
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":288372,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00005)
exit_code=Some(0) duration_ms=421440
stdout:
apx-semantic-phase {"duration_ms":4,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":471,"diagnostic_count":322,"duration_ms":43187,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":471,"dependency_count":643,"diagnostic_count":5985,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":365701,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":471,"dependency_count":643,"diagnostic_count":5985,"duration_ms":1284,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":6685494,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":4,"ok":true,"payload_bytes":6685494,"phase":"lean_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":22}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":232,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":19,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":5222,"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 0e714cddd7a02b78dfce9acd49bcacbdf655be1af5aa62637bc5953e0f46df16
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":415065,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00006)
exit_code=Some(0) duration_ms=379252
stdout:
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":6,"diagnostic_count":0,"duration_ms":487,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":6,"dependency_count":0,"diagnostic_count":0,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":370265,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":6,"dependency_count":0,"diagnostic_count":0,"duration_ms":63,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":11386,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":11386,"phase":"lean_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":22}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":145,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":24,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":3888,"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 e69b7596a484b6aa56daebe3101274ace5df7ceac7a1d1a1621fde6aa454ca84
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":374555,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00007)
exit_code=Some(0) duration_ms=399602
stdout:
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":194,"diagnostic_count":65,"duration_ms":20495,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":194,"dependency_count":345,"diagnostic_count":120,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":369256,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":194,"dependency_count":345,"diagnostic_count":120,"duration_ms":165,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":2717344,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":2,"ok":true,"payload_bytes":2717344,"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":27,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":4774,"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 877107122381a5f781c625da64cd9679c19ba32c3ea30a90e77c1333fdc5405c
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":393730,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00008)
exit_code=Some(0) duration_ms=375135
stdout:
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":0,"diagnostic_count":0,"duration_ms":3,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":0,"dependency_count":0,"diagnostic_count":0,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":367123,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":0,"dependency_count":0,"diagnostic_count":0,"duration_ms":70,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":824,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":824,"phase":"lean_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":24}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":116,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":23,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":3660,"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 6016b85032006c16277cc4bcb8285554ca483116798671eee68247a861ce3c80
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":370661,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00009)
exit_code=Some(0) duration_ms=400029
stdout:
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":136,"diagnostic_count":71,"duration_ms":8804,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":136,"dependency_count":337,"diagnostic_count":821,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":379582,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":136,"dependency_count":337,"diagnostic_count":821,"duration_ms":201,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":835159,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":1,"ok":true,"payload_bytes":835159,"phase":"lean_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":22}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":172,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":23,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":5970,"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 50b5328954002592b7edc0486e8ae5f1152aa983fb8d62523a5a913cfb70afd9
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":392337,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00010)
exit_code=Some(0) duration_ms=386785
stdout:
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":36,"diagnostic_count":27,"duration_ms":2476,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":36,"dependency_count":27,"diagnostic_count":32,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":375709,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":36,"dependency_count":27,"diagnostic_count":32,"duration_ms":66,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":196734,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":1,"ok":true,"payload_bytes":196734,"phase":"lean_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":131,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":23,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":4079,"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 68d0f716f8355725ee6f9d7ee0e09b1245d653cb481c21c6c1d1ea185ef2dbd5
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":381921,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00011)
exit_code=Some(0) duration_ms=376406
stdout:
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":69,"diagnostic_count":54,"duration_ms":4822,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":69,"dependency_count":81,"diagnostic_count":54,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":363272,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":69,"dependency_count":81,"diagnostic_count":54,"duration_ms":103,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":450967,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":1,"ok":true,"payload_bytes":450967,"phase":"lean_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":21}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":114,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":22,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":3755,"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 18af009ee1a830d425537f50fe744e90c504913261a2f7bca928c9524a7e330c
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":371874,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00012)
exit_code=Some(0) duration_ms=461411
stdout:
apx-semantic-phase {"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":792,"diagnostic_count":519,"duration_ms":86080,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":792,"dependency_count":1446,"diagnostic_count":4839,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":365243,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":792,"dependency_count":1446,"diagnostic_count":4839,"duration_ms":903,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":7656056,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":5,"ok":true,"payload_bytes":7656056,"phase":"lean_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":206,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":15,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":3611,"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 db5d22bbf83d87b9a1c61e62f372485ff411f0f9d85e6f5bc1ca7d9c4c2e4ce8
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":456658,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00013)
exit_code=Some(0) duration_ms=378895
stdout:
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":24,"diagnostic_count":11,"duration_ms":1506,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":24,"dependency_count":38,"diagnostic_count":11,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":368825,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":24,"dependency_count":38,"diagnostic_count":11,"duration_ms":52,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":177128,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":1,"ok":true,"payload_bytes":177128,"phase":"lean_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":21}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":134,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":23,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":3704,"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 1d3717a4e3c625c11a320d9386f89a24144d0ba2b6dfca41d4b039313b24979e
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":374186,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00014)
exit_code=Some(0) duration_ms=384351
stdout:
apx-semantic-phase {"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":17,"diagnostic_count":10,"duration_ms":1058,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":17,"dependency_count":14,"diagnostic_count":24,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":375140,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":17,"dependency_count":14,"diagnostic_count":24,"duration_ms":89,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":110358,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":1,"ok":true,"payload_bytes":110358,"phase":"lean_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":21}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":150,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":22,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":3641,"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 c717b34e158e396b03478eefece2f27c878299f49f4b44d91292b43b6f53c94b
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":379927,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00015)
exit_code=Some(0) duration_ms=399912
stdout:
apx-semantic-phase {"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":57,"diagnostic_count":33,"duration_ms":3950,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":57,"dependency_count":128,"diagnostic_count":33,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":384504,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":57,"dependency_count":128,"diagnostic_count":33,"duration_ms":74,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":196513,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":196513,"phase":"lean_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":127,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":20,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":6773,"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 d3a54fbe1a8ca53303a50de52609a68b329948be498efcbe587263568df4249f
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":392350,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00016)
exit_code=Some(0) duration_ms=393954
stdout:
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":38,"diagnostic_count":28,"duration_ms":2693,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":38,"dependency_count":30,"diagnostic_count":28,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":382864,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":38,"dependency_count":30,"diagnostic_count":28,"duration_ms":71,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":318410,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":318410,"phase":"lean_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":22}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":133,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":22,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":3777,"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 2bb7262fc3426db0348f4842d887f6e4b95e31b0be86ef935773b25e74197268
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":389372,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00017)
exit_code=Some(0) duration_ms=421747
stdout:
apx-semantic-phase {"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":367,"diagnostic_count":137,"duration_ms":39135,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":367,"dependency_count":1331,"diagnostic_count":187,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":373778,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":367,"dependency_count":1331,"diagnostic_count":187,"duration_ms":250,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":3138984,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":2,"ok":true,"payload_bytes":3138984,"phase":"lean_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":9}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":112,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":19,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":3908,"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 af4e8eb363ed4bc674e410239e2538aa02a73f0eaadef9f96a6c3590c6afa1ec
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":417037,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00018)
exit_code=None duration_ms=266006
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":22}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":123,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":23,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":4113,"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 070e77e5c3334a7bcb19ace775ad6f6878902bc9e0961dcd1900b95f349e9efb
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
/usr/bin/podman timed out after 266s
podman cleanup removed verifier container apx-verifier-job-519-runtime-semantic_extract-2181-1781752473397778809-21
$ semantic_extract (extract-batch-00019)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00020)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00021)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00022)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00023)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00024)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00025)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00026)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00027)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00028)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00029)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00030)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00031)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00032)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00033)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00034)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00035)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00036)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00037)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00038)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00039)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00040)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00041)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00042)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00043)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00044)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00045)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00046)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00047)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00048)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00049)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00050)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00051)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00052)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00053)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00054)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00055)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00056)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00057)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00058)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00059)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00060)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00061)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00062)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00063)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00064)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00065)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00066)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00067)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00068)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00069)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
$ semantic_extract (extract-batch-00070)
exit_code=None duration_ms=0
stderr:
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
Stored Lean workspace build cache
Command runs
semantic_extract exit -
semantic_extract (extract-batch-00039)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00040)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00041)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00042)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00043)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00044)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00045)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00046)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00047)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00048)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00049)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00050)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00051)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00052)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00053)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00054)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00055)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00056)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00057)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00058)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00059)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00060)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00061)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00062)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00063)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00064)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00065)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00066)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00067)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00068)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00069)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00070)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
git_clone exit 0
git clone --depth 1 --branch main --single-branch https://github.com/AlexKontorovich/PrimeNumberTheoremAnd.git /var/lib/apodeixis/repos/job-519-source
Cloning into '/var/lib/apodeixis/repos/job-519-source'...
git_checkout exit 0
git checkout 5754873e8dae73f3b50f8f2b7a4f0b15d4df58aa
Note: switching to '5754873e8dae73f3b50f8f2b7a4f0b15d4df58aa'. 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 5754873 feat(laplace): windowed principal-value sinc kernel convergence (#1589)
lake_cache exit 0
lake exe cache get
Current branch: HEAD Using cache (Azure) from origin: (some leanprover-community/mathlib4) Attempting to download 8459 file(s) from leanprover-community/mathlib4 cache Decompressed 8459 file(s) Already decompressed 8459 file(s)
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes Downloaded: 1 file(s) [attempted 1/8459 = 0%, 9 KB/s], Decompressed: 0 Downloaded: 15 file(s) [attempted 15/8459 = 0%, 4 KB/s], Decompressed: 13 Downloaded: 31 file(s) [attempted 31/8459 = 0%, 21 KB/s], Decompressed: 30 Downloaded: 64 file(s) [attempted 64/8459 = 0%, 336 KB/s], Decompressed: 35 Downloaded: 86 file(s) [attempted 86/8459 = 1%, 311 KB/s], Decompressed: 35 Downloaded: 117 file(s) [attempted 117/8459 = 1%, 51 KB/s], Decompressed: 96 Downloaded: 148 file(s) [attempted 148/8459 = 1%, 217 KB/s], Decompressed: 96 Downloaded: 185 file(s) [attempted 185/8459 = 2%, 1201 KB/s], Decompressed: 107 Downloaded: 223 file(s) [attempted 223/8459 = 2%, 212 KB/s], Decompressed: 216 Downloaded: 258 file(s) [attempted 258/8459 = 3%, 185 KB/s], Decompressed: 254 Downloaded: 302 file(s) [attempted 302/8459 = 3%, 321 KB/s], Decompressed: 295 Downloaded: 343 file(s) [attempted 343/8459 = 4%, 241 KB/s], Decompressed: 340 Downloaded: 381 file(s) [attempted 381/8459 = 4%, 227 KB/s], Decompressed: 374 Downloaded: 415 file(s) [attempted 415/8459 = 4%, 166 KB/s], Decompressed: 374 Downloaded: 451 file(s) [attempted 451/8459 = 5%, 292 KB/s], Decompressed: 374 Downloaded: 490 file(s) [attempted 490/8459 = 5%, 443 KB/s], Decompressed: 484 Downloaded: 532 file(s) [attempted 532/8459 = 6%, 326 KB/s], Decompressed: 528 Downloaded: 569 file(s) [attempted 569/8459 = 6%, 22 KB/s], Decompressed: 566 Downloaded: 604 file(s) [attempted 604/8459 = 7%, 71 KB/s], Decompressed: 593 Downloaded: 641 file(s) [attempted 641/8459 = 7%, 84 KB/s], Decompressed: 638 Downloaded: 686 file(s) [attempted 686/8459 = 8%, 207 KB/s], Decompressed: 682 Downloaded: 727 file(s) [attempted 727/8459 = 8%, 70 KB/s], Decompressed: 723 Downloaded: 771 file(s) [attempted 771/8459 = 9%, 189 KB/s], Decompressed: 761 Downloaded: 811 file(s) [attempted 811/8459 = 9%, 161 KB/s], Decompressed: 788 Downloaded: 847 file(s) [attempted 847/8459 = 10%, 95 KB/s], Decompressed: 836 Downloaded: 884 file(s) [attempted 884/8459 = 10%, 40 KB/s], Decompressed: 857 Downloaded: 932 file(s) [attempted 932/8459 = 11%, 130 KB/s], Decompressed: 857 Downloaded: 977 file(s) [attempted 977/8459 = 11%, 742 KB/s], Decompressed: 871 Downloaded: 1015 file(s) [attempted 1015/8459 = 11%, 200 KB/s], Decompressed: 1011 Downloaded: 1052 file(s) [attempted 1052/8459 = 12%, 112 KB/s], Decompressed: 1045 Downloaded: 1093 file(s) [attempted 1093/8459 = 12%, 579 KB/s], Decompressed: 1090 Downloaded: 1131 file(s) [attempted 1131/8459 = 13%, 195 KB/s], Decompressed: 1127 Downloaded: 1172 file(s) [attempted 1172/8459 = 13%, 781 KB/s], Decompressed: 1165 Downloaded: 1213 file(s) [attempted 1213/8459 = 14%, 301 KB/s], Decompressed: 1192 Downloaded: 1240 file(s) [attempted 1240/8459 = 14%, 396 KB/s], Decompressed: 1234 Downloaded: 1286 file(s) [attempted 1286/8459 = 15%, 108 KB/s], Decompressed: 1281 Downloaded: 1326 file(s) [attempted 1326/8459 = 15%, 376 KB/s], Decompressed: 1323 Downloaded: 1367 file(s) [attempted 1367/8459 = 16%, 281 KB/s], Decompressed: 1360 Downloaded: 1401 file(s) [attempted 1401/8459 = 16%, 59 KB/s], Decompressed: 1360 Downloaded: 1439 file(s) [attempted 1439/8459 = 17%, 53 KB/s], Decompressed: 1360 Downloaded: 1483 file(s) [attempted 1483/8459 = 17%, 125 KB/s], Decompressed: 1473 Downloaded: 1524 file(s) [attempted 1524/8459 = 18%, 398 KB/s], Decompressed: 1521 Downloaded: 1569 file(s) [attempted 1569/8459 = 18%, 215 KB/s], Decompressed: 1559 Downloaded: 1603 file(s) [attempted 1603/8459 = 18%, 313 KB/s], Decompressed: 1593 Downloaded: 1641 file(s) [attempted 1641/8459 = 19%, 324 KB/s], Decompressed: 1637 Downloaded: 1685 file(s) [attempted 1685/8459 = 19%, 140 KB/s], Decompressed: 1682 Downloaded: 1730 file(s) [attempted 1730/8459 = 20%, 236 KB/s], Decompressed: 1723 Downloaded: 1771 file(s) [attempted 1771/8459 = 20%, 477 KB/s], Decompressed: 1761 Downloaded: 1805 file(s) [attempted 1805/8459 = 21%, 46 KB/s], Decompressed: 1791 Downloaded: 1839 file(s) [attempted 1839/8459 = 21%, 394 KB/s], Decompressed: 1832 Downloaded: 1880 file(s) [attempted 1880/8459 = 22%, 178 KB/s], Decompressed: 1874 Downloaded: 1921 file(s) [attempted 1921/8459 = 22%, 359 KB/s], Decompressed: 1915 Downloaded: 1963 file(s) [attempted 1963/8459 = 23%, 249 KB/s], Decompressed: 1956 Downloaded: 1997 file(s) [attempted 1997/8459 = 23%, 208 KB/s], Decompressed: 1993 Downloaded: 2034 file(s) [attempted 2034/8459 = 24%, 480 KB/s], Decompressed: 2031 Downloaded: 2072 file(s) [attempted 2072/8459 = 24%, 221 KB/s], Decompressed: 2062 Downloaded: 2113 file(s) [attempted 2113/8459 = 24%, 245 KB/s], Decompressed: 2110 Downloaded: 2154 file(s) [attempted 2154/8459 = 25%, 127 KB/s], Decompressed: 2147 Downloaded: 2188 file(s) [attempted 2188/8459 = 25%, 952 KB/s], Decompressed: 2175 Downloaded: 2226 file(s) [attempted 2226/8459 = 26%, 289 KB/s], Decompressed: 2175 Downloaded: 2264 file(s) [attempted 2264/8459 = 26%, 468 KB/s], Decompressed: 2185 Downloaded: 2305 file(s) [attempted 2305/8459 = 27%, 201 KB/s], Decompressed: 2298 Downloaded: 2342 file(s) [attempted 2342/8459 = 27%, 4867 KB/s], Decompressed: 2308 Downloaded: 2380 file(s) [attempted 2380/8459 = 28%, 658 KB/s], Decompressed: 2377 Downloaded: 2418 file(s) [attempted 2418/8459 = 28%, 958 KB/s], Decompressed: 2411 Downloaded: 2455 file(s) [attempted 2455/8459 = 29%, 453 KB/s], Decompressed: 2442 Downloaded: 2493 file(s) [attempted 2493/8459 = 29%, 347 KB/s], Decompressed: 2483 Downloaded: 2531 file(s) [attempted 2531/8459 = 29%, 522 KB/s], Decompressed: 2527 Downloaded: 2568 file(s) [attempted 2568/8459 = 30%, 30 KB/s], Decompressed: 2561 Downloaded: 2609 file(s) [attempted 2609/8459 = 30%, 117 KB/s], Decompressed: 2599 Downloaded: 2650 file(s) [attempted 2650/8459 = 31%, 1444 KB/s], Decompressed: 2626 Downloaded: 2685 file(s) [attempted 2685/8459 = 31%, 46 KB/s], Decompressed: 2681 Downloaded: 2722 file(s) [attempted 2722/8459 = 32%, 174 KB/s], Decompressed: 2715 Downloaded: 2763 file(s) [attempted 2763/8459 = 32%, 21 KB/s], Decompressed: 2715 Downloaded: 2801 file(s) [attempted 2801/8459 = 33%, 489 KB/s], Decompressed: 2715 Downloaded: 2842 file(s) [attempted 2842/8459 = 33%, 364 KB/s], Decompressed: 2722 Downloaded: 2883 file(s) [attempted 2883/8459 = 34%, 598 KB/s], Decompressed: 2722 Downloaded: 2921 file(s) [attempted 2921/8459 = 34%, 591 KB/s], Decompressed: 2722 Downloaded: 2962 file(s) [attempted 2962/8459 = 35%, 420 KB/s], Decompressed: 2722 Downloaded: 3003 file(s) [attempted 3003/8459 = 35%, 951 KB/s], Decompressed: 2963 Downloaded: 3041 file(s) [attempted 3041/8459 = 35%, 284 KB/s], Decompressed: 3034 Downloaded: 3078 file(s) [attempted 3078/8459 = 36%, 893 KB/s], Decompressed: 3065 Downloaded: 3116 file(s) [attempted 3116/8459 = 36%, 231 KB/s], Decompressed: 3112 Downloaded: 3157 file(s) [attempted 3157/8459 = 37%, 180 KB/s], Decompressed: 3154 Downloaded: 3198 file(s) [attempted 3198/8459 = 37%, 37 KB/s], Decompressed: 3191 Downloaded: 3239 file(s) [attempted 3239/8459 = 38%, 204 KB/s], Decompressed: 3229 Downloaded: 3273 file(s) [attempted 3273/8459 = 38%, 67 KB/s], Decompressed: 3266 Downloaded: 3311 file(s) [attempted 3311/8459 = 39%, 159 KB/s], Decompressed: 3304 Downloaded: 3355 file(s) [attempted 3355/8459 = 39%, 456 KB/s], Decompressed: 3345 Downloaded: 3396 file(s) [attempted 3396/8459 = 40%, 50 KB/s], Decompressed: 3383 Downloaded: 3434 file(s) [attempted 3434/8459 = 40%, 583 KB/s], Decompressed: 3420 Downloaded: 3468 file(s) [attempted 3468/8459 = 40%, 697 KB/s], Decompressed: 3465 Downloaded: 3513 file(s) [attempted 3513/8459 = 41%, 1007 KB/s], Decompressed: 3468 Downloaded: 3554 file(s) [attempted 3554/8459 = 42%, 703 KB/s], Decompressed: 3468 Downloaded: 3588 file(s) [attempted 3588/8459 = 42%, 539 KB/s], Decompressed: 3564 Downloaded: 3629 file(s) [attempted 3629/8459 = 42%, 639 KB/s], Decompressed: 3616 Downloaded: 3667 file(s) [attempted 3667/8459 = 43%, 590 KB/s], Decompressed: 3657 Downloaded: 3708 file(s) [attempted 3708/8459 = 43%, 83 KB/s], Decompressed: 3698 Downloaded: 3749 file(s) [attempted 3749/8459 = 44%, 632 KB/s], Decompressed: 3739 Downloaded: 3787 file(s) [attempted 3787/8459 = 44%, 474 KB/s], Decompressed: 3783 Downloaded: 3828 file(s) [attempted 3828/8459 = 45%, 86 KB/s], Decompressed: 3824 Downloaded: 3869 file(s) [attempted 3869/8459 = 45%, 1067 KB/s], Decompressed: 3859 Downloaded: 3910 file(s) [attempted 3910/8459 = 46%, 82 KB/s], Decompressed: 3903 Downloaded: 3953 file(s) [attempted 3953/8459 = 46%, 397 KB/s], Decompressed: 3944 Downloaded: 3989 file(s) [attempted 3989/8459 = 47%, 175 KB/s], Decompressed: 3978 Downloaded: 4026 file(s) [attempted 4026/8459 = 47%, 81 KB/s], Decompressed: 4019 Downloaded: 4067 file(s) [attempted 4067/8459 = 48%, 1226 KB/s], Decompressed: 4040 Downloaded: 4108 file(s) [attempted 4108/8459 = 48%, 359 KB/s], Decompressed: 4040 Downloaded: 4149 file(s) [attempted 4149/8459 = 49%, 37 KB/s], Decompressed: 4141 Downloaded: 4184 file(s) [attempted 4184/8459 = 49%, 296 KB/s], Decompressed: 4177 Downloaded: 4222 file(s) [attempted 4222/8459 = 49%, 291 KB/s], Decompressed: 4218 Downloaded: 4262 file(s) [attempted 4262/8459 = 50%, 199 KB/s], Decompressed: 4256 Downloaded: 4303 file(s) [attempted 4303/8459 = 50%, 162 KB/s], Decompressed: 4300 Downloaded: 4342 file(s) [attempted 4342/8459 = 51%, 372 KB/s], Decompressed: 4331 Downloaded: 4379 file(s) [attempted 4379/8459 = 51%, 484 KB/s], Decompressed: 4375 Downloaded: 4416 file(s) [attempted 4416/8459 = 52%, 100 KB/s], Decompressed: 4413 Downloaded: 4457 file(s) [attempted 4457/8459 = 52%, 37 KB/s], Decompressed: 4451 Downloaded: 4499 file(s) [attempted 4499/8459 = 53%, 236 KB/s], Decompressed: 4492 Downloaded: 4540 file(s) [attempted 4540/8459 = 53%, 22 KB/s], Decompressed: 4536 Downloaded: 4577 file(s) [attempted 4577/8459 = 54%, 448 KB/s], Decompressed: 4574 Downloaded: 4618 file(s) [attempted 4618/8459 = 54%, 42 KB/s], Decompressed: 4611 Downloaded: 4659 file(s) [attempted 4659/8459 = 55%, 782 KB/s], Decompressed: 4649 Downloaded: 4697 file(s) [attempted 4697/8459 = 55%, 1375 KB/s], Decompressed: 4687 Downloaded: 4738 file(s) [attempted 4738/8459 = 56%, 161 KB/s], Decompressed: 4728 Downloaded: 4779 file(s) [attempted 4779/8459 = 56%, 78 KB/s], Decompressed: 4769 Downloaded: 4817 file(s) [attempted 4817/8459 = 56%, 203 KB/s], Decompressed: 4813 Downloaded: 4858 file(s) [attempted 4858/8459 = 57%, 72 KB/s], Decompressed: 4851 Downloaded: 4892 file(s) [attempted 4892/8459 = 57%, 427 KB/s], Decompressed: 4872 Downloaded: 4933 file(s) [attempted 4933/8459 = 58%, 367 KB/s], Decompressed: 4906 Downloaded: 4978 file(s) [attempted 4978/8459 = 58%, 58 KB/s], Decompressed: 4906 Downloaded: 5015 file(s) [attempted 5015/8459 = 59%, 217 KB/s], Decompressed: 4998 Downloaded: 5053 file(s) [attempted 5053/8459 = 59%, 36 KB/s], Decompressed: 5032 Downloaded: 5094 file(s) [attempted 5094/8459 = 60%, 603 KB/s], Decompressed: 5032 Downloaded: 5135 file(s) [attempted 5135/8459 = 60%, 350 KB/s], Decompressed: 5039 Downloaded: 5180 file(s) [attempted 5180/8459 = 61%, 344 KB/s], Decompressed: 5169 Downloaded: 5214 file(s) [attempted 5214/8459 = 61%, 130 KB/s], Decompressed: 5210 Downloaded: 5255 file(s) [attempted 5255/8459 = 62%, 90 KB/s], Decompressed: 5248 Downloaded: 5296 file(s) [attempted 5296/8459 = 62%, 60 KB/s], Decompressed: 5293 Downloaded: 5340 file(s) [attempted 5340/8459 = 63%, 252 KB/s], Decompressed: 5334 Downloaded: 5381 file(s) [attempted 5381/8459 = 63%, 59 KB/s], Decompressed: 5371 Downloaded: 5416 file(s) [attempted 5416/8459 = 64%, 30 KB/s], Decompressed: 5405 Downloaded: 5460 file(s) [attempted 5460/8459 = 64%, 263 KB/s], Decompressed: 5457 Downloaded: 5501 file(s) [attempted 5501/8459 = 65%, 298 KB/s], Decompressed: 5494 Downloaded: 5542 file(s) [attempted 5542/8459 = 65%, 39 KB/s], Decompressed: 5536 Downloaded: 5580 file(s) [attempted 5580/8459 = 65%, 489 KB/s], Decompressed: 5566 Downloaded: 5614 file(s) [attempted 5614/8459 = 66%, 387 KB/s], Decompressed: 5611 Downloaded: 5662 file(s) [attempted 5662/8459 = 66%, 218 KB/s], Decompressed: 5614 Downloaded: 5703 file(s) [attempted 5703/8459 = 67%, 68 KB/s], Decompressed: 5614 Downloaded: 5744 file(s) [attempted 5744/8459 = 67%, 38 KB/s], Decompressed: 5737 Downloaded: 5789 file(s) [attempted 5789/8459 = 68%, 435 KB/s], Decompressed: 5744 Downloaded: 5826 file(s) [attempted 5826/8459 = 68%, 103 KB/s], Decompressed: 5744 Downloaded: 5864 file(s) [attempted 5864/8459 = 69%, 167 KB/s], Decompressed: 5854 Downloaded: 5905 file(s) [attempted 5905/8459 = 69%, 341 KB/s], Decompressed: 5898 Downloaded: 5946 file(s) [attempted 5946/8459 = 70%, 101 KB/s], Decompressed: 5939 Downloaded: 5984 file(s) [attempted 5984/8459 = 70%, 242 KB/s], Decompressed: 5977 Downloaded: 6025 file(s) [attempted 6025/8459 = 71%, 29 KB/s], Decompressed: 6015 Downloaded: 6059 file(s) [attempted 6059/8459 = 71%, 564 KB/s], Decompressed: 6052 Downloaded: 6100 file(s) [attempted 6100/8459 = 72%, 601 KB/s], Decompressed: 6093 Downloaded: 6141 file(s) [attempted 6141/8459 = 72%, 938 KB/s], Decompressed: 6107 Downloaded: 6186 file(s) [attempted 6186/8459 = 73%, 700 KB/s], Decompressed: 6107 Downloaded: 6223 file(s) [attempted 6223/8459 = 73%, 123 KB/s], Decompressed: 6213 Downloaded: 6258 file(s) [attempted 6258/8459 = 73%, 68 KB/s], Decompressed: 6251 Downloaded: 6295 file(s) [attempted 6295/8459 = 74%, 729 KB/s], Decompressed: 6292 Downloaded: 6340 file(s) [attempted 6340/8459 = 74%, 674 KB/s], Decompressed: 6329 Downloaded: 6381 file(s) [attempted 6381/8459 = 75%, 36 KB/s], Decompressed: 6371 Downloaded: 6422 file(s) [attempted 6422/8459 = 75%, 1386 KB/s], Decompressed: 6408 Downloaded: 6460 file(s) [attempted 6460/8459 = 76%, 603 KB/s], Decompressed: 6449 Downloaded: 6501 file(s) [attempted 6501/8459 = 76%, 169 KB/s], Decompressed: 6497 Downloaded: 6545 file(s) [attempted 6545/8459 = 77%, 513 KB/s], Decompressed: 6538 Downloaded: 6583 file(s) [attempted 6583/8459 = 77%, 347 KB/s], Decompressed: 6572 Downloaded: 6623 file(s) [attempted 6623/8459 = 78%, 539 KB/s], Decompressed: 6610 Downloaded: 6665 file(s) [attempted 6665/8459 = 78%, 81 KB/s], Decompressed: 6620 Downloaded: 6703 file(s) [attempted 6703/8459 = 79%, 242 KB/s], Decompressed: 6620 Downloaded: 6747 file(s) [attempted 6747/8459 = 79%, 110 KB/s], Decompressed: 6716 Downloaded: 6785 file(s) [attempted 6785/8459 = 80%, 533 KB/s], Decompressed: 6781 Downloaded: 6826 file(s) [attempted 6826/8459 = 80%, 1363 KB/s], Decompressed: 6809 Downloaded: 6867 file(s) [attempted 6867/8459 = 81%, 91 KB/s], Decompressed: 6860 Downloaded: 6904 file(s) [attempted 6904/8459 = 81%, 167 KB/s], Decompressed: 6898 Downloaded: 6945 file(s) [attempted 6945/8459 = 82%, 203 KB/s], Decompressed: 6939 Downloaded: 6981 file(s) [attempted 6981/8459 = 82%, 493 KB/s], Decompressed: 6976 Downloaded: 7024 file(s) [attempted 7024/8459 = 83%, 694 KB/s], Decompressed: 7021 Downloaded: 7069 file(s) [attempted 7069/8459 = 83%, 144 KB/s], Decompressed: 7065 Downloaded: 7110 file(s) [attempted 7110/8459 = 84%, 51 KB/s], Decompressed: 7106 Downloaded: 7151 file(s) [attempted 7151/8459 = 84%, 112 KB/s], Decompressed: 7134 Downloaded: 7185 file(s) [attempted 7185/8459 = 84%, 1377 KB/s], Decompressed: 7178 Downloaded: 7226 file(s) [attempted 7226/8459 = 85%, 445 KB/s], Decompressed: 7223 Downloaded: 7271 file(s) [attempted 7271/8459 = 85%, 891 KB/s], Decompressed: 7260 Downloaded: 7314 file(s) [attempted 7314/8459 = 86%, 186 KB/s], Decompressed: 7308 Downloaded: 7353 file(s) [attempted 7353/8459 = 86%, 53 KB/s], Decompressed: 7342 Downloaded: 7390 file(s) [attempted 7390/8459 = 87%, 176 KB/s], Decompressed: 7380 Downloaded: 7428 file(s) [attempted 7428/8459 = 87%, 351 KB/s], Decompressed: 7421 Downloaded: 7473 file(s) [attempted 7473/8459 = 88%, 96 KB/s], Decompressed: 7445 Downloaded: 7512 file(s) [attempted 7512/8459 = 88%, 137 KB/s], Decompressed: 7500 Downloaded: 7548 file(s) [attempted 7548/8459 = 89%, 202 KB/s], Decompressed: 7541 Downloaded: 7587 file(s) [attempted 7587/8459 = 89%, 149 KB/s], Decompressed: 7579 Downloaded: 7630 file(s) [attempted 7630/8459 = 90%, 1030 KB/s], Decompressed: 7623 Downloaded: 7674 file(s) [attempted 7674/8459 = 90%, 1208 KB/s], Decompressed: 7668 Downloaded: 7716 file(s) [attempted 7716/8459 = 91%, 54 KB/s], Decompressed: 7702 Downloaded: 7750 file(s) [attempted 7750/8459 = 91%, 76 KB/s], Decompressed: 7743 Downloaded: 7794 file(s) [attempted 7794/8459 = 92%, 483 KB/s], Decompressed: 7787 Downloaded: 7835 file(s) [attempted 7835/8459 = 92%, 858 KB/s], Decompressed: 7822 Downloaded: 7880 file(s) [attempted 7880/8459 = 93%, 195 KB/s], Decompressed: 7876 Downloaded: 7928 file(s) [attempted 7928/8459 = 93%, 193 KB/s], Decompressed: 7917 Downloaded: 7969 file(s) [attempted 7969/8459 = 94%, 76 KB/s], Decompressed: 7965 Downloaded: 8003 file(s) [attempted 8003/8459 = 94%, 53 KB/s], Decompressed: 7996 Downloaded: 8044 file(s) [attempted 8044/8459 = 95%, 444 KB/s], Decompressed: 8037 Downloaded: 8085 file(s) [attempted 8085/8459 = 95%, 350 KB/s], Decompressed: 8071 Downloaded: 8123 file(s) [attempted 8123/8459 = 96%, 796 KB/s], Decompressed: 8119 Downloaded: 8167 file(s) [attempted 8167/8459 = 96%, 334 KB/s], Decompressed: 8160 Downloaded: 8206 file(s) [attempted 8206/8459 = 97%, 393 KB/s], Decompressed: 8195 Downloaded: 8243 file(s) [attempted 8243/8459 = 97%, 200 KB/s], Decompressed: 8195 Downloaded: 8287 file(s) [attempted 8287/8459 = 97%, 132 KB/s], Decompressed: 8205 Downloaded: 8328 file(s) [attempted 8328/8459 = 98%, 534 KB/s], Decompressed: 8318 Downloaded: 8369 file(s) [attempted 8369/8459 = 98%, 469 KB/s], Decompressed: 8366 Downloaded: 8410 file(s) [attempted 8410/8459 = 99%, 957 KB/s], Decompressed: 8400 Downloaded: 8448 file(s) [attempted 8448/8459 = 99%, 220 KB/s], Decompressed: 8444 Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 220 KB/s], Decompressed: 8455
lean_checker exit 0
lake build
ℹ [3536/3547] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3561/3571] Replayed PrimeNumberTheoremAnd.StrongPNT
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1475:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1524:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1641:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1786:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2181:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2271:6: declaration uses `sorry`
✔ [3566/3572] Built PrimeNumberTheoremAnd.BorelCaratheodory (126s)
⚠ [3694/3709] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3812/3819] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3817/3820] Built PrimeNumberTheoremAnd.IEANTN.Mertens (13s)
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:922:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:935:16: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:948:16: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:961:16: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:973:16: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1039:8: declaration uses `sorry`
⚠ [3880/3892] Built PrimeNumberTheoremAnd.IEANTN.ZetaAppendix (49s)
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2577:8: `simp [v, Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2578:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2599:8: `simp [v', Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2600:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2817:8: `simp [v, Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2818:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2833:8: `simp [v', Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2834:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2963:4: `simp [W]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2964:4: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3069:4: `simp [p]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3070:4: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3084:4: `simp [Set.uIcc_of_le hab]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3084:4: Try this:
[apply] simp only [_root_.deriv_ofReal]
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3085:4: `fun_prop` uses `⊢`!
⚠ [3881/3892] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
⚠ [3883/3893] Built PrimeNumberTheoremAnd.IEANTN.ZetaSummary (19s)
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:35:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:48:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:58:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:68:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:78:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:88:8: declaration uses `sorry`
✔ [3887/3894] Built PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions (2.5s)
✔ [3890/3895] Built PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions (7.6s)
⚠ [3891/3895] Built PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky (5.1s)
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:45:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:112:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:149:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:153:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:165:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:177:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:218:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:228:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:257:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:354:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:368:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:383:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:402:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:408:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:418:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:464:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:473:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:488:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:530:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:557:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:585:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:636:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:649:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:661:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:705:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:715:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:728:8: declaration uses `sorry`
✔ [3894/3907] Built PrimeNumberTheoremAnd.IEANTN.CostaPereira (8.6s)
⚠ [4017/4025] Built PrimeNumberTheoremAnd.IEANTN.Buthe (10s)
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:31:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:41:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:51:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:61:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:83:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:131:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:142:8: declaration uses `sorry`
⚠ [4018/4025] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app (16s)
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:47:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:168:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:516:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1127:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1180:8: declaration uses `sorry`
⚠ [4020/4026] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime (10s)
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
⚠ [4022/4055] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW (26s)
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1518:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2184:8: declaration uses `sorry`
✔ [4033/4061] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_a2_bounds (10s)
✔ [4036/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core (7.4s)
✔ [4038/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_65_85 (17s)
✔ [4039/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_misc (10s)
✔ [4040/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_12600_24000 (65s)
✔ [4041/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_10600_12500 (58s)
✔ [4042/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_8600_10500 (54s)
✔ [4043/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_6600_8500 (57s)
✔ [4044/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4900_6500 (62s)
✔ [4045/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4400_4875 (70s)
✔ [4046/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3900_4375 (56s)
✔ [4047/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3400_3875 (53s)
✔ [4048/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2900_3375 (51s)
✔ [4049/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2400_2875 (50s)
✔ [4050/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_1900_2375 (48s)
✔ [4051/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_100_1875 (55s)
✔ [4052/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_90_95 (15s)
✔ [4053/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_values (9.3s)
✔ [4054/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_next (16s)
ℹ [4055/4068] Built PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 (46s)
info: PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:359:15: Try this:
[apply] ring_nf
The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
✔ [4057/4068] Built PrimeNumberTheoremAnd.IEANTN.PrimeInInterval (15s)
✔ [4059/4072] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_20_43 (66s)
⚠ [4060/4074] Built PrimeNumberTheoremAnd.IEANTN.CH2.CH2 (21s)
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3156:8: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3245:4: Try this:
[apply] ring_nf
The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3615:4: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.
Note: This linter can be disabled with `set_option linter.style.show false`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:4207:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:4221:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:4235:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:4247:8: declaration uses `sorry`
⚠ [4062/4074] Replayed PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:85:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:129:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:304:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:449:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:464:8: declaration uses `sorry`
✔ [4064/4074] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_44_59 (39s)
✔ [4066/4074] Built PrimeNumberTheoremAnd.IEANTN.Chebyshev (15s)
⚠ [4067/4074] Built PrimeNumberTheoremAnd.IEANTN.Dusart (16s)
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:89:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:148:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:171:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:274:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:286:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:310:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:321:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:332:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:343:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:354:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:366:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:377:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:388:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:399:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:410:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:620:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:680:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:692:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:705:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:716:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:728:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:736:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:748:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:760:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:772:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:784:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:796:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:808:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:820:8: declaration uses `sorry`
✔ [4070/4074] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows (4.8s)
⚠ [4072/4074] Built PrimeNumberTheoremAnd.IEANTN.FKS2 (56s)
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:316:2: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.
Note: This linter can be disabled with `set_option linter.style.show false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3776:32: Try this:
[apply] ring_nf
The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3781:4: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.
Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3784:6: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.
Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3786:4: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.
Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3776:32: The following tactic starts with 2 goals and ends with 2 goals, 1 of which is not operated on.
ring
Please focus on the current goal, for instance using `·` (typed as "\.").
Note: This linter can be disabled with `set_option linter.style.multiGoal false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3827:4: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.
Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3830:8: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.
Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: `simp_all +decide [ επ_num, μ_num ]` is a flexible tactic modifying `⊢`. Try `simp_all?` and use the suggested `simp_all only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: Try this:
[apply] simp_all +decide only [ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3836:4: `have h63 :=
theorem_6_3 (by linarith : 14 ≤ x₁) x₂.toReal
(by
cases x₂ <;> norm_num at *; · linarith;
· exact absurd hc (by exact ne_of_lt (EReal.coe_lt_top _)))
x hx₁
(by
cases x₂ <;> norm_num at *; · linarith;
· exact absurd hc (by exact ne_of_lt (EReal.coe_lt_top _)))
(by
cases x₂ <;> norm_num at *; · exact_mod_cast hc;
· exact mul_nonneg (by linarith) (Real.log_nonneg (by linarith)))` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: `simp_all +decide [ επ_num, μ_num ]` is a flexible tactic modifying `⊢`. Try `simp_all?` and use the suggested `simp_all only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: Try this:
[apply] simp_all +decide only [ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3846:4: `unfold μ_num_1` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3847:35: `simp_all +decide [ mul_assoc, mul_comm, mul_left_comm ]` is a flexible tactic modifying `⊢`. Try `simp_all?` and use the suggested `simp_all only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3847:35: Try this:
[apply] simp_all +decide only [Fin.Iio_last_eq_map, Finset.sum_sub_distrib, Finset.sum_map, Fin.coe_castSuccEmb,
Fin.coeSucc_eq_succ, ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3849:6: `exact absurd (this y hy₁) (by norm_num [h]; linarith)` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: `simp_all +decide [ επ_num, μ_num ]` is a flexible tactic modifying `⊢`. Try `simp_all?` and use the suggested `simp_all only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: Try this:
[apply] simp_all +decide only [ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3858:6: `exact absurd ‹_› (not_le_of_gt hc)` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4652:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4679:8: declaration uses `sorry`
✔ [4073/4079] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_dispatch (26s)
✔ [4087/4108] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtCore (17s)
✔ [4091/4109] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_13 (13s)
✔ [4092/4109] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_12 (21s)
✔ [4093/4109] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_11 (21s)
✔ [4094/4109] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_10 (21s)
✔ [4095/4109] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_09 (20s)
✔ [4096/4109] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_08 (21s)
✔ [4097/4109] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_07 (21s)
✔ [4098/4109] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_06 (20s)
✔ [4099/4109] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_05 (21s)
✔ [4100/4109] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_04 (21s)
✔ [4101/4109] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_03 (21s)
✔ [4102/4109] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_02 (20s)
✔ [4103/4109] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_01 (20s)
✔ [4104/4110] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_00 (21s)
⚠ [4107/4111] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext (3.7s)
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean:116:8: declaration uses `sorry`
⚠ [4109/4116] Built PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor (6.6s)
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:19:72: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.
Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:109:37: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.
Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:122:60: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.
Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
⚠ [4121/4130] Replayed PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting
warning: PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:2045:6: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.
Note: This linter can be disabled with `set_option linter.style.show false`
✔ [4125/4166] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower (9.2s)
⚠ [4144/4181] Built PrimeNumberTheoremAnd.IEANTN.TMEEMT (13s)
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:93:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:104:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:117:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:146:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:154:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:179:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:187:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:195:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:333:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:341:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:470:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:515:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:530:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:564:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:573:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:582:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:591:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:600:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:616:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:625:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:634:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:643:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:678:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:687:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:696:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:722:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:745:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:756:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:767:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:778:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:788:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:796:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:805:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:814:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:937:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:957:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:987:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1013:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1027:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1035:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1050:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1065:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1074:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1089:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1107:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1119:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1136:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1147:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1169:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1183:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1197:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1227:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1243:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1254:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1278:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1292:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1306:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1320:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1334:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1369:8: declaration uses `sorry`
⚠ [4152/4187] Built PrimeNumberTheoremAnd.IEANTN.SecondarySummary (9.4s)
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:61:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:204:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:214:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:228:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:243:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:256:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:338:8: declaration uses `sorry`
✔ [4154/4187] Built PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.DigammaSeries (17s)
ℹ [4157/4187] Replayed PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations
info: PrimeNumberTheoremAnd/IEANTN/Ramanujan/RamanujanCalculations.lean:76:4: Try this:
[apply] ring_nf
The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
⚠ [4158/4187] Replayed PrimeNumberTheoremAnd.IwaniecKowalskiCh1
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:74:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:91:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:638:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:680:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:718:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:986:3: error: doc-strings should start with a single space or newline
Note: This linter can be disabled with `set_option linter.style.docString false`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1259:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1429:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1444:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1456:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1474:6: declaration uses `sorry`
✔ [4163/4187] Built PrimeNumberTheoremAnd.IEANTN.MobiusLemma (10s)
⚠ [4166/4187] Built PrimeNumberTheoremAnd.IEANTN.Goldbach (6.2s)
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
✔ [4168/4187] Built PrimeNumberTheoremAnd.LaplaceInversion (9.7s)
✔ [4169/4187] Built PrimeNumberTheoremAnd.IEANTN.Lcm (25s)
✔ [4170/4187] Built PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan (51s)
✔ [4171/4187] Built PrimeNumberTheoremAnd.PerronFormula (6.5s)
✔ [4173/4187] Built PrimeNumberTheoremAnd.IEANTN.PrimarySummary (2.7s)
⚠ [4185/4187] Built PrimeNumberTheoremAnd.IEANTN.Kadiri (12s)
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:132:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:169:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:206:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:277:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:325:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:357:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1277:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1320:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1407:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1490:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2720:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2746:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:3352:8: declaration uses `sorry`
✔ [4186/4187] Built PrimeNumberTheoremAnd (4.4s)
Build completed successfully (4187 jobs).
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
blueprint_build exit 0
lake build :blueprint
✔ [15/35] Built Batteries.Lean.NameMapAttribute:c.o (1.4s)
✔ [26/35] Built Cli.Basic:c.o (2.0s)
✔ [30/35] Built Cli.Extensions:c.o (492ms)
✔ [33/39] Built Cli:c.o (62ms)
ℹ [3594/3612] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3619/3643] Replayed PrimeNumberTheoremAnd.StrongPNT
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1475:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1524:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1641:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1786:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2181:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2271:6: declaration uses `sorry`
✔ [3637/3647] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.BorelCaratheodory:blueprint (10s)
⚠ [3764/3773] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3891/3902] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3894/3902] Replayed PrimeNumberTheoremAnd.IEANTN.Mertens
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:922:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:935:16: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:948:16: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:961:16: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:973:16: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1039:8: declaration uses `sorry`
✔ [3900/3910] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Mertens:blueprint (43s)
⚠ [3960/3986] Replayed PrimeNumberTheoremAnd.IEANTN.ZetaAppendix
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2577:8: `simp [v, Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2578:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2599:8: `simp [v', Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2600:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2817:8: `simp [v, Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2818:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2833:8: `simp [v', Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2834:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2963:4: `simp [W]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2964:4: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3069:4: `simp [p]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3070:4: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3084:4: `simp [Set.uIcc_of_le hab]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3084:4: Try this:
[apply] simp only [_root_.deriv_ofReal]
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3085:4: `fun_prop` uses `⊢`!
⚠ [3962/3986] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
✔ [3967/3988] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaAppendix:blueprint (25s)
⚠ [3968/3988] Replayed PrimeNumberTheoremAnd.IEANTN.ZetaSummary
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:35:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:48:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:58:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:68:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:78:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:88:8: declaration uses `sorry`
✔ [3974/3988] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaSummary:blueprint (3.2s)
✔ [3981/3990] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions:blueprint (2.7s)
⚠ [3982/3990] Replayed PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:45:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:112:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:149:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:153:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:165:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:177:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:218:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:228:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:257:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:354:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:368:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:383:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:402:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:408:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:418:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:464:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:473:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:488:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:530:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:557:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:585:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:636:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:649:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:661:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:705:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:715:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:728:8: declaration uses `sorry`
✔ [3984/3992] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky:blueprint (15s)
✔ [3985/3992] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions:blueprint (9.1s)
✔ [3988/4000] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CostaPereira:blueprint (6.4s)
⚠ [4106/4122] Replayed PrimeNumberTheoremAnd.IEANTN.Buthe
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:31:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:41:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:51:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:61:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:83:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:131:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:142:8: declaration uses `sorry`
⚠ [4111/4130] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
✔ [4114/4130] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Buthe:blueprint (6.1s)
⚠ [4115/4130] Replayed PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:47:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:168:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:516:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1127:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1180:8: declaration uses `sorry`
✔ [4119/4178] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime:blueprint (20s)
✔ [4120/4178] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app:blueprint (17s)
⚠ [4122/4178] Replayed PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1518:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2184:8: declaration uses `sorry`
✔ [4125/4186] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW:blueprint (23s)
✔ [4136/4198] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_a2_bounds:blueprint (4.7s)
✔ [4139/4200] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core:blueprint (2.9s)
ℹ [4148/4200] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1
info: PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:359:15: Try this:
[apply] ring_nf
The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
✔ [4161/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_next:blueprint (2.0s)
✔ [4162/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_values:blueprint (2.9s)
✔ [4164/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_65_85:blueprint (2.9s)
✔ [4165/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_90_95:blueprint (2.9s)
✔ [4166/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_100_1875:blueprint (2.9s)
✔ [4167/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_1900_2375:blueprint (2.9s)
✔ [4168/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2400_2875:blueprint (2.9s)
✔ [4169/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2900_3375:blueprint (2.9s)
✔ [4170/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3400_3875:blueprint (2.9s)
✔ [4171/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3900_4375:blueprint (2.9s)
✔ [4172/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4400_4875:blueprint (3.0s)
✔ [4173/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4900_6500:blueprint (2.0s)
✔ [4174/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_6600_8500:blueprint (2.9s)
✔ [4175/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_8600_10500:blueprint (2.9s)
✔ [4176/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_10600_12500:blueprint (2.0s)
✔ [4177/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_12600_24000:blueprint (2.9s)
✔ [4178/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_misc:blueprint (2.9s)
✔ [4179/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1:blueprint (49s)
⚠ [4180/4206] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3156:8: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3245:4: Try this:
[apply] ring_nf
The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3615:4: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.
Note: This linter can be disabled with `set_option linter.style.show false`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:4207:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:4221:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:4235:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:4247:8: declaration uses `sorry`
✔ [4182/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimeInInterval:blueprint (4.4s)
⚠ [4184/4206] Replayed PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:85:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:129:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:304:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:449:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:464:8: declaration uses `sorry`
✔ [4187/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_20_43:blueprint (2.9s)
✔ [4189/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CH2.CH2:blueprint (18s)
⚠ [4192/4206] Replayed PrimeNumberTheoremAnd.IEANTN.Dusart
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:89:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:148:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:171:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:274:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:286:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:310:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:321:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:332:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:343:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:354:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:366:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:377:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:388:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:399:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:410:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:620:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:680:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:692:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:705:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:716:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:728:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:736:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:748:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:760:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:772:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:784:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:796:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:808:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:820:8: declaration uses `sorry`
✔ [4195/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_44_59:blueprint (2.9s)
✔ [4197/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Chebyshev:blueprint (17s)
✔ [4198/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Dusart:blueprint (18s)
⚠ [4200/4206] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:316:2: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.
Note: This linter can be disabled with `set_option linter.style.show false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3776:32: Try this:
[apply] ring_nf
The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3781:4: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.
Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3784:6: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.
Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3786:4: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.
Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3776:32: The following tactic starts with 2 goals and ends with 2 goals, 1 of which is not operated on.
ring
Please focus on the current goal, for instance using `·` (typed as "\.").
Note: This linter can be disabled with `set_option linter.style.multiGoal false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3827:4: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.
Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3830:8: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.
Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: `simp_all +decide [ επ_num, μ_num ]` is a flexible tactic modifying `⊢`. Try `simp_all?` and use the suggested `simp_all only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: Try this:
[apply] simp_all +decide only [ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3836:4: `have h63 :=
theorem_6_3 (by linarith : 14 ≤ x₁) x₂.toReal
(by
cases x₂ <;> norm_num at *; · linarith;
· exact absurd hc (by exact ne_of_lt (EReal.coe_lt_top _)))
x hx₁
(by
cases x₂ <;> norm_num at *; · linarith;
· exact absurd hc (by exact ne_of_lt (EReal.coe_lt_top _)))
(by
cases x₂ <;> norm_num at *; · exact_mod_cast hc;
· exact mul_nonneg (by linarith) (Real.log_nonneg (by linarith)))` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: `simp_all +decide [ επ_num, μ_num ]` is a flexible tactic modifying `⊢`. Try `simp_all?` and use the suggested `simp_all only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: Try this:
[apply] simp_all +decide only [ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3846:4: `unfold μ_num_1` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3847:35: `simp_all +decide [ mul_assoc, mul_comm, mul_left_comm ]` is a flexible tactic modifying `⊢`. Try `simp_all?` and use the suggested `simp_all only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3847:35: Try this:
[apply] simp_all +decide only [Fin.Iio_last_eq_map, Finset.sum_sub_distrib, Finset.sum_map, Fin.coe_castSuccEmb,
Fin.coeSucc_eq_succ, ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3849:6: `exact absurd (this y hy₁) (by norm_num [h]; linarith)` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: `simp_all +decide [ επ_num, μ_num ]` is a flexible tactic modifying `⊢`. Try `simp_all?` and use the suggested `simp_all only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: Try this:
[apply] simp_all +decide only [ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3858:6: `exact absurd ‹_› (not_le_of_gt hc)` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4652:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4679:8: declaration uses `sorry`
✔ [4201/4212] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows:blueprint (2.9s)
✔ [4204/4212] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2:blueprint (30s)
✔ [4206/4259] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_dispatch:blueprint (14s)
✔ [4223/4261] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtCore:blueprint (3.0s)
✔ [4241/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_00:blueprint (2.9s)
✔ [4242/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_01:blueprint (2.9s)
✔ [4243/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_02:blueprint (2.9s)
✔ [4244/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_03:blueprint (2.9s)
✔ [4245/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_04:blueprint (2.9s)
✔ [4246/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_05:blueprint (2.9s)
✔ [4247/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_06:blueprint (2.9s)
✔ [4248/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_07:blueprint (2.9s)
✔ [4249/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_08:blueprint (2.9s)
✔ [4250/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_09:blueprint (2.9s)
✔ [4251/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_10:blueprint (2.9s)
✔ [4252/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_11:blueprint (2.0s)
✔ [4253/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_12:blueprint (2.9s)
✔ [4254/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_13:blueprint (2.9s)
⚠ [4255/4262] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean:116:8: declaration uses `sorry`
✔ [4257/4264] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext:blueprint (2.9s)
⚠ [4258/4264] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:19:72: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.
Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:109:37: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.
Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:122:60: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.
Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
✔ [4261/4299] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor:blueprint (5.5s)
⚠ [4272/4299] Replayed PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting
warning: PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:2045:6: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.
Note: This linter can be disabled with `set_option linter.style.show false`
✔ [4279/4356] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower:blueprint (3.1s)
⚠ [4280/4356] Replayed PrimeNumberTheoremAnd.IEANTN.TMEEMT
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:93:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:104:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:117:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:146:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:154:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:179:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:187:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:195:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:333:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:341:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:470:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:515:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:530:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:564:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:573:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:582:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:591:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:600:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:616:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:625:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:634:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:643:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:678:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:687:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:696:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:722:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:745:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:756:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:767:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:778:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:788:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:796:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:805:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:814:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:937:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:957:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:987:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1013:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1027:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1035:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1050:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1065:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1074:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1089:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1107:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1119:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1136:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1147:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1169:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1183:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1197:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1227:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1243:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1254:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1278:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1292:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1306:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1320:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1334:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1369:8: declaration uses `sorry`
✔ [4299/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.TMEEMT:blueprint (43s)
⚠ [4300/4395] Replayed PrimeNumberTheoremAnd.IEANTN.SecondarySummary
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:61:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:204:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:214:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:228:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:243:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:256:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:338:8: declaration uses `sorry`
ℹ [4328/4395] Replayed PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations
info: PrimeNumberTheoremAnd/IEANTN/Ramanujan/RamanujanCalculations.lean:76:4: Try this:
[apply] ring_nf
The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
⚠ [4329/4395] Replayed PrimeNumberTheoremAnd.IwaniecKowalskiCh1
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:74:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:91:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:638:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:680:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:718:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:986:3: error: doc-strings should start with a single space or newline
Note: This linter can be disabled with `set_option linter.style.docString false`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1259:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1429:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1444:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1456:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1474:6: declaration uses `sorry`
✔ [4333/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondarySummary:blueprint (6.5s)
⚠ [4334/4395] Replayed PrimeNumberTheoremAnd.IEANTN.Goldbach
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
✔ [4344/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.DigammaSeries:blueprint (2.4s)
✔ [4354/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.MobiusLemma:blueprint (10s)
✔ [4356/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Goldbach:blueprint (5.8s)
✔ [4379/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.LaplaceInversion:blueprint (2.5s)
✔ [4380/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Lcm:blueprint (10s)
✔ [4381/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimarySummary:blueprint (2.8s)
✔ [4382/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan:blueprint (14s)
✔ [4384/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.PerronFormula:blueprint (20s)
⚠ [4390/4395] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:132:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:169:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:206:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:277:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:325:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:357:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1277:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1320:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1407:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1490:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2720:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2746:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:3352:8: declaration uses `sorry`
✔ [4391/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Kadiri:blueprint (42s)
✔ [4393/4396] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (3.2s)
ℹ [4394/4396] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (60ms)
info: Blueprint indexing
Build completed successfully (4396 jobs).
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00000)
apx-semantic-phase {"duration_ms":4,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":20,"diagnostic_count":12,"duration_ms":1445,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":20,"dependency_count":29,"diagnostic_count":110,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":363804,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":20,"dependency_count":29,"diagnostic_count":110,"duration_ms":107,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":173726,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":3,"ok":true,"payload_bytes":173726,"phase":"lean_json_write"}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"core_compile","duration_ms":4304}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":168,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":25,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":4048,"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 5741e1a44ae06aad78a68854fd2e21d57fb81612889b2505612cab2fd9c44553
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":369119,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00001)
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":97,"diagnostic_count":49,"duration_ms":7409,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":97,"dependency_count":170,"diagnostic_count":1037,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":359054,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":97,"dependency_count":170,"diagnostic_count":1037,"duration_ms":232,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":1249897,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":1,"ok":true,"payload_bytes":1249897,"phase":"lean_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":22}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":191,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":24,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":3655,"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 5b77841087ccab3bcfb34d5a043c9fa5b17370b1dfa57d99f47ad48210893493
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":370464,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00002)
apx-semantic-phase {"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":209,"diagnostic_count":121,"duration_ms":12350,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":209,"dependency_count":112,"diagnostic_count":121,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":286194,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":209,"dependency_count":112,"diagnostic_count":121,"duration_ms":138,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":2085440,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":3,"ok":true,"payload_bytes":2085440,"phase":"lean_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":24}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":140,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":25,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":3225,"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 51b4d997b7ef0937d9360853ece8692b7955dcf8e72ba6aa1548224968760561
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":301879,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00003)
apx-semantic-phase {"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":320,"diagnostic_count":209,"duration_ms":23324,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":320,"dependency_count":576,"diagnostic_count":3709,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":369538,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":320,"dependency_count":576,"diagnostic_count":3709,"duration_ms":649,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":3206467,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":4,"ok":true,"payload_bytes":3206467,"phase":"lean_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":248,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":23,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":3942,"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 d203f7a84cac617a041c0c41d596da8a2cffed777b2b3d148400d0836b1525bd
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":397791,"ok":true}
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":30,"diagnostic_count":8,"duration_ms":1978,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":30,"dependency_count":56,"diagnostic_count":328,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":282937,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":30,"dependency_count":56,"diagnostic_count":328,"duration_ms":120,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":430335,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":1,"ok":true,"payload_bytes":430335,"phase":"lean_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":210,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":25,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":3496,"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 4bc71e7804c1e324b3fac66104e45900b93c56607d510147ae600737b5556517
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":288372,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00005)
apx-semantic-phase {"duration_ms":4,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":471,"diagnostic_count":322,"duration_ms":43187,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":471,"dependency_count":643,"diagnostic_count":5985,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":365701,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":471,"dependency_count":643,"diagnostic_count":5985,"duration_ms":1284,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":6685494,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":4,"ok":true,"payload_bytes":6685494,"phase":"lean_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":22}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":232,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":19,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":5222,"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 0e714cddd7a02b78dfce9acd49bcacbdf655be1af5aa62637bc5953e0f46df16
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":415065,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00006)
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":6,"diagnostic_count":0,"duration_ms":487,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":6,"dependency_count":0,"diagnostic_count":0,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":370265,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":6,"dependency_count":0,"diagnostic_count":0,"duration_ms":63,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":11386,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":11386,"phase":"lean_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":22}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":145,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":24,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":3888,"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 e69b7596a484b6aa56daebe3101274ace5df7ceac7a1d1a1621fde6aa454ca84
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":374555,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00007)
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":194,"diagnostic_count":65,"duration_ms":20495,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":194,"dependency_count":345,"diagnostic_count":120,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":369256,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":194,"dependency_count":345,"diagnostic_count":120,"duration_ms":165,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":2717344,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":2,"ok":true,"payload_bytes":2717344,"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":27,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":4774,"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 877107122381a5f781c625da64cd9679c19ba32c3ea30a90e77c1333fdc5405c
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":393730,"ok":true}
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":0,"diagnostic_count":0,"duration_ms":3,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":0,"dependency_count":0,"diagnostic_count":0,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":367123,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":0,"dependency_count":0,"diagnostic_count":0,"duration_ms":70,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":824,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":824,"phase":"lean_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":24}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":116,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":23,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":3660,"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 6016b85032006c16277cc4bcb8285554ca483116798671eee68247a861ce3c80
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":370661,"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":136,"diagnostic_count":71,"duration_ms":8804,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":136,"dependency_count":337,"diagnostic_count":821,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":379582,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":136,"dependency_count":337,"diagnostic_count":821,"duration_ms":201,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":835159,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":1,"ok":true,"payload_bytes":835159,"phase":"lean_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":22}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":172,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":23,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":5970,"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 50b5328954002592b7edc0486e8ae5f1152aa983fb8d62523a5a913cfb70afd9
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":392337,"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":36,"diagnostic_count":27,"duration_ms":2476,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":36,"dependency_count":27,"diagnostic_count":32,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":375709,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":36,"dependency_count":27,"diagnostic_count":32,"duration_ms":66,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":196734,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":1,"ok":true,"payload_bytes":196734,"phase":"lean_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":131,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":23,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":4079,"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 68d0f716f8355725ee6f9d7ee0e09b1245d653cb481c21c6c1d1ea185ef2dbd5
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":381921,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00011)
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":69,"diagnostic_count":54,"duration_ms":4822,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":69,"dependency_count":81,"diagnostic_count":54,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":363272,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":69,"dependency_count":81,"diagnostic_count":54,"duration_ms":103,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":450967,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":1,"ok":true,"payload_bytes":450967,"phase":"lean_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":21}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":114,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":22,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":3755,"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 18af009ee1a830d425537f50fe744e90c504913261a2f7bca928c9524a7e330c
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":371874,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00012)
apx-semantic-phase {"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":792,"diagnostic_count":519,"duration_ms":86080,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":792,"dependency_count":1446,"diagnostic_count":4839,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":365243,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":792,"dependency_count":1446,"diagnostic_count":4839,"duration_ms":903,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":7656056,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":5,"ok":true,"payload_bytes":7656056,"phase":"lean_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":206,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":15,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":3611,"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 db5d22bbf83d87b9a1c61e62f372485ff411f0f9d85e6f5bc1ca7d9c4c2e4ce8
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":456658,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00013)
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":24,"diagnostic_count":11,"duration_ms":1506,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":24,"dependency_count":38,"diagnostic_count":11,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":368825,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":24,"dependency_count":38,"diagnostic_count":11,"duration_ms":52,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":177128,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":1,"ok":true,"payload_bytes":177128,"phase":"lean_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":21}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":134,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":23,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":3704,"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 1d3717a4e3c625c11a320d9386f89a24144d0ba2b6dfca41d4b039313b24979e
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":374186,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00014)
apx-semantic-phase {"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":17,"diagnostic_count":10,"duration_ms":1058,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":17,"dependency_count":14,"diagnostic_count":24,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":375140,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":17,"dependency_count":14,"diagnostic_count":24,"duration_ms":89,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":110358,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":1,"ok":true,"payload_bytes":110358,"phase":"lean_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":21}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":150,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":22,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":3641,"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 c717b34e158e396b03478eefece2f27c878299f49f4b44d91292b43b6f53c94b
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":379927,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00015)
apx-semantic-phase {"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":57,"diagnostic_count":33,"duration_ms":3950,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":57,"dependency_count":128,"diagnostic_count":33,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":384504,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":57,"dependency_count":128,"diagnostic_count":33,"duration_ms":74,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":196513,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":196513,"phase":"lean_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":127,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":20,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":6773,"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 d3a54fbe1a8ca53303a50de52609a68b329948be498efcbe587263568df4249f
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":392350,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00016)
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":38,"diagnostic_count":28,"duration_ms":2693,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":38,"dependency_count":30,"diagnostic_count":28,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":382864,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":38,"dependency_count":30,"diagnostic_count":28,"duration_ms":71,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":318410,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":318410,"phase":"lean_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":22}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":133,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":22,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":3777,"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 2bb7262fc3426db0348f4842d887f6e4b95e31b0be86ef935773b25e74197268
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":389372,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00017)
apx-semantic-phase {"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":367,"diagnostic_count":137,"duration_ms":39135,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":367,"dependency_count":1331,"diagnostic_count":187,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":373778,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":367,"dependency_count":1331,"diagnostic_count":187,"duration_ms":250,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":3138984,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":2,"ok":true,"payload_bytes":3138984,"phase":"lean_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":9}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":112,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":19,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":3908,"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 af4e8eb363ed4bc674e410239e2538aa02a73f0eaadef9f96a6c3590c6afa1ec
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"lean_import_env_extract_write","duration_ms":417037,"ok":true}
semantic_extract exit -
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00018)
apx-semantic-phase {"phase":"core_compile","duration_ms":22}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":123,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":23,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":4113,"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 070e77e5c3334a7bcb19ace775ad6f6878902bc9e0961dcd1900b95f349e9efb
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
/usr/bin/podman timed out after 266s
podman cleanup removed verifier container apx-verifier-job-519-runtime-semantic_extract-2181-1781752473397778809-21 semantic_extract exit -
semantic_extract (extract-batch-00019)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00020)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00021)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00022)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00023)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00024)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00025)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00026)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00027)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00028)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00029)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00030)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00031)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00032)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00033)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00034)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00035)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00036)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00037)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started
semantic_extract exit -
semantic_extract (extract-batch-00038)
semantic extraction timed out: exact extraction budget of 7200s was exhausted before this batch started