Job 1541

CakeML:36d5c13ef89908d2c2bf082c13186087bd1502f6
  Merge pull request #828 from CakeML/sat_encodings [Jun 04 08:57:36]
HOL:90009e5249fd1c36d9ee3320c07e341d79654c55
  Some alternative definitions of (sub-,super-)martingales [Jun 04 11:42:36]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64
Artefacts:cake-x64-32.tar.gz
cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz

Jun 08 09:37:18 Claimed job
Jun 08 09:37:24 Building HOL
Jun 08 09:53:29 Starting developers
Jun 08 09:53:33 Finished developers                                               4s 117MB
Jun 08 09:53:34 Starting developers/bin
Jun 08 09:53:41 Finished developers/bin                                           7s   1GB
Jun 08 09:53:41 Starting semantics/ffi
Jun 08 09:53:52 Finished semantics/ffi                                           11s 242MB
Jun 08 09:53:53 Starting semantics
Jun 08 09:55:30 Finished semantics                                             1m36s   1GB
Jun 08 09:55:30 Starting semantics/proofs
Jun 08 09:59:25 Finished semantics/proofs                                      3m54s   1GB
Jun 08 09:59:25 Starting semantics/alt_semantics
Jun 08 09:59:34 Finished semantics/alt_semantics                                  9s 337MB
Jun 08 09:59:35 Starting semantics/alt_semantics/proofs
Jun 08 10:01:56 Finished semantics/alt_semantics/proofs                        2m21s   1GB
Jun 08 10:01:56 Starting basis/pure
Jun 08 10:05:05 Finished basis/pure                                            3m08s   1GB
Jun 08 10:05:05 Starting translator
Jun 08 10:08:45 Finished translator                                            3m39s   1GB
Jun 08 10:08:45 Starting compiler/parsing
Jun 08 10:10:02 Finished compiler/parsing                                      1m17s   2GB
Jun 08 10:10:02 Starting characteristic
Jun 08 10:15:54 Finished characteristic                                        5m51s   1GB
Jun 08 10:15:55 Starting translator/monadic
Jun 08 10:17:38 Finished translator/monadic                                    1m43s   1GB
Jun 08 10:17:39 Starting basis
Jun 08 11:05:28 Finished basis                                                47m49s  14GB
Jun 08 11:05:29 Starting compiler/inference
Jun 08 11:06:49 Finished compiler/inference                                    1m19s   1GB
Jun 08 11:06:49 Starting compiler/backend/reg_alloc
Jun 08 11:08:00 Finished compiler/backend/reg_alloc                            1m10s   1GB
Jun 08 11:08:00 Starting compiler/backend/gc
Jun 08 11:11:53 Finished compiler/backend/gc                                   3m53s   2GB
Jun 08 11:11:54 Starting compiler/backend
Jun 08 11:17:05 Finished compiler/backend                                      5m11s   4GB
Jun 08 11:17:06 Starting compiler/encoders/asm
Jun 08 11:17:29 Finished compiler/encoders/asm                                   23s 614MB
Jun 08 11:17:29 Starting compiler/encoders/x64
Jun 08 11:18:36 Finished compiler/encoders/x64                                 1m06s 752MB
Jun 08 11:18:36 Starting compiler/encoders/arm7
Jun 08 11:20:48 Finished compiler/encoders/arm7                                2m11s   1GB
Jun 08 11:20:48 Starting compiler/encoders/arm8
Jun 08 11:21:29 Finished compiler/encoders/arm8                                  40s 825MB
Jun 08 11:21:29 Starting compiler/encoders/mips
Jun 08 11:23:06 Finished compiler/encoders/mips                                1m37s   1GB
Jun 08 11:23:06 Starting compiler/encoders/riscv
Jun 08 11:25:02 Finished compiler/encoders/riscv                               1m55s   1GB
Jun 08 11:25:02 Starting compiler/encoders/ag32
Jun 08 11:25:21 Finished compiler/encoders/ag32                                  18s 603MB
Jun 08 11:25:21 Starting compiler/backend/x64
Jun 08 11:25:41 Finished compiler/backend/x64                                    19s   1GB
Jun 08 11:25:41 Starting compiler/backend/arm7
Jun 08 11:26:03 Finished compiler/backend/arm7                                   21s   1GB
Jun 08 11:26:03 Starting compiler/backend/arm8
Jun 08 11:26:22 Finished compiler/backend/arm8                                   19s   1GB
Jun 08 11:26:23 Starting compiler/backend/mips
Jun 08 11:26:43 Finished compiler/backend/mips                                   19s   1GB
Jun 08 11:26:43 Starting compiler/backend/riscv
Jun 08 11:27:03 Finished compiler/backend/riscv                                  19s   1GB
Jun 08 11:27:03 Starting compiler/backend/ag32
Jun 08 11:28:16 Finished compiler/backend/ag32                                 1m12s   1GB
Jun 08 11:28:16 Starting compiler/parsing/proofs
Jun 08 11:34:25 Finished compiler/parsing/proofs                               6m08s   1GB
Jun 08 11:34:26 Starting compiler/inference/proofs
Jun 08 11:37:04 Finished compiler/inference/proofs                             2m38s   1GB
Jun 08 11:37:05 Starting compiler/backend/semantics
Jun 08 12:10:46 Finished compiler/backend/semantics                           33m41s   2GB
Jun 08 12:10:47 Starting compiler/backend/reg_alloc/proofs
Jun 08 12:14:37 Finished compiler/backend/reg_alloc/proofs                     3m49s   1GB
Jun 08 12:14:37 Starting compiler/backend/proofs
Jun 08 13:13:26 Finished compiler/backend/proofs                              58m48s  18GB
Jun 08 13:13:26 Starting compiler/encoders/x64/proofs
Jun 08 13:23:52 Finished compiler/encoders/x64/proofs                         10m26s   3GB
Jun 08 13:23:52 Starting compiler/encoders/arm7/proofs
Jun 08 13:38:19 Finished compiler/encoders/arm7/proofs                        14m25s   3GB
Jun 08 13:38:19 Starting compiler/encoders/arm8/proofs
Jun 08 13:45:37 Finished compiler/encoders/arm8/proofs                         7m18s   1GB
Jun 08 13:45:37 Starting compiler/encoders/mips/proofs
Jun 08 13:56:27 Finished compiler/encoders/mips/proofs                        10m49s   1GB
Jun 08 13:56:27 Starting compiler/encoders/riscv/proofs
Jun 08 14:06:07 Finished compiler/encoders/riscv/proofs                        9m39s   1GB
Jun 08 14:06:07 Starting compiler/encoders/ag32/proofs
Jun 08 14:08:54 Finished compiler/encoders/ag32/proofs                         2m47s 881MB
Jun 08 14:08:55 Starting compiler/backend/x64/proofs
Jun 08 14:09:17 Finished compiler/backend/x64/proofs                             22s   1GB
Jun 08 14:09:17 Starting compiler/backend/arm7/proofs
Jun 08 14:09:41 Finished compiler/backend/arm7/proofs                            23s   1GB
Jun 08 14:09:41 Starting compiler/backend/arm8/proofs
Jun 08 14:10:04 Finished compiler/backend/arm8/proofs                            22s   1GB
Jun 08 14:10:05 Starting compiler/backend/mips/proofs
Jun 08 14:10:29 Finished compiler/backend/mips/proofs                            23s   2GB
Jun 08 14:10:29 Starting compiler/backend/riscv/proofs
Jun 08 14:10:51 Finished compiler/backend/riscv/proofs                           21s   1GB
Jun 08 14:10:51 Starting compiler/backend/ag32/proofs
Jun 08 14:24:45 Finished compiler/backend/ag32/proofs                         13m53s   2GB
Jun 08 14:24:45 Starting compiler/proofs
Jun 08 14:26:47 Finished compiler/proofs                                       2m01s   5GB
Jun 08 14:26:47 Starting candle/set-theory
Jun 08 14:27:17 Finished candle/set-theory                                       29s 901MB
Jun 08 14:27:17 Starting candle/syntax-lib
Jun 08 14:27:28 Finished candle/syntax-lib                                       10s 725MB
Jun 08 14:27:28 Starting candle/standard/syntax
Jun 08 14:29:24 Finished candle/standard/syntax                                1m55s   1GB
Jun 08 14:29:24 Starting candle/standard/semantics
Jun 08 14:31:14 Finished candle/standard/semantics                             1m49s 932MB
Jun 08 14:31:14 Starting candle/standard/monadic
Jun 08 14:33:06 Finished candle/standard/monadic                               1m51s   1GB
Jun 08 14:33:06 Starting candle/standard/ml_kernel
Jun 08 14:39:07 Finished candle/standard/ml_kernel                             6m01s   6GB
Jun 08 14:39:08 Starting candle/overloading/syntax
Jun 08 14:42:29 Finished candle/overloading/syntax                             3m20s   1GB
Jun 08 14:42:29 Starting candle/overloading/semantics
Jun 08 14:55:17 Finished candle/overloading/semantics                         12m48s   4GB
Jun 08 14:55:18 Starting characteristic/examples
Jun 08 14:56:41 Finished characteristic/examples                               1m22s   3GB
Jun 08 14:56:41 Starting tutorial/solutions
Jun 08 15:12:56 Finished tutorial/solutions                                   16m14s   8GB
Jun 08 15:12:56 Starting translator/monadic/examples
Jun 08 15:16:21 Finished translator/monadic/examples                           3m25s   2GB
Jun 08 15:16:21 Starting examples
Jun 08 15:25:56 Finished examples                                              9m34s   4GB
Jun 08 15:25:56 Starting examples/compilation/x64
Jun 08 17:57:16 Finished examples/compilation/x64                           2h31m19s  16GB
Jun 08 17:57:16 Starting examples/compilation/x64/proofs
Jun 08 17:59:12 Finished examples/compilation/x64/proofs                       1m55s   3GB
Jun 08 17:59:12 Starting examples/compilation/ag32
Jun 08 18:34:44 Finished examples/compilation/ag32                            35m31s   7GB
Jun 08 18:34:44 Starting examples/compilation/ag32/proofs
Jun 08 18:35:39 Finished examples/compilation/ag32/proofs                        53s   3GB
Jun 08 18:35:39 Starting examples/cost
Jun 08 19:35:12 Finished examples/cost                                        59m32s   7GB
Jun 08 19:35:12 Starting examples/lpr_checker
Jun 08 19:39:23 Finished examples/lpr_checker                                  4m10s   4GB
Jun 08 19:39:23 Starting examples/lpr_checker/compilation
Jun 08 19:58:45 Finished examples/lpr_checker/compilation                     19m21s  11GB
Jun 08 19:58:45 Starting examples/lpr_checker/compilation/proofs
Jun 08 19:59:28 Finished examples/lpr_checker/compilation/proofs                 42s   3GB
Jun 08 19:59:28 Starting examples/lpr_checker/array
Jun 08 20:15:04 Finished examples/lpr_checker/array                           15m35s   3GB
Jun 08 20:15:04 Starting examples/lpr_checker/array/compilation
Jun 08 20:35:52 Finished examples/lpr_checker/array/compilation               20m46s  12GB
Jun 08 20:35:52 Starting examples/lpr_checker/array/compilation/proofs
Jun 08 20:37:04 Finished examples/lpr_checker/array/compilation/proofs         1m12s   3GB
Jun 08 20:37:05 Starting examples/opentheory
Jun 08 20:47:31 Finished examples/opentheory                                  10m26s   4GB
Jun 08 20:47:31 Starting examples/opentheory
Jun 08 20:47:32 Finished examples/opentheory                                      1s  23MB
Jun 08 20:47:33 Starting examples/opentheory/compilation
Jun 08 21:20:26 Finished examples/opentheory/compilation                      32m52s  20GB
Jun 08 21:20:26 Starting examples/opentheory/compilation/proofs
Jun 08 21:21:08 Finished examples/opentheory/compilation/proofs                  42s   3GB
Jun 08 21:21:08 Starting examples/opentheory/compilation/ag32
Jun 08 21:56:15 Finished examples/opentheory/compilation/ag32                 35m05s  19GB
Jun 08 21:56:15 Starting examples/opentheory/compilation/ag32/proofs
Jun 08 21:57:54 Finished examples/opentheory/compilation/ag32/proofs           1m39s   5GB
Jun 08 21:57:54 Starting examples/sat_encodings
Jun 08 21:59:45 Finished examples/sat_encodings                                1m50s 784MB
Jun 08 21:59:45 Starting examples/sat_encodings/case_studies
Jun 08 22:01:27 Finished examples/sat_encodings/case_studies                   1m41s 704MB
Jun 08 22:01:27 Starting examples/sat_encodings/translation
Jun 08 22:07:25 Finished examples/sat_encodings/translation                    5m57s   3GB
Jun 08 22:07:26 Starting examples/sat_encodings/translation/compilation
Jun 08 22:53:33 Finished examples/sat_encodings/translation/compilation       46m07s  19GB
Jun 08 22:53:33 Starting translator/okasaki-examples
Jun 08 22:58:19 Finished translator/okasaki-examples                           4m44s   1GB
Jun 08 22:58:19 Starting translator/other-examples
Jun 08 23:00:32 Finished translator/other-examples                             2m12s   1GB
Jun 08 23:00:32 Starting compiler/parsing/tests
Jun 08 23:01:00 Finished compiler/parsing/tests                                  27s 636MB
Jun 08 23:01:00 Starting compiler/inference/tests
Jun 08 23:09:11 Finished compiler/inference/tests                              8m10s   6GB
Jun 08 23:09:11 Starting compiler/bootstrap/translation
Jun 09 01:55:37 Finished compiler/bootstrap/translation                     2h46m25s  26GB
Jun 09 01:55:37 Starting unverified/sexpr-bootstrap/x64/64
Jun 09 02:07:15 Finished unverified/sexpr-bootstrap/x64/64                    11m33s   9GB
Jun 09 02:07:16 Starting unverified/sexpr-bootstrap/x64/32
Jun 09 02:17:25 Finished unverified/sexpr-bootstrap/x64/32                    10m05s   8GB
Jun 09 02:17:25 Starting compiler/benchmarks
Jun 09 02:17:27 Finished compiler/benchmarks                                      1s  24MB
Jun 09 02:17:28 Starting compiler/bootstrap/compilation/x64/64
Jun 09 15:17:27 Finished compiler/bootstrap/compilation/x64/64             12h59m55s  64GB
Jun 09 15:17:27 Starting compiler/bootstrap/compilation/x64/64/proofs
Jun 09 15:20:28 Finished compiler/bootstrap/compilation/x64/64/proofs          3m00s  12GB
Jun 09 15:20:28 Starting compiler/bootstrap/compilation/x64/32
Jun 10 03:09:07 Finished compiler/bootstrap/compilation/x64/32             11h48m35s  64GB
Jun 10 03:09:07 Starting compiler/bootstrap/compilation/x64/32/proofs
Jun 10 03:12:09 Finished compiler/bootstrap/compilation/x64/32/proofs          3m01s  13GB
Jun 10 03:12:09 Starting compiler/bootstrap/compilation/ag32/32
Jun 10 15:12:14 Finished compiler/bootstrap/compilation/ag32/32            12h00m05s  64GB
Jun 10 15:12:15 Starting compiler/bootstrap/compilation/ag32/32/proofs
Jun 10 15:33:24 Finished compiler/bootstrap/compilation/ag32/32/proofs        21m09s  24GB
Jun 10 15:33:24 SUCCESS