Job 2124

CakeML:856f1d46cc19b4ced4723300b696246381574520
  Merge pull request #948 from CakeML/lex-decimal-chars [May 03 11:46:15]
HOL:a1fef6b1b65a1fc1cc6adf024553ae6f135c1a94
  Add some theorems about abs to integerScript; more modern syntax [May 10 10:45:08]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux
Artefacts:cake-x64-32.tar.gz
cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz

May 13 09:56:23 Claimed job
May 13 09:56:24 Reusing HOL
May 13 09:57:03 Starting developers
May 13 09:57:09 Finished developers                                               5s  72MB
May 13 09:57:09 Starting developers/bin
May 13 09:57:15 Finished developers/bin                                           6s   1GB
May 13 09:57:15 Starting compiler/proofs
May 13 11:49:52 Finished compiler/proofs                                    1h52m35s  19GB
May 13 11:49:52 Starting compiler/bootstrap/translation
May 13 19:47:15 Finished compiler/bootstrap/translation                     7h57m21s  45GB
May 13 19:47:15 Starting semantics/ffi
May 13 19:47:21 Finished semantics/ffi                                            6s 228MB
May 13 19:47:21 Starting semantics
May 13 19:47:23 Finished semantics                                                1s  21MB
May 13 19:47:23 Starting semantics/proofs
May 13 19:47:54 Finished semantics/proofs                                        31s 740MB
May 13 19:47:54 Starting semantics/alt_semantics
May 13 19:48:25 Finished semantics/alt_semantics                                 30s 813MB
May 13 19:48:25 Starting semantics/alt_semantics/proofs
May 13 20:00:08 Finished semantics/alt_semantics/proofs                       11m42s   1GB
May 13 20:00:08 Starting basis/pure
May 13 20:00:10 Finished basis/pure                                               1s  20MB
May 13 20:00:10 Starting translator
May 13 20:02:00 Finished translator                                            1m49s   2GB
May 13 20:02:00 Starting compiler/parsing
May 13 20:02:01 Finished compiler/parsing                                         1s  25MB
May 13 20:02:01 Starting characteristic
May 13 20:02:03 Finished characteristic                                           1s  22MB
May 13 20:02:04 Starting translator/monadic
May 13 20:02:06 Finished translator/monadic                                       1s  24MB
May 13 20:02:06 Starting basis
May 13 20:06:00 Finished basis                                                 3m54s   3GB
May 13 20:06:01 Starting compiler/inference
May 13 20:06:02 Finished compiler/inference                                       1s  18MB
May 13 20:06:02 Starting compiler/backend/reg_alloc
May 13 20:06:04 Finished compiler/backend/reg_alloc                               1s  19MB
May 13 20:06:04 Starting compiler/backend/gc
May 13 20:06:06 Finished compiler/backend/gc                                      2s  26MB
May 13 20:06:07 Starting compiler/backend
May 13 20:06:19 Finished compiler/backend                                        12s 843MB
May 13 20:06:19 Starting compiler/encoders/asm
May 13 20:06:21 Finished compiler/encoders/asm                                    1s  22MB
May 13 20:06:21 Starting compiler/encoders/x64
May 13 20:06:23 Finished compiler/encoders/x64                                    1s  27MB
May 13 20:06:23 Starting compiler/encoders/arm7
May 13 20:06:25 Finished compiler/encoders/arm7                                   1s  22MB
May 13 20:06:25 Starting compiler/encoders/arm8
May 13 20:06:27 Finished compiler/encoders/arm8                                   1s  21MB
May 13 20:06:27 Starting compiler/encoders/arm8_asl
May 13 22:31:16 Finished compiler/encoders/arm8_asl                         2h24m47s  46GB
May 13 22:31:16 Starting compiler/encoders/mips
May 13 22:31:18 Finished compiler/encoders/mips                                   1s  24MB
May 13 22:31:18 Starting compiler/encoders/riscv
May 13 22:31:20 Finished compiler/encoders/riscv                                  1s  24MB
May 13 22:31:20 Starting compiler/encoders/ag32
May 13 22:31:22 Finished compiler/encoders/ag32                                   1s  19MB
May 13 22:31:22 Starting compiler/backend/x64
May 13 22:31:24 Finished compiler/backend/x64                                     2s  28MB
May 13 22:31:24 Starting compiler/backend/arm7
May 13 22:31:27 Finished compiler/backend/arm7                                    2s  29MB
May 13 22:31:27 Starting compiler/backend/arm8
May 13 22:31:29 Finished compiler/backend/arm8                                    2s  22MB
May 13 22:31:29 Starting compiler/backend/mips
May 13 22:31:31 Finished compiler/backend/mips                                    2s  29MB
May 13 22:31:31 Starting compiler/backend/riscv
May 13 22:31:34 Finished compiler/backend/riscv                                   2s  24MB
May 13 22:31:34 Starting compiler/backend/ag32
May 13 22:33:01 Finished compiler/backend/ag32                                 1m27s   1GB
May 13 22:33:02 Starting compiler/parsing/proofs
May 13 22:33:03 Finished compiler/parsing/proofs                                  1s  19MB
May 13 22:33:03 Starting compiler/inference/proofs
May 13 22:33:05 Finished compiler/inference/proofs                                1s  20MB
May 13 22:33:05 Starting compiler/backend/semantics
May 13 22:34:16 Finished compiler/backend/semantics                            1m10s   1GB
May 13 22:34:16 Starting compiler/backend/reg_alloc/proofs
May 13 22:34:18 Finished compiler/backend/reg_alloc/proofs                        1s  22MB
May 13 22:34:18 Starting compiler/backend/proofs
May 13 22:35:17 Finished compiler/backend/proofs                                 58s   2GB
May 13 22:35:17 Starting compiler/backend/serialiser
May 13 22:35:20 Finished compiler/backend/serialiser                              2s  28MB
May 13 22:35:20 Starting compiler/encoders/x64/proofs
May 13 22:45:11 Finished compiler/encoders/x64/proofs                          9m50s   5GB
May 13 22:45:11 Starting compiler/encoders/arm7/proofs
May 13 22:58:53 Finished compiler/encoders/arm7/proofs                        13m42s   3GB
May 13 22:58:53 Starting compiler/encoders/arm8/proofs
May 13 23:05:46 Finished compiler/encoders/arm8/proofs                         6m53s   1GB
May 13 23:05:46 Starting compiler/encoders/arm8_asl/proofs
May 13 23:57:46 Finished compiler/encoders/arm8_asl/proofs                    51m57s   5GB
May 13 23:57:46 Starting compiler/encoders/mips/proofs
May 14 00:08:29 Finished compiler/encoders/mips/proofs                        10m42s   2GB
May 14 00:08:29 Starting compiler/encoders/riscv/proofs
May 14 00:17:33 Finished compiler/encoders/riscv/proofs                        9m04s   1GB
May 14 00:17:33 Starting compiler/encoders/ag32/proofs
May 14 00:20:11 Finished compiler/encoders/ag32/proofs                         2m38s 967MB
May 14 00:20:11 Starting compiler/backend/x64/proofs
May 14 00:20:40 Finished compiler/backend/x64/proofs                             28s   1GB
May 14 00:20:40 Starting compiler/backend/arm7/proofs
May 14 00:21:13 Finished compiler/backend/arm7/proofs                            33s   1GB
May 14 00:21:13 Starting compiler/backend/arm8/proofs
May 14 00:21:45 Finished compiler/backend/arm8/proofs                            31s   2GB
May 14 00:21:45 Starting compiler/backend/arm8_asl
May 14 00:22:09 Finished compiler/backend/arm8_asl                               23s   1GB
May 14 00:22:09 Starting compiler/backend/mips/proofs
May 14 00:22:41 Finished compiler/backend/mips/proofs                            31s   1GB
May 14 00:22:41 Starting compiler/backend/riscv/proofs
May 14 00:23:14 Finished compiler/backend/riscv/proofs                           32s   2GB
May 14 00:23:14 Starting compiler/backend/ag32/proofs
May 14 00:37:07 Finished compiler/backend/ag32/proofs                         13m52s   4GB
May 14 00:37:07 Starting candle/set-theory
May 14 00:37:47 Finished candle/set-theory                                       39s   1GB
May 14 00:37:47 Starting candle/syntax-lib
May 14 00:37:49 Finished candle/syntax-lib                                        1s  17MB
May 14 00:37:49 Starting candle/standard/syntax
May 14 00:37:59 Finished candle/standard/syntax                                  10s 711MB
May 14 00:37:59 Starting candle/standard/semantics
May 14 00:39:57 Finished candle/standard/semantics                             1m57s   1GB
May 14 00:39:57 Starting candle/standard/monadic
May 14 00:39:59 Finished candle/standard/monadic                                  1s  20MB
May 14 00:39:59 Starting candle/standard/ml_kernel
May 14 00:41:37 Finished candle/standard/ml_kernel                             1m38s   2GB
May 14 00:41:37 Starting candle/overloading/syntax
May 14 00:45:01 Finished candle/overloading/syntax                             3m24s   1GB
May 14 00:45:01 Starting candle/overloading/semantics
May 14 00:57:24 Finished candle/overloading/semantics                         12m22s   2GB
May 14 00:57:24 Starting candle/overloading/monadic
May 14 01:00:04 Finished candle/overloading/monadic                            2m38s   1GB
May 14 01:00:05 Starting candle/overloading/ml_kernel
May 14 01:08:05 Finished candle/overloading/ml_kernel                          8m00s   4GB
May 14 01:08:05 Starting candle/overloading/ml_checker
May 14 01:10:43 Finished candle/overloading/ml_checker                         2m38s   2GB
May 14 01:10:43 Starting candle/prover
May 14 01:20:38 Finished candle/prover                                         9m55s   4GB
May 14 01:20:38 Starting pancake
May 14 01:21:23 Finished pancake                                                 44s 998MB
May 14 01:21:23 Starting pancake/ffi
May 14 01:21:23 Finished pancake/ffi                                              0s  13MB
May 14 01:21:24 Starting pancake/semantics
May 14 01:23:56 Finished pancake/semantics                                     2m32s   1GB
May 14 01:23:56 Starting pancake/proofs
May 14 01:28:03 Finished pancake/proofs                                        4m07s   3GB
May 14 01:28:03 Starting characteristic/examples
May 14 01:29:47 Finished characteristic/examples                               1m44s   3GB
May 14 01:29:47 Starting tutorial/solutions
May 14 01:44:52 Finished tutorial/solutions                                   15m04s   9GB
May 14 01:44:53 Starting translator/monadic/examples
May 14 01:48:58 Finished translator/monadic/examples                           4m05s   2GB
May 14 01:48:58 Starting examples
May 14 02:04:54 Finished examples                                             15m54s   5GB
May 14 02:04:54 Starting examples/compilation/x64
May 14 04:04:42 Finished examples/compilation/x64                           1h59m45s  19GB
May 14 04:04:43 Starting examples/compilation/x64/proofs
May 14 04:07:16 Finished examples/compilation/x64/proofs                       2m32s   4GB
May 14 04:07:16 Starting examples/compilation/ag32
May 14 04:37:49 Finished examples/compilation/ag32                            30m32s   7GB
May 14 04:37:49 Starting examples/compilation/ag32/proofs
May 14 04:38:50 Finished examples/compilation/ag32/proofs                      1m00s   4GB
May 14 04:38:50 Starting examples/compilation/to_word
May 14 04:42:08 Finished examples/compilation/to_word                          3m18s   5GB
May 14 04:42:08 Starting examples/lpr_checker
May 14 04:43:15 Finished examples/lpr_checker                                  1m06s   1GB
May 14 04:43:15 Starting examples/lpr_checker/array
May 14 05:19:53 Finished examples/lpr_checker/array                           36m36s   5GB
May 14 05:19:53 Starting examples/lpr_checker/array/compilation
May 14 06:00:40 Finished examples/lpr_checker/array/compilation               40m46s  23GB
May 14 06:00:40 Starting examples/lpr_checker/array/compilation/proofs
May 14 06:02:14 Finished examples/lpr_checker/array/compilation/proofs         1m34s   7GB
May 14 06:02:14 Starting examples/opentheory
May 14 06:13:18 Finished examples/opentheory                                  11m03s   5GB
May 14 06:13:18 Starting examples/opentheory
May 14 06:13:20 Finished examples/opentheory                                      1s  38MB
May 14 06:13:20 Starting examples/opentheory/compilation
May 14 06:49:50 Finished examples/opentheory/compilation                      36m27s  30GB
May 14 06:49:50 Starting examples/opentheory/compilation/proofs
May 14 06:50:54 Finished examples/opentheory/compilation/proofs                1m04s   5GB
May 14 06:50:54 Starting examples/opentheory/compilation/ag32
May 14 07:23:48 Finished examples/opentheory/compilation/ag32                 32m53s  28GB
May 14 07:23:48 Starting examples/opentheory/compilation/ag32/proofs
May 14 07:25:44 Finished examples/opentheory/compilation/ag32/proofs           1m55s   7GB
May 14 07:25:44 Starting examples/sat_encodings
May 14 07:27:43 Finished examples/sat_encodings                                1m59s 858MB
May 14 07:27:43 Starting examples/sat_encodings/case_studies
May 14 07:29:34 Finished examples/sat_encodings/case_studies                   1m50s   1GB
May 14 07:29:34 Starting examples/sat_encodings/translation
May 14 07:35:46 Finished examples/sat_encodings/translation                    6m12s   3GB
May 14 07:35:46 Starting examples/sat_encodings/translation/compilation
May 14 08:23:03 Finished examples/sat_encodings/translation/compilation       47m15s  22GB
May 14 08:23:03 Starting examples/deflate
May 14 08:24:04 Finished examples/deflate                                      1m00s 854MB
May 14 08:24:04 Starting examples/deflate/translation
May 14 08:25:45 Finished examples/deflate/translation                          1m41s   3GB
May 14 08:25:45 Starting examples/deflate/translation/compilation
May 14 08:45:47 Finished examples/deflate/translation/compilation             20m02s  12GB
May 14 08:45:47 Starting translator/okasaki-examples
May 14 08:51:02 Finished translator/okasaki-examples                           5m14s   2GB
May 14 08:51:02 Starting translator/other-examples
May 14 08:53:45 Finished translator/other-examples                             2m43s   1GB
May 14 08:53:46 Starting compiler/parsing/tests
May 14 08:54:17 Finished compiler/parsing/tests                                  31s 735MB
May 14 08:54:17 Starting compiler/inference/tests
May 14 09:02:33 Finished compiler/inference/tests                              8m15s   5GB
May 14 09:02:33 Starting compiler/printing/test
May 14 09:06:24 Finished compiler/printing/test                                3m50s   3GB
May 14 09:06:24 Starting icing/flover
May 14 09:49:22 Finished icing/flover                                         42m57s   2GB
May 14 09:49:22 Starting icing/
May 14 10:45:27 Finished icing/                                               56m04s   7GB
May 14 10:45:28 Starting icing/examples
May 14 10:46:59 Finished icing/examples                                        1m31s   3GB
May 14 10:46:59 Starting compiler/repl
May 14 10:55:58 Finished compiler/repl                                         8m56s   4GB
May 14 10:55:58 Starting unverified/sexpr-bootstrap/x64/64
May 14 11:09:26 Finished unverified/sexpr-bootstrap/x64/64                    13m25s  16GB
May 14 11:09:26 Starting unverified/sexpr-bootstrap/x64/32
May 14 11:20:20 Finished unverified/sexpr-bootstrap/x64/32                    10m52s  12GB
May 14 11:20:20 Starting compiler/benchmarks
May 14 11:35:39 Finished compiler/benchmarks                                  15m19s   2GB
May 14 11:35:40 Starting compiler/bootstrap/compilation/x64/64
May 14 23:25:34 Finished compiler/bootstrap/compilation/x64/64             11h49m51s  64GB
May 14 23:25:34 Starting compiler/bootstrap/compilation/x64/64/proofs
May 14 23:46:13 Finished compiler/bootstrap/compilation/x64/64/proofs         20m38s  44GB
May 14 23:46:13 Starting compiler/bootstrap/compilation/x64/32
May 15 06:39:42 Finished compiler/bootstrap/compilation/x64/32              6h53m28s  64GB
May 15 06:39:42 Starting compiler/bootstrap/compilation/x64/32/proofs
May 15 06:42:36 Finished compiler/bootstrap/compilation/x64/32/proofs          2m54s  18GB
May 15 06:42:37 Starting compiler/bootstrap/compilation/ag32/32
May 15 13:44:03 Finished compiler/bootstrap/compilation/ag32/32             7h01m24s  63GB
May 15 13:44:03 Starting compiler/bootstrap/compilation/ag32/32/proofs
May 15 13:50:34 Finished compiler/bootstrap/compilation/ag32/32/proofs         6m30s  34GB
May 15 13:50:34 SUCCESS