Job 972

CakeML:f1d2a87b9c33a17a9a43afe09045efc348d14f68
  Update a top-of-file comment and sync basis/README.md [Jul 30 07:25:29]
#671 (fp_basis)
Merging into:112863b9cb5837f7731f07322f6a70494471f50d
  Merge pull request #674 from CakeML/zero-byte [Jul 28 19:21:00]
HOL:97dbc36bb2dc0ee2df2198032e6901f15f9dba85
  Start port of material about f.o. compactness from HOL Light [Jul 29 06:57:52]
Machine:te1

Jul 30 07:48:39 Claimed job
Jul 30 07:48:45 Building HOL
Jul 30 08:02:00 Starting developers
Jul 30 08:02:03 Finished developers                                               2s  34MB
Jul 30 08:02:03 Starting developers/bin
Jul 30 08:02:10 Finished developers/bin                                           7s 971MB
Jul 30 08:02:10 Starting semantics/ffi
Jul 30 08:03:06 Finished semantics/ffi                                           55s 598MB
Jul 30 08:03:06 Starting semantics
Jul 30 08:05:22 Finished semantics                                             2m15s   1GB
Jul 30 08:05:22 Starting semantics/proofs
Jul 30 08:09:48 Finished semantics/proofs                                      4m26s   1GB
Jul 30 08:09:48 Starting semantics/alt_semantics
Jul 30 08:10:00 Finished semantics/alt_semantics                                 11s 275MB
Jul 30 08:10:00 Starting semantics/alt_semantics/proofs
Jul 30 08:12:36 Finished semantics/alt_semantics/proofs                        2m36s 862MB
Jul 30 08:12:36 Starting basis/pure
Jul 30 08:17:39 Finished basis/pure                                            5m02s 690MB
Jul 30 08:17:39 Starting translator
Jul 30 08:20:07 Finished translator                                            2m27s   1GB
Jul 30 08:20:07 Starting compiler/parsing
Jul 30 08:21:29 Finished compiler/parsing                                      1m22s   2GB
Jul 30 08:21:29 Starting characteristic
Jul 30 08:28:53 Finished characteristic                                        7m24s   2GB
Jul 30 08:28:53 Starting translator/monadic
Jul 30 08:31:04 Finished translator/monadic                                    2m10s   1GB
Jul 30 08:31:04 Starting basis
Jul 30 08:55:56 Finished basis                                                24m51s   3GB
Jul 30 08:55:56 Starting compiler/inference
Jul 30 08:58:38 Finished compiler/inference                                    2m42s   1GB
Jul 30 08:58:38 Starting compiler/backend/reg_alloc
Jul 30 08:59:59 Finished compiler/backend/reg_alloc                            1m19s   1GB
Jul 30 08:59:59 Starting compiler/backend/gc
Jul 30 09:12:42 Finished compiler/backend/gc                                  12m43s   2GB
Jul 30 09:12:42 Starting compiler/backend
Jul 30 09:12:45 Finished compiler/backend                                         2s  34MB
Jul 30 09:12:45 Starting compiler/encoders/asm
Jul 30 09:12:46 Finished compiler/encoders/asm                                    1s  22MB
Jul 30 09:12:46 Starting compiler/encoders/x64
Jul 30 09:14:13 Finished compiler/encoders/x64                                 1m27s 730MB
Jul 30 09:14:13 Starting compiler/encoders/arm7
Jul 30 09:16:43 Finished compiler/encoders/arm7                                2m29s   1GB
Jul 30 09:16:43 Starting compiler/encoders/arm8
Jul 30 09:17:30 Finished compiler/encoders/arm8                                  47s 531MB
Jul 30 09:17:30 Starting compiler/encoders/mips
Jul 30 09:19:10 Finished compiler/encoders/mips                                1m40s 972MB
Jul 30 09:19:10 Starting compiler/encoders/riscv
Jul 30 09:21:08 Finished compiler/encoders/riscv                               1m57s   1GB
Jul 30 09:21:08 Starting compiler/encoders/ag32
Jul 30 09:21:33 Finished compiler/encoders/ag32                                  24s 806MB
Jul 30 09:21:33 Starting compiler/backend/x64
Jul 30 09:21:57 Finished compiler/backend/x64                                    23s 902MB
Jul 30 09:21:57 Starting compiler/backend/arm7
Jul 30 09:22:25 Finished compiler/backend/arm7                                   27s   1GB
Jul 30 09:22:25 Starting compiler/backend/arm8
Jul 30 09:22:50 Finished compiler/backend/arm8                                   25s   1GB
Jul 30 09:22:51 Starting compiler/backend/mips
Jul 30 09:23:17 Finished compiler/backend/mips                                   26s   1GB
Jul 30 09:23:17 Starting compiler/backend/riscv
Jul 30 09:23:43 Finished compiler/backend/riscv                                  26s   1GB
Jul 30 09:23:43 Starting compiler/backend/ag32
Jul 30 09:25:16 Finished compiler/backend/ag32                                 1m32s   1GB
Jul 30 09:25:16 Starting compiler/parsing/proofs
Jul 30 09:34:21 Finished compiler/parsing/proofs                               9m04s   1GB
Jul 30 09:34:21 Starting compiler/inference/proofs
Jul 30 09:38:23 Finished compiler/inference/proofs                             4m01s 940MB
Jul 30 09:38:23 Starting compiler/backend/semantics
Jul 30 09:48:08 Finished compiler/backend/semantics                            9m44s   1GB
Jul 30 09:48:08 Starting compiler/backend/reg_alloc/proofs
Jul 30 09:52:51 Finished compiler/backend/reg_alloc/proofs                     4m42s 902MB
Jul 30 09:52:51 Starting compiler/backend/proofs
Jul 30 10:45:33 Finished compiler/backend/proofs                              52m42s   5GB
Jul 30 10:45:33 Starting compiler/encoders/x64/proofs
Jul 30 10:59:12 Finished compiler/encoders/x64/proofs                         13m38s   6GB
Jul 30 10:59:12 Starting compiler/encoders/arm7/proofs
Jul 30 11:17:34 Finished compiler/encoders/arm7/proofs                        18m22s   4GB
Jul 30 11:17:34 Starting compiler/encoders/arm8/proofs
Jul 30 11:26:48 Finished compiler/encoders/arm8/proofs                         9m13s   1GB
Jul 30 11:26:48 Starting compiler/encoders/mips/proofs
Jul 30 11:40:19 Finished compiler/encoders/mips/proofs                        13m30s   3GB
Jul 30 11:40:19 Starting compiler/encoders/riscv/proofs
Jul 30 11:51:52 Finished compiler/encoders/riscv/proofs                       11m33s   1GB
Jul 30 11:51:52 Starting compiler/encoders/ag32/proofs
Jul 30 11:55:12 Finished compiler/encoders/ag32/proofs                         3m19s 908MB
Jul 30 11:55:12 Starting compiler/backend/x64/proofs
Jul 30 11:55:39 Finished compiler/backend/x64/proofs                             26s   1GB
Jul 30 11:55:39 Starting compiler/backend/arm7/proofs
Jul 30 11:56:07 Finished compiler/backend/arm7/proofs                            27s   1GB
Jul 30 11:56:07 Starting compiler/backend/arm8/proofs
Jul 30 11:56:32 Finished compiler/backend/arm8/proofs                            25s 826MB
Jul 30 11:56:32 Starting compiler/backend/mips/proofs
Jul 30 11:56:59 Finished compiler/backend/mips/proofs                            26s 949MB
Jul 30 11:56:59 Starting compiler/backend/riscv/proofs
Jul 30 11:57:27 Finished compiler/backend/riscv/proofs                           27s   1GB
Jul 30 11:57:27 Starting compiler/backend/ag32/proofs
Jul 30 12:10:06 Finished compiler/backend/ag32/proofs                         12m38s   2GB
Jul 30 12:10:06 Starting compiler/proofs
Jul 30 12:11:54 Finished compiler/proofs                                       1m47s   3GB
Jul 30 12:11:54 Starting candle/set-theory
Jul 30 12:12:32 Finished candle/set-theory                                       37s 723MB
Jul 30 12:12:32 Starting candle/syntax-lib
Jul 30 12:12:47 Finished candle/syntax-lib                                       15s 667MB
Jul 30 12:12:47 Starting candle/standard/syntax
Jul 30 12:15:13 Finished candle/standard/syntax                                2m25s   1GB
Jul 30 12:15:13 Starting candle/standard/semantics
Jul 30 12:17:37 Finished candle/standard/semantics                             2m24s   1GB
Jul 30 12:17:37 Starting candle/standard/monadic
Jul 30 12:19:49 Finished candle/standard/monadic                               2m12s   1GB
Jul 30 12:19:49 Starting candle/standard/ml_kernel
Jul 30 12:25:02 Finished candle/standard/ml_kernel                             5m12s   3GB
Jul 30 12:25:02 Starting candle/standard/opentheory
Jul 30 12:36:59 Finished candle/standard/opentheory                           11m56s   4GB
Jul 30 12:36:59 Starting candle/standard/opentheory/compilation
Jul 30 13:15:33 Finished candle/standard/opentheory/compilation               38m33s  12GB
Jul 30 13:15:33 Starting candle/standard/opentheory/compilation/proofs
Jul 30 13:16:33 Finished candle/standard/opentheory/compilation/proofs           59s   2GB
Jul 30 13:16:33 Starting characteristic/examples
Jul 30 13:18:31 Finished characteristic/examples                               1m57s   2GB
Jul 30 13:18:31 Starting tutorial/solutions
Jul 30 13:35:43 Finished tutorial/solutions                                   17m12s   9GB
Jul 30 13:35:43 Starting translator/monadic/examples
Jul 30 13:39:21 Finished translator/monadic/examples                           3m38s   2GB
Jul 30 13:39:21 Starting examples
Jul 30 13:49:45 Finished examples                                             10m24s   3GB
Jul 30 13:49:45 Starting examples/compilation/x64
Jul 30 16:35:19 Finished examples/compilation/x64                           2h45m33s  17GB
Jul 30 16:35:19 Starting examples/compilation/x64/proofs
Jul 30 16:37:21 Finished examples/compilation/x64/proofs                       2m01s   2GB
Jul 30 16:37:21 Starting examples/compilation/ag32
Jul 30 17:15:39 Finished examples/compilation/ag32                            38m17s   7GB
Jul 30 17:15:39 Starting examples/compilation/ag32/proofs
Jul 30 17:16:46 Finished examples/compilation/ag32/proofs                      1m07s   3GB
Jul 30 17:16:46 Starting translator/okasaki-examples
Jul 30 17:22:21 Finished translator/okasaki-examples                           5m34s   2GB
Jul 30 17:22:22 Starting translator/other-examples
Jul 30 17:27:28 Finished translator/other-examples                             5m06s   1GB
Jul 30 17:27:28 Starting compiler/parsing/tests
Jul 30 17:28:03 Finished compiler/parsing/tests                                  34s 573MB
Jul 30 17:28:03 Starting compiler/inference/tests
Jul 30 17:33:28 Finished compiler/inference/tests                              5m24s   4GB
Jul 30 17:33:28 Starting compiler/bootstrap/translation
Jul 30 20:53:41 Finished compiler/bootstrap/translation                     3h20m13s  43GB
Jul 30 20:53:41 Starting unverified/sexpr-bootstrap/x64/64
Jul 30 21:10:11 Finished unverified/sexpr-bootstrap/x64/64                    16m29s   3GB
Jul 30 21:10:11 Starting unverified/sexpr-bootstrap/x64/32
Jul 30 21:23:02 Finished unverified/sexpr-bootstrap/x64/32                    12m51s   2GB
Jul 30 21:23:03 Starting compiler/benchmarks
Jul 30 21:23:08 Finished compiler/benchmarks                                      5s  38MB
Jul 30 21:23:09 Starting compiler/bootstrap/compilation/x64/64
Jul 31 13:44:49 Finished compiler/bootstrap/compilation/x64/64             16h21m39s  58GB
Jul 31 13:44:49 Starting compiler/bootstrap/compilation/x64/64/proofs
Jul 31 13:50:40 Finished compiler/bootstrap/compilation/x64/64/proofs          5m51s   5GB
Jul 31 13:50:40 Starting compiler/bootstrap/compilation/x64/32
Aug 01 03:09:34 Finished compiler/bootstrap/compilation/x64/32             13h18m53s  58GB
Aug 01 03:09:34 Starting compiler/bootstrap/compilation/x64/32/proofs
Aug 01 03:14:15 Finished compiler/bootstrap/compilation/x64/32/proofs          4m40s   4GB
Aug 01 03:14:15 Starting compiler/bootstrap/compilation/ag32/32
Aug 05 10:05:31 Resuming compiler/bootstrap/compilation/ag32/32
Aug 06 00:00:06 Finished compiler/bootstrap/compilation/ag32/32            13h54m34s  62GB
Aug 06 00:00:06 Starting compiler/bootstrap/compilation/ag32/32/proofs
Aug 06 00:33:51 Finished compiler/bootstrap/compilation/ag32/32/proofs        33m44s  16GB
Aug 06 00:33:51 SUCCESS