Job 2038

CakeML:1661429b34cdf995d92d39224d4cea1a98d0b46b
  Fix do_app_ok proof [Nov 09 11:21:35]
#911 (libm_gen)
Merging into:3d27e77937edd037e810801a4e7849352300104f
  Add [schematic] to a definition (suggested by @mn200) [Nov 07 20:36:24]
HOL:126d898e2a2195a717f5757375b93570965286f1
  Cleanup and tweak release notes for next version in a few places [Nov 03 06:41:06]
Machine:oven3

Nov 09 14:34:50 Claimed job
Nov 09 14:35:03 Building HOL
Nov 09 14:58:13 Starting developers
Nov 09 14:58:22 Finished developers                                               9s 146MB
Nov 09 14:58:24 Starting developers/bin
Nov 09 14:58:36 Finished developers/bin                                          12s   1GB
Nov 09 14:58:37 Starting compiler/proofs
Nov 09 18:28:26 Finished compiler/proofs                                    3h29m48s  25GB
Nov 09 18:28:26 Starting compiler/bootstrap/translation
Nov 10 04:52:54 Finished compiler/bootstrap/translation                    10h24m28s  42GB
Nov 10 04:52:55 Starting semantics/ffi
Nov 10 04:53:02 Finished semantics/ffi                                            7s 231MB
Nov 10 04:53:03 Starting semantics
Nov 10 04:53:05 Finished semantics                                                2s  32MB
Nov 10 04:53:05 Starting semantics/proofs
Nov 10 04:54:22 Finished semantics/proofs                                      1m15s   1GB
Nov 10 04:54:22 Starting semantics/alt_semantics
Nov 10 04:55:22 Finished semantics/alt_semantics                                 59s 647MB
Nov 10 04:55:22 Starting semantics/alt_semantics/proofs
Nov 10 05:21:36 Finished semantics/alt_semantics/proofs                       26m13s   1GB
Nov 10 05:21:36 Starting basis/pure
Nov 10 05:21:39 Finished basis/pure                                               2s  18MB
Nov 10 05:21:39 Starting translator
Nov 10 05:25:23 Finished translator                                            3m43s   2GB
Nov 10 05:25:24 Starting compiler/parsing
Nov 10 05:25:26 Finished compiler/parsing                                         2s  17MB
Nov 10 05:25:26 Starting characteristic
Nov 10 05:25:30 Finished characteristic                                           3s  35MB
Nov 10 05:25:30 Starting translator/monadic
Nov 10 05:25:33 Finished translator/monadic                                       3s  24MB
Nov 10 05:25:33 Starting basis
Nov 10 05:33:13 Finished basis                                                 7m38s   2GB
Nov 10 05:33:13 Starting compiler/inference
Nov 10 05:33:16 Finished compiler/inference                                       2s  17MB
Nov 10 05:33:16 Starting compiler/backend/reg_alloc
Nov 10 05:33:19 Finished compiler/backend/reg_alloc                               2s  17MB
Nov 10 05:33:19 Starting compiler/backend/gc
Nov 10 05:33:23 Finished compiler/backend/gc                                      3s  42MB
Nov 10 05:33:23 Starting compiler/backend
Nov 10 05:33:45 Finished compiler/backend                                        22s 670MB
Nov 10 05:33:46 Starting compiler/encoders/asm
Nov 10 05:33:49 Finished compiler/encoders/asm                                    2s  32MB
Nov 10 05:33:49 Starting compiler/encoders/x64
Nov 10 05:33:52 Finished compiler/encoders/x64                                    2s  29MB
Nov 10 05:33:52 Starting compiler/encoders/arm7
Nov 10 05:33:55 Finished compiler/encoders/arm7                                   2s  22MB
Nov 10 05:33:55 Starting compiler/encoders/arm8
Nov 10 05:33:58 Finished compiler/encoders/arm8                                   2s  33MB
Nov 10 05:33:59 Starting compiler/encoders/arm8_asl
Nov 10 09:56:00 Finished compiler/encoders/arm8_asl                         4h22m01s  44GB
Nov 10 09:56:00 Starting compiler/encoders/mips
Nov 10 09:56:03 Finished compiler/encoders/mips                                   2s  32MB
Nov 10 09:56:03 Starting compiler/encoders/riscv
Nov 10 09:56:06 Finished compiler/encoders/riscv                                  2s  32MB
Nov 10 09:56:06 Starting compiler/encoders/ag32
Nov 10 09:56:09 Finished compiler/encoders/ag32                                   2s  36MB
Nov 10 09:56:10 Starting compiler/backend/x64
Nov 10 09:56:13 Finished compiler/backend/x64                                     3s  29MB
Nov 10 09:56:14 Starting compiler/backend/arm7
Nov 10 09:56:17 Finished compiler/backend/arm7                                    3s  33MB
Nov 10 09:56:18 Starting compiler/backend/arm8
Nov 10 09:56:22 Finished compiler/backend/arm8                                    3s  33MB
Nov 10 09:56:22 Starting compiler/backend/mips
Nov 10 09:56:26 Finished compiler/backend/mips                                    3s  34MB
Nov 10 09:56:26 Starting compiler/backend/riscv
Nov 10 09:56:30 Finished compiler/backend/riscv                                   3s  32MB
Nov 10 09:56:30 Starting compiler/backend/ag32
Nov 10 09:59:25 Finished compiler/backend/ag32                                 2m54s   1GB
Nov 10 09:59:25 Starting compiler/parsing/proofs
Nov 10 09:59:28 Finished compiler/parsing/proofs                                  2s  16MB
Nov 10 09:59:28 Starting compiler/inference/proofs
Nov 10 09:59:31 Finished compiler/inference/proofs                                2s  32MB
Nov 10 09:59:32 Starting compiler/backend/semantics
Nov 10 10:01:54 Finished compiler/backend/semantics                            2m22s   1GB
Nov 10 10:01:54 Starting compiler/backend/reg_alloc/proofs
Nov 10 10:01:58 Finished compiler/backend/reg_alloc/proofs                        3s  33MB
Nov 10 10:01:58 Starting compiler/backend/proofs
Nov 10 10:03:50 Finished compiler/backend/proofs                               1m51s   2GB
Nov 10 10:03:50 Starting compiler/backend/serialiser
Nov 10 10:03:55 Finished compiler/backend/serialiser                              5s  33MB
Nov 10 10:03:56 Starting compiler/encoders/x64/proofs
Nov 10 10:25:51 Finished compiler/encoders/x64/proofs                         21m54s   6GB
Nov 10 10:25:51 Starting compiler/encoders/arm7/proofs
Nov 10 10:57:47 Finished compiler/encoders/arm7/proofs                        31m55s   8GB
Nov 10 10:57:47 Starting compiler/encoders/arm8/proofs
Nov 10 11:13:46 Finished compiler/encoders/arm8/proofs                        15m59s   1GB
Nov 10 11:13:47 Starting compiler/encoders/arm8_asl/proofs
Nov 10 13:10:32 Finished compiler/encoders/arm8_asl/proofs                  1h56m44s   7GB
Nov 10 13:10:32 Starting compiler/encoders/mips/proofs
Nov 10 13:34:24 Finished compiler/encoders/mips/proofs                        23m51s   2GB
Nov 10 13:34:24 Starting compiler/encoders/riscv/proofs
Nov 10 13:54:24 Finished compiler/encoders/riscv/proofs                       20m00s   1GB
Nov 10 13:54:25 Starting compiler/encoders/ag32/proofs
Nov 10 14:00:25 Finished compiler/encoders/ag32/proofs                         5m59s 833MB
Nov 10 14:00:25 Starting compiler/backend/x64/proofs
Nov 10 14:01:20 Finished compiler/backend/x64/proofs                             54s   1GB
Nov 10 14:01:20 Starting compiler/backend/arm7/proofs
Nov 10 14:02:17 Finished compiler/backend/arm7/proofs                            56s   1GB
Nov 10 14:02:17 Starting compiler/backend/arm8/proofs
Nov 10 14:03:11 Finished compiler/backend/arm8/proofs                            54s   1GB
Nov 10 14:03:12 Starting compiler/backend/arm8_asl
Nov 10 14:03:55 Finished compiler/backend/arm8_asl                               42s   1GB
Nov 10 14:03:55 Starting compiler/backend/mips/proofs
Nov 10 14:04:52 Finished compiler/backend/mips/proofs                            57s   2GB
Nov 10 14:04:53 Starting compiler/backend/riscv/proofs
Nov 10 14:05:47 Finished compiler/backend/riscv/proofs                           54s   1GB
Nov 10 14:05:48 Starting compiler/backend/ag32/proofs
Nov 10 14:36:20 Finished compiler/backend/ag32/proofs                         30m31s   3GB
Nov 10 14:36:20 Starting candle/set-theory
Nov 10 14:37:28 Finished candle/set-theory                                     1m07s   1GB
Nov 10 14:37:28 Starting candle/syntax-lib
Nov 10 14:37:31 Finished candle/syntax-lib                                        2s  33MB
Nov 10 14:37:31 Starting candle/standard/syntax
Nov 10 14:37:51 Finished candle/standard/syntax                                  19s 513MB
Nov 10 14:37:51 Starting candle/standard/semantics
Nov 10 14:41:47 Finished candle/standard/semantics                             3m55s   1GB
Nov 10 14:41:47 Starting candle/standard/monadic
Nov 10 14:41:50 Finished candle/standard/monadic                                  3s  33MB
Nov 10 14:41:51 Starting candle/standard/ml_kernel
Nov 10 14:45:05 Finished candle/standard/ml_kernel                             3m14s   3GB
Nov 10 14:45:05 Starting candle/overloading/syntax
Nov 10 14:51:59 Finished candle/overloading/syntax                             6m53s   1GB
Nov 10 14:52:00 Starting candle/overloading/semantics
Nov 10 15:18:37 Finished candle/overloading/semantics                         26m36s   2GB
Nov 10 15:18:37 Starting candle/overloading/monadic
Nov 10 15:24:12 Finished candle/overloading/monadic                            5m35s   1GB
Nov 10 15:24:13 Starting candle/overloading/ml_kernel
Nov 10 15:39:44 Finished candle/overloading/ml_kernel                         15m30s   3GB
Nov 10 15:39:44 Starting candle/overloading/ml_checker
Nov 10 15:45:10 Finished candle/overloading/ml_checker                         5m25s   3GB
Nov 10 15:45:10 Starting candle/prover
Nov 10 16:06:29 Finished candle/prover                                        21m18s   3GB
Nov 10 16:06:29 Starting pancake
Nov 10 16:12:45 Finished pancake                                               6m15s   4GB
Nov 10 16:12:45 Starting pancake/ffi
Nov 10 16:12:46 Finished pancake/ffi                                              0s  12MB
Nov 10 16:12:46 Starting pancake/semantics
Nov 10 16:17:57 Finished pancake/semantics                                     5m11s   1GB
Nov 10 16:17:58 Starting pancake/proofs
Nov 10 16:24:08 Finished pancake/proofs                                        6m10s   1GB
Nov 10 16:24:08 Starting characteristic/examples
Nov 10 16:27:08 Finished characteristic/examples                               2m59s   2GB
Nov 10 16:27:08 Starting tutorial/solutions
Nov 10 17:01:30 Finished tutorial/solutions                                   34m21s   9GB
Nov 10 17:01:31 Starting translator/monadic/examples
Nov 10 17:08:23 Finished translator/monadic/examples                           6m52s   2GB
Nov 10 17:08:24 Starting examples
Nov 10 17:27:43 Finished examples                                             19m19s   3GB
Nov 10 17:27:44 Starting examples/compilation/x64
Nov 10 22:05:23 Finished examples/compilation/x64                           4h37m39s  23GB
Nov 10 22:05:23 Starting examples/compilation/x64/proofs
Nov 10 22:09:06 Finished examples/compilation/x64/proofs                       3m42s   3GB
Nov 10 22:09:06 Starting examples/compilation/ag32
Nov 10 23:24:41 Finished examples/compilation/ag32                          1h15m34s   8GB
Nov 10 23:24:42 Starting examples/compilation/ag32/proofs
Nov 10 23:26:26 Finished examples/compilation/ag32/proofs                      1m44s   3GB
Nov 10 23:26:27 Starting examples/compilation/to_word
Nov 10 23:33:03 Finished examples/compilation/to_word                          6m36s   5GB
Nov 10 23:33:03 Starting examples/lpr_checker
Nov 10 23:35:02 Finished examples/lpr_checker                                  1m57s 983MB
Nov 10 23:35:02 Starting examples/lpr_checker/array
Nov 11 00:55:27 Finished examples/lpr_checker/array                         1h20m24s   4GB
Nov 11 00:55:27 Starting examples/lpr_checker/array/compilation
Nov 11 02:17:14 Finished examples/lpr_checker/array/compilation             1h21m46s  36GB
Nov 11 02:17:15 Starting examples/lpr_checker/array/compilation/proofs
Nov 11 02:19:50 Finished examples/lpr_checker/array/compilation/proofs         2m35s   5GB
Nov 11 02:19:51 Starting examples/opentheory
Nov 11 02:42:19 Finished examples/opentheory                                  22m27s   5GB
Nov 11 02:42:19 Starting examples/opentheory
Nov 11 02:42:23 Finished examples/opentheory                                      3s  33MB
Nov 11 02:42:23 Starting examples/opentheory/compilation
Nov 11 04:07:04 Finished examples/opentheory/compilation                    1h24m41s  32GB
Nov 11 04:07:05 Starting examples/opentheory/compilation/proofs
Nov 11 04:08:40 Finished examples/opentheory/compilation/proofs                1m35s   3GB
Nov 11 04:08:40 Starting examples/opentheory/compilation/ag32
Nov 11 05:30:39 Finished examples/opentheory/compilation/ag32               1h21m58s  39GB
Nov 11 05:30:39 Starting examples/opentheory/compilation/ag32/proofs
Nov 11 05:34:53 Finished examples/opentheory/compilation/ag32/proofs           4m13s   6GB
Nov 11 05:34:54 Starting examples/sat_encodings
Nov 11 05:38:43 Finished examples/sat_encodings                                3m49s 703MB
Nov 11 05:38:44 Starting examples/sat_encodings/case_studies
Nov 11 05:42:22 Finished examples/sat_encodings/case_studies                   3m38s 986MB
Nov 11 05:42:23 Starting examples/sat_encodings/translation
Nov 11 05:53:56 Finished examples/sat_encodings/translation                   11m33s   5GB
Nov 11 05:53:56 Starting examples/sat_encodings/translation/compilation
Nov 11 07:19:00 Finished examples/sat_encodings/translation/compilation     1h25m02s  22GB
Nov 11 07:19:00 Starting examples/deflate
Nov 11 07:20:43 Finished examples/deflate                                      1m42s 812MB
Nov 11 07:20:43 Starting examples/deflate/translation
Nov 11 07:23:43 Finished examples/deflate/translation                          2m59s   3GB
Nov 11 07:23:43 Starting examples/deflate/translation/compilation
Nov 11 08:02:34 Finished examples/deflate/translation/compilation             38m50s  12GB
Nov 11 08:02:34 Starting translator/okasaki-examples
Nov 11 08:12:28 Finished translator/okasaki-examples                           9m54s   2GB
Nov 11 08:12:29 Starting translator/other-examples
Nov 11 08:17:15 Finished translator/other-examples                             4m46s   1GB
Nov 11 08:17:16 Starting compiler/parsing/tests
Nov 11 08:18:24 Finished compiler/parsing/tests                                1m08s 601MB
Nov 11 08:18:25 Starting compiler/inference/tests
Nov 11 08:34:52 Finished compiler/inference/tests                             16m27s   6GB
Nov 11 08:34:53 Starting compiler/printing/test
Nov 11 08:42:11 Finished compiler/printing/test                                7m17s   3GB
Nov 11 08:42:11 Starting icing/flover
Nov 11 08:42:11 SysErr ("No such file or directory", SOME ENOENT)
Nov 11 08:42:11 FAILED: icing/flover