Job 1864

CakeML:80dbdc408d661d56e349acf8aed8ea42fe20e2e2
  Add CF specs for Array.appi [Apr 12 09:06:24]
#878 (array-appi-fix)
Merging into:37af395434ed1290ae673bd6e3b3e07f8b5c03c4
  Fix some broken pancake proofs [Apr 18 10:13:33]
HOL:3b1931c130fcab243da332adb2c1413c42c59cf9
  Escape # in TeX output [Apr 12 23:45:24]
Machine:oven3

Apr 18 10:20:33 Claimed job
Apr 18 10:20:35 Reusing HOL
Apr 18 10:21:28 Starting developers
Apr 18 10:21:36 Finished developers                                               8s 162MB
Apr 18 10:21:37 Starting developers/bin
Apr 18 10:22:00 Finished developers/bin                                          23s   1GB
Apr 18 10:22:00 Starting semantics/ffi
Apr 18 10:22:25 Finished semantics/ffi                                           24s 259MB
Apr 18 10:22:26 Starting semantics
Apr 18 10:26:23 Finished semantics                                             3m56s   1GB
Apr 18 10:26:23 Starting semantics/proofs
Apr 18 10:35:51 Finished semantics/proofs                                      9m28s   4GB
Apr 18 10:35:52 Starting semantics/alt_semantics
Apr 18 10:36:40 Finished semantics/alt_semantics                                 48s 487MB
Apr 18 10:36:40 Starting semantics/alt_semantics/proofs
Apr 18 10:43:11 Finished semantics/alt_semantics/proofs                        6m31s   1GB
Apr 18 10:43:12 Starting basis/pure
Apr 18 10:45:25 Finished basis/pure                                            2m13s   1GB
Apr 18 10:45:25 Starting translator
Apr 18 10:51:38 Finished translator                                            6m12s   1GB
Apr 18 10:51:38 Starting compiler/parsing
Apr 18 10:54:21 Finished compiler/parsing                                      2m42s   2GB
Apr 18 10:54:21 Starting characteristic
Apr 18 11:07:51 Finished characteristic                                       13m30s   2GB
Apr 18 11:07:52 Starting translator/monadic
Apr 18 11:11:58 Finished translator/monadic                                    4m06s   1GB
Apr 18 11:11:58 Starting basis
Apr 18 12:54:41 Finished basis                                              1h42m42s  10GB
Apr 18 12:54:41 Starting compiler/inference
Apr 18 12:57:32 Finished compiler/inference                                    2m50s   1GB
Apr 18 12:57:32 Starting compiler/backend/reg_alloc
Apr 18 13:00:46 Finished compiler/backend/reg_alloc                            3m14s   1GB
Apr 18 13:00:47 Starting compiler/backend/gc
Apr 18 13:09:17 Finished compiler/backend/gc                                   8m29s   2GB
Apr 18 13:09:17 Starting compiler/backend
Apr 18 13:20:02 Finished compiler/backend                                     10m45s   2GB
Apr 18 13:20:02 Starting compiler/encoders/asm
Apr 18 13:21:08 Finished compiler/encoders/asm                                 1m05s   1GB
Apr 18 13:21:09 Starting compiler/encoders/x64
Apr 18 13:22:13 Finished compiler/encoders/x64                                 1m04s 996MB
Apr 18 13:22:14 Starting compiler/encoders/arm7
Apr 18 13:24:19 Finished compiler/encoders/arm7                                2m05s 821MB
Apr 18 13:24:19 Starting compiler/encoders/arm8
Apr 18 13:24:55 Finished compiler/encoders/arm8                                  35s 677MB
Apr 18 13:24:55 Starting compiler/encoders/arm8_asl
Apr 18 13:32:00 Finished compiler/encoders/arm8_asl                            7m04s   1GB
Apr 18 13:32:00 Starting compiler/encoders/mips
Apr 18 13:32:45 Finished compiler/encoders/mips                                  44s   1GB
Apr 18 13:32:45 Starting compiler/encoders/riscv
Apr 18 13:33:27 Finished compiler/encoders/riscv                                 41s 858MB
Apr 18 13:33:27 Starting compiler/encoders/ag32
Apr 18 13:34:15 Finished compiler/encoders/ag32                                  47s 784MB
Apr 18 13:34:15 Starting compiler/backend/x64
Apr 18 13:35:01 Finished compiler/backend/x64                                    46s   1GB
Apr 18 13:35:02 Starting compiler/backend/arm7
Apr 18 13:35:54 Finished compiler/backend/arm7                                   52s   1GB
Apr 18 13:35:54 Starting compiler/backend/arm8
Apr 18 13:36:44 Finished compiler/backend/arm8                                   49s   1GB
Apr 18 13:36:44 Starting compiler/backend/mips
Apr 18 13:37:33 Finished compiler/backend/mips                                   48s   1GB
Apr 18 13:37:33 Starting compiler/backend/riscv
Apr 18 13:38:22 Finished compiler/backend/riscv                                  48s   1GB
Apr 18 13:38:22 Starting compiler/backend/ag32
Apr 18 13:41:23 Finished compiler/backend/ag32                                 3m00s   1GB
Apr 18 13:41:23 Starting compiler/parsing/proofs
Apr 18 13:50:00 Finished compiler/parsing/proofs                               8m36s   1GB
Apr 18 13:50:00 Starting compiler/inference/proofs
Apr 18 13:55:40 Finished compiler/inference/proofs                             5m38s   1GB
Apr 18 13:55:40 Starting compiler/backend/semantics
Apr 18 14:58:47 Finished compiler/backend/semantics                         1h03m06s   1GB
Apr 18 14:58:47 Starting compiler/backend/reg_alloc/proofs
Apr 18 15:06:31 Finished compiler/backend/reg_alloc/proofs                     7m43s   1GB
Apr 18 15:06:32 Starting compiler/backend/proofs
Apr 18 16:48:08 Finished compiler/backend/proofs                            1h41m36s  19GB
Apr 18 16:48:08 Starting compiler/backend/serialiser
Apr 18 16:51:34 Finished compiler/backend/serialiser                           3m25s   2GB
Apr 18 16:51:34 Starting compiler/encoders/x64/proofs
Apr 18 17:12:53 Finished compiler/encoders/x64/proofs                         21m18s   5GB
Apr 18 17:12:53 Starting compiler/encoders/arm7/proofs
Apr 18 17:42:45 Finished compiler/encoders/arm7/proofs                        29m52s   3GB
Apr 18 17:42:46 Starting compiler/encoders/arm8/proofs
Apr 18 17:58:33 Finished compiler/encoders/arm8/proofs                        15m47s   1GB
Apr 18 17:58:34 Starting compiler/encoders/arm8_asl/proofs
Apr 18 18:33:21 Finished compiler/encoders/arm8_asl/proofs                    34m47s   1GB
Apr 18 18:33:21 Starting compiler/encoders/mips/proofs
Apr 18 18:56:10 Finished compiler/encoders/mips/proofs                        22m47s   2GB
Apr 18 18:56:10 Starting compiler/encoders/riscv/proofs
Apr 18 19:16:17 Finished compiler/encoders/riscv/proofs                       20m06s   1GB
Apr 18 19:16:17 Starting compiler/encoders/ag32/proofs
Apr 18 19:22:04 Finished compiler/encoders/ag32/proofs                         5m46s 864MB
Apr 18 19:22:04 Starting compiler/backend/x64/proofs
Apr 18 19:23:06 Finished compiler/backend/x64/proofs                           1m01s   1GB
Apr 18 19:23:06 Starting compiler/backend/arm7/proofs
Apr 18 19:24:08 Finished compiler/backend/arm7/proofs                          1m01s   1GB
Apr 18 19:24:08 Starting compiler/backend/arm8/proofs
Apr 18 19:25:12 Finished compiler/backend/arm8/proofs                          1m03s   1GB
Apr 18 19:25:12 Starting compiler/backend/arm8_asl
Apr 18 19:26:03 Finished compiler/backend/arm8_asl                               50s   1GB
Apr 18 19:26:03 Starting compiler/backend/mips/proofs
Apr 18 19:27:05 Finished compiler/backend/mips/proofs                          1m02s   1GB
Apr 18 19:27:06 Starting compiler/backend/riscv/proofs
Apr 18 19:28:08 Finished compiler/backend/riscv/proofs                         1m02s   1GB
Apr 18 19:28:09 Starting compiler/backend/ag32/proofs
Apr 18 19:56:14 Finished compiler/backend/ag32/proofs                         28m05s   3GB
Apr 18 19:56:14 Starting compiler/proofs
Apr 18 20:00:45 Finished compiler/proofs                                       4m30s   3GB
Apr 18 20:00:45 Starting candle/set-theory
Apr 18 20:01:58 Finished candle/set-theory                                     1m12s 994MB
Apr 18 20:01:58 Starting candle/syntax-lib
Apr 18 20:02:28 Finished candle/syntax-lib                                       29s 629MB
Apr 18 20:02:28 Starting candle/standard/syntax
Apr 18 20:06:53 Finished candle/standard/syntax                                4m24s   1GB
Apr 18 20:06:53 Starting candle/standard/semantics
Apr 18 20:11:03 Finished candle/standard/semantics                             4m09s   1GB
Apr 18 20:11:03 Starting candle/standard/monadic
Apr 18 20:15:05 Finished candle/standard/monadic                               4m01s   1GB
Apr 18 20:15:05 Starting candle/standard/ml_kernel
Apr 18 20:28:11 Finished candle/standard/ml_kernel                            13m05s   3GB
Apr 18 20:28:11 Starting candle/overloading/syntax
Apr 18 20:35:12 Finished candle/overloading/syntax                             7m00s   1GB
Apr 18 20:35:13 Starting candle/overloading/semantics
Apr 18 21:01:19 Finished candle/overloading/semantics                         26m06s   2GB
Apr 18 21:01:20 Starting candle/overloading/monadic
Apr 18 21:06:47 Finished candle/overloading/monadic                            5m26s   1GB
Apr 18 21:06:47 Starting candle/overloading/ml_kernel
Apr 18 21:21:49 Finished candle/overloading/ml_kernel                         15m01s   4GB
Apr 18 21:21:49 Starting candle/overloading/ml_checker
Apr 18 21:27:09 Finished candle/overloading/ml_checker                         5m20s   3GB
Apr 18 21:27:09 Starting candle/prover
Apr 18 21:45:22 Finished candle/prover                                        18m11s   3GB
Apr 18 21:45:22 Starting pancake
Apr 18 21:53:10 Finished pancake                                               7m47s   4GB
Apr 18 21:53:10 Starting pancake/ffi
Apr 18 21:53:11 Finished pancake/ffi                                              0s  30MB
Apr 18 21:53:11 Starting pancake/semantics
Apr 18 21:58:32 Finished pancake/semantics                                     5m21s 971MB
Apr 18 21:58:32 Starting pancake/proofs
Apr 18 22:24:39 Finished pancake/proofs                                       26m05s   6GB
Apr 18 22:24:39 Starting characteristic/examples
Apr 18 22:27:31 Finished characteristic/examples                               2m51s   3GB
Apr 18 22:27:31 Starting tutorial/solutions
Apr 18 23:04:32 Finished tutorial/solutions                                   37m00s   9GB
Apr 18 23:04:32 Starting translator/monadic/examples
Apr 18 23:11:29 Finished translator/monadic/examples                           6m56s   2GB
Apr 18 23:11:29 Starting examples
Apr 18 23:30:44 Finished examples                                             19m14s   3GB
Apr 18 23:30:44 Starting examples/compilation/x64
Apr 19 05:09:38 Finished examples/compilation/x64                           5h38m52s  26GB
Apr 19 05:09:38 Starting examples/compilation/x64/proofs
Apr 19 05:14:22 Finished examples/compilation/x64/proofs                       4m43s   3GB
Apr 19 05:14:22 Starting examples/compilation/ag32
Apr 19 06:33:13 Finished examples/compilation/ag32                          1h18m51s   9GB
Apr 19 06:33:14 Starting examples/compilation/ag32/proofs
Apr 19 06:35:06 Finished examples/compilation/ag32/proofs                      1m52s   2GB
Apr 19 06:35:06 Starting examples/cost
Apr 19 08:33:52 Finished examples/cost                                      1h58m44s   9GB
Apr 19 08:33:52 Starting examples/lpr_checker
Apr 19 08:36:03 Finished examples/lpr_checker                                  2m10s 871MB
Apr 19 08:36:03 Starting examples/lpr_checker/array
Apr 19 09:39:28 Finished examples/lpr_checker/array                         1h03m25s  10GB
Apr 19 09:39:29 Starting examples/lpr_checker/array/compilation
Apr 19 12:43:41 Finished examples/lpr_checker/array/compilation             3h04m12s  37GB
Apr 19 12:43:41 Starting examples/lpr_checker/array/compilation/proofs
Apr 19 12:46:34 Finished examples/lpr_checker/array/compilation/proofs         2m52s   6GB
Apr 19 12:46:34 Starting examples/opentheory
Apr 19 13:07:54 Finished examples/opentheory                                  21m19s   6GB
Apr 19 13:07:54 Starting examples/opentheory
Apr 19 13:07:58 Finished examples/opentheory                                      2s  33MB
Apr 19 13:07:58 Starting examples/opentheory/compilation
Apr 19 14:41:42 Finished examples/opentheory/compilation                    1h33m43s  35GB
Apr 19 14:41:42 Starting examples/opentheory/compilation/proofs
Apr 19 14:43:58 Finished examples/opentheory/compilation/proofs                2m15s   3GB
Apr 19 14:43:58 Starting examples/opentheory/compilation/ag32
Apr 19 16:14:55 Finished examples/opentheory/compilation/ag32               1h30m57s  39GB
Apr 19 16:14:56 Starting examples/opentheory/compilation/ag32/proofs
Apr 19 16:18:44 Finished examples/opentheory/compilation/ag32/proofs           3m47s   5GB
Apr 19 16:18:44 Starting examples/sat_encodings
Apr 19 16:23:04 Finished examples/sat_encodings                                4m20s 859MB
Apr 19 16:23:05 Starting examples/sat_encodings/case_studies
Apr 19 16:27:00 Finished examples/sat_encodings/case_studies                   3m54s 935MB
Apr 19 16:27:00 Starting examples/sat_encodings/translation
Apr 19 16:39:07 Finished examples/sat_encodings/translation                   12m06s   4GB
Apr 19 16:39:07 Starting examples/sat_encodings/translation/compilation
Apr 19 18:08:23 Finished examples/sat_encodings/translation/compilation     1h29m15s  20GB
Apr 19 18:08:23 Starting translator/okasaki-examples
Apr 19 18:18:09 Finished translator/okasaki-examples                           9m45s   1GB
Apr 19 18:18:09 Starting translator/other-examples
Apr 19 18:22:02 Finished translator/other-examples                             3m52s   1GB
Apr 19 18:22:03 Starting compiler/parsing/tests
Apr 19 18:23:09 Finished compiler/parsing/tests                                1m06s 545MB
Apr 19 18:23:10 Starting compiler/inference/tests
Apr 19 18:38:37 Finished compiler/inference/tests                             15m27s   5GB
Apr 19 18:38:37 Starting compiler/printing/test
Apr 19 18:46:08 Finished compiler/printing/test                                7m30s   3GB
Apr 19 18:46:09 Starting compiler/repl
Apr 19 19:11:07 Finished compiler/repl                                        24m58s   4GB
Apr 19 19:11:07 Starting compiler/bootstrap/translation
Apr 20 03:45:13 Finished compiler/bootstrap/translation                     8h34m04s  38GB
Apr 20 03:45:13 Starting unverified/sexpr-bootstrap/x64/64
Apr 20 04:07:09 Finished unverified/sexpr-bootstrap/x64/64                    21m56s  12GB
Apr 20 04:07:10 Starting unverified/sexpr-bootstrap/x64/32
Apr 20 04:25:46 Finished unverified/sexpr-bootstrap/x64/32                    18m36s  10GB
Apr 20 04:25:46 Starting compiler/benchmarks
Apr 20 04:25:52 Finished compiler/benchmarks                                      5s  53MB
Apr 20 04:25:52 Starting compiler/bootstrap/compilation/x64/64
Apr 21 19:44:25 Finished compiler/bootstrap/compilation/x64/64             39h18m32s 109GB
Apr 21 19:44:25 Starting compiler/bootstrap/compilation/x64/64/proofs
Apr 21 20:25:15 Finished compiler/bootstrap/compilation/x64/64/proofs         40m49s  52GB
Apr 21 20:25:15 Starting compiler/bootstrap/compilation/x64/32
Apr 23 01:52:01 Finished compiler/bootstrap/compilation/x64/32             29h26m44s 109GB
Apr 23 01:52:01 Starting compiler/bootstrap/compilation/x64/32/proofs
Apr 23 02:01:04 Finished compiler/bootstrap/compilation/x64/32/proofs          9m02s  15GB
Apr 23 02:01:04 Starting compiler/bootstrap/compilation/ag32/32
Apr 24 05:21:31 Finished compiler/bootstrap/compilation/ag32/32            27h20m26s 110GB
Apr 24 05:21:31 Starting compiler/bootstrap/compilation/ag32/32/proofs
Apr 24 05:46:13 Finished compiler/bootstrap/compilation/ag32/32/proofs        24m41s  51GB
Apr 24 05:46:13 SUCCESS