CakeML Regression Test

Job 527

CakeML:f3ddc8c130c2731129843c22c6808b348c219385
  Tweak a theorem stmt to look better in a paper [Oct 08 14:07:47]
#535 (data-to-word-tweak)
Merging into:2ce1a84a603f5e9acdd2601314dd649077ede745
  Use modules in bootstrap translation. [Oct 11 13:44:11]
HOL:32537a5663e731a4d41cf53adf51cc27b71a0e97
  Get temporal_deep/src/model_check to build by fixing Holmakefile [Oct 11 22:55:58]
Machine:oven1 4.15.9-300.fc27.x86_64 x86_64 GNU/Linux

Oct 12 15:00:44 Claimed job
Oct 12 15:00:50 Reusing HOL
Oct 12 15:01:43 Starting developers/bin
Oct 12 15:02:58 Finished developers/bin                                        1m14s 912MB
Oct 12 15:02:58 Starting semantics/ffi
Oct 12 15:03:11 Finished semantics/ffi                                           11s 270MB
Oct 12 15:03:12 Starting semantics
Oct 12 15:04:33 Finished semantics                                             1m20s 980MB
Oct 12 15:04:34 Starting semantics/proofs
Oct 12 15:07:22 Finished semantics/proofs                                      2m47s   1GB
Oct 12 15:07:23 Starting basis/pure
Oct 12 15:08:18 Finished basis/pure                                              54s 674MB
Oct 12 15:08:19 Starting translator
Oct 12 15:11:41 Finished translator                                            3m21s   1GB
Oct 12 15:11:41 Starting compiler/parsing
Oct 12 15:13:09 Finished compiler/parsing                                      1m26s   1GB
Oct 12 15:13:10 Starting characteristic
Oct 12 15:15:52 Finished characteristic                                        2m41s   1GB
Oct 12 15:15:53 Starting translator/monadic
Oct 12 15:17:23 Finished translator/monadic                                    1m29s   1GB
Oct 12 15:17:24 Starting basis
Oct 12 15:35:08 Finished basis                                                17m43s   2GB
Oct 12 15:35:09 Starting compiler/inference
Oct 12 15:37:03 Finished compiler/inference                                    1m52s   1GB
Oct 12 15:37:03 Starting compiler/backend/reg_alloc
Oct 12 15:38:08 Finished compiler/backend/reg_alloc                            1m04s 938MB
Oct 12 15:38:09 Starting compiler/backend/gc
Oct 12 15:47:28 Finished compiler/backend/gc                                   9m18s   4GB
Oct 12 15:47:28 Starting compiler/backend
Oct 12 15:47:32 Finished compiler/backend                                         3s  22MB
Oct 12 15:47:33 Starting compiler/encoders/asm
Oct 12 15:47:35 Finished compiler/encoders/asm                                    1s  12MB
Oct 12 15:47:35 Starting compiler/encoders/x64
Oct 12 15:48:27 Finished compiler/encoders/x64                                   51s 599MB
Oct 12 15:48:28 Starting compiler/encoders/arm6
Oct 12 15:50:13 Finished compiler/encoders/arm6                                1m44s   1GB
Oct 12 15:50:13 Starting compiler/encoders/arm8
Oct 12 15:50:41 Finished compiler/encoders/arm8                                  26s 467MB
Oct 12 15:50:41 Starting compiler/encoders/mips
Oct 12 15:51:39 Finished compiler/encoders/mips                                  57s 875MB
Oct 12 15:51:40 Starting compiler/encoders/riscv
Oct 12 15:52:41 Finished compiler/encoders/riscv                               1m00s 871MB
Oct 12 15:52:41 Starting compiler/backend/x64
Oct 12 15:53:00 Finished compiler/backend/x64                                    18s   1GB
Oct 12 15:53:01 Starting compiler/backend/arm6
Oct 12 15:53:21 Finished compiler/backend/arm6                                   19s   1GB
Oct 12 15:53:22 Starting compiler/backend/arm8
Oct 12 15:53:42 Finished compiler/backend/arm8                                   18s   1GB
Oct 12 15:53:42 Starting compiler/backend/mips
Oct 12 15:54:02 Finished compiler/backend/mips                                   19s   1GB
Oct 12 15:54:03 Starting compiler/backend/riscv
Oct 12 15:54:23 Finished compiler/backend/riscv                                  18s   1GB
Oct 12 15:54:23 Starting compiler/parsing/proofs
Oct 12 16:00:27 Finished compiler/parsing/proofs                               6m02s 795MB
Oct 12 16:00:27 Starting compiler/inference/proofs
Oct 12 16:03:19 Finished compiler/inference/proofs                             2m50s   1GB
Oct 12 16:03:20 Starting compiler/backend/semantics
Oct 12 16:12:09 Finished compiler/backend/semantics                            8m48s   1GB
Oct 12 16:12:09 Starting compiler/backend/reg_alloc/proofs
Oct 12 16:19:16 Finished compiler/backend/reg_alloc/proofs                     7m05s 515MB
Oct 12 16:19:16 Starting compiler/backend/proofs
Oct 12 17:00:13 Finished compiler/backend/proofs                              40m56s   4GB
Oct 12 17:00:14 Starting compiler/encoders/x64/proofs
Oct 12 17:07:35 Finished compiler/encoders/x64/proofs                          7m20s   5GB
Oct 12 17:07:36 Starting compiler/encoders/arm6/proofs
Oct 12 17:15:09 Finished compiler/encoders/arm6/proofs                         7m32s   2GB
Oct 12 17:15:09 Starting compiler/encoders/arm8/proofs
Oct 12 17:20:26 Finished compiler/encoders/arm8/proofs                         5m16s 988MB
Oct 12 17:20:27 Starting compiler/encoders/mips/proofs
Oct 12 17:27:50 Finished compiler/encoders/mips/proofs                         7m22s   1GB
Oct 12 17:27:51 Starting compiler/encoders/riscv/proofs
Oct 12 17:35:47 Finished compiler/encoders/riscv/proofs                        7m55s 748MB
Oct 12 17:35:48 Starting compiler/backend/x64/proofs
Oct 12 17:36:08 Finished compiler/backend/x64/proofs                             20s   1GB
Oct 12 17:36:09 Starting compiler/backend/arm6/proofs
Oct 12 17:36:33 Finished compiler/backend/arm6/proofs                            23s   1GB
Oct 12 17:36:34 Starting compiler/backend/arm8/proofs
Oct 12 17:36:54 Finished compiler/backend/arm8/proofs                            19s 776MB
Oct 12 17:36:54 Starting compiler/backend/mips/proofs
Oct 12 17:37:17 Finished compiler/backend/mips/proofs                            21s   1GB
Oct 12 17:37:17 Starting compiler/backend/riscv/proofs
Oct 12 17:37:39 Finished compiler/backend/riscv/proofs                           20s   1GB
Oct 12 17:37:40 Starting compiler/proofs
Oct 12 17:38:59 Finished compiler/proofs                                       1m18s   2GB
Oct 12 17:39:00 Starting candle/set-theory
Oct 12 17:39:26 Finished candle/set-theory                                       25s 598MB
Oct 12 17:39:27 Starting candle/syntax-lib
Oct 12 17:39:38 Finished candle/syntax-lib                                       10s 624MB
Oct 12 17:39:39 Starting candle/standard/syntax
Oct 12 17:41:12 Finished candle/standard/syntax                                1m32s 525MB
Oct 12 17:41:12 Starting candle/standard/semantics
Oct 12 17:42:34 Finished candle/standard/semantics                             1m21s   1GB
Oct 12 17:42:34 Starting candle/standard/monadic
Oct 12 17:44:09 Finished candle/standard/monadic                               1m33s   1GB
Oct 12 17:44:10 Starting candle/standard/ml_kernel
Oct 12 17:59:57 Finished candle/standard/ml_kernel                            15m46s   5GB
Oct 12 17:59:58 Starting candle/standard/opentheory
Oct 12 18:08:42 Finished candle/standard/opentheory                            8m43s   5GB
Oct 12 18:08:43 Starting candle/standard/opentheory/compilation
Oct 12 18:43:10 Finished candle/standard/opentheory/compilation               34m26s  17GB
Oct 12 18:43:11 Starting characteristic/examples
Oct 12 18:44:47 Finished characteristic/examples                               1m35s   1GB
Oct 12 18:44:47 Starting tutorial/solutions
Oct 12 18:58:17 Finished tutorial/solutions                                   13m28s   6GB
Oct 12 18:58:17 Starting translator/monadic/examples
Oct 12 19:00:03 Finished translator/monadic/examples                           1m45s   2GB
Oct 12 19:00:04 Starting examples
Oct 12 19:05:46 Finished examples                                              5m42s   4GB
Oct 12 19:05:47 Starting examples/compilation
Oct 12 21:01:51 Finished examples/compilation                               1h56m02s   8GB
Oct 12 21:01:51 Starting examples/compilation/proofs
Oct 12 21:03:47 Finished examples/compilation/proofs                           1m55s   3GB
Oct 12 21:03:48 Starting compiler/benchmarks
Oct 12 21:03:49 Finished compiler/benchmarks                                      0s   4MB
Oct 12 21:03:49 Starting translator/okasaki-examples
Oct 12 21:07:18 Finished translator/okasaki-examples                           3m28s   1GB
Oct 12 21:07:19 Starting translator/other-examples
Oct 12 21:10:51 Finished translator/other-examples                             3m30s 850MB
Oct 12 21:10:51 Starting compiler/parsing/tests
Oct 12 21:11:17 Finished compiler/parsing/tests                                  25s 286MB
Oct 12 21:11:18 Starting compiler/inference/tests
Oct 12 21:15:20 Finished compiler/inference/tests                              4m00s   3GB
Oct 12 21:15:20 Starting compiler/bootstrap/translation
Oct 13 03:23:49 Finished compiler/bootstrap/translation                     6h08m27s  53GB
Oct 13 03:23:49 Starting unverified/sexpr-bootstrap/x64/64
Oct 13 03:31:50 Finished unverified/sexpr-bootstrap/x64/64                     7m59s  14GB
Oct 13 03:31:51 Starting unverified/sexpr-bootstrap/x64/32
Oct 13 03:37:18 Finished unverified/sexpr-bootstrap/x64/32                     5m26s  18GB
Oct 13 03:37:19 Starting compiler/bootstrap/compilation/x64/64
Oct 13 19:04:54 Finished compiler/bootstrap/compilation/x64/64             15h27m33s  64GB
Oct 13 19:04:54 Starting compiler/bootstrap/compilation/x64/64/proofs
Oct 13 19:08:13 Finished compiler/bootstrap/compilation/x64/64/proofs          3m18s  24GB
Oct 13 19:08:14 Starting compiler/bootstrap/compilation/x64/32
Oct 14 05:01:46 Finished compiler/bootstrap/compilation/x64/32              9h53m31s  64GB
Oct 14 05:01:47 Starting compiler/bootstrap/compilation/x64/32/proofs
Oct 14 05:05:10 Finished compiler/bootstrap/compilation/x64/32/proofs          3m22s  21GB
Oct 14 05:05:11 SUCCESS