Job 1180

CakeML:6810c429dfe49d0cf051af09b3aba612f609af8b
  Fix parsing of large floats as in #725 [Feb 10 12:18:25]
#726 (fix_fp_ffi)
Merging into:bc31859d41b156f0209a253ab1cee3f334e9b742
  Fix type error caused by HOL change to ThmSetData API [Feb 10 03:15:23]
HOL:1ada1617c02bd7b9335a433e842dc2590e539c6b
  Revert "Eta-expand GEN_REWRITE_CONV so that bounded rewrites work bet [Feb 08 01:35:04]
Machine:stove 4.15.0-55-generic x86_64 GNU/Linux

Feb 10 12:34:54 Claimed job
Feb 10 12:35:00 Building HOL
Feb 10 12:45:33 Starting developers
Feb 10 12:45:37 Finished developers                                               4s 102MB
Feb 10 12:45:37 Starting developers/bin
Feb 10 12:45:44 Finished developers/bin                                           6s   1GB
Feb 10 12:45:44 Starting semantics/ffi
Feb 10 12:45:54 Finished semantics/ffi                                            9s 247MB
Feb 10 12:45:54 Starting semantics
Feb 10 12:47:20 Finished semantics                                             1m26s   1GB
Feb 10 12:47:20 Starting semantics/proofs
Feb 10 12:50:28 Finished semantics/proofs                                      3m07s   1GB
Feb 10 12:50:28 Starting semantics/alt_semantics
Feb 10 12:50:36 Finished semantics/alt_semantics                                  7s 330MB
Feb 10 12:50:36 Starting semantics/alt_semantics/proofs
Feb 10 12:52:35 Finished semantics/alt_semantics/proofs                        1m58s 752MB
Feb 10 12:52:35 Starting basis/pure
Feb 10 12:55:20 Finished basis/pure                                            2m44s 795MB
Feb 10 12:55:20 Starting translator
Feb 10 12:57:46 Finished translator                                            2m25s   1GB
Feb 10 12:57:46 Starting compiler/parsing
Feb 10 12:58:49 Finished compiler/parsing                                      1m02s   2GB
Feb 10 12:58:49 Starting characteristic
Feb 10 13:04:21 Finished characteristic                                        5m32s   2GB
Feb 10 13:04:21 Starting translator/monadic
Feb 10 13:05:56 Finished translator/monadic                                    1m33s   1GB
Feb 10 13:05:56 Starting basis
Feb 10 13:37:46 Finished basis                                                31m48s  20GB
Feb 10 13:37:46 Starting compiler/inference
Feb 10 13:39:54 Finished compiler/inference                                    2m07s   2GB
Feb 10 13:39:54 Starting compiler/backend/reg_alloc
Feb 10 13:40:53 Finished compiler/backend/reg_alloc                              59s   1GB
Feb 10 13:40:53 Starting compiler/backend/gc
Feb 10 13:44:00 Finished compiler/backend/gc                                   3m06s   2GB
Feb 10 13:44:00 Starting compiler/backend
Feb 10 13:48:09 Finished compiler/backend                                      4m08s   3GB
Feb 10 13:48:09 Starting compiler/encoders/asm
Feb 10 13:48:30 Finished compiler/encoders/asm                                   20s 790MB
Feb 10 13:48:30 Starting compiler/encoders/x64
Feb 10 13:49:23 Finished compiler/encoders/x64                                   53s 999MB
Feb 10 13:49:23 Starting compiler/encoders/arm7
Feb 10 13:51:02 Finished compiler/encoders/arm7                                1m38s   1GB
Feb 10 13:51:02 Starting compiler/encoders/arm8
Feb 10 13:51:34 Finished compiler/encoders/arm8                                  31s 838MB
Feb 10 13:51:34 Starting compiler/encoders/mips
Feb 10 13:52:38 Finished compiler/encoders/mips                                1m03s   1GB
Feb 10 13:52:38 Starting compiler/encoders/riscv
Feb 10 13:53:54 Finished compiler/encoders/riscv                               1m16s 832MB
Feb 10 13:53:54 Starting compiler/encoders/ag32
Feb 10 13:54:11 Finished compiler/encoders/ag32                                  17s 776MB
Feb 10 13:54:11 Starting compiler/backend/x64
Feb 10 13:54:29 Finished compiler/backend/x64                                    17s   1GB
Feb 10 13:54:30 Starting compiler/backend/arm7
Feb 10 13:54:48 Finished compiler/backend/arm7                                   18s   1GB
Feb 10 13:54:49 Starting compiler/backend/arm8
Feb 10 13:55:06 Finished compiler/backend/arm8                                   16s   1GB
Feb 10 13:55:06 Starting compiler/backend/mips
Feb 10 13:55:24 Finished compiler/backend/mips                                   18s   1GB
Feb 10 13:55:24 Starting compiler/backend/riscv
Feb 10 13:55:43 Finished compiler/backend/riscv                                  18s   1GB
Feb 10 13:55:43 Starting compiler/backend/ag32
Feb 10 13:56:48 Finished compiler/backend/ag32                                 1m04s   1GB
Feb 10 13:56:48 Starting compiler/parsing/proofs
Feb 10 14:02:12 Finished compiler/parsing/proofs                               5m24s   1GB
Feb 10 14:02:13 Starting compiler/inference/proofs
Feb 10 14:05:02 Finished compiler/inference/proofs                             2m49s   1GB
Feb 10 14:05:02 Starting compiler/backend/semantics
Feb 10 14:30:47 Finished compiler/backend/semantics                           25m44s   2GB
Feb 10 14:30:47 Starting compiler/backend/reg_alloc/proofs
Feb 10 14:34:01 Finished compiler/backend/reg_alloc/proofs                     3m13s   1GB
Feb 10 14:34:01 Starting compiler/backend/proofs
Feb 10 15:30:50 Finished compiler/backend/proofs                              56m48s  21GB
Feb 10 15:30:50 Starting compiler/encoders/x64/proofs
Feb 10 15:39:50 Finished compiler/encoders/x64/proofs                          9m00s   4GB
Feb 10 15:39:50 Starting compiler/encoders/arm7/proofs
Feb 10 15:51:50 Finished compiler/encoders/arm7/proofs                        11m59s   3GB
Feb 10 15:51:50 Starting compiler/encoders/arm8/proofs
Feb 10 15:57:51 Finished compiler/encoders/arm8/proofs                         6m01s   1GB
Feb 10 15:57:51 Starting compiler/encoders/mips/proofs
Feb 10 16:06:58 Finished compiler/encoders/mips/proofs                         9m05s   2GB
Feb 10 16:06:58 Starting compiler/encoders/riscv/proofs
Feb 10 16:15:11 Finished compiler/encoders/riscv/proofs                        8m13s   1GB
Feb 10 16:15:11 Starting compiler/encoders/ag32/proofs
Feb 10 16:17:32 Finished compiler/encoders/ag32/proofs                         2m20s 973MB
Feb 10 16:17:32 Starting compiler/backend/x64/proofs
Feb 10 16:17:51 Finished compiler/backend/x64/proofs                             19s   1GB
Feb 10 16:17:52 Starting compiler/backend/arm7/proofs
Feb 10 16:18:13 Finished compiler/backend/arm7/proofs                            20s   1GB
Feb 10 16:18:13 Starting compiler/backend/arm8/proofs
Feb 10 16:18:33 Finished compiler/backend/arm8/proofs                            20s   1GB
Feb 10 16:18:33 Starting compiler/backend/mips/proofs
Feb 10 16:18:53 Finished compiler/backend/mips/proofs                            19s   1GB
Feb 10 16:18:53 Starting compiler/backend/riscv/proofs
Feb 10 16:19:13 Finished compiler/backend/riscv/proofs                           19s   1GB
Feb 10 16:19:13 Starting compiler/backend/ag32/proofs
Feb 10 16:31:30 Finished compiler/backend/ag32/proofs                         12m16s   2GB
Feb 10 16:31:30 Starting compiler/proofs
Feb 10 16:33:15 Finished compiler/proofs                                       1m45s   3GB
Feb 10 16:33:15 Starting candle/set-theory
Feb 10 16:33:43 Finished candle/set-theory                                       27s 761MB
Feb 10 16:33:43 Starting candle/syntax-lib
Feb 10 16:33:53 Finished candle/syntax-lib                                       10s 647MB
Feb 10 16:33:53 Starting candle/standard/syntax
Feb 10 16:35:35 Finished candle/standard/syntax                                1m41s   1GB
Feb 10 16:35:35 Starting candle/standard/semantics
Feb 10 16:37:13 Finished candle/standard/semantics                             1m38s   1GB
Feb 10 16:37:13 Starting candle/standard/monadic
Feb 10 16:38:45 Finished candle/standard/monadic                               1m32s   1GB
Feb 10 16:38:46 Starting candle/standard/ml_kernel
Feb 10 16:43:41 Finished candle/standard/ml_kernel                             4m55s   4GB
Feb 10 16:43:41 Starting candle/standard/opentheory
Feb 10 16:52:43 Finished candle/standard/opentheory                            9m01s   4GB
Feb 10 16:52:43 Starting candle/standard/opentheory/compilation
Feb 10 17:23:20 Finished candle/standard/opentheory/compilation               30m36s  16GB
Feb 10 17:23:20 Starting candle/standard/opentheory/compilation/proofs
Feb 10 17:23:58 Finished candle/standard/opentheory/compilation/proofs           38s   4GB
Feb 10 17:23:58 Starting characteristic/examples
Feb 10 17:25:27 Finished characteristic/examples                               1m28s   2GB
Feb 10 17:25:27 Starting tutorial/solutions
Feb 10 17:39:36 Finished tutorial/solutions                                   14m08s   7GB
Feb 10 17:39:36 Starting translator/monadic/examples
Feb 10 17:42:27 Finished translator/monadic/examples                           2m51s   2GB
Feb 10 17:42:27 Starting examples
Feb 10 17:50:51 Finished examples                                              8m23s   3GB
Feb 10 17:50:51 Starting examples/compilation/x64
Feb 10 20:04:04 Finished examples/compilation/x64                           2h13m12s  14GB
Feb 10 20:04:04 Starting examples/compilation/x64/proofs
Feb 10 20:05:40 Finished examples/compilation/x64/proofs                       1m35s   2GB
Feb 10 20:05:40 Starting examples/compilation/ag32
Feb 10 20:35:35 Finished examples/compilation/ag32                            29m54s   6GB
Feb 10 20:35:35 Starting examples/compilation/ag32/proofs
Feb 10 20:36:17 Finished examples/compilation/ag32/proofs                        41s   3GB
Feb 10 20:36:17 Starting examples/cost
Feb 10 21:15:34 Finished examples/cost                                        39m16s   8GB
Feb 10 21:15:34 Starting examples/lpr_checker
Feb 10 21:19:13 Finished examples/lpr_checker                                  3m38s   3GB
Feb 10 21:19:13 Starting examples/lpr_checker/compilation
Feb 10 21:35:09 Finished examples/lpr_checker/compilation                     15m56s   9GB
Feb 10 21:35:09 Starting examples/lpr_checker/compilation/proofs
Feb 10 21:35:49 Finished examples/lpr_checker/compilation/proofs                 39s   2GB
Feb 10 21:35:49 Starting examples/lpr_checker/array
Feb 10 21:44:45 Finished examples/lpr_checker/array                            8m56s   3GB
Feb 10 21:44:45 Starting examples/lpr_checker/array/compilation
Feb 10 21:59:55 Finished examples/lpr_checker/array/compilation               15m10s   8GB
Feb 10 21:59:56 Starting examples/lpr_checker/array/compilation/proofs
Feb 10 22:00:38 Finished examples/lpr_checker/array/compilation/proofs           42s   3GB
Feb 10 22:00:39 Starting translator/okasaki-examples
Feb 10 22:04:45 Finished translator/okasaki-examples                           4m06s   1GB
Feb 10 22:04:45 Starting translator/other-examples
Feb 10 22:06:31 Finished translator/other-examples                             1m46s   1GB
Feb 10 22:06:31 Starting compiler/parsing/tests
Feb 10 22:06:56 Finished compiler/parsing/tests                                  24s 682MB
Feb 10 22:06:56 Starting compiler/inference/tests
Feb 10 22:11:15 Finished compiler/inference/tests                              4m18s   3GB
Feb 10 22:11:15 Starting compiler/bootstrap/translation
Feb 11 01:37:07 Finished compiler/bootstrap/translation                     3h25m51s  37GB
Feb 11 01:37:07 Starting unverified/sexpr-bootstrap/x64/64
Feb 11 01:52:38 Finished unverified/sexpr-bootstrap/x64/64                    15m30s   7GB
Feb 11 01:52:38 Starting unverified/sexpr-bootstrap/x64/32
Feb 11 02:03:19 Finished unverified/sexpr-bootstrap/x64/32                    10m40s   8GB
Feb 11 02:03:19 Starting compiler/benchmarks
Feb 11 02:03:21 Finished compiler/benchmarks                                      1s  33MB
Feb 11 02:03:21 Starting compiler/bootstrap/compilation/x64/64
Feb 11 16:09:19 Finished compiler/bootstrap/compilation/x64/64             14h05m57s  64GB
Feb 11 16:09:19 Starting compiler/bootstrap/compilation/x64/64/proofs
Feb 11 16:12:52 Finished compiler/bootstrap/compilation/x64/64/proofs          3m32s  16GB
Feb 11 16:12:52 Starting compiler/bootstrap/compilation/x64/32
Feb 13 14:42:18 Resuming compiler/bootstrap/compilation/x64/32
Feb 13 17:16:33 Finished compiler/bootstrap/compilation/x64/32              2h34m13s  64GB
Feb 13 17:16:33 Starting compiler/bootstrap/compilation/x64/32/proofs
Feb 13 17:19:52 Finished compiler/bootstrap/compilation/x64/32/proofs          3m19s  14GB
Feb 13 17:19:52 Starting compiler/bootstrap/compilation/ag32/32
Feb 14 07:12:42 Finished compiler/bootstrap/compilation/ag32/32            13h52m49s  64GB
Feb 14 07:12:42 Starting compiler/bootstrap/compilation/ag32/32/proofs
Feb 14 07:28:40 Finished compiler/bootstrap/compilation/ag32/32/proofs        15m57s  31GB
Feb 14 07:28:40 SUCCESS