Job 1178

CakeML:ea9c31be21392fff4368718527b96960080722c7
  Fix bootstrap translation of dataLang explorer [Feb 04 13:59:15]
#723 (explorer-data)
Merging into:bc31859d41b156f0209a253ab1cee3f334e9b742
  Fix type error caused by HOL change to ThmSetData API [Feb 10 03:15:23]
HOL:1ada1617c02bd7b9335a433e842dc2590e539c6b
  Revert "Eta-expand GEN_REWRITE_CONV so that bounded rewrites work bet [Feb 08 01:35:04]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Feb 10 05:15:04 Claimed job
Feb 10 05:16:46 Building HOL
Feb 10 05:28:08 Starting developers
Feb 10 05:28:13 Finished developers                                               4s  87MB
Feb 10 05:28:13 Starting developers/bin
Feb 10 05:29:56 Finished developers/bin                                        1m42s   1GB
Feb 10 05:29:56 Starting semantics/ffi
Feb 10 05:30:07 Finished semantics/ffi                                           10s 220MB
Feb 10 05:30:07 Starting semantics
Feb 10 05:31:38 Finished semantics                                             1m31s 918MB
Feb 10 05:31:39 Starting semantics/proofs
Feb 10 05:35:09 Finished semantics/proofs                                      3m29s   1GB
Feb 10 05:35:09 Starting semantics/alt_semantics
Feb 10 05:35:18 Finished semantics/alt_semantics                                  8s 264MB
Feb 10 05:35:18 Starting semantics/alt_semantics/proofs
Feb 10 05:37:28 Finished semantics/alt_semantics/proofs                        2m09s 831MB
Feb 10 05:37:29 Starting basis/pure
Feb 10 05:40:31 Finished basis/pure                                            3m01s 855MB
Feb 10 05:40:31 Starting translator
Feb 10 05:43:08 Finished translator                                            2m37s   1GB
Feb 10 05:43:09 Starting compiler/parsing
Feb 10 05:44:21 Finished compiler/parsing                                      1m11s   1GB
Feb 10 05:44:21 Starting characteristic
Feb 10 05:50:18 Finished characteristic                                        5m56s   1GB
Feb 10 05:50:18 Starting translator/monadic
Feb 10 05:51:55 Finished translator/monadic                                    1m37s   1GB
Feb 10 05:51:55 Starting basis
Feb 10 06:27:20 Finished basis                                                35m24s  13GB
Feb 10 06:27:21 Starting compiler/inference
Feb 10 06:29:41 Finished compiler/inference                                    2m20s   2GB
Feb 10 06:29:41 Starting compiler/backend/reg_alloc
Feb 10 06:30:45 Finished compiler/backend/reg_alloc                            1m03s   1GB
Feb 10 06:30:45 Starting compiler/backend/gc
Feb 10 06:34:22 Finished compiler/backend/gc                                   3m36s   1GB
Feb 10 06:34:22 Starting compiler/backend
Feb 10 06:38:55 Finished compiler/backend                                      4m33s   3GB
Feb 10 06:38:56 Starting compiler/encoders/asm
Feb 10 06:39:18 Finished compiler/encoders/asm                                   22s 820MB
Feb 10 06:39:19 Starting compiler/encoders/x64
Feb 10 06:40:17 Finished compiler/encoders/x64                                   58s 869MB
Feb 10 06:40:17 Starting compiler/encoders/arm7
Feb 10 06:42:08 Finished compiler/encoders/arm7                                1m50s   1GB
Feb 10 06:42:08 Starting compiler/encoders/arm8
Feb 10 06:42:42 Finished compiler/encoders/arm8                                  33s 653MB
Feb 10 06:42:42 Starting compiler/encoders/mips
Feb 10 06:43:54 Finished compiler/encoders/mips                                1m11s   1GB
Feb 10 06:43:54 Starting compiler/encoders/riscv
Feb 10 06:45:21 Finished compiler/encoders/riscv                               1m26s 732MB
Feb 10 06:45:21 Starting compiler/encoders/ag32
Feb 10 06:45:39 Finished compiler/encoders/ag32                                  17s 795MB
Feb 10 06:45:39 Starting compiler/backend/x64
Feb 10 06:45:58 Finished compiler/backend/x64                                    18s   1GB
Feb 10 06:45:58 Starting compiler/backend/arm7
Feb 10 06:46:18 Finished compiler/backend/arm7                                   19s   1GB
Feb 10 06:46:19 Starting compiler/backend/arm8
Feb 10 06:46:36 Finished compiler/backend/arm8                                   17s 991MB
Feb 10 06:46:37 Starting compiler/backend/mips
Feb 10 06:46:56 Finished compiler/backend/mips                                   19s   1GB
Feb 10 06:46:56 Starting compiler/backend/riscv
Feb 10 06:47:16 Finished compiler/backend/riscv                                  19s   1GB
Feb 10 06:47:16 Starting compiler/backend/ag32
Feb 10 06:48:28 Finished compiler/backend/ag32                                 1m11s   1GB
Feb 10 06:48:29 Starting compiler/parsing/proofs
Feb 10 06:54:21 Finished compiler/parsing/proofs                               5m52s 876MB
Feb 10 06:54:22 Starting compiler/inference/proofs
Feb 10 06:57:30 Finished compiler/inference/proofs                             3m07s   1GB
Feb 10 06:57:30 Starting compiler/backend/semantics
Feb 10 07:28:14 Finished compiler/backend/semantics                           30m44s   2GB
Feb 10 07:28:15 Starting compiler/backend/reg_alloc/proofs
Feb 10 07:31:53 Finished compiler/backend/reg_alloc/proofs                     3m38s 879MB
Feb 10 07:31:53 Starting compiler/backend/proofs
Feb 10 08:39:03 Finished compiler/backend/proofs                            1h07m08s  15GB
Feb 10 08:39:03 Starting compiler/encoders/x64/proofs
Feb 10 08:48:55 Finished compiler/encoders/x64/proofs                          9m51s   4GB
Feb 10 08:48:55 Starting compiler/encoders/arm7/proofs
Feb 10 09:02:19 Finished compiler/encoders/arm7/proofs                        13m23s   3GB
Feb 10 09:02:20 Starting compiler/encoders/arm8/proofs
Feb 10 09:09:02 Finished compiler/encoders/arm8/proofs                         6m42s   1GB
Feb 10 09:09:03 Starting compiler/encoders/mips/proofs
Feb 10 09:19:04 Finished compiler/encoders/mips/proofs                        10m00s   2GB
Feb 10 09:19:04 Starting compiler/encoders/riscv/proofs
Feb 10 09:28:10 Finished compiler/encoders/riscv/proofs                        9m05s   1GB
Feb 10 09:28:10 Starting compiler/encoders/ag32/proofs
Feb 10 09:30:49 Finished compiler/encoders/ag32/proofs                         2m38s 737MB
Feb 10 09:30:49 Starting compiler/backend/x64/proofs
Feb 10 09:31:10 Finished compiler/backend/x64/proofs                             21s   1GB
Feb 10 09:31:11 Starting compiler/backend/arm7/proofs
Feb 10 09:31:32 Finished compiler/backend/arm7/proofs                            21s   1GB
Feb 10 09:31:33 Starting compiler/backend/arm8/proofs
Feb 10 09:31:52 Finished compiler/backend/arm8/proofs                            19s   1GB
Feb 10 09:31:53 Starting compiler/backend/mips/proofs
Feb 10 09:32:13 Finished compiler/backend/mips/proofs                            19s   1GB
Feb 10 09:32:13 Starting compiler/backend/riscv/proofs
Feb 10 09:32:34 Finished compiler/backend/riscv/proofs                           20s   1GB
Feb 10 09:32:34 Starting compiler/backend/ag32/proofs
Feb 10 09:46:04 Finished compiler/backend/ag32/proofs                         13m29s   3GB
Feb 10 09:46:04 Starting compiler/proofs
Feb 10 09:47:52 Finished compiler/proofs                                       1m47s   2GB
Feb 10 09:47:52 Starting candle/set-theory
Feb 10 09:48:21 Finished candle/set-theory                                       28s 672MB
Feb 10 09:48:22 Starting candle/syntax-lib
Feb 10 09:48:32 Finished candle/syntax-lib                                       10s 670MB
Feb 10 09:48:32 Starting candle/standard/syntax
Feb 10 09:50:23 Finished candle/standard/syntax                                1m50s   1GB
Feb 10 09:50:23 Starting candle/standard/semantics
Feb 10 09:52:08 Finished candle/standard/semantics                             1m44s   1GB
Feb 10 09:52:08 Starting candle/standard/monadic
Feb 10 09:53:51 Finished candle/standard/monadic                               1m43s   1GB
Feb 10 09:53:51 Starting candle/standard/ml_kernel
Feb 10 09:59:23 Finished candle/standard/ml_kernel                             5m30s   5GB
Feb 10 09:59:23 Starting candle/standard/opentheory
Feb 10 10:09:23 Finished candle/standard/opentheory                           10m00s   3GB
Feb 10 10:09:23 Starting candle/standard/opentheory/compilation
Feb 10 10:40:55 Finished candle/standard/opentheory/compilation               31m31s  13GB
Feb 10 10:40:55 Starting candle/standard/opentheory/compilation/proofs
Feb 10 10:41:34 Finished candle/standard/opentheory/compilation/proofs           38s   2GB
Feb 10 10:41:34 Starting characteristic/examples
Feb 10 10:43:08 Finished characteristic/examples                               1m34s   2GB
Feb 10 10:43:09 Starting tutorial/solutions
Feb 10 10:57:56 Finished tutorial/solutions                                   14m47s   7GB
Feb 10 10:57:56 Starting translator/monadic/examples
Feb 10 11:00:57 Finished translator/monadic/examples                           3m00s   2GB
Feb 10 11:00:58 Starting examples
Feb 10 11:10:44 Finished examples                                              9m45s   3GB
Feb 10 11:10:44 Starting examples/compilation/x64
Feb 10 13:29:30 Finished examples/compilation/x64                           2h18m46s  12GB
Feb 10 13:29:31 Starting examples/compilation/x64/proofs
Feb 10 13:31:13 Finished examples/compilation/x64/proofs                       1m42s   3GB
Feb 10 13:31:14 Starting examples/compilation/ag32
Feb 10 14:02:39 Finished examples/compilation/ag32                            31m25s   7GB
Feb 10 14:02:39 Starting examples/compilation/ag32/proofs
Feb 10 14:03:24 Finished examples/compilation/ag32/proofs                        44s   2GB
Feb 10 14:03:24 Starting examples/cost
Feb 10 14:46:26 Finished examples/cost                                        43m01s   6GB
Feb 10 14:46:27 Starting examples/lpr_checker
Feb 10 14:50:17 Finished examples/lpr_checker                                  3m49s   3GB
Feb 10 14:50:17 Starting examples/lpr_checker/compilation
Feb 10 15:07:22 Finished examples/lpr_checker/compilation                     17m05s   8GB
Feb 10 15:07:23 Starting examples/lpr_checker/compilation/proofs
Feb 10 15:08:01 Finished examples/lpr_checker/compilation/proofs                 38s   2GB
Feb 10 15:08:01 Starting examples/lpr_checker/array
Feb 10 15:17:45 Finished examples/lpr_checker/array                            9m43s   3GB
Feb 10 15:17:45 Starting examples/lpr_checker/array/compilation
Feb 10 15:33:41 Finished examples/lpr_checker/array/compilation               15m56s   9GB
Feb 10 15:33:42 Starting examples/lpr_checker/array/compilation/proofs
Feb 10 15:34:25 Finished examples/lpr_checker/array/compilation/proofs           42s   3GB
Feb 10 15:34:25 Starting translator/okasaki-examples
Feb 10 15:38:52 Finished translator/okasaki-examples                           4m26s   1GB
Feb 10 15:38:52 Starting translator/other-examples
Feb 10 15:40:56 Finished translator/other-examples                             2m02s   1GB
Feb 10 15:40:56 Starting compiler/parsing/tests
Feb 10 15:41:22 Finished compiler/parsing/tests                                  25s 576MB
Feb 10 15:41:22 Starting compiler/inference/tests
Feb 10 15:46:00 Finished compiler/inference/tests                              4m37s   4GB
Feb 10 15:46:00 Starting compiler/bootstrap/translation
Feb 10 19:35:33 Finished compiler/bootstrap/translation                     3h49m32s  46GB
Feb 10 19:35:33 Starting unverified/sexpr-bootstrap/x64/64
Feb 10 19:50:09 Finished unverified/sexpr-bootstrap/x64/64                    14m34s   8GB
Feb 10 19:50:09 Starting unverified/sexpr-bootstrap/x64/32
Feb 10 20:00:30 Finished unverified/sexpr-bootstrap/x64/32                    10m21s   9GB
Feb 10 20:00:31 Starting compiler/benchmarks
Feb 10 20:00:33 Finished compiler/benchmarks                                      1s  35MB
Feb 10 20:00:33 Starting compiler/bootstrap/compilation/x64/64
Feb 11 11:04:34 Finished compiler/bootstrap/compilation/x64/64             15h04m00s  64GB
Feb 11 11:04:35 Starting compiler/bootstrap/compilation/x64/64/proofs
Feb 11 11:08:25 Finished compiler/bootstrap/compilation/x64/64/proofs          3m49s  16GB
Feb 11 11:08:25 Starting compiler/bootstrap/compilation/x64/32
Feb 12 00:35:32 Finished compiler/bootstrap/compilation/x64/32             13h27m05s  64GB
Feb 12 00:35:33 Starting compiler/bootstrap/compilation/x64/32/proofs
Feb 12 00:39:13 Finished compiler/bootstrap/compilation/x64/32/proofs          3m40s  14GB
Feb 12 00:39:13 Starting compiler/bootstrap/compilation/ag32/32
Feb 12 15:34:53 Finished compiler/bootstrap/compilation/ag32/32            14h55m38s  64GB
Feb 12 15:34:53 Starting compiler/bootstrap/compilation/ag32/32/proofs
Feb 12 15:52:20 Finished compiler/bootstrap/compilation/ag32/32/proofs        17m27s  32GB
Feb 12 15:52:21 SUCCESS