Job 1842

CakeML:fdfc6cb0a6e41a4b274c99b382f2c494152ee3dc
  Shuffle around some itree semantics theorems [Mar 31 15:24:39]
#870 (itree-semantics)
Merging into:8eb9e723e9f4cc989c97a68a0a5adbf6e5bec1e3
  Merge pull request #869 from CakeML/ffi-changes [Mar 31 15:20:09]
HOL:e423188b196a54551b2b4fddb00dc960d0ee96c4
  Minkowski's inequality and its applications in Probability (#1009) [Mar 25 02:18:56]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Mar 31 15:30:13 Claimed job
Mar 31 15:30:17 Reusing HOL
Mar 31 15:30:31 Starting developers
Mar 31 15:30:35 Finished developers                                               4s 116MB
Mar 31 15:30:35 Starting developers/bin
Mar 31 15:30:43 Finished developers/bin                                           7s   1GB
Mar 31 15:30:43 Starting semantics/ffi
Mar 31 15:30:54 Finished semantics/ffi                                           10s 226MB
Mar 31 15:30:54 Starting semantics
Mar 31 15:32:52 Finished semantics                                             1m58s 879MB
Mar 31 15:32:52 Starting semantics/proofs
Mar 31 15:37:00 Finished semantics/proofs                                      4m07s   2GB
Mar 31 15:37:00 Starting semantics/alt_semantics
Mar 31 15:37:25 Finished semantics/alt_semantics                                 24s 582MB
Mar 31 15:37:26 Starting semantics/alt_semantics/proofs
Mar 31 15:40:35 Finished semantics/alt_semantics/proofs                        3m09s   1GB
Mar 31 15:40:36 Starting basis/pure
Mar 31 15:41:41 Finished basis/pure                                            1m05s 835MB
Mar 31 15:41:41 Starting translator
Mar 31 15:44:39 Finished translator                                            2m57s   2GB
Mar 31 15:44:39 Starting compiler/parsing
Mar 31 15:45:55 Finished compiler/parsing                                      1m16s   2GB
Mar 31 15:45:55 Starting characteristic
Mar 31 15:52:17 Finished characteristic                                        6m21s   2GB
Mar 31 15:52:18 Starting translator/monadic
Mar 31 15:54:16 Finished translator/monadic                                    1m58s   1GB
Mar 31 15:54:16 Starting basis
Mar 31 16:40:55 Finished basis                                                46m37s  13GB
Mar 31 16:40:55 Starting compiler/inference
Mar 31 16:42:16 Finished compiler/inference                                    1m21s   1GB
Mar 31 16:42:16 Starting compiler/backend/reg_alloc
Mar 31 16:44:00 Finished compiler/backend/reg_alloc                            1m44s   1GB
Mar 31 16:44:00 Starting compiler/backend/gc
Mar 31 16:48:23 Finished compiler/backend/gc                                   4m22s   1GB
Mar 31 16:48:23 Starting compiler/backend
Mar 31 16:54:01 Finished compiler/backend                                      5m38s   2GB
Mar 31 16:54:01 Starting compiler/encoders/asm
Mar 31 16:54:31 Finished compiler/encoders/asm                                   29s 727MB
Mar 31 16:54:31 Starting compiler/encoders/x64
Mar 31 16:55:01 Finished compiler/encoders/x64                                   29s   1GB
Mar 31 16:55:02 Starting compiler/encoders/arm7
Mar 31 16:56:00 Finished compiler/encoders/arm7                                  58s 866MB
Mar 31 16:56:00 Starting compiler/encoders/arm8
Mar 31 16:56:17 Finished compiler/encoders/arm8                                  17s   1GB
Mar 31 16:56:18 Starting compiler/encoders/arm8_asl
Mar 31 16:58:49 Finished compiler/encoders/arm8_asl                            2m31s   1GB
Mar 31 16:58:49 Starting compiler/encoders/mips
Mar 31 16:59:10 Finished compiler/encoders/mips                                  21s   1GB
Mar 31 16:59:10 Starting compiler/encoders/riscv
Mar 31 16:59:30 Finished compiler/encoders/riscv                                 19s   1GB
Mar 31 16:59:30 Starting compiler/encoders/ag32
Mar 31 16:59:52 Finished compiler/encoders/ag32                                  21s 691MB
Mar 31 16:59:52 Starting compiler/backend/x64
Mar 31 17:00:13 Finished compiler/backend/x64                                    21s   1GB
Mar 31 17:00:13 Starting compiler/backend/arm7
Mar 31 17:00:37 Finished compiler/backend/arm7                                   23s   1GB
Mar 31 17:00:37 Starting compiler/backend/arm8
Mar 31 17:01:00 Finished compiler/backend/arm8                                   22s   1GB
Mar 31 17:01:00 Starting compiler/backend/mips
Mar 31 17:01:24 Finished compiler/backend/mips                                   23s   1GB
Mar 31 17:01:24 Starting compiler/backend/riscv
Mar 31 17:01:47 Finished compiler/backend/riscv                                  22s   1GB
Mar 31 17:01:47 Starting compiler/backend/ag32
Mar 31 17:03:13 Finished compiler/backend/ag32                                 1m26s   1GB
Mar 31 17:03:13 Starting compiler/parsing/proofs
Mar 31 17:06:59 Finished compiler/parsing/proofs                               3m45s   1GB
Mar 31 17:06:59 Starting compiler/inference/proofs
Mar 31 17:09:37 Finished compiler/inference/proofs                             2m37s 964MB
Mar 31 17:09:37 Starting compiler/backend/semantics
Mar 31 17:38:04 Finished compiler/backend/semantics                           28m26s   2GB
Mar 31 17:38:04 Starting compiler/backend/reg_alloc/proofs
Mar 31 17:41:36 Finished compiler/backend/reg_alloc/proofs                     3m31s 995MB
Mar 31 17:41:36 Starting compiler/backend/proofs
Mar 31 18:32:01 Finished compiler/backend/proofs                              50m24s  15GB
Mar 31 18:32:01 Starting compiler/backend/serialiser
Mar 31 18:33:39 Finished compiler/backend/serialiser                           1m38s   2GB
Mar 31 18:33:39 Starting compiler/encoders/x64/proofs
Mar 31 18:43:09 Finished compiler/encoders/x64/proofs                          9m28s   4GB
Mar 31 18:43:09 Starting compiler/encoders/arm7/proofs
Mar 31 18:56:24 Finished compiler/encoders/arm7/proofs                        13m14s   3GB
Mar 31 18:56:24 Starting compiler/encoders/arm8/proofs
Mar 31 19:03:08 Finished compiler/encoders/arm8/proofs                         6m44s   1GB
Mar 31 19:03:08 Starting compiler/encoders/arm8_asl/proofs
Mar 31 19:18:24 Finished compiler/encoders/arm8_asl/proofs                    15m15s   2GB
Mar 31 19:18:24 Starting compiler/encoders/mips/proofs
Mar 31 19:28:24 Finished compiler/encoders/mips/proofs                        10m00s   2GB
Mar 31 19:28:25 Starting compiler/encoders/riscv/proofs
Mar 31 19:37:14 Finished compiler/encoders/riscv/proofs                        8m49s   1GB
Mar 31 19:37:15 Starting compiler/encoders/ag32/proofs
Mar 31 19:39:47 Finished compiler/encoders/ag32/proofs                         2m31s 907MB
Mar 31 19:39:47 Starting compiler/backend/x64/proofs
Mar 31 19:40:16 Finished compiler/backend/x64/proofs                             28s   1GB
Mar 31 19:40:16 Starting compiler/backend/arm7/proofs
Mar 31 19:40:45 Finished compiler/backend/arm7/proofs                            28s   1GB
Mar 31 19:40:45 Starting compiler/backend/arm8/proofs
Mar 31 19:41:13 Finished compiler/backend/arm8/proofs                            28s   2GB
Mar 31 19:41:13 Starting compiler/backend/arm8_asl
Mar 31 19:41:36 Finished compiler/backend/arm8_asl                               22s   1GB
Mar 31 19:41:36 Starting compiler/backend/mips/proofs
Mar 31 19:42:05 Finished compiler/backend/mips/proofs                            28s   1GB
Mar 31 19:42:05 Starting compiler/backend/riscv/proofs
Mar 31 19:42:33 Finished compiler/backend/riscv/proofs                           28s   1GB
Mar 31 19:42:33 Starting compiler/backend/ag32/proofs
Mar 31 19:55:16 Finished compiler/backend/ag32/proofs                         12m40s   2GB
Mar 31 19:55:16 Starting compiler/proofs
Mar 31 19:57:26 Finished compiler/proofs                                       2m09s   4GB
Mar 31 19:57:26 Starting candle/set-theory
Mar 31 19:58:00 Finished candle/set-theory                                       34s   1GB
Mar 31 19:58:00 Starting candle/syntax-lib
Mar 31 19:58:14 Finished candle/syntax-lib                                       13s 580MB
Mar 31 19:58:14 Starting candle/standard/syntax
Mar 31 20:00:17 Finished candle/standard/syntax                                2m03s   1GB
Mar 31 20:00:18 Starting candle/standard/semantics
Mar 31 20:02:09 Finished candle/standard/semantics                             1m51s   1GB
Mar 31 20:02:09 Starting candle/standard/monadic
Mar 31 20:04:03 Finished candle/standard/monadic                               1m54s   1GB
Mar 31 20:04:03 Starting candle/standard/ml_kernel
Mar 31 20:10:12 Finished candle/standard/ml_kernel                             6m08s   4GB
Mar 31 20:10:12 Starting candle/overloading/syntax
Mar 31 20:13:23 Finished candle/overloading/syntax                             3m10s   1GB
Mar 31 20:13:23 Starting candle/overloading/semantics
Mar 31 20:25:23 Finished candle/overloading/semantics                         11m59s   2GB
Mar 31 20:25:23 Starting candle/overloading/monadic
Mar 31 20:27:55 Finished candle/overloading/monadic                            2m32s   1GB
Mar 31 20:27:56 Starting candle/overloading/ml_kernel
Mar 31 20:34:59 Finished candle/overloading/ml_kernel                          7m02s   3GB
Mar 31 20:34:59 Starting candle/overloading/ml_checker
Mar 31 20:37:26 Finished candle/overloading/ml_checker                         2m27s   2GB
Mar 31 20:37:26 Starting candle/prover
Mar 31 20:45:37 Finished candle/prover                                         8m10s   3GB
Mar 31 20:45:38 Starting pancake
Mar 31 20:49:28 Finished pancake                                               3m50s   4GB
Mar 31 20:49:28 Starting pancake/ffi
Mar 31 20:49:28 Finished pancake/ffi                                              0s  35MB
Mar 31 20:49:28 Starting pancake/semantics
Mar 31 20:51:54 Finished pancake/semantics                                     2m25s   1GB
Mar 31 20:51:54 Starting pancake/proofs
Mar 31 21:03:51 Finished pancake/proofs                                       11m55s   4GB
Mar 31 21:03:51 Starting characteristic/examples
Mar 31 21:05:13 Finished characteristic/examples                               1m21s   3GB
Mar 31 21:05:13 Starting tutorial/solutions
Mar 31 21:21:31 Finished tutorial/solutions                                   16m18s  11GB
Mar 31 21:21:31 Starting translator/monadic/examples
Mar 31 21:25:23 Finished translator/monadic/examples                           3m51s   2GB
Mar 31 21:25:23 Starting examples
Mar 31 21:34:41 Finished examples                                              9m17s   4GB
Mar 31 21:34:41 Starting examples/compilation/x64
Apr 01 00:04:32 Finished examples/compilation/x64                           2h29m50s  17GB
Apr 01 00:04:33 Starting examples/compilation/x64/proofs
Apr 01 00:07:13 Finished examples/compilation/x64/proofs                       2m40s   3GB
Apr 01 00:07:13 Starting examples/compilation/ag32
Apr 01 00:42:24 Finished examples/compilation/ag32                            35m11s   8GB
Apr 01 00:42:25 Starting examples/compilation/ag32/proofs
Apr 01 00:43:21 Finished examples/compilation/ag32/proofs                        56s   3GB
Apr 01 00:43:21 Starting examples/cost
Apr 01 01:38:37 Finished examples/cost                                        55m14s   8GB
Apr 01 01:38:37 Starting examples/lpr_checker
Apr 01 01:39:39 Finished examples/lpr_checker                                  1m02s   1GB
Apr 01 01:39:40 Starting examples/lpr_checker/array
Apr 01 02:07:51 Finished examples/lpr_checker/array                           28m11s   5GB
Apr 01 02:07:51 Starting examples/lpr_checker/array/compilation
Apr 01 03:34:24 Finished examples/lpr_checker/array/compilation             1h26m31s  25GB
Apr 01 03:34:24 Starting examples/lpr_checker/array/compilation/proofs
Apr 01 03:35:51 Finished examples/lpr_checker/array/compilation/proofs         1m27s   7GB
Apr 01 03:35:51 Starting examples/opentheory
Apr 01 03:45:38 Finished examples/opentheory                                   9m46s   4GB
Apr 01 03:45:38 Starting examples/opentheory
Apr 01 03:45:39 Finished examples/opentheory                                      1s 133MB
Apr 01 03:45:39 Starting examples/opentheory/compilation
Apr 01 04:26:15 Finished examples/opentheory/compilation                      40m35s  29GB
Apr 01 04:26:15 Starting examples/opentheory/compilation/proofs
Apr 01 04:27:07 Finished examples/opentheory/compilation/proofs                  52s   3GB
Apr 01 04:27:07 Starting examples/opentheory/compilation/ag32
Apr 01 05:05:18 Finished examples/opentheory/compilation/ag32                 38m09s  28GB
Apr 01 05:05:18 Starting examples/opentheory/compilation/ag32/proofs
Apr 01 05:07:33 Finished examples/opentheory/compilation/ag32/proofs           2m15s   7GB
Apr 01 05:07:33 Starting examples/sat_encodings
Apr 01 05:09:34 Finished examples/sat_encodings                                2m00s 699MB
Apr 01 05:09:34 Starting examples/sat_encodings/case_studies
Apr 01 05:11:16 Finished examples/sat_encodings/case_studies                   1m41s   1GB
Apr 01 05:11:16 Starting examples/sat_encodings/translation
Apr 01 05:16:59 Finished examples/sat_encodings/translation                    5m43s   5GB
Apr 01 05:16:59 Starting examples/sat_encodings/translation/compilation
Apr 01 06:05:49 Finished examples/sat_encodings/translation/compilation       48m49s  21GB
Apr 01 06:05:50 Starting translator/okasaki-examples
Apr 01 06:10:36 Finished translator/okasaki-examples                           4m45s   1GB
Apr 01 06:10:36 Starting translator/other-examples
Apr 01 06:11:24 Finished translator/other-examples                               48s   1GB
Apr 01 06:11:25 Starting compiler/parsing/tests
Apr 01 06:11:55 Finished compiler/parsing/tests                                  30s 577MB
Apr 01 06:11:55 Starting compiler/inference/tests
Apr 01 06:19:54 Finished compiler/inference/tests                              7m59s   3GB
Apr 01 06:19:55 Starting compiler/printing/test
Apr 01 06:23:35 Finished compiler/printing/test                                3m40s   3GB
Apr 01 06:23:35 Starting compiler/repl
Apr 01 06:36:00 Finished compiler/repl                                        12m24s   6GB
Apr 01 06:36:00 Starting compiler/bootstrap/translation Apr 01 06:36:00 32430s