CakeML Regression Test

Job 688

CakeML:46f7ad9cc1730cf5dd01765aa230e2da66e974a0
  Remove a couple of references to FDOM_FDIFF, which is now automatic [Jan 17 01:02:33]
#605 (cleanup)
Merging into:4c7bf47ab5ec3da9da1e0f994b560d0342f6e9e1
  Merge pull request #604 from Gaj7/master [Jan 16 14:54:23]
HOL:ce7414f3a9b67a55c010a5194ca0029e347b7810
  More easily moved theorems from CakeML (this time to finite_map) [Jan 17 00:42:39]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Jan 18 03:51:56 Claimed job
Jan 18 03:52:19 Building HOL
Jan 18 04:01:35 Starting developers
Jan 18 04:01:38 Finished developers                                               2s  21MB
Jan 18 04:01:38 Starting developers/bin
Jan 18 04:02:51 Finished developers/bin                                        1m11s 916MB
Jan 18 04:02:51 Starting semantics/ffi
Jan 18 04:03:30 Finished semantics/ffi                                           37s 488MB
Jan 18 04:03:31 Starting semantics
Jan 18 04:05:08 Finished semantics                                             1m36s   1GB
Jan 18 04:05:08 Starting semantics/proofs
Jan 18 04:08:27 Finished semantics/proofs                                      3m17s 953MB
Jan 18 04:08:28 Starting basis/pure
Jan 18 04:12:02 Finished basis/pure                                            3m34s 744MB
Jan 18 04:12:03 Starting translator
Jan 18 04:13:45 Finished translator                                            1m41s   1GB
Jan 18 04:13:45 Starting compiler/parsing
Jan 18 04:14:49 Finished compiler/parsing                                      1m02s   1GB
Jan 18 04:14:49 Starting characteristic
Jan 18 04:18:10 Finished characteristic                                        3m20s   1GB
Jan 18 04:18:11 Starting translator/monadic
Jan 18 04:19:41 Finished translator/monadic                                    1m28s   1GB
Jan 18 04:19:41 Starting basis
Jan 18 04:35:43 Finished basis                                                16m01s   2GB
Jan 18 04:35:44 Starting compiler/inference
Jan 18 04:37:42 Finished compiler/inference                                    1m57s   1GB
Jan 18 04:37:43 Starting compiler/backend/reg_alloc
Jan 18 04:38:36 Finished compiler/backend/reg_alloc                              51s   1GB
Jan 18 04:38:36 Starting compiler/backend/gc
Jan 18 04:47:38 Finished compiler/backend/gc                                   9m01s   1GB
Jan 18 04:47:39 Starting compiler/backend
Jan 18 04:47:42 Finished compiler/backend                                         2s  19MB
Jan 18 04:47:43 Starting compiler/encoders/asm
Jan 18 04:47:45 Finished compiler/encoders/asm                                    1s  13MB
Jan 18 04:47:45 Starting compiler/encoders/x64
Jan 18 04:48:47 Finished compiler/encoders/x64                                 1m01s 563MB
Jan 18 04:48:48 Starting compiler/encoders/arm6
Jan 18 04:50:41 Finished compiler/encoders/arm6                                1m52s   1GB
Jan 18 04:50:41 Starting compiler/encoders/arm8
Jan 18 04:51:13 Finished compiler/encoders/arm8                                  30s 620MB
Jan 18 04:51:14 Starting compiler/encoders/mips
Jan 18 04:52:20 Finished compiler/encoders/mips                                1m05s 867MB
Jan 18 04:52:20 Starting compiler/encoders/riscv
Jan 18 04:53:28 Finished compiler/encoders/riscv                               1m07s 962MB
Jan 18 04:53:29 Starting compiler/encoders/ag32
Jan 18 04:53:47 Finished compiler/encoders/ag32                                  17s 830MB
Jan 18 04:53:47 Starting compiler/backend/x64
Jan 18 04:54:05 Finished compiler/backend/x64                                    17s 881MB
Jan 18 04:54:06 Starting compiler/backend/arm6
Jan 18 04:54:26 Finished compiler/backend/arm6                                   20s   1GB
Jan 18 04:54:27 Starting compiler/backend/arm8
Jan 18 04:54:46 Finished compiler/backend/arm8                                   18s   1GB
Jan 18 04:54:47 Starting compiler/backend/mips
Jan 18 04:55:06 Finished compiler/backend/mips                                   18s   1GB
Jan 18 04:55:07 Starting compiler/backend/riscv
Jan 18 04:55:27 Finished compiler/backend/riscv                                  19s   1GB
Jan 18 04:55:27 Starting compiler/backend/ag32
Jan 18 04:56:40 Finished compiler/backend/ag32                                 1m11s   1GB
Jan 18 04:56:40 Starting compiler/parsing/proofs
Jan 18 05:02:31 Finished compiler/parsing/proofs                               5m49s 834MB
Jan 18 05:02:31 Starting compiler/inference/proofs
Jan 18 05:05:25 Finished compiler/inference/proofs                             2m53s 946MB
Jan 18 05:05:26 Starting compiler/backend/semantics
Jan 18 05:13:01 Finished compiler/backend/semantics                            7m34s   1GB
Jan 18 05:13:02 Starting compiler/backend/reg_alloc/proofs
Jan 18 05:15:48 Finished compiler/backend/reg_alloc/proofs                     2m45s 823MB
Jan 18 05:15:48 Starting compiler/backend/proofs
Jan 18 05:54:35 Finished compiler/backend/proofs                              38m45s   3GB
Jan 18 05:54:36 Starting compiler/encoders/x64/proofs
Jan 18 06:05:19 Finished compiler/encoders/x64/proofs                         10m43s   4GB
Jan 18 06:05:20 Starting compiler/encoders/arm6/proofs
Jan 18 06:20:25 Finished compiler/encoders/arm6/proofs                        15m04s   3GB
Jan 18 06:20:26 Starting compiler/encoders/arm8/proofs
Jan 18 06:26:30 Finished compiler/encoders/arm8/proofs                         6m04s   1GB
Jan 18 06:26:31 Starting compiler/encoders/mips/proofs
Jan 18 06:37:44 Finished compiler/encoders/mips/proofs                        11m11s   2GB
Jan 18 06:37:44 Starting compiler/encoders/riscv/proofs
Jan 18 06:45:51 Finished compiler/encoders/riscv/proofs                        8m05s 934MB
Jan 18 06:45:52 Starting compiler/encoders/ag32/proofs
Jan 18 06:48:34 Finished compiler/encoders/ag32/proofs                         2m41s 616MB
Jan 18 06:48:35 Starting compiler/backend/x64/proofs
Jan 18 06:48:56 Finished compiler/backend/x64/proofs                             19s   1GB
Jan 18 06:48:56 Starting compiler/backend/arm6/proofs
Jan 18 06:49:18 Finished compiler/backend/arm6/proofs                            21s 916MB
Jan 18 06:49:19 Starting compiler/backend/arm8/proofs
Jan 18 06:49:39 Finished compiler/backend/arm8/proofs                            19s   1GB
Jan 18 06:49:40 Starting compiler/backend/mips/proofs
Jan 18 06:50:01 Finished compiler/backend/mips/proofs                            20s   1GB
Jan 18 06:50:02 Starting compiler/backend/riscv/proofs
Jan 18 06:50:23 Finished compiler/backend/riscv/proofs                           20s   1GB
Jan 18 06:50:24 Starting compiler/backend/ag32/proofs
Jan 18 06:59:36 Finished compiler/backend/ag32/proofs                          9m11s   2GB
Jan 18 06:59:37 Starting compiler/proofs
Jan 18 07:01:00 Finished compiler/proofs                                       1m22s   3GB
Jan 18 07:01:00 Starting candle/set-theory
Jan 18 07:01:27 Finished candle/set-theory                                       26s 685MB
Jan 18 07:01:28 Starting candle/syntax-lib
Jan 18 07:01:39 Finished candle/syntax-lib                                       10s 680MB
Jan 18 07:01:40 Starting candle/standard/syntax
Jan 18 07:03:31 Finished candle/standard/syntax                                1m50s 975MB
Jan 18 07:03:32 Starting candle/standard/semantics
Jan 18 07:05:15 Finished candle/standard/semantics                             1m42s 891MB
Jan 18 07:05:15 Starting candle/standard/monadic
Jan 18 07:07:02 Finished candle/standard/monadic                               1m45s   1GB
Jan 18 07:07:02 Starting candle/standard/ml_kernel
Jan 18 07:10:50 Finished candle/standard/ml_kernel                             3m46s   3GB
Jan 18 07:10:50 Starting candle/standard/opentheory
Jan 18 07:19:32 Finished candle/standard/opentheory                            8m41s   5GB
Jan 18 07:19:33 Starting candle/standard/opentheory/compilation
Jan 18 07:48:32 Finished candle/standard/opentheory/compilation               28m58s  16GB
Jan 18 07:48:33 Starting candle/standard/opentheory/compilation/proofs
Jan 18 07:49:22 Finished candle/standard/opentheory/compilation/proofs           48s   5GB
Jan 18 07:49:23 Starting characteristic/examples
Jan 18 07:50:51 Finished characteristic/examples                               1m28s   3GB
Jan 18 07:50:52 Starting tutorial/solutions
Jan 18 08:03:55 Finished tutorial/solutions                                   13m02s   6GB
Jan 18 08:03:55 Starting translator/monadic/examples
Jan 18 08:06:08 Finished translator/monadic/examples                           2m11s   2GB
Jan 18 08:06:08 Starting examples
Jan 18 08:13:42 Finished examples                                              7m33s   3GB
Jan 18 08:13:43 Starting examples/compilation/x64
Jan 18 10:15:01 Finished examples/compilation/x64                           2h01m17s   9GB
Jan 18 10:15:01 Starting examples/compilation/x64/proofs
Jan 18 10:16:51 Finished examples/compilation/x64/proofs                       1m49s   4GB
Jan 18 10:16:52 Starting examples/compilation/ag32
Jan 18 10:44:31 Finished examples/compilation/ag32                            27m38s   6GB
Jan 18 10:44:32 Starting examples/compilation/ag32/proofs
Jan 18 10:45:21 Finished examples/compilation/ag32/proofs                        48s   4GB
Jan 18 10:45:21 Starting translator/okasaki-examples
Jan 18 10:49:21 Finished translator/okasaki-examples                           3m58s   1GB
Jan 18 10:49:21 Starting translator/other-examples
Jan 18 10:52:55 Finished translator/other-examples                             3m33s   1GB
Jan 18 10:52:56 Starting compiler/parsing/tests
Jan 18 10:53:22 Finished compiler/parsing/tests                                  26s 472MB
Jan 18 10:53:23 Starting compiler/inference/tests
Jan 18 10:57:25 Finished compiler/inference/tests                              4m01s   3GB
Jan 18 10:57:26 Starting compiler/bootstrap/translation
Jan 18 13:25:59 Finished compiler/bootstrap/translation                     2h28m32s  33GB
Jan 18 13:25:59 Starting unverified/sexpr-bootstrap/x64/64
Jan 18 13:34:11 Finished unverified/sexpr-bootstrap/x64/64                     8m11s  15GB
Jan 18 13:34:12 Starting unverified/sexpr-bootstrap/x64/32
Jan 18 13:39:01 Finished unverified/sexpr-bootstrap/x64/32                     4m47s  18GB
Jan 18 13:39:01 Starting compiler/bootstrap/compilation/x64/64
Jan 18 23:35:57 Finished compiler/bootstrap/compilation/x64/64              9h56m54s  64GB
Jan 18 23:35:58 Starting compiler/bootstrap/compilation/x64/64/proofs
Jan 18 23:42:16 Finished compiler/bootstrap/compilation/x64/64/proofs          6m17s  31GB
Jan 18 23:42:16 Starting compiler/bootstrap/compilation/x64/32
Jan 19 08:54:56 Finished compiler/bootstrap/compilation/x64/32              9h12m38s  64GB
Jan 19 08:54:56 Starting compiler/bootstrap/compilation/x64/32/proofs
Jan 19 09:01:05 Finished compiler/bootstrap/compilation/x64/32/proofs          6m07s  32GB
Jan 19 09:01:05 SUCCESS