Verification run
Run 128
failed commit
5693c6340837 toolchain lean-v4-30-0 prover lean took 2h 20m · finished 2w ago ./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset) failed with exit code 1 (toolchain lean-v4-30-0, command: <command argv unavailable>)
Package inputs
This verification run did not include a theorem package lock. Its inputs depend only on repository, toolchain, image, and command inputs.
Trust verification
Recomputes trust checks from the recorded attestations, manifest, and command history.
(verification not run)
Manifest
Loads the published files manifest and location metadata for this job.
(manifest not loaded)
Verifier log excerpt
(11s)
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:167:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:204:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:275:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:355:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:714:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:749:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:792:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:879:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:962:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2192:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2218:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2824:8: declaration uses `sorry`
✔ [4153/4154] Built PrimeNumberTheoremAnd (8.4s)
Build completed successfully (4154 jobs).
stderr:
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
$ lake build :blueprint
exit_code=Some(0) duration_ms=956134
stdout:
✔ [15/35] Built Batteries.Lean.NameMapAttribute:c.o (1.6s)
✔ [26/35] Built Cli.Basic:c.o (3.1s)
✔ [30/35] Built Cli.Extensions:c.o (501ms)
✔ [33/40] Built Cli:c.o (66ms)
✔ [3509/3519] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.ZetaBounds:blueprint (77s)
ℹ [3593/3610] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3595/3611] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.MediumPNT:blueprint (60s)
✔ [3614/3641] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Backlund.ZeroCountCrude:blueprint (3.3s)
⚠ [3628/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/3643] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.StrongPNT:blueprint (49s)
✔ [3636/3644] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.BorelCaratheodory:blueprint (6.8s)
⚠ [3766/3784] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
✔ [3879/3902] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.LogTables:blueprint (3.8s)
⚠ [3891/3902] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3894/3902] Replayed PrimeNumberTheoremAnd.IEANTN.Mertens
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:925:16: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:929:0: Real.eulerMascheroniConstant_eq_neg_deriv : eulerMascheroniConstant = -deriv Gamma 1
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:939:8: declaration uses `sorry`
✔ [3899/3910] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.EulerMascheroniBounds:blueprint (2.6s)
⚠ [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 `⊢`!
✔ [3959/3986] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky_tables:blueprint (2.6s)
⚠ [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/3987] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaAppendix:blueprint (30s)
⚠ [3972/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.5s)
✔ [3981/3988] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions:blueprint (2.0s)
⚠ [3982/3990] Replayed PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:45:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:112:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:149:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:153:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:165:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:177:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:218:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:228:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:257:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:354:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:368:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:383:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:402:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:408:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:418:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:464:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:473:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:488:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:530:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:557:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:585:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:636:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:649:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:661:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:705:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:715:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:728:8: declaration uses `sorry`
✔ [3984/3992] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky:blueprint (16s)
✔ [3985/3992] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions:blueprint (9.0s)
✔ [3988/4006] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CostaPereira:blueprint (6.7s)
⚠ [4107/4122] Replayed PrimeNumberTheoremAnd.IEANTN.Buthe
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:31:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:41:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:51:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:61:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:83:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:131:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:142:8: declaration uses `sorry`
✔ [4112/4126] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Buthe:blueprint (6.5s)
⚠ [4113/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`
⚠ [4115/4126] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
✔ [4119/4178] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime:blueprint (24s)
✔ [4120/4178] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app:blueprint (20s)
✔ [4121/4178] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_tables:blueprint (8.6s)
⚠ [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 (27s)
✔ [4136/4198] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_a2_bounds:blueprint (7.8s)
ℹ [4139/4198] 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.
✔ [4140/4200] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core:blueprint (3.3s)
✔ [4161/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_next:blueprint (3.2s)
✔ [4162/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_values:blueprint (3.2s)
✔ [4164/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_65_85:blueprint (3.2s)
✔ [4165/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_90_95:blueprint (3.3s)
✔ [4166/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_100_1875:blueprint (3.3s)
✔ [4167/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_1900_2375:blueprint (3.4s)
✔ [4168/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2400_2875:blueprint (3.4s)
✔ [4169/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2900_3375:blueprint (3.4s)
✔ [4170/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3400_3875:blueprint (3.3s)
✔ [4171/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3900_4375:blueprint (3.3s)
✔ [4172/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4400_4875:blueprint (3.3s)
✔ [4173/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4900_6500:blueprint (3.3s)
✔ [4174/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_6600_8500:blueprint (3.3s)
✔ [4175/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_8600_10500:blueprint (3.4s)
✔ [4176/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_10600_12500:blueprint (3.3s)
✔ [4177/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_12600_24000:blueprint (3.5s)
✔ [4178/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_misc:blueprint (3.2s)
✔ [4179/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1:blueprint (51s)
⚠ [4180/4208] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3156:8: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3245:4: Try this:
[apply] ring_nf
The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3572:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3819:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3833:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3847:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3859:8: declaration uses `sorry`
✔ [4182/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimeInInterval:blueprint (4.7s)
⚠ [4184/4208] 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/4209] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:315: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`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3776:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4432:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4454:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4481:8: declaration uses `sorry`
✔ [4190/4209] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CH2.CH2:blueprint (19s)
⚠ [4193/4209] 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:747:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:759:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:771:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:783:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:795:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:807:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:819:8: declaration uses `sorry`
✔ [4195/4210] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_20_43:blueprint (3.4s)
✔ [4197/4210] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2:blueprint (32s)
✔ [4200/4211] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_44_59:blueprint (3.5s)
✔ [4202/4211] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Chebyshev:blueprint (18s)
✔ [4203/4211] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Dusart:blueprint (19s)
✔ [4206/4214] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows:blueprint (3.2s)
✔ [4208/4214] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Erdos392:blueprint (17s)
✔ [4211/4217] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_dispatch:blueprint (17s)
⚠ [4219/4238] 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`
✔ [4221/4238] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting:blueprint (75s)
✔ [4229/4306] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower:blueprint (21s)
⚠ [4230/4306] Replayed PrimeNumberTheoremAnd.IEANTN.TMEEMT
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:51:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:62:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:84:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:100:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:108:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:133:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:141:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:149:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:287:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:295:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:424:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:469:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:484:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:518:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:527:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:536:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:545:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:554:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:570:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:579:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:588:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:597:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:632:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:641:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:650:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:676:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:699:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:710:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:721:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:732:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:742:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:750:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:759:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:768:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:891:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:911:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:941:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:967:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:981:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:989:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1004:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1019:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1028:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1043:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1061:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1073:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1090:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1101:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1123:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1137:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1151:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1181:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1197:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1208:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1232:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1246:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1260:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1274:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1288:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1323:8: declaration uses `sorry`
✔ [4249/4321] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.TMEEMT:blueprint (49s)
⚠ [4257/4331] Replayed PrimeNumberTheoremAnd.IEANTN.SecondarySummary
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:60:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:203:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:213:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:227:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:242:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:255:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:337:8: declaration uses `sorry`
✔ [4276/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondarySummary:blueprint (10s)
⚠ [4281/4343] Replayed PrimeNumberTheoremAnd.IEANTN.Goldbach
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
⚠ [4290/4343] 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`
✔ [4292/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.MobiusLemma:blueprint (11s)
✔ [4295/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Goldbach:blueprint (6.6s)
✔ [4303/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Lcm:blueprint (11s)
✔ [4309/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimarySummary:blueprint (3.1s)
ℹ [4319/4343] 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.
✔ [4332/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan:blueprint (16s)
⚠ [4338/4343] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:167:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:204:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:275:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:355:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:714:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:749:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:792:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:879:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:962:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2192:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2218:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2824:8: declaration uses `sorry`
✔ [4339/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Kadiri:blueprint (53s)
✔ [4341/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (22s)
ℹ [4342/4344] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (165ms)
info: Blueprint indexing
Build completed successfully (4344 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)
exit_code=Some(1) duration_ms=63646
stdout:
.apodeixis/lean-runner/RepositorySemanticRunner.lean:1:0: error: object file '/apx/source/.lake/packages/leancert/.lake/build/lib/lean/LeanCert/ANT/Asymp.olean' of module LeanCert.ANT.Asymp does not exist
stderr:
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"core_compile","duration_ms":23253}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":11216,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":24,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper failed: helper support module '.apodeixis/lean-runner/RepositorySemanticRunner.lean' did not compile
remediation: inspect the generated helper support sources under .apodeixis/lean-runner
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00000)
exit_code=Some(1) duration_ms=3251
stdout:
.apodeixis/lean-runner/RepositorySemanticRunner.lean:1:0: error: object file '/apx/source/.lake/packages/leancert/.lake/build/lib/lean/LeanCert/ANT/Asymp.olean' of module LeanCert.ANT.Asymp does not exist
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":24}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":113,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":24,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper failed: helper support module '.apodeixis/lean-runner/RepositorySemanticRunner.lean' did not compile
remediation: inspect the generated helper support sources under .apodeixis/lean-runner
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00001)
exit_code=Some(0) duration_ms=979061
stdout:
apx-semantic-phase {"duration_ms":41,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":150,"diagnostic_count":101,"duration_ms":12084,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":150,"dependency_count":111,"diagnostic_count":242,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":484301,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":150,"dependency_count":111,"diagnostic_count":242,"duration_ms":165,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":930453,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":6,"ok":true,"payload_bytes":930453,"phase":"lean_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":24}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":153,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":14,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":247780,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 071474aaab06ac48322d22feed6b213f258ca14becb7bdb8a3f374972386fc44
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":729199,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00002-a)
exit_code=Some(1) duration_ms=2869
stdout:
.apodeixis/lean-runner/RepositorySemanticRunner.lean:1:0: error: object file '/apx/source/.lake/packages/leancert/.lake/build/lib/lean/LeanCert/ANT/Asymp.olean' of module LeanCert.ANT.Asymp does not exist
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":24}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":121,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":11,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper failed: helper support module '.apodeixis/lean-runner/RepositorySemanticRunner.lean' did not compile
remediation: inspect the generated helper support sources under .apodeixis/lean-runner
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00002-b)
exit_code=Some(1) duration_ms=2910
stdout:
.apodeixis/lean-runner/RepositorySemanticRunner.lean:1:0: error: object file '/apx/source/.lake/packages/leancert/.lake/build/lib/lean/LeanCert/ANT/Asymp.olean' of module LeanCert.ANT.Asymp does not exist
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":155,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":23,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper failed: helper support module '.apodeixis/lean-runner/RepositorySemanticRunner.lean' did not compile
remediation: inspect the generated helper support sources under .apodeixis/lean-runner
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00003-a)
exit_code=Some(1) duration_ms=3343
stdout:
.apodeixis/lean-runner/RepositorySemanticRunner.lean:1:0: error: object file '/apx/source/.lake/packages/leancert/.lake/build/lib/lean/LeanCert/ANT/Asymp.olean' of module LeanCert.ANT.Asymp does not exist
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":21}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":140,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":23,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper failed: helper support module '.apodeixis/lean-runner/RepositorySemanticRunner.lean' did not compile
remediation: inspect the generated helper support sources under .apodeixis/lean-runner
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00003-b)
exit_code=Some(1) duration_ms=3255
stdout:
.apodeixis/lean-runner/RepositorySemanticRunner.lean:1:0: error: object file '/apx/source/.lake/packages/leancert/.lake/build/lib/lean/LeanCert/ANT/Asymp.olean' of module LeanCert.ANT.Asymp does not exist
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":24}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":179,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":26,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper failed: helper support module '.apodeixis/lean-runner/RepositorySemanticRunner.lean' did not compile
remediation: inspect the generated helper support sources under .apodeixis/lean-runner
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00004-a)
exit_code=Some(1) duration_ms=2935
stdout:
.apodeixis/lean-runner/RepositorySemanticRunner.lean:1:0: error: object file '/apx/source/.lake/packages/leancert/.lake/build/lib/lean/LeanCert/ANT/Asymp.olean' of module LeanCert.ANT.Asymp does not exist
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":157,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":25,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper failed: helper support module '.apodeixis/lean-runner/RepositorySemanticRunner.lean' did not compile
remediation: inspect the generated helper support sources under .apodeixis/lean-runner
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00004-b)
exit_code=Some(1) duration_ms=3021
stdout:
.apodeixis/lean-runner/RepositorySemanticRunner.lean:1:0: error: object file '/apx/source/.lake/packages/leancert/.lake/build/lib/lean/LeanCert/ANT/Asymp.olean' of module LeanCert.ANT.Asymp does not exist
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":21}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":174,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":25,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper failed: helper support module '.apodeixis/lean-runner/RepositorySemanticRunner.lean' did not compile
remediation: inspect the generated helper support sources under .apodeixis/lean-runner
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00005-a)
exit_code=Some(1) duration_ms=3185
stdout:
.apodeixis/lean-runner/RepositorySemanticRunner.lean:1:0: error: object file '/apx/source/.lake/packages/leancert/.lake/build/lib/lean/LeanCert/ANT/Asymp.olean' of module LeanCert.ANT.Asymp does not exist
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":146,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":21,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper failed: helper support module '.apodeixis/lean-runner/RepositorySemanticRunner.lean' did not compile
remediation: inspect the generated helper support sources under .apodeixis/lean-runner
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00005-b)
exit_code=Some(1) duration_ms=3476
stdout:
.apodeixis/lean-runner/RepositorySemanticRunner.lean:1:0: error: object file '/apx/source/.lake/packages/leancert/.lake/build/lib/lean/LeanCert/ANT/Asymp.olean' of module LeanCert.ANT.Asymp does not exist
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":480,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":19,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper failed: helper support module '.apodeixis/lean-runner/RepositorySemanticRunner.lean' did not compile
remediation: inspect the generated helper support sources under .apodeixis/lean-runner
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00006-a)
exit_code=Some(1) duration_ms=3157
stdout:
.apodeixis/lean-runner/RepositorySemanticRunner.lean:1:0: error: object file '/apx/source/.lake/packages/leancert/.lake/build/lib/lean/LeanCert/ANT/Asymp.olean' of module LeanCert.ANT.Asymp does not exist
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":14}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":128,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":19,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper failed: helper support module '.apodeixis/lean-runner/RepositorySemanticRunner.lean' did not compile
remediation: inspect the generated helper support sources under .apodeixis/lean-runner
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00006-b)
exit_code=Some(1) duration_ms=3401
stdout:
.apodeixis/lean-runner/RepositorySemanticRunner.lean:1:0: error: object file '/apx/source/.lake/packages/leancert/.lake/build/lib/lean/LeanCert/ANT/Asymp.olean' of module LeanCert.ANT.Asymp does not exist
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":194,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":24,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper failed: helper support module '.apodeixis/lean-runner/RepositorySemanticRunner.lean' did not compile
remediation: inspect the generated helper support sources under .apodeixis/lean-runner
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00007-a)
exit_code=Some(1) duration_ms=3143
stdout:
.apodeixis/lean-runner/RepositorySemanticRunner.lean:1:0: error: object file '/apx/source/.lake/packages/leancert/.lake/build/lib/lean/LeanCert/ANT/Asymp.olean' of module LeanCert.ANT.Asymp does not exist
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":20}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":135,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":23,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper failed: helper support module '.apodeixis/lean-runner/RepositorySemanticRunner.lean' did not compile
remediation: inspect the generated helper support sources under .apodeixis/lean-runner
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00007-b)
exit_code=Some(1) duration_ms=3002
stdout:
.apodeixis/lean-runner/RepositorySemanticRunner.lean:1:0: error: object file '/apx/source/.lake/packages/leancert/.lake/build/lib/lean/LeanCert/ANT/Asymp.olean' of module LeanCert.ANT.Asymp does not exist
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":11}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":159,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":24,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper failed: helper support module '.apodeixis/lean-runner/RepositorySemanticRunner.lean' did not compile
remediation: inspect the generated helper support sources under .apodeixis/lean-runner
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00008-a)
exit_code=Some(1) duration_ms=2943
stdout:
.apodeixis/lean-runner/RepositorySemanticRunner.lean:1:0: error: object file '/apx/source/.lake/packages/leancert/.lake/build/lib/lean/LeanCert/ANT/Asymp.olean' of module LeanCert.ANT.Asymp does not exist
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":22}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":166,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":10,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper failed: helper support module '.apodeixis/lean-runner/RepositorySemanticRunner.lean' did not compile
remediation: inspect the generated helper support sources under .apodeixis/lean-runner
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00008-b)
exit_code=Some(1) duration_ms=3172
stdout:
.apodeixis/lean-runner/RepositorySemanticRun.lean:1:0: error: object file '/apx/source/.lake/packages/leancert/.lake/build/lib/lean/LeanCert/ANT/Asymp.olean' of module LeanCert.ANT.Asymp does not exist
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":206,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache cae750046114722b09a8e3704629027638efe6aeeb2025b674540c0c4aa8d420
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":2337,"ok":false}
lean semantic helper failed: generated static runner exited non-zero
remediation: inspect the generated repository runner and imported root modules
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00009)
exit_code=Some(0) duration_ms=511913
stdout:
apx-semantic-phase {"duration_ms":3,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":41,"diagnostic_count":6,"duration_ms":3142,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":41,"dependency_count":37,"diagnostic_count":9,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":475245,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":41,"dependency_count":37,"diagnostic_count":9,"duration_ms":119,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":355715,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":5,"ok":true,"payload_bytes":355715,"phase":"lean_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":19}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":124,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache e4b42e55817c080a724ce408535b0c0d4c3a60c2c17ba73d8ed5359158620ce8
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":27,"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":510579,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00010)
exit_code=Some(0) duration_ms=532983
stdout:
apx-semantic-phase {"duration_ms":235,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":255,"diagnostic_count":136,"duration_ms":19851,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":255,"dependency_count":329,"diagnostic_count":198,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":454759,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":255,"dependency_count":329,"diagnostic_count":198,"duration_ms":231,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":1366471,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":17,"ok":true,"payload_bytes":1366471,"phase":"lean_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":19}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":396,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":17,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":48467,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 7ff5246c1e00973820a8d237012b69f5031ecaf965ddb2bbb0b37dcddfa1c349
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":482684,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00011)
exit_code=Some(0) duration_ms=587752
stdout:
apx-semantic-phase {"duration_ms":25,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":67,"diagnostic_count":53,"duration_ms":5367,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":67,"dependency_count":60,"diagnostic_count":53,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":479887,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":67,"dependency_count":60,"diagnostic_count":53,"duration_ms":422,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":270148,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":8,"ok":true,"payload_bytes":270148,"phase":"lean_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":2222,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":25,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":76331,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 2dcd93d4adeb7db279f4d9b70d24077b98ca9e248f8fea4e5d1a5464cd8a04b1
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":506842,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00012)
exit_code=Some(0) duration_ms=583867
stdout:
apx-semantic-phase {"duration_ms":101,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":70,"diagnostic_count":54,"duration_ms":4848,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":70,"dependency_count":75,"diagnostic_count":54,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":481928,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":70,"dependency_count":75,"diagnostic_count":54,"duration_ms":106,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":415546,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":4,"ok":true,"payload_bytes":415546,"phase":"lean_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":9}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":635,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 7c7e15aaa4b0f4fda4874fe7acaf801d6891b0ed704d7efee8b308653c879011
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":46,"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":581701,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00013)
exit_code=Some(0) duration_ms=610511
stdout:
apx-semantic-phase {"duration_ms":29,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":235,"diagnostic_count":164,"duration_ms":18234,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":235,"dependency_count":633,"diagnostic_count":533,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":495255,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":235,"dependency_count":633,"diagnostic_count":533,"duration_ms":935,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":1764949,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":8,"ok":true,"payload_bytes":1764949,"phase":"lean_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":21}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":1744,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":27,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":78193,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache e30f7a7702153b0e76deba6a67b3462973f6915fdc008d975521c302e0bc73aa
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":528204,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00014)
exit_code=Some(0) duration_ms=665425
stdout:
apx-semantic-phase {"duration_ms":30,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":263,"diagnostic_count":178,"duration_ms":22905,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":263,"dependency_count":583,"diagnostic_count":199,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":502769,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":263,"dependency_count":583,"diagnostic_count":199,"duration_ms":215,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":1968805,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":10,"ok":true,"payload_bytes":1968805,"phase":"lean_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":19}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":1950,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":11,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":122556,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 8662e5f1451bce3be4a746d7a1ff8e8c547708ef504f0e8382d7ed2add740a0a
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":538977,"ok":true}
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00015)
exit_code=Some(1) duration_ms=13115
stdout:
.apodeixis/lean-runner/RepositorySemanticRun.lean:1:0: error: object file '/apx/source/.lake/packages/leancert/.lake/build/lib/lean/LeanCert/ANT/Asymp.olean' of module LeanCert.ANT.Asymp does not exist
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":1362,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache da9f756dea6de60400adc70233ed9274c380658d1444e316dba3809092e0957d
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":10085,"ok":false}
lean semantic helper failed: generated static runner exited non-zero
remediation: inspect the generated repository runner and imported root modules
$ ./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00016)
exit_code=Some(0) duration_ms=596309
stdout:
apx-semantic-phase {"duration_ms":29,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":0,"diagnostic_count":0,"duration_ms":35,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":0,"dependency_count":0,"diagnostic_count":0,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":505852,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":0,"dependency_count":0,"diagnostic_count":0,"duration_ms":113,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":772,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":16,"ok":true,"payload_bytes":772,"phase":"lean_json_write"}
stderr:
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":475,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":27,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":76649,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache c51de46e3f0cacd534b1130418e5a64c4b80713514cbedc4176f2630a787bfa3
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":518200,"ok":true}
Stored Lean workspace build cache
Command runs
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%, 16 KB/s], Decompressed: 0 Downloaded: 16 file(s) [attempted 16/8459 = 0%, 2 KB/s], Decompressed: 14 Downloaded: 43 file(s) [attempted 43/8459 = 0%, 22 KB/s], Decompressed: 42 Downloaded: 65 file(s) [attempted 65/8459 = 0%, 96 KB/s], Decompressed: 61 Downloaded: 93 file(s) [attempted 93/8459 = 1%, 183 KB/s], Decompressed: 90 Downloaded: 127 file(s) [attempted 127/8459 = 1%, 267 KB/s], Decompressed: 124 Downloaded: 162 file(s) [attempted 162/8459 = 1%, 369 KB/s], Decompressed: 158 Downloaded: 196 file(s) [attempted 196/8459 = 2%, 468 KB/s], Decompressed: 192 Downloaded: 230 file(s) [attempted 230/8459 = 2%, 596 KB/s], Decompressed: 223 Downloaded: 264 file(s) [attempted 264/8459 = 3%, 173 KB/s], Decompressed: 262 Downloaded: 302 file(s) [attempted 302/8459 = 3%, 811 KB/s], Decompressed: 299 Downloaded: 343 file(s) [attempted 343/8459 = 4%, 236 KB/s], Decompressed: 340 Downloaded: 384 file(s) [attempted 384/8459 = 4%, 135 KB/s], Decompressed: 381 Downloaded: 419 file(s) [attempted 419/8459 = 4%, 435 KB/s], Decompressed: 415 Downloaded: 457 file(s) [attempted 457/8459 = 5%, 196 KB/s], Decompressed: 449 Downloaded: 494 file(s) [attempted 494/8459 = 5%, 74 KB/s], Decompressed: 490 Downloaded: 535 file(s) [attempted 535/8459 = 6%, 69 KB/s], Decompressed: 528 Downloaded: 576 file(s) [attempted 576/8459 = 6%, 501 KB/s], Decompressed: 569 Downloaded: 614 file(s) [attempted 614/8459 = 7%, 281 KB/s], Decompressed: 604 Downloaded: 649 file(s) [attempted 649/8459 = 7%, 238 KB/s], Decompressed: 645 Downloaded: 693 file(s) [attempted 693/8459 = 8%, 223 KB/s], Decompressed: 689 Downloaded: 737 file(s) [attempted 737/8459 = 8%, 462 KB/s], Decompressed: 734 Downloaded: 778 file(s) [attempted 778/8459 = 9%, 355 KB/s], Decompressed: 771 Downloaded: 812 file(s) [attempted 812/8459 = 9%, 90 KB/s], Decompressed: 802 Downloaded: 850 file(s) [attempted 850/8459 = 10%, 94 KB/s], Decompressed: 843 Downloaded: 891 file(s) [attempted 891/8459 = 10%, 122 KB/s], Decompressed: 888 Downloaded: 939 file(s) [attempted 939/8459 = 11%, 71 KB/s], Decompressed: 932 Downloaded: 980 file(s) [attempted 980/8459 = 11%, 71 KB/s], Decompressed: 977 Downloaded: 1013 file(s) [attempted 1013/8459 = 11%, 830 KB/s], Decompressed: 1004 Downloaded: 1056 file(s) [attempted 1056/8459 = 12%, 246 KB/s], Decompressed: 1052 Downloaded: 1093 file(s) [attempted 1093/8459 = 12%, 566 KB/s], Decompressed: 1090 Downloaded: 1138 file(s) [attempted 1138/8459 = 13%, 234 KB/s], Decompressed: 1121 Downloaded: 1172 file(s) [attempted 1172/8459 = 13%, 267 KB/s], Decompressed: 1165 Downloaded: 1207 file(s) [attempted 1207/8459 = 14%, 978 KB/s], Decompressed: 1199 Downloaded: 1247 file(s) [attempted 1247/8459 = 14%, 68 KB/s], Decompressed: 1240 Downloaded: 1289 file(s) [attempted 1289/8459 = 15%, 244 KB/s], Decompressed: 1281 Downloaded: 1323 file(s) [attempted 1323/8459 = 15%, 1078 KB/s], Decompressed: 1319 Downloaded: 1364 file(s) [attempted 1364/8459 = 16%, 203 KB/s], Decompressed: 1360 Downloaded: 1405 file(s) [attempted 1405/8459 = 16%, 422 KB/s], Decompressed: 1401 Downloaded: 1446 file(s) [attempted 1446/8459 = 17%, 1087 KB/s], Decompressed: 1435 Downloaded: 1483 file(s) [attempted 1483/8459 = 17%, 52 KB/s], Decompressed: 1480 Downloaded: 1524 file(s) [attempted 1524/8459 = 18%, 83 KB/s], Decompressed: 1521 Downloaded: 1562 file(s) [attempted 1562/8459 = 18%, 154 KB/s], Decompressed: 1555 Downloaded: 1603 file(s) [attempted 1603/8459 = 18%, 44 KB/s], Decompressed: 1600 Downloaded: 1644 file(s) [attempted 1644/8459 = 19%, 416 KB/s], Decompressed: 1637 Downloaded: 1685 file(s) [attempted 1685/8459 = 19%, 287 KB/s], Decompressed: 1682 Downloaded: 1728 file(s) [attempted 1728/8459 = 20%, 253 KB/s], Decompressed: 1716 Downloaded: 1764 file(s) [attempted 1764/8459 = 20%, 146 KB/s], Decompressed: 1754 Downloaded: 1805 file(s) [attempted 1805/8459 = 21%, 190 KB/s], Decompressed: 1802 Downloaded: 1846 file(s) [attempted 1846/8459 = 21%, 39 KB/s], Decompressed: 1839 Downloaded: 1880 file(s) [attempted 1880/8459 = 22%, 99 KB/s], Decompressed: 1877 Downloaded: 1919 file(s) [attempted 1919/8459 = 22%, 544 KB/s], Decompressed: 1911 Downloaded: 1959 file(s) [attempted 1959/8459 = 23%, 193 KB/s], Decompressed: 1952 Downloaded: 2002 file(s) [attempted 2002/8459 = 23%, 77 KB/s], Decompressed: 1993 Downloaded: 2041 file(s) [attempted 2041/8459 = 24%, 323 KB/s], Decompressed: 2034 Downloaded: 2079 file(s) [attempted 2079/8459 = 24%, 1167 KB/s], Decompressed: 2072 Downloaded: 2120 file(s) [attempted 2120/8459 = 25%, 115 KB/s], Decompressed: 2113 Downloaded: 2164 file(s) [attempted 2164/8459 = 25%, 207 KB/s], Decompressed: 2158 Downloaded: 2206 file(s) [attempted 2206/8459 = 26%, 428 KB/s], Decompressed: 2199 Downloaded: 2247 file(s) [attempted 2247/8459 = 26%, 995 KB/s], Decompressed: 2243 Downloaded: 2288 file(s) [attempted 2288/8459 = 27%, 308 KB/s], Decompressed: 2281 Downloaded: 2322 file(s) [attempted 2322/8459 = 27%, 94 KB/s], Decompressed: 2318 Downloaded: 2365 file(s) [attempted 2365/8459 = 27%, 103 KB/s], Decompressed: 2360 Downloaded: 2401 file(s) [attempted 2401/8459 = 28%, 332 KB/s], Decompressed: 2397 Downloaded: 2445 file(s) [attempted 2445/8459 = 28%, 263 KB/s], Decompressed: 2442 Downloaded: 2486 file(s) [attempted 2486/8459 = 29%, 190 KB/s], Decompressed: 2479 Downloaded: 2523 file(s) [attempted 2523/8459 = 29%, 683 KB/s], Decompressed: 2517 Downloaded: 2561 file(s) [attempted 2561/8459 = 30%, 49 KB/s], Decompressed: 2558 Downloaded: 2599 file(s) [attempted 2599/8459 = 30%, 115 KB/s], Decompressed: 2596 Downloaded: 2640 file(s) [attempted 2640/8459 = 31%, 715 KB/s], Decompressed: 2633 Downloaded: 2679 file(s) [attempted 2679/8459 = 31%, 209 KB/s], Decompressed: 2674 Downloaded: 2714 file(s) [attempted 2714/8459 = 32%, 995 KB/s], Decompressed: 2705 Downloaded: 2753 file(s) [attempted 2753/8459 = 32%, 204 KB/s], Decompressed: 2750 Downloaded: 2798 file(s) [attempted 2798/8459 = 33%, 1152 KB/s], Decompressed: 2794 Downloaded: 2839 file(s) [attempted 2839/8459 = 33%, 85 KB/s], Decompressed: 2832 Downloaded: 2878 file(s) [attempted 2878/8459 = 34%, 511 KB/s], Decompressed: 2869 Downloaded: 2911 file(s) [attempted 2911/8459 = 34%, 233 KB/s], Decompressed: 2907 Downloaded: 2955 file(s) [attempted 2955/8459 = 34%, 96 KB/s], Decompressed: 2952 Downloaded: 2996 file(s) [attempted 2996/8459 = 35%, 185 KB/s], Decompressed: 2993 Downloaded: 3038 file(s) [attempted 3038/8459 = 35%, 1013 KB/s], Decompressed: 3034 Downloaded: 3078 file(s) [attempted 3078/8459 = 36%, 446 KB/s], Decompressed: 3071 Downloaded: 3116 file(s) [attempted 3116/8459 = 36%, 163 KB/s], Decompressed: 3102 Downloaded: 3150 file(s) [attempted 3150/8459 = 37%, 129 KB/s], Decompressed: 3147 Downloaded: 3195 file(s) [attempted 3195/8459 = 37%, 276 KB/s], Decompressed: 3191 Downloaded: 3239 file(s) [attempted 3239/8459 = 38%, 205 KB/s], Decompressed: 3232 Downloaded: 3277 file(s) [attempted 3277/8459 = 38%, 251 KB/s], Decompressed: 3273 Downloaded: 3321 file(s) [attempted 3321/8459 = 39%, 88 KB/s], Decompressed: 3318 Downloaded: 3362 file(s) [attempted 3362/8459 = 39%, 61 KB/s], Decompressed: 3355 Downloaded: 3398 file(s) [attempted 3398/8459 = 40%, 120 KB/s], Decompressed: 3393 Downloaded: 3441 file(s) [attempted 3441/8459 = 40%, 66 KB/s], Decompressed: 3438 Downloaded: 3479 file(s) [attempted 3479/8459 = 41%, 1749 KB/s], Decompressed: 3475 Downloaded: 3520 file(s) [attempted 3520/8459 = 41%, 99 KB/s], Decompressed: 3513 Downloaded: 3557 file(s) [attempted 3557/8459 = 42%, 104 KB/s], Decompressed: 3544 Downloaded: 3595 file(s) [attempted 3595/8459 = 42%, 31 KB/s], Decompressed: 3592 Downloaded: 3634 file(s) [attempted 3634/8459 = 42%, 56 KB/s], Decompressed: 3629 Downloaded: 3671 file(s) [attempted 3671/8459 = 43%, 424 KB/s], Decompressed: 3663 Downloaded: 3711 file(s) [attempted 3711/8459 = 43%, 67 KB/s], Decompressed: 3701 Downloaded: 3749 file(s) [attempted 3749/8459 = 44%, 223 KB/s], Decompressed: 3746 Downloaded: 3787 file(s) [attempted 3787/8459 = 44%, 415 KB/s], Decompressed: 3783 Downloaded: 3828 file(s) [attempted 3828/8459 = 45%, 109 KB/s], Decompressed: 3824 Downloaded: 3867 file(s) [attempted 3867/8459 = 45%, 976 KB/s], Decompressed: 3859 Downloaded: 3910 file(s) [attempted 3910/8459 = 46%, 21 KB/s], Decompressed: 3903 Downloaded: 3951 file(s) [attempted 3951/8459 = 46%, 214 KB/s], Decompressed: 3944 Downloaded: 3985 file(s) [attempted 3985/8459 = 47%, 318 KB/s], Decompressed: 3978 Downloaded: 4026 file(s) [attempted 4026/8459 = 47%, 619 KB/s], Decompressed: 4016 Downloaded: 4060 file(s) [attempted 4060/8459 = 47%, 1044 KB/s], Decompressed: 4057 Downloaded: 4101 file(s) [attempted 4101/8459 = 48%, 70 KB/s], Decompressed: 4098 Downloaded: 4146 file(s) [attempted 4146/8459 = 49%, 66 KB/s], Decompressed: 4139 Downloaded: 4184 file(s) [attempted 4184/8459 = 49%, 298 KB/s], Decompressed: 4180 Downloaded: 4221 file(s) [attempted 4221/8459 = 49%, 405 KB/s], Decompressed: 4214 Downloaded: 4259 file(s) [attempted 4259/8459 = 50%, 214 KB/s], Decompressed: 4257 Downloaded: 4300 file(s) [attempted 4300/8459 = 50%, 1125 KB/s], Decompressed: 4293 Downloaded: 4341 file(s) [attempted 4341/8459 = 51%, 369 KB/s], Decompressed: 4338 Downloaded: 4379 file(s) [attempted 4379/8459 = 51%, 1011 KB/s], Decompressed: 4368 Downloaded: 4416 file(s) [attempted 4416/8459 = 52%, 282 KB/s], Decompressed: 4410 Downloaded: 4454 file(s) [attempted 4454/8459 = 52%, 94 KB/s], Decompressed: 4447 Downloaded: 4492 file(s) [attempted 4492/8459 = 53%, 236 KB/s], Decompressed: 4488 Downloaded: 4536 file(s) [attempted 4536/8459 = 53%, 573 KB/s], Decompressed: 4533 Downloaded: 4574 file(s) [attempted 4574/8459 = 54%, 516 KB/s], Decompressed: 4567 Downloaded: 4611 file(s) [attempted 4611/8459 = 54%, 86 KB/s], Decompressed: 4608 Downloaded: 4649 file(s) [attempted 4649/8459 = 54%, 180 KB/s], Decompressed: 4642 Downloaded: 4687 file(s) [attempted 4687/8459 = 55%, 47 KB/s], Decompressed: 4680 Downloaded: 4731 file(s) [attempted 4731/8459 = 55%, 574 KB/s], Decompressed: 4730 Downloaded: 4772 file(s) [attempted 4772/8459 = 56%, 23 KB/s], Decompressed: 4769 Downloaded: 4813 file(s) [attempted 4813/8459 = 56%, 213 KB/s], Decompressed: 4810 Downloaded: 4848 file(s) [attempted 4848/8459 = 57%, 81 KB/s], Decompressed: 4837 Downloaded: 4882 file(s) [attempted 4882/8459 = 57%, 1005 KB/s], Decompressed: 4878 Downloaded: 4926 file(s) [attempted 4926/8459 = 58%, 147 KB/s], Decompressed: 4919 Downloaded: 4964 file(s) [attempted 4964/8459 = 58%, 1698 KB/s], Decompressed: 4957 Downloaded: 5002 file(s) [attempted 5002/8459 = 59%, 692 KB/s], Decompressed: 4998 Downloaded: 5041 file(s) [attempted 5041/8459 = 59%, 255 KB/s], Decompressed: 5032 Downloaded: 5080 file(s) [attempted 5080/8459 = 60%, 142 KB/s], Decompressed: 5077 Downloaded: 5121 file(s) [attempted 5121/8459 = 60%, 309 KB/s], Decompressed: 5115 Downloaded: 5159 file(s) [attempted 5159/8459 = 60%, 59 KB/s], Decompressed: 5152 Downloaded: 5200 file(s) [attempted 5200/8459 = 61%, 107 KB/s], Decompressed: 5193 Downloaded: 5241 file(s) [attempted 5241/8459 = 61%, 80 KB/s], Decompressed: 5234 Downloaded: 5282 file(s) [attempted 5282/8459 = 62%, 287 KB/s], Decompressed: 5272 Downloaded: 5320 file(s) [attempted 5320/8459 = 62%, 478 KB/s], Decompressed: 5313 Downloaded: 5361 file(s) [attempted 5361/8459 = 63%, 188 KB/s], Decompressed: 5354 Downloaded: 5405 file(s) [attempted 5405/8459 = 63%, 58 KB/s], Decompressed: 5402 Downloaded: 5443 file(s) [attempted 5443/8459 = 64%, 484 KB/s], Decompressed: 5440 Downloaded: 5488 file(s) [attempted 5488/8459 = 64%, 278 KB/s], Decompressed: 5481 Downloaded: 5522 file(s) [attempted 5522/8459 = 65%, 227 KB/s], Decompressed: 5518 Downloaded: 5562 file(s) [attempted 5562/8459 = 65%, 167 KB/s], Decompressed: 5553 Downloaded: 5601 file(s) [attempted 5601/8459 = 66%, 234 KB/s], Decompressed: 5597 Downloaded: 5642 file(s) [attempted 5642/8459 = 66%, 560 KB/s], Decompressed: 5638 Downloaded: 5676 file(s) [attempted 5676/8459 = 67%, 48 KB/s], Decompressed: 5672 Downloaded: 5713 file(s) [attempted 5713/8459 = 67%, 478 KB/s], Decompressed: 5703 Downloaded: 5753 file(s) [attempted 5753/8459 = 68%, 447 KB/s], Decompressed: 5748 Downloaded: 5796 file(s) [attempted 5796/8459 = 68%, 42 KB/s], Decompressed: 5792 Downloaded: 5833 file(s) [attempted 5833/8459 = 68%, 61 KB/s], Decompressed: 5830 Downloaded: 5871 file(s) [attempted 5871/8459 = 69%, 183 KB/s], Decompressed: 5864 Downloaded: 5906 file(s) [attempted 5906/8459 = 69%, 327 KB/s], Decompressed: 5902 Downloaded: 5950 file(s) [attempted 5950/8459 = 70%, 25 KB/s], Decompressed: 5946 Downloaded: 5991 file(s) [attempted 5991/8459 = 70%, 143 KB/s], Decompressed: 5987 Downloaded: 6028 file(s) [attempted 6028/8459 = 71%, 137 KB/s], Decompressed: 6018 Downloaded: 6069 file(s) [attempted 6069/8459 = 71%, 348 KB/s], Decompressed: 6066 Downloaded: 6110 file(s) [attempted 6110/8459 = 72%, 548 KB/s], Decompressed: 6100 Downloaded: 6148 file(s) [attempted 6148/8459 = 72%, 1195 KB/s], Decompressed: 6141 Downloaded: 6189 file(s) [attempted 6189/8459 = 73%, 70 KB/s], Decompressed: 6182 Downloaded: 6227 file(s) [attempted 6227/8459 = 73%, 215 KB/s], Decompressed: 6223 Downloaded: 6264 file(s) [attempted 6264/8459 = 74%, 184 KB/s], Decompressed: 6254 Downloaded: 6299 file(s) [attempted 6299/8459 = 74%, 783 KB/s], Decompressed: 6292 Downloaded: 6337 file(s) [attempted 6337/8459 = 74%, 56 KB/s], Decompressed: 6329 Downloaded: 6377 file(s) [attempted 6377/8459 = 75%, 296 KB/s], Decompressed: 6374 Downloaded: 6422 file(s) [attempted 6422/8459 = 75%, 554 KB/s], Decompressed: 6418 Downloaded: 6456 file(s) [attempted 6456/8459 = 76%, 262 KB/s], Decompressed: 6446 Downloaded: 6494 file(s) [attempted 6494/8459 = 76%, 76 KB/s], Decompressed: 6490 Downloaded: 6535 file(s) [attempted 6535/8459 = 77%, 194 KB/s], Decompressed: 6528 Downloaded: 6576 file(s) [attempted 6576/8459 = 77%, 393 KB/s], Decompressed: 6569 Downloaded: 6612 file(s) [attempted 6612/8459 = 78%, 277 KB/s], Decompressed: 6607 Downloaded: 6650 file(s) [attempted 6650/8459 = 78%, 285 KB/s], Decompressed: 6644 Downloaded: 6685 file(s) [attempted 6685/8459 = 79%, 244 KB/s], Decompressed: 6682 Downloaded: 6726 file(s) [attempted 6726/8459 = 79%, 125 KB/s], Decompressed: 6723 Downloaded: 6761 file(s) [attempted 6761/8459 = 79%, 425 KB/s], Decompressed: 6757 Downloaded: 6798 file(s) [attempted 6798/8459 = 80%, 194 KB/s], Decompressed: 6791 Downloaded: 6833 file(s) [attempted 6833/8459 = 80%, 283 KB/s], Decompressed: 6829 Downloaded: 6874 file(s) [attempted 6874/8459 = 81%, 372 KB/s], Decompressed: 6867 Downloaded: 6910 file(s) [attempted 6910/8459 = 81%, 221 KB/s], Decompressed: 6904 Downloaded: 6949 file(s) [attempted 6949/8459 = 82%, 887 KB/s], Decompressed: 6946 Downloaded: 6990 file(s) [attempted 6990/8459 = 82%, 1356 KB/s], Decompressed: 6983 Downloaded: 7031 file(s) [attempted 7031/8459 = 83%, 76 KB/s], Decompressed: 7024 Downloaded: 7069 file(s) [attempted 7069/8459 = 83%, 1001 KB/s], Decompressed: 7062 Downloaded: 7106 file(s) [attempted 7106/8459 = 84%, 556 KB/s], Decompressed: 7100 Downloaded: 7146 file(s) [attempted 7146/8459 = 84%, 409 KB/s], Decompressed: 7141 Downloaded: 7183 file(s) [attempted 7183/8459 = 84%, 86 KB/s], Decompressed: 7178 Downloaded: 7223 file(s) [attempted 7223/8459 = 85%, 304 KB/s], Decompressed: 7216 Downloaded: 7260 file(s) [attempted 7260/8459 = 85%, 301 KB/s], Decompressed: 7257 Downloaded: 7301 file(s) [attempted 7301/8459 = 86%, 1903 KB/s], Decompressed: 7298 Downloaded: 7343 file(s) [attempted 7343/8459 = 86%, 109 KB/s], Decompressed: 7339 Downloaded: 7384 file(s) [attempted 7384/8459 = 87%, 455 KB/s], Decompressed: 7380 Downloaded: 7421 file(s) [attempted 7421/8459 = 87%, 376 KB/s], Decompressed: 7414 Downloaded: 7461 file(s) [attempted 7461/8459 = 88%, 935 KB/s], Decompressed: 7455 Downloaded: 7500 file(s) [attempted 7500/8459 = 88%, 166 KB/s], Decompressed: 7497 Downloaded: 7543 file(s) [attempted 7543/8459 = 89%, 1985 KB/s], Decompressed: 7534 Downloaded: 7575 file(s) [attempted 7575/8459 = 89%, 165 KB/s], Decompressed: 7572 Downloaded: 7613 file(s) [attempted 7613/8459 = 89%, 33 KB/s], Decompressed: 7609 Downloaded: 7651 file(s) [attempted 7651/8459 = 90%, 485 KB/s], Decompressed: 7647 Downloaded: 7695 file(s) [attempted 7695/8459 = 90%, 895 KB/s], Decompressed: 7688 Downloaded: 7736 file(s) [attempted 7736/8459 = 91%, 26 KB/s], Decompressed: 7729 Downloaded: 7774 file(s) [attempted 7774/8459 = 91%, 160 KB/s], Decompressed: 7770 Downloaded: 7811 file(s) [attempted 7811/8459 = 92%, 286 KB/s], Decompressed: 7808 Downloaded: 7849 file(s) [attempted 7849/8459 = 92%, 79 KB/s], Decompressed: 7846 Downloaded: 7893 file(s) [attempted 7893/8459 = 93%, 288 KB/s], Decompressed: 7883 Downloaded: 7932 file(s) [attempted 7932/8459 = 93%, 206 KB/s], Decompressed: 7928 Downloaded: 7973 file(s) [attempted 7973/8459 = 94%, 649 KB/s], Decompressed: 7969 Downloaded: 8010 file(s) [attempted 8010/8459 = 94%, 110 KB/s], Decompressed: 8006 Downloaded: 8047 file(s) [attempted 8047/8459 = 95%, 1621 KB/s], Decompressed: 8044 Downloaded: 8085 file(s) [attempted 8085/8459 = 95%, 176 KB/s], Decompressed: 8078 Downloaded: 8123 file(s) [attempted 8123/8459 = 96%, 36 KB/s], Decompressed: 8116 Downloaded: 8164 file(s) [attempted 8164/8459 = 96%, 116 KB/s], Decompressed: 8157 Downloaded: 8203 file(s) [attempted 8203/8459 = 96%, 262 KB/s], Decompressed: 8198 Downloaded: 8241 file(s) [attempted 8241/8459 = 97%, 231 KB/s], Decompressed: 8236 Downloaded: 8280 file(s) [attempted 8280/8459 = 97%, 940 KB/s], Decompressed: 8273 Downloaded: 8325 file(s) [attempted 8325/8459 = 98%, 469 KB/s], Decompressed: 8318 Downloaded: 8366 file(s) [attempted 8366/8459 = 98%, 332 KB/s], Decompressed: 8362 Downloaded: 8400 file(s) [attempted 8400/8459 = 99%, 127 KB/s], Decompressed: 8397 Downloaded: 8438 file(s) [attempted 8438/8459 = 99%, 77 KB/s], Decompressed: 8424 Downloaded: 8459 file(s) [attempted 8459/8459 = 100%, 77 KB/s], Decompressed: 8451
git_clone exit 0
git clone --depth 1 --branch main --single-branch https://github.com/AlexKontorovich/PrimeNumberTheoremAnd.git /var/lib/apodeixis/repos/job-872-source
Cloning into '/var/lib/apodeixis/repos/job-872-source'...
git_checkout exit 128
git checkout 5693c63408375e690243c38a2855066a60afb949
fatal: reference is not a tree: 5693c63408375e690243c38a2855066a60afb949
git_checkout exit 0
git fetch --depth 1 origin 5693c63408375e690243c38a2855066a60afb949
From https://github.com/AlexKontorovich/PrimeNumberTheoremAnd * branch 5693c63408375e690243c38a2855066a60afb949 -> FETCH_HEAD
git_checkout exit 0
git checkout 5693c63408375e690243c38a2855066a60afb949 (after fetch)
Note: switching to '5693c63408375e690243c38a2855066a60afb949'. 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 5693c63 feat(FKS2): extended Table 4 mid-range interpolation for Eπ (towards #721) (#1563)
lean_checker exit 0
lake build
✔ [3473/3481] Built PrimeNumberTheoremAnd.ZetaBounds (95s)
ℹ [3537/3548] Built PrimeNumberTheoremAnd.MediumPNT (41s)
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3548/3561] Built PrimeNumberTheoremAnd.Backlund.ZeroCountCrude (29s)
⚠ [3563/3571] Built PrimeNumberTheoremAnd.StrongPNT (13s)
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`
✔ [3567/3576] Built PrimeNumberTheoremAnd.BorelCaratheodory (4.8s)
⚠ [3694/3710] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
✔ [3805/3817] Built PrimeNumberTheoremAnd.IEANTN.LogTables (30s)
⚠ [3812/3819] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3814/3819] Replayed PrimeNumberTheoremAnd.IEANTN.Mertens
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:925:16: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:929:0: Real.eulerMascheroniConstant_eq_neg_deriv : eulerMascheroniConstant = -deriv Gamma 1
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:939:8: declaration uses `sorry`
✔ [3817/3824] Built PrimeNumberTheoremAnd.EulerMascheroniBounds (11s)
✔ [3873/3884] Built PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky_tables (2.0s)
⚠ [3880/3892] Built PrimeNumberTheoremAnd.IEANTN.ZetaAppendix (55s)
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2577:8: `simp [v, Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2578:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2599:8: `simp [v', Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2600:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2817:8: `simp [v, Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2818:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2833:8: `simp [v', Set.uIcc_of_le hab.le]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2834:8: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2963:4: `simp [W]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2964:4: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3069:4: `simp [p]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3070:4: `fun_prop` uses `⊢`!
warning: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3084:4: `simp [Set.uIcc_of_le hab]` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.
Note: This linter can be disabled with `set_option linter.flexible false`
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3084:4: Try this:
[apply] simp only [_root_.deriv_ofReal]
info: PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3085:4: `fun_prop` uses `⊢`!
⚠ [3881/3892] Replayed LeanCert.Examples.Li2Bounds
warning: LeanCert/Examples/Li2Bounds.lean:40:8: declaration uses `sorry`
warning: LeanCert/Examples/Li2Bounds.lean:48:8: declaration uses `sorry`
⚠ [3883/3894] Built PrimeNumberTheoremAnd.IEANTN.ZetaSummary (25s)
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.1s)
✔ [3891/3895] Built PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions (8.7s)
⚠ [3892/3895] Built PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky (9.8s)
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.3s)
⚠ [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/4025] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app (16s)
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:47:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:168:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:516:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1127:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1180:8: declaration uses `sorry`
✔ [4019/4025] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_tables (91s)
⚠ [4020/4026] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime (23s)
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
⚠ [4022/4055] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW (33s)
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 (17s)
✔ [4036/4061] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core (9.1s)
✔ [4038/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_65_85 (22s)
✔ [4039/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_misc (15s)
✔ [4040/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_12600_24000 (76s)
✔ [4041/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_10600_12500 (75s)
✔ [4042/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_8600_10500 (62s)
✔ [4043/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_6600_8500 (61s)
✔ [4044/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4900_6500 (63s)
✔ [4045/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4400_4875 (65s)
✔ [4046/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3900_4375 (71s)
✔ [4047/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3400_3875 (77s)
✔ [4048/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2900_3375 (75s)
✔ [4049/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2400_2875 (43s)
✔ [4050/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_1900_2375 (40s)
✔ [4051/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_100_1875 (39s)
✔ [4052/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_90_95 (6.1s)
✔ [4053/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_values (9.7s)
✔ [4054/4068] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_next (18s)
ℹ [4055/4068] Built PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 (47s)
info: PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:359:15: Try this:
[apply] ring_nf
The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
✔ [4057/4068] Built PrimeNumberTheoremAnd.IEANTN.PrimeInInterval (5.4s)
✔ [4059/4070] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_20_43 (64s)
⚠ [4060/4075] Built PrimeNumberTheoremAnd.IEANTN.CH2.CH2 (15s)
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3156:8: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3245:4: Try this:
[apply] ring_nf
The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3572:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3819:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3833:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3847:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3859:8: declaration uses `sorry`
⚠ [4062/4075] 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`
✔ [4063/4075] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_44_59 (41s)
⚠ [4066/4075] Built PrimeNumberTheoremAnd.IEANTN.FKS2 (54s)
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:315: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`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3776:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4432:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4454:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4481:8: declaration uses `sorry`
✔ [4069/4076] Built PrimeNumberTheoremAnd.IEANTN.Chebyshev (22s)
⚠ [4070/4076] Built PrimeNumberTheoremAnd.IEANTN.Dusart (18s)
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:747:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:759:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:771:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:783:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:795:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:807:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:819:8: declaration uses `sorry`
✔ [4071/4076] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows (5.3s)
✔ [4074/4077] Built PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_dispatch (18s)
✔ [4075/4077] Built PrimeNumberTheoremAnd.IEANTN.Erdos392 (45s)
⚠ [4087/4097] Built PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting (12s)
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`
✔ [4092/4131] Built PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower (10s)
⚠ [4094/4133] Built PrimeNumberTheoremAnd.IEANTN.TMEEMT (14s)
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:51:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:62:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:84:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:100:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:108:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:133:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:141:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:149:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:287:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:295:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:424:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:469:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:484:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:518:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:527:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:536:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:545:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:554:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:570:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:579:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:588:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:597:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:632:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:641:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:650:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:676:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:699:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:710:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:721:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:732:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:742:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:750:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:759:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:768:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:891:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:911:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:941:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:967:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:981:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:989:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1004:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1019:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1028:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1043:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1061:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1073:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1090:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1101:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1123:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1137:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1151:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1181:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1197:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1208:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1232:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1246:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1260:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1274:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1288:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1323:8: declaration uses `sorry`
⚠ [4112/4141] Built PrimeNumberTheoremAnd.IEANTN.SecondarySummary (9.8s)
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:60:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:203:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:213:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:227:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:242:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:255:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:337:8: declaration uses `sorry`
⚠ [4119/4147] Built PrimeNumberTheoremAnd.IEANTN.Goldbach (6.5s)
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
✔ [4126/4154] Built PrimeNumberTheoremAnd.IEANTN.MobiusLemma (11s)
✔ [4128/4154] Built PrimeNumberTheoremAnd.IEANTN.Lcm (26s)
⚠ [4130/4154] 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`
✔ [4133/4154] Built PrimeNumberTheoremAnd.IEANTN.PrimarySummary (2.7s)
ℹ [4141/4154] 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.
✔ [4151/4154] Built PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan (54s)
⚠ [4152/4154] Built PrimeNumberTheoremAnd.IEANTN.Kadiri (11s)
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:167:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:204:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:275:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:355:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:714:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:749:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:792:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:879:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:962:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2192:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2218:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2824:8: declaration uses `sorry`
✔ [4153/4154] Built PrimeNumberTheoremAnd (8.4s)
Build completed successfully (4154 jobs).
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
blueprint_build exit 0
lake build :blueprint
✔ [15/35] Built Batteries.Lean.NameMapAttribute:c.o (1.6s)
✔ [26/35] Built Cli.Basic:c.o (3.1s)
✔ [30/35] Built Cli.Extensions:c.o (501ms)
✔ [33/40] Built Cli:c.o (66ms)
✔ [3509/3519] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.ZetaBounds:blueprint (77s)
ℹ [3593/3610] Replayed PrimeNumberTheoremAnd.MediumPNT
info: PrimeNumberTheoremAnd/MediumPNT.lean:4282:0: 'MediumPNT' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3595/3611] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.MediumPNT:blueprint (60s)
✔ [3614/3641] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.Backlund.ZeroCountCrude:blueprint (3.3s)
⚠ [3628/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/3643] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.StrongPNT:blueprint (49s)
✔ [3636/3644] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.BorelCaratheodory:blueprint (6.8s)
⚠ [3766/3784] Replayed PrimeNumberTheoremAnd.Wiener
warning: PrimeNumberTheoremAnd/Wiener.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/Wiener.lean:342:8: declaration uses `sorry`
✔ [3879/3902] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.LogTables:blueprint (3.8s)
⚠ [3891/3902] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldZeta.lean:18:8: declaration uses `sorry`
⚠ [3894/3902] Replayed PrimeNumberTheoremAnd.IEANTN.Mertens
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:925:16: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:929:0: Real.eulerMascheroniConstant_eq_neg_deriv : eulerMascheroniConstant = -deriv Gamma 1
warning: PrimeNumberTheoremAnd/IEANTN/Mertens.lean:939:8: declaration uses `sorry`
✔ [3899/3910] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.EulerMascheroniBounds:blueprint (2.6s)
⚠ [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 `⊢`!
✔ [3959/3986] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky_tables:blueprint (2.6s)
⚠ [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/3987] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.ZetaAppendix:blueprint (30s)
⚠ [3972/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.5s)
✔ [3981/3988] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions:blueprint (2.0s)
⚠ [3982/3990] Replayed PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:45:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:112:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:149:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:153:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:165:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:177:18: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:218:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:228:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:257:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:354:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:368:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:383:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:402:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:408:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:418:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:464:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:473:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:488:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:530:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:557:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:585:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:636:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:649:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:661:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:705:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:715:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FioriKadiriSwidinsky/FioriKadiriSwidinsky.lean:728:8: declaration uses `sorry`
✔ [3984/3992] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FioriKadiriSwidinsky.FioriKadiriSwidinsky:blueprint (16s)
✔ [3985/3992] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondaryDefinitions:blueprint (9.0s)
✔ [3988/4006] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CostaPereira:blueprint (6.7s)
⚠ [4107/4122] Replayed PrimeNumberTheoremAnd.IEANTN.Buthe
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:31:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:41:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:51:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:61:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:83:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:131:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Buthe.lean:142:8: declaration uses `sorry`
✔ [4112/4126] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Buthe:blueprint (6.5s)
⚠ [4113/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`
⚠ [4115/4126] Replayed PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime
warning: PrimeNumberTheoremAnd/IEANTN/RosserSchoenfeld/RosserSchoenfeldPrime.lean:1008:8: declaration uses `sorry`
✔ [4119/4178] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime:blueprint (24s)
✔ [4120/4178] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app:blueprint (20s)
✔ [4121/4178] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_tables:blueprint (8.6s)
⚠ [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 (27s)
✔ [4136/4198] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_a2_bounds:blueprint (7.8s)
ℹ [4139/4198] 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.
✔ [4140/4200] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core:blueprint (3.3s)
✔ [4161/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_next:blueprint (3.2s)
✔ [4162/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_values:blueprint (3.2s)
✔ [4164/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_65_85:blueprint (3.2s)
✔ [4165/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_90_95:blueprint (3.3s)
✔ [4166/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_100_1875:blueprint (3.3s)
✔ [4167/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_1900_2375:blueprint (3.4s)
✔ [4168/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2400_2875:blueprint (3.4s)
✔ [4169/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_2900_3375:blueprint (3.4s)
✔ [4170/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3400_3875:blueprint (3.3s)
✔ [4171/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_3900_4375:blueprint (3.3s)
✔ [4172/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4400_4875:blueprint (3.3s)
✔ [4173/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_4900_6500:blueprint (3.3s)
✔ [4174/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_6600_8500:blueprint (3.3s)
✔ [4175/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_8600_10500:blueprint (3.4s)
✔ [4176/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_10600_12500:blueprint (3.3s)
✔ [4177/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_regime3_12600_24000:blueprint (3.5s)
✔ [4178/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_misc:blueprint (3.2s)
✔ [4179/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1:blueprint (51s)
⚠ [4180/4208] Replayed PrimeNumberTheoremAnd.IEANTN.CH2.CH2
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3156:8: declaration uses `sorry`
info: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3245:4: Try this:
[apply] ring_nf
The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3572:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3819:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3833:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3847:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3859:8: declaration uses `sorry`
✔ [4182/4208] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimeInInterval:blueprint (4.7s)
⚠ [4184/4208] 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/4209] Replayed PrimeNumberTheoremAnd.IEANTN.FKS2
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:315: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`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3776:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4432:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4454:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/FKS2.lean:4481:8: declaration uses `sorry`
✔ [4190/4209] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.CH2.CH2:blueprint (19s)
⚠ [4193/4209] 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:747:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:759:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:771:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:783:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:795:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:807:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Dusart.lean:819:8: declaration uses `sorry`
✔ [4195/4210] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_20_43:blueprint (3.4s)
✔ [4197/4210] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.FKS2:blueprint (32s)
✔ [4200/4211] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_44_59:blueprint (3.5s)
✔ [4202/4211] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Chebyshev:blueprint (18s)
✔ [4203/4211] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Dusart:blueprint (19s)
✔ [4206/4214] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows:blueprint (3.2s)
✔ [4208/4214] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Erdos392:blueprint (17s)
✔ [4211/4217] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_dispatch:blueprint (17s)
⚠ [4219/4238] 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`
✔ [4221/4238] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting:blueprint (75s)
✔ [4229/4306] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RSPrimeLower:blueprint (21s)
⚠ [4230/4306] Replayed PrimeNumberTheoremAnd.IEANTN.TMEEMT
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:51:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:62:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:73:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:84:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:100:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:108:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:133:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:141:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:149:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:287:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:295:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:424:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:469:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:484:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:518:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:527:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:536:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:545:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:554:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:570:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:579:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:588:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:597:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:632:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:641:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:650:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:676:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:699:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:710:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:721:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:732:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:742:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:750:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:759:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:768:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:891:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:911:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:941:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:967:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:981:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:989:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1004:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1019:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1028:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1043:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1061:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1073:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1090:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1101:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1123:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1137:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1151:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1181:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1197:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1208:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1232:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1246:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1260:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1274:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1288:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/TMEEMT.lean:1323:8: declaration uses `sorry`
✔ [4249/4321] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.TMEEMT:blueprint (49s)
⚠ [4257/4331] Replayed PrimeNumberTheoremAnd.IEANTN.SecondarySummary
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:60:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:203:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:213:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:227:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:242:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:255:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:337:8: declaration uses `sorry`
✔ [4276/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.SecondarySummary:blueprint (10s)
⚠ [4281/4343] Replayed PrimeNumberTheoremAnd.IEANTN.Goldbach
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:155:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Goldbach.lean:182:8: declaration uses `sorry`
⚠ [4290/4343] 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`
✔ [4292/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.MobiusLemma:blueprint (11s)
✔ [4295/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Goldbach:blueprint (6.6s)
✔ [4303/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Lcm:blueprint (11s)
✔ [4309/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.PrimarySummary:blueprint (3.1s)
ℹ [4319/4343] 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.
✔ [4332/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan:blueprint (16s)
⚠ [4338/4343] Replayed PrimeNumberTheoremAnd.IEANTN.Kadiri
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:130:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:167:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:204:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:275:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:323:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:355:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:714:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:749:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:792:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:879:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:962:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2192:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2218:8: declaration uses `sorry`
warning: PrimeNumberTheoremAnd/IEANTN/Kadiri.lean:2824:8: declaration uses `sorry`
✔ [4339/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd.IEANTN.Kadiri:blueprint (53s)
✔ [4341/4343] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (22s)
ℹ [4342/4344] Built PrimeNumberTheoremAnd/PrimeNumberTheoremAnd:blueprint (165ms)
info: Blueprint indexing
Build completed successfully (4344 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 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-stable-superset)
.apodeixis/lean-runner/RepositorySemanticRunner.lean:1:0: error: object file '/apx/source/.lake/packages/leancert/.lake/build/lib/lean/LeanCert/ANT/Asymp.olean' of module LeanCert.ANT.Asymp does not exist
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"core_compile","duration_ms":23253}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":11216,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":24,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper failed: helper support module '.apodeixis/lean-runner/RepositorySemanticRunner.lean' did not compile
remediation: inspect the generated helper support sources under .apodeixis/lean-runner
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00000)
.apodeixis/lean-runner/RepositorySemanticRunner.lean:1:0: error: object file '/apx/source/.lake/packages/leancert/.lake/build/lib/lean/LeanCert/ANT/Asymp.olean' of module LeanCert.ANT.Asymp does not exist
apx-semantic-phase {"phase":"core_compile","duration_ms":24}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":113,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":24,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper failed: helper support module '.apodeixis/lean-runner/RepositorySemanticRunner.lean' did not compile
remediation: inspect the generated helper support sources under .apodeixis/lean-runner
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00001)
apx-semantic-phase {"duration_ms":41,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":150,"diagnostic_count":101,"duration_ms":12084,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":150,"dependency_count":111,"diagnostic_count":242,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":484301,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":150,"dependency_count":111,"diagnostic_count":242,"duration_ms":165,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":930453,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":6,"ok":true,"payload_bytes":930453,"phase":"lean_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":24}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":153,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":14,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":247780,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 071474aaab06ac48322d22feed6b213f258ca14becb7bdb8a3f374972386fc44
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":729199,"ok":true}
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00002-a)
.apodeixis/lean-runner/RepositorySemanticRunner.lean:1:0: error: object file '/apx/source/.lake/packages/leancert/.lake/build/lib/lean/LeanCert/ANT/Asymp.olean' of module LeanCert.ANT.Asymp does not exist
apx-semantic-phase {"phase":"core_compile","duration_ms":24}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":121,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":11,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper failed: helper support module '.apodeixis/lean-runner/RepositorySemanticRunner.lean' did not compile
remediation: inspect the generated helper support sources under .apodeixis/lean-runner
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00002-b)
.apodeixis/lean-runner/RepositorySemanticRunner.lean:1:0: error: object file '/apx/source/.lake/packages/leancert/.lake/build/lib/lean/LeanCert/ANT/Asymp.olean' of module LeanCert.ANT.Asymp does not exist
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":155,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":23,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper failed: helper support module '.apodeixis/lean-runner/RepositorySemanticRunner.lean' did not compile
remediation: inspect the generated helper support sources under .apodeixis/lean-runner
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00003-a)
.apodeixis/lean-runner/RepositorySemanticRunner.lean:1:0: error: object file '/apx/source/.lake/packages/leancert/.lake/build/lib/lean/LeanCert/ANT/Asymp.olean' of module LeanCert.ANT.Asymp does not exist
apx-semantic-phase {"phase":"core_compile","duration_ms":21}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":140,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":23,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper failed: helper support module '.apodeixis/lean-runner/RepositorySemanticRunner.lean' did not compile
remediation: inspect the generated helper support sources under .apodeixis/lean-runner
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00003-b)
.apodeixis/lean-runner/RepositorySemanticRunner.lean:1:0: error: object file '/apx/source/.lake/packages/leancert/.lake/build/lib/lean/LeanCert/ANT/Asymp.olean' of module LeanCert.ANT.Asymp does not exist
apx-semantic-phase {"phase":"core_compile","duration_ms":24}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":179,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":26,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper failed: helper support module '.apodeixis/lean-runner/RepositorySemanticRunner.lean' did not compile
remediation: inspect the generated helper support sources under .apodeixis/lean-runner
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00004-a)
.apodeixis/lean-runner/RepositorySemanticRunner.lean:1:0: error: object file '/apx/source/.lake/packages/leancert/.lake/build/lib/lean/LeanCert/ANT/Asymp.olean' of module LeanCert.ANT.Asymp does not exist
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":157,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":25,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper failed: helper support module '.apodeixis/lean-runner/RepositorySemanticRunner.lean' did not compile
remediation: inspect the generated helper support sources under .apodeixis/lean-runner
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00004-b)
.apodeixis/lean-runner/RepositorySemanticRunner.lean:1:0: error: object file '/apx/source/.lake/packages/leancert/.lake/build/lib/lean/LeanCert/ANT/Asymp.olean' of module LeanCert.ANT.Asymp does not exist
apx-semantic-phase {"phase":"core_compile","duration_ms":21}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":174,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":25,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper failed: helper support module '.apodeixis/lean-runner/RepositorySemanticRunner.lean' did not compile
remediation: inspect the generated helper support sources under .apodeixis/lean-runner
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00005-a)
.apodeixis/lean-runner/RepositorySemanticRunner.lean:1:0: error: object file '/apx/source/.lake/packages/leancert/.lake/build/lib/lean/LeanCert/ANT/Asymp.olean' of module LeanCert.ANT.Asymp does not exist
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":146,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":21,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper failed: helper support module '.apodeixis/lean-runner/RepositorySemanticRunner.lean' did not compile
remediation: inspect the generated helper support sources under .apodeixis/lean-runner
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00005-b)
.apodeixis/lean-runner/RepositorySemanticRunner.lean:1:0: error: object file '/apx/source/.lake/packages/leancert/.lake/build/lib/lean/LeanCert/ANT/Asymp.olean' of module LeanCert.ANT.Asymp does not exist
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":480,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":19,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper failed: helper support module '.apodeixis/lean-runner/RepositorySemanticRunner.lean' did not compile
remediation: inspect the generated helper support sources under .apodeixis/lean-runner
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00006-a)
.apodeixis/lean-runner/RepositorySemanticRunner.lean:1:0: error: object file '/apx/source/.lake/packages/leancert/.lake/build/lib/lean/LeanCert/ANT/Asymp.olean' of module LeanCert.ANT.Asymp does not exist
apx-semantic-phase {"phase":"core_compile","duration_ms":14}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":128,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":19,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper failed: helper support module '.apodeixis/lean-runner/RepositorySemanticRunner.lean' did not compile
remediation: inspect the generated helper support sources under .apodeixis/lean-runner
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00006-b)
.apodeixis/lean-runner/RepositorySemanticRunner.lean:1:0: error: object file '/apx/source/.lake/packages/leancert/.lake/build/lib/lean/LeanCert/ANT/Asymp.olean' of module LeanCert.ANT.Asymp does not exist
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":194,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":24,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper failed: helper support module '.apodeixis/lean-runner/RepositorySemanticRunner.lean' did not compile
remediation: inspect the generated helper support sources under .apodeixis/lean-runner
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00007-a)
.apodeixis/lean-runner/RepositorySemanticRunner.lean:1:0: error: object file '/apx/source/.lake/packages/leancert/.lake/build/lib/lean/LeanCert/ANT/Asymp.olean' of module LeanCert.ANT.Asymp does not exist
apx-semantic-phase {"phase":"core_compile","duration_ms":20}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":135,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":23,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper failed: helper support module '.apodeixis/lean-runner/RepositorySemanticRunner.lean' did not compile
remediation: inspect the generated helper support sources under .apodeixis/lean-runner
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00007-b)
.apodeixis/lean-runner/RepositorySemanticRunner.lean:1:0: error: object file '/apx/source/.lake/packages/leancert/.lake/build/lib/lean/LeanCert/ANT/Asymp.olean' of module LeanCert.ANT.Asymp does not exist
apx-semantic-phase {"phase":"core_compile","duration_ms":11}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":159,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":24,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper failed: helper support module '.apodeixis/lean-runner/RepositorySemanticRunner.lean' did not compile
remediation: inspect the generated helper support sources under .apodeixis/lean-runner
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00008-a)
.apodeixis/lean-runner/RepositorySemanticRunner.lean:1:0: error: object file '/apx/source/.lake/packages/leancert/.lake/build/lib/lean/LeanCert/ANT/Asymp.olean' of module LeanCert.ANT.Asymp does not exist
apx-semantic-phase {"phase":"core_compile","duration_ms":22}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":166,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":10,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
lean semantic helper failed: helper support module '.apodeixis/lean-runner/RepositorySemanticRunner.lean' did not compile
remediation: inspect the generated helper support sources under .apodeixis/lean-runner
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00008-b)
.apodeixis/lean-runner/RepositorySemanticRun.lean:1:0: error: object file '/apx/source/.lake/packages/leancert/.lake/build/lib/lean/LeanCert/ANT/Asymp.olean' of module LeanCert.ANT.Asymp does not exist
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":206,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache cae750046114722b09a8e3704629027638efe6aeeb2025b674540c0c4aa8d420
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":2337,"ok":false}
lean semantic helper failed: generated static runner exited non-zero
remediation: inspect the generated repository runner and imported root modules
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00009)
apx-semantic-phase {"duration_ms":3,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":41,"diagnostic_count":6,"duration_ms":3142,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":41,"dependency_count":37,"diagnostic_count":9,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":475245,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":41,"dependency_count":37,"diagnostic_count":9,"duration_ms":119,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":355715,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":5,"ok":true,"payload_bytes":355715,"phase":"lean_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":19}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":124,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache e4b42e55817c080a724ce408535b0c0d4c3a60c2c17ba73d8ed5359158620ce8
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":27,"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":510579,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00010)
apx-semantic-phase {"duration_ms":235,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":255,"diagnostic_count":136,"duration_ms":19851,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":255,"dependency_count":329,"diagnostic_count":198,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":454759,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":255,"dependency_count":329,"diagnostic_count":198,"duration_ms":231,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":1366471,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":17,"ok":true,"payload_bytes":1366471,"phase":"lean_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":19}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":396,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":17,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":48467,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 7ff5246c1e00973820a8d237012b69f5031ecaf965ddb2bbb0b37dcddfa1c349
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":482684,"ok":true}
semantic_extract exit 1
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00015)
.apodeixis/lean-runner/RepositorySemanticRun.lean:1:0: error: object file '/apx/source/.lake/packages/leancert/.lake/build/lib/lean/LeanCert/ANT/Asymp.olean' of module LeanCert.ANT.Asymp does not exist
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":1362,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache da9f756dea6de60400adc70233ed9274c380658d1444e316dba3809092e0957d
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":10085,"ok":false}
lean semantic helper failed: generated static runner exited non-zero
remediation: inspect the generated repository runner and imported root modules
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00011)
apx-semantic-phase {"duration_ms":25,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":67,"diagnostic_count":53,"duration_ms":5367,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":67,"dependency_count":60,"diagnostic_count":53,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":479887,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":67,"dependency_count":60,"diagnostic_count":53,"duration_ms":422,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":270148,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":8,"ok":true,"payload_bytes":270148,"phase":"lean_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":2222,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":25,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":76331,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 2dcd93d4adeb7db279f4d9b70d24077b98ca9e248f8fea4e5d1a5464cd8a04b1
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":506842,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00012)
apx-semantic-phase {"duration_ms":101,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":70,"diagnostic_count":54,"duration_ms":4848,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":70,"dependency_count":75,"diagnostic_count":54,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":481928,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":70,"dependency_count":75,"diagnostic_count":54,"duration_ms":106,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":415546,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":4,"ok":true,"payload_bytes":415546,"phase":"lean_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":9}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":635,"runner_cache_enabled":true}
lean semantic helper: restored compiled static runner cache 7c7e15aaa4b0f4fda4874fe7acaf801d6891b0ed704d7efee8b308653c879011
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":46,"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":581701,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00013)
apx-semantic-phase {"duration_ms":29,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":235,"diagnostic_count":164,"duration_ms":18234,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":235,"dependency_count":633,"diagnostic_count":533,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":495255,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":235,"dependency_count":633,"diagnostic_count":533,"duration_ms":935,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":1764949,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":8,"ok":true,"payload_bytes":1764949,"phase":"lean_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":21}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":1744,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":27,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":78193,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache e30f7a7702153b0e76deba6a67b3462973f6915fdc008d975521c302e0bc73aa
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":528204,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00014)
apx-semantic-phase {"duration_ms":30,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":263,"diagnostic_count":178,"duration_ms":22905,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":263,"dependency_count":583,"diagnostic_count":199,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":502769,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":263,"dependency_count":583,"diagnostic_count":199,"duration_ms":215,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":1968805,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":10,"ok":true,"payload_bytes":1968805,"phase":"lean_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":19}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":1950,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":11,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":122556,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache 8662e5f1451bce3be4a746d7a1ff8e8c547708ef504f0e8382d7ed2add740a0a
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":538977,"ok":true}
semantic_extract exit 0
./.apodeixis/tools/lean-semantic-extract.sh (extract-batch-00016)
apx-semantic-phase {"duration_ms":29,"ok":true,"phase":"lean_request_parse"}
apx-semantic-phase {"declaration_count":0,"diagnostic_count":0,"duration_ms":35,"ok":true,"phase":"lean_declaration_extraction","target_module_count":1}
apx-semantic-phase {"declaration_count":0,"dependency_count":0,"diagnostic_count":0,"duration_ms":0,"ok":true,"phase":"lean_dependency_build"}
apx-semantic-phase {"duration_ms":505852,"module_count":1,"ok":true,"phase":"lean_module_facts","target_module_count":1}
apx-semantic-phase {"declaration_count":0,"dependency_count":0,"diagnostic_count":0,"duration_ms":113,"module_count":1,"ok":true,"phase":"lean_response_build"}
apx-semantic-phase {"duration_ms":0,"ok":true,"payload_bytes":772,"phase":"lean_json_serialize"}
apx-semantic-phase {"duration_ms":16,"ok":true,"payload_bytes":772,"phase":"lean_json_write"}
apx-semantic-phase {"phase":"core_compile","duration_ms":23}
apx-semantic-phase {"phase":"runner_cache_key","duration_ms":475,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_lookup","duration_ms":27,"runner_cache_hit":false}
warning: mathlib: repository '/apx/source/.lake/packages/mathlib' has local changes
warning: batteries: repository '/apx/source/.lake/packages/batteries' has local changes
apx-semantic-phase {"phase":"runner_compile","duration_ms":76649,"runner_cache_enabled":true}
apx-semantic-phase {"phase":"runner_cache_store","duration_ms":0,"runner_cache_enabled":true}
lean semantic helper: stored compiled static runner cache c51de46e3f0cacd534b1130418e5a64c4b80713514cbedc4176f2630a787bfa3
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":518200,"ok":true}