Job 1183

CakeML:98517e4fe4c021fed1618b82a5929ad6de54806b
  Remove some inventing type variable messages [Feb 10 04:41:43]
#714 (nopacklib)
Merging into:658771300986c1238e414b06f1443f7f4f08424a
  Merge pull request #723 from talsewell/explorer-data [Feb 11 23:28:15]
HOL:bbc6f9a1dc624543ead89ce3c72e7a8d773e37db
  Added BOREL_INDUCT (was: Induct_on_Borel_functions) [Feb 09 23:16:11]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Feb 13 22:15:01 Claimed job
Feb 13 22:15:05 Reusing HOL
Feb 13 22:15:58 Starting developers
Feb 13 22:16:02 Finished developers                                               4s 108MB
Feb 13 22:16:03 Starting developers/bin
Feb 13 22:17:47 Finished developers/bin                                        1m43s   1GB
Feb 13 22:17:47 Starting semantics/ffi
Feb 13 22:17:58 Finished semantics/ffi                                           10s 243MB
Feb 13 22:17:58 Starting semantics
Feb 13 22:19:20 Finished semantics                                             1m21s   1GB
Feb 13 22:19:20 Starting semantics/proofs
Feb 13 22:22:47 Finished semantics/proofs                                      3m26s 980MB
Feb 13 22:22:47 Starting semantics/alt_semantics
Feb 13 22:22:56 Finished semantics/alt_semantics                                  8s 305MB
Feb 13 22:22:56 Starting semantics/alt_semantics/proofs
Feb 13 22:25:05 Finished semantics/alt_semantics/proofs                        2m09s 787MB
Feb 13 22:25:05 Starting basis/pure
Feb 13 22:25:55 Finished basis/pure                                              49s 819MB
Feb 13 22:25:55 Starting translator
Feb 13 22:28:32 Finished translator                                            2m36s   1GB
Feb 13 22:28:32 Starting compiler/parsing
Feb 13 22:29:42 Finished compiler/parsing                                      1m10s   3GB
Feb 13 22:29:43 Starting characteristic
Feb 13 22:35:43 Finished characteristic                                        6m00s   2GB
Feb 13 22:35:43 Starting translator/monadic
Feb 13 22:37:19 Finished translator/monadic                                    1m35s   1GB
Feb 13 22:37:19 Starting basis
Feb 13 23:10:31 Finished basis                                                33m11s  17GB
Feb 13 23:10:32 Starting compiler/inference
Feb 13 23:12:43 Finished compiler/inference                                    2m11s   2GB
Feb 13 23:12:43 Starting compiler/backend/reg_alloc
Feb 13 23:13:46 Finished compiler/backend/reg_alloc                            1m02s   1GB
Feb 13 23:13:46 Starting compiler/backend/gc
Feb 13 23:17:03 Finished compiler/backend/gc                                   3m16s   2GB
Feb 13 23:17:03 Starting compiler/backend
Feb 13 23:21:33 Finished compiler/backend                                      4m29s   3GB
Feb 13 23:21:33 Starting compiler/encoders/asm
Feb 13 23:21:56 Finished compiler/encoders/asm                                   22s 813MB
Feb 13 23:21:56 Starting compiler/encoders/x64
Feb 13 23:22:21 Finished compiler/encoders/x64                                   24s 833MB
Feb 13 23:22:21 Starting compiler/encoders/arm7
Feb 13 23:23:10 Finished compiler/encoders/arm7                                  48s 634MB
Feb 13 23:23:10 Starting compiler/encoders/arm8
Feb 13 23:23:24 Finished compiler/encoders/arm8                                  12s 929MB
Feb 13 23:23:24 Starting compiler/encoders/mips
Feb 13 23:23:41 Finished compiler/encoders/mips                                  17s   1GB
Feb 13 23:23:42 Starting compiler/encoders/riscv
Feb 13 23:23:57 Finished compiler/encoders/riscv                                 15s 819MB
Feb 13 23:23:57 Starting compiler/encoders/ag32
Feb 13 23:24:16 Finished compiler/encoders/ag32                                  18s 584MB
Feb 13 23:24:16 Starting compiler/backend/x64
Feb 13 23:24:35 Finished compiler/backend/x64                                    18s   1GB
Feb 13 23:24:35 Starting compiler/backend/arm7
Feb 13 23:24:55 Finished compiler/backend/arm7                                   19s   1GB
Feb 13 23:24:55 Starting compiler/backend/arm8
Feb 13 23:25:12 Finished compiler/backend/arm8                                   17s   1GB
Feb 13 23:25:13 Starting compiler/backend/mips
Feb 13 23:25:32 Finished compiler/backend/mips                                   18s   1GB
Feb 13 23:25:32 Starting compiler/backend/riscv
Feb 13 23:25:52 Finished compiler/backend/riscv                                  19s   1GB
Feb 13 23:25:52 Starting compiler/backend/ag32
Feb 13 23:27:03 Finished compiler/backend/ag32                                 1m10s 886MB
Feb 13 23:27:03 Starting compiler/parsing/proofs
Feb 13 23:32:49 Finished compiler/parsing/proofs                               5m46s   1GB
Feb 13 23:32:50 Starting compiler/inference/proofs
Feb 13 23:35:56 Finished compiler/inference/proofs                             3m06s   1GB
Feb 13 23:35:56 Starting compiler/backend/semantics
Feb 14 00:06:51 Finished compiler/backend/semantics                           30m53s   1GB
Feb 14 00:06:51 Starting compiler/backend/reg_alloc/proofs
Feb 14 00:10:36 Finished compiler/backend/reg_alloc/proofs                     3m45s 739MB
Feb 14 00:10:37 Starting compiler/backend/proofs
Feb 14 01:18:09 Finished compiler/backend/proofs                            1h07m32s  14GB
Feb 14 01:18:09 Starting compiler/encoders/x64/proofs
Feb 14 01:28:00 Finished compiler/encoders/x64/proofs                          9m49s   4GB
Feb 14 01:28:00 Starting compiler/encoders/arm7/proofs
Feb 14 01:41:16 Finished compiler/encoders/arm7/proofs                        13m15s   3GB
Feb 14 01:41:16 Starting compiler/encoders/arm8/proofs
Feb 14 01:47:56 Finished compiler/encoders/arm8/proofs                         6m39s   1GB
Feb 14 01:47:56 Starting compiler/encoders/mips/proofs
Feb 14 01:57:55 Finished compiler/encoders/mips/proofs                         9m58s   2GB
Feb 14 01:57:55 Starting compiler/encoders/riscv/proofs
Feb 14 02:06:43 Finished compiler/encoders/riscv/proofs                        8m47s   1GB
Feb 14 02:06:43 Starting compiler/encoders/ag32/proofs
Feb 14 02:09:22 Finished compiler/encoders/ag32/proofs                         2m39s 789MB
Feb 14 02:09:23 Starting compiler/backend/x64/proofs
Feb 14 02:09:44 Finished compiler/backend/x64/proofs                             20s   1GB
Feb 14 02:09:44 Starting compiler/backend/arm7/proofs
Feb 14 02:10:06 Finished compiler/backend/arm7/proofs                            21s   1GB
Feb 14 02:10:06 Starting compiler/backend/arm8/proofs
Feb 14 02:10:26 Finished compiler/backend/arm8/proofs                            19s   1GB
Feb 14 02:10:27 Starting compiler/backend/mips/proofs
Feb 14 02:10:48 Finished compiler/backend/mips/proofs                            20s   1GB
Feb 14 02:10:48 Starting compiler/backend/riscv/proofs
Feb 14 02:11:09 Finished compiler/backend/riscv/proofs                           20s   1GB
Feb 14 02:11:09 Starting compiler/backend/ag32/proofs
Feb 14 02:24:29 Finished compiler/backend/ag32/proofs                         13m18s   2GB
Feb 14 02:24:29 Starting compiler/proofs
Feb 14 02:26:01 Finished compiler/proofs                                       1m32s   3GB
Feb 14 02:26:02 Starting candle/set-theory
Feb 14 02:26:30 Finished candle/set-theory                                       28s 711MB
Feb 14 02:26:30 Starting candle/syntax-lib
Feb 14 02:26:41 Finished candle/syntax-lib                                       10s 562MB
Feb 14 02:26:41 Starting candle/standard/syntax
Feb 14 02:28:32 Finished candle/standard/syntax                                1m50s 925MB
Feb 14 02:28:32 Starting candle/standard/semantics
Feb 14 02:30:17 Finished candle/standard/semantics                             1m44s 914MB
Feb 14 02:30:17 Starting candle/standard/monadic
Feb 14 02:32:00 Finished candle/standard/monadic                               1m42s   1GB
Feb 14 02:32:00 Starting candle/standard/ml_kernel
Feb 14 02:37:27 Finished candle/standard/ml_kernel                             5m26s   4GB
Feb 14 02:37:27 Starting candle/standard/opentheory
Feb 14 02:46:56 Finished candle/standard/opentheory                            9m28s   5GB
Feb 14 02:46:56 Starting candle/standard/opentheory/compilation
Feb 14 03:19:09 Finished candle/standard/opentheory/compilation               32m12s  16GB
Feb 14 03:19:10 Starting candle/standard/opentheory/compilation/proofs
Feb 14 03:19:47 Finished candle/standard/opentheory/compilation/proofs           37s   3GB
Feb 14 03:19:48 Starting characteristic/examples
Feb 14 03:21:03 Finished characteristic/examples                               1m14s   2GB
Feb 14 03:21:03 Starting tutorial/solutions
Feb 14 03:35:42 Finished tutorial/solutions                                   14m38s   7GB
Feb 14 03:35:42 Starting translator/monadic/examples
Feb 14 03:38:46 Finished translator/monadic/examples                           3m04s   2GB
Feb 14 03:38:47 Starting examples
Feb 14 03:47:11 Finished examples                                              8m24s   5GB
Feb 14 03:47:11 Starting examples/compilation/x64
Feb 14 06:03:14 Finished examples/compilation/x64                           2h16m02s  13GB
Feb 14 06:03:15 Starting examples/compilation/x64/proofs
Feb 14 06:04:47 Finished examples/compilation/x64/proofs                       1m32s   2GB
Feb 14 06:04:47 Starting examples/compilation/ag32
Feb 14 06:36:09 Finished examples/compilation/ag32                            31m21s   6GB
Feb 14 06:36:09 Starting examples/compilation/ag32/proofs
Feb 14 06:37:01 Finished examples/compilation/ag32/proofs                        51s   3GB
Feb 14 06:37:01 Starting examples/cost
Feb 14 07:19:45 Finished examples/cost                                        42m43s   6GB
Feb 14 07:19:45 Starting examples/lpr_checker
Feb 14 07:23:26 Finished examples/lpr_checker                                  3m40s   2GB
Feb 14 07:23:26 Starting examples/lpr_checker/compilation
Feb 14 07:40:18 Finished examples/lpr_checker/compilation                     16m51s  10GB
Feb 14 07:40:18 Starting examples/lpr_checker/compilation/proofs
Feb 14 07:40:54 Finished examples/lpr_checker/compilation/proofs                 35s   2GB
Feb 14 07:40:55 Starting examples/lpr_checker/array
Feb 14 07:49:07 Finished examples/lpr_checker/array                            8m11s   3GB
Feb 14 07:49:07 Starting examples/lpr_checker/array/compilation
Feb 14 08:05:02 Finished examples/lpr_checker/array/compilation               15m54s   7GB
Feb 14 08:05:02 Starting examples/lpr_checker/array/compilation/proofs
Feb 14 08:05:46 Finished examples/lpr_checker/array/compilation/proofs           43s   3GB
Feb 14 08:05:46 Starting translator/okasaki-examples
Feb 14 08:10:12 Finished translator/okasaki-examples                           4m25s   1GB
Feb 14 08:10:12 Starting translator/other-examples
Feb 14 08:10:54 Finished translator/other-examples                               41s   1GB
Feb 14 08:10:54 Starting compiler/parsing/tests
Feb 14 08:11:20 Finished compiler/parsing/tests                                  25s 479MB
Feb 14 08:11:20 Starting compiler/inference/tests
Feb 14 08:15:46 Finished compiler/inference/tests                              4m26s   4GB
Feb 14 08:15:47 Starting compiler/bootstrap/translation
Feb 14 12:03:51 Finished compiler/bootstrap/translation                     3h48m03s  38GB
Feb 14 12:03:51 Starting unverified/sexpr-bootstrap/x64/64
Feb 14 12:17:56 Finished unverified/sexpr-bootstrap/x64/64                    14m04s   4GB
Feb 14 12:17:56 Starting unverified/sexpr-bootstrap/x64/32
Feb 14 12:27:57 Finished unverified/sexpr-bootstrap/x64/32                    10m00s   8GB
Feb 14 12:27:57 Starting compiler/benchmarks
Feb 14 12:27:59 Finished compiler/benchmarks                                      1s  26MB
Feb 14 12:28:00 Starting compiler/bootstrap/compilation/x64/64
Feb 15 03:20:05 Finished compiler/bootstrap/compilation/x64/64             14h52m05s  64GB
Feb 15 03:20:05 Starting compiler/bootstrap/compilation/x64/64/proofs
Feb 15 03:23:12 Finished compiler/bootstrap/compilation/x64/64/proofs          3m06s  13GB
Feb 15 03:23:12 Starting compiler/bootstrap/compilation/x64/32
Feb 15 16:55:32 Finished compiler/bootstrap/compilation/x64/32             13h32m19s  64GB
Feb 15 16:55:32 Starting compiler/bootstrap/compilation/x64/32/proofs
Feb 15 16:58:27 Finished compiler/bootstrap/compilation/x64/32/proofs          2m55s  12GB
Feb 15 16:58:28 Starting compiler/bootstrap/compilation/ag32/32
Feb 16 07:52:35 Finished compiler/bootstrap/compilation/ag32/32            14h54m07s  64GB
Feb 16 07:52:36 Starting compiler/bootstrap/compilation/ag32/32/proofs
Feb 16 08:18:00 Finished compiler/bootstrap/compilation/ag32/32/proofs        25m24s  29GB
Feb 16 08:18:00 SUCCESS