Job 2272

CakeML:e026a91d58aabda091e58bb8b4b8ca67b192f07c
  Fix mlvector given changes in HOL [Jan 17 02:43:46]
HOL:9f33a8dbd0595687aca5bd6997f9786be5cd346e
  Add some EVAL tests for mapi and toSortedAList [Jan 14 01:27:14]
Machine:stove 5.15.0-86-generic x86_64 GNU/Linux
Artefacts:cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz

Jan 17 09:38:29 Claimed job
Jan 17 09:38:36 Building HOL
Jan 17 09:53:27 Starting developers
Jan 17 09:53:32 Finished developers                                               5s 171MB
Jan 17 09:53:33 Starting developers/bin
Jan 17 09:53:39 Finished developers/bin                                           6s   1GB
Jan 17 09:53:39 Starting compiler/proofs
Jan 17 12:14:32 Finished compiler/proofs                                    2h20m53s  17GB
Jan 17 12:14:32 Starting compiler/bootstrap/translation
Jan 17 21:08:28 Finished compiler/bootstrap/translation                     8h53m55s  35GB
Jan 17 21:08:28 Starting semantics/ffi
Jan 17 21:08:34 Finished semantics/ffi                                            5s 213MB
Jan 17 21:08:34 Starting semantics
Jan 17 21:08:35 Finished semantics                                                1s  19MB
Jan 17 21:08:35 Starting semantics/proofs
Jan 17 21:09:09 Finished semantics/proofs                                        33s   1GB
Jan 17 21:09:09 Starting semantics/alt_semantics
Jan 17 21:09:41 Finished semantics/alt_semantics                                 31s 874MB
Jan 17 21:09:41 Starting semantics/alt_semantics/proofs
Jan 17 21:21:34 Finished semantics/alt_semantics/proofs                       11m52s   1GB
Jan 17 21:21:34 Starting basis/pure
Jan 17 21:21:36 Finished basis/pure                                               1s  17MB
Jan 17 21:21:36 Starting translator
Jan 17 21:23:25 Finished translator                                            1m48s   1GB
Jan 17 21:23:25 Starting compiler/parsing
Jan 17 21:23:26 Finished compiler/parsing                                         1s  20MB
Jan 17 21:23:27 Starting characteristic
Jan 17 21:23:29 Finished characteristic                                           1s  22MB
Jan 17 21:23:29 Starting translator/monadic
Jan 17 21:23:31 Finished translator/monadic                                       1s  20MB
Jan 17 21:23:31 Starting basis
Jan 17 21:27:14 Finished basis                                                 3m43s   3GB
Jan 17 21:27:14 Starting compiler/inference
Jan 17 21:27:16 Finished compiler/inference                                       1s  20MB
Jan 17 21:27:16 Starting compiler/backend/reg_alloc
Jan 17 21:27:18 Finished compiler/backend/reg_alloc                               1s  21MB
Jan 17 21:27:18 Starting compiler/backend/gc
Jan 17 21:27:20 Finished compiler/backend/gc                                      2s  27MB
Jan 17 21:27:20 Starting compiler/backend
Jan 17 21:27:33 Finished compiler/backend                                        12s 793MB
Jan 17 21:27:33 Starting compiler/encoders/asm
Jan 17 21:27:35 Finished compiler/encoders/asm                                    1s  22MB
Jan 17 21:27:35 Starting compiler/encoders/x64
Jan 17 21:27:37 Finished compiler/encoders/x64                                    1s  21MB
Jan 17 21:27:37 Starting compiler/encoders/arm7
Jan 17 21:27:38 Finished compiler/encoders/arm7                                   1s  25MB
Jan 17 21:27:39 Starting compiler/encoders/arm8
Jan 17 21:27:40 Finished compiler/encoders/arm8                                   1s  20MB
Jan 17 21:27:40 Starting compiler/encoders/arm8_asl
Jan 17 23:54:02 Finished compiler/encoders/arm8_asl                         2h26m20s  41GB
Jan 17 23:54:02 Starting compiler/encoders/mips
Jan 17 23:54:03 Finished compiler/encoders/mips                                   1s  23MB
Jan 17 23:54:04 Starting compiler/encoders/riscv
Jan 17 23:54:05 Finished compiler/encoders/riscv                                  1s  20MB
Jan 17 23:54:06 Starting compiler/encoders/ag32
Jan 17 23:54:07 Finished compiler/encoders/ag32                                   1s  26MB
Jan 17 23:54:07 Starting compiler/backend/x64
Jan 17 23:54:10 Finished compiler/backend/x64                                     2s  26MB
Jan 17 23:54:10 Starting compiler/backend/arm7
Jan 17 23:54:12 Finished compiler/backend/arm7                                    2s  23MB
Jan 17 23:54:12 Starting compiler/backend/arm8
Jan 17 23:54:14 Finished compiler/backend/arm8                                    2s  21MB
Jan 17 23:54:14 Starting compiler/backend/mips
Jan 17 23:54:17 Finished compiler/backend/mips                                    2s  28MB
Jan 17 23:54:17 Starting compiler/backend/riscv
Jan 17 23:54:19 Finished compiler/backend/riscv                                   2s  22MB
Jan 17 23:54:19 Starting compiler/backend/ag32
Jan 17 23:55:45 Finished compiler/backend/ag32                                 1m26s   1GB
Jan 17 23:55:46 Starting compiler/parsing/proofs
Jan 17 23:55:47 Finished compiler/parsing/proofs                                  1s  18MB
Jan 17 23:55:47 Starting compiler/inference/proofs
Jan 17 23:55:49 Finished compiler/inference/proofs                                1s  21MB
Jan 17 23:55:49 Starting compiler/backend/semantics
Jan 17 23:57:03 Finished compiler/backend/semantics                            1m13s   1GB
Jan 17 23:57:03 Starting compiler/backend/reg_alloc/proofs
Jan 17 23:57:05 Finished compiler/backend/reg_alloc/proofs                        1s  23MB
Jan 17 23:57:05 Starting compiler/backend/proofs
Jan 17 23:58:03 Finished compiler/backend/proofs                                 58s   2GB
Jan 17 23:58:04 Starting compiler/backend/serialiser
Jan 17 23:58:07 Finished compiler/backend/serialiser                              2s  34MB
Jan 17 23:58:07 Starting compiler/encoders/x64/proofs
Jan 18 00:07:54 Finished compiler/encoders/x64/proofs                          9m47s   6GB
Jan 18 00:07:54 Starting compiler/encoders/arm7/proofs
Jan 18 00:21:39 Finished compiler/encoders/arm7/proofs                        13m44s   4GB
Jan 18 00:21:39 Starting compiler/encoders/arm8/proofs
Jan 18 00:28:37 Finished compiler/encoders/arm8/proofs                         6m58s   1GB
Jan 18 00:28:37 Starting compiler/encoders/arm8_asl/proofs
Jan 18 01:21:23 Finished compiler/encoders/arm8_asl/proofs                    52m45s  10GB
Jan 18 01:21:23 Starting compiler/encoders/mips/proofs
Jan 18 01:31:55 Finished compiler/encoders/mips/proofs                        10m32s   3GB
Jan 18 01:31:55 Starting compiler/encoders/riscv/proofs
Jan 18 01:40:42 Finished compiler/encoders/riscv/proofs                        8m46s   2GB
Jan 18 01:40:42 Starting compiler/encoders/ag32/proofs
Jan 18 01:43:12 Finished compiler/encoders/ag32/proofs                         2m30s   1GB
Jan 18 01:43:12 Starting compiler/backend/x64/proofs
Jan 18 01:43:42 Finished compiler/backend/x64/proofs                             29s   2GB
Jan 18 01:43:42 Starting compiler/backend/arm7/proofs
Jan 18 01:44:16 Finished compiler/backend/arm7/proofs                            33s   2GB
Jan 18 01:44:16 Starting compiler/backend/arm8/proofs
Jan 18 01:44:47 Finished compiler/backend/arm8/proofs                            31s   1GB
Jan 18 01:44:48 Starting compiler/backend/arm8_asl
Jan 18 01:45:12 Finished compiler/backend/arm8_asl                               24s   2GB
Jan 18 01:45:12 Starting compiler/backend/mips/proofs
Jan 18 01:45:46 Finished compiler/backend/mips/proofs                            33s   2GB
Jan 18 01:45:46 Starting compiler/backend/riscv/proofs
Jan 18 01:46:19 Finished compiler/backend/riscv/proofs                           33s   2GB
Jan 18 01:46:19 Starting compiler/backend/ag32/proofs
Jan 18 01:59:59 Finished compiler/backend/ag32/proofs                         13m39s   3GB
Jan 18 01:59:59 Starting candle/set-theory
Jan 18 02:00:38 Finished candle/set-theory                                       39s   1GB
Jan 18 02:00:38 Starting candle/syntax-lib
Jan 18 02:00:40 Finished candle/syntax-lib                                        1s  19MB
Jan 18 02:00:40 Starting candle/standard/syntax
Jan 18 02:00:52 Finished candle/standard/syntax                                  11s 699MB
Jan 18 02:00:52 Starting candle/standard/semantics
Jan 18 02:02:52 Finished candle/standard/semantics                             2m00s   1GB
Jan 18 02:02:52 Starting candle/standard/monadic
Jan 18 02:02:54 Finished candle/standard/monadic                                  1s  22MB
Jan 18 02:02:54 Starting candle/standard/ml_kernel
Jan 18 02:04:34 Finished candle/standard/ml_kernel                             1m39s   3GB
Jan 18 02:04:34 Starting candle/overloading/syntax
Jan 18 02:07:57 Finished candle/overloading/syntax                             3m23s   1GB
Jan 18 02:07:57 Starting candle/overloading/semantics
Jan 18 02:20:09 Finished candle/overloading/semantics                         12m11s   3GB
Jan 18 02:20:09 Starting candle/overloading/monadic
Jan 18 02:22:55 Finished candle/overloading/monadic                            2m46s   1GB
Jan 18 02:22:55 Starting candle/overloading/ml_kernel
Jan 18 02:30:51 Finished candle/overloading/ml_kernel                          7m56s   3GB
Jan 18 02:30:52 Starting candle/overloading/ml_checker
Jan 18 02:33:26 Finished candle/overloading/ml_checker                         2m34s   3GB
Jan 18 02:33:26 Starting candle/prover
Jan 18 02:43:36 Finished candle/prover                                        10m10s   3GB
Jan 18 02:43:36 Starting pancake
Jan 18 02:44:19 Finished pancake                                                 42s 863MB
Jan 18 02:44:19 Starting pancake/ffi
Jan 18 02:44:20 Finished pancake/ffi                                              0s  13MB
Jan 18 02:44:20 Starting pancake/semantics
Jan 18 02:46:49 Finished pancake/semantics                                     2m29s   1GB
Jan 18 02:46:50 Starting pancake/parser
Jan 18 02:47:13 Finished pancake/parser                                          22s   1GB
Jan 18 02:47:13 Starting pancake/proofs
Jan 18 03:20:31 Finished pancake/proofs                                       33m17s   4GB
Jan 18 03:20:31 Starting characteristic/examples
Jan 18 03:22:06 Finished characteristic/examples                               1m35s   2GB
Jan 18 03:22:07 Starting tutorial/solutions
Jan 18 03:37:57 Finished tutorial/solutions                                   15m50s   8GB
Jan 18 03:37:57 Starting translator/monadic/examples
Jan 18 03:42:03 Finished translator/monadic/examples                           4m05s   2GB
Jan 18 03:42:03 Starting examples
Jan 18 03:58:36 Finished examples                                             16m32s   5GB
Jan 18 03:58:36 Starting examples/compilation/x64
Jan 18 06:00:02 Finished examples/compilation/x64                           2h01m26s  16GB
Jan 18 06:00:03 Starting examples/compilation/x64/proofs
Jan 18 06:02:37 Finished examples/compilation/x64/proofs                       2m34s   4GB
Jan 18 06:02:37 Starting examples/compilation/ag32
Jan 18 06:32:55 Finished examples/compilation/ag32                            30m17s   9GB
Jan 18 06:32:55 Starting examples/compilation/ag32/proofs
Jan 18 06:34:02 Finished examples/compilation/ag32/proofs                      1m06s   5GB
Jan 18 06:34:02 Starting examples/compilation/to_word
Jan 18 06:37:20 Finished examples/compilation/to_word                          3m18s   4GB
Jan 18 06:37:20 Starting examples/lpr_checker
Jan 18 06:38:27 Finished examples/lpr_checker                                  1m06s   1GB
Jan 18 06:38:27 Starting examples/lpr_checker/array
Jan 18 07:09:56 Finished examples/lpr_checker/array                           31m28s   7GB
Jan 18 07:09:56 Starting examples/lpr_checker/array/compilation
Jan 18 08:00:51 Finished examples/lpr_checker/array/compilation               50m54s  27GB
Jan 18 08:00:51 Starting examples/lpr_checker/array/compilation/proofs
Jan 18 08:02:55 Finished examples/lpr_checker/array/compilation/proofs         2m03s   3GB
Jan 18 08:02:55 Starting examples/lpr_checker/array/compilation/proofsARM8
Jan 18 08:08:33 Finished examples/lpr_checker/array/compilation/proofsARM8     5m37s  17GB
Jan 18 08:08:33 Starting examples/pseudo_bool
Jan 18 08:10:22 Finished examples/pseudo_bool                                  1m48s   1GB
Jan 18 08:10:22 Starting examples/pseudo_bool/cnf_encoding
Jan 18 08:10:48 Finished examples/pseudo_bool/cnf_encoding                       26s 687MB
Jan 18 08:10:48 Starting examples/pseudo_bool/graph_encoding
Jan 18 08:11:31 Finished examples/pseudo_bool/graph_encoding                     42s   1GB
Jan 18 08:11:31 Starting examples/pseudo_bool/array
Jan 18 09:05:54 Finished examples/pseudo_bool/array                           54m22s   6GB
Jan 18 09:05:54 Starting examples/pseudo_bool/array/compilation
Jan 18 12:02:54 Finished examples/pseudo_bool/array/compilation             2h56m59s  33GB
Jan 18 12:02:54 Starting examples/pseudo_bool/array/compilation/proofs
Jan 18 12:05:44 Finished examples/pseudo_bool/array/compilation/proofs         2m50s   5GB
Jan 18 12:05:45 Starting examples/opentheory
Jan 18 12:16:46 Finished examples/opentheory                                  11m01s   4GB
Jan 18 12:16:46 Starting examples/opentheory
Jan 18 12:16:48 Finished examples/opentheory                                      1s  35MB
Jan 18 12:16:48 Starting examples/opentheory/compilation
Jan 18 12:55:18 Finished examples/opentheory/compilation                      38m29s  38GB
Jan 18 12:55:18 Starting examples/opentheory/compilation/proofs
Jan 18 12:56:22 Finished examples/opentheory/compilation/proofs                1m04s   4GB
Jan 18 12:56:22 Starting examples/opentheory/compilation/ag32
Jan 18 13:30:43 Finished examples/opentheory/compilation/ag32                 34m20s  30GB
Jan 18 13:30:43 Starting examples/opentheory/compilation/ag32/proofs
Jan 18 13:32:39 Finished examples/opentheory/compilation/ag32/proofs           1m55s   7GB
Jan 18 13:32:39 Starting examples/sat_encodings
Jan 18 13:34:44 Finished examples/sat_encodings                                2m04s 938MB
Jan 18 13:34:44 Starting examples/sat_encodings/case_studies
Jan 18 13:36:32 Finished examples/sat_encodings/case_studies                   1m48s   1GB
Jan 18 13:36:32 Starting examples/sat_encodings/translation
Jan 18 13:42:42 Finished examples/sat_encodings/translation                    6m09s   4GB
Jan 18 13:42:42 Starting examples/sat_encodings/translation/compilation
Jan 18 14:31:19 Finished examples/sat_encodings/translation/compilation       48m36s  23GB
Jan 18 14:31:19 Starting examples/deflate
Jan 18 14:32:19 Finished examples/deflate                                      1m00s 854MB
Jan 18 14:32:19 Starting examples/deflate/translation
Jan 18 14:34:03 Finished examples/deflate/translation                          1m43s   3GB
Jan 18 14:34:03 Starting examples/deflate/translation/compilation
Jan 18 14:54:19 Finished examples/deflate/translation/compilation             20m15s  14GB
Jan 18 14:54:19 Starting examples/vipr
Jan 18 14:58:30 Finished examples/vipr                                         4m10s   3GB
Jan 18 14:58:30 Starting examples/vipr/compilation
Jan 18 15:18:59 Finished examples/vipr/compilation                            20m28s  15GB
Jan 18 15:18:59 Starting translator/okasaki-examples
Jan 18 15:24:10 Finished translator/okasaki-examples                           5m10s   2GB
Jan 18 15:24:10 Starting translator/other-examples
Jan 18 15:26:55 Finished translator/other-examples                             2m44s   1GB
Jan 18 15:26:55 Starting compiler/parsing/tests
Jan 18 15:27:27 Finished compiler/parsing/tests                                  31s 811MB
Jan 18 15:27:27 Starting compiler/inference/tests
Jan 18 15:36:08 Finished compiler/inference/tests                              8m40s   6GB
Jan 18 15:36:08 Starting compiler/printing/test
Jan 18 15:40:01 Finished compiler/printing/test                                3m52s   3GB
Jan 18 15:40:01 Starting icing/flover
Jan 18 16:23:30 Finished icing/flover                                         43m28s   2GB
Jan 18 16:23:30 Starting icing/
Jan 18 17:18:08 Finished icing/                                               54m37s   7GB
Jan 18 17:18:08 Starting icing/examples
Jan 18 17:19:42 Finished icing/examples                                        1m33s   4GB
Jan 18 17:19:42 Starting compiler/repl
Jan 18 17:28:31 Finished compiler/repl                                         8m49s   6GB
Jan 18 17:28:31 Starting unverified/sexpr-bootstrap/x64/64
Jan 18 17:42:08 Finished unverified/sexpr-bootstrap/x64/64                    13m35s  15GB
Jan 18 17:42:08 Starting unverified/sexpr-bootstrap/x64/32
Jan 18 17:53:13 Finished unverified/sexpr-bootstrap/x64/32                    11m04s  14GB
Jan 18 17:53:14 Starting compiler/benchmarks
Jan 18 18:08:50 Finished compiler/benchmarks                                  15m36s   2GB
Jan 18 18:08:50 Starting compiler/bootstrap/compilation/x64/64
Jan 19 06:45:56 Finished compiler/bootstrap/compilation/x64/64             12h37m05s  64GB
Jan 19 06:45:56 Starting compiler/bootstrap/compilation/x64/64/proofs
Jan 19 07:18:18 Finished compiler/bootstrap/compilation/x64/64/proofs         32m21s  16GB
Jan 19 07:18:18 Starting compiler/bootstrap/compilation/x64/32
Jan 19 07:18:20 FAILED: compiler/bootstrap/compilation/x64/32
Scanning [1m$(HOLDIR)/src/sort[0m
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/basis[0m