Job 2365

CakeML:b82ce2d867fe551f5fd2b2d71ba41db7afaa5dbd
  Add arm8 bootstrap [Apr 13 15:53:58]
#991 (master)
Merging into:9c063a7d92cadb36c49a6e45856ae0db734dc9e5
  Merge pull request #989 from CakeML/pan_errors [Apr 11 22:24:05]
HOL:4c9b707ee09fa5cfedca6cfb6ebb91a371a8b447
  Fix proof failure caused by name generation change in 68ea515ce46a83 [Apr 10 23:20:47]
Machine:stove 5.15.0-86-generic x86_64 GNU/Linux

Apr 15 03:50:59 Claimed job
Apr 15 03:51:03 Building HOL
Apr 15 04:04:05 Starting developers
Apr 15 04:04:10 Finished developers                                               5s  90MB
Apr 15 04:04:10 Starting developers/bin
Apr 15 04:04:16 Finished developers/bin                                           5s   1GB
Apr 15 04:04:17 Starting compiler/proofs
Apr 15 06:05:33 Finished compiler/proofs                                    2h01m16s  19GB
Apr 15 06:05:33 Starting compiler/bootstrap/translation
Apr 15 14:26:21 Finished compiler/bootstrap/translation                     8h20m47s  46GB
Apr 15 14:26:21 Starting semantics/ffi
Apr 15 14:26:26 Finished semantics/ffi                                            4s 393MB
Apr 15 14:26:26 Starting semantics
Apr 15 14:26:28 Finished semantics                                                1s  19MB
Apr 15 14:26:28 Starting semantics/proofs
Apr 15 14:27:03 Finished semantics/proofs                                        34s 745MB
Apr 15 14:27:03 Starting semantics/alt_semantics
Apr 15 14:27:37 Finished semantics/alt_semantics                                 33s 842MB
Apr 15 14:27:37 Starting semantics/alt_semantics/proofs
Apr 15 14:39:39 Finished semantics/alt_semantics/proofs                       12m01s   1GB
Apr 15 14:39:39 Starting basis/pure
Apr 15 14:39:40 Finished basis/pure                                               1s  19MB
Apr 15 14:39:40 Starting translator
Apr 15 14:41:31 Finished translator                                            1m50s   1GB
Apr 15 14:41:31 Starting compiler/parsing
Apr 15 14:41:33 Finished compiler/parsing                                         1s  18MB
Apr 15 14:41:33 Starting characteristic
Apr 15 14:41:35 Finished characteristic                                           1s  29MB
Apr 15 14:41:35 Starting translator/monadic
Apr 15 14:41:37 Finished translator/monadic                                       1s  25MB
Apr 15 14:41:37 Starting basis
Apr 15 14:45:22 Finished basis                                                 3m44s   3GB
Apr 15 14:45:22 Starting compiler/inference
Apr 15 14:45:24 Finished compiler/inference                                       1s  21MB
Apr 15 14:45:24 Starting compiler/backend/reg_alloc
Apr 15 14:45:25 Finished compiler/backend/reg_alloc                               1s  20MB
Apr 15 14:45:25 Starting compiler/backend/gc
Apr 15 14:45:28 Finished compiler/backend/gc                                      2s  28MB
Apr 15 14:45:28 Starting compiler/backend
Apr 15 14:45:40 Finished compiler/backend                                        12s 820MB
Apr 15 14:45:40 Starting compiler/encoders/asm
Apr 15 14:45:42 Finished compiler/encoders/asm                                    1s  22MB
Apr 15 14:45:42 Starting compiler/encoders/x64
Apr 15 14:45:44 Finished compiler/encoders/x64                                    1s  22MB
Apr 15 14:45:44 Starting compiler/encoders/arm7
Apr 15 14:45:46 Finished compiler/encoders/arm7                                   1s  27MB
Apr 15 14:45:46 Starting compiler/encoders/arm8
Apr 15 14:45:48 Finished compiler/encoders/arm8                                   1s  21MB
Apr 15 14:45:48 Starting compiler/encoders/arm8_asl
Apr 15 17:17:37 Finished compiler/encoders/arm8_asl                         2h31m48s  32GB
Apr 15 17:17:37 Starting compiler/encoders/mips
Apr 15 17:17:39 Finished compiler/encoders/mips                                   1s  24MB
Apr 15 17:17:39 Starting compiler/encoders/riscv
Apr 15 17:17:41 Finished compiler/encoders/riscv                                  1s  26MB
Apr 15 17:17:41 Starting compiler/encoders/ag32
Apr 15 17:17:43 Finished compiler/encoders/ag32                                   1s  19MB
Apr 15 17:17:43 Starting compiler/backend/x64
Apr 15 17:17:45 Finished compiler/backend/x64                                     2s  24MB
Apr 15 17:17:45 Starting compiler/backend/arm7
Apr 15 17:17:47 Finished compiler/backend/arm7                                    2s  25MB
Apr 15 17:17:47 Starting compiler/backend/arm8
Apr 15 17:17:50 Finished compiler/backend/arm8                                    2s  22MB
Apr 15 17:17:50 Starting compiler/backend/mips
Apr 15 17:17:52 Finished compiler/backend/mips                                    2s  25MB
Apr 15 17:17:52 Starting compiler/backend/riscv
Apr 15 17:17:54 Finished compiler/backend/riscv                                   2s  32MB
Apr 15 17:17:54 Starting compiler/backend/ag32
Apr 15 17:19:21 Finished compiler/backend/ag32                                 1m26s   1GB
Apr 15 17:19:21 Starting compiler/parsing/proofs
Apr 15 17:19:23 Finished compiler/parsing/proofs                                  1s  19MB
Apr 15 17:19:23 Starting compiler/inference/proofs
Apr 15 17:19:25 Finished compiler/inference/proofs                                1s  20MB
Apr 15 17:19:25 Starting compiler/backend/semantics
Apr 15 17:23:12 Finished compiler/backend/semantics                            3m46s   2GB
Apr 15 17:23:12 Starting compiler/backend/reg_alloc/proofs
Apr 15 17:23:14 Finished compiler/backend/reg_alloc/proofs                        1s  20MB
Apr 15 17:23:14 Starting compiler/backend/proofs
Apr 15 17:24:14 Finished compiler/backend/proofs                                 59s   2GB
Apr 15 17:24:14 Starting compiler/backend/serialiser
Apr 15 17:24:17 Finished compiler/backend/serialiser                              2s  32MB
Apr 15 17:24:17 Starting compiler/encoders/x64/proofs
Apr 15 17:34:07 Finished compiler/encoders/x64/proofs                          9m50s   7GB
Apr 15 17:34:07 Starting compiler/encoders/arm7/proofs
Apr 15 17:48:04 Finished compiler/encoders/arm7/proofs                        13m56s   3GB
Apr 15 17:48:05 Starting compiler/encoders/arm8/proofs
Apr 15 17:54:57 Finished compiler/encoders/arm8/proofs                         6m52s   1GB
Apr 15 17:54:57 Starting compiler/encoders/arm8_asl/proofs
Apr 15 18:49:06 Finished compiler/encoders/arm8_asl/proofs                    54m09s   8GB
Apr 15 18:49:07 Starting compiler/encoders/mips/proofs
Apr 15 18:59:52 Finished compiler/encoders/mips/proofs                        10m45s   2GB
Apr 15 18:59:52 Starting compiler/encoders/riscv/proofs
Apr 15 19:08:54 Finished compiler/encoders/riscv/proofs                        9m02s   1GB
Apr 15 19:08:54 Starting compiler/encoders/ag32/proofs
Apr 15 19:11:29 Finished compiler/encoders/ag32/proofs                         2m34s   1GB
Apr 15 19:11:29 Starting compiler/backend/x64/proofs
Apr 15 19:11:59 Finished compiler/backend/x64/proofs                             30s   1GB
Apr 15 19:11:59 Starting compiler/backend/arm7/proofs
Apr 15 19:12:35 Finished compiler/backend/arm7/proofs                            35s   2GB
Apr 15 19:12:35 Starting compiler/backend/arm8/proofs
Apr 15 19:13:07 Finished compiler/backend/arm8/proofs                            31s   2GB
Apr 15 19:13:07 Starting compiler/backend/arm8_asl
Apr 15 19:13:31 Finished compiler/backend/arm8_asl                               24s   1GB
Apr 15 19:13:32 Starting compiler/backend/mips/proofs
Apr 15 19:14:04 Finished compiler/backend/mips/proofs                            32s   2GB
Apr 15 19:14:04 Starting compiler/backend/riscv/proofs
Apr 15 19:14:41 Finished compiler/backend/riscv/proofs                           36s   2GB
Apr 15 19:14:41 Starting compiler/backend/ag32/proofs
Apr 15 19:29:10 Finished compiler/backend/ag32/proofs                         14m29s   3GB
Apr 15 19:29:11 Starting candle/set-theory
Apr 15 19:29:49 Finished candle/set-theory                                       38s   1GB
Apr 15 19:29:49 Starting candle/syntax-lib
Apr 15 19:29:51 Finished candle/syntax-lib                                        1s  20MB
Apr 15 19:29:51 Starting candle/standard/syntax
Apr 15 19:30:02 Finished candle/standard/syntax                                  10s 775MB
Apr 15 19:30:02 Starting candle/standard/semantics
Apr 15 19:32:03 Finished candle/standard/semantics                             2m00s   1GB
Apr 15 19:32:03 Starting candle/standard/monadic
Apr 15 19:32:05 Finished candle/standard/monadic                                  1s  21MB
Apr 15 19:32:05 Starting candle/standard/ml_kernel
Apr 15 19:33:43 Finished candle/standard/ml_kernel                             1m37s   3GB
Apr 15 19:33:43 Starting candle/overloading/syntax
Apr 15 19:37:05 Finished candle/overloading/syntax                             3m21s   1GB
Apr 15 19:37:05 Starting candle/overloading/semantics
Apr 15 19:49:31 Finished candle/overloading/semantics                         12m25s   3GB
Apr 15 19:49:31 Starting candle/overloading/monadic
Apr 15 19:52:15 Finished candle/overloading/monadic                            2m44s   1GB
Apr 15 19:52:15 Starting candle/overloading/ml_kernel
Apr 15 20:00:16 Finished candle/overloading/ml_kernel                          8m00s   3GB
Apr 15 20:00:16 Starting candle/overloading/ml_checker
Apr 15 20:02:49 Finished candle/overloading/ml_checker                         2m32s   2GB
Apr 15 20:02:49 Starting candle/prover
Apr 15 20:12:43 Finished candle/prover                                         9m53s   3GB
Apr 15 20:12:43 Starting pancake
Apr 15 20:13:29 Finished pancake                                                 46s 936MB
Apr 15 20:13:29 Starting pancake/ffi
Apr 15 20:13:30 Finished pancake/ffi                                              0s  13MB
Apr 15 20:13:30 Starting pancake/semantics
Apr 15 20:16:06 Finished pancake/semantics                                     2m36s   1GB
Apr 15 20:16:06 Starting pancake/parser
Apr 15 20:16:30 Finished pancake/parser                                          23s   1GB
Apr 15 20:16:30 Starting pancake/proofs
Apr 15 20:51:11 Finished pancake/proofs                                       34m40s   4GB
Apr 15 20:51:11 Starting characteristic/examples
Apr 15 20:52:58 Finished characteristic/examples                               1m46s   3GB
Apr 15 20:52:58 Starting tutorial/solutions
Apr 15 21:08:32 Finished tutorial/solutions                                   15m34s   9GB
Apr 15 21:08:32 Starting translator/monadic/examples
Apr 15 21:12:41 Finished translator/monadic/examples                           4m08s   2GB
Apr 15 21:12:41 Starting examples
Apr 15 21:28:44 Finished examples                                             16m02s   4GB
Apr 15 21:28:44 Starting examples/compilation/x64
Apr 15 23:29:47 Finished examples/compilation/x64                           2h01m02s  22GB
Apr 15 23:29:47 Starting examples/compilation/x64/proofs
Apr 15 23:32:25 Finished examples/compilation/x64/proofs                       2m38s   4GB
Apr 15 23:32:25 Starting examples/compilation/ag32
Apr 16 00:03:23 Finished examples/compilation/ag32                            30m57s   9GB
Apr 16 00:03:23 Starting examples/compilation/ag32/proofs
Apr 16 00:04:29 Finished examples/compilation/ag32/proofs                      1m06s   5GB
Apr 16 00:04:30 Starting examples/compilation/to_word
Apr 16 00:07:50 Finished examples/compilation/to_word                          3m20s   6GB
Apr 16 00:07:50 Starting examples/lpr_checker
Apr 16 00:08:57 Finished examples/lpr_checker                                  1m06s   1GB
Apr 16 00:08:57 Starting examples/lpr_checker/array
Apr 16 00:41:37 Finished examples/lpr_checker/array                           32m39s   4GB
Apr 16 00:41:37 Starting examples/lpr_checker/array/compilation
Apr 16 01:34:11 Finished examples/lpr_checker/array/compilation               52m34s  26GB
Apr 16 01:34:11 Starting examples/lpr_checker/array/compilation/proofs
Apr 16 01:36:07 Finished examples/lpr_checker/array/compilation/proofs         1m54s   3GB
Apr 16 01:36:07 Starting examples/lpr_checker/array/compilation/proofsARM8
Apr 16 01:45:25 Finished examples/lpr_checker/array/compilation/proofsARM8     9m18s  22GB
Apr 16 01:45:25 Starting examples/xlrup_checker
Apr 16 01:46:24 Finished examples/xlrup_checker                                  58s   1GB
Apr 16 01:46:24 Starting examples/xlrup_checker/array
Apr 16 02:03:57 Finished examples/xlrup_checker/array                         17m33s   5GB
Apr 16 02:03:57 Starting examples/xlrup_checker/array/compilation
Apr 16 02:26:56 Finished examples/xlrup_checker/array/compilation             22m58s  19GB
Apr 16 02:26:57 Starting examples/xlrup_checker/array/compilation/proofs
Apr 16 02:27:58 Finished examples/xlrup_checker/array/compilation/proofs       1m01s   4GB
Apr 16 02:27:58 Starting examples/pseudo_bool
Apr 16 02:29:56 Finished examples/pseudo_bool                                  1m57s   1GB
Apr 16 02:29:56 Starting examples/pseudo_bool/cnf_encoding
Apr 16 02:30:24 Finished examples/pseudo_bool/cnf_encoding                       28s   1GB
Apr 16 02:30:24 Starting examples/pseudo_bool/graph_encoding
Apr 16 02:31:08 Finished examples/pseudo_bool/graph_encoding                     43s 891MB
Apr 16 02:31:08 Starting examples/pseudo_bool/array
Apr 16 03:46:37 Finished examples/pseudo_bool/array                         1h15m29s   8GB
Apr 16 03:46:37 Starting examples/pseudo_bool/array/compilation
Apr 16 11:42:19 Finished examples/pseudo_bool/array/compilation             7h55m40s  64GB
Apr 16 11:42:19 Starting examples/pseudo_bool/array/compilation/proofs
Apr 16 11:44:59 Finished examples/pseudo_bool/array/compilation/proofs         2m40s   6GB
Apr 16 11:44:59 Starting examples/opentheory
Apr 16 11:55:54 Finished examples/opentheory                                  10m54s   4GB
Apr 16 11:55:54 Starting examples/opentheory
Apr 16 11:55:56 Finished examples/opentheory                                      1s  27MB
Apr 16 11:55:56 Starting examples/opentheory/compilation
Apr 16 12:35:23 Finished examples/opentheory/compilation                      39m27s  35GB
Apr 16 12:35:23 Starting examples/opentheory/compilation/proofs
Apr 16 12:36:26 Finished examples/opentheory/compilation/proofs                1m02s   4GB
Apr 16 12:36:26 Starting examples/opentheory/compilation/ag32
Apr 16 13:10:02 Finished examples/opentheory/compilation/ag32                 33m35s  32GB
Apr 16 13:10:02 Starting examples/opentheory/compilation/ag32/proofs
Apr 16 13:11:58 Finished examples/opentheory/compilation/ag32/proofs           1m55s   4GB
Apr 16 13:11:58 Starting examples/sat_encodings
Apr 16 13:14:01 Finished examples/sat_encodings                                2m03s   1GB
Apr 16 13:14:01 Starting examples/sat_encodings/case_studies
Apr 16 13:15:50 Finished examples/sat_encodings/case_studies                   1m48s   1GB
Apr 16 13:15:50 Starting examples/sat_encodings/translation
Apr 16 13:21:57 Finished examples/sat_encodings/translation                    6m07s   5GB
Apr 16 13:21:57 Starting examples/sat_encodings/translation/compilation
Apr 16 14:08:38 Finished examples/sat_encodings/translation/compilation       46m40s  20GB
Apr 16 14:08:38 Starting examples/deflate
Apr 16 14:09:37 Finished examples/deflate                                        59s 913MB
Apr 16 14:09:37 Starting examples/deflate/translation
Apr 16 14:11:22 Finished examples/deflate/translation                          1m43s   3GB
Apr 16 14:11:22 Starting examples/deflate/translation/compilation
Apr 16 14:32:08 Finished examples/deflate/translation/compilation             20m46s  12GB
Apr 16 14:32:08 Starting examples/vipr
Apr 16 14:36:12 Finished examples/vipr                                         4m03s   3GB
Apr 16 14:36:12 Starting examples/vipr/compilation
Apr 16 14:57:15 Finished examples/vipr/compilation                            21m02s  21GB
Apr 16 14:57:15 Starting translator/okasaki-examples
Apr 16 15:02:31 Finished translator/okasaki-examples                           5m15s   2GB
Apr 16 15:02:31 Starting translator/other-examples
Apr 16 15:05:45 Finished translator/other-examples                             3m13s   1GB
Apr 16 15:05:45 Starting compiler/parsing/tests
Apr 16 15:06:17 Finished compiler/parsing/tests                                  32s 815MB
Apr 16 15:06:17 Starting compiler/inference/tests
Apr 16 15:14:55 Finished compiler/inference/tests                              8m37s   3GB
Apr 16 15:14:55 Starting compiler/printing/test
Apr 16 15:18:51 Finished compiler/printing/test                                3m56s   3GB
Apr 16 15:18:52 Starting icing/flover
Apr 16 16:02:35 Finished icing/flover                                         43m43s   2GB
Apr 16 16:02:35 Starting icing/
Apr 16 16:57:23 Finished icing/                                               54m48s   7GB
Apr 16 16:57:23 Starting icing/examples
Apr 16 16:59:02 Finished icing/examples                                        1m39s   6GB
Apr 16 16:59:02 Starting compiler/repl
Apr 16 17:07:52 Finished compiler/repl                                         8m49s   4GB
Apr 16 17:07:52 Starting unverified/sexpr-bootstrap/x64/64
Apr 16 17:21:23 Finished unverified/sexpr-bootstrap/x64/64                    13m30s  14GB
Apr 16 17:21:23 Starting unverified/sexpr-bootstrap/x64/32
Apr 16 17:32:30 Finished unverified/sexpr-bootstrap/x64/32                    11m07s  13GB
Apr 16 17:32:30 Starting compiler/benchmarks
Apr 16 17:48:04 Finished compiler/benchmarks                                  15m33s   2GB
Apr 16 17:48:04 Starting compiler/bootstrap/compilation/x64/64
Apr 17 06:09:13 Finished compiler/bootstrap/compilation/x64/64             12h21m08s  64GB
Apr 17 06:09:13 Starting compiler/bootstrap/compilation/x64/64/proofs
Apr 17 06:30:09 Finished compiler/bootstrap/compilation/x64/64/proofs         20m56s  39GB
Apr 17 06:30:10 Starting compiler/bootstrap/compilation/x64/32
Apr 17 13:57:59 Finished compiler/bootstrap/compilation/x64/32              7h27m49s  64GB
Apr 17 13:57:59 Starting compiler/bootstrap/compilation/x64/32/proofs
Apr 17 14:01:08 Finished compiler/bootstrap/compilation/x64/32/proofs          3m08s  19GB
Apr 17 14:01:08 Starting compiler/bootstrap/compilation/ag32/32
Apr 17 21:25:00 Finished compiler/bootstrap/compilation/ag32/32             7h23m51s  63GB
Apr 17 21:25:00 Starting compiler/bootstrap/compilation/ag32/32/proofs
Apr 17 21:32:28 Finished compiler/bootstrap/compilation/ag32/32/proofs         7m28s  49GB
Apr 17 21:32:28 SUCCESS