Verification run
Run 4
failed commit
manual toolchain lean-v4-31-0-rc1 prover lean took 23m 17s · finished 6w ago ./.apodeixis/tools/lean-semantic-extract.sh failed with exit code 137 (toolchain lean-v4-31-0-rc1, command: elan run leanprover/lean4:v4.31.0-rc1 -- bash -c export PATH="$(dirname "$(elan which lean)"):$PATH"; exec "$@" apx-lean-phase ./.apodeixis/tools/lean-semantic-extract.sh)
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
(no log excerpt)
Command runs
git_clone exit 0
git clone --depth 1 --branch main --single-branch https://github.com/ImperialCollegeLondon/FLT.git /var/lib/apodeixis/repos/job-45-source
Cloning into '/var/lib/apodeixis/repos/job-45-source'...
lake_cache exit 0
lake exe cache get
Current branch: HEAD Using cache (Azure) from origin: (some leanprover-community/mathlib4) Attempting to download 8477 file(s) from leanprover-community/mathlib4 cache Decompressed 8477 file(s) Already decompressed 8477 file(s)
info: checkdecls: cloning https://github.com/PatrickMassot/checkdecls.git info: checkdecls: checking out revision '3d425859e73fcfbef85b9638c2a91708ef4a22d4' info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git info: mathlib: checking out revision 'd568c8c09630de097a046763c17b9ea99f95f950' info: plausible: cloning https://github.com/leanprover-community/plausible info: plausible: checking out revision 'd575be693add4fe9cb996968968ce42ce75c5ccd' info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient info: LeanSearchClient: checking out revision 'c5d5b8fe6e5158def25cd28eb94e4141ad97c843' info: importGraph: cloning https://github.com/leanprover-community/import-graph info: importGraph: checking out revision '6db47de43aa7f516708053ae2fdadd29dd9baaaa' info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4 info: proofwidgets: checking out revision '85bb7e7637e84a7d9803be7d954579fdae42c64b' info: aesop: cloning https://github.com/leanprover-community/aesop info: aesop: checking out revision 'fafca80479ff95e041d84373dda7122adf1295f2' info: Qq: cloning https://github.com/leanprover-community/quote4 info: Qq: checking out revision '8d33324ee877e9735d2829bc6f1f439e60cf98b1' info: batteries: cloning https://github.com/leanprover-community/batteries info: batteries: checking out revision '708b057842c4cd0845fba132bd94b08493f6fc42' info: Cli: cloning https://github.com/leanprover/lean4-cli info: Cli: checking out revision '48bdcff4c5fa27e09028f9f330e59baa0d4640cf' ✔ [4/24] Built Batteries.Data.String.Basic (574ms) ✔ [5/24] Built Cache.Lean (575ms) ✔ [6/24] Built Cache.Init (375ms) ✔ [7/24] Built Batteries.Data.Array.Match (1.0s) ✔ [8/24] Built Batteries.Data.String.Basic:c.o (578ms) ✔ [9/24] Built Cache.Lean:c.o (185ms) ✔ [10/24] Built Cache.Init:c.o (148ms) ✔ [11/24] Built Batteries.Tactic.OpenPrivate (1.2s) ✔ [12/24] Built Batteries.Data.Array.Match:c.o (220ms) ✔ [13/24] Built Batteries.Data.String.Matcher (391ms) ✔ [14/24] Built Batteries.Data.String.Matcher:c.o (155ms) ✔ [15/24] Built Batteries.Tactic.OpenPrivate:c.o (1.0s) ✔ [16/24] Built Cache.IO (1.7s) ✔ [17/24] Built Cache.Hashing (931ms) ✔ [18/24] Built Cache.IO:c.o (1.2s) ✔ [19/24] Built Cache.Hashing:c.o (342ms) ✔ [20/24] Built Cache.Requests (2.1s) ✔ [21/24] Built Cache.Main (1.0s) ✔ [22/24] Built Cache.Main:c.o (504ms) ✔ [23/24] Built Cache.Requests:c.o (1.8s) ✔ [24/24] Built cache:exe (2.4s) Downloaded: 1 file(s) [attempted 1/8477 = 0%, 9 KB/s], Decompressed: 0 Downloaded: 14 file(s) [attempted 14/8477 = 0%, 4 KB/s], Decompressed: 12 Downloaded: 39 file(s) [attempted 39/8477 = 0%, 14 KB/s], Decompressed: 33 Downloaded: 69 file(s) [attempted 69/8477 = 0%, 42 KB/s], Decompressed: 58 Downloaded: 96 file(s) [attempted 96/8477 = 1%, 74 KB/s], Decompressed: 83 Downloaded: 127 file(s) [attempted 127/8477 = 1%, 278 KB/s], Decompressed: 110 Downloaded: 158 file(s) [attempted 158/8477 = 1%, 77 KB/s], Decompressed: 127 Downloaded: 196 file(s) [attempted 196/8477 = 2%, 514 KB/s], Decompressed: 169 Downloaded: 230 file(s) [attempted 230/8477 = 2%, 222 KB/s], Decompressed: 192 Downloaded: 271 file(s) [attempted 271/8477 = 3%, 433 KB/s], Decompressed: 223 Downloaded: 316 file(s) [attempted 316/8477 = 3%, 154 KB/s], Decompressed: 254 Downloaded: 350 file(s) [attempted 350/8477 = 4%, 21 KB/s], Decompressed: 254 Downloaded: 391 file(s) [attempted 391/8477 = 4%, 120 KB/s], Decompressed: 299 Downloaded: 429 file(s) [attempted 429/8477 = 5%, 55 KB/s], Decompressed: 299 Downloaded: 470 file(s) [attempted 470/8477 = 5%, 78 KB/s], Decompressed: 367 Downloaded: 511 file(s) [attempted 511/8477 = 6%, 887 KB/s], Decompressed: 367 Downloaded: 545 file(s) [attempted 545/8477 = 6%, 181 KB/s], Decompressed: 439 Downloaded: 586 file(s) [attempted 586/8477 = 6%, 19 KB/s], Decompressed: 439 Downloaded: 627 file(s) [attempted 627/8477 = 7%, 156 KB/s], Decompressed: 518 Downloaded: 662 file(s) [attempted 662/8477 = 7%, 150 KB/s], Decompressed: 518 Downloaded: 706 file(s) [attempted 706/8477 = 8%, 83 KB/s], Decompressed: 518 Downloaded: 747 file(s) [attempted 747/8477 = 8%, 387 KB/s], Decompressed: 518 Downloaded: 788 file(s) [attempted 788/8477 = 9%, 387 KB/s], Decompressed: 624 Downloaded: 830 file(s) [attempted 830/8477 = 9%, 532 KB/s], Decompressed: 624 Downloaded: 867 file(s) [attempted 867/8477 = 10%, 37 KB/s], Decompressed: 624 Downloaded: 908 file(s) [attempted 908/8477 = 10%, 46 KB/s], Decompressed: 754 Downloaded: 949 file(s) [attempted 949/8477 = 11%, 410 KB/s], Decompressed: 754 Downloaded: 987 file(s) [attempted 987/8477 = 11%, 112 KB/s], Decompressed: 754 Downloaded: 1021 file(s) [attempted 1021/8477 = 12%, 236 KB/s], Decompressed: 754 Downloaded: 1062 file(s) [attempted 1062/8477 = 12%, 695 KB/s], Decompressed: 898 Downloaded: 1104 file(s) [attempted 1104/8477 = 13%, 73 KB/s], Decompressed: 898 Downloaded: 1145 file(s) [attempted 1145/8477 = 13%, 124 KB/s], Decompressed: 898 Downloaded: 1176 file(s) [attempted 1176/8477 = 13%, 40 KB/s], Decompressed: 898 Downloaded: 1216 file(s) [attempted 1216/8477 = 14%, 187 KB/s], Decompressed: 898 Downloaded: 1258 file(s) [attempted 1258/8477 = 14%, 41 KB/s], Decompressed: 1062 Downloaded: 1299 file(s) [attempted 1299/8477 = 15%, 1962 KB/s], Decompressed: 1062 Downloaded: 1340 file(s) [attempted 1340/8477 = 15%, 131 KB/s], Decompressed: 1062 Downloaded: 1377 file(s) [attempted 1377/8477 = 16%, 1162 KB/s], Decompressed: 1062 Downloaded: 1415 file(s) [attempted 1415/8477 = 16%, 93 KB/s], Decompressed: 1062 Downloaded: 1449 file(s) [attempted 1449/8477 = 17%, 277 KB/s], Decompressed: 1062 Downloaded: 1494 file(s) [attempted 1494/8477 = 17%, 366 KB/s], Decompressed: 1254 Downloaded: 1538 file(s) [attempted 1538/8477 = 18%, 163 KB/s], Decompressed: 1254 Downloaded: 1579 file(s) [attempted 1579/8477 = 18%, 595 KB/s], Decompressed: 1254 Downloaded: 1610 file(s) [attempted 1610/8477 = 18%, 329 KB/s], Decompressed: 1254 Downloaded: 1644 file(s) [attempted 1644/8477 = 19%, 628 KB/s], Decompressed: 1254 Downloaded: 1682 file(s) [attempted 1682/8477 = 19%, 93 KB/s], Decompressed: 1254 Downloaded: 1723 file(s) [attempted 1723/8477 = 20%, 143 KB/s], Decompressed: 1254 Downloaded: 1761 file(s) [attempted 1761/8477 = 20%, 940 KB/s], Decompressed: 1483 Downloaded: 1798 file(s) [attempted 1798/8477 = 21%, 183 KB/s], Decompressed: 1483 Downloaded: 1839 file(s) [attempted 1839/8477 = 21%, 95 KB/s], Decompressed: 1483 Downloaded: 1880 file(s) [attempted 1880/8477 = 22%, 1465 KB/s], Decompressed: 1483 Downloaded: 1921 file(s) [attempted 1921/8477 = 22%, 386 KB/s], Decompressed: 1483 Downloaded: 1959 file(s) [attempted 1959/8477 = 23%, 198 KB/s], Decompressed: 1483 Downloaded: 1997 file(s) [attempted 1997/8477 = 23%, 65 KB/s], Decompressed: 1483 Downloaded: 2034 file(s) [attempted 2034/8477 = 23%, 650 KB/s], Decompressed: 1733 Downloaded: 2079 file(s) [attempted 2079/8477 = 24%, 250 KB/s], Decompressed: 1733 Downloaded: 2123 file(s) [attempted 2123/8477 = 25%, 116 KB/s], Decompressed: 1733 Downloaded: 2164 file(s) [attempted 2164/8477 = 25%, 402 KB/s], Decompressed: 1733 Downloaded: 2202 file(s) [attempted 2202/8477 = 25%, 140 KB/s], Decompressed: 1733 Downloaded: 2236 file(s) [attempted 2236/8477 = 26%, 316 KB/s], Decompressed: 1733 Downloaded: 2274 file(s) [attempted 2274/8477 = 26%, 557 KB/s], Decompressed: 1733 Downloaded: 2318 file(s) [attempted 2318/8477 = 27%, 111 KB/s], Decompressed: 1733 Downloaded: 2360 file(s) [attempted 2360/8477 = 27%, 48 KB/s], Decompressed: 2004 Downloaded: 2397 file(s) [attempted 2397/8477 = 28%, 41 KB/s], Decompressed: 2004 Downloaded: 2435 file(s) [attempted 2435/8477 = 28%, 487 KB/s], Decompressed: 2004 Downloaded: 2472 file(s) [attempted 2472/8477 = 29%, 239 KB/s], Decompressed: 2004 Downloaded: 2520 file(s) [attempted 2520/8477 = 29%, 117 KB/s], Decompressed: 2004 Downloaded: 2565 file(s) [attempted 2565/8477 = 30%, 793 KB/s], Decompressed: 2004 Downloaded: 2603 file(s) [attempted 2603/8477 = 30%, 1786 KB/s], Decompressed: 2004 Downloaded: 2644 file(s) [attempted 2644/8477 = 31%, 35 KB/s], Decompressed: 2004 Downloaded: 2678 file(s) [attempted 2678/8477 = 31%, 531 KB/s], Decompressed: 2004 Downloaded: 2719 file(s) [attempted 2719/8477 = 32%, 77 KB/s], Decompressed: 2325 Downloaded: 2763 file(s) [attempted 2763/8477 = 32%, 1142 KB/s], Decompressed: 2325 Downloaded: 2801 file(s) [attempted 2801/8477 = 33%, 152 KB/s], Decompressed: 2325 Downloaded: 2839 file(s) [attempted 2839/8477 = 33%, 1301 KB/s], Decompressed: 2325 Downloaded: 2876 file(s) [attempted 2876/8477 = 33%, 611 KB/s], Decompressed: 2325 Downloaded: 2917 file(s) [attempted 2917/8477 = 34%, 235 KB/s], Decompressed: 2325 Downloaded: 2958 file(s) [attempted 2958/8477 = 34%, 628 KB/s], Decompressed: 2325 Downloaded: 2996 file(s) [attempted 2996/8477 = 35%, 296 KB/s], Decompressed: 2325 Downloaded: 3037 file(s) [attempted 3037/8477 = 35%, 52 KB/s], Decompressed: 2325 Downloaded: 3078 file(s) [attempted 3078/8477 = 36%, 190 KB/s], Decompressed: 2325 Downloaded: 3119 file(s) [attempted 3119/8477 = 36%, 425 KB/s], Decompressed: 2325 Downloaded: 3160 file(s) [attempted 3160/8477 = 37%, 220 KB/s], Decompressed: 2695 Downloaded: 3201 file(s) [attempted 3201/8477 = 37%, 286 KB/s], Decompressed: 2695 Downloaded: 3239 file(s) [attempted 3239/8477 = 38%, 169 KB/s], Decompressed: 2695 Downloaded: 3280 file(s) [attempted 3280/8477 = 38%, 97 KB/s], Decompressed: 2695 Downloaded: 3318 file(s) [attempted 3318/8477 = 39%, 200 KB/s], Decompressed: 2695 Downloaded: 3359 file(s) [attempted 3359/8477 = 39%, 263 KB/s], Decompressed: 2695 Downloaded: 3403 file(s) [attempted 3403/8477 = 40%, 1104 KB/s], Decompressed: 2695 Downloaded: 3444 file(s) [attempted 3444/8477 = 40%, 252 KB/s], Decompressed: 2695 Downloaded: 3479 file(s) [attempted 3479/8477 = 41%, 47 KB/s], Decompressed: 2695 Downloaded: 3523 file(s) [attempted 3523/8477 = 41%, 193 KB/s], Decompressed: 2695 Downloaded: 3568 file(s) [attempted 3568/8477 = 42%, 420 KB/s], Decompressed: 2695 Downloaded: 3598 file(s) [attempted 3598/8477 = 42%, 548 KB/s], Decompressed: 2695 Downloaded: 3646 file(s) [attempted 3646/8477 = 43%, 134 KB/s], Decompressed: 3136 Downloaded: 3684 file(s) [attempted 3684/8477 = 43%, 75 KB/s], Decompressed: 3136 Downloaded: 3722 file(s) [attempted 3722/8477 = 43%, 168 KB/s], Decompressed: 3136 Downloaded: 3763 file(s) [attempted 3763/8477 = 44%, 658 KB/s], Decompressed: 3136 Downloaded: 3804 file(s) [attempted 3804/8477 = 44%, 283 KB/s], Decompressed: 3136 Downloaded: 3848 file(s) [attempted 3848/8477 = 45%, 398 KB/s], Decompressed: 3136 Downloaded: 3889 file(s) [attempted 3889/8477 = 45%, 103 KB/s], Decompressed: 3136 Downloaded: 3927 file(s) [attempted 3927/8477 = 46%, 48 KB/s], Decompressed: 3136 Downloaded: 3961 file(s) [attempted 3961/8477 = 46%, 398 KB/s], Decompressed: 3136 Downloaded: 4006 file(s) [attempted 4006/8477 = 47%, 280 KB/s], Decompressed: 3136 Downloaded: 4040 file(s) [attempted 4040/8477 = 47%, 931 KB/s], Decompressed: 3136 Downloaded: 4081 file(s) [attempted 4081/8477 = 48%, 132 KB/s], Decompressed: 3136 Downloaded: 4115 file(s) [attempted 4115/8477 = 48%, 376 KB/s], Decompressed: 3136 Downloaded: 4153 file(s) [attempted 4153/8477 = 48%, 957 KB/s], Decompressed: 3136 Downloaded: 4190 file(s) [attempted 4190/8477 = 49%, 974 KB/s], Decompressed: 3136 Downloaded: 4228 file(s) [attempted 4228/8477 = 49%, 411 KB/s], Decompressed: 3639 Downloaded: 4262 file(s) [attempted 4262/8477 = 50%, 34 KB/s], Decompressed: 3639 Downloaded: 4293 file(s) [attempted 4293/8477 = 50%, 126 KB/s], Decompressed: 3639 Downloaded: 4334 file(s) [attempted 4334/8477 = 51%, 716 KB/s], Decompressed: 3639 Downloaded: 4379 file(s) [attempted 4379/8477 = 51%, 203 KB/s], Decompressed: 3639 Downloaded: 4420 file(s) [attempted 4420/8477 = 52%, 84 KB/s], Decompressed: 3639 Downloaded: 4457 file(s) [attempted 4457/8477 = 52%, 196 KB/s], Decompressed: 3639 Downloaded: 4495 file(s) [attempted 4495/8477 = 53%, 370 KB/s], Decompressed: 3639 Downloaded: 4529 file(s) [attempted 4529/8477 = 53%, 299 KB/s], Decompressed: 3639 Downloaded: 4574 file(s) [attempted 4574/8477 = 53%, 945 KB/s], Decompressed: 3639 Downloaded: 4611 file(s) [attempted 4611/8477 = 54%, 393 KB/s], Decompressed: 3639 Downloaded: 4649 file(s) [attempted 4649/8477 = 54%, 519 KB/s], Decompressed: 3639 Downloaded: 4687 file(s) [attempted 4687/8477 = 55%, 540 KB/s], Decompressed: 3639 Downloaded: 4728 file(s) [attempted 4728/8477 = 55%, 286 KB/s], Decompressed: 3639 Downloaded: 4772 file(s) [attempted 4772/8477 = 56%, 22 KB/s], Decompressed: 3639 Downloaded: 4810 file(s) [attempted 4810/8477 = 56%, 384 KB/s], Decompressed: 3639 Downloaded: 4848 file(s) [attempted 4848/8477 = 57%, 594 KB/s], Decompressed: 3639 Downloaded: 4885 file(s) [attempted 4885/8477 = 57%, 182 KB/s], Decompressed: 4214 Downloaded: 4926 file(s) [attempted 4926/8477 = 58%, 49 KB/s], Decompressed: 4214 Downloaded: 4964 file(s) [attempted 4964/8477 = 58%, 115 KB/s], Decompressed: 4214 Downloaded: 5002 file(s) [attempted 5002/8477 = 59%, 50 KB/s], Decompressed: 4214 Downloaded: 5046 file(s) [attempted 5046/8477 = 59%, 310 KB/s], Decompressed: 4214 Downloaded: 5080 file(s) [attempted 5080/8477 = 59%, 47 KB/s], Decompressed: 4214 Downloaded: 5124 file(s) [attempted 5124/8477 = 60%, 143 KB/s], Decompressed: 4214 Downloaded: 5159 file(s) [attempted 5159/8477 = 60%, 121 KB/s], Decompressed: 4214 Downloaded: 5200 file(s) [attempted 5200/8477 = 61%, 112 KB/s], Decompressed: 4214 Downloaded: 5238 file(s) [attempted 5238/8477 = 61%, 70 KB/s], Decompressed: 4214 Downloaded: 5275 file(s) [attempted 5275/8477 = 62%, 498 KB/s], Decompressed: 4214 Downloaded: 5316 file(s) [attempted 5316/8477 = 62%, 153 KB/s], Decompressed: 4214 Downloaded: 5354 file(s) [attempted 5354/8477 = 63%, 156 KB/s], Decompressed: 4214 Downloaded: 5395 file(s) [attempted 5395/8477 = 63%, 315 KB/s], Decompressed: 4214 Downloaded: 5442 file(s) [attempted 5442/8477 = 64%, 65 KB/s], Decompressed: 4214 Downloaded: 5481 file(s) [attempted 5481/8477 = 64%, 578 KB/s], Decompressed: 4214 Downloaded: 5518 file(s) [attempted 5518/8477 = 65%, 1187 KB/s], Decompressed: 4214 Downloaded: 5542 file(s) [attempted 5542/8477 = 65%, 75 KB/s], Decompressed: 4214 Downloaded: 5590 file(s) [attempted 5590/8477 = 65%, 497 KB/s], Decompressed: 4214 Downloaded: 5638 file(s) [attempted 5638/8477 = 66%, 20 KB/s], Decompressed: 4214 Downloaded: 5683 file(s) [attempted 5683/8477 = 67%, 344 KB/s], Decompressed: 4882 Downloaded: 5720 file(s) [attempted 5720/8477 = 67%, 150 KB/s], Decompressed: 4882 Downloaded: 5758 file(s) [attempted 5758/8477 = 67%, 367 KB/s], Decompressed: 4882 Downloaded: 5789 file(s) [attempted 5789/8477 = 68%, 212 KB/s], Decompressed: 4882 Downloaded: 5833 file(s) [attempted 5833/8477 = 68%, 112 KB/s], Decompressed: 4882 Downloaded: 5874 file(s) [attempted 5874/8477 = 69%, 344 KB/s], Decompressed: 4882 Downloaded: 5913 file(s) [attempted 5913/8477 = 69%, 342 KB/s], Decompressed: 4882 Downloaded: 5953 file(s) [attempted 5953/8477 = 70%, 60 KB/s], Decompressed: 4882 Downloaded: 5984 file(s) [attempted 5984/8477 = 70%, 224 KB/s], Decompressed: 4882 Downloaded: 6028 file(s) [attempted 6028/8477 = 71%, 51 KB/s], Decompressed: 4882 Downloaded: 6069 file(s) [attempted 6069/8477 = 71%, 355 KB/s], Decompressed: 4882 Downloaded: 6110 file(s) [attempted 6110/8477 = 72%, 35 KB/s], Decompressed: 4882 Downloaded: 6152 file(s) [attempted 6152/8477 = 72%, 145 KB/s], Decompressed: 4882 Downloaded: 6199 file(s) [attempted 6199/8477 = 73%, 134 KB/s], Decompressed: 4882 Downloaded: 6234 file(s) [attempted 6234/8477 = 73%, 462 KB/s], Decompressed: 4882 Downloaded: 6271 file(s) [attempted 6271/8477 = 73%, 32 KB/s], Decompressed: 4882 Downloaded: 6306 file(s) [attempted 6306/8477 = 74%, 113 KB/s], Decompressed: 4882 Downloaded: 6340 file(s) [attempted 6340/8477 = 74%, 108 KB/s], Decompressed: 4882 Downloaded: 6388 file(s) [attempted 6388/8477 = 75%, 1283 KB/s], Decompressed: 4882 Downloaded: 6439 file(s) [attempted 6439/8477 = 75%, 82 KB/s], Decompressed: 4882 Downloaded: 6487 file(s) [attempted 6487/8477 = 76%, 276 KB/s], Decompressed: 4882 Downloaded: 6535 file(s) [attempted 6535/8477 = 77%, 1006 KB/s], Decompressed: 5655 Downloaded: 6576 file(s) [attempted 6576/8477 = 77%, 159 KB/s], Decompressed: 5655 Downloaded: 6610 file(s) [attempted 6610/8477 = 77%, 57 KB/s], Decompressed: 5655 Downloaded: 6648 file(s) [attempted 6648/8477 = 78%, 250 KB/s], Decompressed: 5655 Downloaded: 6685 file(s) [attempted 6685/8477 = 78%, 391 KB/s], Decompressed: 5655 Downloaded: 6730 file(s) [attempted 6730/8477 = 79%, 25 KB/s], Decompressed: 5655 Downloaded: 6761 file(s) [attempted 6761/8477 = 79%, 247 KB/s], Decompressed: 5655 Downloaded: 6805 file(s) [attempted 6805/8477 = 80%, 453 KB/s], Decompressed: 5655 Downloaded: 6843 file(s) [attempted 6843/8477 = 80%, 131 KB/s], Decompressed: 5655 Downloaded: 6880 file(s) [attempted 6880/8477 = 81%, 155 KB/s], Decompressed: 5655 Downloaded: 6922 file(s) [attempted 6922/8477 = 81%, 31 KB/s], Decompressed: 5655 Downloaded: 6963 file(s) [attempted 6963/8477 = 82%, 119 KB/s], Decompressed: 5655 Downloaded: 7004 file(s) [attempted 7004/8477 = 82%, 821 KB/s], Decompressed: 5655 Downloaded: 7038 file(s) [attempted 7038/8477 = 83%, 78 KB/s], Decompressed: 5655 Downloaded: 7082 file(s) [attempted 7082/8477 = 83%, 419 KB/s], Decompressed: 5655 Downloaded: 7120 file(s) [attempted 7120/8477 = 83%, 216 KB/s], Decompressed: 5655 Downloaded: 7158 file(s) [attempted 7158/8477 = 84%, 1593 KB/s], Decompressed: 5655 Downloaded: 7199 file(s) [attempted 7199/8477 = 84%, 85 KB/s], Decompressed: 5655 Downloaded: 7247 file(s) [attempted 7247/8477 = 85%, 582 KB/s], Decompressed: 5655 Downloaded: 7288 file(s) [attempted 7288/8477 = 85%, 183 KB/s], Decompressed: 5655 Downloaded: 7322 file(s) [attempted 7322/8477 = 86%, 84 KB/s], Decompressed: 5655 Downloaded: 7363 file(s) [attempted 7363/8477 = 86%, 519 KB/s], Decompressed: 5655 Downloaded: 7401 file(s) [attempted 7401/8477 = 87%, 450 KB/s], Decompressed: 5655 Downloaded: 7442 file(s) [attempted 7442/8477 = 87%, 100 KB/s], Decompressed: 5655 Downloaded: 7476 file(s) [attempted 7476/8477 = 88%, 440 KB/s], Decompressed: 5655 Downloaded: 7510 file(s) [attempted 7510/8477 = 88%, 398 KB/s], Decompressed: 5655 Downloaded: 7544 file(s) [attempted 7544/8477 = 88%, 629 KB/s], Decompressed: 6504 Downloaded: 7579 file(s) [attempted 7579/8477 = 89%, 225 KB/s], Decompressed: 6504 Downloaded: 7623 file(s) [attempted 7623/8477 = 89%, 135 KB/s], Decompressed: 6504 Downloaded: 7671 file(s) [attempted 7671/8477 = 90%, 237 KB/s], Decompressed: 6504 Downloaded: 7712 file(s) [attempted 7712/8477 = 90%, 45 KB/s], Decompressed: 6504 Downloaded: 7746 file(s) [attempted 7746/8477 = 91%, 148 KB/s], Decompressed: 6504 Downloaded: 7774 file(s) [attempted 7774/8477 = 91%, 291 KB/s], Decompressed: 6504 Downloaded: 7801 file(s) [attempted 7801/8477 = 92%, 163 KB/s], Decompressed: 6504 Downloaded: 7825 file(s) [attempted 7825/8477 = 92%, 661 KB/s], Decompressed: 6504 Downloaded: 7852 file(s) [attempted 7852/8477 = 92%, 297 KB/s], Decompressed: 6504 Downloaded: 7876 file(s) [attempted 7876/8477 = 92%, 845 KB/s], Decompressed: 6504 Downloaded: 7897 file(s) [attempted 7897/8477 = 93%, 627 KB/s], Decompressed: 6504 Downloaded: 7914 file(s) [attempted 7914/8477 = 93%, 608 KB/s], Decompressed: 6504 Downloaded: 7928 file(s) [attempted 7928/8477 = 93%, 555 KB/s], Decompressed: 6504 Downloaded: 7941 file(s) [attempted 7941/8477 = 93%, 287 KB/s], Decompressed: 6504 Downloaded: 7959 file(s) [attempted 7959/8477 = 93%, 646 KB/s], Decompressed: 6504 Downloaded: 8003 file(s) [attempted 8003/8477 = 94%, 167 KB/s], Decompressed: 6504 Downloaded: 8020 file(s) [attempted 8020/8477 = 94%, 176 KB/s], Decompressed: 6504 Downloaded: 8065 file(s) [attempted 8065/8477 = 95%, 142 KB/s], Decompressed: 6504 Downloaded: 8109 file(s) [attempted 8109/8477 = 95%, 311 KB/s], Decompressed: 6504 Downloaded: 8157 file(s) [attempted 8157/8477 = 96%, 104 KB/s], Decompressed: 6504 Downloaded: 8198 file(s) [attempted 8198/8477 = 96%, 48 KB/s], Decompressed: 6504 Downloaded: 8225 file(s) [attempted 8225/8477 = 97%, 1558 KB/s], Decompressed: 6504 Downloaded: 8270 file(s) [attempted 8270/8477 = 97%, 306 KB/s], Decompressed: 6504 Downloaded: 8308 file(s) [attempted 8308/8477 = 98%, 474 KB/s], Decompressed: 6504 Downloaded: 8348 file(s) [attempted 8348/8477 = 98%, 44 KB/s], Decompressed: 6504 Downloaded: 8390 file(s) [attempted 8390/8477 = 98%, 344 KB/s], Decompressed: 6504 Downloaded: 8421 file(s) [attempted 8421/8477 = 99%, 691 KB/s], Decompressed: 6504 Downloaded: 8465 file(s) [attempted 8465/8477 = 99%, 219 KB/s], Decompressed: 7527 Downloaded: 8475 file(s) [attempted 8475/8477 = 99%, 268 KB/s], Decompressed: 7527 Downloaded: 8477 file(s) [attempted 8477/8477 = 100%, 268 KB/s], Decompressed: 7527
lean_checker exit 0
lake build
✔ [513/702] Built FLT.Assumptions.KnownIn1980s (365ms) ✔ [2948/2957] Built FLT.Assumptions.Mazur (4.4s) ✔ [3126/3222] Built FLT.Deformations.ContinuousRepresentation.IsTopologicalModule (4.5s) ✔ [3127/3222] Built FLT.Mathlib.Algebra.Algebra.Tower (4.5s) ✔ [3246/3316] Built FLT.Assumptions.Odlyzko (4.7s) ✔ [3294/3316] Built FLT.Mathlib.Topology.Algebra.Module.Quotient (2.1s) ✔ [3295/3316] Built FLT.Mathlib.Algebra.FixedPoints.Basic (3.3s) ✔ [3296/3316] Built FLT.Mathlib.Topology.Algebra.Group.Units (1.8s) ✔ [3298/3316] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Basic (4.9s) ✔ [3299/3316] Built FLT.Mathlib.Order.Filter.Cofinite (2.3s) ✔ [3300/3316] Built FLT.Mathlib.Topology.Bases (1.9s) ✔ [3303/3316] Built FLT.Mathlib.MeasureTheory.Measure.Typeclasses.Finite (2.0s) ✔ [3304/3316] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.RestrictedProduct (1.0s) ✔ [3305/3316] Built FLT.Mathlib.Topology.Algebra.Module.ModuleTopology (8.1s) ✔ [3307/3317] Built FLT.Mathlib.MeasureTheory.Group.Action (3.9s) ✔ [3308/3317] Built FLT.Mathlib.Topology.Algebra.ContinuousMonoidHom (2.5s) ✔ [3310/3330] Built FLT.Mathlib.MeasureTheory.Group.Measure (2.4s) ✔ [3316/3337] Built FLT.DedekindDomain.FiniteAdeleRing.TensorPi (6.5s) ✔ [3321/3337] Built FLT.Mathlib.RingTheory.TensorProduct.Pi (1.9s) ✔ [3322/3337] Built FLT.Hacks.RightActionInstances (7.2s) ✔ [3323/3338] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Equiv (8.6s) ✔ [3326/3338] Built FLT.Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic (1.9s) ✔ [3328/3342] Built FLT.Mathlib.RingTheory.DedekindDomain.AdicValuation (2.9s) ✔ [3330/3342] Built FLT.Mathlib.LinearAlgebra.Dimension.Constructions (2.4s) ✔ [3333/3348] Built FLT.Mathlib.RingTheory.Valuation.ValuationSubring (3.3s) ✔ [3339/3353] Built FLT.Mathlib.RingTheory.Ideal.Quotient.Basic (1.9s) ✔ [3342/3359] Built FLT.Mathlib.LinearAlgebra.Countable (2.3s) ✔ [3348/3375] Built FLT.AutomorphicForm.QuaternionAlgebra.Defs (6.4s) ✔ [3356/3375] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (9.0s) ✔ [3359/3375] Built FLT.Mathlib.Topology.Algebra.Valued.WithZeroMulInt (4.9s) ✔ [3361/3375] Built FLT.Mathlib.RingTheory.Localization.BaseChange (4.7s) ✔ [3362/3375] Built FLT.Mathlib.NumberTheory.NumberField.InfinitePlace.Completion (4.2s) ✔ [3363/3377] Built FLT.HaarMeasure.HaarChar.AddEquiv (12s) ✔ [3366/3384] Built FLT.DedekindDomain.AdicValuation (17s) ✔ [3372/3393] Built FLT.NumberField.Completion.Finite (4.4s) ✔ [3375/3393] Built FLT.HaarMeasure.HaarChar.Ring (5.2s) ✔ [3376/3393] Built FLT.DedekindDomain.IntegralClosure (11s) ✔ [3377/3393] Built FLT.Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing (18s) ✔ [3379/3403] Built FLT.Mathlib.Algebra.Module.Submodule.Basic (1.4s) ✔ [3380/3403] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.AdicCompletion (2.2s) ✔ [3382/3403] Built FLT.Mathlib.RingTheory.TensorProduct.Basis (2.6s) ✔ [3383/3403] Built FLT.Mathlib.Algebra.Algebra.Hom (3.4s) ✔ [3384/3404] Built FLT.NumberField.HeightOneSpectrum (2.3s) ✔ [3387/3404] Built FLT.Mathlib.Topology.Algebra.MulAction (1.7s) ✔ [3388/3404] Built FLT.Mathlib.Algebra.IsDirectLimit (3.8s) ✔ [3389/3404] Built FLT.Mathlib.LinearAlgebra.Pi (2.3s) ✔ [3390/3404] Built FLT.Mathlib.Topology.Algebra.Algebra.Hom (2.6s) ✔ [3392/3407] Built FLT.Mathlib.Topology.Algebra.UniformRing (2.3s) ✔ [3394/3407] Built FLT.Mathlib.Algebra.Algebra.Pi (1.9s) ✔ [3396/3407] Built FLT.Mathlib.Algebra.Algebra.Bilinear (3.7s) ✔ [3397/3409] Built FLT.Mathlib.NumberTheory.NumberField.FiniteAdeleRing (3.9s) ✔ [3399/3423] Built FLT.DedekindDomain.FiniteAdeleRing.IsDirectLimitRestricted (2.8s) ✔ [3402/3423] Built FLT.Mathlib.NumberTheory.NumberField.InfiniteAdeleRing (4.6s) ✔ [3404/3423] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.FiniteAdeleRing (3.3s) ✔ [3405/3423] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Module (13s) ✔ [3406/3423] Built FLT.Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (3.6s) ✔ [3407/3423] Built FLT.Mathlib.Topology.Algebra.Group.Quotient (1.6s) ✔ [3408/3423] Built FLT.Mathlib.Topology.Algebra.ContinuousAlgEquiv (1.9s) ✔ [3409/3423] Built FLT.Mathlib.Topology.Algebra.Module.FiniteDimension (2.1s) ✔ [3410/3426] Built FLT.DedekindDomain.FiniteAdeleRing.TensorRestrictedProduct (15s) ✔ [3413/3426] Built FLT.Mathlib.Topology.Constructions (1.8s) ✔ [3415/3435] Built FLT.NumberField.InfinitePlace.Extension (4.5s) ✔ [3417/3435] Built FLT.Mathlib.NumberTheory.NumberField.AdeleRing (3.5s) ✔ [3419/3435] Built FLT.Mathlib.Topology.MetricSpace.Pseudo.Matrix (3.4s) ✔ [3420/3435] Built FLT.Mathlib.Topology.Algebra.Module.Equiv (4.5s) ✔ [3421/3435] Built FLT.Mathlib.Data.Real.Archimedean (3.1s) ✔ [3423/3435] Built FLT.Mathlib.LinearAlgebra.Matrix.Transvection (3.8s) ✔ [3425/3438] Built FLT.NumberField.Padics.RestrictedProduct (6.3s) ✔ [3426/3438] Built FLT.Mathlib.Topology.MetricSpace.ProperSpace.InfinitePlace (3.7s) ✔ [3428/3440] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.InfinitePlace (4.3s) ✔ [3430/3454] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.AdeleRing (2.6s) ✔ [3436/3460] Built FLT.Mathlib.RingTheory.SimpleRing.TensorProduct (11s) ✔ [3439/3463] Built FLT.Mathlib.NumberTheory.Padics.PadicIntegers (3.0s) ✔ [3441/3463] Built FLT.Mathlib.LinearAlgebra.TensorProduct.FiniteFree (2.9s) ✔ [3442/3466] Built FLT.Mathlib.NumberTheory.Padics.HeightOneSpectrum (7.0s) ✔ [3443/3466] Built FLT.Mathlib.LinearAlgebra.TensorProduct.Algebra (3.5s) ✔ [3445/3466] Built FLT.HaarMeasure.MeasurableSpacePadics (4.2s) ✔ [3447/3466] Built FLT.HaarMeasure.HaarChar.RealComplex (4.9s) ✔ [3449/3466] Built FLT.Mathlib.LinearAlgebra.TensorProduct.Basis (2.1s) ✔ [3450/3466] Built FLT.Mathlib.Topology.Algebra.Module.TensorProduct (6.4s) ✔ [3452/3466] Built FLT.HaarMeasure.HaarChar.Padic (4.9s) ✔ [3453/3466] Built FLT.Mathlib.GroupTheory.DoubleCoset (2.4s) ✔ [3455/3471] Built FLT.Mathlib.Algebra.Central.TensorProduct (4.1s) ✔ [3457/3471] Built FLT.NumberField.Completion.Infinite (38s) ✔ [3460/3475] Built FLT.Mathlib.LinearAlgebra.Determinant (9.3s) ✔ [3462/3485] Built FLT.DedekindDomain.FiniteAdeleRing.TensorProduct (12s) ✔ [3469/3485] Built FLT.DedekindDomain.Completion.BaseChange (73s) ✔ [3470/3485] Built FLT.Mathlib.Topology.HomToDiscrete (3.2s) ✔ [3471/3496] Built FLT.HaarMeasure.HaarChar.FiniteDimensional (5.5s) ✔ [3473/3496] Built FLT.Mathlib.Topology.Polish (2.2s) ✔ [3475/3497] Built FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Abstract (3.1s) ✔ [3477/3497] Built FLT.Mathlib.Topology.Algebra.Valued.ValuationTopology (2.2s) ✔ [3478/3497] Built FLT.Mathlib.Topology.Instances.Matrix (2.6s) ✔ [3479/3497] Built FLT.Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs (2.4s) ✔ [3480/3497] Built FLT.NumberField.InfiniteAdeleRing (22s) ✔ [3485/3500] Built FLT.DedekindDomain.FiniteAdeleRing.LocalUnits (6.0s) ✔ [3487/3507] Built FLT.Mathlib.MeasureTheory.Haar.Extension (3.5s) ✔ [3694/3713] Built FLT.Mathlib.Algebra.IsQuaternionAlgebra (2.8s) ✔ [3698/3713] Built FLT.Deformations.RepresentationTheory.ContinuousSMulDiscrete (1.0s) ✔ [3702/3734] Built FLT.Basic.FreyPackage (6.2s) ✔ [3719/3734] Built FLT.Deformations.Lemmas (9.4s) ✔ [3720/3734] Built FLT.QuaternionAlgebra.NumberField (18s) ✔ [3724/3737] Built FLT.Deformations.RepresentationTheory.IntegralClosure (5.3s) ✔ [3726/3737] Built FLT.Deformations.RepresentationTheory.Frobenius (7.7s) ✔ [3742/3754] Built FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Local (17s) ✔ [3745/3763] Built FLT.HaarMeasure.HaarChar.FiniteAdeleRing (65s) ✔ [3755/3782] Built FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Concrete (16s) ✔ [3772/3803] Built FLT.Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (2.4s) ✔ [3778/3803] Built FLT.Deformations.RepresentationTheory.AbsoluteGaloisGroup (28s) ✔ [3779/3803] Built FLT.Data.Hurwitz (8.4s) ✔ [3780/3803] Built FLT.Deformations.RepresentationTheory.Etale (18s) ✔ [3782/3805] Built FLT.Patching.Utils.InverseLimit (2.1s) ✔ [3785/3806] Built FLT.Data.QHat (12s) ✔ [3786/3812] Built FLT.Deformations.Algebra.InverseLimit.Basic (8.8s) ✔ [3789/3825] Built FLT.Data.HurwitzRatHat (3.6s) ✔ [3791/3825] Built FLT.Patching.Utils.Lemmas (7.4s) ✔ [3795/3825] Built FLT.Mathlib.RingTheory.LocalRing.Defs (2.9s) ✔ [3797/3825] Built FLT.Deformations.Algebra.InverseLimit.Topology (5.7s) ✔ [3798/3825] Built FLT.Mathlib.RepresentationTheory.Basic (3.5s) ✔ [3799/3825] Built FLT.GaloisRepresentation.Cyclotomic (2.9s) ✔ [3801/3825] Built FLT.Deformations.IsResidueAlgebra (3.1s) ✔ [3802/3825] Built FLT.Patching.Utils.AdicTopology (6.0s) ✔ [3803/3830] Built FLT.Deformations.Subfunctor (2.1s) ✔ [3804/3830] Built FLT.Deformations.RepresentationTheory.GaloisRep (21s) ✔ [3806/3830] Built FLT.Deformations.RepresentationTheory.Irreducible (2.2s) ✔ [3807/3831] Built FLT.Deformations.IsProartinian (3.2s) ✔ [3808/3831] Built FLT.GaloisRepresentation.Automorphic (3.9s) ✔ [3809/3831] Built FLT.DedekindDomain.FiniteAdeleRing.BaseChange (113s) ✔ [3811/3834] Built FLT.Deformations.RepresentationTheory.GaloisRepFamily (3.3s) ✔ [3813/3835] Built FLT.EllipticCurve.Torsion (3.5s) ✔ [3933/3966] Built FLT.GaloisRepresentation.HardlyRamified.Defs (3.2s) ✔ [3934/3966] Built FLT.GroupScheme.FiniteFlat (325ms) ✔ [3935/3966] Built FLT.Deformations.Categories (4.6s) ✔ [3936/3966] Built FLT.Mathlib.Algebra.Order.AbsoluteValue.Basic (2.5s) ✔ [3937/3966] Built FLT.Mathlib.Analysis.Normed.Ring.WithAbs (2.7s) ✔ [3938/3966] Built FLT.Mathlib.Data.Set.Prod (711ms) ✔ [3939/3966] Built FLT.Mathlib.Data.Fin.Basic (1.6s) ✔ [3940/3966] Built FLT.Mathlib.GroupTheory.Index (1.4s) ✔ [3941/3966] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.Padic (1.7s) ✔ [3942/3966] Built FLT.Mathlib.MeasureTheory.Measure.Regular (2.1s) ✔ [3945/3966] Built FLT.Mathlib.NumberTheory.NumberField.Completion (1.6s) ✔ [3946/3966] Built FLT.Mathlib.Topology.Algebra.Monoid (1.6s) ✔ [3947/3966] Built FLT.GaloisRepresentation.HardlyRamified.ModThree (2.7s) ✔ [3948/3966] Built FLT.GaloisRepresentation.HardlyRamified.Threeadic (3.3s) ✔ [3949/3966] Built FLT.GaloisRepresentation.HardlyRamified.Lift (3.0s) ✔ [3950/3966] Built FLT.GaloisRepresentation.HardlyRamified.Frey (2.0s) ✔ [3951/3969] Built FLT.GaloisRepresentation.HardlyRamified.Family (3.5s) ✔ [3956/3980] Built FLT.Mathlib.Topology.Algebra.Order.Field (3.7s) ✔ [3964/3983] Built FLT.Deformations.LiftFunctor (6.2s) ✔ [3967/3983] Built FLT.Basic.Reductions (3.7s) ✔ [3968/3985] Built FLT.Patching.Utils.TopologicallyFG (2.5s) ✔ [3970/3985] Built FLT.Deformations.Representable (4.1s) ✔ [3971/3994] Built FLT.NumberField.DiscriminantBounds (6.1s) ✔ [3990/4009] Built FLT.TateCurve.TateCurve (616ms) ✔ [3991/4009] Built FLT.Patching.Utils.StructureFiniteness (7.1s) ✔ [3992/4009] Built FLT.Patching.Utils.Depth (5.4s) ✔ [3993/4009] Built FLT.GlobalLanglandsConjectures.GLnDefs (14s) ✔ [3994/4009] Built FLT.Patching.Utils.CompactHausdorffRings (3.6s) ✔ [3995/4009] Built FLT.GlobalLanglandsConjectures.GLzero (2.8s) ✔ [3996/4009] Built FLT.Patching.Ultraproduct (11s) ✔ [3997/4009] Built FLT.NumberField.AdeleRing (43s) ✔ [3998/4009] Built FLT.Patching.VanishingFilter (4.5s) ✔ [3999/4009] Built FLT.Patching.Algebra (16s) ✔ [4000/4009] Built FLT.HaarMeasure.HaarChar.AdeleRing (17s) ✔ [4001/4009] Built FLT.Patching.Module (20s) ✔ [4002/4009] Built FLT.Patching.Over (14s) ✔ [4003/4009] Built FLT.Patching.System (11s) ✔ [4004/4009] Built FLT.Patching.REqualsT (4.2s) ✔ [4005/4009] Built FLT.DivisionAlgebra.Finiteness (46s) ✔ [4006/4009] Built FLT.AutomorphicForm.QuaternionAlgebra.FiniteDimensional (2.2s) ✔ [4007/4009] Built FLT (1.8s) ✔ [4008/4009] Built FermatsLastTheorem (16s) Build completed successfully (4009 jobs).
blueprint_build exit 1
lake build :blueprint
error: unknown package facet `blueprint`
semantic_extract exit 137
./.apodeixis/tools/lean-semantic-extract.sh
/apx/source/.apodeixis/tools/lean-semantic-extract.sh: line 136: 12701 Killed python3 <<'PY'
import hashlib
import json
import os
import pathlib
import sys
request_path = pathlib.Path(os.environ["APX_LEAN_HELPER_REQUEST_PATH"])
response_path = pathlib.Path(os.environ["APX_LEAN_HELPER_RESPONSE_PATH"])
with request_path.open("r", encoding="utf-8") as handle:
request = json.load(handle)
if request.get("operation") != "extract_repository_semantics":
raise SystemExit(0)
with response_path.open("r", encoding="utf-8") as handle:
response = json.load(handle)
if "helper" not in response:
raise SystemExit(0)
helper = response.get("helper")
helper_version = response.get("helper_version")
if not helper or helper_version in (None, ""):
print(
"lean semantic extractor failed: repository semantics response is missing helper metadata required for normalization",
file=sys.stderr,
)
raise SystemExit(1)
without_checksum = {k: v for k, v in response.items() if k != "checksum"}
canonical = json.dumps(without_checksum, sort_keys=True, separators=(",", ":"), ensure_ascii=False)
response["checksum"] = hashlib.sha256(canonical.encode("utf-8")).hexdigest()
tmp_path = pathlib.Path(f"{response_path}.tmp")
with tmp_path.open("w", encoding="utf-8") as handle:
json.dump(response, handle, sort_keys=True, separators=(",", ":"), ensure_ascii=False)
os.replace(tmp_path, response_path)
PY