Run 134

lake build :blueprint

✔ [27/35] Built Cli.Basic:c.o (9.4s)
✔ [30/35] Built Cli.Extensions:c.o (486ms)
✔ [33/42] Built Cli:c.o (89ms)
ℹ [3692/3734] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3706/3734] 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/3870] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3966/3982] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [4048/4069] 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`
⚠ [4051/4069] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
⚠ [4061/4130] 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`
⚠ [4198/4213] 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`
⚠ [4202/4217] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1017:8: declaration uses `sorry`
⚠ [4206/4217] 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`
⚠ [4212/4273] 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`
⚠ [4269/4292] 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`
⚠ [4286/4310] 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`
⚠ [4288/4310] 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/4310] 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/4310] 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/4482] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean:116:8: declaration uses `sorry`
⚠ [4351/4482] 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`
⚠ [4396/4497] 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`
⚠ [4398/4497] 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`
⚠ [4400/4497] Replayed PrimeNumberTheoremAnd.IEANTN.Goldbach
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
⚠ [4445/4497] 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`
✔ [4459/4497] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.LaplaceInversion:blueprint (9.4s)
✔ [4483/4497] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.SincKernelErrorBounds:blueprint (2.5s)
✔ [4491/4497] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.KadiriEq13:blueprint (21s)
⚠ [4492/4497] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:134:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:171:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:208:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:464:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:496:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1442:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1529:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1612:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2842:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2868:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:3474:8: declaration uses `sorry`
✔ [4493/4497] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Kadiri:blueprint (48s)
✔ [4495/4498] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (9.4s)
ℹ [4496/4498] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (60ms)
info: Blueprint indexing
Build completed successfully (4498 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-887-source

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

git checkout f71f5dd716b9a6970caa68ce1f939f92c8f77a18

Note: switching to 'f71f5dd716b9a6970caa68ce1f939f92c8f77a18'.

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 f71f5dd LaplaceInversion: +itI vertical-line continuity and a continuous exp-bounded helper (#1620)

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: 14 file(s) [attempted 14/8546 = 0%, 1 KB/s], Decompressed: 13
Downloaded: 38 file(s) [attempted 38/8546 = 0%, 34 KB/s], Decompressed: 34
Downloaded: 68 file(s) [attempted 68/8546 = 0%, 53 KB/s], Decompressed: 67
Downloaded: 102 file(s) [attempted 102/8546 = 1%, 203 KB/s], Decompressed: 68
Downloaded: 143 file(s) [attempted 143/8546 = 1%, 333 KB/s], Decompressed: 72
Downloaded: 180 file(s) [attempted 180/8546 = 2%, 647 KB/s], Decompressed: 167
Downloaded: 218 file(s) [attempted 218/8546 = 2%, 296 KB/s], Decompressed: 167
Downloaded: 248 file(s) [attempted 248/8546 = 2%, 709 KB/s], Decompressed: 174
Downloaded: 282 file(s) [attempted 282/8546 = 3%, 640 KB/s], Decompressed: 174
Downloaded: 322 file(s) [attempted 322/8546 = 3%, 667 KB/s], Decompressed: 238
Downloaded: 363 file(s) [attempted 363/8546 = 4%, 88 KB/s], Decompressed: 360
Downloaded: 406 file(s) [attempted 406/8546 = 4%, 197 KB/s], Decompressed: 383
Downloaded: 438 file(s) [attempted 438/8546 = 5%, 27 KB/s], Decompressed: 383
Downloaded: 478 file(s) [attempted 478/8546 = 5%, 773 KB/s], Decompressed: 390
Downloaded: 519 file(s) [attempted 519/8546 = 6%, 637 KB/s], Decompressed: 495
Downloaded: 559 file(s) [attempted 559/8546 = 6%, 146 KB/s], Decompressed: 495
Downloaded: 603 file(s) [attempted 603/8546 = 7%, 182 KB/s], Decompressed: 502
Downloaded: 644 file(s) [attempted 644/8546 = 7%, 283 KB/s], Decompressed: 502
Downloaded: 681 file(s) [attempted 681/8546 = 7%, 63 KB/s], Decompressed: 580
Downloaded: 720 file(s) [attempted 720/8546 = 8%, 392 KB/s], Decompressed: 715
Downloaded: 759 file(s) [attempted 759/8546 = 8%, 219 KB/s], Decompressed: 756
Downloaded: 796 file(s) [attempted 796/8546 = 9%, 66 KB/s], Decompressed: 793
Downloaded: 837 file(s) [attempted 837/8546 = 9%, 351 KB/s], Decompressed: 824
Downloaded: 869 file(s) [attempted 869/8546 = 10%, 93 KB/s], Decompressed: 864
Downloaded: 912 file(s) [attempted 912/8546 = 10%, 384 KB/s], Decompressed: 871
Downloaded: 952 file(s) [attempted 952/8546 = 11%, 173 KB/s], Decompressed: 871
Downloaded: 993 file(s) [attempted 993/8546 = 11%, 432 KB/s], Decompressed: 874
Downloaded: 1023 file(s) [attempted 1023/8546 = 11%, 194 KB/s], Decompressed: 874
Downloaded: 1061 file(s) [attempted 1061/8546 = 12%, 170 KB/s], Decompressed: 1047
Downloaded: 1094 file(s) [attempted 1094/8546 = 12%, 265 KB/s], Decompressed: 1091
Downloaded: 1138 file(s) [attempted 1138/8546 = 13%, 225 KB/s], Decompressed: 1135
Downloaded: 1180 file(s) [attempted 1180/8546 = 13%, 36 KB/s], Decompressed: 1172
Downloaded: 1216 file(s) [attempted 1216/8546 = 14%, 330 KB/s], Decompressed: 1203
Downloaded: 1250 file(s) [attempted 1250/8546 = 14%, 471 KB/s], Decompressed: 1203
Downloaded: 1291 file(s) [attempted 1291/8546 = 15%, 313 KB/s], Decompressed: 1209
Downloaded: 1335 file(s) [attempted 1335/8546 = 15%, 578 KB/s], Decompressed: 1209
Downloaded: 1375 file(s) [attempted 1375/8546 = 16%, 215 KB/s], Decompressed: 1209
Downloaded: 1412 file(s) [attempted 1412/8546 = 16%, 182 KB/s], Decompressed: 1291
Downloaded: 1446 file(s) [attempted 1446/8546 = 16%, 682 KB/s], Decompressed: 1291
Downloaded: 1490 file(s) [attempted 1490/8546 = 17%, 325 KB/s], Decompressed: 1477
Downloaded: 1529 file(s) [attempted 1529/8546 = 17%, 82 KB/s], Decompressed: 1524
Downloaded: 1571 file(s) [attempted 1571/8546 = 18%, 590 KB/s], Decompressed: 1568
Downloaded: 1614 file(s) [attempted 1614/8546 = 18%, 471 KB/s], Decompressed: 1605
Downloaded: 1649 file(s) [attempted 1649/8546 = 19%, 244 KB/s], Decompressed: 1632
Downloaded: 1686 file(s) [attempted 1686/8546 = 19%, 110 KB/s], Decompressed: 1632
Downloaded: 1730 file(s) [attempted 1730/8546 = 20%, 159 KB/s], Decompressed: 1636
Downloaded: 1769 file(s) [attempted 1769/8546 = 20%, 71 KB/s], Decompressed: 1764
Downloaded: 1806 file(s) [attempted 1806/8546 = 21%, 914 KB/s], Decompressed: 1801
Downloaded: 1845 file(s) [attempted 1845/8546 = 21%, 671 KB/s], Decompressed: 1835
Downloaded: 1879 file(s) [attempted 1879/8546 = 21%, 1674 KB/s], Decompressed: 1876
Downloaded: 1923 file(s) [attempted 1923/8546 = 22%, 74 KB/s], Decompressed: 1920
Downloaded: 1960 file(s) [attempted 1960/8546 = 22%, 40 KB/s], Decompressed: 1954
Downloaded: 1998 file(s) [attempted 1998/8546 = 23%, 121 KB/s], Decompressed: 1991
Downloaded: 2038 file(s) [attempted 2038/8546 = 23%, 1529 KB/s], Decompressed: 2031
Downloaded: 2075 file(s) [attempted 2075/8546 = 24%, 180 KB/s], Decompressed: 2031
Downloaded: 2116 file(s) [attempted 2116/8546 = 24%, 113 KB/s], Decompressed: 2031
Downloaded: 2153 file(s) [attempted 2153/8546 = 25%, 411 KB/s], Decompressed: 2038
Downloaded: 2194 file(s) [attempted 2194/8546 = 25%, 98 KB/s], Decompressed: 2038
Downloaded: 2234 file(s) [attempted 2234/8546 = 26%, 70 KB/s], Decompressed: 2119
Downloaded: 2278 file(s) [attempted 2278/8546 = 26%, 156 KB/s], Decompressed: 2119
Downloaded: 2309 file(s) [attempted 2309/8546 = 27%, 190 KB/s], Decompressed: 2119
Downloaded: 2346 file(s) [attempted 2346/8546 = 27%, 233 KB/s], Decompressed: 2119
Downloaded: 2387 file(s) [attempted 2387/8546 = 27%, 103 KB/s], Decompressed: 2119
Downloaded: 2431 file(s) [attempted 2431/8546 = 28%, 247 KB/s], Decompressed: 2207
Downloaded: 2471 file(s) [attempted 2471/8546 = 28%, 58 KB/s], Decompressed: 2207
Downloaded: 2502 file(s) [attempted 2502/8546 = 29%, 1668 KB/s], Decompressed: 2390
Downloaded: 2539 file(s) [attempted 2539/8546 = 29%, 974 KB/s], Decompressed: 2390
Downloaded: 2583 file(s) [attempted 2583/8546 = 30%, 1279 KB/s], Decompressed: 2488
Downloaded: 2627 file(s) [attempted 2627/8546 = 30%, 1048 KB/s], Decompressed: 2593
Downloaded: 2667 file(s) [attempted 2667/8546 = 31%, 190 KB/s], Decompressed: 2593
Downloaded: 2701 file(s) [attempted 2701/8546 = 31%, 215 KB/s], Decompressed: 2694
Downloaded: 2735 file(s) [attempted 2735/8546 = 32%, 136 KB/s], Decompressed: 2728
Downloaded: 2779 file(s) [attempted 2779/8546 = 32%, 101 KB/s], Decompressed: 2728
Downloaded: 2820 file(s) [attempted 2820/8546 = 32%, 155 KB/s], Decompressed: 2732
Downloaded: 2860 file(s) [attempted 2860/8546 = 33%, 86 KB/s], Decompressed: 2853
Downloaded: 2897 file(s) [attempted 2897/8546 = 33%, 89 KB/s], Decompressed: 2887
Downloaded: 2935 file(s) [attempted 2935/8546 = 34%, 622 KB/s], Decompressed: 2931
Downloaded: 2979 file(s) [attempted 2979/8546 = 34%, 609 KB/s], Decompressed: 2938
Downloaded: 3019 file(s) [attempted 3019/8546 = 35%, 446 KB/s], Decompressed: 2938
Downloaded: 3060 file(s) [attempted 3060/8546 = 35%, 110 KB/s], Decompressed: 2962
Downloaded: 3100 file(s) [attempted 3100/8546 = 36%, 204 KB/s], Decompressed: 2962
Downloaded: 3141 file(s) [attempted 3141/8546 = 36%, 140 KB/s], Decompressed: 2962
Downloaded: 3171 file(s) [attempted 3171/8546 = 37%, 37 KB/s], Decompressed: 3053
Downloaded: 3215 file(s) [attempted 3215/8546 = 37%, 225 KB/s], Decompressed: 3053
Downloaded: 3259 file(s) [attempted 3259/8546 = 38%, 995 KB/s], Decompressed: 3053
Downloaded: 3303 file(s) [attempted 3303/8546 = 38%, 154 KB/s], Decompressed: 3053
Downloaded: 3340 file(s) [attempted 3340/8546 = 39%, 84 KB/s], Decompressed: 3053
Downloaded: 3378 file(s) [attempted 3378/8546 = 39%, 365 KB/s], Decompressed: 3053
Downloaded: 3418 file(s) [attempted 3418/8546 = 39%, 52 KB/s], Decompressed: 3147
Downloaded: 3462 file(s) [attempted 3462/8546 = 40%, 67 KB/s], Decompressed: 3147
Downloaded: 3506 file(s) [attempted 3506/8546 = 41%, 155 KB/s], Decompressed: 3418
Downloaded: 3543 file(s) [attempted 3543/8546 = 41%, 99 KB/s], Decompressed: 3418
Downloaded: 3577 file(s) [attempted 3577/8546 = 41%, 114 KB/s], Decompressed: 3491
Downloaded: 3621 file(s) [attempted 3621/8546 = 42%, 33 KB/s], Decompressed: 3611
Downloaded: 3662 file(s) [attempted 3662/8546 = 42%, 586 KB/s], Decompressed: 3611
Downloaded: 3706 file(s) [attempted 3706/8546 = 43%, 334 KB/s], Decompressed: 3614
Downloaded: 3750 file(s) [attempted 3750/8546 = 43%, 259 KB/s], Decompressed: 3746
Downloaded: 3791 file(s) [attempted 3791/8546 = 44%, 71 KB/s], Decompressed: 3780
Downloaded: 3824 file(s) [attempted 3824/8546 = 44%, 615 KB/s], Decompressed: 3821
Downloaded: 3867 file(s) [attempted 3867/8546 = 45%, 429 KB/s], Decompressed: 3861
Downloaded: 3902 file(s) [attempted 3902/8546 = 45%, 1050 KB/s], Decompressed: 3899
Downloaded: 3946 file(s) [attempted 3946/8546 = 46%, 138 KB/s], Decompressed: 3916
Downloaded: 3989 file(s) [attempted 3989/8546 = 46%, 396 KB/s], Decompressed: 3916
Downloaded: 4022 file(s) [attempted 4022/8546 = 47%, 1798 KB/s], Decompressed: 3922
Downloaded: 4058 file(s) [attempted 4058/8546 = 47%, 1422 KB/s], Decompressed: 3922
Downloaded: 4091 file(s) [attempted 4091/8546 = 47%, 1087 KB/s], Decompressed: 3922
Downloaded: 4135 file(s) [attempted 4135/8546 = 48%, 774 KB/s], Decompressed: 3922
Downloaded: 4179 file(s) [attempted 4179/8546 = 48%, 968 KB/s], Decompressed: 3922
Downloaded: 4220 file(s) [attempted 4220/8546 = 49%, 290 KB/s], Decompressed: 3922
Downloaded: 4261 file(s) [attempted 4261/8546 = 49%, 268 KB/s], Decompressed: 3922
Downloaded: 4294 file(s) [attempted 4294/8546 = 50%, 47 KB/s], Decompressed: 4007
Downloaded: 4338 file(s) [attempted 4338/8546 = 50%, 113 KB/s], Decompressed: 4007
Downloaded: 4376 file(s) [attempted 4376/8546 = 51%, 218 KB/s], Decompressed: 4372
Downloaded: 4420 file(s) [attempted 4420/8546 = 51%, 839 KB/s], Decompressed: 4406
Downloaded: 4464 file(s) [attempted 4464/8546 = 52%, 833 KB/s], Decompressed: 4423
Downloaded: 4497 file(s) [attempted 4497/8546 = 52%, 153 KB/s], Decompressed: 4423
Downloaded: 4535 file(s) [attempted 4535/8546 = 53%, 239 KB/s], Decompressed: 4430
Downloaded: 4575 file(s) [attempted 4575/8546 = 53%, 963 KB/s], Decompressed: 4430
Downloaded: 4619 file(s) [attempted 4619/8546 = 54%, 510 KB/s], Decompressed: 4430
Downloaded: 4663 file(s) [attempted 4663/8546 = 54%, 890 KB/s], Decompressed: 4430
Downloaded: 4700 file(s) [attempted 4700/8546 = 54%, 54 KB/s], Decompressed: 4514
Downloaded: 4744 file(s) [attempted 4744/8546 = 55%, 34 KB/s], Decompressed: 4514
Downloaded: 4785 file(s) [attempted 4785/8546 = 55%, 278 KB/s], Decompressed: 4514
Downloaded: 4822 file(s) [attempted 4822/8546 = 56%, 116 KB/s], Decompressed: 4514
Downloaded: 4858 file(s) [attempted 4858/8546 = 56%, 159 KB/s], Decompressed: 4514
Downloaded: 4900 file(s) [attempted 4900/8546 = 57%, 319 KB/s], Decompressed: 4514
Downloaded: 4937 file(s) [attempted 4937/8546 = 57%, 93 KB/s], Decompressed: 4514
Downloaded: 4978 file(s) [attempted 4978/8546 = 58%, 70 KB/s], Decompressed: 4514
Downloaded: 5022 file(s) [attempted 5022/8546 = 58%, 161 KB/s], Decompressed: 4514
Downloaded: 5059 file(s) [attempted 5059/8546 = 59%, 381 KB/s], Decompressed: 4683
Downloaded: 5096 file(s) [attempted 5096/8546 = 59%, 58 KB/s], Decompressed: 4683
Downloaded: 5140 file(s) [attempted 5140/8546 = 60%, 97 KB/s], Decompressed: 4683
Downloaded: 5177 file(s) [attempted 5177/8546 = 60%, 311 KB/s], Decompressed: 5174
Downloaded: 5218 file(s) [attempted 5218/8546 = 61%, 954 KB/s], Decompressed: 5211
Downloaded: 5255 file(s) [attempted 5255/8546 = 61%, 26 KB/s], Decompressed: 5252
Downloaded: 5296 file(s) [attempted 5296/8546 = 61%, 49 KB/s], Decompressed: 5265
Downloaded: 5336 file(s) [attempted 5336/8546 = 62%, 296 KB/s], Decompressed: 5265
Downloaded: 5377 file(s) [attempted 5377/8546 = 62%, 1199 KB/s], Decompressed: 5370
Downloaded: 5415 file(s) [attempted 5415/8546 = 63%, 235 KB/s], Decompressed: 5407
Downloaded: 5453 file(s) [attempted 5453/8546 = 63%, 187 KB/s], Decompressed: 5448
Downloaded: 5495 file(s) [attempted 5495/8546 = 64%, 242 KB/s], Decompressed: 5478
Downloaded: 5529 file(s) [attempted 5529/8546 = 64%, 46 KB/s], Decompressed: 5478
Downloaded: 5573 file(s) [attempted 5573/8546 = 65%, 117 KB/s], Decompressed: 5478
Downloaded: 5614 file(s) [attempted 5614/8546 = 65%, 1156 KB/s], Decompressed: 5607
Downloaded: 5654 file(s) [attempted 5654/8546 = 66%, 74 KB/s], Decompressed: 5651
Downloaded: 5694 file(s) [attempted 5694/8546 = 66%, 546 KB/s], Decompressed: 5685
Downloaded: 5725 file(s) [attempted 5725/8546 = 66%, 227 KB/s], Decompressed: 5722
Downloaded: 5764 file(s) [attempted 5764/8546 = 67%, 183 KB/s], Decompressed: 5759
Downloaded: 5805 file(s) [attempted 5805/8546 = 67%, 69 KB/s], Decompressed: 5800
Downloaded: 5849 file(s) [attempted 5849/8546 = 68%, 437 KB/s], Decompressed: 5840
Downloaded: 5883 file(s) [attempted 5883/8546 = 68%, 322 KB/s], Decompressed: 5874
Downloaded: 5918 file(s) [attempted 5918/8546 = 69%, 357 KB/s], Decompressed: 5915
Downloaded: 5959 file(s) [attempted 5959/8546 = 69%, 812 KB/s], Decompressed: 5955
Downloaded: 6003 file(s) [attempted 6003/8546 = 70%, 1006 KB/s], Decompressed: 5966
Downloaded: 6044 file(s) [attempted 6044/8546 = 70%, 209 KB/s], Decompressed: 6037
Downloaded: 6084 file(s) [attempted 6084/8546 = 71%, 50 KB/s], Decompressed: 6081
Downloaded: 6119 file(s) [attempted 6119/8546 = 71%, 37 KB/s], Decompressed: 6098
Downloaded: 6158 file(s) [attempted 6158/8546 = 72%, 1936 KB/s], Decompressed: 6098
Downloaded: 6199 file(s) [attempted 6199/8546 = 72%, 142 KB/s], Decompressed: 6185
Downloaded: 6236 file(s) [attempted 6236/8546 = 72%, 61 KB/s], Decompressed: 6229
Downloaded: 6277 file(s) [attempted 6277/8546 = 73%, 160 KB/s], Decompressed: 6255
Downloaded: 6311 file(s) [attempted 6311/8546 = 73%, 191 KB/s], Decompressed: 6255
Downloaded: 6351 file(s) [attempted 6351/8546 = 74%, 194 KB/s], Decompressed: 6260
Downloaded: 6388 file(s) [attempted 6388/8546 = 74%, 446 KB/s], Decompressed: 6382
Downloaded: 6429 file(s) [attempted 6429/8546 = 75%, 1393 KB/s], Decompressed: 6405
Downloaded: 6473 file(s) [attempted 6473/8546 = 75%, 348 KB/s], Decompressed: 6405
Downloaded: 6514 file(s) [attempted 6514/8546 = 76%, 90 KB/s], Decompressed: 6415
Downloaded: 6551 file(s) [attempted 6551/8546 = 76%, 169 KB/s], Decompressed: 6547
Downloaded: 6591 file(s) [attempted 6591/8546 = 77%, 1009 KB/s], Decompressed: 6581
Downloaded: 6629 file(s) [attempted 6629/8546 = 77%, 266 KB/s], Decompressed: 6585
Downloaded: 6673 file(s) [attempted 6673/8546 = 78%, 98 KB/s], Decompressed: 6585
Downloaded: 6713 file(s) [attempted 6713/8546 = 78%, 32 KB/s], Decompressed: 6585
Downloaded: 6750 file(s) [attempted 6750/8546 = 78%, 57 KB/s], Decompressed: 6740
Downloaded: 6788 file(s) [attempted 6788/8546 = 79%, 517 KB/s], Decompressed: 6781
Downloaded: 6829 file(s) [attempted 6829/8546 = 79%, 494 KB/s], Decompressed: 6825
Downloaded: 6871 file(s) [attempted 6871/8546 = 80%, 92 KB/s], Decompressed: 6862
Downloaded: 6906 file(s) [attempted 6906/8546 = 80%, 316 KB/s], Decompressed: 6892
Downloaded: 6937 file(s) [attempted 6937/8546 = 81%, 148 KB/s], Decompressed: 6933
Downloaded: 6980 file(s) [attempted 6980/8546 = 81%, 958 KB/s], Decompressed: 6977
Downloaded: 7028 file(s) [attempted 7028/8546 = 82%, 289 KB/s], Decompressed: 7024
Downloaded: 7078 file(s) [attempted 7078/8546 = 82%, 159 KB/s], Decompressed: 7048
Downloaded: 7126 file(s) [attempted 7126/8546 = 83%, 305 KB/s], Decompressed: 7048
Downloaded: 7166 file(s) [attempted 7166/8546 = 83%, 955 KB/s], Decompressed: 7048
Downloaded: 7204 file(s) [attempted 7204/8546 = 84%, 1256 KB/s], Decompressed: 7048
Downloaded: 7240 file(s) [attempted 7240/8546 = 84%, 86 KB/s], Decompressed: 7217
Downloaded: 7275 file(s) [attempted 7275/8546 = 85%, 209 KB/s], Decompressed: 7271
Downloaded: 7319 file(s) [attempted 7319/8546 = 85%, 117 KB/s], Decompressed: 7315
Downloaded: 7359 file(s) [attempted 7359/8546 = 86%, 937 KB/s], Decompressed: 7342
Downloaded: 7400 file(s) [attempted 7400/8546 = 86%, 672 KB/s], Decompressed: 7393
Downloaded: 7434 file(s) [attempted 7434/8546 = 86%, 68 KB/s], Decompressed: 7427
Downloaded: 7474 file(s) [attempted 7474/8546 = 87%, 261 KB/s], Decompressed: 7471
Downloaded: 7520 file(s) [attempted 7520/8546 = 87%, 123 KB/s], Decompressed: 7515
Downloaded: 7559 file(s) [attempted 7559/8546 = 88%, 587 KB/s], Decompressed: 7515
Downloaded: 7593 file(s) [attempted 7593/8546 = 88%, 219 KB/s], Decompressed: 7518
Downloaded: 7633 file(s) [attempted 7633/8546 = 89%, 723 KB/s], Decompressed: 7626
Downloaded: 7674 file(s) [attempted 7674/8546 = 89%, 145 KB/s], Decompressed: 7670
Downloaded: 7714 file(s) [attempted 7714/8546 = 90%, 150 KB/s], Decompressed: 7708
Downloaded: 7752 file(s) [attempted 7752/8546 = 90%, 184 KB/s], Decompressed: 7748
Downloaded: 7792 file(s) [attempted 7792/8546 = 91%, 82 KB/s], Decompressed: 7765
Downloaded: 7833 file(s) [attempted 7833/8546 = 91%, 224 KB/s], Decompressed: 7765
Downloaded: 7873 file(s) [attempted 7873/8546 = 92%, 865 KB/s], Decompressed: 7772
Downloaded: 7914 file(s) [attempted 7914/8546 = 92%, 135 KB/s], Decompressed: 7772
Downloaded: 7951 file(s) [attempted 7951/8546 = 93%, 677 KB/s], Decompressed: 7846
Downloaded: 7995 file(s) [attempted 7995/8546 = 93%, 56 KB/s], Decompressed: 7846
Downloaded: 8039 file(s) [attempted 8039/8546 = 94%, 108 KB/s], Decompressed: 7941
Downloaded: 8073 file(s) [attempted 8073/8546 = 94%, 228 KB/s], Decompressed: 8026
Downloaded: 8114 file(s) [attempted 8114/8546 = 94%, 896 KB/s], Decompressed: 8026
Downloaded: 8153 file(s) [attempted 8153/8546 = 95%, 835 KB/s], Decompressed: 8147
Downloaded: 8195 file(s) [attempted 8195/8546 = 95%, 287 KB/s], Decompressed: 8174
Downloaded: 8232 file(s) [attempted 8232/8546 = 96%, 772 KB/s], Decompressed: 8174
Downloaded: 8273 file(s) [attempted 8273/8546 = 96%, 1251 KB/s], Decompressed: 8181
Downloaded: 8313 file(s) [attempted 8313/8546 = 97%, 501 KB/s], Decompressed: 8306
Downloaded: 8350 file(s) [attempted 8350/8546 = 97%, 132 KB/s], Decompressed: 8347
Downloaded: 8393 file(s) [attempted 8393/8546 = 98%, 64 KB/s], Decompressed: 8384
Downloaded: 8428 file(s) [attempted 8428/8546 = 98%, 96 KB/s], Decompressed: 8427
Downloaded: 8472 file(s) [attempted 8472/8546 = 99%, 794 KB/s], Decompressed: 8469
Downloaded: 8516 file(s) [attempted 8516/8546 = 99%, 144 KB/s], Decompressed: 8509
Downloaded: 8543 file(s) [attempted 8543/8546 = 99%, 116 KB/s], Decompressed: 8536
Downloaded: 8546 file(s) [attempted 8546/8546 = 100%, 116 KB/s], Decompressed: 8536

lake build

ℹ [3626/3636] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3647/3656] 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`
⚠ [3778/3805] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3893/3900] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3959/3977] 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`
⚠ [3962/3977] 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/3977] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
⚠ [4108/4150] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1017:8: declaration uses `sorry`
⚠ [4110/4150] 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/4150] 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/4150] 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`
⚠ [4152/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`
⚠ [4157/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/4210] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean:116:8: declaration uses `sorry`
⚠ [4201/4210] 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`
⚠ [4238/4277] 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`
⚠ [4243/4277] 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`
⚠ [4252/4284] 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`
⚠ [4255/4286] Replayed PrimeNumberTheoremAnd.IEANTN.Goldbach
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
✔ [4262/4286] Built PrimeNumberTheoremAnd.LaplaceInversion (172s)
✔ [4273/4286] Built PrimeNumberTheoremAnd.SincKernelErrorBounds (2.7s)
✔ [4283/4286] Built PrimeNumberTheoremAnd.IEANTN.KadiriEq13 (87s)
⚠ [4284/4286] Built PrimeNumberTheoremAnd.IEANTN.Kadiri (13s)
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:134:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:171:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:208:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:464:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:496:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1442:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1529:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1612:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2842:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2868:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:3474:8: declaration uses `sorry`
✔ [4285/4286] Built PrimeNumberTheoremAnd (51s)
Build completed successfully (4286 jobs).

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-stable-superset)

apx-semantic-phase	{"duration_ms":5,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase	{"declaration_count":0,"diagnostic_count":0,"duration_ms":9,"module_name":"PrimeNumberTheoremAnd","module_path":"PrimeNumberTheoremAnd.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":524210,"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":3,"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":3,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":458,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":194,"diagnostic_count":66,"duration_ms":25602,"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":469368,"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":194,"diagnostic_count":66,"duration_ms":37,"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":2556808,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":4,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":2556808,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":29,"diagnostic_count":14,"duration_ms":2393,"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":502371,"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":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":284495,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":284495,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":228,"diagnostic_count":131,"duration_ms":21333,"module_name":"PrimeNumberTheoremAnd.LaplaceInversion","module_path":"PrimeNumberTheoremAnd/LaplaceInversion.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":333501,"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":24,"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":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":2223936,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":2,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":2223936,"phase":"lean_module_json_write"}
apx-semantic-phase	{"declaration_count":10,"diagnostic_count":8,"duration_ms":698,"module_name":"PrimeNumberTheoremAnd.SincKernelErrorBounds","module_path":"PrimeNumberTheoremAnd/SincKernelErrorBounds.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase	{"duration_ms":344023,"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":4,"module_payload_kind":"fragment","ok":true,"payload_bytes":73564,"phase":"lean_module_json_serialize"}
apx-semantic-phase	{"duration_ms":1,"module_index":4,"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":8287}
apx-semantic-phase	{"phase":"runner_cache_key","duration_ms":19471,"runner_cache_enabled":true}
apx-semantic-phase	{"phase":"runner_cache_lookup","duration_ms":28,"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":40747,"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 8c5ad81c565950dc70698114c0707157b8ca6834ee1b0fa1802b4015d0d152dc
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":2233987,"ok":true}