Job 1944

CakeML:fbd56dc0d32e0e8b24d8ea10dd77112eee529460
  Fix a bunch of real$abs --> realax$abs (also for min, max) [Jun 23 20:53:47]
HOL:3810cf53c6050c5b2748cb042415145bd842957f
  Make parsing in RealField properly independent of context [Jun 21 00:55:21]
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

Jun 23 21:00:48 Claimed job
Jun 23 21:00:52 Reusing HOL
Jun 23 21:01:06 Starting developers
Jun 23 21:01:10 Finished developers                                               4s 147MB
Jun 23 21:01:11 Starting developers/bin
Jun 23 21:01:17 Finished developers/bin                                           6s   1GB
Jun 23 21:01:17 Starting semantics/ffi
Jun 23 21:01:27 Finished semantics/ffi                                            9s 227MB
Jun 23 21:01:27 Starting semantics
Jun 23 21:03:57 Finished semantics                                             2m29s   1GB
Jun 23 21:03:57 Starting semantics/proofs
Jun 23 21:10:57 Finished semantics/proofs                                      6m59s   1GB
Jun 23 21:10:57 Starting semantics/alt_semantics
Jun 23 21:11:25 Finished semantics/alt_semantics                                 27s 527MB
Jun 23 21:11:25 Starting semantics/alt_semantics/proofs
Jun 23 21:22:54 Finished semantics/alt_semantics/proofs                       11m28s   1GB
Jun 23 21:22:54 Starting basis/pure
Jun 23 21:24:01 Finished basis/pure                                            1m06s 933MB
Jun 23 21:24:01 Starting translator
Jun 23 21:27:40 Finished translator                                            3m38s   2GB
Jun 23 21:27:40 Starting compiler/parsing
Jun 23 21:29:05 Finished compiler/parsing                                      1m24s   4GB
Jun 23 21:29:05 Starting characteristic
Jun 23 21:36:07 Finished characteristic                                        7m02s   1GB
Jun 23 21:36:07 Starting translator/monadic
Jun 23 21:38:10 Finished translator/monadic                                    2m02s   1GB
Jun 23 21:38:10 Starting basis
Jun 23 22:29:16 Finished basis                                                51m03s  13GB
Jun 23 22:29:17 Starting compiler/inference
Jun 23 22:30:47 Finished compiler/inference                                    1m30s   1GB
Jun 23 22:30:48 Starting compiler/backend/reg_alloc
Jun 23 22:32:33 Finished compiler/backend/reg_alloc                            1m44s   1GB
Jun 23 22:32:33 Starting compiler/backend/gc
Jun 23 22:37:04 Finished compiler/backend/gc                                   4m30s   2GB
Jun 23 22:37:04 Starting compiler/backend
Jun 23 22:43:16 Finished compiler/backend                                      6m12s   3GB
Jun 23 22:43:16 Starting compiler/encoders/asm
Jun 23 22:43:47 Finished compiler/encoders/asm                                   30s 693MB
Jun 23 22:43:47 Starting compiler/encoders/x64
Jun 23 22:44:17 Finished compiler/encoders/x64                                   29s   1GB
Jun 23 22:44:17 Starting compiler/encoders/arm7
Jun 23 22:45:16 Finished compiler/encoders/arm7                                  58s 841MB
Jun 23 22:45:16 Starting compiler/encoders/arm8
Jun 23 22:45:33 Finished compiler/encoders/arm8                                  16s   1GB
Jun 23 22:45:33 Starting compiler/encoders/arm8_asl
Jun 23 22:48:11 Finished compiler/encoders/arm8_asl                            2m37s   1GB
Jun 23 22:48:11 Starting compiler/encoders/mips
Jun 23 22:48:32 Finished compiler/encoders/mips                                  21s   1GB
Jun 23 22:48:33 Starting compiler/encoders/riscv
Jun 23 22:48:52 Finished compiler/encoders/riscv                                 18s 891MB
Jun 23 22:48:52 Starting compiler/encoders/ag32
Jun 23 22:49:14 Finished compiler/encoders/ag32                                  21s 801MB
Jun 23 22:49:14 Starting compiler/backend/x64
Jun 23 22:49:37 Finished compiler/backend/x64                                    22s   1GB
Jun 23 22:49:37 Starting compiler/backend/arm7
Jun 23 22:50:01 Finished compiler/backend/arm7                                   24s   1GB
Jun 23 22:50:02 Starting compiler/backend/arm8
Jun 23 22:50:24 Finished compiler/backend/arm8                                   22s   1GB
Jun 23 22:50:25 Starting compiler/backend/mips
Jun 23 22:50:47 Finished compiler/backend/mips                                   22s   1GB
Jun 23 22:50:47 Starting compiler/backend/riscv
Jun 23 22:51:10 Finished compiler/backend/riscv                                  22s   1GB
Jun 23 22:51:10 Starting compiler/backend/ag32
Jun 23 22:52:37 Finished compiler/backend/ag32                                 1m26s   1GB
Jun 23 22:52:37 Starting compiler/parsing/proofs
Jun 23 22:56:22 Finished compiler/parsing/proofs                               3m44s   1GB
Jun 23 22:56:22 Starting compiler/inference/proofs
Jun 23 22:59:06 Finished compiler/inference/proofs                             2m43s   1GB
Jun 23 22:59:06 Starting compiler/backend/semantics
Jun 23 23:25:45 Finished compiler/backend/semantics                           26m38s   3GB
Jun 23 23:25:45 Starting compiler/backend/reg_alloc/proofs
Jun 23 23:29:20 Finished compiler/backend/reg_alloc/proofs                     3m34s   1GB
Jun 23 23:29:20 Starting compiler/backend/proofs
Jun 24 00:24:10 Finished compiler/backend/proofs                              54m49s  19GB
Jun 24 00:24:10 Starting compiler/backend/serialiser
Jun 24 00:25:55 Finished compiler/backend/serialiser                           1m44s   2GB
Jun 24 00:25:55 Starting compiler/encoders/x64/proofs
Jun 24 00:35:36 Finished compiler/encoders/x64/proofs                          9m38s   4GB
Jun 24 00:35:36 Starting compiler/encoders/arm7/proofs
Jun 24 00:48:52 Finished compiler/encoders/arm7/proofs                        13m15s   3GB
Jun 24 00:48:52 Starting compiler/encoders/arm8/proofs
Jun 24 00:55:27 Finished compiler/encoders/arm8/proofs                         6m35s   1GB
Jun 24 00:55:28 Starting compiler/encoders/arm8_asl/proofs
Jun 24 01:10:57 Finished compiler/encoders/arm8_asl/proofs                    15m29s   2GB
Jun 24 01:10:58 Starting compiler/encoders/mips/proofs
Jun 24 01:21:10 Finished compiler/encoders/mips/proofs                        10m11s   3GB
Jun 24 01:21:10 Starting compiler/encoders/riscv/proofs
Jun 24 01:30:09 Finished compiler/encoders/riscv/proofs                        8m58s   1GB
Jun 24 01:30:09 Starting compiler/encoders/ag32/proofs
Jun 24 01:32:43 Finished compiler/encoders/ag32/proofs                         2m34s 693MB
Jun 24 01:32:43 Starting compiler/backend/x64/proofs
Jun 24 01:33:13 Finished compiler/backend/x64/proofs                             29s   1GB
Jun 24 01:33:13 Starting compiler/backend/arm7/proofs
Jun 24 01:33:44 Finished compiler/backend/arm7/proofs                            30s   1GB
Jun 24 01:33:44 Starting compiler/backend/arm8/proofs
Jun 24 01:34:13 Finished compiler/backend/arm8/proofs                            29s   1GB
Jun 24 01:34:13 Starting compiler/backend/arm8_asl
Jun 24 01:34:36 Finished compiler/backend/arm8_asl                               22s   1GB
Jun 24 01:34:36 Starting compiler/backend/mips/proofs
Jun 24 01:35:06 Finished compiler/backend/mips/proofs                            29s   1GB
Jun 24 01:35:06 Starting compiler/backend/riscv/proofs
Jun 24 01:35:35 Finished compiler/backend/riscv/proofs                           29s   2GB
Jun 24 01:35:36 Starting compiler/backend/ag32/proofs
Jun 24 01:49:17 Finished compiler/backend/ag32/proofs                         13m41s   2GB
Jun 24 01:49:17 Starting compiler/proofs
Jun 24 01:51:30 Finished compiler/proofs                                       2m12s   3GB
Jun 24 01:51:30 Starting candle/set-theory
Jun 24 01:52:04 Finished candle/set-theory                                       34s   1GB
Jun 24 01:52:05 Starting candle/syntax-lib
Jun 24 01:52:18 Finished candle/syntax-lib                                       13s 680MB
Jun 24 01:52:18 Starting candle/standard/syntax
Jun 24 01:54:22 Finished candle/standard/syntax                                2m03s   1GB
Jun 24 01:54:22 Starting candle/standard/semantics
Jun 24 01:56:11 Finished candle/standard/semantics                             1m49s   1GB
Jun 24 01:56:12 Starting candle/standard/monadic
Jun 24 01:58:07 Finished candle/standard/monadic                               1m55s   1GB
Jun 24 01:58:07 Starting candle/standard/ml_kernel
Jun 24 02:04:29 Finished candle/standard/ml_kernel                             6m21s   3GB
Jun 24 02:04:29 Starting candle/overloading/syntax
Jun 24 02:07:41 Finished candle/overloading/syntax                             3m11s   1GB
Jun 24 02:07:41 Starting candle/overloading/semantics
Jun 24 02:19:30 Finished candle/overloading/semantics                         11m48s   2GB
Jun 24 02:19:30 Starting candle/overloading/monadic
Jun 24 02:22:08 Finished candle/overloading/monadic                            2m37s   1GB
Jun 24 02:22:08 Starting candle/overloading/ml_kernel
Jun 24 02:29:33 Finished candle/overloading/ml_kernel                          7m24s   3GB
Jun 24 02:29:33 Starting candle/overloading/ml_checker
Jun 24 02:31:58 Finished candle/overloading/ml_checker                         2m25s   3GB
Jun 24 02:31:58 Starting candle/prover
Jun 24 02:42:44 Finished candle/prover                                        10m44s   2GB
Jun 24 02:42:44 Starting pancake
Jun 24 02:46:38 Finished pancake                                               3m53s   3GB
Jun 24 02:46:38 Starting pancake/ffi
Jun 24 02:46:38 Finished pancake/ffi                                              0s  35MB
Jun 24 02:46:38 Starting pancake/semantics
Jun 24 02:49:15 Finished pancake/semantics                                     2m36s   1GB
Jun 24 02:49:15 Starting pancake/proofs
Jun 24 03:01:13 Finished pancake/proofs                                       11m57s   7GB
Jun 24 03:01:13 Starting characteristic/examples
Jun 24 03:02:36 Finished characteristic/examples                               1m23s   3GB
Jun 24 03:02:37 Starting tutorial/solutions
Jun 24 03:18:41 Finished tutorial/solutions                                   16m04s   9GB
Jun 24 03:18:42 Starting translator/monadic/examples
Jun 24 03:22:38 Finished translator/monadic/examples                           3m56s   2GB
Jun 24 03:22:38 Starting examples
Jun 24 03:32:29 Finished examples                                              9m51s   4GB
Jun 24 03:32:29 Starting examples/compilation/x64
Jun 24 05:36:31 Finished examples/compilation/x64                           2h03m58s  17GB
Jun 24 05:36:31 Starting examples/compilation/x64/proofs
Jun 24 05:39:00 Finished examples/compilation/x64/proofs                       2m28s   3GB
Jun 24 05:39:00 Starting examples/compilation/ag32
Jun 24 06:12:28 Finished examples/compilation/ag32                            33m27s   8GB
Jun 24 06:12:28 Starting examples/compilation/ag32/proofs
Jun 24 06:13:24 Finished examples/compilation/ag32/proofs                        56s   4GB
Jun 24 06:13:25 Starting examples/lpr_checker
Jun 24 06:14:27 Finished examples/lpr_checker                                  1m02s   1GB
Jun 24 06:14:27 Starting examples/lpr_checker/array
Jun 24 06:47:30 Finished examples/lpr_checker/array                           33m01s   5GB
Jun 24 06:47:30 Starting examples/lpr_checker/array/compilation
Jun 24 07:25:25 Finished examples/lpr_checker/array/compilation               37m55s  27GB
Jun 24 07:25:25 Starting examples/lpr_checker/array/compilation/proofs
Jun 24 07:26:50 Finished examples/lpr_checker/array/compilation/proofs         1m24s   5GB
Jun 24 07:26:50 Starting examples/opentheory
Jun 24 07:37:28 Finished examples/opentheory                                  10m37s   5GB
Jun 24 07:37:28 Starting examples/opentheory
Jun 24 07:37:29 Finished examples/opentheory                                      1s 132MB
Jun 24 07:37:29 Starting examples/opentheory/compilation
Jun 24 08:15:01 Finished examples/opentheory/compilation                      37m27s  29GB
Jun 24 08:15:01 Starting examples/opentheory/compilation/proofs
Jun 24 08:15:58 Finished examples/opentheory/compilation/proofs                  57s   4GB
Jun 24 08:15:59 Starting examples/opentheory/compilation/ag32
Jun 24 08:50:22 Finished examples/opentheory/compilation/ag32                 34m22s  28GB
Jun 24 08:50:22 Starting examples/opentheory/compilation/ag32/proofs
Jun 24 08:52:07 Finished examples/opentheory/compilation/ag32/proofs           1m45s   3GB
Jun 24 08:52:08 Starting examples/sat_encodings
Jun 24 08:54:11 Finished examples/sat_encodings                                2m03s 896MB
Jun 24 08:54:12 Starting examples/sat_encodings/case_studies
Jun 24 08:55:55 Finished examples/sat_encodings/case_studies                   1m43s   1GB
Jun 24 08:55:56 Starting examples/sat_encodings/translation
Jun 24 09:01:51 Finished examples/sat_encodings/translation                    5m55s   5GB
Jun 24 09:01:51 Starting examples/sat_encodings/translation/compilation
Jun 24 09:48:29 Finished examples/sat_encodings/translation/compilation       46m36s  23GB
Jun 24 09:48:29 Starting examples/deflate
Jun 24 09:49:29 Finished examples/deflate                                        59s 848MB
Jun 24 09:49:29 Starting examples/deflate/translation
Jun 24 09:51:00 Finished examples/deflate/translation                          1m30s   3GB
Jun 24 09:51:00 Starting examples/deflate/translation/compilation
Jun 24 10:11:34 Finished examples/deflate/translation/compilation             20m33s  12GB
Jun 24 10:11:34 Starting translator/okasaki-examples
Jun 24 10:16:36 Finished translator/okasaki-examples                           5m01s   1GB
Jun 24 10:16:36 Starting translator/other-examples
Jun 24 10:17:26 Finished translator/other-examples                               49s   1GB
Jun 24 10:17:26 Starting compiler/parsing/tests
Jun 24 10:17:57 Finished compiler/parsing/tests                                  30s 613MB
Jun 24 10:17:57 Starting compiler/inference/tests
Jun 24 10:26:33 Finished compiler/inference/tests                              8m36s   3GB
Jun 24 10:26:33 Starting compiler/printing/test
Jun 24 10:30:22 Finished compiler/printing/test                                3m48s   2GB
Jun 24 10:30:22 Starting icing/flover
Jun 24 11:14:07 Finished icing/flover                                         43m44s   1GB
Jun 24 11:14:08 Starting icing/
Jun 24 12:12:20 Finished icing/                                               58m12s   8GB
Jun 24 12:12:20 Starting icing/examples
Jun 24 12:14:01 Finished icing/examples                                        1m40s   3GB
Jun 24 12:14:01 Starting compiler/repl
Jun 24 12:27:11 Finished compiler/repl                                        13m08s   8GB
Jun 24 12:27:11 Starting compiler/bootstrap/translation
Jun 24 16:39:58 Finished compiler/bootstrap/translation                     4h12m46s  31GB
Jun 24 16:39:58 Starting unverified/sexpr-bootstrap/x64/64
Jun 24 16:51:56 Finished unverified/sexpr-bootstrap/x64/64                    11m56s  12GB
Jun 24 16:51:56 Starting unverified/sexpr-bootstrap/x64/32
Jun 24 17:01:52 Finished unverified/sexpr-bootstrap/x64/32                     9m55s  12GB
Jun 24 17:01:52 Starting compiler/benchmarks
Jun 24 17:02:48 Finished compiler/benchmarks                                     55s 673MB
Jun 24 17:02:49 Starting compiler/bootstrap/compilation/x64/64
Jun 25 03:44:28 Finished compiler/bootstrap/compilation/x64/64             10h41m30s  64GB
Jun 25 03:44:30 Starting compiler/bootstrap/compilation/x64/64/proofs
Jun 25 04:01:37 Finished compiler/bootstrap/compilation/x64/64/proofs         17m07s  18GB
Jun 25 04:01:37 Starting compiler/bootstrap/compilation/x64/32
Jun 25 10:33:09 Finished compiler/bootstrap/compilation/x64/32              6h31m30s  64GB
Jun 25 10:33:09 Starting compiler/bootstrap/compilation/x64/32/proofs
Jun 25 10:35:52 Finished compiler/bootstrap/compilation/x64/32/proofs          2m43s  12GB
Jun 25 10:35:52 Starting compiler/bootstrap/compilation/ag32/32
Jun 25 17:14:25 Finished compiler/bootstrap/compilation/ag32/32             6h38m31s  64GB
Jun 25 17:14:25 Starting compiler/bootstrap/compilation/ag32/32/proofs
Jun 25 17:20:16 Finished compiler/bootstrap/compilation/ag32/32/proofs         5m51s  25GB
Jun 25 17:20:16 SUCCESS