Job 1179

CakeML:ac8cff50e9e17d1e0608b4dc0c402cad4d9bc10a
  More translator debugging and fixing [Feb 07 13:02:03]
#724 (constrain_op_case)
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:oven2 4.15.0-34-generic x86_64 GNU/Linux

Feb 10 09:43:49 Claimed job
Feb 10 09:43:55 Building HOL
Feb 10 09:53:42 Starting developers
Feb 10 09:53:45 Finished developers                                               2s 112MB
Feb 10 09:53:45 Starting developers/bin
Feb 10 09:53:52 Finished developers/bin                                           7s   1GB
Feb 10 09:53:53 Starting semantics/ffi
Feb 10 09:54:01 Finished semantics/ffi                                            8s 242MB
Feb 10 09:54:01 Starting semantics
Feb 10 09:55:28 Finished semantics                                             1m26s   1GB
Feb 10 09:55:28 Starting semantics/proofs
Feb 10 09:58:37 Finished semantics/proofs                                      3m08s   1GB
Feb 10 09:58:37 Starting semantics/alt_semantics
Feb 10 09:58:44 Finished semantics/alt_semantics                                  6s 315MB
Feb 10 09:58:44 Starting semantics/alt_semantics/proofs
Feb 10 10:00:43 Finished semantics/alt_semantics/proofs                        1m58s 814MB
Feb 10 10:00:43 Starting basis/pure
Feb 10 10:03:30 Finished basis/pure                                            2m47s 934MB
Feb 10 10:03:30 Starting translator
Feb 10 10:06:00 Finished translator                                            2m28s   1GB
Feb 10 10:06:00 Starting compiler/parsing
Feb 10 10:07:05 Finished compiler/parsing                                      1m04s   3GB
Feb 10 10:07:05 Starting characteristic
Feb 10 10:12:41 Finished characteristic                                        5m35s   1GB
Feb 10 10:12:42 Starting translator/monadic
Feb 10 10:14:14 Finished translator/monadic                                    1m32s   1GB
Feb 10 10:14:14 Starting basis
Feb 10 10:47:04 Finished basis                                                32m49s  20GB
Feb 10 10:47:04 Starting compiler/inference
Feb 10 10:48:08 Finished compiler/inference                                    1m03s   1GB
Feb 10 10:48:08 Starting compiler/backend/reg_alloc
Feb 10 10:49:08 Finished compiler/backend/reg_alloc                            1m00s   1GB
Feb 10 10:49:09 Starting compiler/backend/gc
Feb 10 10:52:24 Finished compiler/backend/gc                                   3m15s   2GB
Feb 10 10:52:24 Starting compiler/backend
Feb 10 10:56:46 Finished compiler/backend                                      4m21s   3GB
Feb 10 10:56:46 Starting compiler/encoders/asm
Feb 10 10:57:06 Finished compiler/encoders/asm                                   20s 809MB
Feb 10 10:57:07 Starting compiler/encoders/x64
Feb 10 10:57:59 Finished compiler/encoders/x64                                   52s 991MB
Feb 10 10:58:00 Starting compiler/encoders/arm7
Feb 10 10:59:45 Finished compiler/encoders/arm7                                1m44s   1GB
Feb 10 10:59:45 Starting compiler/encoders/arm8
Feb 10 11:00:16 Finished compiler/encoders/arm8                                  31s 850MB
Feb 10 11:00:16 Starting compiler/encoders/mips
Feb 10 11:01:21 Finished compiler/encoders/mips                                1m04s   1GB
Feb 10 11:01:21 Starting compiler/encoders/riscv
Feb 10 11:02:41 Finished compiler/encoders/riscv                               1m19s   1GB
Feb 10 11:02:41 Starting compiler/encoders/ag32
Feb 10 11:02:57 Finished compiler/encoders/ag32                                  15s 795MB
Feb 10 11:02:57 Starting compiler/backend/x64
Feb 10 11:03:16 Finished compiler/backend/x64                                    18s   1GB
Feb 10 11:03:16 Starting compiler/backend/arm7
Feb 10 11:03:35 Finished compiler/backend/arm7                                   19s   1GB
Feb 10 11:03:35 Starting compiler/backend/arm8
Feb 10 11:03:54 Finished compiler/backend/arm8                                   18s   1GB
Feb 10 11:03:54 Starting compiler/backend/mips
Feb 10 11:04:12 Finished compiler/backend/mips                                   18s   1GB
Feb 10 11:04:12 Starting compiler/backend/riscv
Feb 10 11:04:30 Finished compiler/backend/riscv                                  17s   1GB
Feb 10 11:04:30 Starting compiler/backend/ag32
Feb 10 11:05:37 Finished compiler/backend/ag32                                 1m07s 947MB
Feb 10 11:05:37 Starting compiler/parsing/proofs
Feb 10 11:11:15 Finished compiler/parsing/proofs                               5m37s   1GB
Feb 10 11:11:15 Starting compiler/inference/proofs
Feb 10 11:13:34 Finished compiler/inference/proofs                             2m18s 893MB
Feb 10 11:13:34 Starting compiler/backend/semantics
Feb 10 11:40:03 Finished compiler/backend/semantics                           26m28s   2GB
Feb 10 11:40:03 Starting compiler/backend/reg_alloc/proofs
Feb 10 11:43:19 Finished compiler/backend/reg_alloc/proofs                     3m15s 866MB
Feb 10 11:43:19 Starting compiler/backend/proofs
Feb 10 12:44:00 Finished compiler/backend/proofs                            1h00m40s  19GB
Feb 10 12:44:00 Starting compiler/encoders/x64/proofs
Feb 10 12:52:56 Finished compiler/encoders/x64/proofs                          8m56s   5GB
Feb 10 12:52:57 Starting compiler/encoders/arm7/proofs
Feb 10 13:05:08 Finished compiler/encoders/arm7/proofs                        12m11s   3GB
Feb 10 13:05:08 Starting compiler/encoders/arm8/proofs
Feb 10 13:11:21 Finished compiler/encoders/arm8/proofs                         6m13s   1GB
Feb 10 13:11:21 Starting compiler/encoders/mips/proofs
Feb 10 13:20:32 Finished compiler/encoders/mips/proofs                         9m10s   2GB
Feb 10 13:20:32 Starting compiler/encoders/riscv/proofs
Feb 10 13:28:48 Finished compiler/encoders/riscv/proofs                        8m15s   1GB
Feb 10 13:28:48 Starting compiler/encoders/ag32/proofs
Feb 10 13:31:11 Finished compiler/encoders/ag32/proofs                         2m22s 785MB
Feb 10 13:31:11 Starting compiler/backend/x64/proofs
Feb 10 13:31:30 Finished compiler/backend/x64/proofs                             19s   1GB
Feb 10 13:31:30 Starting compiler/backend/arm7/proofs
Feb 10 13:31:50 Finished compiler/backend/arm7/proofs                            19s   1GB
Feb 10 13:31:50 Starting compiler/backend/arm8/proofs
Feb 10 13:32:09 Finished compiler/backend/arm8/proofs                            18s 834MB
Feb 10 13:32:09 Starting compiler/backend/mips/proofs
Feb 10 13:32:29 Finished compiler/backend/mips/proofs                            19s   1GB
Feb 10 13:32:29 Starting compiler/backend/riscv/proofs
Feb 10 13:32:49 Finished compiler/backend/riscv/proofs                           19s   1GB
Feb 10 13:32:49 Starting compiler/backend/ag32/proofs
Feb 10 13:44:56 Finished compiler/backend/ag32/proofs                         12m07s   3GB
Feb 10 13:44:57 Starting compiler/proofs
Feb 10 13:46:43 Finished compiler/proofs                                       1m46s   3GB
Feb 10 13:46:44 Starting candle/set-theory
Feb 10 13:47:11 Finished candle/set-theory                                       27s 816MB
Feb 10 13:47:11 Starting candle/syntax-lib
Feb 10 13:47:21 Finished candle/syntax-lib                                        9s 653MB
Feb 10 13:47:21 Starting candle/standard/syntax
Feb 10 13:49:05 Finished candle/standard/syntax                                1m44s   1GB
Feb 10 13:49:05 Starting candle/standard/semantics
Feb 10 13:50:43 Finished candle/standard/semantics                             1m37s   1GB
Feb 10 13:50:43 Starting candle/standard/monadic
Feb 10 13:52:17 Finished candle/standard/monadic                               1m33s   1GB
Feb 10 13:52:17 Starting candle/standard/ml_kernel
Feb 10 13:57:11 Finished candle/standard/ml_kernel                             4m53s   3GB
Feb 10 13:57:11 Starting candle/standard/opentheory
Feb 10 14:06:24 Finished candle/standard/opentheory                            9m12s   4GB
Feb 10 14:06:24 Starting candle/standard/opentheory/compilation
Feb 10 14:38:27 Finished candle/standard/opentheory/compilation               32m03s  25GB
Feb 10 14:38:28 Starting candle/standard/opentheory/compilation/proofs
Feb 10 14:39:08 Finished candle/standard/opentheory/compilation/proofs           40s   3GB
Feb 10 14:39:08 Starting characteristic/examples
Feb 10 14:40:37 Finished characteristic/examples                               1m28s   2GB
Feb 10 14:40:37 Starting tutorial/solutions
Feb 10 14:55:01 Finished tutorial/solutions                                   14m24s   6GB
Feb 10 14:55:01 Starting translator/monadic/examples
Feb 10 14:57:58 Finished translator/monadic/examples                           2m56s   2GB
Feb 10 14:57:58 Starting examples
Feb 10 15:07:15 Finished examples                                              9m16s   3GB
Feb 10 15:07:15 Starting examples/compilation/x64
Feb 10 17:23:45 Finished examples/compilation/x64                           2h16m28s  12GB
Feb 10 17:23:45 Starting examples/compilation/x64/proofs
Feb 10 17:25:23 Finished examples/compilation/x64/proofs                       1m37s   3GB
Feb 10 17:25:23 Starting examples/compilation/ag32
Feb 10 17:55:13 Finished examples/compilation/ag32                            29m49s   6GB
Feb 10 17:55:13 Starting examples/compilation/ag32/proofs
Feb 10 17:55:57 Finished examples/compilation/ag32/proofs                        43s   3GB
Feb 10 17:55:57 Starting examples/cost
Feb 10 18:37:26 Finished examples/cost                                        41m28s   7GB
Feb 10 18:37:26 Starting examples/lpr_checker
Feb 10 18:41:11 Finished examples/lpr_checker                                  3m44s   4GB
Feb 10 18:41:11 Starting examples/lpr_checker/compilation
Feb 10 18:58:02 Finished examples/lpr_checker/compilation                     16m51s   9GB
Feb 10 18:58:02 Starting examples/lpr_checker/compilation/proofs
Feb 10 18:58:42 Finished examples/lpr_checker/compilation/proofs                 39s   3GB
Feb 10 18:58:42 Starting examples/lpr_checker/array
Feb 10 19:08:01 Finished examples/lpr_checker/array                            9m18s   3GB
Feb 10 19:08:01 Starting examples/lpr_checker/array/compilation
Feb 10 19:23:32 Finished examples/lpr_checker/array/compilation               15m31s   7GB
Feb 10 19:23:32 Starting examples/lpr_checker/array/compilation/proofs
Feb 10 19:24:19 Finished examples/lpr_checker/array/compilation/proofs           46s   3GB
Feb 10 19:24:19 Starting translator/okasaki-examples
Feb 10 19:28:30 Finished translator/okasaki-examples                           4m10s   1GB
Feb 10 19:28:30 Starting translator/other-examples
Feb 10 19:30:19 Finished translator/other-examples                             1m48s   1GB
Feb 10 19:30:19 Starting compiler/parsing/tests
Feb 10 19:30:43 Finished compiler/parsing/tests                                  24s 561MB
Feb 10 19:30:44 Starting compiler/inference/tests
Feb 12 06:18:07 Resuming compiler/inference/tests