Job 2296

CakeML:42f4bd7d5dadb18b5e2aff3acfde2eba990f96d6
  fix broken proof [Feb 10 12:50:54]
#980 (xlrup)
Merging into:b76383b2a589101f171319130980075afdc90158
  Fix data_to_word_assignProof given integer$Num rewrites changes [Jan 30 06:21:36]
HOL:c5f2bc287fa6507cfb3372b4b827105b9633636b
  Other cheatsheet additions: `iff_tac`/`eq_tac` and `ExclSF` [Feb 08 23:51:55]
Machine:stove 5.15.0-86-generic x86_64 GNU/Linux

Feb 11 15:27:02 Claimed job
Feb 11 15:27:04 Reusing HOL
Feb 11 15:27:55 Starting developers
Feb 11 15:28:01 Finished developers                                               5s 106MB
Feb 11 15:28:01 Starting developers/bin
Feb 11 15:28:07 Finished developers/bin                                           6s   1GB
Feb 11 15:28:07 Starting compiler/proofs
Feb 12 15:45:38 Resuming compiler/proofs
Feb 12 15:48:34 Finished compiler/proofs                                       2m56s   6GB
Feb 12 15:48:34 Starting compiler/bootstrap/translation
Feb 12 23:59:13 Finished compiler/bootstrap/translation                     8h10m38s  46GB
Feb 12 23:59:13 Starting semantics/ffi
Feb 12 23:59:18 Finished semantics/ffi                                            4s 384MB
Feb 12 23:59:18 Starting semantics
Feb 12 23:59:19 Finished semantics                                                1s  18MB
Feb 12 23:59:20 Starting semantics/proofs
Feb 12 23:59:53 Finished semantics/proofs                                        32s 730MB
Feb 12 23:59:53 Starting semantics/alt_semantics
Feb 13 00:00:25 Finished semantics/alt_semantics                                 32s 885MB
Feb 13 00:00:25 Starting semantics/alt_semantics/proofs
Feb 13 00:12:25 Finished semantics/alt_semantics/proofs                       11m59s   1GB
Feb 13 00:12:25 Starting basis/pure
Feb 13 00:12:26 Finished basis/pure                                               1s  19MB
Feb 13 00:12:26 Starting translator
Feb 13 00:14:15 Finished translator                                            1m48s   2GB
Feb 13 00:14:15 Starting compiler/parsing
Feb 13 00:14:17 Finished compiler/parsing                                         1s  21MB
Feb 13 00:14:17 Starting characteristic
Feb 13 00:14:19 Finished characteristic                                           1s  25MB
Feb 13 00:14:19 Starting translator/monadic
Feb 13 00:14:21 Finished translator/monadic                                       1s  20MB
Feb 13 00:14:21 Starting basis
Feb 13 00:18:05 Finished basis                                                 3m43s   3GB
Feb 13 00:18:05 Starting compiler/inference
Feb 13 00:18:07 Finished compiler/inference                                       1s  21MB
Feb 13 00:18:07 Starting compiler/backend/reg_alloc
Feb 13 00:18:08 Finished compiler/backend/reg_alloc                               1s  23MB
Feb 13 00:18:08 Starting compiler/backend/gc
Feb 13 00:18:11 Finished compiler/backend/gc                                      2s  25MB
Feb 13 00:18:11 Starting compiler/backend
Feb 13 00:18:24 Finished compiler/backend                                        12s 855MB
Feb 13 00:18:24 Starting compiler/encoders/asm
Feb 13 00:18:26 Finished compiler/encoders/asm                                    1s  20MB
Feb 13 00:18:26 Starting compiler/encoders/x64
Feb 13 00:18:28 Finished compiler/encoders/x64                                    1s  24MB
Feb 13 00:18:28 Starting compiler/encoders/arm7
Feb 13 00:18:29 Finished compiler/encoders/arm7                                   1s  21MB
Feb 13 00:18:30 Starting compiler/encoders/arm8
Feb 13 00:18:31 Finished compiler/encoders/arm8                                   1s  25MB
Feb 13 00:18:31 Starting compiler/encoders/arm8_asl
Feb 13 02:44:03 Finished compiler/encoders/arm8_asl                         2h25m31s  40GB
Feb 13 02:44:03 Starting compiler/encoders/mips
Feb 13 02:44:05 Finished compiler/encoders/mips                                   1s  26MB
Feb 13 02:44:05 Starting compiler/encoders/riscv
Feb 13 02:44:07 Finished compiler/encoders/riscv                                  1s  18MB
Feb 13 02:44:07 Starting compiler/encoders/ag32
Feb 13 02:44:09 Finished compiler/encoders/ag32                                   1s  18MB
Feb 13 02:44:09 Starting compiler/backend/x64
Feb 13 02:44:11 Finished compiler/backend/x64                                     2s  22MB
Feb 13 02:44:12 Starting compiler/backend/arm7
Feb 13 02:44:14 Finished compiler/backend/arm7                                    2s  25MB
Feb 13 02:44:14 Starting compiler/backend/arm8
Feb 13 02:44:16 Finished compiler/backend/arm8                                    2s  29MB
Feb 13 02:44:16 Starting compiler/backend/mips
Feb 13 02:44:19 Finished compiler/backend/mips                                    2s  28MB
Feb 13 02:44:19 Starting compiler/backend/riscv
Feb 13 02:44:21 Finished compiler/backend/riscv                                   2s  22MB
Feb 13 02:44:21 Starting compiler/backend/ag32
Feb 13 02:45:46 Finished compiler/backend/ag32                                 1m24s   1GB
Feb 13 02:45:46 Starting compiler/parsing/proofs
Feb 13 02:45:48 Finished compiler/parsing/proofs                                  1s  19MB
Feb 13 02:45:48 Starting compiler/inference/proofs
Feb 13 02:45:50 Finished compiler/inference/proofs                                1s  24MB
Feb 13 02:45:50 Starting compiler/backend/semantics
Feb 13 02:47:04 Finished compiler/backend/semantics                            1m13s   1GB
Feb 13 02:47:04 Starting compiler/backend/reg_alloc/proofs
Feb 13 02:47:06 Finished compiler/backend/reg_alloc/proofs                        1s  20MB
Feb 13 02:47:06 Starting compiler/backend/proofs
Feb 13 02:48:06 Finished compiler/backend/proofs                               1m00s   2GB
Feb 13 02:48:06 Starting compiler/backend/serialiser
Feb 13 02:48:09 Finished compiler/backend/serialiser                              2s  40MB
Feb 13 02:48:09 Starting compiler/encoders/x64/proofs
Feb 13 02:58:03 Finished compiler/encoders/x64/proofs                          9m53s   6GB
Feb 13 02:58:03 Starting compiler/encoders/arm7/proofs
Feb 13 03:11:52 Finished compiler/encoders/arm7/proofs                        13m48s   3GB
Feb 13 03:11:52 Starting compiler/encoders/arm8/proofs
Feb 13 03:18:54 Finished compiler/encoders/arm8/proofs                         7m01s   1GB
Feb 13 03:18:54 Starting compiler/encoders/arm8_asl/proofs
Feb 13 04:11:38 Finished compiler/encoders/arm8_asl/proofs                    52m43s   9GB
Feb 13 04:11:38 Starting compiler/encoders/mips/proofs
Feb 13 04:22:21 Finished compiler/encoders/mips/proofs                        10m42s   2GB
Feb 13 04:22:21 Starting compiler/encoders/riscv/proofs
Feb 13 04:31:24 Finished compiler/encoders/riscv/proofs                        9m03s   1GB
Feb 13 04:31:24 Starting compiler/encoders/ag32/proofs
Feb 13 04:33:56 Finished compiler/encoders/ag32/proofs                         2m31s   1GB
Feb 13 04:33:56 Starting compiler/backend/x64/proofs
Feb 13 04:34:25 Finished compiler/backend/x64/proofs                             29s   1GB
Feb 13 04:34:25 Starting compiler/backend/arm7/proofs
Feb 13 04:34:58 Finished compiler/backend/arm7/proofs                            32s   2GB
Feb 13 04:34:58 Starting compiler/backend/arm8/proofs
Feb 13 04:35:28 Finished compiler/backend/arm8/proofs                            30s   1GB
Feb 13 04:35:28 Starting compiler/backend/arm8_asl
Feb 13 04:35:53 Finished compiler/backend/arm8_asl                               24s   1GB
Feb 13 04:35:53 Starting compiler/backend/mips/proofs
Feb 13 04:36:28 Finished compiler/backend/mips/proofs                            34s   2GB
Feb 13 04:36:28 Starting compiler/backend/riscv/proofs
Feb 13 04:37:02 Finished compiler/backend/riscv/proofs                           33s   2GB
Feb 13 04:37:02 Starting compiler/backend/ag32/proofs
Feb 13 04:51:07 Finished compiler/backend/ag32/proofs                         14m04s   3GB
Feb 13 04:51:07 Starting candle/set-theory
Feb 13 04:51:47 Finished candle/set-theory                                       39s   1GB
Feb 13 04:51:47 Starting candle/syntax-lib
Feb 13 04:51:49 Finished candle/syntax-lib                                        1s  20MB
Feb 13 04:51:49 Starting candle/standard/syntax
Feb 13 04:51:59 Finished candle/standard/syntax                                  10s 725MB
Feb 13 04:51:59 Starting candle/standard/semantics
Feb 13 04:53:59 Finished candle/standard/semantics                             1m59s   1GB
Feb 13 04:53:59 Starting candle/standard/monadic
Feb 13 04:54:01 Finished candle/standard/monadic                                  1s  28MB
Feb 13 04:54:01 Starting candle/standard/ml_kernel
Feb 13 04:55:41 Finished candle/standard/ml_kernel                             1m39s   3GB
Feb 13 04:55:41 Starting candle/overloading/syntax
Feb 13 04:59:06 Finished candle/overloading/syntax                             3m25s   1GB
Feb 13 04:59:06 Starting candle/overloading/semantics
Feb 13 05:11:21 Finished candle/overloading/semantics                         12m15s   2GB
Feb 13 05:11:21 Starting candle/overloading/monadic
Feb 13 05:14:06 Finished candle/overloading/monadic                            2m43s   1GB
Feb 13 05:14:06 Starting candle/overloading/ml_kernel
Feb 13 05:22:01 Finished candle/overloading/ml_kernel                          7m55s   3GB
Feb 13 05:22:01 Starting candle/overloading/ml_checker
Feb 13 05:24:38 Finished candle/overloading/ml_checker                         2m36s   2GB
Feb 13 05:24:38 Starting candle/prover
Feb 13 05:34:48 Finished candle/prover                                        10m09s   3GB
Feb 13 05:34:48 Starting pancake
Feb 13 05:35:34 Finished pancake                                                 46s 926MB
Feb 13 05:35:34 Starting pancake/ffi
Feb 13 05:35:35 Finished pancake/ffi                                              0s  13MB
Feb 13 05:35:35 Starting pancake/semantics
Feb 13 05:38:07 Finished pancake/semantics                                     2m31s   1GB
Feb 13 05:38:07 Starting pancake/parser
Feb 13 05:38:29 Finished pancake/parser                                          22s 968MB
Feb 13 05:38:29 Starting pancake/proofs
Feb 13 06:11:50 Finished pancake/proofs                                       33m20s   6GB
Feb 13 06:11:50 Starting characteristic/examples
Feb 13 06:13:39 Finished characteristic/examples                               1m48s   2GB
Feb 13 06:13:39 Starting tutorial/solutions
Feb 13 06:28:57 Finished tutorial/solutions                                   15m17s   9GB
Feb 13 06:28:57 Starting translator/monadic/examples
Feb 13 06:33:05 Finished translator/monadic/examples                           4m07s   4GB
Feb 13 06:33:05 Starting examples
Feb 13 06:49:31 Finished examples                                             16m26s   4GB
Feb 13 06:49:31 Starting examples/compilation/x64
Feb 13 08:49:20 Finished examples/compilation/x64                           1h59m48s  18GB
Feb 13 08:49:20 Starting examples/compilation/x64/proofs
Feb 13 08:51:59 Finished examples/compilation/x64/proofs                       2m38s   4GB
Feb 13 08:51:59 Starting examples/compilation/ag32
Feb 13 09:22:04 Finished examples/compilation/ag32                            30m04s   9GB
Feb 13 09:22:04 Starting examples/compilation/ag32/proofs
Feb 13 09:23:12 Finished examples/compilation/ag32/proofs                      1m07s   5GB
Feb 13 09:23:12 Starting examples/compilation/to_word
Feb 13 09:26:33 Finished examples/compilation/to_word                          3m21s   7GB
Feb 13 09:26:33 Starting examples/lpr_checker
Feb 13 09:27:39 Finished examples/lpr_checker                                  1m06s   1GB
Feb 13 09:27:39 Starting examples/lpr_checker/array
Feb 13 09:59:07 Finished examples/lpr_checker/array                           31m27s   5GB
Feb 13 09:59:07 Starting examples/lpr_checker/array/compilation
Feb 13 10:50:01 Finished examples/lpr_checker/array/compilation               50m53s  20GB
Feb 13 10:50:01 Starting examples/lpr_checker/array/compilation/proofs
Feb 13 10:52:02 Finished examples/lpr_checker/array/compilation/proofs         2m01s   3GB
Feb 13 10:52:02 Starting examples/lpr_checker/array/compilation/proofsARM8
Feb 13 10:57:50 Finished examples/lpr_checker/array/compilation/proofsARM8     5m47s  22GB
Feb 13 10:57:50 Starting examples/xlrup_checker
Feb 13 10:58:49 Finished examples/xlrup_checker                                  59s   1GB
Feb 13 10:58:49 Starting examples/xlrup_checker/array
Feb 13 11:16:25 Finished examples/xlrup_checker/array                         17m35s   4GB
Feb 13 11:16:25 Starting examples/xlrup_checker/array/compilation
Feb 13 11:38:31 Finished examples/xlrup_checker/array/compilation             22m05s  15GB
Feb 13 11:38:31 Starting examples/xlrup_checker/array/compilation/proofs
Feb 13 11:39:38 Finished examples/xlrup_checker/array/compilation/proofs       1m06s   5GB
Feb 13 11:39:38 Starting examples/xlrup_checker/array/compilation/proofsARM8
Feb 13 11:39:38 SysErr ("No such file or directory", SOME ENOENT)
Feb 13 11:39:38 FAILED: examples/xlrup_checker/array/compilation/proofsARM8