Job 1537

CakeML:13d491ce5cb330bb5243ebe8553c511511374a54
  Add new example (sat_encodings) to build sequence [May 28 20:09:10]
#828 (sat_encodings)
Merging into:e186cc1984bac5cce7c150b458fe1604eece7703
  Fix cost examples [May 21 07:35:10]
HOL:726c826a3afc24a0e7a679e9c686aa25b5acb84a
  Manual, axiomatised bounded-natural functor development [May 27 12:11:23]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

May 28 20:23:15 Claimed job
May 28 20:23:20 Building HOL
May 28 20:39:18 Starting developers
May 28 20:39:23 Finished developers                                               4s 108MB
May 28 20:39:23 Starting developers/bin
May 28 20:39:30 Finished developers/bin                                           7s   1GB
May 28 20:39:30 Starting semantics/ffi
May 28 20:39:42 Finished semantics/ffi                                           11s 248MB
May 28 20:39:42 Starting semantics
May 28 20:41:19 Finished semantics                                             1m36s   1GB
May 28 20:41:20 Starting semantics/proofs
May 28 20:45:13 Finished semantics/proofs                                      3m53s   1GB
May 28 20:45:14 Starting semantics/alt_semantics
May 28 20:45:23 Finished semantics/alt_semantics                                  9s 303MB
May 28 20:45:24 Starting semantics/alt_semantics/proofs
May 28 20:47:47 Finished semantics/alt_semantics/proofs                        2m23s 703MB
May 28 20:47:47 Starting basis/pure
May 28 20:50:53 Finished basis/pure                                            3m05s 923MB
May 28 20:50:53 Starting translator
May 28 20:54:34 Finished translator                                            3m40s   2GB
May 28 20:54:34 Starting compiler/parsing
May 28 20:55:51 Finished compiler/parsing                                      1m16s   2GB
May 28 20:55:51 Starting characteristic
May 28 21:01:48 Finished characteristic                                        5m56s   2GB
May 28 21:01:48 Starting translator/monadic
May 28 21:03:31 Finished translator/monadic                                    1m42s   1GB
May 28 21:03:31 Starting basis
May 28 21:51:01 Finished basis                                                47m29s  14GB
May 28 21:51:01 Starting compiler/inference
May 28 21:52:19 Finished compiler/inference                                    1m17s   1GB
May 28 21:52:20 Starting compiler/backend/reg_alloc
May 28 21:53:31 Finished compiler/backend/reg_alloc                            1m10s   1GB
May 28 21:53:31 Starting compiler/backend/gc
May 28 21:57:24 Finished compiler/backend/gc                                   3m53s   2GB
May 28 21:57:25 Starting compiler/backend
May 31 15:17:36 Resuming compiler/backend
May 31 15:17:37 Finished compiler/backend                                         1s  17MB
May 31 15:17:38 Starting compiler/encoders/asm
May 31 15:18:01 Finished compiler/encoders/asm                                   22s 681MB
May 31 15:18:01 Starting compiler/encoders/x64
May 31 15:19:08 Finished compiler/encoders/x64                                 1m06s   1GB
May 31 15:19:08 Starting compiler/encoders/arm7
May 31 15:21:20 Finished compiler/encoders/arm7                                2m12s   1GB
May 31 15:21:20 Starting compiler/encoders/arm8
May 31 15:22:01 Finished compiler/encoders/arm8                                  40s 986MB
May 31 15:22:01 Starting compiler/encoders/mips
May 31 15:23:38 Finished compiler/encoders/mips                                1m36s   1GB
May 31 15:23:38 Starting compiler/encoders/riscv
May 31 15:25:34 Finished compiler/encoders/riscv                               1m55s   1GB
May 31 15:25:34 Starting compiler/encoders/ag32
May 31 15:25:53 Finished compiler/encoders/ag32                                  18s 847MB
May 31 15:25:54 Starting compiler/backend/x64
May 31 15:26:13 Finished compiler/backend/x64                                    19s   1GB
May 31 15:26:14 Starting compiler/backend/arm7
May 31 15:26:35 Finished compiler/backend/arm7                                   21s   1GB
May 31 15:26:36 Starting compiler/backend/arm8
May 31 15:26:56 Finished compiler/backend/arm8                                   20s   1GB
May 31 15:26:56 Starting compiler/backend/mips
May 31 15:27:17 Finished compiler/backend/mips                                   20s   1GB
May 31 15:27:17 Starting compiler/backend/riscv
May 31 15:27:38 Finished compiler/backend/riscv                                  20s   1GB
May 31 15:27:38 Starting compiler/backend/ag32
May 31 15:28:52 Finished compiler/backend/ag32                                 1m13s   1GB
May 31 15:28:52 Starting compiler/parsing/proofs
May 31 15:34:59 Finished compiler/parsing/proofs                               6m06s   1GB
May 31 15:34:59 Starting compiler/inference/proofs
May 31 15:37:38 Finished compiler/inference/proofs                             2m38s   1GB
May 31 15:37:38 Starting compiler/backend/semantics
May 31 16:11:21 Finished compiler/backend/semantics                           33m42s   2GB
May 31 16:11:21 Starting compiler/backend/reg_alloc/proofs
May 31 16:15:14 Finished compiler/backend/reg_alloc/proofs                     3m52s 798MB
May 31 16:15:15 Starting compiler/backend/proofs
May 31 17:14:40 Finished compiler/backend/proofs                              59m24s  14GB
May 31 17:14:40 Starting compiler/encoders/x64/proofs
May 31 17:25:03 Finished compiler/encoders/x64/proofs                         10m23s   5GB
May 31 17:25:03 Starting compiler/encoders/arm7/proofs
May 31 17:39:33 Finished compiler/encoders/arm7/proofs                        14m29s   3GB
May 31 17:39:33 Starting compiler/encoders/arm8/proofs
May 31 17:47:00 Finished compiler/encoders/arm8/proofs                         7m26s   1GB
May 31 17:47:00 Starting compiler/encoders/mips/proofs
May 31 17:57:37 Finished compiler/encoders/mips/proofs                        10m37s   3GB
May 31 17:57:38 Starting compiler/encoders/riscv/proofs
May 31 18:07:08 Finished compiler/encoders/riscv/proofs                        9m29s   1GB
May 31 18:07:08 Starting compiler/encoders/ag32/proofs
May 31 18:09:57 Finished compiler/encoders/ag32/proofs                         2m49s 723MB
May 31 18:09:58 Starting compiler/backend/x64/proofs
May 31 18:10:21 Finished compiler/backend/x64/proofs                             22s   1GB
May 31 18:10:21 Starting compiler/backend/arm7/proofs
May 31 18:10:45 Finished compiler/backend/arm7/proofs                            23s   1GB
May 31 18:10:45 Starting compiler/backend/arm8/proofs
May 31 18:11:09 Finished compiler/backend/arm8/proofs                            23s   1GB
May 31 18:11:10 Starting compiler/backend/mips/proofs
May 31 18:11:33 Finished compiler/backend/mips/proofs                            22s   1GB
May 31 18:11:33 Starting compiler/backend/riscv/proofs
May 31 18:11:56 Finished compiler/backend/riscv/proofs                           22s   1GB
May 31 18:11:56 Starting compiler/backend/ag32/proofs
May 31 18:25:59 Finished compiler/backend/ag32/proofs                         14m02s   2GB
May 31 18:25:59 Starting compiler/proofs
May 31 18:28:01 Finished compiler/proofs                                       2m01s   3GB
May 31 18:28:01 Starting candle/set-theory
May 31 18:28:31 Finished candle/set-theory                                       29s 697MB
May 31 18:28:31 Starting candle/syntax-lib
May 31 18:28:43 Finished candle/syntax-lib                                       10s 458MB
May 31 18:28:43 Starting candle/standard/syntax
May 31 18:30:40 Finished candle/standard/syntax                                1m56s 938MB
May 31 18:30:40 Starting candle/standard/semantics
May 31 18:32:28 Finished candle/standard/semantics                             1m48s   1GB
May 31 18:32:29 Starting candle/standard/monadic
May 31 18:34:20 Finished candle/standard/monadic                               1m51s   1GB
May 31 18:34:20 Starting candle/standard/ml_kernel
May 31 18:40:23 Finished candle/standard/ml_kernel                             6m02s   5GB
May 31 18:40:23 Starting candle/overloading/syntax
May 31 18:43:43 Finished candle/overloading/syntax                             3m20s 909MB
May 31 18:43:43 Starting candle/overloading/semantics
May 31 18:56:36 Finished candle/overloading/semantics                         12m52s   3GB
May 31 18:56:37 Starting characteristic/examples
May 31 18:58:00 Finished characteristic/examples                               1m23s   2GB
May 31 18:58:01 Starting tutorial/solutions
May 31 19:14:03 Finished tutorial/solutions                                   16m02s   8GB
May 31 19:14:03 Starting translator/monadic/examples
May 31 19:17:32 Finished translator/monadic/examples                           3m28s   3GB
May 31 19:17:33 Starting examples
May 31 19:26:38 Finished examples                                              9m05s   3GB
May 31 19:26:38 Starting examples/compilation/x64
May 31 21:58:13 Finished examples/compilation/x64                           2h31m34s  15GB
May 31 21:58:13 Starting examples/compilation/x64/proofs
May 31 22:00:19 Finished examples/compilation/x64/proofs                       2m05s   3GB
May 31 22:00:20 Starting examples/compilation/ag32
May 31 22:35:36 Finished examples/compilation/ag32                            35m16s   7GB
May 31 22:35:37 Starting examples/compilation/ag32/proofs
May 31 22:36:28 Finished examples/compilation/ag32/proofs                        51s   4GB
May 31 22:36:28 Starting examples/cost
May 31 23:35:15 Finished examples/cost                                        58m46s   9GB
May 31 23:35:15 Starting examples/lpr_checker
May 31 23:39:22 Finished examples/lpr_checker                                  4m07s   2GB
May 31 23:39:23 Starting examples/lpr_checker/compilation
May 31 23:58:42 Finished examples/lpr_checker/compilation                     19m18s  10GB
May 31 23:58:42 Starting examples/lpr_checker/compilation/proofs
May 31 23:59:28 Finished examples/lpr_checker/compilation/proofs                 46s   2GB
May 31 23:59:29 Starting examples/lpr_checker/array
Jun 01 00:15:19 Finished examples/lpr_checker/array                           15m50s   6GB
Jun 01 00:15:19 Starting examples/lpr_checker/array/compilation
Jun 01 00:36:28 Finished examples/lpr_checker/array/compilation               21m08s  11GB
Jun 01 00:36:28 Starting examples/lpr_checker/array/compilation/proofs
Jun 01 00:37:19 Finished examples/lpr_checker/array/compilation/proofs           50s   4GB
Jun 01 00:37:20 Starting examples/opentheory
Jun 01 00:47:52 Finished examples/opentheory                                  10m32s   6GB
Jun 01 00:47:52 Starting examples/opentheory
Jun 01 00:47:54 Finished examples/opentheory                                      1s  17MB
Jun 01 00:47:54 Starting examples/opentheory/compilation
Jun 01 01:21:39 Finished examples/opentheory/compilation                      33m44s  17GB
Jun 01 01:21:39 Starting examples/opentheory/compilation/proofs
Jun 01 01:22:20 Finished examples/opentheory/compilation/proofs                  40s   2GB
Jun 01 01:22:20 Starting examples/opentheory/compilation/ag32
Jun 01 01:57:43 Finished examples/opentheory/compilation/ag32                 35m22s  16GB
Jun 01 01:57:44 Starting examples/opentheory/compilation/ag32/proofs
Jun 01 01:59:23 Finished examples/opentheory/compilation/ag32/proofs           1m38s   5GB
Jun 01 01:59:23 Starting examples/sat_encodings
Jun 01 02:01:15 Finished examples/sat_encodings                                1m51s 827MB
Jun 01 02:01:15 Starting examples/sat_encodings/case_studies
Jun 01 02:06:05 Finished examples/sat_encodings/case_studies                   4m50s 738MB
Jun 01 02:06:05 Starting examples/sat_encodings/translation
Jun 01 02:12:34 Finished examples/sat_encodings/translation                    6m27s   3GB
Jun 01 02:12:34 Starting examples/sat_encodings/translation/compilation
Jun 01 02:58:28 Finished examples/sat_encodings/translation/compilation       45m53s  11GB
Jun 01 02:58:28 Starting translator/okasaki-examples
Jun 01 03:03:14 Finished translator/okasaki-examples                           4m45s   1GB
Jun 01 03:03:14 Starting translator/other-examples
Jun 01 03:05:27 Finished translator/other-examples                             2m12s   1GB
Jun 01 03:05:27 Starting compiler/parsing/tests
Jun 01 03:05:54 Finished compiler/parsing/tests                                  26s 628MB
Jun 01 03:05:54 Starting compiler/inference/tests
Jun 01 03:14:07 Finished compiler/inference/tests                              8m12s   3GB
Jun 01 03:14:07 Starting compiler/bootstrap/translation
Jun 01 06:01:07 Finished compiler/bootstrap/translation                     2h46m59s  26GB
Jun 01 06:01:07 Starting unverified/sexpr-bootstrap/x64/64
Jun 01 06:12:47 Finished unverified/sexpr-bootstrap/x64/64                    11m39s   8GB
Jun 01 06:12:47 Starting unverified/sexpr-bootstrap/x64/32
Jun 01 06:22:44 Finished unverified/sexpr-bootstrap/x64/32                     9m56s   8GB
Jun 01 06:22:44 Starting compiler/benchmarks
Jun 01 06:22:46 Finished compiler/benchmarks                                      1s  23MB
Jun 01 06:22:47 Starting compiler/bootstrap/compilation/x64/64
Jun 01 19:03:19 Finished compiler/bootstrap/compilation/x64/64             12h40m31s  64GB
Jun 01 19:03:19 Starting compiler/bootstrap/compilation/x64/64/proofs
Jun 01 19:06:24 Finished compiler/bootstrap/compilation/x64/64/proofs          3m05s  12GB
Jun 01 19:06:24 Starting compiler/bootstrap/compilation/x64/32
Jun 02 06:37:05 Finished compiler/bootstrap/compilation/x64/32             11h30m39s  64GB
Jun 02 06:37:05 Starting compiler/bootstrap/compilation/x64/32/proofs
Jun 02 06:39:55 Finished compiler/bootstrap/compilation/x64/32/proofs          2m49s  11GB
Jun 02 06:39:55 Starting compiler/bootstrap/compilation/ag32/32
Jun 02 18:39:20 Finished compiler/bootstrap/compilation/ag32/32            11h59m25s  64GB
Jun 02 18:39:21 Starting compiler/bootstrap/compilation/ag32/32/proofs
Jun 02 19:00:07 Finished compiler/bootstrap/compilation/ag32/32/proofs        20m45s  18GB
Jun 02 19:00:07 SUCCESS