Verification run
Run 3
failed commit
manual toolchain lean-v4-31-0-rc1 prover lean took 21m 16s · 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-43-source
Cloning into '/var/lib/apodeixis/repos/job-43-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 (760ms) ✔ [5/24] Built Cache.Lean (745ms) ✔ [6/24] Built Cache.Init (354ms) ✔ [7/24] Built Batteries.Data.Array.Match (1.2s) ✔ [8/24] Built Batteries.Tactic.OpenPrivate (1.3s) ✔ [9/24] Built Batteries.Data.String.Basic:c.o (210ms) ✔ [10/24] Built Cache.Lean:c.o (583ms) ✔ [11/24] Built Cache.Init:c.o (111ms) ✔ [12/24] Built Batteries.Data.Array.Match:c.o (249ms) ✔ [13/24] Built Batteries.Data.String.Matcher (436ms) ✔ [14/24] Built Batteries.Data.String.Matcher:c.o (195ms) ✔ [15/24] Built Batteries.Tactic.OpenPrivate:c.o (996ms) ✔ [16/24] Built Cache.IO (1.7s) ✔ [17/24] Built Cache.Hashing (883ms) ✔ [18/24] Built Cache.IO:c.o (1.2s) ✔ [19/24] Built Cache.Hashing:c.o (352ms) ✔ [20/24] Built Cache.Requests (2.0s) ✔ [21/24] Built Cache.Main (1.1s) ✔ [22/24] Built Cache.Main:c.o (512ms) ✔ [23/24] Built Cache.Requests:c.o (1.9s) ✔ [24/24] Built cache:exe (2.5s) Downloaded: 1 file(s) [attempted 1/8477 = 0%, 10 KB/s], Decompressed: 0 Downloaded: 12 file(s) [attempted 12/8477 = 0%, 1 KB/s], Decompressed: 11 Downloaded: 34 file(s) [attempted 34/8477 = 0%, 16 KB/s], Decompressed: 31 Downloaded: 61 file(s) [attempted 61/8477 = 0%, 44 KB/s], Decompressed: 56 Downloaded: 89 file(s) [attempted 89/8477 = 1%, 311 KB/s], Decompressed: 72 Downloaded: 121 file(s) [attempted 121/8477 = 1%, 34 KB/s], Decompressed: 100 Downloaded: 148 file(s) [attempted 148/8477 = 1%, 121 KB/s], Decompressed: 134 Downloaded: 182 file(s) [attempted 182/8477 = 2%, 48 KB/s], Decompressed: 165 Downloaded: 216 file(s) [attempted 216/8477 = 2%, 454 KB/s], Decompressed: 189 Downloaded: 258 file(s) [attempted 258/8477 = 3%, 185 KB/s], Decompressed: 216 Downloaded: 295 file(s) [attempted 295/8477 = 3%, 152 KB/s], Decompressed: 216 Downloaded: 326 file(s) [attempted 326/8477 = 3%, 360 KB/s], Decompressed: 251 Downloaded: 367 file(s) [attempted 367/8477 = 4%, 186 KB/s], Decompressed: 302 Downloaded: 408 file(s) [attempted 408/8477 = 4%, 548 KB/s], Decompressed: 302 Downloaded: 449 file(s) [attempted 449/8477 = 5%, 55 KB/s], Decompressed: 360 Downloaded: 480 file(s) [attempted 480/8477 = 5%, 1109 KB/s], Decompressed: 360 Downloaded: 514 file(s) [attempted 514/8477 = 6%, 617 KB/s], Decompressed: 419 Downloaded: 559 file(s) [attempted 559/8477 = 6%, 231 KB/s], Decompressed: 419 Downloaded: 600 file(s) [attempted 600/8477 = 7%, 340 KB/s], Decompressed: 494 Downloaded: 638 file(s) [attempted 638/8477 = 7%, 116 KB/s], Decompressed: 494 Downloaded: 672 file(s) [attempted 672/8477 = 7%, 323 KB/s], Decompressed: 566 Downloaded: 713 file(s) [attempted 713/8477 = 8%, 277 KB/s], Decompressed: 566 Downloaded: 754 file(s) [attempted 754/8477 = 8%, 59 KB/s], Decompressed: 566 Downloaded: 795 file(s) [attempted 795/8477 = 9%, 108 KB/s], Decompressed: 662 Downloaded: 840 file(s) [attempted 840/8477 = 9%, 74 KB/s], Decompressed: 662 Downloaded: 878 file(s) [attempted 878/8477 = 10%, 996 KB/s], Decompressed: 758 Downloaded: 915 file(s) [attempted 915/8477 = 10%, 531 KB/s], Decompressed: 758 Downloaded: 956 file(s) [attempted 956/8477 = 11%, 31 KB/s], Decompressed: 843 Downloaded: 1001 file(s) [attempted 1001/8477 = 11%, 552 KB/s], Decompressed: 843 Downloaded: 1042 file(s) [attempted 1042/8477 = 12%, 1319 KB/s], Decompressed: 941 Downloaded: 1080 file(s) [attempted 1080/8477 = 12%, 220 KB/s], Decompressed: 941 Downloaded: 1117 file(s) [attempted 1117/8477 = 13%, 1169 KB/s], Decompressed: 1028 Downloaded: 1151 file(s) [attempted 1151/8477 = 13%, 153 KB/s], Decompressed: 1028 Downloaded: 1196 file(s) [attempted 1196/8477 = 14%, 157 KB/s], Decompressed: 1028 Downloaded: 1234 file(s) [attempted 1234/8477 = 14%, 1138 KB/s], Decompressed: 1112 Downloaded: 1275 file(s) [attempted 1275/8477 = 15%, 120 KB/s], Decompressed: 1112 Downloaded: 1312 file(s) [attempted 1312/8477 = 15%, 632 KB/s], Decompressed: 1206 Downloaded: 1346 file(s) [attempted 1346/8477 = 15%, 128 KB/s], Decompressed: 1206 Downloaded: 1384 file(s) [attempted 1384/8477 = 16%, 68 KB/s], Decompressed: 1206 Downloaded: 1429 file(s) [attempted 1429/8477 = 16%, 390 KB/s], Decompressed: 1295 Downloaded: 1466 file(s) [attempted 1466/8477 = 17%, 94 KB/s], Decompressed: 1295 Downloaded: 1504 file(s) [attempted 1504/8477 = 17%, 242 KB/s], Decompressed: 1394 Downloaded: 1538 file(s) [attempted 1538/8477 = 18%, 72 KB/s], Decompressed: 1394 Downloaded: 1579 file(s) [attempted 1579/8477 = 18%, 259 KB/s], Decompressed: 1394 Downloaded: 1624 file(s) [attempted 1624/8477 = 19%, 396 KB/s], Decompressed: 1490 Downloaded: 1665 file(s) [attempted 1665/8477 = 19%, 306 KB/s], Decompressed: 1490 Downloaded: 1702 file(s) [attempted 1702/8477 = 20%, 209 KB/s], Decompressed: 1490 Downloaded: 1740 file(s) [attempted 1740/8477 = 20%, 112 KB/s], Decompressed: 1600 Downloaded: 1778 file(s) [attempted 1778/8477 = 20%, 224 KB/s], Decompressed: 1600 Downloaded: 1815 file(s) [attempted 1815/8477 = 21%, 60 KB/s], Decompressed: 1600 Downloaded: 1856 file(s) [attempted 1856/8477 = 21%, 472 KB/s], Decompressed: 1713 Downloaded: 1897 file(s) [attempted 1897/8477 = 22%, 564 KB/s], Decompressed: 1713 Downloaded: 1932 file(s) [attempted 1932/8477 = 22%, 255 KB/s], Decompressed: 1713 Downloaded: 1966 file(s) [attempted 1966/8477 = 23%, 94 KB/s], Decompressed: 1832 Downloaded: 2010 file(s) [attempted 2010/8477 = 23%, 765 KB/s], Decompressed: 1832 Downloaded: 2055 file(s) [attempted 2055/8477 = 24%, 113 KB/s], Decompressed: 1832 Downloaded: 2099 file(s) [attempted 2099/8477 = 24%, 245 KB/s], Decompressed: 1949 Downloaded: 2141 file(s) [attempted 2141/8477 = 25%, 890 KB/s], Decompressed: 1949 Downloaded: 2175 file(s) [attempted 2175/8477 = 25%, 538 KB/s], Decompressed: 1949 Downloaded: 2209 file(s) [attempted 2209/8477 = 26%, 187 KB/s], Decompressed: 1949 Downloaded: 2257 file(s) [attempted 2257/8477 = 26%, 194 KB/s], Decompressed: 1949 Downloaded: 2298 file(s) [attempted 2298/8477 = 27%, 25 KB/s], Decompressed: 2099 Downloaded: 2336 file(s) [attempted 2336/8477 = 27%, 147 KB/s], Decompressed: 2099 Downloaded: 2377 file(s) [attempted 2377/8477 = 28%, 304 KB/s], Decompressed: 2099 Downloaded: 2407 file(s) [attempted 2407/8477 = 28%, 705 KB/s], Decompressed: 2099 Downloaded: 2452 file(s) [attempted 2452/8477 = 28%, 61 KB/s], Decompressed: 2099 Downloaded: 2493 file(s) [attempted 2493/8477 = 29%, 51 KB/s], Decompressed: 2277 Downloaded: 2534 file(s) [attempted 2534/8477 = 29%, 119 KB/s], Decompressed: 2277 Downloaded: 2575 file(s) [attempted 2575/8477 = 30%, 430 KB/s], Decompressed: 2277 Downloaded: 2620 file(s) [attempted 2620/8477 = 30%, 272 KB/s], Decompressed: 2277 Downloaded: 2650 file(s) [attempted 2650/8477 = 31%, 200 KB/s], Decompressed: 2277 Downloaded: 2688 file(s) [attempted 2688/8477 = 31%, 213 KB/s], Decompressed: 2455 Downloaded: 2729 file(s) [attempted 2729/8477 = 32%, 84 KB/s], Decompressed: 2455 Downloaded: 2770 file(s) [attempted 2770/8477 = 32%, 1812 KB/s], Decompressed: 2455 Downloaded: 2811 file(s) [attempted 2811/8477 = 33%, 565 KB/s], Decompressed: 2455 Downloaded: 2839 file(s) [attempted 2839/8477 = 33%, 105 KB/s], Decompressed: 2455 Downloaded: 2880 file(s) [attempted 2880/8477 = 33%, 517 KB/s], Decompressed: 2455 Downloaded: 2924 file(s) [attempted 2924/8477 = 34%, 680 KB/s], Decompressed: 2661 Downloaded: 2969 file(s) [attempted 2969/8477 = 35%, 140 KB/s], Decompressed: 2661 Downloaded: 3006 file(s) [attempted 3006/8477 = 35%, 444 KB/s], Decompressed: 2661 Downloaded: 3041 file(s) [attempted 3041/8477 = 35%, 1107 KB/s], Decompressed: 2661 Downloaded: 3075 file(s) [attempted 3075/8477 = 36%, 194 KB/s], Decompressed: 2661 Downloaded: 3123 file(s) [attempted 3123/8477 = 36%, 228 KB/s], Decompressed: 2661 Downloaded: 3171 file(s) [attempted 3171/8477 = 37%, 148 KB/s], Decompressed: 2890 Downloaded: 3215 file(s) [attempted 3215/8477 = 37%, 518 KB/s], Decompressed: 2890 Downloaded: 3253 file(s) [attempted 3253/8477 = 38%, 367 KB/s], Decompressed: 2890 Downloaded: 3284 file(s) [attempted 3284/8477 = 38%, 135 KB/s], Decompressed: 2890 Downloaded: 3325 file(s) [attempted 3325/8477 = 39%, 842 KB/s], Decompressed: 2890 Downloaded: 3366 file(s) [attempted 3366/8477 = 39%, 75 KB/s], Decompressed: 2890 Downloaded: 3407 file(s) [attempted 3407/8477 = 40%, 738 KB/s], Decompressed: 2890 Downloaded: 3444 file(s) [attempted 3444/8477 = 40%, 384 KB/s], Decompressed: 2890 Downloaded: 3479 file(s) [attempted 3479/8477 = 41%, 676 KB/s], Decompressed: 2890 Downloaded: 3520 file(s) [attempted 3520/8477 = 41%, 533 KB/s], Decompressed: 2890 Downloaded: 3557 file(s) [attempted 3557/8477 = 41%, 46 KB/s], Decompressed: 3171 Downloaded: 3598 file(s) [attempted 3598/8477 = 42%, 72 KB/s], Decompressed: 3171 Downloaded: 3639 file(s) [attempted 3639/8477 = 42%, 235 KB/s], Decompressed: 3171 Downloaded: 3678 file(s) [attempted 3678/8477 = 43%, 110 KB/s], Decompressed: 3171 Downloaded: 3722 file(s) [attempted 3722/8477 = 43%, 240 KB/s], Decompressed: 3171 Downloaded: 3756 file(s) [attempted 3756/8477 = 44%, 471 KB/s], Decompressed: 3171 Downloaded: 3797 file(s) [attempted 3797/8477 = 44%, 87 KB/s], Decompressed: 3171 Downloaded: 3835 file(s) [attempted 3835/8477 = 45%, 697 KB/s], Decompressed: 3171 Downloaded: 3872 file(s) [attempted 3872/8477 = 45%, 54 KB/s], Decompressed: 3171 Downloaded: 3913 file(s) [attempted 3913/8477 = 46%, 223 KB/s], Decompressed: 3171 Downloaded: 3948 file(s) [attempted 3948/8477 = 46%, 480 KB/s], Decompressed: 3171 Downloaded: 3992 file(s) [attempted 3992/8477 = 47%, 56 KB/s], Decompressed: 3171 Downloaded: 4026 file(s) [attempted 4026/8477 = 47%, 38 KB/s], Decompressed: 3547 Downloaded: 4067 file(s) [attempted 4067/8477 = 47%, 637 KB/s], Decompressed: 3547 Downloaded: 4108 file(s) [attempted 4108/8477 = 48%, 173 KB/s], Decompressed: 3547 Downloaded: 4146 file(s) [attempted 4146/8477 = 48%, 202 KB/s], Decompressed: 3547 Downloaded: 4190 file(s) [attempted 4190/8477 = 49%, 299 KB/s], Decompressed: 3547 Downloaded: 4232 file(s) [attempted 4232/8477 = 49%, 395 KB/s], Decompressed: 3547 Downloaded: 4269 file(s) [attempted 4269/8477 = 50%, 314 KB/s], Decompressed: 3547 Downloaded: 4300 file(s) [attempted 4300/8477 = 50%, 305 KB/s], Decompressed: 3547 Downloaded: 4345 file(s) [attempted 4345/8477 = 51%, 311 KB/s], Decompressed: 3547 Downloaded: 4386 file(s) [attempted 4386/8477 = 51%, 807 KB/s], Decompressed: 3547 Downloaded: 4430 file(s) [attempted 4430/8477 = 52%, 1071 KB/s], Decompressed: 3547 Downloaded: 4475 file(s) [attempted 4475/8477 = 52%, 88 KB/s], Decompressed: 3547 Downloaded: 4505 file(s) [attempted 4505/8477 = 53%, 242 KB/s], Decompressed: 3547 Downloaded: 4543 file(s) [attempted 4543/8477 = 53%, 918 KB/s], Decompressed: 3547 Downloaded: 4587 file(s) [attempted 4587/8477 = 54%, 341 KB/s], Decompressed: 3999 Downloaded: 4622 file(s) [attempted 4622/8477 = 54%, 389 KB/s], Decompressed: 3999 Downloaded: 4666 file(s) [attempted 4666/8477 = 55%, 35 KB/s], Decompressed: 3999 Downloaded: 4711 file(s) [attempted 4711/8477 = 55%, 1361 KB/s], Decompressed: 3999 Downloaded: 4745 file(s) [attempted 4745/8477 = 55%, 387 KB/s], Decompressed: 3999 Downloaded: 4786 file(s) [attempted 4786/8477 = 56%, 80 KB/s], Decompressed: 3999 Downloaded: 4827 file(s) [attempted 4827/8477 = 56%, 610 KB/s], Decompressed: 3999 Downloaded: 4865 file(s) [attempted 4865/8477 = 57%, 409 KB/s], Decompressed: 3999 Downloaded: 4899 file(s) [attempted 4899/8477 = 57%, 43 KB/s], Decompressed: 3999 Downloaded: 4940 file(s) [attempted 4940/8477 = 58%, 176 KB/s], Decompressed: 3999 Downloaded: 4984 file(s) [attempted 4984/8477 = 58%, 251 KB/s], Decompressed: 3999 Downloaded: 5026 file(s) [attempted 5026/8477 = 59%, 205 KB/s], Decompressed: 3999 Downloaded: 5063 file(s) [attempted 5063/8477 = 59%, 135 KB/s], Decompressed: 3999 Downloaded: 5097 file(s) [attempted 5097/8477 = 60%, 99 KB/s], Decompressed: 3999 Downloaded: 5139 file(s) [attempted 5139/8477 = 60%, 42 KB/s], Decompressed: 3999 Downloaded: 5176 file(s) [attempted 5176/8477 = 61%, 922 KB/s], Decompressed: 3999 Downloaded: 5221 file(s) [attempted 5221/8477 = 61%, 191 KB/s], Decompressed: 3999 Downloaded: 5258 file(s) [attempted 5258/8477 = 62%, 237 KB/s], Decompressed: 4550 Downloaded: 5299 file(s) [attempted 5299/8477 = 62%, 410 KB/s], Decompressed: 4550 Downloaded: 5340 file(s) [attempted 5340/8477 = 62%, 45 KB/s], Decompressed: 4550 Downloaded: 5375 file(s) [attempted 5375/8477 = 63%, 432 KB/s], Decompressed: 4550 Downloaded: 5419 file(s) [attempted 5419/8477 = 63%, 294 KB/s], Decompressed: 4550 Downloaded: 5457 file(s) [attempted 5457/8477 = 64%, 459 KB/s], Decompressed: 4550 Downloaded: 5494 file(s) [attempted 5494/8477 = 64%, 529 KB/s], Decompressed: 4550 Downloaded: 5532 file(s) [attempted 5532/8477 = 65%, 181 KB/s], Decompressed: 4550 Downloaded: 5570 file(s) [attempted 5570/8477 = 65%, 283 KB/s], Decompressed: 4550 Downloaded: 5611 file(s) [attempted 5611/8477 = 66%, 317 KB/s], Decompressed: 4550 Downloaded: 5652 file(s) [attempted 5652/8477 = 66%, 160 KB/s], Decompressed: 4550 Downloaded: 5690 file(s) [attempted 5690/8477 = 67%, 32 KB/s], Decompressed: 4550 Downloaded: 5724 file(s) [attempted 5724/8477 = 67%, 381 KB/s], Decompressed: 4550 Downloaded: 5761 file(s) [attempted 5761/8477 = 67%, 367 KB/s], Decompressed: 4550 Downloaded: 5802 file(s) [attempted 5802/8477 = 68%, 131 KB/s], Decompressed: 4550 Downloaded: 5847 file(s) [attempted 5847/8477 = 68%, 102 KB/s], Decompressed: 4550 Downloaded: 5891 file(s) [attempted 5891/8477 = 69%, 56 KB/s], Decompressed: 4550 Downloaded: 5929 file(s) [attempted 5929/8477 = 69%, 206 KB/s], Decompressed: 4550 Downloaded: 5970 file(s) [attempted 5970/8477 = 70%, 31 KB/s], Decompressed: 4550 Downloaded: 6008 file(s) [attempted 6008/8477 = 70%, 311 KB/s], Decompressed: 5224 Downloaded: 6045 file(s) [attempted 6045/8477 = 71%, 42 KB/s], Decompressed: 5224 Downloaded: 6090 file(s) [attempted 6090/8477 = 71%, 224 KB/s], Decompressed: 5224 Downloaded: 6128 file(s) [attempted 6128/8477 = 72%, 167 KB/s], Decompressed: 5224 Downloaded: 6165 file(s) [attempted 6165/8477 = 72%, 1189 KB/s], Decompressed: 5224 Downloaded: 6206 file(s) [attempted 6206/8477 = 73%, 463 KB/s], Decompressed: 5224 Downloaded: 6234 file(s) [attempted 6234/8477 = 73%, 460 KB/s], Decompressed: 5224 Downloaded: 6278 file(s) [attempted 6278/8477 = 74%, 50 KB/s], Decompressed: 5224 Downloaded: 6316 file(s) [attempted 6316/8477 = 74%, 2344 KB/s], Decompressed: 5224 Downloaded: 6360 file(s) [attempted 6360/8477 = 75%, 399 KB/s], Decompressed: 5224 Downloaded: 6398 file(s) [attempted 6398/8477 = 75%, 234 KB/s], Decompressed: 5224 Downloaded: 6432 file(s) [attempted 6432/8477 = 75%, 1706 KB/s], Decompressed: 5224 Downloaded: 6473 file(s) [attempted 6473/8477 = 76%, 887 KB/s], Decompressed: 5224 Downloaded: 6507 file(s) [attempted 6507/8477 = 76%, 473 KB/s], Decompressed: 5224 Downloaded: 6545 file(s) [attempted 6545/8477 = 77%, 48 KB/s], Decompressed: 5224 Downloaded: 6586 file(s) [attempted 6586/8477 = 77%, 483 KB/s], Decompressed: 5224 Downloaded: 6624 file(s) [attempted 6624/8477 = 78%, 161 KB/s], Decompressed: 5224 Downloaded: 6665 file(s) [attempted 6665/8477 = 78%, 50 KB/s], Decompressed: 5224 Downloaded: 6696 file(s) [attempted 6696/8477 = 78%, 60 KB/s], Decompressed: 5224 Downloaded: 6740 file(s) [attempted 6740/8477 = 79%, 343 KB/s], Decompressed: 5224 Downloaded: 6785 file(s) [attempted 6785/8477 = 80%, 1364 KB/s], Decompressed: 5224 Downloaded: 6826 file(s) [attempted 6826/8477 = 80%, 327 KB/s], Decompressed: 5224 Downloaded: 6853 file(s) [attempted 6853/8477 = 80%, 40 KB/s], Decompressed: 5987 Downloaded: 6894 file(s) [attempted 6894/8477 = 81%, 318 KB/s], Decompressed: 5987 Downloaded: 6939 file(s) [attempted 6939/8477 = 81%, 80 KB/s], Decompressed: 5987 Downloaded: 6983 file(s) [attempted 6983/8477 = 82%, 53 KB/s], Decompressed: 5987 Downloaded: 7017 file(s) [attempted 7017/8477 = 82%, 345 KB/s], Decompressed: 5987 Downloaded: 7045 file(s) [attempted 7045/8477 = 83%, 149 KB/s], Decompressed: 5987 Downloaded: 7076 file(s) [attempted 7076/8477 = 83%, 143 KB/s], Decompressed: 5987 Downloaded: 7113 file(s) [attempted 7113/8477 = 83%, 552 KB/s], Decompressed: 5987 Downloaded: 7147 file(s) [attempted 7147/8477 = 84%, 1562 KB/s], Decompressed: 5987 Downloaded: 7171 file(s) [attempted 7171/8477 = 84%, 138 KB/s], Decompressed: 5987 Downloaded: 7195 file(s) [attempted 7195/8477 = 84%, 91 KB/s], Decompressed: 5987 Downloaded: 7219 file(s) [attempted 7219/8477 = 85%, 746 KB/s], Decompressed: 5987 Downloaded: 7247 file(s) [attempted 7247/8477 = 85%, 271 KB/s], Decompressed: 5987 Downloaded: 7271 file(s) [attempted 7271/8477 = 85%, 218 KB/s], Decompressed: 5987 Downloaded: 7291 file(s) [attempted 7291/8477 = 86%, 199 KB/s], Decompressed: 5987 Downloaded: 7312 file(s) [attempted 7312/8477 = 86%, 319 KB/s], Decompressed: 5987 Downloaded: 7332 file(s) [attempted 7332/8477 = 86%, 852 KB/s], Decompressed: 5987 Downloaded: 7380 file(s) [attempted 7380/8477 = 87%, 236 KB/s], Decompressed: 5987 Downloaded: 7408 file(s) [attempted 7408/8477 = 87%, 65 KB/s], Decompressed: 5987 Downloaded: 7445 file(s) [attempted 7445/8477 = 87%, 153 KB/s], Decompressed: 5987 Downloaded: 7486 file(s) [attempted 7486/8477 = 88%, 370 KB/s], Decompressed: 5987 Downloaded: 7531 file(s) [attempted 7531/8477 = 88%, 193 KB/s], Decompressed: 5987 Downloaded: 7565 file(s) [attempted 7565/8477 = 89%, 627 KB/s], Decompressed: 5987 Downloaded: 7599 file(s) [attempted 7599/8477 = 89%, 107 KB/s], Decompressed: 5987 Downloaded: 7644 file(s) [attempted 7644/8477 = 90%, 190 KB/s], Decompressed: 5987 Downloaded: 7681 file(s) [attempted 7681/8477 = 90%, 366 KB/s], Decompressed: 5987 Downloaded: 7722 file(s) [attempted 7722/8477 = 91%, 177 KB/s], Decompressed: 6843 Downloaded: 7760 file(s) [attempted 7760/8477 = 91%, 105 KB/s], Decompressed: 6843 Downloaded: 7801 file(s) [attempted 7801/8477 = 92%, 30 KB/s], Decompressed: 6843 Downloaded: 7842 file(s) [attempted 7842/8477 = 92%, 402 KB/s], Decompressed: 6843 Downloaded: 7883 file(s) [attempted 7883/8477 = 92%, 50 KB/s], Decompressed: 6843 Downloaded: 7921 file(s) [attempted 7921/8477 = 93%, 625 KB/s], Decompressed: 6843 Downloaded: 7955 file(s) [attempted 7955/8477 = 93%, 86 KB/s], Decompressed: 6843 Downloaded: 7993 file(s) [attempted 7993/8477 = 94%, 191 KB/s], Decompressed: 6843 Downloaded: 8034 file(s) [attempted 8034/8477 = 94%, 3274 KB/s], Decompressed: 6843 Downloaded: 8082 file(s) [attempted 8082/8477 = 95%, 151 KB/s], Decompressed: 6843 Downloaded: 8119 file(s) [attempted 8119/8477 = 95%, 380 KB/s], Decompressed: 6843 Downloaded: 8157 file(s) [attempted 8157/8477 = 96%, 104 KB/s], Decompressed: 6843 Downloaded: 8195 file(s) [attempted 8195/8477 = 96%, 53 KB/s], Decompressed: 6843 Downloaded: 8236 file(s) [attempted 8236/8477 = 97%, 97 KB/s], Decompressed: 6843 Downloaded: 8277 file(s) [attempted 8277/8477 = 97%, 104 KB/s], Decompressed: 6843 Downloaded: 8314 file(s) [attempted 8314/8477 = 98%, 697 KB/s], Decompressed: 6843 Downloaded: 8352 file(s) [attempted 8352/8477 = 98%, 85 KB/s], Decompressed: 6843 Downloaded: 8393 file(s) [attempted 8393/8477 = 99%, 574 KB/s], Decompressed: 6843 Downloaded: 8431 file(s) [attempted 8431/8477 = 99%, 265 KB/s], Decompressed: 6843 Downloaded: 8468 file(s) [attempted 8468/8477 = 99%, 193 KB/s], Decompressed: 6843 Downloaded: 8477 file(s) [attempted 8477/8477 = 100%, 193 KB/s], Decompressed: 6843
lean_checker exit 0
lake build
✔ [557/739] Built FLT.Assumptions.KnownIn1980s (415ms) ✔ [2949/2971] Built FLT.Assumptions.Mazur (4.8s) ✔ [3094/3199] Built FLT.Deformations.ContinuousRepresentation.IsTopologicalModule (4.7s) ✔ [3095/3199] Built FLT.Mathlib.Algebra.Algebra.Tower (4.7s) ✔ [3194/3266] Built FLT.Assumptions.Odlyzko (4.7s) ✔ [3295/3316] Built FLT.Mathlib.Topology.Algebra.Module.Quotient (1.7s) ✔ [3296/3316] Built FLT.Mathlib.Algebra.FixedPoints.Basic (2.3s) ✔ [3297/3316] Built FLT.Mathlib.Topology.Algebra.Group.Units (1.6s) ✔ [3299/3316] Built FLT.Mathlib.Order.Filter.Cofinite (1.4s) ✔ [3301/3316] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Basic (3.9s) ✔ [3303/3316] Built FLT.Mathlib.Topology.Bases (1.2s) ✔ [3304/3316] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.RestrictedProduct (1.6s) ✔ [3305/3316] Built FLT.Mathlib.Topology.Algebra.Module.ModuleTopology (5.6s) ✔ [3306/3316] Built FLT.Mathlib.MeasureTheory.Measure.Typeclasses.Finite (1.4s) ✔ [3308/3317] Built FLT.Mathlib.MeasureTheory.Group.Action (2.6s) ✔ [3309/3317] Built FLT.Mathlib.Topology.Algebra.ContinuousMonoidHom (1.8s) ✔ [3310/3330] Built FLT.Mathlib.MeasureTheory.Group.Measure (2.0s) ✔ [3316/3337] Built FLT.DedekindDomain.FiniteAdeleRing.TensorPi (4.6s) ✔ [3321/3337] Built FLT.Mathlib.RingTheory.TensorProduct.Pi (1.4s) ✔ [3322/3337] Built FLT.Hacks.RightActionInstances (5.1s) ✔ [3325/3338] Built FLT.Mathlib.RingTheory.DedekindDomain.AdicValuation (2.3s) ✔ [3326/3338] Built FLT.Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic (1.6s) ✔ [3327/3342] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Equiv (7.1s) ✔ [3330/3342] Built FLT.Mathlib.LinearAlgebra.Dimension.Constructions (1.6s) ✔ [3332/3347] Built FLT.Mathlib.RingTheory.Valuation.ValuationSubring (2.4s) ✔ [3339/3353] Built FLT.Mathlib.RingTheory.Ideal.Quotient.Basic (1.4s) ✔ [3343/3359] Built FLT.Mathlib.LinearAlgebra.Countable (1.7s) ✔ [3348/3359] Built FLT.AutomorphicForm.QuaternionAlgebra.Defs (5.2s) ✔ [3356/3375] Built FLT.Mathlib.Topology.Algebra.Valued.WithZeroMulInt (3.7s) ✔ [3360/3377] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (6.8s) ✔ [3363/3377] Built FLT.Mathlib.RingTheory.Localization.BaseChange (3.2s) ✔ [3366/3379] Built FLT.Mathlib.NumberTheory.NumberField.InfinitePlace.Completion (2.9s) ✔ [3368/3379] Built FLT.DedekindDomain.AdicValuation (13s) ✔ [3371/3393] Built FLT.HaarMeasure.HaarChar.AddEquiv (9.4s) ✔ [3373/3393] Built FLT.DedekindDomain.IntegralClosure (8.7s) ✔ [3375/3393] Built FLT.NumberField.Completion.Finite (2.8s) ✔ [3376/3393] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.AdicCompletion (2.1s) ✔ [3377/3393] Built FLT.Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing (13s) ✔ [3378/3403] Built FLT.HaarMeasure.HaarChar.Ring (4.1s) ✔ [3379/3403] Built FLT.Mathlib.Algebra.Module.Submodule.Basic (1.3s) ✔ [3382/3403] Built FLT.Mathlib.Algebra.Algebra.Hom (2.0s) ✔ [3383/3403] Built FLT.Mathlib.RingTheory.TensorProduct.Basis (1.9s) ✔ [3386/3407] Built FLT.Mathlib.Topology.Algebra.MulAction (1.4s) ✔ [3387/3407] Built FLT.NumberField.HeightOneSpectrum (1.9s) ✔ [3388/3407] Built FLT.Mathlib.Algebra.IsDirectLimit (2.5s) ✔ [3389/3407] Built FLT.Mathlib.LinearAlgebra.Pi (1.6s) ✔ [3390/3407] Built FLT.Mathlib.Topology.Algebra.UniformRing (1.5s) ✔ [3391/3407] Built FLT.Mathlib.Topology.Algebra.Algebra.Hom (2.1s) ✔ [3395/3407] Built FLT.Mathlib.Algebra.Algebra.Pi (1.6s) ✔ [3397/3407] Built FLT.Mathlib.Algebra.Algebra.Bilinear (2.5s) ✔ [3398/3422] Built FLT.DedekindDomain.FiniteAdeleRing.IsDirectLimitRestricted (2.1s) ✔ [3400/3422] Built FLT.Mathlib.NumberTheory.NumberField.FiniteAdeleRing (3.5s) ✔ [3401/3423] Built FLT.Mathlib.NumberTheory.NumberField.InfiniteAdeleRing (3.7s) ✔ [3404/3423] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.FiniteAdeleRing (2.5s) ✔ [3405/3423] Built FLT.Mathlib.Topology.Algebra.RestrictedProduct.Module (8.0s) ✔ [3406/3423] Built FLT.Mathlib.Topology.Algebra.Group.Quotient (1.7s) ✔ [3407/3423] Built FLT.Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (2.9s) ✔ [3408/3423] Built FLT.Mathlib.Topology.Algebra.ContinuousAlgEquiv (1.9s) ✔ [3409/3423] Built FLT.Mathlib.Topology.Algebra.Module.FiniteDimension (1.0s) ✔ [3410/3426] Built FLT.DedekindDomain.FiniteAdeleRing.TensorRestrictedProduct (10s) ✔ [3412/3426] Built FLT.NumberField.InfinitePlace.Extension (3.4s) ✔ [3415/3435] Built FLT.Mathlib.Topology.Constructions (1.2s) ✔ [3417/3435] Built FLT.Mathlib.NumberTheory.NumberField.AdeleRing (2.4s) ✔ [3419/3435] Built FLT.Mathlib.Topology.Algebra.Module.Equiv (2.8s) ✔ [3420/3435] Built FLT.Mathlib.Topology.MetricSpace.Pseudo.Matrix (2.3s) ✔ [3421/3435] Built FLT.Mathlib.Data.Real.Archimedean (1.0s) ✔ [3423/3435] Built FLT.Mathlib.LinearAlgebra.Matrix.Transvection (2.8s) ✔ [3425/3438] Built FLT.NumberField.Padics.RestrictedProduct (4.5s) ✔ [3426/3438] Built FLT.Mathlib.Topology.MetricSpace.ProperSpace.InfinitePlace (3.0s) ✔ [3428/3438] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.InfinitePlace (3.2s) ✔ [3430/3454] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.AdeleRing (2.4s) ✔ [3436/3460] Built FLT.Mathlib.RingTheory.SimpleRing.TensorProduct (8.9s) ✔ [3439/3463] Built FLT.Mathlib.NumberTheory.Padics.PadicIntegers (3.5s) ✔ [3441/3463] Built FLT.Mathlib.LinearAlgebra.TensorProduct.FiniteFree (2.0s) ✔ [3442/3466] Built FLT.Mathlib.NumberTheory.Padics.HeightOneSpectrum (5.6s) ✔ [3443/3466] Built FLT.Mathlib.LinearAlgebra.TensorProduct.Algebra (2.8s) ✔ [3444/3466] Built FLT.HaarMeasure.MeasurableSpacePadics (2.9s) ✔ [3447/3466] Built FLT.HaarMeasure.HaarChar.RealComplex (4.1s) ✔ [3449/3466] Built FLT.Mathlib.LinearAlgebra.TensorProduct.Basis (2.3s) ✔ [3450/3466] Built FLT.Mathlib.Topology.Algebra.Module.TensorProduct (4.2s) ✔ [3452/3466] Built FLT.HaarMeasure.HaarChar.Padic (4.0s) ✔ [3453/3466] Built FLT.Mathlib.Algebra.Central.TensorProduct (3.7s) ✔ [3455/3467] Built FLT.Mathlib.GroupTheory.DoubleCoset (1.6s) ✔ [3456/3471] Built FLT.NumberField.Completion.Infinite (28s) ✔ [3458/3471] Built FLT.Mathlib.LinearAlgebra.Determinant (5.7s) ✔ [3461/3485] Built FLT.DedekindDomain.FiniteAdeleRing.TensorProduct (9.5s) ✔ [3469/3485] Built FLT.DedekindDomain.Completion.BaseChange (54s) ✔ [3470/3485] Built FLT.HaarMeasure.HaarChar.FiniteDimensional (4.2s) ✔ [3472/3496] Built FLT.Mathlib.Topology.HomToDiscrete (2.0s) ✔ [3473/3496] Built FLT.Mathlib.Topology.Polish (1.9s) ✔ [3475/3497] Built FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Abstract (2.6s) ✔ [3477/3497] Built FLT.Mathlib.Topology.Algebra.Valued.ValuationTopology (2.1s) ✔ [3478/3497] Built FLT.Mathlib.Topology.Instances.Matrix (1.5s) ✔ [3479/3497] Built FLT.NumberField.InfiniteAdeleRing (16s) ✔ [3482/3497] Built FLT.Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs (1.9s) ✔ [3484/3500] Built FLT.Mathlib.MeasureTheory.Haar.Extension (2.6s) ✔ [3487/3500] Built FLT.DedekindDomain.FiniteAdeleRing.LocalUnits (4.3s) ✔ [3664/3710] Built FLT.Mathlib.Algebra.IsQuaternionAlgebra (2.1s) ✔ [3698/3714] Built FLT.Deformations.RepresentationTheory.ContinuousSMulDiscrete (1.8s) ✔ [3702/3734] Built FLT.Basic.FreyPackage (5.4s) ✔ [3719/3736] Built FLT.QuaternionAlgebra.NumberField (12s) ✔ [3721/3737] Built FLT.Deformations.Lemmas (6.1s) ✔ [3725/3744] Built FLT.Deformations.RepresentationTheory.IntegralClosure (3.7s) ✔ [3730/3758] Built FLT.Deformations.RepresentationTheory.Frobenius (5.0s) ✔ [3745/3758] Built FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Local (11s) ✔ [3747/3763] Built FLT.HaarMeasure.HaarChar.FiniteAdeleRing (48s) ✔ [3755/3782] Built FLT.AutomorphicForm.QuaternionAlgebra.HeckeOperators.Concrete (13s) ✔ [3772/3803] Built FLT.Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas (2.0s) ✔ [3778/3803] Built FLT.Deformations.RepresentationTheory.AbsoluteGaloisGroup (18s) ✔ [3779/3803] Built FLT.Data.Hurwitz (6.0s) ✔ [3780/3803] Built FLT.Deformations.RepresentationTheory.Etale (13s) ✔ [3782/3805] Built FLT.Data.QHat (9.4s) ✔ [3784/3805] Built FLT.Patching.Utils.InverseLimit (1.4s) ✔ [3785/3805] Built FLT.Deformations.Algebra.InverseLimit.Basic (7.4s) ✔ [3787/3806] Built FLT.Data.HurwitzRatHat (2.7s) ✔ [3790/3825] Built FLT.Deformations.Algebra.InverseLimit.Topology (4.6s) ✔ [3795/3825] Built FLT.Patching.Utils.Lemmas (6.1s) ✔ [3797/3825] Built FLT.Mathlib.RingTheory.LocalRing.Defs (1.6s) ✔ [3798/3825] Built FLT.Mathlib.RepresentationTheory.Basic (2.5s) ✔ [3800/3825] Built FLT.GaloisRepresentation.Cyclotomic (2.3s) ✔ [3801/3825] Built FLT.Deformations.Subfunctor (1.2s) ✔ [3802/3825] Built FLT.Deformations.IsResidueAlgebra (2.6s) ✔ [3803/3825] Built FLT.Deformations.RepresentationTheory.GaloisRep (15s) ✔ [3804/3830] Built FLT.Patching.Utils.AdicTopology (4.4s) ✔ [3805/3830] Built FLT.Deformations.RepresentationTheory.Irreducible (1.5s) ✔ [3806/3830] Built FLT.DedekindDomain.FiniteAdeleRing.BaseChange (80s) ✔ [3807/3830] Built FLT.Deformations.RepresentationTheory.GaloisRepFamily (2.2s) ✔ [3808/3830] Built FLT.GaloisRepresentation.Automorphic (3.0s) ✔ [3810/3865] Built FLT.EllipticCurve.Torsion (2.6s) ✔ [3932/3966] Built FLT.GaloisRepresentation.HardlyRamified.Defs (2.6s) ✔ [3933/3966] Built FLT.GroupScheme.FiniteFlat (256ms) ✔ [3934/3966] Built FLT.Deformations.IsProartinian (2.3s) ✔ [3935/3966] Built FLT.Mathlib.Data.Fin.Basic (1.1s) ✔ [3936/3966] Built FLT.Mathlib.Algebra.Order.AbsoluteValue.Basic (1.6s) ✔ [3937/3966] Built FLT.Mathlib.Analysis.Normed.Ring.WithAbs (1.8s) ✔ [3938/3966] Built FLT.Mathlib.Data.Set.Prod (577ms) ✔ [3939/3966] Built FLT.Mathlib.GroupTheory.Index (1.2s) ✔ [3940/3966] Built FLT.Mathlib.MeasureTheory.Constructions.BorelSpace.Padic (1.4s) ✔ [3942/3966] Built FLT.Mathlib.MeasureTheory.Measure.Regular (1.4s) ✔ [3944/3966] Built FLT.Mathlib.NumberTheory.NumberField.Completion (1.4s) ✔ [3945/3966] Built FLT.Mathlib.Topology.Algebra.Monoid (1.3s) ✔ [3946/3966] Built FLT.GaloisRepresentation.HardlyRamified.Threeadic (2.0s) ✔ [3947/3966] Built FLT.GaloisRepresentation.HardlyRamified.ModThree (2.3s) ✔ [3948/3966] Built FLT.GaloisRepresentation.HardlyRamified.Lift (2.2s) ✔ [3949/3966] Built FLT.GaloisRepresentation.HardlyRamified.Family (2.6s) ✔ [3950/3969] Built FLT.GaloisRepresentation.HardlyRamified.Frey (2.2s) ✔ [3952/3971] Built FLT.Deformations.Categories (3.9s) ✔ [3956/3983] Built FLT.Basic.Reductions (2.5s) ✔ [3959/3983] Built FLT.Mathlib.Topology.Algebra.Order.Field (3.0s) ✔ [3966/3985] Built FLT.Patching.Utils.TopologicallyFG (1.8s) ✔ [3969/3985] Built FLT.Deformations.LiftFunctor (4.9s) ✔ [3970/3985] Built FLT.NumberField.DiscriminantBounds (4.4s) ✔ [3972/3985] Built FLT.Patching.Utils.StructureFiniteness (4.9s) ✔ [3975/4009] Built FLT.Deformations.Representable (3.3s) ✔ [3991/4009] Built FLT.TateCurve.TateCurve (267ms) ✔ [3992/4009] Built FLT.GlobalLanglandsConjectures.GLnDefs (10s) ✔ [3993/4009] Built FLT.Patching.Utils.CompactHausdorffRings (3.4s) ✔ [3994/4009] Built FLT.Patching.Utils.Depth (5.0s) ✔ [3995/4009] Built FLT.GlobalLanglandsConjectures.GLzero (3.7s) ✔ [3996/4009] Built FLT.Patching.Ultraproduct (11s) ✔ [3997/4009] Built FLT.NumberField.AdeleRing (34s) ✔ [3998/4009] Built FLT.Patching.VanishingFilter (3.5s) ✔ [3999/4009] Built FLT.Patching.Algebra (13s) ✔ [4000/4009] Built FLT.HaarMeasure.HaarChar.AdeleRing (14s) ✔ [4001/4009] Built FLT.Patching.Module (15s) ✔ [4002/4009] Built FLT.Patching.Over (13s) ✔ [4003/4009] Built FLT.Patching.System (10s) ✔ [4004/4009] Built FLT.Patching.REqualsT (3.0s) ✔ [4005/4009] Built FLT.DivisionAlgebra.Finiteness (42s) ✔ [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: 12700 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)
def canonical_json(obj):
if isinstance(obj, dict):
return {k: canonical_json(v) for k, v in sorted(obj.items())}
if isinstance(obj, list):
return [canonical_json(v) for v in obj]
return obj
without_checksum = {k: v for k, v in response.items() if k != "checksum"}
canonical = json.dumps(canonical_json(without_checksum), 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