Run 138

lake build :blueprint

✔ [27/35] Built Cli.Basic:c.o (7.5s)
✔ [30/35] Built Cli.Extensions:c.o (481ms)
✔ [33/41] Built Cli:c.o (69ms)
ℹ [3689/3724] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3707/3728] Replayed PrimeNumberTheoremAnd.StrongPNT
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1559:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1608:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1725:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1870:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2265:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2355:6: declaration uses `sorry`
⚠ [3848/3869] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3971/3983] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [4045/4067] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
⚠ [4052/4076] 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`
⚠ [4056/4076] 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`
⚠ [4201/4271] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1017:8: declaration uses `sorry`
⚠ [4205/4271] 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`
⚠ [4207/4271] 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`
⚠ [4211/4271] Replayed PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1519:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2185:8: declaration uses `sorry`
⚠ [4276/4302] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2634:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3685:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3699:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3713:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3725:8: declaration uses `sorry`
⚠ [4283/4302] 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`
⚠ [4285/4302] 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:737:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:749:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:761:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:773:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:785:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:797:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:809:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:821:8: declaration uses `sorry`
ℹ [4297/4352] 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.
⚠ [4300/4352] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4643:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4670:8: declaration uses `sorry`
⚠ [4349/4414] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean:116:8: declaration uses `sorry`
⚠ [4351/4414] 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`
⚠ [4393/4488] Replayed PrimeNumberTheoremAnd.IEANTN.TMEEMT
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:146:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:159:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:172:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:185:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:201:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:209:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:234:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:242:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:250:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:388:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:396:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:525:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:570:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:585:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:619:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:628:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:637:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:646:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:655:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:671:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:680:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:689:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:698:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:733:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:742:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:751:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:777:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:800:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:811:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:822:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:833:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:843:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:851:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:860:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:869:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:992:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1012:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1042:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1068:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1082:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1090:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1105:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1120:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1129:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1144:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1162:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1174:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1191:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1202:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1224:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1238:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1252:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1282:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1309:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1333:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1347:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1361:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1375:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1389:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1424:8: declaration uses `sorry`
⚠ [4425/4501] 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`
⚠ [4428/4501] 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`
✔ [4440/4501] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.KadiriEq12Foundations:blueprint (5.7s)
⚠ [4451/4501] Replayed PrimeNumberTheoremAnd.IEANTN.Goldbach
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
✔ [4457/4501] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.LaplaceInversion:blueprint (2.6s)
✔ [4472/4501] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.SincKernelErrorBounds:blueprint (2.5s)
✔ [4489/4501] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.KadiriSupport:blueprint (3.5s)
✔ [4495/4501] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.KadiriEq13:blueprint (8.8s)
⚠ [4496/4501] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:135:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:172:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:209:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:465:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:497:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1319:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1406:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1489:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2719:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2745:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:3351:8: declaration uses `sorry`
✔ [4497/4501] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Kadiri:blueprint (46s)
✔ [4499/4501] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (36s)
ℹ [4500/4502] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (80ms)
info: Blueprint indexing
Build completed successfully (4502 jobs).

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

lake exe cache get

Current branch: HEAD
Using cache from origin: (some leanprover-community/mathlib4)
Attempting to download 8546 file(s) from leanprover-community/mathlib4 cache at https://lakecache.blob.core.windows.net/mathlib4-master
Decompressed 8546 file(s)
Already decompressed 8546 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/8546 = 0%, 10 KB/s], Decompressed: 0
Downloaded: 15 file(s) [attempted 15/8546 = 0%, 1 KB/s], Decompressed: 13
Downloaded: 37 file(s) [attempted 37/8546 = 0%, 28 KB/s], Decompressed: 36
Downloaded: 64 file(s) [attempted 64/8546 = 0%, 329 KB/s], Decompressed: 61
Downloaded: 85 file(s) [attempted 85/8546 = 0%, 181 KB/s], Decompressed: 81
Downloaded: 114 file(s) [attempted 114/8546 = 1%, 76 KB/s], Decompressed: 105
Downloaded: 146 file(s) [attempted 146/8546 = 1%, 369 KB/s], Decompressed: 139
Downloaded: 183 file(s) [attempted 183/8546 = 2%, 141 KB/s], Decompressed: 177
Downloaded: 221 file(s) [attempted 221/8546 = 2%, 296 KB/s], Decompressed: 217
Downloaded: 248 file(s) [attempted 248/8546 = 2%, 576 KB/s], Decompressed: 244
Downloaded: 284 file(s) [attempted 284/8546 = 3%, 185 KB/s], Decompressed: 278
Downloaded: 322 file(s) [attempted 322/8546 = 3%, 149 KB/s], Decompressed: 319
Downloaded: 366 file(s) [attempted 366/8546 = 4%, 345 KB/s], Decompressed: 363
Downloaded: 398 file(s) [attempted 398/8546 = 4%, 109 KB/s], Decompressed: 393
Downloaded: 427 file(s) [attempted 427/8546 = 4%, 566 KB/s], Decompressed: 424
Downloaded: 454 file(s) [attempted 454/8546 = 5%, 685 KB/s], Decompressed: 451
Downloaded: 478 file(s) [attempted 478/8546 = 5%, 78 KB/s], Decompressed: 475
Downloaded: 505 file(s) [attempted 505/8546 = 5%, 144 KB/s], Decompressed: 502
Downloaded: 549 file(s) [attempted 549/8546 = 6%, 337 KB/s], Decompressed: 546
Downloaded: 593 file(s) [attempted 593/8546 = 6%, 371 KB/s], Decompressed: 590
Downloaded: 630 file(s) [attempted 630/8546 = 7%, 297 KB/s], Decompressed: 613
Downloaded: 654 file(s) [attempted 654/8546 = 7%, 847 KB/s], Decompressed: 651
Downloaded: 701 file(s) [attempted 701/8546 = 8%, 75 KB/s], Decompressed: 698
Downloaded: 752 file(s) [attempted 752/8546 = 8%, 150 KB/s], Decompressed: 746
Downloaded: 800 file(s) [attempted 800/8546 = 9%, 293 KB/s], Decompressed: 796
Downloaded: 847 file(s) [attempted 847/8546 = 9%, 217 KB/s], Decompressed: 844
Downloaded: 891 file(s) [attempted 891/8546 = 10%, 1597 KB/s], Decompressed: 888
Downloaded: 918 file(s) [attempted 918/8546 = 10%, 211 KB/s], Decompressed: 911
Downloaded: 962 file(s) [attempted 962/8546 = 11%, 401 KB/s], Decompressed: 959
Downloaded: 1002 file(s) [attempted 1002/8546 = 11%, 192 KB/s], Decompressed: 996
Downloaded: 1045 file(s) [attempted 1045/8546 = 12%, 582 KB/s], Decompressed: 1037
Downloaded: 1077 file(s) [attempted 1077/8546 = 12%, 58 KB/s], Decompressed: 1067
Downloaded: 1118 file(s) [attempted 1118/8546 = 13%, 68 KB/s], Decompressed: 1114
Downloaded: 1165 file(s) [attempted 1165/8546 = 13%, 150 KB/s], Decompressed: 1162
Downloaded: 1207 file(s) [attempted 1207/8546 = 14%, 59 KB/s], Decompressed: 1202
Downloaded: 1246 file(s) [attempted 1246/8546 = 14%, 274 KB/s], Decompressed: 1243
Downloaded: 1284 file(s) [attempted 1284/8546 = 15%, 56 KB/s], Decompressed: 1263
Downloaded: 1321 file(s) [attempted 1321/8546 = 15%, 798 KB/s], Decompressed: 1263
Downloaded: 1365 file(s) [attempted 1365/8546 = 15%, 54 KB/s], Decompressed: 1270
Downloaded: 1412 file(s) [attempted 1412/8546 = 16%, 88 KB/s], Decompressed: 1270
Downloaded: 1456 file(s) [attempted 1456/8546 = 17%, 125 KB/s], Decompressed: 1449
Downloaded: 1487 file(s) [attempted 1487/8546 = 17%, 611 KB/s], Decompressed: 1480
Downloaded: 1527 file(s) [attempted 1527/8546 = 17%, 987 KB/s], Decompressed: 1483
Downloaded: 1568 file(s) [attempted 1568/8546 = 18%, 257 KB/s], Decompressed: 1483
Downloaded: 1615 file(s) [attempted 1615/8546 = 18%, 44 KB/s], Decompressed: 1612
Downloaded: 1656 file(s) [attempted 1656/8546 = 19%, 259 KB/s], Decompressed: 1639
Downloaded: 1686 file(s) [attempted 1686/8546 = 19%, 122 KB/s], Decompressed: 1679
Downloaded: 1730 file(s) [attempted 1730/8546 = 20%, 243 KB/s], Decompressed: 1727
Downloaded: 1774 file(s) [attempted 1774/8546 = 20%, 299 KB/s], Decompressed: 1750
Downloaded: 1818 file(s) [attempted 1818/8546 = 21%, 284 KB/s], Decompressed: 1750
Downloaded: 1859 file(s) [attempted 1859/8546 = 21%, 111 KB/s], Decompressed: 1842
Downloaded: 1889 file(s) [attempted 1889/8546 = 22%, 298 KB/s], Decompressed: 1886
Downloaded: 1930 file(s) [attempted 1930/8546 = 22%, 627 KB/s], Decompressed: 1926
Downloaded: 1970 file(s) [attempted 1970/8546 = 23%, 650 KB/s], Decompressed: 1957
Downloaded: 2018 file(s) [attempted 2018/8546 = 23%, 103 KB/s], Decompressed: 1957
Downloaded: 2060 file(s) [attempted 2060/8546 = 24%, 442 KB/s], Decompressed: 2038
Downloaded: 2095 file(s) [attempted 2095/8546 = 24%, 22 KB/s], Decompressed: 2089
Downloaded: 2133 file(s) [attempted 2133/8546 = 24%, 78 KB/s], Decompressed: 2129
Downloaded: 2173 file(s) [attempted 2173/8546 = 25%, 128 KB/s], Decompressed: 2139
Downloaded: 2217 file(s) [attempted 2217/8546 = 25%, 137 KB/s], Decompressed: 2139
Downloaded: 2258 file(s) [attempted 2258/8546 = 26%, 105 KB/s], Decompressed: 2241
Downloaded: 2292 file(s) [attempted 2292/8546 = 26%, 570 KB/s], Decompressed: 2281
Downloaded: 2332 file(s) [attempted 2332/8546 = 27%, 133 KB/s], Decompressed: 2325
Downloaded: 2369 file(s) [attempted 2369/8546 = 27%, 237 KB/s], Decompressed: 2366
Downloaded: 2410 file(s) [attempted 2410/8546 = 28%, 244 KB/s], Decompressed: 2407
Downloaded: 2451 file(s) [attempted 2451/8546 = 28%, 139 KB/s], Decompressed: 2447
Downloaded: 2491 file(s) [attempted 2491/8546 = 29%, 865 KB/s], Decompressed: 2488
Downloaded: 2532 file(s) [attempted 2532/8546 = 29%, 149 KB/s], Decompressed: 2501
Downloaded: 2569 file(s) [attempted 2569/8546 = 30%, 413 KB/s], Decompressed: 2501
Downloaded: 2606 file(s) [attempted 2606/8546 = 30%, 61 KB/s], Decompressed: 2505
Downloaded: 2647 file(s) [attempted 2647/8546 = 30%, 339 KB/s], Decompressed: 2505
Downloaded: 2687 file(s) [attempted 2687/8546 = 31%, 174 KB/s], Decompressed: 2505
Downloaded: 2728 file(s) [attempted 2728/8546 = 31%, 468 KB/s], Decompressed: 2725
Downloaded: 2762 file(s) [attempted 2762/8546 = 32%, 564 KB/s], Decompressed: 2753
Downloaded: 2802 file(s) [attempted 2802/8546 = 32%, 31 KB/s], Decompressed: 2796
Downloaded: 2843 file(s) [attempted 2843/8546 = 33%, 34 KB/s], Decompressed: 2840
Downloaded: 2887 file(s) [attempted 2887/8546 = 33%, 246 KB/s], Decompressed: 2884
Downloaded: 2934 file(s) [attempted 2934/8546 = 34%, 785 KB/s], Decompressed: 2904
Downloaded: 2978 file(s) [attempted 2978/8546 = 34%, 198 KB/s], Decompressed: 2904
Downloaded: 3012 file(s) [attempted 3012/8546 = 35%, 292 KB/s], Decompressed: 3005
Downloaded: 3049 file(s) [attempted 3049/8546 = 35%, 296 KB/s], Decompressed: 3039
Downloaded: 3090 file(s) [attempted 3090/8546 = 36%, 166 KB/s], Decompressed: 3083
Downloaded: 3135 file(s) [attempted 3135/8546 = 36%, 689 KB/s], Decompressed: 3131
Downloaded: 3171 file(s) [attempted 3171/8546 = 37%, 42 KB/s], Decompressed: 3164
Downloaded: 3214 file(s) [attempted 3214/8546 = 37%, 1251 KB/s], Decompressed: 3202
Downloaded: 3246 file(s) [attempted 3246/8546 = 37%, 75 KB/s], Decompressed: 3239
Downloaded: 3286 file(s) [attempted 3286/8546 = 38%, 1015 KB/s], Decompressed: 3283
Downloaded: 3329 file(s) [attempted 3329/8546 = 38%, 689 KB/s], Decompressed: 3317
Downloaded: 3364 file(s) [attempted 3364/8546 = 39%, 561 KB/s], Decompressed: 3357
Downloaded: 3401 file(s) [attempted 3401/8546 = 39%, 258 KB/s], Decompressed: 3398
Downloaded: 3445 file(s) [attempted 3445/8546 = 40%, 175 KB/s], Decompressed: 3408
Downloaded: 3489 file(s) [attempted 3489/8546 = 40%, 289 KB/s], Decompressed: 3482
Downloaded: 3530 file(s) [attempted 3530/8546 = 41%, 752 KB/s], Decompressed: 3526
Downloaded: 3570 file(s) [attempted 3570/8546 = 41%, 38 KB/s], Decompressed: 3560
Downloaded: 3608 file(s) [attempted 3608/8546 = 42%, 119 KB/s], Decompressed: 3603
Downloaded: 3648 file(s) [attempted 3648/8546 = 42%, 558 KB/s], Decompressed: 3603
Downloaded: 3689 file(s) [attempted 3689/8546 = 43%, 645 KB/s], Decompressed: 3608
Downloaded: 3729 file(s) [attempted 3729/8546 = 43%, 587 KB/s], Decompressed: 3608
Downloaded: 3770 file(s) [attempted 3770/8546 = 44%, 480 KB/s], Decompressed: 3608
Downloaded: 3807 file(s) [attempted 3807/8546 = 44%, 167 KB/s], Decompressed: 3689
Downloaded: 3851 file(s) [attempted 3851/8546 = 45%, 483 KB/s], Decompressed: 3689
Downloaded: 3888 file(s) [attempted 3888/8546 = 45%, 82 KB/s], Decompressed: 3885
Downloaded: 3929 file(s) [attempted 3929/8546 = 45%, 418 KB/s], Decompressed: 3922
Downloaded: 3969 file(s) [attempted 3969/8546 = 46%, 289 KB/s], Decompressed: 3959
Downloaded: 4010 file(s) [attempted 4010/8546 = 46%, 317 KB/s], Decompressed: 4003
Downloaded: 4051 file(s) [attempted 4051/8546 = 47%, 31 KB/s], Decompressed: 4017
Downloaded: 4095 file(s) [attempted 4095/8546 = 47%, 24 KB/s], Decompressed: 4017
Downloaded: 4135 file(s) [attempted 4135/8546 = 48%, 995 KB/s], Decompressed: 4128
Downloaded: 4172 file(s) [attempted 4172/8546 = 48%, 56 KB/s], Decompressed: 4169
Downloaded: 4213 file(s) [attempted 4213/8546 = 49%, 23 KB/s], Decompressed: 4206
Downloaded: 4254 file(s) [attempted 4254/8546 = 49%, 671 KB/s], Decompressed: 4250
Downloaded: 4294 file(s) [attempted 4294/8546 = 50%, 54 KB/s], Decompressed: 4291
Downloaded: 4338 file(s) [attempted 4338/8546 = 50%, 653 KB/s], Decompressed: 4331
Downloaded: 4375 file(s) [attempted 4375/8546 = 51%, 221 KB/s], Decompressed: 4372
Downloaded: 4410 file(s) [attempted 4410/8546 = 51%, 261 KB/s], Decompressed: 4406
Downloaded: 4453 file(s) [attempted 4453/8546 = 52%, 104 KB/s], Decompressed: 4446
Downloaded: 4490 file(s) [attempted 4490/8546 = 52%, 96 KB/s], Decompressed: 4446
Downloaded: 4521 file(s) [attempted 4521/8546 = 52%, 242 KB/s], Decompressed: 4446
Downloaded: 4565 file(s) [attempted 4565/8546 = 53%, 381 KB/s], Decompressed: 4558
Downloaded: 4605 file(s) [attempted 4605/8546 = 53%, 75 KB/s], Decompressed: 4568
Downloaded: 4649 file(s) [attempted 4649/8546 = 54%, 116 KB/s], Decompressed: 4568
Downloaded: 4691 file(s) [attempted 4691/8546 = 54%, 97 KB/s], Decompressed: 4680
Downloaded: 4724 file(s) [attempted 4724/8546 = 55%, 223 KB/s], Decompressed: 4720
Downloaded: 4764 file(s) [attempted 4764/8546 = 55%, 121 KB/s], Decompressed: 4761
Downloaded: 4805 file(s) [attempted 4805/8546 = 56%, 1311 KB/s], Decompressed: 4768
Downloaded: 4842 file(s) [attempted 4842/8546 = 56%, 568 KB/s], Decompressed: 4768
Downloaded: 4881 file(s) [attempted 4881/8546 = 57%, 155 KB/s], Decompressed: 4876
Downloaded: 4920 file(s) [attempted 4920/8546 = 57%, 1140 KB/s], Decompressed: 4917
Downloaded: 4964 file(s) [attempted 4964/8546 = 58%, 734 KB/s], Decompressed: 4961
Downloaded: 5005 file(s) [attempted 5005/8546 = 58%, 344 KB/s], Decompressed: 5001
Downloaded: 5042 file(s) [attempted 5042/8546 = 58%, 294 KB/s], Decompressed: 5035
Downloaded: 5080 file(s) [attempted 5080/8546 = 59%, 588 KB/s], Decompressed: 5076
Downloaded: 5116 file(s) [attempted 5116/8546 = 59%, 3944 KB/s], Decompressed: 5103
Downloaded: 5154 file(s) [attempted 5154/8546 = 60%, 370 KB/s], Decompressed: 5150
Downloaded: 5194 file(s) [attempted 5194/8546 = 60%, 61 KB/s], Decompressed: 5187
Downloaded: 5235 file(s) [attempted 5235/8546 = 61%, 86 KB/s], Decompressed: 5204
Downloaded: 5275 file(s) [attempted 5275/8546 = 61%, 94 KB/s], Decompressed: 5204
Downloaded: 5313 file(s) [attempted 5313/8546 = 62%, 1553 KB/s], Decompressed: 5211
Downloaded: 5353 file(s) [attempted 5353/8546 = 62%, 372 KB/s], Decompressed: 5211
Downloaded: 5397 file(s) [attempted 5397/8546 = 63%, 189 KB/s], Decompressed: 5292
Downloaded: 5438 file(s) [attempted 5438/8546 = 63%, 843 KB/s], Decompressed: 5292
Downloaded: 5478 file(s) [attempted 5478/8546 = 64%, 218 KB/s], Decompressed: 5380
Downloaded: 5515 file(s) [attempted 5515/8546 = 64%, 939 KB/s], Decompressed: 5502
Downloaded: 5553 file(s) [attempted 5553/8546 = 64%, 95 KB/s], Decompressed: 5502
Downloaded: 5593 file(s) [attempted 5593/8546 = 65%, 622 KB/s], Decompressed: 5505
Downloaded: 5634 file(s) [attempted 5634/8546 = 65%, 122 KB/s], Decompressed: 5620
Downloaded: 5678 file(s) [attempted 5678/8546 = 66%, 756 KB/s], Decompressed: 5620
Downloaded: 5715 file(s) [attempted 5715/8546 = 66%, 50 KB/s], Decompressed: 5624
Downloaded: 5749 file(s) [attempted 5749/8546 = 67%, 422 KB/s], Decompressed: 5745
Downloaded: 5789 file(s) [attempted 5789/8546 = 67%, 657 KB/s], Decompressed: 5783
Downloaded: 5827 file(s) [attempted 5827/8546 = 68%, 458 KB/s], Decompressed: 5823
Downloaded: 5868 file(s) [attempted 5868/8546 = 68%, 443 KB/s], Decompressed: 5864
Downloaded: 5904 file(s) [attempted 5904/8546 = 69%, 237 KB/s], Decompressed: 5877
Downloaded: 5935 file(s) [attempted 5935/8546 = 69%, 176 KB/s], Decompressed: 5877
Downloaded: 5976 file(s) [attempted 5976/8546 = 69%, 51 KB/s], Decompressed: 5958
Downloaded: 6023 file(s) [attempted 6023/8546 = 70%, 128 KB/s], Decompressed: 5972
Downloaded: 6067 file(s) [attempted 6067/8546 = 70%, 711 KB/s], Decompressed: 5972
Downloaded: 6097 file(s) [attempted 6097/8546 = 71%, 90 KB/s], Decompressed: 6006
Downloaded: 6138 file(s) [attempted 6138/8546 = 71%, 230 KB/s], Decompressed: 6006
Downloaded: 6178 file(s) [attempted 6178/8546 = 72%, 166 KB/s], Decompressed: 6006
Downloaded: 6216 file(s) [attempted 6216/8546 = 72%, 799 KB/s], Decompressed: 6091
Downloaded: 6256 file(s) [attempted 6256/8546 = 73%, 211 KB/s], Decompressed: 6091
Downloaded: 6297 file(s) [attempted 6297/8546 = 73%, 143 KB/s], Decompressed: 6182
Downloaded: 6331 file(s) [attempted 6331/8546 = 74%, 321 KB/s], Decompressed: 6182
Downloaded: 6378 file(s) [attempted 6378/8546 = 74%, 160 KB/s], Decompressed: 6280
Downloaded: 6419 file(s) [attempted 6419/8546 = 75%, 107 KB/s], Decompressed: 6280
Downloaded: 6452 file(s) [attempted 6452/8546 = 75%, 867 KB/s], Decompressed: 6280
Downloaded: 6496 file(s) [attempted 6496/8546 = 76%, 85 KB/s], Decompressed: 6493
Downloaded: 6534 file(s) [attempted 6534/8546 = 76%, 130 KB/s], Decompressed: 6530
Downloaded: 6578 file(s) [attempted 6578/8546 = 76%, 43 KB/s], Decompressed: 6574
Downloaded: 6615 file(s) [attempted 6615/8546 = 77%, 335 KB/s], Decompressed: 6608
Downloaded: 6652 file(s) [attempted 6652/8546 = 77%, 347 KB/s], Decompressed: 6649
Downloaded: 6689 file(s) [attempted 6689/8546 = 78%, 853 KB/s], Decompressed: 6686
Downloaded: 6731 file(s) [attempted 6731/8546 = 78%, 162 KB/s], Decompressed: 6720
Downloaded: 6765 file(s) [attempted 6765/8546 = 79%, 375 KB/s], Decompressed: 6760
Downloaded: 6806 file(s) [attempted 6806/8546 = 79%, 200 KB/s], Decompressed: 6798
Downloaded: 6845 file(s) [attempted 6845/8546 = 80%, 108 KB/s], Decompressed: 6838
Downloaded: 6885 file(s) [attempted 6885/8546 = 80%, 490 KB/s], Decompressed: 6882
Downloaded: 6925 file(s) [attempted 6925/8546 = 81%, 315 KB/s], Decompressed: 6919
Downloaded: 6960 file(s) [attempted 6960/8546 = 81%, 151 KB/s], Decompressed: 6953
Downloaded: 7004 file(s) [attempted 7004/8546 = 81%, 197 KB/s], Decompressed: 6997
Downloaded: 7042 file(s) [attempted 7042/8546 = 82%, 53 KB/s], Decompressed: 7034
Downloaded: 7082 file(s) [attempted 7082/8546 = 82%, 485 KB/s], Decompressed: 7078
Downloaded: 7112 file(s) [attempted 7112/8546 = 83%, 72 KB/s], Decompressed: 7109
Downloaded: 7149 file(s) [attempted 7149/8546 = 83%, 277 KB/s], Decompressed: 7143
Downloaded: 7193 file(s) [attempted 7193/8546 = 84%, 73 KB/s], Decompressed: 7143
Downloaded: 7229 file(s) [attempted 7229/8546 = 84%, 254 KB/s], Decompressed: 7146
Downloaded: 7265 file(s) [attempted 7265/8546 = 85%, 289 KB/s], Decompressed: 7261
Downloaded: 7298 file(s) [attempted 7298/8546 = 85%, 298 KB/s], Decompressed: 7295
Downloaded: 7339 file(s) [attempted 7339/8546 = 85%, 117 KB/s], Decompressed: 7335
Downloaded: 7379 file(s) [attempted 7379/8546 = 86%, 1931 KB/s], Decompressed: 7373
Downloaded: 7417 file(s) [attempted 7417/8546 = 86%, 351 KB/s], Decompressed: 7373
Downloaded: 7454 file(s) [attempted 7454/8546 = 87%, 551 KB/s], Decompressed: 7376
Downloaded: 7491 file(s) [attempted 7491/8546 = 87%, 616 KB/s], Decompressed: 7488
Downloaded: 7532 file(s) [attempted 7532/8546 = 88%, 927 KB/s], Decompressed: 7528
Downloaded: 7579 file(s) [attempted 7579/8546 = 88%, 26 KB/s], Decompressed: 7532
Downloaded: 7620 file(s) [attempted 7620/8546 = 89%, 185 KB/s], Decompressed: 7535
Downloaded: 7657 file(s) [attempted 7657/8546 = 89%, 256 KB/s], Decompressed: 7535
Downloaded: 7697 file(s) [attempted 7697/8546 = 90%, 488 KB/s], Decompressed: 7535
Downloaded: 7735 file(s) [attempted 7735/8546 = 90%, 204 KB/s], Decompressed: 7731
Downloaded: 7775 file(s) [attempted 7775/8546 = 90%, 46 KB/s], Decompressed: 7772
Downloaded: 7819 file(s) [attempted 7819/8546 = 91%, 121 KB/s], Decompressed: 7816
Downloaded: 7860 file(s) [attempted 7860/8546 = 91%, 151 KB/s], Decompressed: 7853
Downloaded: 7898 file(s) [attempted 7898/8546 = 92%, 245 KB/s], Decompressed: 7890
Downloaded: 7934 file(s) [attempted 7934/8546 = 92%, 2332 KB/s], Decompressed: 7927
Downloaded: 7975 file(s) [attempted 7975/8546 = 93%, 60 KB/s], Decompressed: 7927
Downloaded: 8015 file(s) [attempted 8015/8546 = 93%, 87 KB/s], Decompressed: 7931
Downloaded: 8056 file(s) [attempted 8056/8546 = 94%, 905 KB/s], Decompressed: 7931
Downloaded: 8093 file(s) [attempted 8093/8546 = 94%, 280 KB/s], Decompressed: 7931
Downloaded: 8130 file(s) [attempted 8130/8546 = 95%, 761 KB/s], Decompressed: 8015
Downloaded: 8171 file(s) [attempted 8171/8546 = 95%, 510 KB/s], Decompressed: 8015
Downloaded: 8208 file(s) [attempted 8208/8546 = 96%, 569 KB/s], Decompressed: 8205
Downloaded: 8251 file(s) [attempted 8251/8546 = 96%, 1342 KB/s], Decompressed: 8245
Downloaded: 8293 file(s) [attempted 8293/8546 = 97%, 76 KB/s], Decompressed: 8272
Downloaded: 8330 file(s) [attempted 8330/8546 = 97%, 232 KB/s], Decompressed: 8272
Downloaded: 8364 file(s) [attempted 8364/8546 = 97%, 1079 KB/s], Decompressed: 8360
Downloaded: 8403 file(s) [attempted 8403/8546 = 98%, 52 KB/s], Decompressed: 8394
Downloaded: 8445 file(s) [attempted 8445/8546 = 98%, 1099 KB/s], Decompressed: 8442
Downloaded: 8489 file(s) [attempted 8489/8546 = 99%, 49 KB/s], Decompressed: 8482
Downloaded: 8526 file(s) [attempted 8526/8546 = 99%, 78 KB/s], Decompressed: 8520
Downloaded: 8546 file(s) [attempted 8546/8546 = 100%, 78 KB/s], Decompressed: 8543

lake build

ℹ [3629/3638] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3643/3655] Replayed PrimeNumberTheoremAnd.StrongPNT
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1559:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1608:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1725:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1870:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2265:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2355:6: declaration uses `sorry`
⚠ [3779/3805] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3894/3901] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3961/3982] 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`
⚠ [3963/3982] 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`
⚠ [3965/3982] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
⚠ [4107/4114] 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`
⚠ [4109/4147] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1017:8: declaration uses `sorry`
⚠ [4111/4147] 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`
⚠ [4113/4147] Replayed PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1519:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2185:8: declaration uses `sorry`
⚠ [4151/4165] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2634:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3685:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3699:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3713:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3725:8: declaration uses `sorry`
⚠ [4156/4165] 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`
⚠ [4160/4202] 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:737:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:749:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:761:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:773:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:785:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:797:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:809:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:821:8: declaration uses `sorry`
ℹ [4167/4202] 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.
⚠ [4169/4202] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4643:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4670:8: declaration uses `sorry`
⚠ [4200/4213] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean:116:8: declaration uses `sorry`
⚠ [4201/4213] 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`
⚠ [4226/4280] Replayed PrimeNumberTheoremAnd.IEANTN.TMEEMT
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:146:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:159:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:172:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:185:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:201:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:209:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:234:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:242:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:250:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:388:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:396:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:525:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:570:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:585:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:619:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:628:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:637:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:646:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:655:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:671:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:680:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:689:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:698:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:733:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:742:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:751:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:777:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:800:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:811:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:822:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:833:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:843:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:851:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:860:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:869:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:992:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1012:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1042:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1068:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1082:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1090:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1105:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1120:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1129:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1144:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1162:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1174:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1191:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1202:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1224:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1238:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1252:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1282:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1309:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1333:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1347:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1361:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1375:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1389:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1424:8: declaration uses `sorry`
⚠ [4241/4280] 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`
✔ [4254/4288] Built PrimeNumberTheoremAnd.IEANTN.KadiriEq12Foundations (108s)
⚠ [4257/4288] 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`
⚠ [4259/4288] Replayed PrimeNumberTheoremAnd.IEANTN.Goldbach
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
✔ [4263/4288] Built PrimeNumberTheoremAnd.LaplaceInversion (18s)
✔ [4275/4288] Built PrimeNumberTheoremAnd.SincKernelErrorBounds (2.7s)
✔ [4282/4288] Built PrimeNumberTheoremAnd.IEANTN.KadiriSupport (6.7s)
✔ [4285/4288] Built PrimeNumberTheoremAnd.IEANTN.KadiriEq13 (22s)
⚠ [4286/4288] Built PrimeNumberTheoremAnd.IEANTN.Kadiri (12s)
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:135:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:172:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:209:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:465:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:497:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1319:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1406:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1489:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2719:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2745:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:3351:8: declaration uses `sorry`
✔ [4287/4288] Built PrimeNumberTheoremAnd (26s)
Build completed successfully (4288 jobs).

warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes

git clone --depth 1 --branch main --single-branch https://github.com/AlexKontorovich/PrimeNumberTheoremAnd.git /var/lib/apodeixis/repos/job-922-source

Cloning into '/var/lib/apodeixis/repos/job-922-source'...

git checkout d963a6e694a05cd82e5f9b9ae7f4d94123e85393

Note: switching to 'd963a6e694a05cd82e5f9b9ae7f4d94123e85393'.

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 d963a6e KADIRI: shared support file and lemma de-privatization for the equation PRs (#1634)

./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset)

apx-semantic-phase	{"duration_ms":3,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":0,"diagnostic_count":0,"duration_ms":8,"module_name":"PrimeNumberTheoremAnd","module_path":"PrimeNumberTheoremAnd.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":516376,"module_count":1,"module_name":"PrimeNumberTheoremAnd","module_path":"PrimeNumberTheoremAnd.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":0,"diagnostic_count":0,"duration_ms":13,"module_count":1,"module_name":"PrimeNumberTheoremAnd","module_path":"PrimeNumberTheoremAnd.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":458,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":11,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":458,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":190,"diagnostic_count":66,"duration_ms":23707,"module_name":"PrimeNumberTheoremAnd.IEANTN.Kadiri","module_path":"PrimeNumberTheoremAnd/IEANTN/Kadiri.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":520246,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Kadiri","module_path":"PrimeNumberTheoremAnd/IEANTN/Kadiri.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":190,"diagnostic_count":66,"duration_ms":62,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Kadiri","module_path":"PrimeNumberTheoremAnd/IEANTN/Kadiri.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":2488911,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":3,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":2488911,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":25,"diagnostic_count":8,"duration_ms":2433,"module_name":"PrimeNumberTheoremAnd.IEANTN.KadiriEq12Foundations","module_path":"PrimeNumberTheoremAnd/IEANTN/KadiriEq12Foundations.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":409531,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.KadiriEq12Foundations","module_path":"PrimeNumberTheoremAnd/IEANTN/KadiriEq12Foundations.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":25,"diagnostic_count":8,"duration_ms":3,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.KadiriEq12Foundations","module_path":"PrimeNumberTheoremAnd/IEANTN/KadiriEq12Foundations.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":298120,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":298120,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":29,"diagnostic_count":14,"duration_ms":2589,"module_name":"PrimeNumberTheoremAnd.IEANTN.KadiriEq13","module_path":"PrimeNumberTheoremAnd/IEANTN/KadiriEq13.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":474235,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.KadiriEq13","module_path":"PrimeNumberTheoremAnd/IEANTN/KadiriEq13.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":29,"diagnostic_count":14,"duration_ms":3,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.KadiriEq13","module_path":"PrimeNumberTheoremAnd/IEANTN/KadiriEq13.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":283811,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":283811,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":27,"diagnostic_count":8,"duration_ms":2589,"module_name":"PrimeNumberTheoremAnd.IEANTN.KadiriSupport","module_path":"PrimeNumberTheoremAnd/IEANTN/KadiriSupport.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":423933,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.KadiriSupport","module_path":"PrimeNumberTheoremAnd/IEANTN/KadiriSupport.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":27,"diagnostic_count":8,"duration_ms":2,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.KadiriSupport","module_path":"PrimeNumberTheoremAnd/IEANTN/KadiriSupport.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":4,"module_payload_kind":"fragment","ok":true,"payload_bytes":359096,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":4,"module_payload_kind":"fragment","ok":true,"payload_bytes":359096,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":228,"diagnostic_count":131,"duration_ms":22297,"module_name":"PrimeNumberTheoremAnd.LaplaceInversion","module_path":"PrimeNumberTheoremAnd/LaplaceInversion.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":351984,"module_count":1,"module_name":"PrimeNumberTheoremAnd.LaplaceInversion","module_path":"PrimeNumberTheoremAnd/LaplaceInversion.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":228,"diagnostic_count":131,"duration_ms":10,"module_count":1,"module_name":"PrimeNumberTheoremAnd.LaplaceInversion","module_path":"PrimeNumberTheoremAnd/LaplaceInversion.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":5,"module_payload_kind":"fragment","ok":true,"payload_bytes":2223874,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":5,"module_payload_kind":"fragment","ok":true,"payload_bytes":2223874,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":10,"diagnostic_count":8,"duration_ms":828,"module_name":"PrimeNumberTheoremAnd.SincKernelErrorBounds","module_path":"PrimeNumberTheoremAnd/SincKernelErrorBounds.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":347102,"module_count":1,"module_name":"PrimeNumberTheoremAnd.SincKernelErrorBounds","module_path":"PrimeNumberTheoremAnd/SincKernelErrorBounds.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase	{"declaration_count":10,"diagnostic_count":8,"duration_ms":2,"module_count":1,"module_name":"PrimeNumberTheoremAnd.SincKernelErrorBounds","module_path":"PrimeNumberTheoremAnd/SincKernelErrorBounds.lean","ok":true,"phase":"lean_module_fragment_build"}
apx-semantic-phase	{"duration_ms":0,"module_index":6,"module_payload_kind":"fragment","ok":true,"payload_bytes":73564,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":0,"module_index":6,"module_payload_kind":"fragment","ok":true,"payload_bytes":73564,"phase":"lean_module_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":92437}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":11171,"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":178230,"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 871556dc509db5618ccf32c9b437a3a6480ea9f48e5bda520c918f4115704fc2
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":3106496,"ok":true}