Job 1194

CakeML:11e91a41765701cdc746dfee9a1da9fbe68d7a8d
  Tweak variable names to work around a probably bug [Feb 21 12:21:01]
#724 (constrain_op_case)
Merging into:210f5c2ce0804027acbac59d87eab48cdeed1625
  Merge pull request #727 from IlmariReissumies/ad-hoc-overloading [Feb 21 09:48:53]
HOL:9d20add95c75b8c69157845df5d5e74f24633371
  Merge remote-tracking branch 'origin/interaction-guide-update' into d [Feb 19 09:30:56]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Feb 21 12:28:16 Claimed job
Feb 21 12:28:23 Building HOL
Feb 21 12:39:10 Starting developers
Feb 21 12:39:13 Finished developers                                               2s 101MB
Feb 21 12:39:13 Starting developers/bin
Feb 21 12:39:20 Finished developers/bin                                           6s   1GB
Feb 21 12:39:20 Starting semantics/ffi
Feb 21 12:39:29 Finished semantics/ffi                                            8s 256MB
Feb 21 12:39:29 Starting semantics
Feb 21 12:40:55 Finished semantics                                             1m25s   1GB
Feb 21 12:40:55 Starting semantics/proofs
Feb 21 12:44:05 Finished semantics/proofs                                      3m09s   1GB
Feb 21 12:44:05 Starting semantics/alt_semantics
Feb 21 12:44:12 Finished semantics/alt_semantics                                  6s 327MB
Feb 21 12:44:13 Starting semantics/alt_semantics/proofs
Feb 21 12:46:12 Finished semantics/alt_semantics/proofs                        1m59s 801MB
Feb 21 12:46:12 Starting basis/pure
Feb 21 12:48:58 Finished basis/pure                                            2m45s 771MB
Feb 21 12:48:59 Starting translator
Feb 21 12:51:27 Finished translator                                            2m28s   1GB
Feb 21 12:51:28 Starting compiler/parsing
Feb 21 12:52:36 Finished compiler/parsing                                      1m08s   2GB
Feb 21 12:52:36 Starting characteristic
Feb 21 12:58:09 Finished characteristic                                        5m32s   2GB
Feb 21 12:58:09 Starting translator/monadic
Feb 21 12:59:41 Finished translator/monadic                                    1m30s   1GB
Feb 21 12:59:41 Starting basis
Feb 21 13:29:42 Finished basis                                                29m59s  16GB
Feb 21 13:29:42 Starting compiler/inference
Feb 21 13:30:46 Finished compiler/inference                                    1m03s   1GB
Feb 21 13:30:46 Starting compiler/backend/reg_alloc
Feb 21 13:31:47 Finished compiler/backend/reg_alloc                            1m01s   1GB
Feb 21 13:31:47 Starting compiler/backend/gc
Feb 21 13:35:02 Finished compiler/backend/gc                                   3m14s   2GB
Feb 21 13:35:02 Starting compiler/backend
Feb 21 13:39:24 Finished compiler/backend                                      4m21s   3GB
Feb 21 13:39:24 Starting compiler/encoders/asm
Feb 21 13:39:44 Finished compiler/encoders/asm                                   20s 770MB
Feb 21 13:39:44 Starting compiler/encoders/x64
Feb 21 13:40:37 Finished compiler/encoders/x64                                   52s 969MB
Feb 21 13:40:37 Starting compiler/encoders/arm7
Feb 21 13:42:15 Finished compiler/encoders/arm7                                1m37s   1GB
Feb 21 13:42:15 Starting compiler/encoders/arm8
Feb 21 13:42:46 Finished compiler/encoders/arm8                                  30s 922MB
Feb 21 13:42:46 Starting compiler/encoders/mips
Feb 21 13:43:50 Finished compiler/encoders/mips                                1m03s   1GB
Feb 21 13:43:50 Starting compiler/encoders/riscv
Feb 21 13:45:07 Finished compiler/encoders/riscv                               1m16s 922MB
Feb 21 13:45:07 Starting compiler/encoders/ag32
Feb 21 13:45:23 Finished compiler/encoders/ag32                                  16s 806MB
Feb 21 13:45:23 Starting compiler/backend/x64
Feb 21 13:45:41 Finished compiler/backend/x64                                    17s   1GB
Feb 21 13:45:41 Starting compiler/backend/arm7
Feb 21 13:46:00 Finished compiler/backend/arm7                                   18s   1GB
Feb 21 13:46:00 Starting compiler/backend/arm8
Feb 21 13:46:18 Finished compiler/backend/arm8                                   17s   1GB
Feb 21 13:46:18 Starting compiler/backend/mips
Feb 21 13:46:35 Finished compiler/backend/mips                                   17s   1GB
Feb 21 13:46:35 Starting compiler/backend/riscv
Feb 21 13:46:54 Finished compiler/backend/riscv                                  18s   1GB
Feb 21 13:46:54 Starting compiler/backend/ag32
Feb 21 13:47:59 Finished compiler/backend/ag32                                 1m05s   1GB
Feb 21 13:48:00 Starting compiler/parsing/proofs
Feb 21 13:53:32 Finished compiler/parsing/proofs                               5m32s   1GB
Feb 21 13:53:32 Starting compiler/inference/proofs
Feb 21 13:55:50 Finished compiler/inference/proofs                             2m17s   1GB
Feb 21 13:55:50 Starting compiler/backend/semantics
Feb 21 14:21:38 Finished compiler/backend/semantics                           25m47s   2GB
Feb 21 14:21:39 Starting compiler/backend/reg_alloc/proofs
Feb 21 14:24:57 Finished compiler/backend/reg_alloc/proofs                     3m18s   1GB
Feb 21 14:24:57 Starting compiler/backend/proofs
Feb 21 15:26:04 Finished compiler/backend/proofs                            1h01m06s  20GB
Feb 21 15:26:04 Starting compiler/encoders/x64/proofs
Feb 21 15:35:03 Finished compiler/encoders/x64/proofs                          8m58s   5GB
Feb 21 15:35:03 Starting compiler/encoders/arm7/proofs
Feb 21 15:47:42 Finished compiler/encoders/arm7/proofs                        12m38s   3GB
Feb 21 15:47:42 Starting compiler/encoders/arm8/proofs
Feb 21 15:53:56 Finished compiler/encoders/arm8/proofs                         6m12s   1GB
Feb 21 15:53:56 Starting compiler/encoders/mips/proofs
Feb 21 16:03:19 Finished compiler/encoders/mips/proofs                         9m22s   2GB
Feb 21 16:03:19 Starting compiler/encoders/riscv/proofs
Feb 21 16:11:43 Finished compiler/encoders/riscv/proofs                        8m23s   1GB
Feb 21 16:11:43 Starting compiler/encoders/ag32/proofs
Feb 21 16:14:06 Finished compiler/encoders/ag32/proofs                         2m22s 761MB
Feb 21 16:14:06 Starting compiler/backend/x64/proofs
Feb 21 16:14:24 Finished compiler/backend/x64/proofs                             18s 863MB
Feb 21 16:14:25 Starting compiler/backend/arm7/proofs
Feb 21 16:14:45 Finished compiler/backend/arm7/proofs                            20s   1GB
Feb 21 16:14:45 Starting compiler/backend/arm8/proofs
Feb 21 16:15:04 Finished compiler/backend/arm8/proofs                            18s   1GB
Feb 21 16:15:04 Starting compiler/backend/mips/proofs
Feb 21 16:15:24 Finished compiler/backend/mips/proofs                            19s   1GB
Feb 21 16:15:24 Starting compiler/backend/riscv/proofs
Feb 21 16:15:44 Finished compiler/backend/riscv/proofs                           19s   1GB
Feb 21 16:15:44 Starting compiler/backend/ag32/proofs
Feb 21 16:28:05 Finished compiler/backend/ag32/proofs                         12m20s   2GB
Feb 21 16:28:05 Starting compiler/proofs
Feb 21 16:29:45 Finished compiler/proofs                                       1m39s   3GB
Feb 21 16:29:45 Starting candle/set-theory
Feb 21 16:30:12 Finished candle/set-theory                                       26s 873MB
Feb 21 16:30:12 Starting candle/syntax-lib
Feb 21 16:30:22 Finished candle/syntax-lib                                        9s 643MB
Feb 21 16:30:22 Starting candle/standard/syntax
Feb 21 16:32:05 Finished candle/standard/syntax                                1m43s 935MB
Feb 21 16:32:05 Starting candle/standard/semantics
Feb 21 16:33:43 Finished candle/standard/semantics                             1m37s   1GB
Feb 21 16:33:44 Starting candle/standard/monadic
Feb 21 16:35:18 Finished candle/standard/monadic                               1m33s   1GB
Feb 21 16:35:18 Starting candle/standard/ml_kernel
Feb 21 16:40:19 Finished candle/standard/ml_kernel                             5m00s   3GB
Feb 21 16:40:19 Starting candle/standard/opentheory
Feb 21 16:49:00 Finished candle/standard/opentheory                            8m40s   4GB
Feb 21 16:49:00 Starting candle/standard/opentheory/compilation
Feb 21 17:20:42 Finished candle/standard/opentheory/compilation               31m39s  17GB
Feb 21 17:20:44 Starting candle/standard/opentheory/compilation/proofs
Feb 21 17:21:22 Finished candle/standard/opentheory/compilation/proofs           37s   3GB
Feb 21 17:21:22 Starting candle/overloading/syntax
Feb 21 17:24:15 Finished candle/overloading/syntax                             2m53s   1GB
Feb 21 17:24:15 Starting candle/overloading/semantics
Feb 21 17:30:52 Finished candle/overloading/semantics                          6m37s   3GB
Feb 21 17:30:53 Starting characteristic/examples
Feb 21 17:32:04 Finished characteristic/examples                               1m11s   3GB
Feb 21 17:32:04 Starting tutorial/solutions
Feb 21 17:46:15 Finished tutorial/solutions                                   14m10s   6GB
Feb 21 17:46:15 Starting translator/monadic/examples
Feb 21 17:49:13 Finished translator/monadic/examples                           2m58s   2GB
Feb 21 17:49:13 Starting examples
Feb 21 17:57:17 Finished examples                                              8m03s   3GB
Feb 21 17:57:17 Starting examples/compilation/x64
Feb 21 20:09:06 Finished examples/compilation/x64                           2h11m48s  14GB
Feb 21 20:09:06 Starting examples/compilation/x64/proofs
Feb 21 20:10:41 Finished examples/compilation/x64/proofs                       1m34s   2GB
Feb 21 20:10:41 Starting examples/compilation/ag32
Feb 21 20:40:08 Finished examples/compilation/ag32                            29m26s   6GB
Feb 21 20:40:08 Starting examples/compilation/ag32/proofs
Feb 21 20:40:48 Finished examples/compilation/ag32/proofs                        40s   2GB
Feb 21 20:40:49 Starting examples/cost
Feb 21 21:21:12 Finished examples/cost                                        40m23s   7GB
Feb 21 21:21:12 Starting examples/lpr_checker
Feb 21 21:24:39 Finished examples/lpr_checker                                  3m26s   2GB
Feb 21 21:24:39 Starting examples/lpr_checker/compilation
Feb 21 21:41:42 Finished examples/lpr_checker/compilation                     17m03s   8GB
Feb 21 21:41:42 Starting examples/lpr_checker/compilation/proofs
Feb 21 21:42:17 Finished examples/lpr_checker/compilation/proofs                 34s   2GB
Feb 21 21:42:17 Starting examples/lpr_checker/array
Feb 21 21:49:48 Finished examples/lpr_checker/array                            7m30s   3GB
Feb 21 21:49:48 Starting examples/lpr_checker/array/compilation
Feb 21 22:05:29 Finished examples/lpr_checker/array/compilation               15m41s   9GB
Feb 21 22:05:29 Starting examples/lpr_checker/array/compilation/proofs
Feb 21 22:06:07 Finished examples/lpr_checker/array/compilation/proofs           37s   3GB
Feb 21 22:06:07 Starting translator/okasaki-examples
Feb 21 22:10:20 Finished translator/okasaki-examples                           4m12s   1GB
Feb 21 22:10:20 Starting translator/other-examples
Feb 21 22:12:10 Finished translator/other-examples                             1m49s   1GB
Feb 21 22:12:10 Starting compiler/parsing/tests
Feb 21 22:12:35 Finished compiler/parsing/tests                                  24s 647MB
Feb 21 22:12:35 Starting compiler/inference/tests
Feb 21 22:17:00 Finished compiler/inference/tests                              4m24s   4GB
Feb 21 22:17:00 Starting compiler/bootstrap/translation
Feb 22 00:45:13 Finished compiler/bootstrap/translation                     2h28m12s  43GB
Feb 22 00:45:13 Starting unverified/sexpr-bootstrap/x64/64
Feb 22 00:59:55 Finished unverified/sexpr-bootstrap/x64/64                    14m41s   5GB
Feb 22 00:59:55 Starting unverified/sexpr-bootstrap/x64/32
Feb 22 01:10:33 Finished unverified/sexpr-bootstrap/x64/32                    10m37s   8GB
Feb 22 01:10:33 Starting compiler/benchmarks
Feb 22 01:47:23 Finished compiler/benchmarks                                  36m48s   2GB
Feb 22 01:47:24 Starting compiler/bootstrap/compilation/x64/64
Feb 22 16:24:34 Finished compiler/bootstrap/compilation/x64/64             14h37m09s  64GB
Feb 22 16:24:34 Starting compiler/bootstrap/compilation/x64/64/proofs
Feb 22 16:27:52 Finished compiler/bootstrap/compilation/x64/64/proofs          3m17s  13GB
Feb 22 16:27:52 Starting compiler/bootstrap/compilation/x64/32
Feb 23 05:56:08 Finished compiler/bootstrap/compilation/x64/32             13h28m15s  64GB
Feb 23 05:56:08 Starting compiler/bootstrap/compilation/x64/32/proofs
Feb 23 05:59:09 Finished compiler/bootstrap/compilation/x64/32/proofs          3m00s  12GB
Feb 23 05:59:09 Starting compiler/bootstrap/compilation/ag32/32
Feb 23 20:58:24 Finished compiler/bootstrap/compilation/ag32/32            14h59m14s  64GB
Feb 23 20:58:24 Starting compiler/bootstrap/compilation/ag32/32/proofs
Feb 23 21:22:21 Finished compiler/bootstrap/compilation/ag32/32/proofs        23m56s  29GB
Feb 23 21:22:21 SUCCESS