Verification run
Run 147
succeeded commit
569325d78913 toolchain lean-v4-30-0 prover lean took 10h 17m · finished 5d 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
`
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`
✔ [4313/4397] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.TMEEMT:blueprint (47s)
⚠ [4314/4397] 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/4397] 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/4397] 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`
✔ [4332/4397] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondarySummary:blueprint (7.6s)
⚠ [4333/4397] 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/4397] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.MobiusLemma:blueprint (11s)
✔ [4356/4397] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Goldbach:blueprint (6.6s)
✔ [4364/4397] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.LaplaceInversion:blueprint (2.8s)
✔ [4365/4397] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Lcm:blueprint (12s)
✔ [4366/4397] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan:blueprint (16s)
✔ [4367/4397] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.PerronFormula:blueprint (22s)
✔ [4390/4397] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimarySummary:blueprint (3.2s)
⚠ [4392/4397] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:133:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:170:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:207:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:278:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:326:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:358:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1305:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1392:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1475:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2705:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2731:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:3337:8: declaration uses `sorry`
✔ [4393/4397] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Kadiri:blueprint (47s)
✔ [4395/4397] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (25s)
ℹ [4396/4397] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (506ms)
info: Blueprint indexing
Build completed successfully (4398 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=565637
stdout:
apx-semantic-phase {"duration_ms":21,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":353,"diagnostic_count":228,"duration_ms":31801,"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":426691,"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":353,"diagnostic_count":228,"duration_ms":47,"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":1983259,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":10,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":1983259,"phase":"lean_module_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":24}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":10575,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 825230064660125861cba5ff3972606b529771e52c843f5d4500407d8ec59b82
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":554087,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-b)
exit_code=Some(0) duration_ms=2005720
stdout:
apx-semantic-phase {"duration_ms":29,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":0,"diagnostic_count":0,"duration_ms":32,"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":457295,"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":5,"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":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":510,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":10,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":510,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":471,"diagnostic_count":322,"duration_ms":51053,"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":532363,"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":97,"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":5,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":4207991,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":6,"diagnostic_count":0,"duration_ms":1768,"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":430572,"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":0,"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":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":11072,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":11072,"phase":"lean_module_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":27}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":10087,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 825230064660125861cba5ff3972606b529771e52c843f5d4500407d8ec59b82
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":35,"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":1994737,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r2)
exit_code=Some(0) duration_ms=1389423
stdout:
apx-semantic-phase {"duration_ms":19,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":136,"diagnostic_count":71,"duration_ms":10568,"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":423553,"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":28,"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":17,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":509774,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":69,"diagnostic_count":54,"duration_ms":5755,"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":418385,"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":36,"diagnostic_count":27,"duration_ms":2848,"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":419436,"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"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":24}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":11632,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 825230064660125861cba5ff3972606b529771e52c843f5d4500407d8ec59b82
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":59,"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":1376584,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r3)
exit_code=Some(0) duration_ms=1613308
stdout:
apx-semantic-phase {"duration_ms":21,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":792,"diagnostic_count":519,"duration_ms":96257,"module_name":"PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1","module_path":"PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":422384,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1","module_path":"PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":792,"diagnostic_count":519,"duration_ms":38,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1","module_path":"PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.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":5609028,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":7,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":5609028,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":57,"diagnostic_count":33,"duration_ms":3961,"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":432048,"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":4,"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":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":166420,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":166420,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":17,"diagnostic_count":10,"duration_ms":1444,"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":428791,"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":1,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":101503,"phase":"lean_module_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":24}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":14313,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 825230064660125861cba5ff3972606b529771e52c843f5d4500407d8ec59b82
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":53,"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":1597705,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r4)
exit_code=Some(0) duration_ms=1848861
stdout:
apx-semantic-phase {"duration_ms":7,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":128,"diagnostic_count":89,"duration_ms":9907,"module_name":"PrimeNumberTheoremAnd.IEANTN.Chebyshev","module_path":"PrimeNumberTheoremAnd/IEANTN/Chebyshev.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":435774,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Chebyshev","module_path":"PrimeNumberTheoremAnd/IEANTN/Chebyshev.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":128,"diagnostic_count":89,"duration_ms":12,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Chebyshev","module_path":"PrimeNumberTheoremAnd/IEANTN/Chebyshev.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":779360,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":2,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":779360,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":38,"diagnostic_count":28,"duration_ms":3012,"module_name":"PrimeNumberTheoremAnd.IEANTN.CostaPereira","module_path":"PrimeNumberTheoremAnd/IEANTN/CostaPereira.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":426168,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.CostaPereira","module_path":"PrimeNumberTheoremAnd/IEANTN/CostaPereira.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":38,"diagnostic_count":28,"duration_ms":2,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.CostaPereira","module_path":"PrimeNumberTheoremAnd/IEANTN/CostaPereira.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":311165,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":311165,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":368,"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":445988,"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":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":68407,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":1,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":68407,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":297,"diagnostic_count":259,"duration_ms":22809,"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":446927,"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":36,"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":29}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":19751,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 825230064660125861cba5ff3972606b529771e52c843f5d4500407d8ec59b82
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":1828414,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r5)
exit_code=Some(0) duration_ms=1819240
stdout:
apx-semantic-phase {"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":382,"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":439798,"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":1,"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":464,"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":441325,"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":374,"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":436869,"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":1,"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":427,"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":438679,"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":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":82759,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":1,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":82759,"phase":"lean_module_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":22}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":13004,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 825230064660125861cba5ff3972606b529771e52c843f5d4500407d8ec59b82
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":1804922,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r6)
exit_code=Some(0) duration_ms=1784907
stdout:
apx-semantic-phase {"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":458,"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":443433,"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":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":85603,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":0,"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":407,"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":434148,"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":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":87967,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":1,"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":428,"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":441283,"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":1,"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":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":90257,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":90257,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":429,"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":440112,"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":1,"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":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":92539,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":92539,"phase":"lean_module_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":18}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":17692,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 825230064660125861cba5ff3972606b529771e52c843f5d4500407d8ec59b82
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":57,"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":1766401,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r7)
exit_code=Some(0) duration_ms=1767954
stdout:
apx-semantic-phase {"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":476,"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":437931,"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":0,"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":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":94376,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":0,"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":450,"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":433358,"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":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":96327,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":1,"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":445,"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":439564,"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":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":101240,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":101240,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":426,"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":439425,"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":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":102723,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":102723,"phase":"lean_module_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":18}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":10710,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 825230064660125861cba5ff3972606b529771e52c843f5d4500407d8ec59b82
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":1756668,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r8)
exit_code=Some(0) duration_ms=1314313
stdout:
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":150,"diagnostic_count":101,"duration_ms":11335,"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":438017,"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":6,"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":466,"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":431940,"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":1,"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":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":107456,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":1,"module_index":1,"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":6,"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":416757,"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":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":502,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":502,"phase":"lean_module_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":10497,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 825230064660125861cba5ff3972606b529771e52c843f5d4500407d8ec59b82
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":1303241,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r9)
exit_code=Some(0) duration_ms=968684
stdout:
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":679,"diagnostic_count":493,"duration_ms":67373,"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":442817,"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":49,"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":2,"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":3407,"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":438698,"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":2,"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":0,"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":24}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":10700,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 825230064660125861cba5ff3972606b529771e52c843f5d4500407d8ec59b82
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":32,"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":957421,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r10)
exit_code=Some(0) duration_ms=910633
stdout:
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":32,"diagnostic_count":19,"duration_ms":1943,"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":437740,"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":3,"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":2,"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":21082,"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":434337,"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":22,"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":24}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":10002,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 825230064660125861cba5ff3972606b529771e52c843f5d4500407d8ec59b82
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":47,"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":899932,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r11)
exit_code=Some(0) duration_ms=451854
stdout:
apx-semantic-phase {"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":27,"diagnostic_count":9,"duration_ms":1758,"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":434831,"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":2,"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":3,"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":24}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":10113,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 825230064660125861cba5ff3972606b529771e52c843f5d4500407d8ec59b82
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":41,"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":441132,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r12)
exit_code=Some(0) duration_ms=452507
stdout:
apx-semantic-phase {"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":67,"diagnostic_count":53,"duration_ms":4744,"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":432373,"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":6,"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":1,"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":24}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":10166,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 825230064660125861cba5ff3972606b529771e52c843f5d4500407d8ec59b82
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":45,"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":441727,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r13)
exit_code=Some(0) duration_ms=448491
stdout:
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":70,"diagnostic_count":54,"duration_ms":4967,"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":428304,"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":3,"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":0,"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":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":10115,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 825230064660125861cba5ff3972606b529771e52c843f5d4500407d8ec59b82
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":44,"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":437806,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r14)
exit_code=Some(0) duration_ms=475805
stdout:
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":235,"diagnostic_count":164,"duration_ms":18785,"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":441893,"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":10,"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":20}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":10118,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 825230064660125861cba5ff3972606b529771e52c843f5d4500407d8ec59b82
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":45,"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":465172,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r15)
exit_code=Some(0) duration_ms=465858
stdout:
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":263,"diagnostic_count":178,"duration_ms":22270,"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":428257,"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":26,"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":24}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":10180,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 825230064660125861cba5ff3972606b529771e52c843f5d4500407d8ec59b82
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":43,"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":455070,"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-1043-source
Cloning into '/var/lib/apodeixis/repos/job-1043-source'...
git_checkout exit 128
git checkout 569325d78913d6ea9a39af78348644982e893ee8
fatal: reference is not a tree: 569325d78913d6ea9a39af78348644982e893ee8
git_checkout exit 0
git fetch --depth 1 origin 569325d78913d6ea9a39af78348644982e893ee8
From https://github.com/AlexKontorovich/PrimeNumberTheoremAnd * branch 569325d78913d6ea9a39af78348644982e893ee8 -> FETCH_HEAD
git_checkout exit 0
git checkout 569325d78913d6ea9a39af78348644982e893ee8 (after fetch)
Note: switching to '569325d78913d6ea9a39af78348644982e893ee8'. 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 569325d feat(Mertens): prove log_zeta_eq_sum via Euler product (#1582) (#1595)
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: 15 file(s) [attempted 15/8459 = 0%, 2 KB/s], Decompressed: 13 Downloaded: 36 file(s) [attempted 36/8459 = 0%, 15 KB/s], Decompressed: 35 Downloaded: 61 file(s) [attempted 61/8459 = 0%, 222 KB/s], Decompressed: 60 Downloaded: 82 file(s) [attempted 82/8459 = 0%, 608 KB/s], Decompressed: 77 Downloaded: 107 file(s) [attempted 107/8459 = 1%, 42 KB/s], Decompressed: 82 Downloaded: 138 file(s) [attempted 138/8459 = 1%, 68 KB/s], Decompressed: 82 Downloaded: 175 file(s) [attempted 175/8459 = 2%, 660 KB/s], Decompressed: 172 Downloaded: 207 file(s) [attempted 207/8459 = 2%, 50 KB/s], Decompressed: 203 Downloaded: 239 file(s) [attempted 239/8459 = 2%, 509 KB/s], Decompressed: 230 Downloaded: 268 file(s) [attempted 268/8459 = 3%, 364 KB/s], Decompressed: 264 Downloaded: 309 file(s) [attempted 309/8459 = 3%, 422 KB/s], Decompressed: 302 Downloaded: 348 file(s) [attempted 348/8459 = 4%, 636 KB/s], Decompressed: 343 Downloaded: 383 file(s) [attempted 383/8459 = 4%, 213 KB/s], Decompressed: 377 Downloaded: 408 file(s) [attempted 408/8459 = 4%, 222 KB/s], Decompressed: 405 Downloaded: 453 file(s) [attempted 453/8459 = 5%, 900 KB/s], Decompressed: 449 Downloaded: 497 file(s) [attempted 497/8459 = 5%, 86 KB/s], Decompressed: 456 Downloaded: 535 file(s) [attempted 535/8459 = 6%, 69 KB/s], Decompressed: 456 Downloaded: 569 file(s) [attempted 569/8459 = 6%, 155 KB/s], Decompressed: 549 Downloaded: 600 file(s) [attempted 600/8459 = 7%, 34 KB/s], Decompressed: 597 Downloaded: 647 file(s) [attempted 647/8459 = 7%, 173 KB/s], Decompressed: 641 Downloaded: 686 file(s) [attempted 686/8459 = 8%, 131 KB/s], Decompressed: 682 Downloaded: 723 file(s) [attempted 723/8459 = 8%, 304 KB/s], Decompressed: 713 Downloaded: 752 file(s) [attempted 752/8459 = 8%, 205 KB/s], Decompressed: 747 Downloaded: 795 file(s) [attempted 795/8459 = 9%, 522 KB/s], Decompressed: 782 Downloaded: 840 file(s) [attempted 840/8459 = 9%, 202 KB/s], Decompressed: 782 Downloaded: 878 file(s) [attempted 878/8459 = 10%, 66 KB/s], Decompressed: 788 Downloaded: 912 file(s) [attempted 912/8459 = 10%, 534 KB/s], Decompressed: 905 Downloaded: 946 file(s) [attempted 946/8459 = 11%, 276 KB/s], Decompressed: 943 Downloaded: 987 file(s) [attempted 987/8459 = 11%, 247 KB/s], Decompressed: 984 Downloaded: 1028 file(s) [attempted 1028/8459 = 12%, 293 KB/s], Decompressed: 1025 Downloaded: 1066 file(s) [attempted 1066/8459 = 12%, 244 KB/s], Decompressed: 1045 Downloaded: 1100 file(s) [attempted 1100/8459 = 13%, 72 KB/s], Decompressed: 1045 Downloaded: 1134 file(s) [attempted 1134/8459 = 13%, 164 KB/s], Decompressed: 1127 Downloaded: 1175 file(s) [attempted 1175/8459 = 13%, 137 KB/s], Decompressed: 1172 Downloaded: 1216 file(s) [attempted 1216/8459 = 14%, 93 KB/s], Decompressed: 1213 Downloaded: 1261 file(s) [attempted 1261/8459 = 14%, 181 KB/s], Decompressed: 1254 Downloaded: 1295 file(s) [attempted 1295/8459 = 15%, 228 KB/s], Decompressed: 1285 Downloaded: 1333 file(s) [attempted 1333/8459 = 15%, 49 KB/s], Decompressed: 1329 Downloaded: 1374 file(s) [attempted 1374/8459 = 16%, 150 KB/s], Decompressed: 1367 Downloaded: 1415 file(s) [attempted 1415/8459 = 16%, 374 KB/s], Decompressed: 1412 Downloaded: 1450 file(s) [attempted 1450/8459 = 17%, 676 KB/s], Decompressed: 1442 Downloaded: 1487 file(s) [attempted 1487/8459 = 17%, 62 KB/s], Decompressed: 1483 Downloaded: 1524 file(s) [attempted 1524/8459 = 18%, 394 KB/s], Decompressed: 1521 Downloaded: 1566 file(s) [attempted 1566/8459 = 18%, 1012 KB/s], Decompressed: 1562 Downloaded: 1608 file(s) [attempted 1608/8459 = 19%, 55 KB/s], Decompressed: 1603 Downloaded: 1641 file(s) [attempted 1641/8459 = 19%, 631 KB/s], Decompressed: 1631 Downloaded: 1678 file(s) [attempted 1678/8459 = 19%, 149 KB/s], Decompressed: 1672 Downloaded: 1718 file(s) [attempted 1718/8459 = 20%, 252 KB/s], Decompressed: 1713 Downloaded: 1757 file(s) [attempted 1757/8459 = 20%, 338 KB/s], Decompressed: 1750 Downloaded: 1795 file(s) [attempted 1795/8459 = 21%, 263 KB/s], Decompressed: 1791 Downloaded: 1836 file(s) [attempted 1836/8459 = 21%, 638 KB/s], Decompressed: 1829 Downloaded: 1874 file(s) [attempted 1874/8459 = 22%, 283 KB/s], Decompressed: 1867 Downloaded: 1910 file(s) [attempted 1910/8459 = 22%, 134 KB/s], Decompressed: 1887 Downloaded: 1949 file(s) [attempted 1949/8459 = 23%, 728 KB/s], Decompressed: 1942 Downloaded: 1980 file(s) [attempted 1980/8459 = 23%, 130 KB/s], Decompressed: 1976 Downloaded: 2015 file(s) [attempted 2015/8459 = 23%, 287 KB/s], Decompressed: 2010 Downloaded: 2055 file(s) [attempted 2055/8459 = 24%, 41 KB/s], Decompressed: 2052 Downloaded: 2099 file(s) [attempted 2099/8459 = 24%, 290 KB/s], Decompressed: 2089 Downloaded: 2130 file(s) [attempted 2130/8459 = 25%, 1251 KB/s], Decompressed: 2127 Downloaded: 2171 file(s) [attempted 2171/8459 = 25%, 51 KB/s], Decompressed: 2164 Downloaded: 2209 file(s) [attempted 2209/8459 = 26%, 223 KB/s], Decompressed: 2206 Downloaded: 2253 file(s) [attempted 2253/8459 = 26%, 647 KB/s], Decompressed: 2250 Downloaded: 2298 file(s) [attempted 2298/8459 = 27%, 198 KB/s], Decompressed: 2291 Downloaded: 2332 file(s) [attempted 2332/8459 = 27%, 86 KB/s], Decompressed: 2329 Downloaded: 2373 file(s) [attempted 2373/8459 = 28%, 230 KB/s], Decompressed: 2366 Downloaded: 2407 file(s) [attempted 2407/8459 = 28%, 290 KB/s], Decompressed: 2401 Downloaded: 2449 file(s) [attempted 2449/8459 = 28%, 92 KB/s], Decompressed: 2445 Downloaded: 2487 file(s) [attempted 2487/8459 = 29%, 181 KB/s], Decompressed: 2483 Downloaded: 2525 file(s) [attempted 2525/8459 = 29%, 257 KB/s], Decompressed: 2517 Downloaded: 2561 file(s) [attempted 2561/8459 = 30%, 1269 KB/s], Decompressed: 2558 Downloaded: 2599 file(s) [attempted 2599/8459 = 30%, 102 KB/s], Decompressed: 2596 Downloaded: 2640 file(s) [attempted 2640/8459 = 31%, 146 KB/s], Decompressed: 2637 Downloaded: 2681 file(s) [attempted 2681/8459 = 31%, 504 KB/s], Decompressed: 2674 Downloaded: 2722 file(s) [attempted 2722/8459 = 32%, 489 KB/s], Decompressed: 2719 Downloaded: 2760 file(s) [attempted 2760/8459 = 32%, 1097 KB/s], Decompressed: 2757 Downloaded: 2796 file(s) [attempted 2796/8459 = 33%, 146 KB/s], Decompressed: 2791 Downloaded: 2839 file(s) [attempted 2839/8459 = 33%, 100 KB/s], Decompressed: 2835 Downloaded: 2876 file(s) [attempted 2876/8459 = 33%, 58 KB/s], Decompressed: 2873 Downloaded: 2917 file(s) [attempted 2917/8459 = 34%, 117 KB/s], Decompressed: 2914 Downloaded: 2948 file(s) [attempted 2948/8459 = 34%, 223 KB/s], Decompressed: 2945 Downloaded: 2987 file(s) [attempted 2987/8459 = 35%, 408 KB/s], Decompressed: 2982 Downloaded: 3030 file(s) [attempted 3030/8459 = 35%, 820 KB/s], Decompressed: 3027 Downloaded: 3062 file(s) [attempted 3062/8459 = 36%, 1090 KB/s], Decompressed: 3058 Downloaded: 3102 file(s) [attempted 3102/8459 = 36%, 444 KB/s], Decompressed: 3095 Downloaded: 3140 file(s) [attempted 3140/8459 = 37%, 49 KB/s], Decompressed: 3136 Downloaded: 3184 file(s) [attempted 3184/8459 = 37%, 749 KB/s], Decompressed: 3177 Downloaded: 3232 file(s) [attempted 3232/8459 = 38%, 1040 KB/s], Decompressed: 3229 Downloaded: 3270 file(s) [attempted 3270/8459 = 38%, 541 KB/s], Decompressed: 3260 Downloaded: 3304 file(s) [attempted 3304/8459 = 39%, 103 KB/s], Decompressed: 3301 Downloaded: 3342 file(s) [attempted 3342/8459 = 39%, 552 KB/s], Decompressed: 3335 Downloaded: 3383 file(s) [attempted 3383/8459 = 39%, 416 KB/s], Decompressed: 3379 Downloaded: 3427 file(s) [attempted 3427/8459 = 40%, 172 KB/s], Decompressed: 3420 Downloaded: 3465 file(s) [attempted 3465/8459 = 40%, 567 KB/s], Decompressed: 3462 Downloaded: 3505 file(s) [attempted 3505/8459 = 41%, 156 KB/s], Decompressed: 3499 Downloaded: 3533 file(s) [attempted 3533/8459 = 41%, 99 KB/s], Decompressed: 3523 Downloaded: 3578 file(s) [attempted 3578/8459 = 42%, 144 KB/s], Decompressed: 3574 Downloaded: 3619 file(s) [attempted 3619/8459 = 42%, 534 KB/s], Decompressed: 3616 Downloaded: 3660 file(s) [attempted 3660/8459 = 43%, 393 KB/s], Decompressed: 3657 Downloaded: 3694 file(s) [attempted 3694/8459 = 43%, 51 KB/s], Decompressed: 3687 Downloaded: 3728 file(s) [attempted 3728/8459 = 44%, 713 KB/s], Decompressed: 3725 Downloaded: 3770 file(s) [attempted 3770/8459 = 44%, 129 KB/s], Decompressed: 3759 Downloaded: 3807 file(s) [attempted 3807/8459 = 45%, 326 KB/s], Decompressed: 3804 Downloaded: 3841 file(s) [attempted 3841/8459 = 45%, 152 KB/s], Decompressed: 3838 Downloaded: 3876 file(s) [attempted 3876/8459 = 45%, 82 KB/s], Decompressed: 3872 Downloaded: 3917 file(s) [attempted 3917/8459 = 46%, 2269 KB/s], Decompressed: 3913 Downloaded: 3955 file(s) [attempted 3955/8459 = 46%, 88 KB/s], Decompressed: 3948 Downloaded: 3992 file(s) [attempted 3992/8459 = 47%, 121 KB/s], Decompressed: 3985 Downloaded: 4023 file(s) [attempted 4023/8459 = 47%, 1374 KB/s], Decompressed: 3985 Downloaded: 4060 file(s) [attempted 4060/8459 = 47%, 251 KB/s], Decompressed: 3985 Downloaded: 4098 file(s) [attempted 4098/8459 = 48%, 164 KB/s], Decompressed: 4095 Downloaded: 4139 file(s) [attempted 4139/8459 = 48%, 76 KB/s], Decompressed: 4132 Downloaded: 4173 file(s) [attempted 4173/8459 = 49%, 23 KB/s], Decompressed: 4170 Downloaded: 4211 file(s) [attempted 4211/8459 = 49%, 896 KB/s], Decompressed: 4208 Downloaded: 4249 file(s) [attempted 4249/8459 = 50%, 86 KB/s], Decompressed: 4245 Downloaded: 4287 file(s) [attempted 4287/8459 = 50%, 378 KB/s], Decompressed: 4283 Downloaded: 4317 file(s) [attempted 4317/8459 = 51%, 282 KB/s], Decompressed: 4314 Downloaded: 4358 file(s) [attempted 4358/8459 = 51%, 284 KB/s], Decompressed: 4355 Downloaded: 4399 file(s) [attempted 4399/8459 = 52%, 565 KB/s], Decompressed: 4396 Downloaded: 4440 file(s) [attempted 4440/8459 = 52%, 149 KB/s], Decompressed: 4437 Downloaded: 4471 file(s) [attempted 4471/8459 = 52%, 343 KB/s], Decompressed: 4464 Downloaded: 4512 file(s) [attempted 4512/8459 = 53%, 279 KB/s], Decompressed: 4509 Downloaded: 4557 file(s) [attempted 4557/8459 = 53%, 168 KB/s], Decompressed: 4553 Downloaded: 4594 file(s) [attempted 4594/8459 = 54%, 578 KB/s], Decompressed: 4591 Downloaded: 4637 file(s) [attempted 4637/8459 = 54%, 64 KB/s], Decompressed: 4629 Downloaded: 4666 file(s) [attempted 4666/8459 = 55%, 106 KB/s], Decompressed: 4663 Downloaded: 4711 file(s) [attempted 4711/8459 = 55%, 138 KB/s], Decompressed: 4704 Downloaded: 4748 file(s) [attempted 4748/8459 = 56%, 360 KB/s], Decompressed: 4745 Downloaded: 4789 file(s) [attempted 4789/8459 = 56%, 332 KB/s], Decompressed: 4783 Downloaded: 4827 file(s) [attempted 4827/8459 = 57%, 188 KB/s], Decompressed: 4820 Downloaded: 4865 file(s) [attempted 4865/8459 = 57%, 335 KB/s], Decompressed: 4858 Downloaded: 4902 file(s) [attempted 4902/8459 = 57%, 59 KB/s], Decompressed: 4899 Downloaded: 4943 file(s) [attempted 4943/8459 = 58%, 55 KB/s], Decompressed: 4940 Downloaded: 4985 file(s) [attempted 4985/8459 = 58%, 63 KB/s], Decompressed: 4981 Downloaded: 5026 file(s) [attempted 5026/8459 = 59%, 319 KB/s], Decompressed: 5022 Downloaded: 5060 file(s) [attempted 5060/8459 = 59%, 199 KB/s], Decompressed: 5056 Downloaded: 5101 file(s) [attempted 5101/8459 = 60%, 357 KB/s], Decompressed: 5097 Downloaded: 5137 file(s) [attempted 5137/8459 = 60%, 37 KB/s], Decompressed: 5132 Downloaded: 5183 file(s) [attempted 5183/8459 = 61%, 80 KB/s], Decompressed: 5176 Downloaded: 5221 file(s) [attempted 5221/8459 = 61%, 93 KB/s], Decompressed: 5217 Downloaded: 5255 file(s) [attempted 5255/8459 = 62%, 87 KB/s], Decompressed: 5252 Downloaded: 5296 file(s) [attempted 5296/8459 = 62%, 67 KB/s], Decompressed: 5286 Downloaded: 5337 file(s) [attempted 5337/8459 = 63%, 121 KB/s], Decompressed: 5334 Downloaded: 5378 file(s) [attempted 5378/8459 = 63%, 306 KB/s], Decompressed: 5371 Downloaded: 5412 file(s) [attempted 5412/8459 = 63%, 446 KB/s], Decompressed: 5406 Downloaded: 5453 file(s) [attempted 5453/8459 = 64%, 259 KB/s], Decompressed: 5447 Downloaded: 5491 file(s) [attempted 5491/8459 = 64%, 182 KB/s], Decompressed: 5488 Downloaded: 5536 file(s) [attempted 5536/8459 = 65%, 224 KB/s], Decompressed: 5532 Downloaded: 5580 file(s) [attempted 5580/8459 = 65%, 37 KB/s], Decompressed: 5573 Downloaded: 5611 file(s) [attempted 5611/8459 = 66%, 250 KB/s], Decompressed: 5580 Downloaded: 5652 file(s) [attempted 5652/8459 = 66%, 49 KB/s], Decompressed: 5580 Downloaded: 5690 file(s) [attempted 5690/8459 = 67%, 527 KB/s], Decompressed: 5686 Downloaded: 5734 file(s) [attempted 5734/8459 = 67%, 297 KB/s], Decompressed: 5731 Downloaded: 5774 file(s) [attempted 5774/8459 = 68%, 570 KB/s], Decompressed: 5765 Downloaded: 5806 file(s) [attempted 5806/8459 = 68%, 113 KB/s], Decompressed: 5803 Downloaded: 5844 file(s) [attempted 5844/8459 = 69%, 41 KB/s], Decompressed: 5840 Downloaded: 5888 file(s) [attempted 5888/8459 = 69%, 240 KB/s], Decompressed: 5885 Downloaded: 5933 file(s) [attempted 5933/8459 = 70%, 147 KB/s], Decompressed: 5929 Downloaded: 5968 file(s) [attempted 5968/8459 = 70%, 417 KB/s], Decompressed: 5963 Downloaded: 6001 file(s) [attempted 6001/8459 = 70%, 235 KB/s], Decompressed: 5998 Downloaded: 6042 file(s) [attempted 6042/8459 = 71%, 19 KB/s], Decompressed: 6039 Downloaded: 6083 file(s) [attempted 6083/8459 = 71%, 133 KB/s], Decompressed: 6080 Downloaded: 6123 file(s) [attempted 6123/8459 = 72%, 868 KB/s], Decompressed: 6114 Downloaded: 6155 file(s) [attempted 6155/8459 = 72%, 346 KB/s], Decompressed: 6148 Downloaded: 6196 file(s) [attempted 6196/8459 = 73%, 311 KB/s], Decompressed: 6193 Downloaded: 6244 file(s) [attempted 6244/8459 = 73%, 31 KB/s], Decompressed: 6237 Downloaded: 6285 file(s) [attempted 6285/8459 = 74%, 372 KB/s], Decompressed: 6237 Downloaded: 6326 file(s) [attempted 6326/8459 = 74%, 105 KB/s], Decompressed: 6237 Downloaded: 6357 file(s) [attempted 6357/8459 = 75%, 785 KB/s], Decompressed: 6347 Downloaded: 6395 file(s) [attempted 6395/8459 = 75%, 345 KB/s], Decompressed: 6388 Downloaded: 6436 file(s) [attempted 6436/8459 = 76%, 114 KB/s], Decompressed: 6432 Downloaded: 6480 file(s) [attempted 6480/8459 = 76%, 160 KB/s], Decompressed: 6463 Downloaded: 6514 file(s) [attempted 6514/8459 = 77%, 441 KB/s], Decompressed: 6463 Downloaded: 6549 file(s) [attempted 6549/8459 = 77%, 486 KB/s], Decompressed: 6466 Downloaded: 6590 file(s) [attempted 6590/8459 = 77%, 75 KB/s], Decompressed: 6583 Downloaded: 6627 file(s) [attempted 6627/8459 = 78%, 101 KB/s], Decompressed: 6624 Downloaded: 6665 file(s) [attempted 6665/8459 = 78%, 74 KB/s], Decompressed: 6658 Downloaded: 6703 file(s) [attempted 6703/8459 = 79%, 230 KB/s], Decompressed: 6699 Downloaded: 6743 file(s) [attempted 6743/8459 = 79%, 62 KB/s], Decompressed: 6733 Downloaded: 6778 file(s) [attempted 6778/8459 = 80%, 550 KB/s], Decompressed: 6771 Downloaded: 6812 file(s) [attempted 6812/8459 = 80%, 594 KB/s], Decompressed: 6809 Downloaded: 6852 file(s) [attempted 6852/8459 = 81%, 297 KB/s], Decompressed: 6846 Downloaded: 6891 file(s) [attempted 6891/8459 = 81%, 256 KB/s], Decompressed: 6887 Downloaded: 6928 file(s) [attempted 6928/8459 = 81%, 245 KB/s], Decompressed: 6925 Downloaded: 6967 file(s) [attempted 6967/8459 = 82%, 40 KB/s], Decompressed: 6959 Downloaded: 7005 file(s) [attempted 7005/8459 = 82%, 265 KB/s], Decompressed: 7000 Downloaded: 7041 file(s) [attempted 7041/8459 = 83%, 141 KB/s], Decompressed: 7035 Downloaded: 7082 file(s) [attempted 7082/8459 = 83%, 788 KB/s], Decompressed: 7079 Downloaded: 7124 file(s) [attempted 7124/8459 = 84%, 112 KB/s], Decompressed: 7117 Downloaded: 7158 file(s) [attempted 7158/8459 = 84%, 221 KB/s], Decompressed: 7154 Downloaded: 7199 file(s) [attempted 7199/8459 = 85%, 85 KB/s], Decompressed: 7189 Downloaded: 7233 file(s) [attempted 7233/8459 = 85%, 852 KB/s], Decompressed: 7226 Downloaded: 7274 file(s) [attempted 7274/8459 = 85%, 217 KB/s], Decompressed: 7271 Downloaded: 7315 file(s) [attempted 7315/8459 = 86%, 1084 KB/s], Decompressed: 7271 Downloaded: 7349 file(s) [attempted 7349/8459 = 86%, 47 KB/s], Decompressed: 7271 Downloaded: 7384 file(s) [attempted 7384/8459 = 87%, 550 KB/s], Decompressed: 7380 Downloaded: 7428 file(s) [attempted 7428/8459 = 87%, 561 KB/s], Decompressed: 7421 Downloaded: 7473 file(s) [attempted 7473/8459 = 88%, 91 KB/s], Decompressed: 7449 Downloaded: 7507 file(s) [attempted 7507/8459 = 88%, 78 KB/s], Decompressed: 7449 Downloaded: 7538 file(s) [attempted 7538/8459 = 89%, 503 KB/s], Decompressed: 7452 Downloaded: 7579 file(s) [attempted 7579/8459 = 89%, 1383 KB/s], Decompressed: 7575 Downloaded: 7622 file(s) [attempted 7622/8459 = 90%, 156 KB/s], Decompressed: 7613 Downloaded: 7654 file(s) [attempted 7654/8459 = 90%, 452 KB/s], Decompressed: 7647 Downloaded: 7682 file(s) [attempted 7682/8459 = 90%, 48 KB/s], Decompressed: 7675 Downloaded: 7722 file(s) [attempted 7722/8459 = 91%, 33 KB/s], Decompressed: 7719 Downloaded: 7764 file(s) [attempted 7764/8459 = 91%, 95 KB/s], Decompressed: 7757 Downloaded: 7801 file(s) [attempted 7801/8459 = 92%, 713 KB/s], Decompressed: 7791 Downloaded: 7830 file(s) [attempted 7830/8459 = 92%, 274 KB/s], Decompressed: 7825 Downloaded: 7870 file(s) [attempted 7870/8459 = 93%, 201 KB/s], Decompressed: 7866 Downloaded: 7907 file(s) [attempted 7907/8459 = 93%, 568 KB/s], Decompressed: 7904 Downloaded: 7950 file(s) [attempted 7950/8459 = 93%, 33 KB/s], Decompressed: 7945 Downloaded: 7979 file(s) [attempted 7979/8459 = 94%, 1849 KB/s], Decompressed: 7976 Downloaded: 8020 file(s) [attempted 8020/8459 = 94%, 43 KB/s], Decompressed: 8017 Downloaded: 8058 file(s) [attempted 8058/8459 = 95%, 62 KB/s], Decompressed: 8054 Downloaded: 8099 file(s) [attempted 8099/8459 = 95%, 668 KB/s], Decompressed: 8095 Downloaded: 8137 file(s) [attempted 8137/8459 = 96%, 298 KB/s], Decompressed: 8126 Downloaded: 8174 file(s) [attempted 8174/8459 = 96%, 1046 KB/s], Decompressed: 8171 Downloaded: 8212 file(s) [attempted 8212/8459 = 97%, 86 KB/s], Decompressed: 8208 Downloaded: 8250 file(s) [attempted 8250/8459 = 97%, 292 KB/s], Decompressed: 8246 Downloaded: 8291 file(s) [attempted 8291/8459 = 98%, 434 KB/s], Decompressed: 8287 Downloaded: 8327 file(s) [attempted 8327/8459 = 98%, 182 KB/s], Decompressed: 8318 Downloaded: 8362 file(s) [attempted 8362/8459 = 98%, 875 KB/s], Decompressed: 8359 Downloaded: 8400 file(s) [attempted 8400/8459 = 99%, 49 KB/s], Decompressed: 8397 Downloaded: 8445 file(s) [attempted 8445/8459 = 99%, 819 KB/s], Decompressed: 8441 Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 819 KB/s], Decompressed: 8451
lean_checker exit 0
lake build
✔ [3472/3478] Built PrimeNumberTheoremAnd.ResidueCalcOnRectangles (76s)
✔ [3477/3499] Built PrimeNumberTheoremAnd.ZetaBounds (51s)
ℹ [3534/3544] Built PrimeNumberTheoremAnd.MediumPNT (36s)
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3550/3566] Built PrimeNumberTheoremAnd.Backlund.ZeroCountCrude (27s)
⚠ [3563/3571] Built PrimeNumberTheoremAnd.StrongPNT (15s)
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1475:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1524:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1641:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:1786:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2181:6: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/StrongPNT.lean:2271:6: declaration uses `sorry`
✔ [3566/3573] Built PrimeNumberTheoremAnd.BorelCaratheodory (4.6s)
⚠ [3694/3710] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
✔ [3807/3818] Built PrimeNumberTheoremAnd.GeneralMeromorphic (2.9s)
⚠ [3811/3818] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3817/3823] Built PrimeNumberTheoremAnd.IEANTN.Mertens (20s)
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1305:16: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1331:16: declaration uses `sorry`
⚠ [3880/3890] Built PrimeNumberTheoremAnd.IEANTN.ZetaAppendix (66s)
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2577:8: `simp [v, Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2578:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2599:8: `simp [v', Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2600:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2817:8: `simp [v, Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2818:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2833:8: `simp [v', Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2834:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2963:4: `simp [W]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2964:4: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3069:4: `simp [p]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3070:4: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3084:4: `simp [Set.uIcc_of_le hab]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3084:4: Try this:
[apply] simp only [_root_.deriv_ofReal]
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3085:4: `fun_prop` uses `⊢`!
⚠ [3881/3892] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
⚠ [3883/3893] Built PrimeNumberTheoremAnd.IEANTN.ZetaSummary (33s)
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 (3.8s)
✔ [3890/3895] Built PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions (10s)
⚠ [3891/3895] Built PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky (7.2s)
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/3903] Built PrimeNumberTheoremAnd.IEANTN.CostaPereira (9.7s)
⚠ [4017/4025] 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/4026] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app (18s)
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 (17s)
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
⚠ [4023/4057] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW (40s)
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 (29s)
✔ [4036/4061] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core (17s)
✔ [4038/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_65_85 (24s)
✔ [4039/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_misc (19s)
✔ [4040/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_12600_24000 (89s)
✔ [4041/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_10600_12500 (121s)
✔ [4042/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_8600_10500 (68s)
✔ [4043/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_6600_8500 (68s)
✔ [4044/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4900_6500 (66s)
✔ [4045/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4400_4875 (73s)
✔ [4046/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3900_4375 (73s)
✔ [4047/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3400_3875 (75s)
✔ [4048/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2900_3375 (76s)
✔ [4049/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2400_2875 (80s)
✔ [4050/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_1900_2375 (81s)
✔ [4051/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_100_1875 (75s)
✔ [4052/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_90_95 (30s)
✔ [4053/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_values (12s)
✔ [4054/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_next (21s)
ℹ [4055/4068] Built PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 (70s)
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 (46s)
✔ [4059/4072] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_20_43 (80s)
⚠ [4060/4074] Built PrimeNumberTheoremAnd.IEANTN.CH2.CH2 (42s)
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2634:8: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2723: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:3093: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:3685:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3699:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3713:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3725:8: declaration uses `sorry`
⚠ [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 (53s)
✔ [4066/4074] Built PrimeNumberTheoremAnd.IEANTN.Chebyshev (29s)
⚠ [4067/4074] Built PrimeNumberTheoremAnd.IEANTN.Dusart (21s)
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 (6.4s)
⚠ [4072/4074] Built PrimeNumberTheoremAnd.IEANTN.FKS2 (77s)
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/4082] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_dispatch (70s)
✔ [4087/4109] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtCore (21s)
✔ [4091/4109] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_13 (14s)
✔ [4092/4110] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_12 (22s)
✔ [4093/4110] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_11 (22s)
✔ [4094/4110] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_10 (22s)
✔ [4095/4110] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_09 (22s)
✔ [4096/4110] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_08 (22s)
✔ [4097/4110] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_07 (22s)
✔ [4098/4110] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_06 (23s)
✔ [4099/4110] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_05 (22s)
✔ [4100/4110] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_04 (22s)
✔ [4101/4110] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_03 (22s)
✔ [4102/4110] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_02 (22s)
✔ [4103/4110] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_01 (21s)
✔ [4104/4110] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_00 (22s)
⚠ [4108/4112] Built PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext (4.1s)
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean:116:8: declaration uses `sorry`
⚠ [4110/4126] Built PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor (7.4s)
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`
⚠ [4120/4130] Built PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting (13s)
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 (10s)
⚠ [4127/4166] Built PrimeNumberTheoremAnd.IEANTN.TMEEMT (15s)
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`
⚠ [4146/4188] Built PrimeNumberTheoremAnd.IEANTN.SecondarySummary (10s)
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/4188] 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/4188] 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/4188] Built PrimeNumberTheoremAnd.IEANTN.MobiusLemma (13s)
⚠ [4161/4188] Built PrimeNumberTheoremAnd.IEANTN.Goldbach (6.7s)
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
✔ [4168/4188] Built PrimeNumberTheoremAnd.LaplaceInversion (12s)
✔ [4169/4188] Built PrimeNumberTheoremAnd.IEANTN.Lcm (29s)
✔ [4170/4188] Built PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan (56s)
✔ [4171/4188] Built PrimeNumberTheoremAnd.PerronFormula (8.1s)
✔ [4172/4188] Built PrimeNumberTheoremAnd.IEANTN.PrimarySummary (2.8s)
⚠ [4186/4188] Built PrimeNumberTheoremAnd.IEANTN.Kadiri (16s)
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:133:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:170:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:207:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:278:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:326:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:358:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1305:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1392:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1475:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2705:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2731:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:3337:8: declaration uses `sorry`
✔ [4187/4188] Built PrimeNumberTheoremAnd (5.0s)
Build completed successfully (4188 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)
✔ [25/35] Built Cli.Basic:c.o (3.1s)
✔ [30/35] Built Cli.Extensions:c.o (558ms)
✔ [33/39] Built Cli:c.o (66ms)
✔ [3507/3519] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.ResidueCalcOnRectangles:blueprint (29s)
✔ [3512/3549] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.ZetaBounds:blueprint (71s)
ℹ [3593/3610] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3597/3612] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.MediumPNT:blueprint (65s)
✔ [3614/3637] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Backlund.ZeroCountCrude:blueprint (3.6s)
⚠ [3624/3642] 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`
✔ [3630/3642] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.StrongPNT:blueprint (49s)
✔ [3636/3647] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.BorelCaratheodory:blueprint (6.9s)
⚠ [3765/3783] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
⚠ [3885/3900] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
✔ [3887/3901] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.GeneralMeromorphic:blueprint (3.1s)
⚠ [3896/3901] Replayed PrimeNumberTheoremAnd.IEANTN.Mertens
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1305:16: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:1331:16: declaration uses `sorry`
✔ [3899/3910] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Mertens:blueprint (47s)
⚠ [3958/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 (29s)
⚠ [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.8s)
✔ [3981/3990] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions:blueprint (3.2s)
⚠ [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 (11s)
✔ [3988/3996] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CostaPereira:blueprint (6.0s)
⚠ [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`
✔ [4108/4122] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Buthe:blueprint (6.6s)
⚠ [4112/4126] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
⚠ [4115/4126] Replayed PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:47:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:168:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:516:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1127:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1180:8: declaration uses `sorry`
✔ [4119/4178] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime:blueprint (22s)
✔ [4120/4178] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app:blueprint (21s)
⚠ [4122/4178] Replayed PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:1518:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:2184:8: declaration uses `sorry`
✔ [4125/4181] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW:blueprint (24s)
✔ [4136/4198] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_a2_bounds:blueprint (5.7s)
✔ [4139/4200] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core:blueprint (4.3s)
ℹ [4154/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 (52s)
✔ [4162/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_next:blueprint (3.3s)
✔ [4163/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_values:blueprint (3.4s)
✔ [4165/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_65_85:blueprint (4.3s)
✔ [4166/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_90_95:blueprint (3.3s)
✔ [4167/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_100_1875:blueprint (3.4s)
✔ [4168/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_1900_2375:blueprint (3.5s)
✔ [4169/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2400_2875:blueprint (3.5s)
✔ [4170/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2900_3375:blueprint (3.9s)
✔ [4171/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3400_3875:blueprint (3.5s)
✔ [4172/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3900_4375:blueprint (3.7s)
✔ [4173/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4400_4875:blueprint (4.1s)
✔ [4174/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4900_6500:blueprint (3.9s)
✔ [4175/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_6600_8500:blueprint (3.4s)
✔ [4176/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_8600_10500:blueprint (3.5s)
✔ [4177/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_10600_12500:blueprint (3.4s)
✔ [4178/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_12600_24000:blueprint (3.4s)
✔ [4179/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_misc:blueprint (3.3s)
⚠ [4180/4206] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2634:8: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2723: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:3093: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:3685:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3699:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3713:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3725:8: declaration uses `sorry`
✔ [4182/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimeInInterval:blueprint (5.1s)
⚠ [4184/4206] Replayed PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:85:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:129:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:304:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:449:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/eSHP/eSHP.lean:464:8: declaration uses `sorry`
✔ [4187/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_20_43:blueprint (71s)
✔ [4189/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CH2.CH2:blueprint (21s)
⚠ [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.Chebyshev:blueprint (37s)
✔ [4196/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Dusart:blueprint (46s)
✔ [4197/4206] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_44_59:blueprint (4.8s)
⚠ [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/4211] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows:blueprint (26s)
✔ [4203/4211] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2:blueprint (34s)
✔ [4206/4212] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_dispatch:blueprint (25s)
✔ [4220/4260] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtCore:blueprint (59s)
✔ [4238/4261] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_00:blueprint (3.3s)
✔ [4239/4261] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_01:blueprint (3.3s)
✔ [4240/4261] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_02:blueprint (3.3s)
✔ [4241/4261] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_03:blueprint (3.3s)
✔ [4242/4261] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_04:blueprint (3.2s)
✔ [4243/4261] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_05:blueprint (3.2s)
✔ [4244/4261] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_06:blueprint (3.3s)
✔ [4245/4261] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_07:blueprint (3.4s)
✔ [4246/4261] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_08:blueprint (3.3s)
✔ [4247/4261] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_09:blueprint (3.4s)
✔ [4248/4261] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_10:blueprint (3.3s)
✔ [4249/4261] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_11:blueprint (3.4s)
✔ [4250/4261] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_12:blueprint (3.4s)
✔ [4251/4261] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4ExtData_13:blueprint (4.9s)
⚠ [4252/4261] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext
warning: PrimeNumberTheoremAnd/IEANTN/FKS2Tables/Table4Ext.lean:116:8: declaration uses `sorry`
✔ [4257/4263] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Tables.Table4Ext:blueprint (3.3s)
⚠ [4258/4263] 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`
✔ [4260/4271] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2Floor.Cor22Floor:blueprint (12s)
⚠ [4269/4288] 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`
✔ [4272/4288] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting:blueprint (4.7s)
✔ [4287/4387] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower:blueprint (4.0s)
⚠ [4288/4387] 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`
✔ [4313/4397] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.TMEEMT:blueprint (47s)
⚠ [4314/4397] 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/4397] 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/4397] 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`
✔ [4332/4397] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondarySummary:blueprint (7.6s)
⚠ [4333/4397] 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/4397] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.MobiusLemma:blueprint (11s)
✔ [4356/4397] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Goldbach:blueprint (6.6s)
✔ [4364/4397] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.LaplaceInversion:blueprint (2.8s)
✔ [4365/4397] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Lcm:blueprint (12s)
✔ [4366/4397] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan:blueprint (16s)
✔ [4367/4397] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.PerronFormula:blueprint (22s)
✔ [4390/4397] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimarySummary:blueprint (3.2s)
⚠ [4392/4397] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:133:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:170:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:207:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:278:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:326:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:358:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1305:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1392:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:1475:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2705:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2731:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:3337:8: declaration uses `sorry`
✔ [4393/4397] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Kadiri:blueprint (47s)
✔ [4395/4397] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (25s)
ℹ [4396/4397] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (506ms)
info: Blueprint indexing
Build completed successfully (4398 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":21,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":353,"diagnostic_count":228,"duration_ms":31801,"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":426691,"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":353,"diagnostic_count":228,"duration_ms":47,"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":1983259,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":10,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":1983259,"phase":"lean_module_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":24}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":10575,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 825230064660125861cba5ff3972606b529771e52c843f5d4500407d8ec59b82
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":554087,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-b)
apx-semantic-phase {"duration_ms":29,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":0,"diagnostic_count":0,"duration_ms":32,"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":457295,"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":5,"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":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":510,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":10,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":510,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":471,"diagnostic_count":322,"duration_ms":51053,"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":532363,"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":97,"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":5,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":4207991,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":6,"diagnostic_count":0,"duration_ms":1768,"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":430572,"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":0,"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":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":11072,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":11072,"phase":"lean_module_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":27}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":10087,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 825230064660125861cba5ff3972606b529771e52c843f5d4500407d8ec59b82
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":35,"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":1994737,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r2)
apx-semantic-phase {"duration_ms":19,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":136,"diagnostic_count":71,"duration_ms":10568,"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":423553,"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":28,"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":17,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":509774,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":69,"diagnostic_count":54,"duration_ms":5755,"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":418385,"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":36,"diagnostic_count":27,"duration_ms":2848,"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":419436,"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 {"phase":"core_compile","duration_ms":24}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":11632,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 825230064660125861cba5ff3972606b529771e52c843f5d4500407d8ec59b82
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":59,"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":1376584,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r3)
apx-semantic-phase {"duration_ms":21,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":792,"diagnostic_count":519,"duration_ms":96257,"module_name":"PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1","module_path":"PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":422384,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1","module_path":"PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":792,"diagnostic_count":519,"duration_ms":38,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1","module_path":"PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.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":5609028,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":7,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":5609028,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":57,"diagnostic_count":33,"duration_ms":3961,"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":432048,"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":4,"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":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":166420,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":166420,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":17,"diagnostic_count":10,"duration_ms":1444,"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":428791,"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":1,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":101503,"phase":"lean_module_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":24}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":14313,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 825230064660125861cba5ff3972606b529771e52c843f5d4500407d8ec59b82
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":53,"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":1597705,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r4)
apx-semantic-phase {"duration_ms":7,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":128,"diagnostic_count":89,"duration_ms":9907,"module_name":"PrimeNumberTheoremAnd.IEANTN.Chebyshev","module_path":"PrimeNumberTheoremAnd/IEANTN/Chebyshev.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":435774,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Chebyshev","module_path":"PrimeNumberTheoremAnd/IEANTN/Chebyshev.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":128,"diagnostic_count":89,"duration_ms":12,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.Chebyshev","module_path":"PrimeNumberTheoremAnd/IEANTN/Chebyshev.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":779360,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":2,"module_index":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":779360,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":38,"diagnostic_count":28,"duration_ms":3012,"module_name":"PrimeNumberTheoremAnd.IEANTN.CostaPereira","module_path":"PrimeNumberTheoremAnd/IEANTN/CostaPereira.lean","ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"duration_ms":426168,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.CostaPereira","module_path":"PrimeNumberTheoremAnd/IEANTN/CostaPereira.lean","ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":38,"diagnostic_count":28,"duration_ms":2,"module_count":1,"module_name":"PrimeNumberTheoremAnd.IEANTN.CostaPereira","module_path":"PrimeNumberTheoremAnd/IEANTN/CostaPereira.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":311165,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":311165,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":368,"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":445988,"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":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":68407,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":1,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":68407,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":297,"diagnostic_count":259,"duration_ms":22809,"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":446927,"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":36,"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":29}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":19751,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 825230064660125861cba5ff3972606b529771e52c843f5d4500407d8ec59b82
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":1828414,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r5)
apx-semantic-phase {"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":382,"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":439798,"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":1,"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":464,"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":441325,"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":374,"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":436869,"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":1,"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":427,"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":438679,"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":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":82759,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":1,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":82759,"phase":"lean_module_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":22}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":13004,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 825230064660125861cba5ff3972606b529771e52c843f5d4500407d8ec59b82
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":1804922,"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":3,"diagnostic_count":0,"duration_ms":458,"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":443433,"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":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":85603,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":0,"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":407,"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":434148,"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":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":87967,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":1,"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":428,"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":441283,"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":1,"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":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":90257,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":90257,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":429,"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":440112,"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":1,"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":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":92539,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":92539,"phase":"lean_module_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":18}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":17692,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 825230064660125861cba5ff3972606b529771e52c843f5d4500407d8ec59b82
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":57,"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":1766401,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r7)
apx-semantic-phase {"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":476,"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":437931,"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":0,"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":0,"module_payload_kind":"fragment","ok":true,"payload_bytes":94376,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":0,"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":450,"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":433358,"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":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":96327,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":1,"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":445,"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":439564,"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":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":101240,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":101240,"phase":"lean_module_json_write"}
apx-semantic-phase {"declaration_count":3,"diagnostic_count":0,"duration_ms":426,"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":439425,"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":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":102723,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":3,"module_payload_kind":"fragment","ok":true,"payload_bytes":102723,"phase":"lean_module_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":18}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":10710,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 825230064660125861cba5ff3972606b529771e52c843f5d4500407d8ec59b82
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":1756668,"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":150,"diagnostic_count":101,"duration_ms":11335,"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":438017,"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":6,"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":466,"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":431940,"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":1,"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":1,"module_payload_kind":"fragment","ok":true,"payload_bytes":107456,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":1,"module_index":1,"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":6,"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":416757,"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":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":502,"phase":"lean_module_json_serialize"}
apx-semantic-phase {"duration_ms":0,"module_index":2,"module_payload_kind":"fragment","ok":true,"payload_bytes":502,"phase":"lean_module_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":10497,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 825230064660125861cba5ff3972606b529771e52c843f5d4500407d8ec59b82
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":1303241,"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":679,"diagnostic_count":493,"duration_ms":67373,"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":442817,"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":49,"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":2,"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":3407,"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":438698,"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":2,"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":0,"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":24}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":10700,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 825230064660125861cba5ff3972606b529771e52c843f5d4500407d8ec59b82
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":32,"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":957421,"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":32,"diagnostic_count":19,"duration_ms":1943,"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":437740,"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":3,"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":2,"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":21082,"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":434337,"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":22,"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":24}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":10002,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 825230064660125861cba5ff3972606b529771e52c843f5d4500407d8ec59b82
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":47,"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":899932,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r11)
apx-semantic-phase {"duration_ms":1,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":27,"diagnostic_count":9,"duration_ms":1758,"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":434831,"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":2,"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":3,"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":24}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":10113,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 825230064660125861cba5ff3972606b529771e52c843f5d4500407d8ec59b82
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":41,"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":441132,"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":67,"diagnostic_count":53,"duration_ms":4744,"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":432373,"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":6,"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":1,"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":24}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":10166,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 825230064660125861cba5ff3972606b529771e52c843f5d4500407d8ec59b82
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":45,"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":441727,"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":70,"diagnostic_count":54,"duration_ms":4967,"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":428304,"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":3,"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":0,"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":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":10115,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 825230064660125861cba5ff3972606b529771e52c843f5d4500407d8ec59b82
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":44,"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":437806,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r14)
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":235,"diagnostic_count":164,"duration_ms":18785,"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":441893,"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":10,"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":20}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":10118,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 825230064660125861cba5ff3972606b529771e52c843f5d4500407d8ec59b82
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":45,"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":465172,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset-r15)
apx-semantic-phase {"duration_ms":0,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":263,"diagnostic_count":178,"duration_ms":22270,"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":428257,"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":26,"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":24}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":10180,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 825230064660125861cba5ff3972606b529771e52c843f5d4500407d8ec59b82
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":43,"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":455070,"ok":true}