Job 2536

CakeML:680c4514fe31d464bf96f1bb4506c9fda73464d5
  Correct for actual type inference output [Aug 07 09:28:50]
#1034 (set-module)
Merging into:5aca741913e58d680b89a935bec2fb34bf837c4c
  Merge pull request #1031 from talsewell/pancake_mul_to_exp [Aug 07 17:05:52]
HOL:37990a0757640901f13b89fb0114ac3aa2d5e064
  Fix issues simplifying and evaluating {NUM,INT}_{FLOOR,CEILING} [Aug 06 07:52:03]
Machine:lammmington

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