Job 1539

CakeML:537411958b1b5402c5d58912a95722c326f47689
  Tidy up SAT encoder translations [Jun 03 20:33:54]
#828 (sat_encodings)
Merging into:e186cc1984bac5cce7c150b458fe1604eece7703
  Fix cost examples [May 21 07:35:10]
HOL:3309c51ff0fc07e1ac1b254b4206400f551c96bd
  Polish bnfAlgebra, including moving some results to core theories [May 30 11:35:25]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Jun 03 20:34:11 Claimed job
Jun 03 20:34:19 Reusing HOL
Jun 03 20:34:26 Starting developers
Jun 03 20:34:28 Finished developers                                               2s  80MB
Jun 03 20:34:28 Starting developers/bin
Jun 03 20:34:35 Finished developers/bin                                           6s   1GB
Jun 03 20:34:35 Starting semantics/ffi
Jun 03 20:34:45 Finished semantics/ffi                                           10s 273MB
Jun 03 20:34:45 Starting semantics
Jun 03 20:36:09 Finished semantics                                             1m23s   1GB
Jun 03 20:36:10 Starting semantics/proofs
Jun 03 20:39:43 Finished semantics/proofs                                      3m33s   2GB
Jun 03 20:39:43 Starting semantics/alt_semantics
Jun 03 20:39:52 Finished semantics/alt_semantics                                  8s 405MB
Jun 03 20:39:53 Starting semantics/alt_semantics/proofs
Jun 03 20:42:05 Finished semantics/alt_semantics/proofs                        2m12s   1GB
Jun 03 20:42:05 Starting basis/pure
Jun 03 20:43:00 Finished basis/pure                                              54s   1GB
Jun 03 20:43:00 Starting translator
Jun 03 20:46:19 Finished translator                                            3m17s   2GB
Jun 03 20:46:19 Starting compiler/parsing
Jun 03 20:47:28 Finished compiler/parsing                                      1m09s   4GB
Jun 03 20:47:28 Starting characteristic
Jun 03 20:53:18 Finished characteristic                                        5m50s   3GB
Jun 03 20:53:19 Starting translator/monadic
Jun 03 20:55:07 Finished translator/monadic                                    1m48s   2GB
Jun 03 20:55:07 Starting basis
Jun 03 21:38:52 Finished basis                                                43m43s  30GB
Jun 03 21:38:52 Starting compiler/inference
Jun 03 21:40:01 Finished compiler/inference                                    1m08s   2GB
Jun 03 21:40:02 Starting compiler/backend/reg_alloc
Jun 03 21:41:10 Finished compiler/backend/reg_alloc                            1m08s   1GB
Jun 03 21:41:10 Starting compiler/backend/gc
Jun 03 21:44:36 Finished compiler/backend/gc                                   3m25s   3GB
Jun 03 21:44:36 Starting compiler/backend
Jun 03 21:49:45 Finished compiler/backend                                      5m09s   5GB
Jun 03 21:49:46 Starting compiler/encoders/asm
Jun 03 21:50:08 Finished compiler/encoders/asm                                   22s   1GB
Jun 03 21:50:08 Starting compiler/encoders/x64
Jun 03 21:50:35 Finished compiler/encoders/x64                                   26s   1GB
Jun 03 21:50:36 Starting compiler/encoders/arm7
Jun 03 21:51:27 Finished compiler/encoders/arm7                                  51s   1GB
Jun 03 21:51:27 Starting compiler/encoders/arm8
Jun 03 21:51:41 Finished compiler/encoders/arm8                                  13s   1GB
Jun 03 21:51:41 Starting compiler/encoders/mips
Jun 03 21:51:59 Finished compiler/encoders/mips                                  18s   1GB
Jun 03 21:51:59 Starting compiler/encoders/riscv
Jun 03 21:52:15 Finished compiler/encoders/riscv                                 15s   1GB
Jun 03 21:52:15 Starting compiler/encoders/ag32
Jun 03 21:52:34 Finished compiler/encoders/ag32                                  18s 982MB
Jun 03 21:52:34 Starting compiler/backend/x64
Jun 03 21:52:54 Finished compiler/backend/x64                                    19s   1GB
Jun 03 21:52:55 Starting compiler/backend/arm7
Jun 03 21:53:17 Finished compiler/backend/arm7                                   22s   1GB
Jun 03 21:53:17 Starting compiler/backend/arm8
Jun 03 21:53:37 Finished compiler/backend/arm8                                   19s   1GB
Jun 03 21:53:38 Starting compiler/backend/mips
Jun 03 21:53:58 Finished compiler/backend/mips                                   20s   1GB
Jun 03 21:53:59 Starting compiler/backend/riscv
Jun 03 21:54:20 Finished compiler/backend/riscv                                  20s   1GB
Jun 03 21:54:20 Starting compiler/backend/ag32
Jun 03 21:55:28 Finished compiler/backend/ag32                                 1m08s   2GB
Jun 03 21:55:28 Starting compiler/parsing/proofs
Jun 03 22:01:12 Finished compiler/parsing/proofs                               5m43s   1GB
Jun 03 22:01:12 Starting compiler/inference/proofs
Jun 03 22:03:48 Finished compiler/inference/proofs                             2m36s   2GB
Jun 03 22:03:48 Starting compiler/backend/semantics
Jun 03 22:30:46 Finished compiler/backend/semantics                           26m57s   5GB
Jun 03 22:30:47 Starting compiler/backend/reg_alloc/proofs
Jun 03 22:34:06 Finished compiler/backend/reg_alloc/proofs                     3m19s   1GB
Jun 03 22:34:07 Starting compiler/backend/proofs
Jun 03 23:27:48 Finished compiler/backend/proofs                              53m40s  16GB
Jun 03 23:27:48 Starting compiler/encoders/x64/proofs
Jun 03 23:37:06 Finished compiler/encoders/x64/proofs                          9m17s   5GB
Jun 03 23:37:06 Starting compiler/encoders/arm7/proofs
Jun 03 23:50:03 Finished compiler/encoders/arm7/proofs                        12m57s   4GB
Jun 03 23:50:03 Starting compiler/encoders/arm8/proofs
Jun 03 23:56:37 Finished compiler/encoders/arm8/proofs                         6m33s   4GB
Jun 03 23:56:37 Starting compiler/encoders/mips/proofs
Jun 04 00:06:31 Finished compiler/encoders/mips/proofs                         9m53s   5GB
Jun 04 00:06:31 Starting compiler/encoders/riscv/proofs
Jun 04 00:15:09 Finished compiler/encoders/riscv/proofs                        8m37s   3GB
Jun 04 00:15:09 Starting compiler/encoders/ag32/proofs
Jun 04 00:17:31 Finished compiler/encoders/ag32/proofs                         2m21s   1GB
Jun 04 00:17:31 Starting compiler/backend/x64/proofs
Jun 04 00:17:52 Finished compiler/backend/x64/proofs                             21s   1GB
Jun 04 00:17:53 Starting compiler/backend/arm7/proofs
Jun 04 00:18:18 Finished compiler/backend/arm7/proofs                            25s   2GB
Jun 04 00:18:18 Starting compiler/backend/arm8/proofs
Jun 04 00:18:40 Finished compiler/backend/arm8/proofs                            21s   1GB
Jun 04 00:18:40 Starting compiler/backend/mips/proofs
Jun 04 00:19:02 Finished compiler/backend/mips/proofs                            22s   1GB
Jun 04 00:19:03 Starting compiler/backend/riscv/proofs
Jun 04 00:19:26 Finished compiler/backend/riscv/proofs                           23s   2GB
Jun 04 00:19:26 Starting compiler/backend/ag32/proofs
Jun 04 00:31:34 Finished compiler/backend/ag32/proofs                         12m07s   4GB
Jun 04 00:31:35 Starting compiler/proofs
Jun 04 00:33:28 Finished compiler/proofs                                       1m53s   6GB
Jun 04 00:33:28 Starting candle/set-theory
Jun 04 00:33:58 Finished candle/set-theory                                       29s 902MB
Jun 04 00:33:58 Starting candle/syntax-lib
Jun 04 00:34:09 Finished candle/syntax-lib                                       10s 809MB
Jun 04 00:34:09 Starting candle/standard/syntax
Jun 04 00:36:00 Finished candle/standard/syntax                                1m50s   1GB
Jun 04 00:36:00 Starting candle/standard/semantics
Jun 04 00:37:47 Finished candle/standard/semantics                             1m46s   2GB
Jun 04 00:37:47 Starting candle/standard/monadic
Jun 04 00:39:31 Finished candle/standard/monadic                               1m43s   1GB
Jun 04 00:39:32 Starting candle/standard/ml_kernel
Jun 04 00:45:03 Finished candle/standard/ml_kernel                             5m31s   6GB
Jun 04 00:45:03 Starting candle/overloading/syntax
Jun 04 00:48:16 Finished candle/overloading/syntax                             3m12s   1GB
Jun 04 00:48:16 Starting candle/overloading/semantics
Jun 04 01:00:23 Finished candle/overloading/semantics                         12m06s   7GB
Jun 04 01:00:23 Starting characteristic/examples
Jun 04 01:01:43 Finished characteristic/examples                               1m19s   4GB
Jun 04 01:01:43 Starting tutorial/solutions
Jun 04 01:17:17 Finished tutorial/solutions                                   15m34s  14GB
Jun 04 01:17:18 Starting translator/monadic/examples
Jun 04 01:20:44 Finished translator/monadic/examples                           3m26s   3GB
Jun 04 01:20:44 Starting examples
Jun 04 01:30:03 Finished examples                                              9m18s   6GB
Jun 04 01:30:03 Starting examples/compilation/x64
Jun 04 03:53:45 Finished examples/compilation/x64                           2h23m41s  23GB
Jun 04 03:53:45 Starting examples/compilation/x64/proofs
Jun 04 03:55:46 Finished examples/compilation/x64/proofs                       2m00s   3GB
Jun 04 03:55:46 Starting examples/compilation/ag32
Jun 04 04:29:52 Finished examples/compilation/ag32                            34m05s  12GB
Jun 04 04:29:52 Starting examples/compilation/ag32/proofs
Jun 04 04:30:45 Finished examples/compilation/ag32/proofs                        52s   5GB
Jun 04 04:30:45 Starting examples/cost
Jun 04 05:25:50 Finished examples/cost                                        55m04s  13GB
Jun 04 05:25:50 Starting examples/lpr_checker
Jun 04 05:29:50 Finished examples/lpr_checker                                  3m59s   6GB
Jun 04 05:29:50 Starting examples/lpr_checker/compilation
Jun 04 05:48:32 Finished examples/lpr_checker/compilation                     18m41s  13GB
Jun 04 05:48:33 Starting examples/lpr_checker/compilation/proofs
Jun 04 05:49:18 Finished examples/lpr_checker/compilation/proofs                 45s   4GB
Jun 04 05:49:18 Starting examples/lpr_checker/array
Jun 04 06:03:11 Finished examples/lpr_checker/array                           13m53s   4GB
Jun 04 06:03:12 Starting examples/lpr_checker/array/compilation
Jun 04 06:23:03 Finished examples/lpr_checker/array/compilation               19m51s  18GB
Jun 04 06:23:04 Starting examples/lpr_checker/array/compilation/proofs
Jun 04 06:23:55 Finished examples/lpr_checker/array/compilation/proofs           50s   5GB
Jun 04 06:23:55 Starting examples/opentheory
Jun 04 06:33:28 Finished examples/opentheory                                   9m31s   6GB
Jun 04 06:33:28 Starting examples/opentheory
Jun 04 06:33:29 Finished examples/opentheory                                      0s  99MB
Jun 04 06:33:29 Starting examples/opentheory/compilation
Jun 04 07:03:54 Finished examples/opentheory/compilation                      30m24s  18GB
Jun 04 07:03:54 Starting examples/opentheory/compilation/proofs
Jun 04 07:04:39 Finished examples/opentheory/compilation/proofs                  44s   4GB
Jun 04 07:04:39 Starting examples/opentheory/compilation/ag32
Jun 04 07:36:40 Finished examples/opentheory/compilation/ag32                 32m00s  26GB
Jun 04 07:36:40 Starting examples/opentheory/compilation/ag32/proofs
Jun 04 07:38:18 Finished examples/opentheory/compilation/ag32/proofs           1m37s   9GB
Jun 04 07:38:18 Starting examples/sat_encodings
Jun 04 07:40:10 Finished examples/sat_encodings                                1m52s   1GB
Jun 04 07:40:10 Starting examples/sat_encodings/case_studies
Jun 04 07:41:44 Finished examples/sat_encodings/case_studies                   1m33s   1GB
Jun 04 07:41:44 Starting examples/sat_encodings/translation
Jun 04 07:47:31 Finished examples/sat_encodings/translation                    5m46s   6GB
Jun 04 07:47:31 Starting examples/sat_encodings/translation/compilation
Jun 04 08:31:35 Finished examples/sat_encodings/translation/compilation       44m04s  16GB
Jun 04 08:31:35 Starting translator/okasaki-examples
Jun 04 08:36:01 Finished translator/okasaki-examples                           4m25s   3GB
Jun 04 08:36:01 Starting translator/other-examples
Jun 04 08:36:51 Finished translator/other-examples                               47s   2GB
Jun 04 08:36:51 Starting compiler/parsing/tests
Jun 04 08:37:16 Finished compiler/parsing/tests                                  24s 641MB
Jun 04 08:37:16 Starting compiler/inference/tests
Jun 04 08:44:39 Finished compiler/inference/tests                              7m22s   6GB
Jun 04 08:44:39 Starting compiler/bootstrap/translation
Jun 04 11:10:28 Finished compiler/bootstrap/translation                     2h25m48s  47GB
Jun 04 11:10:28 Starting unverified/sexpr-bootstrap/x64/64
Jun 04 11:22:42 Finished unverified/sexpr-bootstrap/x64/64                    12m13s   8GB
Jun 04 11:22:42 Starting unverified/sexpr-bootstrap/x64/32
Jun 04 11:33:13 Finished unverified/sexpr-bootstrap/x64/32                    10m30s   8GB
Jun 04 11:33:13 Starting compiler/benchmarks
Jun 04 12:11:06 Finished compiler/benchmarks                                  37m51s   2GB
Jun 04 12:11:06 Starting compiler/bootstrap/compilation/x64/64
Jun 05 05:18:25 Finished compiler/bootstrap/compilation/x64/64             17h07m16s  64GB
Jun 05 05:18:25 Starting compiler/bootstrap/compilation/x64/64/proofs
Jun 05 05:20:52 Finished compiler/bootstrap/compilation/x64/64/proofs          2m26s  20GB
Jun 05 05:20:52 Starting compiler/bootstrap/compilation/x64/32
Jun 05 19:59:11 Finished compiler/bootstrap/compilation/x64/32             14h38m19s  63GB
Jun 05 19:59:12 Starting compiler/bootstrap/compilation/x64/32/proofs
Jun 05 20:01:23 Finished compiler/bootstrap/compilation/x64/32/proofs          2m10s  14GB
Jun 05 20:01:23 Starting compiler/bootstrap/compilation/ag32/32
Jun 06 11:29:05 Finished compiler/bootstrap/compilation/ag32/32            15h27m41s  63GB
Jun 06 11:29:05 Starting compiler/bootstrap/compilation/ag32/32/proofs
Jun 06 11:38:52 Finished compiler/bootstrap/compilation/ag32/32/proofs         9m46s  56GB
Jun 06 11:38:52 SUCCESS