Job 2195

CakeML:70c9116352cfd04905fbfb3bd8726ca1aaec0f1d
  fix Holmakefile [Aug 16 02:50:12]
#967 (lpr_arm8)
Merging into:5c1bae6b33cf93343962f658faefefee12f74a9c
  Merge pull request #965 from CakeML/explorer [Aug 10 04:53:38]
HOL:c505f5761a545a06f2a80c536262e608021c3955
  Fix the proof of zagier_fix in experimental kernel. [Aug 17 06:53:11]
Machine:lammington

Aug 20 07:53:10 Claimed job
Aug 20 07:53:16 Building HOL
Aug 20 08:08:06 Starting developers
Aug 20 08:08:09 Finished developers                                               2s 199MB
Aug 20 08:08:10 Starting developers/bin
Aug 20 08:08:21 Finished developers/bin                                          10s   1GB
Aug 20 08:08:22 Starting compiler/proofs
Aug 20 09:53:17 Finished compiler/proofs                                    1h44m54s  34GB
Aug 20 09:53:18 Starting compiler/bootstrap/translation
Aug 20 17:49:08 Finished compiler/bootstrap/translation                     7h55m48s  88GB
Aug 20 17:49:09 Starting semantics/ffi
Aug 20 17:49:18 Finished semantics/ffi                                            8s 675MB
Aug 20 17:49:18 Starting semantics
Aug 20 17:49:20 Finished semantics                                                0s  65MB
Aug 20 17:49:20 Starting semantics/proofs
Aug 20 17:49:55 Finished semantics/proofs                                        33s   1GB
Aug 20 17:49:56 Starting semantics/alt_semantics
Aug 20 17:50:35 Finished semantics/alt_semantics                                 38s   1GB
Aug 20 17:50:36 Starting semantics/alt_semantics/proofs
Aug 20 18:01:33 Finished semantics/alt_semantics/proofs                       10m56s   6GB
Aug 20 18:01:34 Starting basis/pure
Aug 20 18:01:35 Finished basis/pure                                               0s  73MB
Aug 20 18:01:36 Starting translator
Aug 20 18:03:26 Finished translator                                            1m48s   3GB
Aug 20 18:03:27 Starting compiler/parsing
Aug 20 18:03:28 Finished compiler/parsing                                         0s  66MB
Aug 20 18:03:29 Starting characteristic
Aug 20 18:03:30 Finished characteristic                                           0s  89MB
Aug 20 18:03:31 Starting translator/monadic
Aug 20 18:03:32 Finished translator/monadic                                       0s  90MB
Aug 20 18:03:33 Starting basis
Aug 20 18:07:25 Finished basis                                                 3m50s   5GB
Aug 20 18:07:25 Starting compiler/inference
Aug 20 18:07:27 Finished compiler/inference                                       0s  81MB
Aug 20 18:07:28 Starting compiler/backend/reg_alloc
Aug 20 18:07:29 Finished compiler/backend/reg_alloc                               0s  65MB
Aug 20 18:07:30 Starting compiler/backend/gc
Aug 20 18:07:31 Finished compiler/backend/gc                                      0s 130MB
Aug 20 18:07:32 Starting compiler/backend
Aug 20 18:07:50 Finished compiler/backend                                        16s   1GB
Aug 20 18:07:50 Starting compiler/encoders/asm
Aug 20 18:07:52 Finished compiler/encoders/asm                                    0s  82MB
Aug 20 18:07:53 Starting compiler/encoders/x64
Aug 20 18:07:54 Finished compiler/encoders/x64                                    0s  89MB
Aug 20 18:07:55 Starting compiler/encoders/arm7
Aug 20 18:07:56 Finished compiler/encoders/arm7                                   0s  95MB
Aug 20 18:07:57 Starting compiler/encoders/arm8
Aug 20 18:07:58 Finished compiler/encoders/arm8                                   0s  90MB
Aug 20 18:07:59 Starting compiler/encoders/arm8_asl
Aug 20 20:28:48 Finished compiler/encoders/arm8_asl                         2h20m47s  45GB
Aug 20 20:28:48 Starting compiler/encoders/mips
Aug 20 20:28:50 Finished compiler/encoders/mips                                   0s  85MB
Aug 20 20:28:51 Starting compiler/encoders/riscv
Aug 20 20:28:52 Finished compiler/encoders/riscv                                  0s  89MB
Aug 20 20:28:53 Starting compiler/encoders/ag32
Aug 20 20:28:54 Finished compiler/encoders/ag32                                   0s  84MB
Aug 20 20:28:55 Starting compiler/backend/x64
Aug 20 20:28:57 Finished compiler/backend/x64                                     0s 123MB
Aug 20 20:28:57 Starting compiler/backend/arm7
Aug 20 20:28:59 Finished compiler/backend/arm7                                    0s 129MB
Aug 20 20:29:00 Starting compiler/backend/arm8
Aug 20 20:29:02 Finished compiler/backend/arm8                                    0s 129MB
Aug 20 20:29:02 Starting compiler/backend/mips
Aug 20 20:29:04 Finished compiler/backend/mips                                    0s 129MB
Aug 20 20:29:05 Starting compiler/backend/riscv
Aug 20 20:29:07 Finished compiler/backend/riscv                                   0s 129MB
Aug 20 20:29:07 Starting compiler/backend/ag32
Aug 20 20:30:26 Finished compiler/backend/ag32                                 1m18s   2GB
Aug 20 20:30:27 Starting compiler/parsing/proofs
Aug 20 20:30:28 Finished compiler/parsing/proofs                                  0s  73MB
Aug 20 20:30:29 Starting compiler/inference/proofs
Aug 20 20:30:31 Finished compiler/inference/proofs                                0s  82MB
Aug 20 20:30:32 Starting compiler/backend/semantics
Aug 20 20:31:59 Finished compiler/backend/semantics                            1m27s   3GB
Aug 20 20:32:00 Starting compiler/backend/reg_alloc/proofs
Aug 20 20:32:02 Finished compiler/backend/reg_alloc/proofs                        0s  90MB
Aug 20 20:32:03 Starting compiler/backend/proofs
Aug 20 20:33:04 Finished compiler/backend/proofs                               1m00s   3GB
Aug 20 20:33:05 Starting compiler/backend/serialiser
Aug 20 20:33:07 Finished compiler/backend/serialiser                              1s 183MB
Aug 20 20:33:07 Starting compiler/encoders/x64/proofs
Aug 20 20:42:42 Finished compiler/encoders/x64/proofs                          9m33s   6GB
Aug 20 20:42:42 Starting compiler/encoders/arm7/proofs
Aug 20 20:55:27 Finished compiler/encoders/arm7/proofs                        12m43s   7GB
Aug 20 20:55:28 Starting compiler/encoders/arm8/proofs
Aug 20 21:02:04 Finished compiler/encoders/arm8/proofs                         6m35s   4GB
Aug 20 21:02:05 Starting compiler/encoders/arm8_asl/proofs
Aug 20 21:50:01 Finished compiler/encoders/arm8_asl/proofs                    47m54s  11GB
Aug 20 21:50:02 Starting compiler/encoders/mips/proofs
Aug 20 22:00:07 Finished compiler/encoders/mips/proofs                        10m04s  10GB
Aug 20 22:00:08 Starting compiler/encoders/riscv/proofs
Aug 20 22:08:46 Finished compiler/encoders/riscv/proofs                        8m36s   6GB
Aug 20 22:08:46 Starting compiler/encoders/ag32/proofs
Aug 20 22:11:20 Finished compiler/encoders/ag32/proofs                         2m33s   3GB
Aug 20 22:11:21 Starting compiler/backend/x64/proofs
Aug 20 22:12:02 Finished compiler/backend/x64/proofs                             39s   3GB
Aug 20 22:12:03 Starting compiler/backend/arm7/proofs
Aug 20 22:12:48 Finished compiler/backend/arm7/proofs                            44s   2GB
Aug 20 22:12:48 Starting compiler/backend/arm8/proofs
Aug 20 22:13:28 Finished compiler/backend/arm8/proofs                            39s   3GB
Aug 20 22:13:29 Starting compiler/backend/arm8_asl
Aug 20 22:13:56 Finished compiler/backend/arm8_asl                               26s   2GB
Aug 20 22:13:57 Starting compiler/backend/mips/proofs
Aug 20 22:14:42 Finished compiler/backend/mips/proofs                            44s   3GB
Aug 20 22:14:43 Starting compiler/backend/riscv/proofs
Aug 20 22:15:32 Finished compiler/backend/riscv/proofs                           48s   4GB
Aug 20 22:15:33 Starting compiler/backend/ag32/proofs
Aug 20 22:28:33 Finished compiler/backend/ag32/proofs                         12m59s   6GB
Aug 20 22:28:34 Starting candle/set-theory
Aug 20 22:29:17 Finished candle/set-theory                                       41s   1GB
Aug 20 22:29:18 Starting candle/syntax-lib
Aug 20 22:29:19 Finished candle/syntax-lib                                        0s  73MB
Aug 20 22:29:20 Starting candle/standard/syntax
Aug 20 22:29:36 Finished candle/standard/syntax                                  15s   1GB
Aug 20 22:29:37 Starting candle/standard/semantics
Aug 20 22:31:59 Finished candle/standard/semantics                             2m21s   2GB
Aug 20 22:32:00 Starting candle/standard/monadic
Aug 20 22:32:01 Finished candle/standard/monadic                                  0s 101MB
Aug 20 22:32:02 Starting candle/standard/ml_kernel
Aug 20 22:33:51 Finished candle/standard/ml_kernel                             1m48s   5GB
Aug 20 22:33:52 Starting candle/overloading/syntax
Aug 20 22:37:22 Finished candle/overloading/syntax                             3m28s   3GB
Aug 20 22:37:22 Starting candle/overloading/semantics
Aug 20 22:48:45 Finished candle/overloading/semantics                         11m21s   6GB
Aug 20 22:48:46 Starting candle/overloading/monadic
Aug 20 22:51:20 Finished candle/overloading/monadic                            2m31s   3GB
Aug 20 22:51:21 Starting candle/overloading/ml_kernel
Aug 20 22:58:52 Finished candle/overloading/ml_kernel                          7m30s   6GB
Aug 20 22:58:53 Starting candle/overloading/ml_checker
Aug 20 23:01:26 Finished candle/overloading/ml_checker                         2m32s   7GB
Aug 20 23:01:27 Starting candle/prover
Aug 20 23:11:29 Finished candle/prover                                        10m01s   5GB
Aug 20 23:11:30 Starting pancake
Aug 20 23:12:29 Finished pancake                                                 57s   1GB
Aug 20 23:12:29 Starting pancake/ffi
Aug 20 23:12:30 Finished pancake/ffi                                              0s  20MB
Aug 20 23:12:31 Starting pancake/semantics
Aug 20 23:14:49 Finished pancake/semantics                                     2m16s   2GB
Aug 20 23:14:50 Starting pancake/parser
Aug 20 23:15:15 Finished pancake/parser                                          24s   1GB
Aug 20 23:15:15 Starting pancake/proofs
Aug 20 23:45:32 Finished pancake/proofs                                       30m15s   9GB
Aug 20 23:45:32 Starting characteristic/examples
Aug 20 23:47:06 Finished characteristic/examples                               1m32s   5GB
Aug 20 23:47:07 Starting tutorial/solutions
Aug 21 00:02:50 Finished tutorial/solutions                                   15m42s  18GB
Aug 21 00:02:51 Starting translator/monadic/examples
Aug 21 00:06:33 Finished translator/monadic/examples                           3m41s   5GB
Aug 21 00:06:34 Starting examples
Aug 21 00:21:16 Finished examples                                             14m41s   7GB
Aug 21 00:21:17 Starting examples/compilation/x64
Aug 21 02:24:28 Finished examples/compilation/x64                           2h03m09s  33GB
Aug 21 02:24:29 Starting examples/compilation/x64/proofs
Aug 21 02:28:10 Finished examples/compilation/x64/proofs                       3m40s   6GB
Aug 21 02:28:11 Starting examples/compilation/ag32
Aug 21 02:57:47 Finished examples/compilation/ag32                            29m35s  12GB
Aug 21 02:57:48 Starting examples/compilation/ag32/proofs
Aug 21 02:59:14 Finished examples/compilation/ag32/proofs                      1m25s   7GB
Aug 21 02:59:15 Starting examples/compilation/to_word
Aug 21 03:03:10 Finished examples/compilation/to_word                          3m53s  12GB
Aug 21 03:03:10 Starting examples/lpr_checker
Aug 21 03:04:25 Finished examples/lpr_checker                                  1m13s   2GB
Aug 21 03:04:25 Starting examples/lpr_checker/array
Aug 21 03:39:13 Finished examples/lpr_checker/array                           34m46s  11GB
Aug 21 03:39:14 Starting examples/lpr_checker/array/compilation
Aug 21 04:13:23 Finished examples/lpr_checker/array/compilation               34m08s  80GB
Aug 21 04:13:24 Starting examples/lpr_checker/array/compilation/proofs
Aug 21 04:15:15 Finished examples/lpr_checker/array/compilation/proofs         1m50s  10GB
Aug 21 04:15:16 Starting examples/lpr_checker/array/compilation/proofsARM8
Aug 21 04:43:03 Finished examples/lpr_checker/array/compilation/proofsARM8    27m44s  37GB
Aug 21 04:43:04 Starting examples/opentheory
Aug 21 04:53:43 Finished examples/opentheory                                  10m38s   6GB
Aug 21 04:53:44 Starting examples/opentheory
Aug 21 04:53:46 Finished examples/opentheory                                      0s 122MB
Aug 21 04:53:47 Starting examples/opentheory/compilation
Aug 21 05:29:13 Finished examples/opentheory/compilation                      35m25s  48GB
Aug 21 05:29:14 Starting examples/opentheory/compilation/proofs
Aug 21 05:30:46 Finished examples/opentheory/compilation/proofs                1m31s   6GB
Aug 21 05:30:47 Starting examples/opentheory/compilation/ag32
Aug 21 06:03:55 Finished examples/opentheory/compilation/ag32                 33m07s  73GB
Aug 21 06:03:56 Starting examples/opentheory/compilation/ag32/proofs
Aug 21 06:06:12 Finished examples/opentheory/compilation/ag32/proofs           2m15s  12GB
Aug 21 06:06:13 Starting examples/sat_encodings
Aug 21 06:08:50 Finished examples/sat_encodings                                2m36s   1GB
Aug 21 06:08:50 Starting examples/sat_encodings/case_studies
Aug 21 06:10:49 Finished examples/sat_encodings/case_studies                   1m57s   2GB
Aug 21 06:10:50 Starting examples/sat_encodings/translation
Aug 21 06:16:52 Finished examples/sat_encodings/translation                    6m01s   7GB
Aug 21 06:16:53 Starting examples/sat_encodings/translation/compilation
Aug 21 06:51:40 Finished examples/sat_encodings/translation/compilation       34m45s  36GB
Aug 21 06:51:41 Starting examples/deflate
Aug 21 06:52:56 Finished examples/deflate                                      1m14s   2GB
Aug 21 06:52:56 Starting examples/deflate/translation
Aug 21 06:54:34 Finished examples/deflate/translation                          1m36s   7GB
Aug 21 06:54:35 Starting examples/deflate/translation/compilation
Aug 21 07:10:55 Finished examples/deflate/translation/compilation             16m19s  22GB
Aug 21 07:10:56 Starting examples/vipr
Aug 21 07:14:56 Finished examples/vipr                                         3m59s   5GB
Aug 21 07:14:57 Starting examples/vipr/compilation
Aug 21 07:34:29 Finished examples/vipr/compilation                            19m31s  26GB
Aug 21 07:34:30 Starting translator/okasaki-examples
Aug 21 07:39:26 Finished translator/okasaki-examples                           4m55s   4GB
Aug 21 07:39:27 Starting translator/other-examples
Aug 21 07:43:14 Finished translator/other-examples                             3m46s   3GB
Aug 21 07:43:15 Starting compiler/parsing/tests
Aug 21 07:43:50 Finished compiler/parsing/tests                                  34s   1GB
Aug 21 07:43:51 Starting compiler/inference/tests
Aug 21 07:51:34 Finished compiler/inference/tests                              7m42s   7GB
Aug 21 07:51:35 Starting compiler/printing/test
Aug 21 07:55:11 Finished compiler/printing/test                                3m35s   6GB
Aug 21 07:55:12 Starting icing/flover
Aug 21 08:31:09 Finished icing/flover                                         35m55s   4GB
Aug 21 08:31:10 Starting icing/
Aug 21 09:26:58 Finished icing/                                               55m48s  31GB
Aug 21 09:26:59 Starting icing/examples
Aug 21 09:28:42 Finished icing/examples                                        1m41s   8GB
Aug 21 09:28:43 Starting compiler/repl
Aug 21 09:37:24 Finished compiler/repl                                         8m40s   9GB
Aug 21 09:37:25 Starting unverified/sexpr-bootstrap/x64/64
Aug 21 09:48:26 Finished unverified/sexpr-bootstrap/x64/64                    11m00s  16GB
Aug 21 09:48:27 Starting unverified/sexpr-bootstrap/x64/32
Aug 21 09:57:25 Finished unverified/sexpr-bootstrap/x64/32                     8m56s  14GB
Aug 21 09:57:26 Starting compiler/benchmarks
Aug 21 09:58:11 Finished compiler/benchmarks                                     44s 713MB
Aug 21 09:58:12 Starting compiler/bootstrap/compilation/x64/64
Aug 22 00:25:04 Finished compiler/bootstrap/compilation/x64/64             14h26m51s 148GB
Aug 22 00:25:05 Starting compiler/bootstrap/compilation/x64/64/proofs
Aug 22 00:46:08 Finished compiler/bootstrap/compilation/x64/64/proofs         21m02s  34GB
Aug 22 00:46:09 Starting compiler/bootstrap/compilation/x64/32
Aug 22 07:54:40 Finished compiler/bootstrap/compilation/x64/32              7h08m29s 127GB
Aug 22 07:54:41 Starting compiler/bootstrap/compilation/x64/32/proofs
Aug 22 07:58:27 Finished compiler/bootstrap/compilation/x64/32/proofs          3m45s  18GB
Aug 22 07:58:28 Starting compiler/bootstrap/compilation/ag32/32
Aug 22 15:47:05 Finished compiler/bootstrap/compilation/ag32/32             7h48m36s 131GB
Aug 22 15:47:06 Starting compiler/bootstrap/compilation/ag32/32/proofs
Aug 22 15:54:39 Finished compiler/bootstrap/compilation/ag32/32/proofs         7m31s  42GB
Aug 22 15:54:39 SUCCESS