Job 2543

CakeML:ae3e90d1273790ae01f404316c1d547a3053c15a
  Merge pull request #1034 from CakeML/set-module [Aug 09 11:01:51]
HOL:37990a0757640901f13b89fb0114ac3aa2d5e064
  Fix issues simplifying and evaluating {NUM,INT}_{FLOOR,CEILING} [Aug 06 07:52:03]
Machine:pavlova
Artefacts:cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz
cake-arm8-64.tar.gz
cake-x64-32.tar.gz

Aug 10 00:04:48 Claimed job
Aug 10 00:04:52 Reusing HOL
Aug 10 00:05:03 Starting developers
Aug 10 00:05:06 Finished developers                                               2s 215MB
Aug 10 00:05:07 Starting developers/bin
Aug 10 00:05:17 Finished developers/bin                                           9s   1GB
Aug 10 00:05:18 Starting compiler/proofs
Aug 10 01:57:30 Finished compiler/proofs                                    1h52m11s  42GB
Aug 10 01:57:31 Starting compiler/bootstrap/translation
Aug 10 10:42:37 Finished compiler/bootstrap/translation                     8h45m04s  77GB
Aug 10 10:42:38 Starting semantics/ffi
Aug 10 10:42:47 Finished semantics/ffi                                            7s 646MB
Aug 10 10:42:48 Starting semantics
Aug 10 10:42:49 Finished semantics                                                0s  70MB
Aug 10 10:42:50 Starting semantics/proofs
Aug 10 10:43:28 Finished semantics/proofs                                        36s   2GB
Aug 10 10:43:28 Starting semantics/alt_semantics
Aug 10 10:44:16 Finished semantics/alt_semantics                                 46s   1GB
Aug 10 10:44:17 Starting semantics/alt_semantics/proofs
Aug 10 10:55:33 Finished semantics/alt_semantics/proofs                       11m14s   3GB
Aug 10 10:55:34 Starting basis/pure
Aug 10 10:55:35 Finished basis/pure                                               0s  71MB
Aug 10 10:55:36 Starting translator
Aug 10 10:57:22 Finished translator                                            1m45s   3GB
Aug 10 10:57:23 Starting compiler/parsing
Aug 10 10:57:25 Finished compiler/parsing                                         0s  73MB
Aug 10 10:57:26 Starting characteristic
Aug 10 10:57:27 Finished characteristic                                           0s  94MB
Aug 10 10:57:28 Starting translator/monadic
Aug 10 10:57:30 Finished translator/monadic                                       0s 101MB
Aug 10 10:57:30 Starting basis
Aug 10 11:01:09 Finished basis                                                 3m38s   5GB
Aug 10 11:01:10 Starting compiler/inference
Aug 10 11:01:12 Finished compiler/inference                                       0s  93MB
Aug 10 11:01:13 Starting compiler/backend/reg_alloc
Aug 10 11:01:14 Finished compiler/backend/reg_alloc                               0s  69MB
Aug 10 11:01:15 Starting compiler/backend/gc
Aug 10 11:01:17 Finished compiler/backend/gc                                      0s 138MB
Aug 10 11:01:18 Starting compiler/backend
Aug 10 11:01:37 Finished compiler/backend                                        18s   1GB
Aug 10 11:01:38 Starting compiler/encoders/asm
Aug 10 11:01:40 Finished compiler/encoders/asm                                    0s  91MB
Aug 10 11:01:41 Starting compiler/encoders/x64
Aug 10 11:01:42 Finished compiler/encoders/x64                                    0s  96MB
Aug 10 11:01:43 Starting compiler/encoders/arm7
Aug 10 11:01:44 Finished compiler/encoders/arm7                                   0s 102MB
Aug 10 11:01:45 Starting compiler/encoders/arm8
Aug 10 11:01:47 Finished compiler/encoders/arm8                                   0s 107MB
Aug 10 11:01:48 Starting compiler/encoders/arm8_asl
Aug 10 11:04:01 Finished compiler/encoders/arm8_asl                            2m12s   1GB
Aug 10 11:04:02 Starting compiler/encoders/mips
Aug 10 11:04:04 Finished compiler/encoders/mips                                   0s 106MB
Aug 10 11:04:04 Starting compiler/encoders/riscv
Aug 10 11:04:06 Finished compiler/encoders/riscv                                  0s 103MB
Aug 10 11:04:07 Starting compiler/encoders/ag32
Aug 10 11:04:08 Finished compiler/encoders/ag32                                   0s  98MB
Aug 10 11:04:09 Starting compiler/backend/x64
Aug 10 11:04:11 Finished compiler/backend/x64                                     0s 137MB
Aug 10 11:04:12 Starting compiler/backend/arm7
Aug 10 11:04:14 Finished compiler/backend/arm7                                    0s 137MB
Aug 10 11:04:15 Starting compiler/backend/arm8
Aug 10 11:04:16 Finished compiler/backend/arm8                                    0s 137MB
Aug 10 11:04:17 Starting compiler/backend/mips
Aug 10 11:04:19 Finished compiler/backend/mips                                    0s 137MB
Aug 10 11:04:20 Starting compiler/backend/riscv
Aug 10 11:04:22 Finished compiler/backend/riscv                                   0s 137MB
Aug 10 11:04:23 Starting compiler/backend/ag32
Aug 10 11:05:45 Finished compiler/backend/ag32                                 1m21s   2GB
Aug 10 11:05:46 Starting compiler/parsing/proofs
Aug 10 11:05:47 Finished compiler/parsing/proofs                                  0s  74MB
Aug 10 11:05:48 Starting compiler/inference/proofs
Aug 10 11:05:49 Finished compiler/inference/proofs                                0s  96MB
Aug 10 11:05:50 Starting compiler/backend/semantics
Aug 10 11:09:45 Finished compiler/backend/semantics                            3m54s   4GB
Aug 10 11:09:46 Starting compiler/backend/reg_alloc/proofs
Aug 10 11:09:48 Finished compiler/backend/reg_alloc/proofs                        0s  93MB
Aug 10 11:09:49 Starting compiler/backend/proofs
Aug 10 11:10:55 Finished compiler/backend/proofs                               1m04s   3GB
Aug 10 11:10:55 Starting compiler/backend/serialiser
Aug 10 11:10:57 Finished compiler/backend/serialiser                              0s 148MB
Aug 10 11:10:58 Starting compiler/encoders/x64/proofs
Aug 10 11:20:30 Finished compiler/encoders/x64/proofs                          9m30s   5GB
Aug 10 11:20:31 Starting compiler/encoders/arm7/proofs
Aug 10 11:33:25 Finished compiler/encoders/arm7/proofs                        12m53s   8GB
Aug 10 11:33:26 Starting compiler/encoders/arm8/proofs
Aug 10 11:40:20 Finished compiler/encoders/arm8/proofs                         6m53s   5GB
Aug 10 11:40:21 Starting compiler/encoders/arm8_asl/proofs
Aug 10 11:54:17 Finished compiler/encoders/arm8_asl/proofs                    13m54s   4GB
Aug 10 11:54:18 Starting compiler/encoders/mips/proofs
Aug 10 12:04:44 Finished compiler/encoders/mips/proofs                        10m25s   8GB
Aug 10 12:04:45 Starting compiler/encoders/riscv/proofs
Aug 10 12:13:21 Finished compiler/encoders/riscv/proofs                        8m34s   6GB
Aug 10 12:13:22 Starting compiler/encoders/ag32/proofs
Aug 10 12:15:46 Finished compiler/encoders/ag32/proofs                         2m23s   2GB
Aug 10 12:15:47 Starting compiler/backend/x64/proofs
Aug 10 12:16:29 Finished compiler/backend/x64/proofs                             41s   3GB
Aug 10 12:16:30 Starting compiler/backend/arm7/proofs
Aug 10 12:17:16 Finished compiler/backend/arm7/proofs                            44s   2GB
Aug 10 12:17:16 Starting compiler/backend/arm8/proofs
Aug 10 12:17:59 Finished compiler/backend/arm8/proofs                            41s   3GB
Aug 10 12:18:00 Starting compiler/backend/arm8_asl
Aug 10 12:18:30 Finished compiler/backend/arm8_asl                               28s   2GB
Aug 10 12:18:30 Starting compiler/backend/mips/proofs
Aug 10 12:19:18 Finished compiler/backend/mips/proofs                            46s   4GB
Aug 10 12:19:19 Starting compiler/backend/riscv/proofs
Aug 10 12:20:12 Finished compiler/backend/riscv/proofs                           52s   3GB
Aug 10 12:20:13 Starting compiler/backend/ag32/proofs
Aug 10 12:34:49 Finished compiler/backend/ag32/proofs                         14m34s   6GB
Aug 10 12:34:50 Starting compiler/backend/cv_compute
Aug 10 12:36:34 Finished compiler/backend/cv_compute                           1m42s   4GB
Aug 10 12:36:35 Starting cv_translator
Aug 10 12:55:48 Finished cv_translator                                        19m12s  13GB
Aug 10 12:55:49 Starting candle/set-theory
Aug 10 12:56:37 Finished candle/set-theory                                       47s   1GB
Aug 10 12:56:38 Starting candle/syntax-lib
Aug 10 12:56:40 Finished candle/syntax-lib                                        0s  75MB
Aug 10 12:56:41 Starting candle/standard/syntax
Aug 10 12:57:00 Finished candle/standard/syntax                                  18s   1GB
Aug 10 12:57:01 Starting candle/standard/semantics
Aug 10 12:59:40 Finished candle/standard/semantics                             2m38s   3GB
Aug 10 12:59:41 Starting candle/standard/monadic
Aug 10 12:59:42 Finished candle/standard/monadic                                  0s 107MB
Aug 10 12:59:43 Starting candle/standard/ml_kernel
Aug 10 13:01:44 Finished candle/standard/ml_kernel                             1m59s   4GB
Aug 10 13:01:45 Starting candle/overloading/syntax
Aug 10 13:05:20 Finished candle/overloading/syntax                             3m34s   3GB
Aug 10 13:05:21 Starting candle/overloading/semantics
Aug 10 13:16:42 Finished candle/overloading/semantics                         11m20s   5GB
Aug 10 13:16:43 Starting candle/overloading/monadic
Aug 10 13:19:19 Finished candle/overloading/monadic                            2m35s   3GB
Aug 10 13:19:20 Starting candle/overloading/ml_kernel
Aug 10 13:27:06 Finished candle/overloading/ml_kernel                          7m45s   6GB
Aug 10 13:27:07 Starting candle/overloading/ml_checker
Aug 10 13:29:47 Finished candle/overloading/ml_checker                         2m38s   7GB
Aug 10 13:29:47 Starting candle/prover
Aug 10 13:39:59 Finished candle/prover                                        10m10s   5GB
Aug 10 13:40:00 Starting pancake
Aug 10 13:41:06 Finished pancake                                               1m04s   1GB
Aug 10 13:41:06 Starting pancake/ffi
Aug 10 13:41:07 Finished pancake/ffi                                              0s  23MB
Aug 10 13:41:08 Starting pancake/semantics
Aug 10 13:43:50 Finished pancake/semantics                                     2m40s   2GB
Aug 10 13:43:51 Starting pancake/parser
Aug 10 13:44:26 Finished pancake/parser                                          34s   2GB
Aug 10 13:44:27 Starting pancake/proofs
Aug 10 14:15:43 Finished pancake/proofs                                       31m15s   9GB
Aug 10 14:15:44 Starting characteristic/examples
Aug 10 14:17:22 Finished characteristic/examples                               1m37s   6GB
Aug 10 14:17:23 Starting tutorial/solutions
Aug 10 14:20:03 Finished tutorial/solutions                                    2m39s   5GB
Aug 10 14:20:04 Starting translator/monadic/examples
Aug 10 14:24:03 Finished translator/monadic/examples                           3m57s   5GB
Aug 10 14:24:03 Starting examples
Aug 10 14:38:33 Finished examples                                             14m28s   8GB
Aug 10 14:38:34 Starting examples/compilation/x64
Aug 10 14:47:58 Finished examples/compilation/x64                              9m23s   7GB
Aug 10 14:47:59 Starting examples/compilation/x64/proofs
Aug 10 14:52:35 Finished examples/compilation/x64/proofs                       4m35s   7GB
Aug 10 14:52:36 Starting examples/compilation/ag32
Aug 10 14:55:18 Finished examples/compilation/ag32                             2m41s   5GB
Aug 10 14:55:19 Starting examples/compilation/ag32/proofs
Aug 10 14:56:58 Finished examples/compilation/ag32/proofs                      1m38s  10GB
Aug 10 14:56:59 Starting examples/compilation/to_word
Aug 10 15:01:03 Finished examples/compilation/to_word                          4m03s  11GB
Aug 10 15:01:04 Starting examples/lpr_checker
Aug 10 15:02:25 Finished examples/lpr_checker                                  1m20s   2GB
Aug 10 15:02:26 Starting examples/lpr_checker/array
Aug 10 15:31:47 Finished examples/lpr_checker/array                           29m20s  26GB
Aug 10 15:31:48 Starting examples/lpr_checker/array/compilation
Aug 10 15:34:24 Finished examples/lpr_checker/array/compilation                2m34s   9GB
Aug 10 15:34:24 Starting examples/lpr_checker/array/compilation/proofs
Aug 10 15:36:25 Finished examples/lpr_checker/array/compilation/proofs         1m59s   8GB
Aug 10 15:36:26 Starting examples/lpr_checker/array/compilation/proofsARM8
Aug 10 15:38:16 Finished examples/lpr_checker/array/compilation/proofsARM8     1m49s   9GB
Aug 10 15:38:16 Starting examples/xlrup_checker
Aug 10 15:39:32 Finished examples/xlrup_checker                                1m14s   2GB
Aug 10 15:39:33 Starting examples/xlrup_checker/array
Aug 10 15:55:03 Finished examples/xlrup_checker/array                         15m29s   6GB
Aug 10 15:55:04 Starting examples/xlrup_checker/array/compilation
Aug 10 15:56:34 Finished examples/xlrup_checker/array/compilation              1m28s   7GB
Aug 10 15:56:34 Starting examples/xlrup_checker/array/compilation/proofs
Aug 10 15:58:26 Finished examples/xlrup_checker/array/compilation/proofs       1m50s   5GB
Aug 10 15:58:27 Starting examples/pseudo_bool
Aug 10 16:00:38 Finished examples/pseudo_bool                                  2m10s   2GB
Aug 10 16:00:39 Starting examples/pseudo_bool/cnf_encoding
Aug 10 16:01:18 Finished examples/pseudo_bool/cnf_encoding                       38s   1GB
Aug 10 16:01:19 Starting examples/pseudo_bool/graph_encoding
Aug 10 16:02:12 Finished examples/pseudo_bool/graph_encoding                     52s   1GB
Aug 10 16:02:13 Starting examples/pseudo_bool/array
Aug 10 17:07:46 Finished examples/pseudo_bool/array                         1h05m31s  29GB
Aug 10 17:07:47 Starting examples/pseudo_bool/array/compilation
Aug 10 17:21:01 Finished examples/pseudo_bool/array/compilation               13m13s  28GB
Aug 10 17:21:02 Starting examples/pseudo_bool/array/compilation/proofs
Aug 10 17:25:00 Finished examples/pseudo_bool/array/compilation/proofs         3m57s   9GB
Aug 10 17:25:01 Starting examples/pseudo_bool/array/compilation/proofsARM8
Aug 10 17:26:54 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m52s   9GB
Aug 10 17:26:55 Starting examples/opentheory
Aug 10 17:38:00 Finished examples/opentheory                                  11m04s   8GB
Aug 10 17:38:01 Starting examples/opentheory
Aug 10 17:38:03 Finished examples/opentheory                                      0s 134MB
Aug 10 17:38:04 Starting examples/opentheory/compilation
Aug 10 17:40:16 Finished examples/opentheory/compilation                       2m11s   6GB
Aug 10 17:40:17 Starting examples/opentheory/compilation/proofs
Aug 10 17:42:04 Finished examples/opentheory/compilation/proofs                1m46s   8GB
Aug 10 17:42:05 Starting examples/opentheory/compilation/ag32
Aug 10 17:44:14 Finished examples/opentheory/compilation/ag32                  2m07s   9GB
Aug 10 17:44:14 Starting examples/opentheory/compilation/ag32/proofs
Aug 10 17:46:36 Finished examples/opentheory/compilation/ag32/proofs           2m20s  13GB
Aug 10 17:46:37 Starting examples/sat_encodings
Aug 10 17:49:34 Finished examples/sat_encodings                                2m55s   2GB
Aug 10 17:49:34 Starting examples/sat_encodings/case_studies
Aug 10 17:51:42 Finished examples/sat_encodings/case_studies                   2m06s   2GB
Aug 10 17:51:43 Starting examples/sat_encodings/translation
Aug 10 17:58:13 Finished examples/sat_encodings/translation                    6m29s   8GB
Aug 10 17:58:14 Starting examples/sat_encodings/translation/compilation
Aug 10 18:00:43 Finished examples/sat_encodings/translation/compilation        2m28s   7GB
Aug 10 18:00:44 Starting examples/deflate
Aug 10 18:02:08 Finished examples/deflate                                      1m22s   1GB
Aug 10 18:02:09 Starting examples/deflate/translation
Aug 10 18:03:52 Finished examples/deflate/translation                          1m42s   7GB
Aug 10 18:03:53 Starting examples/deflate/translation/compilation
Aug 10 18:05:00 Finished examples/deflate/translation/compilation              1m06s   5GB
Aug 10 18:05:01 Starting examples/vipr
Aug 10 18:09:22 Finished examples/vipr                                         4m19s   8GB
Aug 10 18:09:23 Starting examples/vipr/compilation
Aug 10 18:10:39 Finished examples/vipr/compilation                             1m15s   6GB
Aug 10 18:10:40 Starting translator/okasaki-examples
Aug 10 18:15:55 Finished translator/okasaki-examples                           5m14s   4GB
Aug 10 18:15:56 Starting translator/other-examples
Aug 10 18:17:14 Finished translator/other-examples                             1m17s   3GB
Aug 10 18:17:15 Starting compiler/parsing/tests
Aug 10 18:17:53 Finished compiler/parsing/tests                                  37s   2GB
Aug 10 18:17:54 Starting compiler/inference/tests
Aug 10 18:18:39 Finished compiler/inference/tests                                43s   3GB
Aug 10 18:18:40 Starting compiler/printing/test
Aug 10 18:20:15 Finished compiler/printing/test                                1m34s   6GB
Aug 10 18:20:16 Starting icing/flover
Aug 10 18:57:10 Finished icing/flover                                         36m52s   4GB
Aug 10 18:57:11 Starting icing/
Aug 10 19:25:12 Finished icing/                                               28m00s   5GB
Aug 10 19:25:13 Starting icing/examples
Aug 10 19:27:00 Finished icing/examples                                        1m46s   9GB
Aug 10 19:27:01 Starting compiler/repl
Aug 10 19:35:53 Finished compiler/repl                                         8m51s   8GB
Aug 10 19:35:54 Starting unverified/sexpr-bootstrap/x64/64
Aug 10 19:49:30 Finished unverified/sexpr-bootstrap/x64/64                    13m10s  19GB
Aug 10 19:49:31 Starting unverified/sexpr-bootstrap/x64/32
Aug 10 20:00:15 Finished unverified/sexpr-bootstrap/x64/32                    10m23s  14GB
Aug 10 20:00:16 Starting compiler/benchmarks
Aug 10 20:01:01 Finished compiler/benchmarks                                     43s 713MB
Aug 10 20:01:02 Starting compiler/bootstrap/compilation/x64/64
Aug 10 20:42:54 Finished compiler/bootstrap/compilation/x64/64                41m38s 118GB
Aug 10 20:42:55 Starting compiler/bootstrap/compilation/x64/64/proofs
Aug 10 21:06:42 Finished compiler/bootstrap/compilation/x64/64/proofs         23m46s  54GB
Aug 10 21:06:43 Starting compiler/bootstrap/compilation/x64/32
Aug 10 21:45:14 Finished compiler/bootstrap/compilation/x64/32                38m22s 101GB
Aug 10 21:45:15 Starting compiler/bootstrap/compilation/x64/32/proofs
Aug 10 21:50:10 Finished compiler/bootstrap/compilation/x64/32/proofs          4m54s  27GB
Aug 10 21:50:11 Starting compiler/bootstrap/compilation/arm8/64
Aug 10 22:45:36 Finished compiler/bootstrap/compilation/arm8/64               55m16s 138GB
Aug 10 22:45:37 Starting compiler/bootstrap/compilation/arm8/64/proofs
Aug 10 22:51:08 Finished compiler/bootstrap/compilation/arm8/64/proofs         5m29s  31GB
Aug 10 22:51:09 Starting compiler/bootstrap/compilation/ag32/32
Aug 10 23:44:36 Finished compiler/bootstrap/compilation/ag32/32               53m26s  90GB
Aug 10 23:44:37 Starting compiler/bootstrap/compilation/ag32/32/proofs
Aug 10 23:50:22 Finished compiler/bootstrap/compilation/ag32/32/proofs         5m43s  30GB
Aug 10 23:50:23 SUCCESS