Verification run
Run 143
succeeded commit
cf906c1f1472 toolchain lean-v4-30-0 prover lean took 9h 10m · finished 1w ago
Package inputs
This verification run did not include a theorem package lock. Its inputs depend only on repository, toolchain, image, and command inputs.
Trust verification
Recomputes trust checks from the recorded attestations, manifest, and command history.
(verification not run)
Manifest
Loads the published files manifest and location metadata for this job.
(manifest not loaded)
Verifier log excerpt
les.Table4ExtData_02:blueprint (3.1s)
✔ [4244/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_03:blueprint (3.0s)
✔ [4245/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_04:blueprint (3.1s)
✔ [4246/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_05:blueprint (3.0s)
✔ [4247/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_06:blueprint (3.0s)
✔ [4248/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_07:blueprint (3.0s)
✔ [4249/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_08:blueprint (3.1s)
✔ [4250/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_09:blueprint (3.0s)
✔ [4251/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_10:blueprint (3.0s)
✔ [4252/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_11:blueprint (3.1s)
✔ [4253/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_12:blueprint (3.0s)
✔ [4254/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_13:blueprint (3.0s)
⚠ [4255/4262] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean:116:8: declaration uses `sorry`
✔ [4257/4264] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext:blueprint (3.0s)
⚠ [4258/4264] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:19:72: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.
Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:109:37: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.
Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:122:60: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.
Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
✔ [4261/4321] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor:blueprint (5.1s)
⚠ [4273/4321] Replayed PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting
warning: PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:2045:6: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.
Note: This linter can be disabled with `set_option linter.style.show false`
✔ [4283/4385] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower:blueprint (3.1s)
⚠ [4284/4385] Replayed PrimeNumberTheoremAnd.IEANTN.TMEEMT
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:93:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:104:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:117:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:146:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:154:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:179:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:187:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:195:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:333:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:341:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:470:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:515:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:530:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:564:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:573:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:582:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:591:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:600:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:616:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:625:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:634:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:643:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:678:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:687:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:696:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:722:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:745:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:756:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:767:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:778:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:788:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:796:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:805:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:814:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:937:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:957:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:987:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1013:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1027:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1035:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1050:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1065:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1074:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1089:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1107:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1119:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1136:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1147:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1169:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1183:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1197:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1227:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1243:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1254:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1278:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1292:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1306:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1320:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1334:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1369:8: declaration uses `sorry`
✔ [4301/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.TMEEMT:blueprint (46s)
⚠ [4302/4395] Replayed PrimeNumberTheoremAnd.IEANTN.SecondarySummary
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:61:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:204:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:214:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:228:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:243:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:256:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:338:8: declaration uses `sorry`
ℹ [4328/4395] Replayed PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations
info: PrimeNumberTheoremAnd/IEANTN/Ramanujan/RamanujanCalculations.lean:76:4: Try this:
[apply] ring_nf
The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
⚠ [4329/4395] Replayed PrimeNumberTheoremAnd.IwaniecKowalskiCh1
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:74:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:91:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:638:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:680:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:718:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:986:3: error: doc-strings should start with a single space or newline
Note: This linter can be disabled with `set_option linter.style.docString false`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1259:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1429:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1444:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1456:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1474:6: declaration uses `sorry`
✔ [4331/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondarySummary:blueprint (7.1s)
⚠ [4332/4395] Replayed PrimeNumberTheoremAnd.IEANTN.Goldbach
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
✔ [4354/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.MobiusLemma:blueprint (10s)
✔ [4356/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Goldbach:blueprint (6.0s)
✔ [4384/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.LaplaceInversion:blueprint (2.5s)
✔ [4385/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Lcm:blueprint (11s)
✔ [4386/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimarySummary:blueprint (2.0s)
✔ [4387/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan:blueprint (15s)
⚠ [4390/4395] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:132:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:169:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:206:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:277:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:325:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:357:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1277:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1320:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1407:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1490:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2720:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2746:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:3352:8: declaration uses `sorry`
✔ [4391/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Kadiri:blueprint (45s)
✔ [4393/4396] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (6.3s)
ℹ [4394/4396] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (62ms)
info: Blueprint indexing
Build completed successfully (4396 jobs).
stderr:
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-a)
exit_code=Some(0) duration_ms=980541
stdout:
apx-semantic-phase {"duration_ms":25,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":335,"diagnostic_count":221,"duration_ms":28220,"module_name":"PrimeNumberTheoremAnd.IEANTN.Mertens","module_path":"PrimeNumberTheoremAnd/IEANTN/Mertens.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":409014,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Mertens","module_path":"PrimeNumberTheoremAnd/IEANTN/Mertens.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":335,"diagnostic_count":221,"duration_ms":16,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Mertens","module_path":"PrimeNumberTheoremAnd/IEANTN/Mertens.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":1810171,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":2,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":1810171,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":471,"diagnostic_count":322,"duration_ms":49147,"module_name":"PrimeNumberTheoremAnd.IEANTN.ZetaAppendix","module_path":"PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":418447,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.ZetaAppendix","module_path":"PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":471,"diagnostic_count":322,"duration_ms":51,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.ZetaAppendix","module_path":"PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.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":4207991,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":3,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":4207991,"phase":"lean_module_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":9368,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 3a1e46b855f343f1a287a5e3c974890a49a25b796fc831e00246b64839dbcef5
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":49,"runner_cache_hit":true}
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":970349,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-b)
exit_code=Some(0) duration_ms=1781094
stdout:
apx-semantic-phase {"duration_ms":22,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":136,"diagnostic_count":71,"duration_ms":10882,"module_name":"PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky","module_path":"PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":442269,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky","module_path":"PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":136,"diagnostic_count":71,"duration_ms":6,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky","module_path":"PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.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":509774,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":1,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":509774,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":0,"diagnostic_count":0,"duration_ms":5,"module_name":"PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions","module_path":"PrimeNumberTheoremAnd/IEANTN/PrimaryDefinitions.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":424223,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions","module_path":"PrimeNumberTheoremAnd/IEANTN/PrimaryDefinitions.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":0,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions","module_path":"PrimeNumberTheoremAnd/IEANTN/PrimaryDefinitions.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":510,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":510,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":36,"diagnostic_count":27,"duration_ms":2873,"module_name":"PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions","module_path":"PrimeNumberTheoremAnd/IEANTN/SecondaryDefinitions.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":431701,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions","module_path":"PrimeNumberTheoremAnd/IEANTN/SecondaryDefinitions.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":36,"diagnostic_count":27,"duration_ms":3,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions","module_path":"PrimeNumberTheoremAnd/IEANTN/SecondaryDefinitions.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":189395,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":1,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":189395,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":6,"diagnostic_count":0,"duration_ms":495,"module_name":"PrimeNumberTheoremAnd.IEANTN.ZetaSummary","module_path":"PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":423643,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.ZetaSummary","module_path":"PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":6,"diagnostic_count":0,"duration_ms":1,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.ZetaSummary","module_path":"PrimeNumberTheoremAnd/IEANTN/ZetaSummary.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":11072,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":11072,"phase":"lean_module_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":21}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":11107,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 3a1e46b855f343f1a287a5e3c974890a49a25b796fc831e00246b64839dbcef5
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":55,"runner_cache_hit":true}
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":1769311,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r2)
exit_code=Some(0) duration_ms=1748020
stdout:
apx-semantic-phase {"duration_ms":25,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":57,"diagnostic_count":33,"duration_ms":4185,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtCore","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtCore.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":436484,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtCore","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtCore.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":57,"diagnostic_count":33,"duration_ms":3,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtCore","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtCore.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":166420,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":166420,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":69,"diagnostic_count":54,"duration_ms":4916,"module_name":"PrimeNumberTheoremAnd.IEANTN.MobiusLemma","module_path":"PrimeNumberTheoremAnd/IEANTN/MobiusLemma.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":409491,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.MobiusLemma","module_path":"PrimeNumberTheoremAnd/IEANTN/MobiusLemma.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":69,"diagnostic_count":54,"duration_ms":3,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.MobiusLemma","module_path":"PrimeNumberTheoremAnd/IEANTN/MobiusLemma.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":430031,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":1,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":430031,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":17,"diagnostic_count":10,"duration_ms":1145,"module_name":"PrimeNumberTheoremAnd.IEANTN.PrimeInInterval","module_path":"PrimeNumberTheoremAnd/IEANTN/PrimeInInterval.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":416142,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.PrimeInInterval","module_path":"PrimeNumberTheoremAnd/IEANTN/PrimeInInterval.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":17,"diagnostic_count":10,"duration_ms":2,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.PrimeInInterval","module_path":"PrimeNumberTheoremAnd/IEANTN/PrimeInInterval.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":101503,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":101503,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":297,"diagnostic_count":259,"duration_ms":22840,"module_name":"PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime","module_path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":426393,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime","module_path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":297,"diagnostic_count":259,"duration_ms":15,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime","module_path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.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":1556361,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":1,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":1556361,"phase":"lean_module_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":24}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":11073,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 3a1e46b855f343f1a287a5e3c974890a49a25b796fc831e00246b64839dbcef5
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":50,"runner_cache_hit":true}
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":1736113,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r3)
exit_code=Some(0) duration_ms=1836206
stdout:
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":428,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_00","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_00.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":451594,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_00","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_00.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":1,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_00","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_00.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":74842,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":74842,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":659,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_01","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_01.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":450152,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_01","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_01.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_01","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_01.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":77992,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":77992,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":391,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_02","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_02.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":441638,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_02","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_02.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_02","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_02.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":80054,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":80054,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":380,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_13","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_13.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":434622,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_13","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_13.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_13","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_13.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":68407,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":68407,"phase":"lean_module_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":24}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":15172,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 3a1e46b855f343f1a287a5e3c974890a49a25b796fc831e00246b64839dbcef5
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":21,"runner_cache_hit":true}
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":1819931,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r4)
exit_code=Some(0) duration_ms=1842855
stdout:
apx-semantic-phase {"duration_ms":4,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":459,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_03","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_03.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":445195,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_03","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_03.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_03","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_03.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":82759,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":82759,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":427,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_04","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_04.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":439148,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_04","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_04.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_04","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_04.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":85603,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":85603,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":429,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_05","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_05.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":435334,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_05","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_05.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_05","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_05.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":87967,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":87967,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":365,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_06","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_06.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":436040,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_06","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_06.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_06","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_06.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":90257,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":90257,"phase":"lean_module_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":24}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":21035,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 3a1e46b855f343f1a287a5e3c974890a49a25b796fc831e00246b64839dbcef5
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":262,"runner_cache_hit":true}
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":1820561,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r5)
exit_code=Some(0) duration_ms=1756905
stdout:
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":441,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_07","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_07.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":431454,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_07","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_07.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_07","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_07.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":92539,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":92539,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":419,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_08","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_08.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":434196,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_08","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_08.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":1,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_08","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_08.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":94376,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":1,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":94376,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":477,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_09","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_09.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":437716,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_09","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_09.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":1,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_09","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_09.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":96327,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":1,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":96327,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":492,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_10","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_10.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":431964,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_10","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_10.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":1,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_10","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_10.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":101240,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":101240,"phase":"lean_module_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":24}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":14235,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 3a1e46b855f343f1a287a5e3c974890a49a25b796fc831e00246b64839dbcef5
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":33,"runner_cache_hit":true}
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":1741818,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r6)
exit_code=Some(0) duration_ms=1778088
stdout:
apx-semantic-phase {"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":150,"diagnostic_count":101,"duration_ms":12023,"module_name":"PrimeNumberTheoremAnd.IEANTN.Dusart","module_path":"PrimeNumberTheoremAnd/IEANTN/Dusart.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":437106,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Dusart","module_path":"PrimeNumberTheoremAnd/IEANTN/Dusart.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":150,"diagnostic_count":101,"duration_ms":15,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Dusart","module_path":"PrimeNumberTheoremAnd/IEANTN/Dusart.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":849814,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":1,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":849814,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":468,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_11","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_11.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":439099,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_11","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_11.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_11","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_11.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":102723,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":1,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":102723,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":448,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_12","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_12.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":438396,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_12","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_12.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_12","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_12.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":107456,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":1,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":107456,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":0,"diagnostic_count":0,"duration_ms":5,"module_name":"PrimeNumberTheoremAnd.IEANTN.PrimarySummary","module_path":"PrimeNumberTheoremAnd/IEANTN/PrimarySummary.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":433530,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.PrimarySummary","module_path":"PrimeNumberTheoremAnd/IEANTN/PrimarySummary.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":0,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.PrimarySummary","module_path":"PrimeNumberTheoremAnd/IEANTN/PrimarySummary.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":502,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":1,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":502,"phase":"lean_module_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":22}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":11575,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 3a1e46b855f343f1a287a5e3c974890a49a25b796fc831e00246b64839dbcef5
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":38,"runner_cache_hit":true}
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":1765904,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r7)
exit_code=Some(0) duration_ms=976276
stdout:
apx-semantic-phase {"duration_ms":2,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":679,"diagnostic_count":493,"duration_ms":67936,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":442561,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":679,"diagnostic_count":493,"duration_ms":44,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2.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":3913891,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":3,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":3913891,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":41,"diagnostic_count":6,"duration_ms":2718,"module_name":"PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower","module_path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":441701,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower","module_path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":41,"diagnostic_count":6,"duration_ms":1,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower","module_path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.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":344830,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":1,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":344830,"phase":"lean_module_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":18}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":10316,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 3a1e46b855f343f1a287a5e3c974890a49a25b796fc831e00246b64839dbcef5
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":39,"runner_cache_hit":true}
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":965297,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r8)
exit_code=Some(0) duration_ms=892724
stdout:
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":32,"diagnostic_count":19,"duration_ms":2118,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":428644,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":32,"diagnostic_count":19,"duration_ms":2,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.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":94339,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":1,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":94339,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":258,"diagnostic_count":135,"duration_ms":21337,"module_name":"PrimeNumberTheoremAnd.IEANTN.TMEEMT","module_path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":425502,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.TMEEMT","module_path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":258,"diagnostic_count":135,"duration_ms":15,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.TMEEMT","module_path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.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":1269379,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":1,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":1269379,"phase":"lean_module_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":22}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":9745,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 3a1e46b855f343f1a287a5e3c974890a49a25b796fc831e00246b64839dbcef5
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":49,"runner_cache_hit":true}
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":882407,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r9)
exit_code=Some(0) duration_ms=457229
stdout:
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":27,"diagnostic_count":9,"duration_ms":1850,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":439429,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":27,"diagnostic_count":9,"duration_ms":1,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.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":169753,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":1,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":169753,"phase":"lean_module_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":10520,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 3a1e46b855f343f1a287a5e3c974890a49a25b796fc831e00246b64839dbcef5
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":42,"runner_cache_hit":true}
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":446066,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r10)
exit_code=Some(0) duration_ms=451858
stdout:
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":67,"diagnostic_count":53,"duration_ms":4979,"module_name":"PrimeNumberTheoremAnd.IEANTN.SecondarySummary","module_path":"PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":430307,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.SecondarySummary","module_path":"PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":67,"diagnostic_count":53,"duration_ms":4,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.SecondarySummary","module_path":"PrimeNumberTheoremAnd/IEANTN/SecondarySummary.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":257157,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":257157,"phase":"lean_module_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":10956,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 3a1e46b855f343f1a287a5e3c974890a49a25b796fc831e00246b64839dbcef5
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":54,"runner_cache_hit":true}
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":440222,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r11)
exit_code=Some(0) duration_ms=473117
stdout:
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":70,"diagnostic_count":54,"duration_ms":5499,"module_name":"PrimeNumberTheoremAnd.IEANTN.Goldbach","module_path":"PrimeNumberTheoremAnd/IEANTN/Goldbach.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":451837,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Goldbach","module_path":"PrimeNumberTheoremAnd/IEANTN/Goldbach.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":70,"diagnostic_count":54,"duration_ms":7,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Goldbach","module_path":"PrimeNumberTheoremAnd/IEANTN/Goldbach.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":396745,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":1,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":396745,"phase":"lean_module_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":24}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":10464,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 3a1e46b855f343f1a287a5e3c974890a49a25b796fc831e00246b64839dbcef5
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":36,"runner_cache_hit":true}
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":462020,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r12)
exit_code=Some(0) duration_ms=477011
stdout:
apx-semantic-phase {"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":235,"diagnostic_count":164,"duration_ms":19064,"module_name":"PrimeNumberTheoremAnd.IEANTN.Lcm","module_path":"PrimeNumberTheoremAnd/IEANTN/Lcm.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":441800,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Lcm","module_path":"PrimeNumberTheoremAnd/IEANTN/Lcm.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":235,"diagnostic_count":164,"duration_ms":11,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Lcm","module_path":"PrimeNumberTheoremAnd/IEANTN/Lcm.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":1491369,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":1,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":1491369,"phase":"lean_module_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":24}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":10763,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 3a1e46b855f343f1a287a5e3c974890a49a25b796fc831e00246b64839dbcef5
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":38,"runner_cache_hit":true}
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":465586,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r13)
exit_code=Some(0) duration_ms=499176
stdout:
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":263,"diagnostic_count":178,"duration_ms":23212,"module_name":"PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan","module_path":"PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":451787,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan","module_path":"PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":263,"diagnostic_count":178,"duration_ms":12,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan","module_path":"PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.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":1806664,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":1,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":1806664,"phase":"lean_module_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":11151,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 3a1e46b855f343f1a287a5e3c974890a49a25b796fc831e00246b64839dbcef5
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":39,"runner_cache_hit":true}
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":487343,"ok":true}
Stored Lean workspace build cache
Stored Lean semantic extraction cache
Command runs
git_clone exit 0
git clone --depth 1 --branch main --single-branch https://github.com/AlexKontorovich/PrimeNumberTheoremAnd.git /var/lib/apodeixis/repos/job-984-source
Cloning into '/var/lib/apodeixis/repos/job-984-source'...
git_checkout exit 128
git checkout cf906c1f147216e2bc402cee5fcf05aeaf3fde8d
fatal: reference is not a tree: cf906c1f147216e2bc402cee5fcf05aeaf3fde8d
git_checkout exit 0
git fetch --depth 1 origin cf906c1f147216e2bc402cee5fcf05aeaf3fde8d
From https://github.com/AlexKontorovich/PrimeNumberTheoremAnd * branch cf906c1f147216e2bc402cee5fcf05aeaf3fde8d -> FETCH_HEAD
git_checkout exit 0
git checkout cf906c1f147216e2bc402cee5fcf05aeaf3fde8d (after fetch)
Note: switching to 'cf906c1f147216e2bc402cee5fcf05aeaf3fde8d'. 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 cf906c1 feat(Mertens): prove mul_integ_log_log_eq (#1584) (#1593)
lake_cache exit 0
lake exe cache get
Current branch: HEAD Using cache (Azure) from origin: (some leanprover-community/mathlib4) Attempting to download 8459 file(s) from leanprover-community/mathlib4 cache Decompressed 8459 file(s) Already decompressed 8459 file(s)
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes Downloaded: 1 file(s) [attempted 1/8459 = 0%, 10 KB/s], Decompressed: 0 Downloaded: 14 file(s) [attempted 14/8459 = 0%, 5 KB/s], Decompressed: 13 Downloaded: 37 file(s) [attempted 37/8459 = 0%, 17 KB/s], Decompressed: 33 Downloaded: 61 file(s) [attempted 61/8459 = 0%, 283 KB/s], Decompressed: 58 Downloaded: 83 file(s) [attempted 83/8459 = 0%, 151 KB/s], Decompressed: 79 Downloaded: 117 file(s) [attempted 117/8459 = 1%, 72 KB/s], Decompressed: 114 Downloaded: 148 file(s) [attempted 148/8459 = 1%, 125 KB/s], Decompressed: 145 Downloaded: 186 file(s) [attempted 186/8459 = 2%, 45 KB/s], Decompressed: 182 Downloaded: 216 file(s) [attempted 216/8459 = 2%, 288 KB/s], Decompressed: 213 Downloaded: 247 file(s) [attempted 247/8459 = 2%, 118 KB/s], Decompressed: 240 Downloaded: 282 file(s) [attempted 282/8459 = 3%, 109 KB/s], Decompressed: 278 Downloaded: 323 file(s) [attempted 323/8459 = 3%, 98 KB/s], Decompressed: 319 Downloaded: 360 file(s) [attempted 360/8459 = 4%, 162 KB/s], Decompressed: 357 Downloaded: 396 file(s) [attempted 396/8459 = 4%, 242 KB/s], Decompressed: 391 Downloaded: 431 file(s) [attempted 431/8459 = 5%, 28 KB/s], Decompressed: 422 Downloaded: 463 file(s) [attempted 463/8459 = 5%, 843 KB/s], Decompressed: 460 Downloaded: 504 file(s) [attempted 504/8459 = 5%, 773 KB/s], Decompressed: 501 Downloaded: 545 file(s) [attempted 545/8459 = 6%, 62 KB/s], Decompressed: 538 Downloaded: 586 file(s) [attempted 586/8459 = 6%, 74 KB/s], Decompressed: 580 Downloaded: 624 file(s) [attempted 624/8459 = 7%, 77 KB/s], Decompressed: 617 Downloaded: 658 file(s) [attempted 658/8459 = 7%, 49 KB/s], Decompressed: 651 Downloaded: 699 file(s) [attempted 699/8459 = 8%, 65 KB/s], Decompressed: 696 Downloaded: 737 file(s) [attempted 737/8459 = 8%, 77 KB/s], Decompressed: 734 Downloaded: 778 file(s) [attempted 778/8459 = 9%, 394 KB/s], Decompressed: 771 Downloaded: 816 file(s) [attempted 816/8459 = 9%, 86 KB/s], Decompressed: 809 Downloaded: 850 file(s) [attempted 850/8459 = 10%, 92 KB/s], Decompressed: 847 Downloaded: 892 file(s) [attempted 892/8459 = 10%, 83 KB/s], Decompressed: 884 Downloaded: 932 file(s) [attempted 932/8459 = 11%, 115 KB/s], Decompressed: 929 Downloaded: 973 file(s) [attempted 973/8459 = 11%, 82 KB/s], Decompressed: 960 Downloaded: 1010 file(s) [attempted 1010/8459 = 11%, 129 KB/s], Decompressed: 1004 Downloaded: 1049 file(s) [attempted 1049/8459 = 12%, 181 KB/s], Decompressed: 1047 Downloaded: 1086 file(s) [attempted 1086/8459 = 12%, 657 KB/s], Decompressed: 1076 Downloaded: 1127 file(s) [attempted 1127/8459 = 13%, 473 KB/s], Decompressed: 1121 Downloaded: 1166 file(s) [attempted 1166/8459 = 13%, 50 KB/s], Decompressed: 1162 Downloaded: 1206 file(s) [attempted 1206/8459 = 14%, 968 KB/s], Decompressed: 1203 Downloaded: 1251 file(s) [attempted 1251/8459 = 14%, 560 KB/s], Decompressed: 1240 Downloaded: 1283 file(s) [attempted 1283/8459 = 15%, 140 KB/s], Decompressed: 1275 Downloaded: 1323 file(s) [attempted 1323/8459 = 15%, 1039 KB/s], Decompressed: 1319 Downloaded: 1360 file(s) [attempted 1360/8459 = 16%, 211 KB/s], Decompressed: 1353 Downloaded: 1398 file(s) [attempted 1398/8459 = 16%, 89 KB/s], Decompressed: 1391 Downloaded: 1442 file(s) [attempted 1442/8459 = 17%, 53 KB/s], Decompressed: 1439 Downloaded: 1477 file(s) [attempted 1477/8459 = 17%, 1405 KB/s], Decompressed: 1470 Downloaded: 1518 file(s) [attempted 1518/8459 = 17%, 82 KB/s], Decompressed: 1507 Downloaded: 1554 file(s) [attempted 1554/8459 = 18%, 105 KB/s], Decompressed: 1545 Downloaded: 1593 file(s) [attempted 1593/8459 = 18%, 132 KB/s], Decompressed: 1589 Downloaded: 1631 file(s) [attempted 1631/8459 = 19%, 158 KB/s], Decompressed: 1624 Downloaded: 1672 file(s) [attempted 1672/8459 = 19%, 113 KB/s], Decompressed: 1665 Downloaded: 1712 file(s) [attempted 1712/8459 = 20%, 871 KB/s], Decompressed: 1703 Downloaded: 1743 file(s) [attempted 1743/8459 = 20%, 85 KB/s], Decompressed: 1740 Downloaded: 1785 file(s) [attempted 1785/8459 = 21%, 247 KB/s], Decompressed: 1781 Downloaded: 1822 file(s) [attempted 1822/8459 = 21%, 461 KB/s], Decompressed: 1819 Downloaded: 1863 file(s) [attempted 1863/8459 = 22%, 1461 KB/s], Decompressed: 1856 Downloaded: 1901 file(s) [attempted 1901/8459 = 22%, 387 KB/s], Decompressed: 1894 Downloaded: 1935 file(s) [attempted 1935/8459 = 22%, 335 KB/s], Decompressed: 1928 Downloaded: 1976 file(s) [attempted 1976/8459 = 23%, 431 KB/s], Decompressed: 1956 Downloaded: 2019 file(s) [attempted 2019/8459 = 23%, 123 KB/s], Decompressed: 2010 Downloaded: 2052 file(s) [attempted 2052/8459 = 24%, 659 KB/s], Decompressed: 2048 Downloaded: 2095 file(s) [attempted 2095/8459 = 24%, 245 KB/s], Decompressed: 2086 Downloaded: 2130 file(s) [attempted 2130/8459 = 25%, 43 KB/s], Decompressed: 2123 Downloaded: 2171 file(s) [attempted 2171/8459 = 25%, 180 KB/s], Decompressed: 2168 Downloaded: 2209 file(s) [attempted 2209/8459 = 26%, 256 KB/s], Decompressed: 2202 Downloaded: 2247 file(s) [attempted 2247/8459 = 26%, 1009 KB/s], Decompressed: 2243 Downloaded: 2286 file(s) [attempted 2286/8459 = 27%, 309 KB/s], Decompressed: 2277 Downloaded: 2322 file(s) [attempted 2322/8459 = 27%, 78 KB/s], Decompressed: 2321 Downloaded: 2358 file(s) [attempted 2358/8459 = 27%, 195 KB/s], Decompressed: 2353 Downloaded: 2394 file(s) [attempted 2394/8459 = 28%, 316 KB/s], Decompressed: 2387 Downloaded: 2436 file(s) [attempted 2436/8459 = 28%, 188 KB/s], Decompressed: 2431 Downloaded: 2472 file(s) [attempted 2472/8459 = 29%, 104 KB/s], Decompressed: 2469 Downloaded: 2514 file(s) [attempted 2514/8459 = 29%, 115 KB/s], Decompressed: 2507 Downloaded: 2551 file(s) [attempted 2551/8459 = 30%, 214 KB/s], Decompressed: 2548 Downloaded: 2590 file(s) [attempted 2590/8459 = 30%, 138 KB/s], Decompressed: 2582 Downloaded: 2630 file(s) [attempted 2630/8459 = 31%, 67 KB/s], Decompressed: 2623 Downloaded: 2664 file(s) [attempted 2664/8459 = 31%, 660 KB/s], Decompressed: 2661 Downloaded: 2705 file(s) [attempted 2705/8459 = 31%, 698 KB/s], Decompressed: 2702 Downloaded: 2743 file(s) [attempted 2743/8459 = 32%, 95 KB/s], Decompressed: 2739 Downloaded: 2787 file(s) [attempted 2787/8459 = 32%, 476 KB/s], Decompressed: 2784 Downloaded: 2828 file(s) [attempted 2828/8459 = 33%, 32 KB/s], Decompressed: 2822 Downloaded: 2863 file(s) [attempted 2863/8459 = 33%, 439 KB/s], Decompressed: 2859 Downloaded: 2904 file(s) [attempted 2904/8459 = 34%, 115 KB/s], Decompressed: 2900 Downloaded: 2940 file(s) [attempted 2940/8459 = 34%, 778 KB/s], Decompressed: 2935 Downloaded: 2982 file(s) [attempted 2982/8459 = 35%, 22 KB/s], Decompressed: 2979 Downloaded: 3021 file(s) [attempted 3021/8459 = 35%, 140 KB/s], Decompressed: 3013 Downloaded: 3060 file(s) [attempted 3060/8459 = 36%, 31 KB/s], Decompressed: 3051 Downloaded: 3098 file(s) [attempted 3098/8459 = 36%, 175 KB/s], Decompressed: 3088 Downloaded: 3136 file(s) [attempted 3136/8459 = 37%, 95 KB/s], Decompressed: 3133 Downloaded: 3181 file(s) [attempted 3181/8459 = 37%, 411 KB/s], Decompressed: 3174 Downloaded: 3216 file(s) [attempted 3216/8459 = 38%, 40 KB/s], Decompressed: 3212 Downloaded: 3256 file(s) [attempted 3256/8459 = 38%, 71 KB/s], Decompressed: 3253 Downloaded: 3296 file(s) [attempted 3296/8459 = 38%, 83 KB/s], Decompressed: 3288 Downloaded: 3331 file(s) [attempted 3331/8459 = 39%, 201 KB/s], Decompressed: 3321 Downloaded: 3373 file(s) [attempted 3373/8459 = 39%, 267 KB/s], Decompressed: 3369 Downloaded: 3410 file(s) [attempted 3410/8459 = 40%, 204 KB/s], Decompressed: 3403 Downloaded: 3451 file(s) [attempted 3451/8459 = 40%, 377 KB/s], Decompressed: 3444 Downloaded: 3496 file(s) [attempted 3496/8459 = 41%, 1871 KB/s], Decompressed: 3492 Downloaded: 3533 file(s) [attempted 3533/8459 = 41%, 65 KB/s], Decompressed: 3527 Downloaded: 3571 file(s) [attempted 3571/8459 = 42%, 526 KB/s], Decompressed: 3568 Downloaded: 3609 file(s) [attempted 3609/8459 = 42%, 300 KB/s], Decompressed: 3605 Downloaded: 3646 file(s) [attempted 3646/8459 = 43%, 375 KB/s], Decompressed: 3636 Downloaded: 3691 file(s) [attempted 3691/8459 = 43%, 190 KB/s], Decompressed: 3687 Downloaded: 3728 file(s) [attempted 3728/8459 = 44%, 225 KB/s], Decompressed: 3718 Downloaded: 3766 file(s) [attempted 3766/8459 = 44%, 611 KB/s], Decompressed: 3759 Downloaded: 3807 file(s) [attempted 3807/8459 = 45%, 211 KB/s], Decompressed: 3804 Downloaded: 3848 file(s) [attempted 3848/8459 = 45%, 230 KB/s], Decompressed: 3845 Downloaded: 3889 file(s) [attempted 3889/8459 = 45%, 552 KB/s], Decompressed: 3882 Downloaded: 3930 file(s) [attempted 3930/8459 = 46%, 145 KB/s], Decompressed: 3924 Downloaded: 3965 file(s) [attempted 3965/8459 = 46%, 110 KB/s], Decompressed: 3961 Downloaded: 4006 file(s) [attempted 4006/8459 = 47%, 34 KB/s], Decompressed: 4002 Downloaded: 4047 file(s) [attempted 4047/8459 = 47%, 55 KB/s], Decompressed: 4037 Downloaded: 4081 file(s) [attempted 4081/8459 = 48%, 59 KB/s], Decompressed: 4074 Downloaded: 4119 file(s) [attempted 4119/8459 = 48%, 167 KB/s], Decompressed: 4115 Downloaded: 4153 file(s) [attempted 4153/8459 = 49%, 249 KB/s], Decompressed: 4149 Downloaded: 4194 file(s) [attempted 4194/8459 = 49%, 22 KB/s], Decompressed: 4191 Downloaded: 4232 file(s) [attempted 4232/8459 = 50%, 729 KB/s], Decompressed: 4228 Downloaded: 4274 file(s) [attempted 4274/8459 = 50%, 74 KB/s], Decompressed: 4269 Downloaded: 4310 file(s) [attempted 4310/8459 = 50%, 491 KB/s], Decompressed: 4307 Downloaded: 4345 file(s) [attempted 4345/8459 = 51%, 848 KB/s], Decompressed: 4341 Downloaded: 4386 file(s) [attempted 4386/8459 = 51%, 1265 KB/s], Decompressed: 4382 Downloaded: 4430 file(s) [attempted 4430/8459 = 52%, 305 KB/s], Decompressed: 4427 Downloaded: 4470 file(s) [attempted 4470/8459 = 52%, 52 KB/s], Decompressed: 4461 Downloaded: 4505 file(s) [attempted 4505/8459 = 53%, 34 KB/s], Decompressed: 4499 Downloaded: 4538 file(s) [attempted 4538/8459 = 53%, 534 KB/s], Decompressed: 4533 Downloaded: 4578 file(s) [attempted 4578/8459 = 54%, 128 KB/s], Decompressed: 4574 Downloaded: 4618 file(s) [attempted 4618/8459 = 54%, 62 KB/s], Decompressed: 4615 Downloaded: 4662 file(s) [attempted 4662/8459 = 55%, 52 KB/s], Decompressed: 4656 Downloaded: 4691 file(s) [attempted 4691/8459 = 55%, 366 KB/s], Decompressed: 4683 Downloaded: 4728 file(s) [attempted 4728/8459 = 55%, 35 KB/s], Decompressed: 4724 Downloaded: 4772 file(s) [attempted 4772/8459 = 56%, 34 KB/s], Decompressed: 4769 Downloaded: 4813 file(s) [attempted 4813/8459 = 56%, 227 KB/s], Decompressed: 4803 Downloaded: 4848 file(s) [attempted 4848/8459 = 57%, 113 KB/s], Decompressed: 4837 Downloaded: 4882 file(s) [attempted 4882/8459 = 57%, 222 KB/s], Decompressed: 4878 Downloaded: 4923 file(s) [attempted 4923/8459 = 58%, 446 KB/s], Decompressed: 4919 Downloaded: 4967 file(s) [attempted 4967/8459 = 58%, 127 KB/s], Decompressed: 4961 Downloaded: 5005 file(s) [attempted 5005/8459 = 59%, 78 KB/s], Decompressed: 5002 Downloaded: 5043 file(s) [attempted 5043/8459 = 59%, 159 KB/s], Decompressed: 5036 Downloaded: 5080 file(s) [attempted 5080/8459 = 60%, 147 KB/s], Decompressed: 5077 Downloaded: 5121 file(s) [attempted 5121/8459 = 60%, 1855 KB/s], Decompressed: 5118 Downloaded: 5161 file(s) [attempted 5161/8459 = 61%, 1218 KB/s], Decompressed: 5152 Downloaded: 5197 file(s) [attempted 5197/8459 = 61%, 110 KB/s], Decompressed: 5187 Downloaded: 5233 file(s) [attempted 5233/8459 = 61%, 233 KB/s], Decompressed: 5228 Downloaded: 5276 file(s) [attempted 5276/8459 = 62%, 381 KB/s], Decompressed: 5269 Downloaded: 5306 file(s) [attempted 5306/8459 = 62%, 78 KB/s], Decompressed: 5299 Downloaded: 5351 file(s) [attempted 5351/8459 = 63%, 702 KB/s], Decompressed: 5347 Downloaded: 5392 file(s) [attempted 5392/8459 = 63%, 221 KB/s], Decompressed: 5385 Downloaded: 5429 file(s) [attempted 5429/8459 = 64%, 187 KB/s], Decompressed: 5423 Downloaded: 5467 file(s) [attempted 5467/8459 = 64%, 579 KB/s], Decompressed: 5464 Downloaded: 5505 file(s) [attempted 5505/8459 = 65%, 285 KB/s], Decompressed: 5501 Downloaded: 5549 file(s) [attempted 5549/8459 = 65%, 474 KB/s], Decompressed: 5546 Downloaded: 5590 file(s) [attempted 5590/8459 = 66%, 1703 KB/s], Decompressed: 5587 Downloaded: 5625 file(s) [attempted 5625/8459 = 66%, 284 KB/s], Decompressed: 5621 Downloaded: 5664 file(s) [attempted 5664/8459 = 66%, 1222 KB/s], Decompressed: 5655 Downloaded: 5703 file(s) [attempted 5703/8459 = 67%, 183 KB/s], Decompressed: 5700 Downloaded: 5744 file(s) [attempted 5744/8459 = 67%, 100 KB/s], Decompressed: 5741 Downloaded: 5776 file(s) [attempted 5776/8459 = 68%, 184 KB/s], Decompressed: 5772 Downloaded: 5820 file(s) [attempted 5820/8459 = 68%, 190 KB/s], Decompressed: 5813 Downloaded: 5857 file(s) [attempted 5857/8459 = 69%, 343 KB/s], Decompressed: 5850 Downloaded: 5895 file(s) [attempted 5895/8459 = 69%, 144 KB/s], Decompressed: 5891 Downloaded: 5933 file(s) [attempted 5933/8459 = 70%, 132 KB/s], Decompressed: 5929 Downloaded: 5970 file(s) [attempted 5970/8459 = 70%, 219 KB/s], Decompressed: 5967 Downloaded: 6011 file(s) [attempted 6011/8459 = 71%, 601 KB/s], Decompressed: 6008 Downloaded: 6045 file(s) [attempted 6045/8459 = 71%, 635 KB/s], Decompressed: 6042 Downloaded: 6090 file(s) [attempted 6090/8459 = 71%, 1369 KB/s], Decompressed: 6087 Downloaded: 6134 file(s) [attempted 6134/8459 = 72%, 219 KB/s], Decompressed: 6128 Downloaded: 6174 file(s) [attempted 6174/8459 = 72%, 151 KB/s], Decompressed: 6169 Downloaded: 6206 file(s) [attempted 6206/8459 = 73%, 507 KB/s], Decompressed: 6203 Downloaded: 6247 file(s) [attempted 6247/8459 = 73%, 313 KB/s], Decompressed: 6241 Downloaded: 6287 file(s) [attempted 6287/8459 = 74%, 182 KB/s], Decompressed: 6282 Downloaded: 6326 file(s) [attempted 6326/8459 = 74%, 77 KB/s], Decompressed: 6319 Downloaded: 6360 file(s) [attempted 6360/8459 = 75%, 26 KB/s], Decompressed: 6353 Downloaded: 6400 file(s) [attempted 6400/8459 = 75%, 363 KB/s], Decompressed: 6391 Downloaded: 6436 file(s) [attempted 6436/8459 = 76%, 188 KB/s], Decompressed: 6432 Downloaded: 6477 file(s) [attempted 6477/8459 = 76%, 326 KB/s], Decompressed: 6470 Downloaded: 6514 file(s) [attempted 6514/8459 = 77%, 1686 KB/s], Decompressed: 6511 Downloaded: 6552 file(s) [attempted 6552/8459 = 77%, 103 KB/s], Decompressed: 6549 Downloaded: 6590 file(s) [attempted 6590/8459 = 77%, 455 KB/s], Decompressed: 6586 Downloaded: 6627 file(s) [attempted 6627/8459 = 78%, 62 KB/s], Decompressed: 6624 Downloaded: 6668 file(s) [attempted 6668/8459 = 78%, 83 KB/s], Decompressed: 6661 Downloaded: 6706 file(s) [attempted 6706/8459 = 79%, 59 KB/s], Decompressed: 6703 Downloaded: 6744 file(s) [attempted 6744/8459 = 79%, 110 KB/s], Decompressed: 6740 Downloaded: 6783 file(s) [attempted 6783/8459 = 80%, 76 KB/s], Decompressed: 6774 Downloaded: 6822 file(s) [attempted 6822/8459 = 80%, 119 KB/s], Decompressed: 6815 Downloaded: 6863 file(s) [attempted 6863/8459 = 81%, 193 KB/s], Decompressed: 6860 Downloaded: 6901 file(s) [attempted 6901/8459 = 81%, 439 KB/s], Decompressed: 6898 Downloaded: 6942 file(s) [attempted 6942/8459 = 82%, 411 KB/s], Decompressed: 6935 Downloaded: 6980 file(s) [attempted 6980/8459 = 82%, 602 KB/s], Decompressed: 6976 Downloaded: 7017 file(s) [attempted 7017/8459 = 82%, 115 KB/s], Decompressed: 7014 Downloaded: 7065 file(s) [attempted 7065/8459 = 83%, 235 KB/s], Decompressed: 7058 Downloaded: 7110 file(s) [attempted 7110/8459 = 84%, 688 KB/s], Decompressed: 7103 Downloaded: 7147 file(s) [attempted 7147/8459 = 84%, 1354 KB/s], Decompressed: 7144 Downloaded: 7185 file(s) [attempted 7185/8459 = 84%, 139 KB/s], Decompressed: 7178 Downloaded: 7223 file(s) [attempted 7223/8459 = 85%, 723 KB/s], Decompressed: 7219 Downloaded: 7264 file(s) [attempted 7264/8459 = 85%, 694 KB/s], Decompressed: 7260 Downloaded: 7305 file(s) [attempted 7305/8459 = 86%, 138 KB/s], Decompressed: 7298 Downloaded: 7343 file(s) [attempted 7343/8459 = 86%, 299 KB/s], Decompressed: 7336 Downloaded: 7387 file(s) [attempted 7387/8459 = 87%, 572 KB/s], Decompressed: 7377 Downloaded: 7421 file(s) [attempted 7421/8459 = 87%, 203 KB/s], Decompressed: 7418 Downloaded: 7462 file(s) [attempted 7462/8459 = 88%, 935 KB/s], Decompressed: 7455 Downloaded: 7507 file(s) [attempted 7507/8459 = 88%, 80 KB/s], Decompressed: 7500 Downloaded: 7548 file(s) [attempted 7548/8459 = 89%, 631 KB/s], Decompressed: 7542 Downloaded: 7586 file(s) [attempted 7586/8459 = 89%, 1279 KB/s], Decompressed: 7582 Downloaded: 7627 file(s) [attempted 7627/8459 = 90%, 133 KB/s], Decompressed: 7620 Downloaded: 7668 file(s) [attempted 7668/8459 = 90%, 371 KB/s], Decompressed: 7664 Downloaded: 7709 file(s) [attempted 7709/8459 = 91%, 69 KB/s], Decompressed: 7705 Downloaded: 7750 file(s) [attempted 7750/8459 = 91%, 301 KB/s], Decompressed: 7743 Downloaded: 7787 file(s) [attempted 7787/8459 = 92%, 590 KB/s], Decompressed: 7781 Downloaded: 7825 file(s) [attempted 7825/8459 = 92%, 650 KB/s], Decompressed: 7818 Downloaded: 7866 file(s) [attempted 7866/8459 = 92%, 154 KB/s], Decompressed: 7863 Downloaded: 7911 file(s) [attempted 7911/8459 = 93%, 1479 KB/s], Decompressed: 7904 Downloaded: 7948 file(s) [attempted 7948/8459 = 93%, 126 KB/s], Decompressed: 7945 Downloaded: 7988 file(s) [attempted 7988/8459 = 94%, 600 KB/s], Decompressed: 7979 Downloaded: 8023 file(s) [attempted 8023/8459 = 94%, 243 KB/s], Decompressed: 8017 Downloaded: 8065 file(s) [attempted 8065/8459 = 95%, 78 KB/s], Decompressed: 8061 Downloaded: 8102 file(s) [attempted 8102/8459 = 95%, 580 KB/s], Decompressed: 8099 Downloaded: 8143 file(s) [attempted 8143/8459 = 96%, 361 KB/s], Decompressed: 8140 Downloaded: 8181 file(s) [attempted 8181/8459 = 96%, 93 KB/s], Decompressed: 8178 Downloaded: 8222 file(s) [attempted 8222/8459 = 97%, 78 KB/s], Decompressed: 8215 Downloaded: 8260 file(s) [attempted 8260/8459 = 97%, 458 KB/s], Decompressed: 8249 Downloaded: 8297 file(s) [attempted 8297/8459 = 98%, 584 KB/s], Decompressed: 8291 Downloaded: 8332 file(s) [attempted 8332/8459 = 98%, 83 KB/s], Decompressed: 8328 Downloaded: 8373 file(s) [attempted 8373/8459 = 98%, 585 KB/s], Decompressed: 8369 Downloaded: 8414 file(s) [attempted 8414/8459 = 99%, 112 KB/s], Decompressed: 8410 Downloaded: 8450 file(s) [attempted 8450/8459 = 99%, 81 KB/s], Decompressed: 8445 Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 81 KB/s], Decompressed: 8455
lean_checker exit 0
lake build
ℹ [3535/3544] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3556/3570] Replayed PrimeNumberTheoremAnd.StrongPNT
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1475:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1524:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1641:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1786:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2181:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2271:6: declaration uses `sorry`
✔ [3565/3572] Built PrimeNumberTheoremAnd.BorelCaratheodory (58s)
⚠ [3695/3715] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3812/3819] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3817/3834] Built PrimeNumberTheoremAnd.IEANTN.Mertens (14s)
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1169:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1182:16: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1208:16: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1220:16: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1286:8: declaration uses `sorry`
⚠ [3880/3892] Built PrimeNumberTheoremAnd.IEANTN.ZetaAppendix (46s)
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2577:8: `simp [v, Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2578:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2599:8: `simp [v', Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2600:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2817:8: `simp [v, Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2818:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2833:8: `simp [v', Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2834:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2963:4: `simp [W]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2964:4: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3069:4: `simp [p]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3070:4: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3084:4: `simp [Set.uIcc_of_le hab]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3084:4: Try this:
[apply] simp only [_root_.deriv_ofReal]
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3085:4: `fun_prop` uses `⊢`!
⚠ [3881/3892] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
⚠ [3883/3894] Built PrimeNumberTheoremAnd.IEANTN.ZetaSummary (2.0s)
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:35:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:48:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:58:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:68:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:78:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:88:8: declaration uses `sorry`
✔ [3887/3895] Built PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions (2.7s)
✔ [3891/3895] Built PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions (7.5s)
⚠ [3892/3895] Built PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky (5.6s)
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:45:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:112:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:149:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:153:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:165:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:177:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:218:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:228:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:257:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:354:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:368:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:383:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:402:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:408:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:418:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:464:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:473:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:488:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:530:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:557:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:585:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:636:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:649:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:661:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:705:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:715:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:728:8: declaration uses `sorry`
✔ [3894/3907] Built PrimeNumberTheoremAnd.IEANTN.CostaPereira (8.0s)
⚠ [4017/4022] Built PrimeNumberTheoremAnd.IEANTN.Buthe (11s)
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:31:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:41:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:51:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:61:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:83:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:131:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:142:8: declaration uses `sorry`
⚠ [4018/4025] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app (15s)
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:47:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:168:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:516:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1127:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1180:8: declaration uses `sorry`
⚠ [4020/4026] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime (11s)
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
⚠ [4022/4055] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW (27s)
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1518:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2184:8: declaration uses `sorry`
✔ [4033/4061] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_a2_bounds (4.8s)
✔ [4036/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core (7.9s)
✔ [4038/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_65_85 (17s)
✔ [4039/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_misc (11s)
✔ [4040/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_12600_24000 (65s)
✔ [4041/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_10600_12500 (40s)
✔ [4042/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_8600_10500 (39s)
✔ [4043/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_6600_8500 (39s)
✔ [4044/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4900_6500 (38s)
✔ [4045/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4400_4875 (38s)
✔ [4046/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3900_4375 (40s)
✔ [4047/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3400_3875 (39s)
✔ [4048/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2900_3375 (39s)
✔ [4049/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2400_2875 (39s)
✔ [4050/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_1900_2375 (39s)
✔ [4051/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_100_1875 (39s)
✔ [4052/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_90_95 (5.5s)
✔ [4053/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_values (9.5s)
✔ [4054/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_next (18s)
ℹ [4055/4068] Built PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 (46s)
info: PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:359:15: Try this:
[apply] ring_nf
The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
✔ [4057/4070] Built PrimeNumberTheoremAnd.IEANTN.PrimeInInterval (3.8s)
✔ [4059/4072] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_20_43 (60s)
⚠ [4060/4074] Built PrimeNumberTheoremAnd.IEANTN.CH2.CH2 (13s)
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3156:8: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3245:4: Try this:
[apply] ring_nf
The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3615:4: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.
Note: This linter can be disabled with `set_option linter.style.show false`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:4207:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:4221:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:4235:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:4247:8: declaration uses `sorry`
⚠ [4062/4074] Replayed PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:85:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:129:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:304:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:449:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:464:8: declaration uses `sorry`
✔ [4064/4074] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_44_59 (39s)
✔ [4066/4074] Built PrimeNumberTheoremAnd.IEANTN.Chebyshev (14s)
⚠ [4067/4074] Built PrimeNumberTheoremAnd.IEANTN.Dusart (17s)
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:89:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:148:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:171:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:274:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:286:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:310:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:321:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:332:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:343:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:354:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:366:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:377:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:388:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:399:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:410:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:620:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:680:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:692:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:705:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:716:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:728:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:736:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:748:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:760:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:772:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:784:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:796:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:808:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:820:8: declaration uses `sorry`
✔ [4070/4074] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows (4.0s)
⚠ [4072/4074] Built PrimeNumberTheoremAnd.IEANTN.FKS2 (57s)
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:316:2: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.
Note: This linter can be disabled with `set_option linter.style.show false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3776:32: Try this:
[apply] ring_nf
The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3781:4: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.
Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3784:6: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.
Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3786:4: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.
Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3776:32: The following tactic starts with 2 goals and ends with 2 goals, 1 of which is not operated on.
ring
Please focus on the current goal, for instance using `·` (typed as "\.").
Note: This linter can be disabled with `set_option linter.style.multiGoal false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3827:4: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.
Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3830:8: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.
Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: `simp_all +decide [ επ_num, μ_num ]` is a flexible tactic modifying `⊢`. Try `simp_all?` and use the suggested `simp_all only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: Try this:
[apply] simp_all +decide only [ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3836:4: `have h63 :=
theorem_6_3 (by linarith : 14 ≤ x₁) x₂.toReal
(by
cases x₂ <;> norm_num at *; · linarith;
· exact absurd hc (by exact ne_of_lt (EReal.coe_lt_top _)))
x hx₁
(by
cases x₂ <;> norm_num at *; · linarith;
· exact absurd hc (by exact ne_of_lt (EReal.coe_lt_top _)))
(by
cases x₂ <;> norm_num at *; · exact_mod_cast hc;
· exact mul_nonneg (by linarith) (Real.log_nonneg (by linarith)))` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: `simp_all +decide [ επ_num, μ_num ]` is a flexible tactic modifying `⊢`. Try `simp_all?` and use the suggested `simp_all only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: Try this:
[apply] simp_all +decide only [ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3846:4: `unfold μ_num_1` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3847:35: `simp_all +decide [ mul_assoc, mul_comm, mul_left_comm ]` is a flexible tactic modifying `⊢`. Try `simp_all?` and use the suggested `simp_all only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3847:35: Try this:
[apply] simp_all +decide only [Fin.Iio_last_eq_map, Finset.sum_sub_distrib, Finset.sum_map, Fin.coe_castSuccEmb,
Fin.coeSucc_eq_succ, ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3849:6: `exact absurd (this y hy₁) (by norm_num [h]; linarith)` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: `simp_all +decide [ επ_num, μ_num ]` is a flexible tactic modifying `⊢`. Try `simp_all?` and use the suggested `simp_all only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: Try this:
[apply] simp_all +decide only [ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3858:6: `exact absurd ‹_› (not_le_of_gt hc)` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4652:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4679:8: declaration uses `sorry`
✔ [4073/4103] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_dispatch (17s)
✔ [4087/4108] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtCore (17s)
✔ [4091/4108] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_13 (13s)
✔ [4092/4109] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_12 (21s)
✔ [4093/4109] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_11 (21s)
✔ [4094/4109] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_10 (22s)
✔ [4095/4109] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_09 (21s)
✔ [4096/4109] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_08 (21s)
✔ [4097/4109] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_07 (21s)
✔ [4098/4109] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_06 (21s)
✔ [4099/4109] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_05 (21s)
✔ [4100/4109] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_04 (22s)
✔ [4101/4109] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_03 (22s)
✔ [4102/4109] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_02 (21s)
✔ [4103/4109] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_01 (20s)
✔ [4104/4110] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_00 (21s)
⚠ [4107/4111] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext (4.1s)
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean:116:8: declaration uses `sorry`
⚠ [4109/4129] Built PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor (7.0s)
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`
⚠ [4119/4129] Replayed PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting
warning: PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:2045:6: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.
Note: This linter can be disabled with `set_option linter.style.show false`
✔ [4125/4166] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower (9.6s)
⚠ [4127/4166] Built PrimeNumberTheoremAnd.IEANTN.TMEEMT (14s)
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:93:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:104:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:117:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:146:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:154:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:179:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:187:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:195:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:333:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:341:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:470:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:515:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:530:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:564:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:573:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:582:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:591:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:600:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:616:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:625:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:634:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:643:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:678:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:687:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:696:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:722:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:745:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:756:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:767:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:778:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:788:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:796:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:805:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:814:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:937:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:957:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:987:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1013:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1027:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1035:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1050:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1065:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1074:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1089:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1107:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1119:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1136:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1147:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1169:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1183:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1197:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1227:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1243:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1254:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1278:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1292:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1306:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1320:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1334:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1369:8: declaration uses `sorry`
⚠ [4147/4187] Built PrimeNumberTheoremAnd.IEANTN.SecondarySummary (9.3s)
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`
ℹ [4157/4187] Replayed PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations
info: PrimeNumberTheoremAnd/IEANTN/Ramanujan/RamanujanCalculations.lean:76:4: Try this:
[apply] ring_nf
The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
⚠ [4158/4187] Replayed PrimeNumberTheoremAnd.IwaniecKowalskiCh1
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:74:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:91:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:638:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:680:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:718:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:986:3: error: doc-strings should start with a single space or newline
Note: This linter can be disabled with `set_option linter.style.docString false`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1259:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1429:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1444:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1456:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1474:6: declaration uses `sorry`
✔ [4160/4187] Built PrimeNumberTheoremAnd.IEANTN.MobiusLemma (11s)
⚠ [4161/4187] Built PrimeNumberTheoremAnd.IEANTN.Goldbach (6.5s)
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
✔ [4168/4187] Built PrimeNumberTheoremAnd.LaplaceInversion (9.0s)
✔ [4169/4187] Built PrimeNumberTheoremAnd.IEANTN.Lcm (26s)
✔ [4170/4187] Built PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan (54s)
✔ [4173/4187] Built PrimeNumberTheoremAnd.IEANTN.PrimarySummary (2.6s)
⚠ [4185/4187] Built PrimeNumberTheoremAnd.IEANTN.Kadiri (13s)
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:132:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:169:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:206:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:277:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:325:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:357:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1277:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1320:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1407:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1490:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2720:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2746:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:3352:8: declaration uses `sorry`
✔ [4186/4187] Built PrimeNumberTheoremAnd (3.1s)
Build completed successfully (4187 jobs).
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
blueprint_build exit 0
lake build :blueprint
✔ [15/35] Built Batteries.Lean.NameMapAttribute:c.o (1.6s)
✔ [26/35] Built Cli.Basic:c.o (3.1s)
✔ [30/35] Built Cli.Extensions:c.o (507ms)
✔ [33/41] Built Cli:c.o (67ms)
ℹ [3594/3611] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3629/3643] Replayed PrimeNumberTheoremAnd.StrongPNT
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1475:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1524:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1641:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1786:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2181:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2271:6: declaration uses `sorry`
✔ [3636/3647] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.BorelCaratheodory:blueprint (12s)
⚠ [3765/3773] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3891/3901] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3894/3901] Replayed PrimeNumberTheoremAnd.IEANTN.Mertens
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1169:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1182:16: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1208:16: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1220:16: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1286:8: declaration uses `sorry`
✔ [3899/3914] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Mertens:blueprint (45s)
⚠ [3960/3986] Replayed PrimeNumberTheoremAnd.IEANTN.ZetaAppendix
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2577:8: `simp [v, Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2578:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2599:8: `simp [v', Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2600:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2817:8: `simp [v, Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2818:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2833:8: `simp [v', Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2834:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2963:4: `simp [W]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2964:4: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3069:4: `simp [p]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3070:4: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3084:4: `simp [Set.uIcc_of_le hab]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3084:4: Try this:
[apply] simp only [_root_.deriv_ofReal]
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3085:4: `fun_prop` uses `⊢`!
⚠ [3962/3986] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
✔ [3967/3988] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaAppendix:blueprint (27s)
⚠ [3968/3988] Replayed PrimeNumberTheoremAnd.IEANTN.ZetaSummary
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:35:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:48:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:58:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:68:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:78:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean:88:8: declaration uses `sorry`
✔ [3974/3988] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaSummary:blueprint (3.4s)
✔ [3981/3990] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions:blueprint (2.9s)
⚠ [3982/3990] Replayed PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:45:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:112:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:149:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:153:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:165:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:177:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:218:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:228:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:257:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:354:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:368:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:383:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:402:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:408:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:418:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:464:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:473:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:488:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:530:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:557:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:585:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:636:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:649:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:661:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:705:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:715:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:728:8: declaration uses `sorry`
✔ [3984/3992] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky:blueprint (16s)
✔ [3985/3992] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions:blueprint (9.8s)
✔ [3988/3994] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CostaPereira:blueprint (6.7s)
⚠ [4107/4122] Replayed PrimeNumberTheoremAnd.IEANTN.Buthe
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:31:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:41:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:51:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:61:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:83:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:131:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:142:8: declaration uses `sorry`
✔ [4109/4122] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Buthe:blueprint (6.3s)
⚠ [4112/4130] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
⚠ [4115/4130] Replayed PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:47:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:168:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:516:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1127:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1180:8: declaration uses `sorry`
✔ [4119/4177] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime:blueprint (21s)
✔ [4120/4177] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app:blueprint (18s)
⚠ [4122/4177] Replayed PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1518:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2184:8: declaration uses `sorry`
✔ [4125/4181] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW:blueprint (24s)
✔ [4136/4198] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_a2_bounds:blueprint (5.0s)
✔ [4139/4200] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core:blueprint (3.1s)
ℹ [4157/4200] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1
info: PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:359:15: Try this:
[apply] ring_nf
The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
✔ [4161/4203] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1:blueprint (51s)
⚠ [4162/4203] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3156:8: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3245:4: Try this:
[apply] ring_nf
The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3615:4: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.
Note: This linter can be disabled with `set_option linter.style.show false`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:4207:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:4221:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:4235:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:4247:8: declaration uses `sorry`
✔ [4164/4203] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimeInInterval:blueprint (4.6s)
⚠ [4166/4203] Replayed PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:85:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:129:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:304:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:449:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:464:8: declaration uses `sorry`
✔ [4168/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_next:blueprint (3.0s)
✔ [4169/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_values:blueprint (3.0s)
✔ [4171/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_65_85:blueprint (3.1s)
✔ [4172/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_90_95:blueprint (3.1s)
✔ [4173/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_100_1875:blueprint (3.0s)
✔ [4174/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_1900_2375:blueprint (3.1s)
✔ [4175/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2400_2875:blueprint (3.1s)
✔ [4176/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2900_3375:blueprint (3.1s)
✔ [4177/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3400_3875:blueprint (3.1s)
✔ [4178/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3900_4375:blueprint (3.0s)
✔ [4179/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4400_4875:blueprint (3.1s)
✔ [4180/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4900_6500:blueprint (3.1s)
✔ [4181/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_6600_8500:blueprint (3.0s)
✔ [4182/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_8600_10500:blueprint (3.0s)
✔ [4183/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_10600_12500:blueprint (3.0s)
✔ [4184/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_12600_24000:blueprint (3.0s)
✔ [4185/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_misc:blueprint (3.0s)
✔ [4187/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_20_43:blueprint (3.0s)
✔ [4189/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CH2.CH2:blueprint (19s)
⚠ [4192/4206] Replayed PrimeNumberTheoremAnd.IEANTN.Dusart
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:89:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:148:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:171:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:274:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:286:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:310:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:321:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:332:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:343:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:354:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:366:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:377:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:388:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:399:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:410:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:620:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:680:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:692:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:705:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:716:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:728:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:736:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:748:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:760:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:772:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:784:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:796:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:808:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:820:8: declaration uses `sorry`
✔ [4195/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_44_59:blueprint (3.1s)
✔ [4197/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Chebyshev:blueprint (18s)
✔ [4198/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Dusart:blueprint (19s)
⚠ [4200/4206] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:316:2: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.
Note: This linter can be disabled with `set_option linter.style.show false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3776:32: Try this:
[apply] ring_nf
The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3781:4: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.
Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3784:6: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.
Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3786:4: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.
Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3776:32: The following tactic starts with 2 goals and ends with 2 goals, 1 of which is not operated on.
ring
Please focus on the current goal, for instance using `·` (typed as "\.").
Note: This linter can be disabled with `set_option linter.style.multiGoal false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3827:4: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.
Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3830:8: The `refine'` tactic is discouraged: please strongly consider using `refine` or `apply` instead.
Note: This linter can be disabled with `set_option linter.style.refine false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: `simp_all +decide [ επ_num, μ_num ]` is a flexible tactic modifying `⊢`. Try `simp_all?` and use the suggested `simp_all only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: Try this:
[apply] simp_all +decide only [ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3836:4: `have h63 :=
theorem_6_3 (by linarith : 14 ≤ x₁) x₂.toReal
(by
cases x₂ <;> norm_num at *; · linarith;
· exact absurd hc (by exact ne_of_lt (EReal.coe_lt_top _)))
x hx₁
(by
cases x₂ <;> norm_num at *; · linarith;
· exact absurd hc (by exact ne_of_lt (EReal.coe_lt_top _)))
(by
cases x₂ <;> norm_num at *; · exact_mod_cast hc;
· exact mul_nonneg (by linarith) (Real.log_nonneg (by linarith)))` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: `simp_all +decide [ επ_num, μ_num ]` is a flexible tactic modifying `⊢`. Try `simp_all?` and use the suggested `simp_all only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: Try this:
[apply] simp_all +decide only [ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3846:4: `unfold μ_num_1` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3847:35: `simp_all +decide [ mul_assoc, mul_comm, mul_left_comm ]` is a flexible tactic modifying `⊢`. Try `simp_all?` and use the suggested `simp_all only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3847:35: Try this:
[apply] simp_all +decide only [Fin.Iio_last_eq_map, Finset.sum_sub_distrib, Finset.sum_map, Fin.coe_castSuccEmb,
Fin.coeSucc_eq_succ, ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3849:6: `exact absurd (this y hy₁) (by norm_num [h]; linarith)` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: `simp_all +decide [ επ_num, μ_num ]` is a flexible tactic modifying `⊢`. Try `simp_all?` and use the suggested `simp_all only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3835:59: Try this:
[apply] simp_all +decide only [ge_iff_le]
info: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3858:6: `exact absurd ‹_› (not_le_of_gt hc)` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4652:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4679:8: declaration uses `sorry`
✔ [4201/4212] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows:blueprint (3.0s)
✔ [4204/4212] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2:blueprint (32s)
✔ [4206/4249] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_dispatch:blueprint (15s)
✔ [4223/4261] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtCore:blueprint (3.1s)
✔ [4241/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_00:blueprint (3.0s)
✔ [4242/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_01:blueprint (3.0s)
✔ [4243/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_02:blueprint (3.1s)
✔ [4244/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_03:blueprint (3.0s)
✔ [4245/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_04:blueprint (3.1s)
✔ [4246/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_05:blueprint (3.0s)
✔ [4247/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_06:blueprint (3.0s)
✔ [4248/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_07:blueprint (3.0s)
✔ [4249/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_08:blueprint (3.1s)
✔ [4250/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_09:blueprint (3.0s)
✔ [4251/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_10:blueprint (3.0s)
✔ [4252/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_11:blueprint (3.1s)
✔ [4253/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_12:blueprint (3.0s)
✔ [4254/4262] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_13:blueprint (3.0s)
⚠ [4255/4262] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean:116:8: declaration uses `sorry`
✔ [4257/4264] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext:blueprint (3.0s)
⚠ [4258/4264] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:19:72: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.
Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:109:37: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.
Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean:122:60: Using `native_decide` is not allowed in mathlib: because it trusts the entire Lean compiler (not just the Lean kernel), it could quite possibly be used to prove false.
Note: This linter can be disabled with `set_option linter.style.nativeDecide false`
✔ [4261/4321] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor:blueprint (5.1s)
⚠ [4273/4321] Replayed PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting
warning: PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:2045:6: The `show` tactic should only be used to indicate intermediate goal states for readability.
However, this tactic invocation changed the goal. Please use `change` instead for these purposes.
Note: This linter can be disabled with `set_option linter.style.show false`
✔ [4283/4385] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower:blueprint (3.1s)
⚠ [4284/4385] Replayed PrimeNumberTheoremAnd.IEANTN.TMEEMT
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:93:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:104:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:117:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:146:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:154:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:179:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:187:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:195:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:333:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:341:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:470:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:515:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:530:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:564:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:573:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:582:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:591:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:600:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:616:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:625:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:634:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:643:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:678:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:687:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:696:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:722:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:745:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:756:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:767:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:778:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:788:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:796:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:805:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:814:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:937:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:957:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:987:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1013:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1027:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1035:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1050:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1065:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1074:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1089:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1107:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1119:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1136:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1147:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1169:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1183:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1197:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1227:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1243:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1254:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1278:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1292:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1306:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1320:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1334:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1369:8: declaration uses `sorry`
✔ [4301/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.TMEEMT:blueprint (46s)
⚠ [4302/4395] Replayed PrimeNumberTheoremAnd.IEANTN.SecondarySummary
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:61:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:204:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:214:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:228:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:243:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:256:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:338:8: declaration uses `sorry`
ℹ [4328/4395] Replayed PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations
info: PrimeNumberTheoremAnd/IEANTN/Ramanujan/RamanujanCalculations.lean:76:4: Try this:
[apply] ring_nf
The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
⚠ [4329/4395] Replayed PrimeNumberTheoremAnd.IwaniecKowalskiCh1
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:74:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:91:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:298:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:638:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:680:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:718:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:986:3: error: doc-strings should start with a single space or newline
Note: This linter can be disabled with `set_option linter.style.docString false`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1259:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1429:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1444:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1456:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1474:6: declaration uses `sorry`
✔ [4331/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondarySummary:blueprint (7.1s)
⚠ [4332/4395] Replayed PrimeNumberTheoremAnd.IEANTN.Goldbach
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
✔ [4354/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.MobiusLemma:blueprint (10s)
✔ [4356/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Goldbach:blueprint (6.0s)
✔ [4384/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.LaplaceInversion:blueprint (2.5s)
✔ [4385/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Lcm:blueprint (11s)
✔ [4386/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimarySummary:blueprint (2.0s)
✔ [4387/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan:blueprint (15s)
⚠ [4390/4395] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:132:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:169:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:206:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:277:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:325:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:357:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1277:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1320:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1407:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1490:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2720:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2746:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:3352:8: declaration uses `sorry`
✔ [4391/4395] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Kadiri:blueprint (45s)
✔ [4393/4396] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (6.3s)
ℹ [4394/4396] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (62ms)
info: Blueprint indexing
Build completed successfully (4396 jobs).
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-a)
apx-semantic-phase {"duration_ms":25,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":335,"diagnostic_count":221,"duration_ms":28220,"module_name":"PrimeNumberTheoremAnd.IEANTN.Mertens","module_path":"PrimeNumberTheoremAnd/IEANTN/Mertens.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":409014,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Mertens","module_path":"PrimeNumberTheoremAnd/IEANTN/Mertens.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":335,"diagnostic_count":221,"duration_ms":16,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Mertens","module_path":"PrimeNumberTheoremAnd/IEANTN/Mertens.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":1810171,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":2,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":1810171,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":471,"diagnostic_count":322,"duration_ms":49147,"module_name":"PrimeNumberTheoremAnd.IEANTN.ZetaAppendix","module_path":"PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":418447,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.ZetaAppendix","module_path":"PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":471,"diagnostic_count":322,"duration_ms":51,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.ZetaAppendix","module_path":"PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.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":4207991,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":3,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":4207991,"phase":"lean_module_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":9368,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 3a1e46b855f343f1a287a5e3c974890a49a25b796fc831e00246b64839dbcef5
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":49,"runner_cache_hit":true}
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":970349,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-b)
apx-semantic-phase {"duration_ms":22,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":136,"diagnostic_count":71,"duration_ms":10882,"module_name":"PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky","module_path":"PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":442269,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky","module_path":"PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":136,"diagnostic_count":71,"duration_ms":6,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky","module_path":"PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.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":509774,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":1,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":509774,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":0,"diagnostic_count":0,"duration_ms":5,"module_name":"PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions","module_path":"PrimeNumberTheoremAnd/IEANTN/PrimaryDefinitions.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":424223,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions","module_path":"PrimeNumberTheoremAnd/IEANTN/PrimaryDefinitions.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":0,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions","module_path":"PrimeNumberTheoremAnd/IEANTN/PrimaryDefinitions.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":510,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":510,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":36,"diagnostic_count":27,"duration_ms":2873,"module_name":"PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions","module_path":"PrimeNumberTheoremAnd/IEANTN/SecondaryDefinitions.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":431701,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions","module_path":"PrimeNumberTheoremAnd/IEANTN/SecondaryDefinitions.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":36,"diagnostic_count":27,"duration_ms":3,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions","module_path":"PrimeNumberTheoremAnd/IEANTN/SecondaryDefinitions.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":189395,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":1,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":189395,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":6,"diagnostic_count":0,"duration_ms":495,"module_name":"PrimeNumberTheoremAnd.IEANTN.ZetaSummary","module_path":"PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":423643,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.ZetaSummary","module_path":"PrimeNumberTheoremAnd/IEANTN/ZetaSummary.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":6,"diagnostic_count":0,"duration_ms":1,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.ZetaSummary","module_path":"PrimeNumberTheoremAnd/IEANTN/ZetaSummary.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":11072,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":11072,"phase":"lean_module_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":21}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":11107,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 3a1e46b855f343f1a287a5e3c974890a49a25b796fc831e00246b64839dbcef5
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":55,"runner_cache_hit":true}
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":1769311,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r2)
apx-semantic-phase {"duration_ms":25,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":57,"diagnostic_count":33,"duration_ms":4185,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtCore","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtCore.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":436484,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtCore","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtCore.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":57,"diagnostic_count":33,"duration_ms":3,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtCore","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtCore.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":166420,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":166420,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":69,"diagnostic_count":54,"duration_ms":4916,"module_name":"PrimeNumberTheoremAnd.IEANTN.MobiusLemma","module_path":"PrimeNumberTheoremAnd/IEANTN/MobiusLemma.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":409491,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.MobiusLemma","module_path":"PrimeNumberTheoremAnd/IEANTN/MobiusLemma.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":69,"diagnostic_count":54,"duration_ms":3,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.MobiusLemma","module_path":"PrimeNumberTheoremAnd/IEANTN/MobiusLemma.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":430031,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":1,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":430031,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":17,"diagnostic_count":10,"duration_ms":1145,"module_name":"PrimeNumberTheoremAnd.IEANTN.PrimeInInterval","module_path":"PrimeNumberTheoremAnd/IEANTN/PrimeInInterval.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":416142,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.PrimeInInterval","module_path":"PrimeNumberTheoremAnd/IEANTN/PrimeInInterval.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":17,"diagnostic_count":10,"duration_ms":2,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.PrimeInInterval","module_path":"PrimeNumberTheoremAnd/IEANTN/PrimeInInterval.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":101503,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":101503,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":297,"diagnostic_count":259,"duration_ms":22840,"module_name":"PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime","module_path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":426393,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime","module_path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":297,"diagnostic_count":259,"duration_ms":15,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime","module_path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.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":1556361,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":1,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":1556361,"phase":"lean_module_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":24}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":11073,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 3a1e46b855f343f1a287a5e3c974890a49a25b796fc831e00246b64839dbcef5
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":50,"runner_cache_hit":true}
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":1736113,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r3)
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":428,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_00","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_00.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":451594,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_00","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_00.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":1,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_00","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_00.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":74842,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":74842,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":659,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_01","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_01.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":450152,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_01","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_01.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_01","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_01.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":77992,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":77992,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":391,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_02","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_02.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":441638,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_02","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_02.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_02","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_02.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":80054,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":80054,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":380,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_13","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_13.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":434622,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_13","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_13.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_13","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_13.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":68407,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":68407,"phase":"lean_module_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":24}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":15172,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 3a1e46b855f343f1a287a5e3c974890a49a25b796fc831e00246b64839dbcef5
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":21,"runner_cache_hit":true}
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":1819931,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r4)
apx-semantic-phase {"duration_ms":4,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":459,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_03","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_03.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":445195,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_03","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_03.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_03","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_03.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":82759,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":82759,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":427,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_04","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_04.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":439148,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_04","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_04.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_04","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_04.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":85603,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":85603,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":429,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_05","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_05.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":435334,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_05","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_05.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_05","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_05.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":87967,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":87967,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":365,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_06","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_06.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":436040,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_06","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_06.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_06","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_06.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":90257,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":90257,"phase":"lean_module_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":24}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":21035,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 3a1e46b855f343f1a287a5e3c974890a49a25b796fc831e00246b64839dbcef5
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":262,"runner_cache_hit":true}
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":1820561,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r5)
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":441,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_07","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_07.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":431454,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_07","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_07.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_07","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_07.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":92539,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":92539,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":419,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_08","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_08.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":434196,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_08","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_08.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":1,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_08","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_08.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":94376,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":1,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":94376,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":477,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_09","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_09.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":437716,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_09","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_09.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":1,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_09","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_09.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":96327,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":1,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":96327,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":492,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_10","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_10.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":431964,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_10","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_10.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":1,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_10","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_10.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":101240,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":101240,"phase":"lean_module_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":24}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":14235,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 3a1e46b855f343f1a287a5e3c974890a49a25b796fc831e00246b64839dbcef5
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":33,"runner_cache_hit":true}
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":1741818,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r6)
apx-semantic-phase {"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":150,"diagnostic_count":101,"duration_ms":12023,"module_name":"PrimeNumberTheoremAnd.IEANTN.Dusart","module_path":"PrimeNumberTheoremAnd/IEANTN/Dusart.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":437106,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Dusart","module_path":"PrimeNumberTheoremAnd/IEANTN/Dusart.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":150,"diagnostic_count":101,"duration_ms":15,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Dusart","module_path":"PrimeNumberTheoremAnd/IEANTN/Dusart.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":849814,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":1,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":849814,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":468,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_11","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_11.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":439099,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_11","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_11.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_11","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_11.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":102723,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":1,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":102723,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":448,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_12","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_12.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":438396,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_12","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_12.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_12","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4ExtData_12.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":107456,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":1,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":107456,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":0,"diagnostic_count":0,"duration_ms":5,"module_name":"PrimeNumberTheoremAnd.IEANTN.PrimarySummary","module_path":"PrimeNumberTheoremAnd/IEANTN/PrimarySummary.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":433530,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.PrimarySummary","module_path":"PrimeNumberTheoremAnd/IEANTN/PrimarySummary.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":0,"diagnostic_count":0,"duration_ms":0,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.PrimarySummary","module_path":"PrimeNumberTheoremAnd/IEANTN/PrimarySummary.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":502,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":1,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":502,"phase":"lean_module_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":22}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":11575,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 3a1e46b855f343f1a287a5e3c974890a49a25b796fc831e00246b64839dbcef5
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":38,"runner_cache_hit":true}
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":1765904,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r7)
apx-semantic-phase {"duration_ms":2,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":679,"diagnostic_count":493,"duration_ms":67936,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":442561,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":679,"diagnostic_count":493,"duration_ms":44,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2.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":3913891,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":3,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":3913891,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":41,"diagnostic_count":6,"duration_ms":2718,"module_name":"PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower","module_path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":441701,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower","module_path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":41,"diagnostic_count":6,"duration_ms":1,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower","module_path":"PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RSPrimeLower.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":344830,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":1,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":344830,"phase":"lean_module_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":18}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":10316,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 3a1e46b855f343f1a287a5e3c974890a49a25b796fc831e00246b64839dbcef5
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":39,"runner_cache_hit":true}
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":965297,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r8)
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":32,"diagnostic_count":19,"duration_ms":2118,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":428644,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":32,"diagnostic_count":19,"duration_ms":2,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.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":94339,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":1,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":94339,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":258,"diagnostic_count":135,"duration_ms":21337,"module_name":"PrimeNumberTheoremAnd.IEANTN.TMEEMT","module_path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":425502,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.TMEEMT","module_path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":258,"diagnostic_count":135,"duration_ms":15,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.TMEEMT","module_path":"PrimeNumberTheoremAnd/IEANTN/TMEEMT.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":1269379,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":1,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":1269379,"phase":"lean_module_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":22}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":9745,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 3a1e46b855f343f1a287a5e3c974890a49a25b796fc831e00246b64839dbcef5
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":49,"runner_cache_hit":true}
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":882407,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r9)
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":27,"diagnostic_count":9,"duration_ms":1850,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":439429,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":27,"diagnostic_count":9,"duration_ms":1,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor","module_path":"PrimeNumberTheoremAnd/IEANTN/FKS2Floor/Cor22Floor.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":169753,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":1,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":169753,"phase":"lean_module_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":10520,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 3a1e46b855f343f1a287a5e3c974890a49a25b796fc831e00246b64839dbcef5
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":42,"runner_cache_hit":true}
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":446066,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r10)
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":67,"diagnostic_count":53,"duration_ms":4979,"module_name":"PrimeNumberTheoremAnd.IEANTN.SecondarySummary","module_path":"PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":430307,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.SecondarySummary","module_path":"PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":67,"diagnostic_count":53,"duration_ms":4,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.SecondarySummary","module_path":"PrimeNumberTheoremAnd/IEANTN/SecondarySummary.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":257157,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":257157,"phase":"lean_module_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":10956,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 3a1e46b855f343f1a287a5e3c974890a49a25b796fc831e00246b64839dbcef5
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":54,"runner_cache_hit":true}
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":440222,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r11)
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":70,"diagnostic_count":54,"duration_ms":5499,"module_name":"PrimeNumberTheoremAnd.IEANTN.Goldbach","module_path":"PrimeNumberTheoremAnd/IEANTN/Goldbach.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":451837,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Goldbach","module_path":"PrimeNumberTheoremAnd/IEANTN/Goldbach.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":70,"diagnostic_count":54,"duration_ms":7,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Goldbach","module_path":"PrimeNumberTheoremAnd/IEANTN/Goldbach.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":396745,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":1,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":396745,"phase":"lean_module_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":24}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":10464,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 3a1e46b855f343f1a287a5e3c974890a49a25b796fc831e00246b64839dbcef5
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":36,"runner_cache_hit":true}
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":462020,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r12)
apx-semantic-phase {"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":235,"diagnostic_count":164,"duration_ms":19064,"module_name":"PrimeNumberTheoremAnd.IEANTN.Lcm","module_path":"PrimeNumberTheoremAnd/IEANTN/Lcm.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":441800,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Lcm","module_path":"PrimeNumberTheoremAnd/IEANTN/Lcm.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":235,"diagnostic_count":164,"duration_ms":11,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Lcm","module_path":"PrimeNumberTheoremAnd/IEANTN/Lcm.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":1491369,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":1,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":1491369,"phase":"lean_module_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":24}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":10763,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 3a1e46b855f343f1a287a5e3c974890a49a25b796fc831e00246b64839dbcef5
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":38,"runner_cache_hit":true}
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":465586,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r13)
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":263,"diagnostic_count":178,"duration_ms":23212,"module_name":"PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan","module_path":"PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":451787,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan","module_path":"PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":263,"diagnostic_count":178,"duration_ms":12,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan","module_path":"PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.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":1806664,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":1,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":1806664,"phase":"lean_module_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":11151,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 3a1e46b855f343f1a287a5e3c974890a49a25b796fc831e00246b64839dbcef5
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":39,"runner_cache_hit":true}
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":487343,"ok":true}