Job 1174

CakeML:ea9c31be21392fff4368718527b96960080722c7
  Fix bootstrap translation of dataLang explorer [Feb 04 13:59:15]
#723 (explorer-data)
Merging into:8b42180a7ba8a82822ad811b418d4a6b78c2fd18
  Avoid fixity 470 [Feb 06 12:13:17]
HOL:2ab28aee333f79a324fa8db4805e5882e4b841e2
  Use polyscripter more in Core Theories section of DESCRIPTION [Feb 01 05:37:03]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Feb 06 12:13:48 Claimed job
Feb 06 12:13:56 Building HOL
Feb 06 12:24:04 Starting developers
Feb 06 12:24:05 Finished developers                                               0s  30MB
Feb 06 12:24:05 Starting developers/bin
Feb 06 12:24:12 Finished developers/bin                                           6s   1GB
Feb 06 12:24:12 Starting semantics/ffi
Feb 06 12:24:20 Finished semantics/ffi                                            8s 245MB
Feb 06 12:24:20 Starting semantics
Feb 06 12:29:08 Finished semantics                                             4m47s   1GB
Feb 06 12:29:08 Starting semantics/proofs
Feb 06 12:44:55 Finished semantics/proofs                                     15m46s   1GB
Feb 06 12:44:55 Starting semantics/alt_semantics
Feb 06 12:45:02 Finished semantics/alt_semantics                                  7s 307MB
Feb 06 12:45:02 Starting semantics/alt_semantics/proofs
Feb 06 12:52:15 Finished semantics/alt_semantics/proofs                        7m12s 779MB
Feb 06 12:52:15 Starting basis/pure
Feb 06 12:55:10 Finished basis/pure                                            2m53s 739MB
Feb 06 12:55:10 Starting translator
Feb 06 13:07:46 Finished translator                                           12m36s   1GB
Feb 06 13:07:46 Starting compiler/parsing
Feb 06 13:10:23 Finished compiler/parsing                                      2m36s   2GB
Feb 06 13:10:23 Starting characteristic
Feb 06 13:28:50 Finished characteristic                                       18m26s   1GB
Feb 06 13:28:50 Starting translator/monadic
Feb 06 13:30:52 Finished translator/monadic                                    2m01s   1GB
Feb 06 13:30:52 Starting basis
Feb 06 14:04:08 Finished basis                                                33m15s  19GB
Feb 06 14:04:08 Starting compiler/inference
Feb 06 14:07:40 Finished compiler/inference                                    3m32s   2GB
Feb 06 14:07:41 Starting compiler/backend/reg_alloc
Feb 06 14:08:41 Finished compiler/backend/reg_alloc                            1m00s   1GB
Feb 06 14:08:41 Starting compiler/backend/gc
Feb 06 14:12:55 Finished compiler/backend/gc                                   4m13s   2GB
Feb 06 14:12:55 Starting compiler/backend
Feb 06 14:19:49 Finished compiler/backend                                      6m53s   4GB
Feb 06 14:19:49 Starting compiler/encoders/asm
Feb 06 14:20:10 Finished compiler/encoders/asm                                   20s 728MB
Feb 06 14:20:10 Starting compiler/encoders/x64
Feb 06 14:21:22 Finished compiler/encoders/x64                                 1m11s 832MB
Feb 06 14:21:22 Starting compiler/encoders/arm7
Feb 06 14:23:09 Finished compiler/encoders/arm7                                1m46s   1GB
Feb 06 14:23:09 Starting compiler/encoders/arm8
Feb 06 14:23:41 Finished compiler/encoders/arm8                                  31s 822MB
Feb 06 14:23:41 Starting compiler/encoders/mips
Feb 06 14:25:11 Finished compiler/encoders/mips                                1m30s   1GB
Feb 06 14:25:11 Starting compiler/encoders/riscv
Feb 06 14:26:35 Finished compiler/encoders/riscv                               1m24s   1GB
Feb 06 14:26:36 Starting compiler/encoders/ag32
Feb 06 14:26:53 Finished compiler/encoders/ag32                                  16s 624MB
Feb 06 14:26:53 Starting compiler/backend/x64
Feb 06 14:27:11 Finished compiler/backend/x64                                    18s 993MB
Feb 06 14:27:11 Starting compiler/backend/arm7
Feb 06 14:27:31 Finished compiler/backend/arm7                                   19s   1GB
Feb 06 14:27:31 Starting compiler/backend/arm8
Feb 06 14:27:48 Finished compiler/backend/arm8                                   17s   1GB
Feb 06 14:27:48 Starting compiler/backend/mips
Feb 06 14:28:05 Finished compiler/backend/mips                                   16s   1GB
Feb 06 14:28:05 Starting compiler/backend/riscv
Feb 06 14:28:24 Finished compiler/backend/riscv                                  18s   1GB
Feb 06 14:28:24 Starting compiler/backend/ag32
Feb 06 14:29:39 Finished compiler/backend/ag32                                 1m14s 999MB
Feb 06 14:29:39 Starting compiler/parsing/proofs
Feb 06 14:35:31 Finished compiler/parsing/proofs                               5m51s 858MB
Feb 06 14:35:31 Starting compiler/inference/proofs
Feb 06 14:39:17 Finished compiler/inference/proofs                             3m46s   1GB
Feb 06 14:39:18 Starting compiler/backend/semantics
Feb 06 16:21:26 Finished compiler/backend/semantics                         1h42m08s   2GB
Feb 06 16:21:26 Starting compiler/backend/reg_alloc/proofs
Feb 06 16:25:07 Finished compiler/backend/reg_alloc/proofs                     3m40s 964MB
Feb 06 16:25:07 Starting compiler/backend/proofs
Feb 07 02:48:57 Finished compiler/backend/proofs                           10h23m49s  16GB
Feb 07 02:48:57 Starting compiler/encoders/x64/proofs
Feb 07 03:00:53 Finished compiler/encoders/x64/proofs                         11m56s   1GB
Feb 07 03:00:54 Starting compiler/encoders/arm7/proofs
Feb 07 03:14:53 Finished compiler/encoders/arm7/proofs                        13m58s   3GB
Feb 07 03:14:53 Starting compiler/encoders/arm8/proofs
Feb 07 03:22:05 Finished compiler/encoders/arm8/proofs                         7m11s   1GB
Feb 07 03:22:05 Starting compiler/encoders/mips/proofs
Feb 07 03:32:45 Finished compiler/encoders/mips/proofs                        10m39s   2GB
Feb 07 03:32:45 Starting compiler/encoders/riscv/proofs
Feb 07 03:42:24 Finished compiler/encoders/riscv/proofs                        9m39s   1GB
Feb 07 03:42:25 Starting compiler/encoders/ag32/proofs
Feb 07 03:45:02 Finished compiler/encoders/ag32/proofs                         2m37s 691MB
Feb 07 03:45:02 Starting compiler/backend/x64/proofs
Feb 07 03:45:22 Finished compiler/backend/x64/proofs                             19s   1GB
Feb 07 03:45:23 Starting compiler/backend/arm7/proofs
Feb 07 03:45:45 Finished compiler/backend/arm7/proofs                            21s   1GB
Feb 07 03:45:45 Starting compiler/backend/arm8/proofs
Feb 07 03:46:06 Finished compiler/backend/arm8/proofs                            21s   1GB
Feb 07 03:46:06 Starting compiler/backend/mips/proofs
Feb 07 03:46:25 Finished compiler/backend/mips/proofs                            18s   1GB
Feb 07 03:46:26 Starting compiler/backend/riscv/proofs
Feb 07 03:46:45 Finished compiler/backend/riscv/proofs                           19s   1GB
Feb 07 03:46:45 Starting compiler/backend/ag32/proofs
Feb 07 04:01:48 Finished compiler/backend/ag32/proofs                         15m01s   2GB
Feb 07 04:01:48 Starting compiler/proofs
Feb 07 04:03:36 Finished compiler/proofs                                       1m48s   4GB
Feb 07 04:03:37 Starting candle/set-theory
Feb 07 04:04:04 Finished candle/set-theory                                       27s 961MB
Feb 07 04:04:04 Starting candle/syntax-lib
Feb 07 04:04:14 Finished candle/syntax-lib                                        9s 619MB
Feb 07 04:04:14 Starting candle/standard/syntax
Feb 07 04:05:59 Finished candle/standard/syntax                                1m44s   1GB
Feb 07 04:05:59 Starting candle/standard/semantics
Feb 07 04:07:37 Finished candle/standard/semantics                             1m37s   1GB
Feb 07 04:07:37 Starting candle/standard/monadic
Feb 07 04:10:09 Finished candle/standard/monadic                               2m31s   1GB
Feb 07 04:10:09 Starting candle/standard/ml_kernel
Feb 07 04:25:25 Finished candle/standard/ml_kernel                            15m15s   3GB
Feb 07 04:25:25 Starting candle/standard/opentheory
Feb 07 04:36:56 Finished candle/standard/opentheory                           11m31s   5GB
Feb 07 04:36:56 Starting candle/standard/opentheory/compilation
Feb 07 05:11:20 Finished candle/standard/opentheory/compilation               34m23s  17GB
Feb 07 05:11:20 Starting candle/standard/opentheory/compilation/proofs
Feb 07 05:12:01 Finished candle/standard/opentheory/compilation/proofs           40s   3GB
Feb 07 05:12:01 Starting characteristic/examples
Feb 07 05:13:32 Finished characteristic/examples                               1m30s   2GB
Feb 07 05:13:32 Starting tutorial/solutions
Feb 07 05:28:31 Finished tutorial/solutions                                   14m58s   6GB
Feb 07 05:28:32 Starting translator/monadic/examples
Feb 07 05:32:13 Finished translator/monadic/examples                           3m41s   3GB
Feb 07 05:32:14 Starting examples
Feb 07 05:42:06 Finished examples                                              9m52s   3GB
Feb 07 05:42:06 Starting examples/compilation/x64
Feb 07 08:08:33 Finished examples/compilation/x64                           2h26m26s  12GB
Feb 07 08:08:33 Starting examples/compilation/x64/proofs
Feb 07 08:11:02 Finished examples/compilation/x64/proofs                       2m28s   3GB
Feb 07 08:11:02 Starting examples/compilation/ag32
Feb 07 08:52:12 Finished examples/compilation/ag32                            41m09s   6GB
Feb 07 08:52:12 Starting examples/compilation/ag32/proofs
Feb 07 08:53:47 Finished examples/compilation/ag32/proofs                      1m34s   3GB
Feb 07 08:53:48 Starting examples/cost
Feb 07 09:37:54 Finished examples/cost                                        44m06s   6GB
Feb 07 09:37:54 Starting examples/lpr_checker
Feb 07 09:41:41 Finished examples/lpr_checker                                  3m46s   2GB
Feb 07 09:41:41 Starting examples/lpr_checker/compilation
Feb 07 10:01:28 Finished examples/lpr_checker/compilation                     19m47s   8GB
Feb 07 10:01:28 Starting examples/lpr_checker/compilation/proofs
Feb 07 10:02:11 Finished examples/lpr_checker/compilation/proofs                 42s   2GB
Feb 07 10:02:11 Starting examples/lpr_checker/array
Feb 07 10:12:31 Finished examples/lpr_checker/array                           10m19s   3GB
Feb 07 10:12:31 Starting examples/lpr_checker/array/compilation
Feb 07 10:29:45 Finished examples/lpr_checker/array/compilation               17m13s   8GB
Feb 07 10:29:45 Starting examples/lpr_checker/array/compilation/proofs
Feb 07 10:32:07 Finished examples/lpr_checker/array/compilation/proofs         2m21s   4GB
Feb 07 10:32:07 Starting translator/okasaki-examples
Feb 07 10:38:45 Finished translator/okasaki-examples                           6m37s   1GB
Feb 07 10:38:45 Starting translator/other-examples
Feb 07 10:40:41 Finished translator/other-examples                             1m55s   1GB
Feb 07 10:40:41 Starting compiler/parsing/tests
Feb 07 10:41:06 Finished compiler/parsing/tests                                  24s 584MB
Feb 07 10:41:06 Starting compiler/inference/tests
Feb 07 10:45:32 Finished compiler/inference/tests                              4m25s   3GB
Feb 07 10:45:32 Starting compiler/bootstrap/translation
Feb 07 22:20:49 Finished compiler/bootstrap/translation                    11h35m16s  40GB
Feb 07 22:20:49 Starting unverified/sexpr-bootstrap/x64/64
Feb 07 22:36:19 Finished unverified/sexpr-bootstrap/x64/64                    15m29s   6GB
Feb 07 22:36:19 Starting unverified/sexpr-bootstrap/x64/32
Feb 07 22:47:11 Finished unverified/sexpr-bootstrap/x64/32                    10m52s  10GB
Feb 07 22:47:11 Starting compiler/benchmarks
Feb 07 23:26:06 Finished compiler/benchmarks                                  38m54s   2GB
Feb 07 23:26:06 Starting compiler/bootstrap/compilation/x64/64
Feb 08 15:49:43 Finished compiler/bootstrap/compilation/x64/64             16h23m36s  64GB
Feb 08 15:49:43 Starting compiler/bootstrap/compilation/x64/64/proofs
Feb 08 15:53:40 Finished compiler/bootstrap/compilation/x64/64/proofs          3m56s  16GB
Feb 08 15:53:40 Starting compiler/bootstrap/compilation/x64/32
Feb 09 06:26:10 Finished compiler/bootstrap/compilation/x64/32             14h32m29s  64GB
Feb 09 06:26:10 Starting compiler/bootstrap/compilation/x64/32/proofs
Feb 09 06:29:42 Finished compiler/bootstrap/compilation/x64/32/proofs          3m31s  14GB
Feb 09 06:29:42 Starting compiler/bootstrap/compilation/ag32/32
Feb 09 22:52:33 Finished compiler/bootstrap/compilation/ag32/32            16h22m50s  64GB
Feb 09 22:52:33 Starting compiler/bootstrap/compilation/ag32/32/proofs
Feb 10 00:03:39 Finished compiler/bootstrap/compilation/ag32/32/proofs      1h11m05s  33GB
Feb 10 00:03:39 SUCCESS