Job 1232

CakeML:556f8169b007ed57ddea81420886ceea99434afd
  Add concatAll to the signature of Word64Prog [May 19 09:57:09]
#737 (concatAll)
Merging into:e4c7de82bb84f991e4532da8a9cfe557930d1bb4
  Fix a few proof failures due to changes in HOL [May 18 20:17:13]
HOL:d0b4f135f9d0ca34127c775ce90771ace76482e8
  Fix a MULRELNORM instance: 2 * x = inv 2 * y should canonicalise [May 15 07:11:51]
Machine:oven3 4.19.67.1.amd64-smp

May 19 13:40:08 Claimed job
May 19 13:40:16 Building HOL
May 19 14:06:42 Starting developers
May 19 14:06:50 Finished developers                                               7s 144MB
May 19 14:06:50 Starting developers/bin
May 19 14:07:06 Finished developers/bin                                          15s   1GB
May 19 14:07:06 Starting semantics/ffi
May 19 14:07:29 Finished semantics/ffi                                           22s 260MB
May 19 14:07:29 Starting semantics
May 19 14:10:33 Finished semantics                                             3m03s   1GB
May 19 14:10:33 Starting semantics/proofs
May 19 14:18:16 Finished semantics/proofs                                      7m42s 903MB
May 19 14:18:16 Starting semantics/alt_semantics
May 19 14:18:35 Finished semantics/alt_semantics                                 18s 361MB
May 19 14:18:35 Starting semantics/alt_semantics/proofs
May 19 14:23:03 Finished semantics/alt_semantics/proofs                        4m28s 877MB
May 19 14:23:03 Starting basis/pure
May 19 14:29:05 Finished basis/pure                                            6m01s 846MB
May 19 14:29:05 Starting translator
May 19 14:34:30 Finished translator                                            5m24s   1GB
May 19 14:34:30 Starting compiler/parsing
May 19 14:37:00 Finished compiler/parsing                                      2m29s   2GB
May 19 14:37:00 Starting characteristic
May 19 14:49:29 Finished characteristic                                       12m27s   2GB
May 19 14:49:29 Starting translator/monadic
May 19 14:52:48 Finished translator/monadic                                    3m19s   1GB
May 19 14:52:49 Starting basis
May 19 15:58:58 Finished basis                                              1h06m08s  13GB
May 19 15:58:58 Starting compiler/inference
May 19 16:01:25 Finished compiler/inference                                    2m26s   1GB
May 19 16:01:25 Starting compiler/backend/reg_alloc
May 19 16:03:20 Finished compiler/backend/reg_alloc                            1m54s   1GB
May 19 16:03:20 Starting compiler/backend/gc
May 19 16:09:47 Finished compiler/backend/gc                                   6m26s   2GB
May 19 16:09:47 Starting compiler/backend
May 19 16:18:22 Finished compiler/backend                                      8m34s   2GB
May 19 16:18:22 Starting compiler/encoders/asm
May 19 16:19:08 Finished compiler/encoders/asm                                   45s 855MB
May 19 16:19:08 Starting compiler/encoders/x64
May 19 16:21:15 Finished compiler/encoders/x64                                 2m07s 933MB
May 19 16:21:16 Starting compiler/encoders/arm7
May 19 16:25:03 Finished compiler/encoders/arm7                                3m46s   1GB
May 19 16:25:03 Starting compiler/encoders/arm8
May 19 16:26:12 Finished compiler/encoders/arm8                                1m09s 596MB
May 19 16:26:13 Starting compiler/encoders/mips
May 19 16:28:41 Finished compiler/encoders/mips                                2m28s   1GB
May 19 16:28:41 Starting compiler/encoders/riscv
May 19 16:31:39 Finished compiler/encoders/riscv                               2m57s 865MB
May 19 16:31:39 Starting compiler/encoders/ag32
May 19 16:32:17 Finished compiler/encoders/ag32                                  37s 755MB
May 19 16:32:17 Starting compiler/backend/x64
May 19 16:32:58 Finished compiler/backend/x64                                    40s   1GB
May 19 16:32:58 Starting compiler/backend/arm7
May 19 16:33:40 Finished compiler/backend/arm7                                   41s   1GB
May 19 16:33:40 Starting compiler/backend/arm8
May 19 16:34:21 Finished compiler/backend/arm8                                   41s   1GB
May 19 16:34:22 Starting compiler/backend/mips
May 19 16:35:01 Finished compiler/backend/mips                                   38s   1GB
May 19 16:35:01 Starting compiler/backend/riscv
May 19 16:35:44 Finished compiler/backend/riscv                                  43s   1GB
May 19 16:35:45 Starting compiler/backend/ag32
May 19 16:38:07 Finished compiler/backend/ag32                                 2m22s   1GB
May 19 16:38:07 Starting compiler/parsing/proofs
May 19 16:50:22 Finished compiler/parsing/proofs                              12m14s   1GB
May 19 16:50:22 Starting compiler/inference/proofs
May 19 16:55:37 Finished compiler/inference/proofs                             5m15s   1GB
May 19 16:55:38 Starting compiler/backend/semantics
May 19 17:52:09 Finished compiler/backend/semantics                           56m31s   2GB
May 19 17:52:09 Starting compiler/backend/reg_alloc/proofs
May 19 17:59:41 Finished compiler/backend/reg_alloc/proofs                     7m30s   1GB
May 19 17:59:41 Starting compiler/backend/proofs
May 19 19:59:50 Finished compiler/backend/proofs                            2h00m08s  17GB
May 19 19:59:50 Starting compiler/encoders/x64/proofs
May 19 20:20:51 Finished compiler/encoders/x64/proofs                         21m00s   4GB
May 19 20:20:51 Starting compiler/encoders/arm7/proofs
May 19 20:48:39 Finished compiler/encoders/arm7/proofs                        27m47s   3GB
May 19 20:48:39 Starting compiler/encoders/arm8/proofs
May 19 21:03:15 Finished compiler/encoders/arm8/proofs                        14m35s   1GB
May 19 21:03:15 Starting compiler/encoders/mips/proofs
May 19 21:25:26 Finished compiler/encoders/mips/proofs                        22m10s   2GB
May 19 21:25:26 Starting compiler/encoders/riscv/proofs
May 19 21:45:01 Finished compiler/encoders/riscv/proofs                       19m34s   1GB
May 19 21:45:02 Starting compiler/encoders/ag32/proofs
May 19 21:50:34 Finished compiler/encoders/ag32/proofs                         5m32s 883MB
May 19 21:50:34 Starting compiler/backend/x64/proofs
May 19 21:51:18 Finished compiler/backend/x64/proofs                             43s   1GB
May 19 21:51:19 Starting compiler/backend/arm7/proofs
May 19 21:52:04 Finished compiler/backend/arm7/proofs                            45s   1GB
May 19 21:52:04 Starting compiler/backend/arm8/proofs
May 19 21:52:48 Finished compiler/backend/arm8/proofs                            43s   1GB
May 19 21:52:48 Starting compiler/backend/mips/proofs
May 19 21:53:33 Finished compiler/backend/mips/proofs                            44s   1GB
May 19 21:53:33 Starting compiler/backend/riscv/proofs
May 19 21:54:15 Finished compiler/backend/riscv/proofs                           41s   1GB
May 19 21:54:15 Starting compiler/backend/ag32/proofs
May 19 22:22:09 Finished compiler/backend/ag32/proofs                         27m53s   2GB
May 19 22:22:09 Starting compiler/proofs
May 19 22:25:47 Finished compiler/proofs                                       3m38s   3GB
May 19 22:25:47 Starting candle/set-theory
May 19 22:26:43 Finished candle/set-theory                                       55s   1GB
May 19 22:26:43 Starting candle/syntax-lib
May 19 22:27:06 Finished candle/syntax-lib                                       22s 654MB
May 19 22:27:06 Starting candle/standard/syntax
May 19 22:30:58 Finished candle/standard/syntax                                3m52s   1GB
May 19 22:30:58 Starting candle/standard/semantics
May 19 22:34:45 Finished candle/standard/semantics                             3m46s   1GB
May 19 22:34:45 Starting candle/standard/monadic
May 19 22:38:18 Finished candle/standard/monadic                               3m32s   1GB
May 19 22:38:18 Starting candle/standard/ml_kernel
May 19 22:49:17 Finished candle/standard/ml_kernel                            10m58s   5GB
May 19 22:49:17 Starting candle/standard/opentheory
May 19 23:08:42 Finished candle/standard/opentheory                           19m24s   3GB
May 19 23:08:43 Starting candle/standard/opentheory/compilation
May 20 00:11:15 Finished candle/standard/opentheory/compilation             1h02m31s  16GB
May 20 00:11:15 Starting candle/standard/opentheory/compilation/proofs
May 20 00:12:30 Finished candle/standard/opentheory/compilation/proofs         1m15s   3GB
May 20 00:12:31 Starting candle/overloading/syntax
May 20 00:18:59 Finished candle/overloading/syntax                             6m28s 979MB
May 20 00:19:00 Starting candle/overloading/semantics
May 20 00:33:56 Finished candle/overloading/semantics                         14m55s   3GB
May 20 00:33:56 Starting characteristic/examples
May 20 00:36:36 Finished characteristic/examples                               2m39s   2GB
May 20 00:36:36 Starting tutorial/solutions
May 20 01:07:37 Finished tutorial/solutions                                   31m00s   6GB
May 20 01:07:37 Starting translator/monadic/examples
May 20 01:12:42 Finished translator/monadic/examples                           5m04s   2GB
May 20 01:12:42 Starting examples
May 20 01:27:06 Finished examples                                             14m23s   2GB
May 20 01:27:06 Starting examples/compilation/x64
May 20 06:14:53 Finished examples/compilation/x64                           4h47m46s  14GB
May 20 06:14:53 Starting examples/compilation/x64/proofs
May 20 06:17:56 Finished examples/compilation/x64/proofs                       3m02s   2GB
May 20 06:17:56 Starting examples/compilation/ag32
May 20 07:25:28 Finished examples/compilation/ag32                          1h07m31s   5GB
May 20 07:25:28 Starting examples/compilation/ag32/proofs
May 20 07:26:50 Finished examples/compilation/ag32/proofs                      1m21s   2GB
May 20 07:26:50 Starting examples/cost
May 20 08:52:18 Finished examples/cost                                      1h25m26s   6GB
May 20 08:52:18 Starting examples/lpr_checker
May 20 09:00:06 Finished examples/lpr_checker                                  7m48s   4GB
May 20 09:00:06 Starting examples/lpr_checker/compilation
May 20 09:32:23 Finished examples/lpr_checker/compilation                     32m16s   7GB
May 20 09:32:24 Starting examples/lpr_checker/compilation/proofs
May 20 09:33:40 Finished examples/lpr_checker/compilation/proofs               1m16s   3GB
May 20 09:33:41 Starting examples/lpr_checker/array
May 20 09:55:03 Finished examples/lpr_checker/array                           21m21s   3GB
May 20 09:55:03 Starting examples/lpr_checker/array/compilation
May 20 10:32:58 Finished examples/lpr_checker/array/compilation               37m55s   8GB
May 20 10:32:59 Starting examples/lpr_checker/array/compilation/proofs
May 20 10:34:39 Finished examples/lpr_checker/array/compilation/proofs         1m40s   3GB
May 20 10:34:39 Starting translator/okasaki-examples
May 20 10:43:13 Finished translator/okasaki-examples                           8m33s   1GB
May 20 10:43:14 Starting translator/other-examples
May 20 10:46:47 Finished translator/other-examples                             3m33s   1GB
May 20 10:46:48 Starting compiler/parsing/tests
May 20 10:47:46 Finished compiler/parsing/tests                                  58s 728MB
May 20 10:47:46 Starting compiler/inference/tests
May 20 10:56:32 Finished compiler/inference/tests                              8m45s   5GB
May 20 10:56:32 Starting compiler/bootstrap/translation
May 20 16:25:28 Finished compiler/bootstrap/translation                     5h28m53s  77GB
May 20 16:25:28 Starting unverified/sexpr-bootstrap/x64/64
May 20 16:53:52 Finished unverified/sexpr-bootstrap/x64/64                    28m23s   4GB
May 20 16:53:52 Starting unverified/sexpr-bootstrap/x64/32
May 20 17:14:02 Finished unverified/sexpr-bootstrap/x64/32                    20m09s   7GB
May 20 17:14:02 Starting compiler/benchmarks
May 20 17:14:06 Finished compiler/benchmarks                                      3s  32MB
May 20 17:14:06 Starting compiler/bootstrap/compilation/x64/64 May 20 17:14:06 62162s