Job 698

CakeML:f7beb9c7fbb5c4ee5586f57d294610d840ec9932
  Fix remaining cf example [Jan 23 15:00:10]
#609 (cf-div-io)
Merging into:132124a020e9f4e4bb00fb0274f9505461195904
  Merge pull request #608 from CakeML/cheats [Jan 21 17:46:50]
HOL:ce7414f3a9b67a55c010a5194ca0029e347b7810
  More easily moved theorems from CakeML (this time to finite_map) [Jan 17 00:42:39]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Jan 23 15:01:07 Claimed job
Jan 23 15:01:15 Reusing HOL
Jan 23 15:01:25 Starting developers
Jan 23 15:01:26 Finished developers                                               0s  30MB
Jan 23 15:01:27 Starting developers/bin
Jan 23 15:02:02 Finished developers/bin                                          34s 204MB
Jan 23 15:02:03 Starting semantics/ffi
Jan 23 15:02:12 Finished semantics/ffi                                            7s 223MB
Jan 23 15:02:12 Starting semantics
Jan 23 15:03:32 Finished semantics                                             1m19s   1GB
Jan 23 15:03:33 Starting semantics/proofs
Jan 23 15:06:49 Finished semantics/proofs                                      3m15s 985MB
Jan 23 15:06:50 Starting basis/pure
Jan 23 15:07:35 Finished basis/pure                                              43s 670MB
Jan 23 15:07:36 Starting translator
Jan 23 15:09:15 Finished translator                                            1m38s   1GB
Jan 23 15:09:15 Starting compiler/parsing
Jan 23 15:10:19 Finished compiler/parsing                                      1m02s   2GB
Jan 23 15:10:20 Starting characteristic
Jan 23 15:14:45 Finished characteristic                                        4m24s   1GB
Jan 23 15:14:46 Starting translator/monadic
Jan 23 15:16:13 Finished translator/monadic                                    1m26s   1GB
Jan 23 15:16:14 Starting basis
Jan 23 15:33:12 Finished basis                                                16m56s   2GB
Jan 23 15:33:13 Starting compiler/inference
Jan 23 15:34:52 Finished compiler/inference                                    1m38s   1GB
Jan 23 15:34:53 Starting compiler/backend/reg_alloc
Jan 23 15:35:44 Finished compiler/backend/reg_alloc                              50s   1GB
Jan 23 15:35:45 Starting compiler/backend/gc
Jan 23 15:43:36 Finished compiler/backend/gc                                   7m50s   2GB
Jan 23 15:43:37 Starting compiler/backend
Jan 23 15:43:40 Finished compiler/backend                                         1s  17MB
Jan 23 15:43:40 Starting compiler/encoders/asm
Jan 23 15:43:42 Finished compiler/encoders/asm                                    0s  17MB
Jan 23 15:43:42 Starting compiler/encoders/x64
Jan 23 15:44:07 Finished compiler/encoders/x64                                   23s 960MB
Jan 23 15:44:08 Starting compiler/encoders/arm6
Jan 23 15:44:59 Finished compiler/encoders/arm6                                  50s 950MB
Jan 23 15:45:00 Starting compiler/encoders/arm8
Jan 23 15:45:12 Finished compiler/encoders/arm8                                  11s 873MB
Jan 23 15:45:13 Starting compiler/encoders/mips
Jan 23 15:45:30 Finished compiler/encoders/mips                                  16s 800MB
Jan 23 15:45:31 Starting compiler/encoders/riscv
Jan 23 15:45:46 Finished compiler/encoders/riscv                                 13s 772MB
Jan 23 15:45:46 Starting compiler/encoders/ag32
Jan 23 15:46:03 Finished compiler/encoders/ag32                                  15s 814MB
Jan 23 15:46:04 Starting compiler/backend/x64
Jan 23 15:46:21 Finished compiler/backend/x64                                    16s   1GB
Jan 23 15:46:22 Starting compiler/backend/arm6
Jan 23 15:46:41 Finished compiler/backend/arm6                                   18s   1GB
Jan 23 15:46:41 Starting compiler/backend/arm8
Jan 23 15:46:58 Finished compiler/backend/arm8                                   16s 852MB
Jan 23 15:46:59 Starting compiler/backend/mips
Jan 23 15:47:17 Finished compiler/backend/mips                                   16s 940MB
Jan 23 15:47:17 Starting compiler/backend/riscv
Jan 23 15:47:35 Finished compiler/backend/riscv                                  16s   1GB
Jan 23 15:47:36 Starting compiler/backend/ag32
Jan 23 15:48:48 Finished compiler/backend/ag32                                 1m12s   1GB
Jan 23 15:48:49 Starting compiler/parsing/proofs
Jan 23 15:54:49 Finished compiler/parsing/proofs                               5m58s 861MB
Jan 23 15:54:49 Starting compiler/inference/proofs
Jan 23 15:57:43 Finished compiler/inference/proofs                             2m53s   1GB
Jan 23 15:57:44 Starting compiler/backend/semantics
Jan 23 16:05:22 Finished compiler/backend/semantics                            7m37s   1GB
Jan 23 16:05:23 Starting compiler/backend/reg_alloc/proofs
Jan 23 16:08:08 Finished compiler/backend/reg_alloc/proofs                     2m44s   1GB
Jan 23 16:08:09 Starting compiler/backend/proofs
Jan 23 16:47:06 Finished compiler/backend/proofs                              38m56s   3GB
Jan 23 16:47:07 Starting compiler/encoders/x64/proofs
Jan 23 16:57:01 Finished compiler/encoders/x64/proofs                          9m54s   4GB
Jan 23 16:57:02 Starting compiler/encoders/arm6/proofs
Jan 23 17:11:12 Finished compiler/encoders/arm6/proofs                        14m09s   3GB
Jan 24 06:21:02 Resuming compiler/encoders/arm8/proofs
Jan 24 06:27:00 Finished compiler/encoders/arm8/proofs                         5m57s   1GB
Jan 24 06:27:00 Starting compiler/encoders/mips/proofs
Jan 24 06:37:22 Finished compiler/encoders/mips/proofs                        10m21s   2GB
Jan 24 06:37:23 Starting compiler/encoders/riscv/proofs
Jan 24 06:45:24 Finished compiler/encoders/riscv/proofs                        7m59s 949MB
Jan 24 06:45:24 Starting compiler/encoders/ag32/proofs
Jan 24 06:48:08 Finished compiler/encoders/ag32/proofs                         2m42s 721MB
Jan 24 06:48:09 Starting compiler/backend/x64/proofs
Jan 24 06:48:28 Finished compiler/backend/x64/proofs                             18s   1GB
Jan 24 06:48:29 Starting compiler/backend/arm6/proofs
Jan 24 06:48:50 Finished compiler/backend/arm6/proofs                            20s 862MB
Jan 24 06:48:50 Starting compiler/backend/arm8/proofs
Jan 24 06:49:10 Finished compiler/backend/arm8/proofs                            18s   1GB
Jan 24 06:49:11 Starting compiler/backend/mips/proofs
Jan 24 06:49:31 Finished compiler/backend/mips/proofs                            19s   1GB
Jan 24 06:49:32 Starting compiler/backend/riscv/proofs
Jan 24 06:49:51 Finished compiler/backend/riscv/proofs                           18s   1GB
Jan 24 06:49:52 Starting compiler/backend/ag32/proofs
Jan 24 06:59:16 Finished compiler/backend/ag32/proofs                          9m23s   2GB
Jan 24 06:59:17 Starting compiler/proofs
Jan 24 07:00:37 Finished compiler/proofs                                       1m19s   2GB
Jan 24 07:00:38 Starting candle/set-theory
Jan 24 07:01:04 Finished candle/set-theory                                       25s 654MB
Jan 24 07:01:05 Starting candle/syntax-lib
Jan 24 07:01:15 Finished candle/syntax-lib                                        9s 651MB
Jan 24 07:01:16 Starting candle/standard/syntax
Jan 24 07:03:03 Finished candle/standard/syntax                                1m46s   1GB
Jan 24 07:03:04 Starting candle/standard/semantics
Jan 24 07:04:42 Finished candle/standard/semantics                             1m37s   1GB
Jan 24 07:04:43 Starting candle/standard/monadic
Jan 24 07:06:28 Finished candle/standard/monadic                               1m44s   1GB
Jan 24 07:06:29 Starting candle/standard/ml_kernel
Jan 24 07:10:23 Finished candle/standard/ml_kernel                             3m53s   4GB
Jan 24 07:10:24 Starting candle/standard/opentheory
Jan 24 07:19:13 Finished candle/standard/opentheory                            8m48s   4GB
Jan 24 07:19:14 Starting candle/standard/opentheory/compilation
Jan 24 07:47:19 Finished candle/standard/opentheory/compilation               28m03s  12GB
Jan 24 07:47:20 Starting candle/standard/opentheory/compilation/proofs
Jan 24 07:48:03 Finished candle/standard/opentheory/compilation/proofs           42s   4GB
Jan 24 07:48:04 Starting characteristic/examples
Jan 24 07:49:39 Finished characteristic/examples                               1m33s   3GB
Jan 24 07:49:39 Starting tutorial/solutions
Jan 24 08:02:46 Finished tutorial/solutions                                   13m05s   6GB
Jan 24 08:02:47 Starting translator/monadic/examples
Jan 24 08:04:57 Finished translator/monadic/examples                           2m09s   2GB
Jan 24 08:04:57 Starting examples
Jan 24 08:12:58 Finished examples                                              7m59s   3GB
Jan 24 08:12:59 Starting examples/compilation/x64
Jan 24 10:04:46 Finished examples/compilation/x64                           1h51m46s  12GB
Jan 24 10:04:47 Starting examples/compilation/x64/proofs
Jan 24 10:06:32 Finished examples/compilation/x64/proofs                       1m44s   5GB
Jan 24 10:06:33 Starting examples/compilation/ag32
Jan 24 10:34:33 Finished examples/compilation/ag32                            27m59s   5GB
Jan 24 10:34:34 Starting examples/compilation/ag32/proofs
Jan 24 10:35:20 Finished examples/compilation/ag32/proofs                        45s   4GB
Jan 24 10:35:20 Starting translator/okasaki-examples
Jan 24 10:39:28 Finished translator/okasaki-examples                           4m06s   2GB
Jan 24 10:39:29 Starting translator/other-examples
Jan 24 10:40:09 Finished translator/other-examples                               39s   1GB
Jan 24 10:40:10 Starting compiler/parsing/tests
Jan 24 10:40:35 Finished compiler/parsing/tests                                  24s 576MB
Jan 24 10:40:36 Starting compiler/inference/tests
Jan 24 10:44:37 Finished compiler/inference/tests                              4m00s   4GB
Jan 24 10:44:38 Starting compiler/bootstrap/translation
Jan 24 13:16:31 Finished compiler/bootstrap/translation                     2h31m51s  46GB
Jan 24 13:16:32 Starting unverified/sexpr-bootstrap/x64/64
Jan 24 13:24:46 Finished unverified/sexpr-bootstrap/x64/64                     8m13s  13GB
Jan 24 13:24:46 Starting unverified/sexpr-bootstrap/x64/32
Jan 24 13:30:02 Finished unverified/sexpr-bootstrap/x64/32                     5m14s  23GB
Jan 24 13:30:03 Starting compiler/bootstrap/compilation/x64/64
Jan 24 23:48:40 Finished compiler/bootstrap/compilation/x64/64             10h18m35s  64GB
Jan 24 23:48:41 Starting compiler/bootstrap/compilation/x64/64/proofs
Jan 24 23:55:26 Finished compiler/bootstrap/compilation/x64/64/proofs          6m44s  34GB
Jan 24 23:55:27 Starting compiler/bootstrap/compilation/x64/32
Jan 25 08:57:15 Finished compiler/bootstrap/compilation/x64/32              9h01m47s  64GB
Jan 25 08:57:16 Starting compiler/bootstrap/compilation/x64/32/proofs
Jan 25 09:02:57 Finished compiler/bootstrap/compilation/x64/32/proofs          5m39s  28GB
Jan 25 09:02:57 SUCCESS