Job 812

CakeML:fcc5a94f9d5425e6b678ee610a9226cab8fa20bf
  Fix bug in recursive post-processing of monadic translator [Apr 15 15:51:13]
#627 (monadic-trans-cleanup)
Merging into:ccd4671556758a3ad5ce925a7688e8618e915248
  Merge pull request #630 from talsewell/compute-thmset [Apr 20 03:03:19]
HOL:d9d262ad8402d865a72735480268b9f2da63fcd9
  Change ThmSetData to store just theorem names in .dat files [Apr 21 04:26:27]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Apr 22 14:30:16 Claimed job
Apr 22 14:30:56 Building HOL
Apr 22 14:40:17 Starting developers
Apr 22 14:40:19 Finished developers                                               2s  22MB
Apr 22 14:40:19 Starting developers/bin
Apr 22 14:41:29 Finished developers/bin                                        1m09s 918MB
Apr 22 14:41:29 Starting semantics/ffi
Apr 22 14:42:07 Finished semantics/ffi                                           37s 509MB
Apr 22 14:42:07 Starting semantics
Apr 22 14:43:44 Finished semantics                                             1m36s 843MB
Apr 22 14:43:44 Starting semantics/proofs
Apr 22 14:46:43 Finished semantics/proofs                                      2m58s   1GB
Apr 22 14:46:43 Starting basis/pure
Apr 22 14:50:20 Finished basis/pure                                            3m36s 685MB
Apr 22 14:50:20 Starting translator
Apr 22 14:51:58 Finished translator                                            1m37s   1GB
Apr 22 14:51:58 Starting compiler/parsing
Apr 22 14:52:56 Finished compiler/parsing                                        57s   2GB
Apr 22 14:52:57 Starting characteristic
Apr 22 14:58:10 Finished characteristic                                        5m13s   1GB
Apr 22 14:58:10 Starting translator/monadic
Apr 22 14:59:37 Finished translator/monadic                                    1m26s   1GB
Apr 22 14:59:37 Starting basis
Apr 22 15:16:10 Finished basis                                                16m32s   2GB
Apr 22 15:16:10 Starting compiler/inference
Apr 22 15:17:59 Finished compiler/inference                                    1m49s   2GB
Apr 22 15:18:00 Starting compiler/backend/reg_alloc
Apr 22 15:18:59 Finished compiler/backend/reg_alloc                              59s   1GB
Apr 22 15:18:59 Starting compiler/backend/gc
Apr 22 15:28:04 Finished compiler/backend/gc                                   9m04s   1GB
Apr 22 15:28:04 Starting compiler/backend
Apr 22 15:28:07 Finished compiler/backend                                         2s  25MB
Apr 22 15:28:07 Starting compiler/encoders/asm
Apr 22 15:28:09 Finished compiler/encoders/asm                                    1s  12MB
Apr 22 15:28:09 Starting compiler/encoders/x64
Apr 22 15:29:10 Finished compiler/encoders/x64                                 1m00s 704MB
Apr 22 15:29:10 Starting compiler/encoders/arm6
Apr 22 15:30:50 Finished compiler/encoders/arm6                                1m39s   1GB
Apr 22 15:30:50 Starting compiler/encoders/arm8
Apr 22 15:31:23 Finished compiler/encoders/arm8                                  32s 557MB
Apr 22 15:31:23 Starting compiler/encoders/mips
Apr 22 15:32:31 Finished compiler/encoders/mips                                1m07s   1GB
Apr 22 15:32:31 Starting compiler/encoders/riscv
Apr 22 15:33:52 Finished compiler/encoders/riscv                               1m20s 749MB
Apr 22 15:33:52 Starting compiler/encoders/ag32
Apr 22 15:34:09 Finished compiler/encoders/ag32                                  16s 619MB
Apr 22 15:34:10 Starting compiler/backend/x64
Apr 22 15:34:28 Finished compiler/backend/x64                                    18s   1GB
Apr 22 15:34:29 Starting compiler/backend/arm6
Apr 22 15:34:49 Finished compiler/backend/arm6                                   19s   1GB
Apr 22 15:34:49 Starting compiler/backend/arm8
Apr 22 15:35:07 Finished compiler/backend/arm8                                   17s   1GB
Apr 22 15:35:07 Starting compiler/backend/mips
Apr 22 15:35:26 Finished compiler/backend/mips                                   18s   1GB
Apr 22 15:35:27 Starting compiler/backend/riscv
Apr 22 15:35:45 Finished compiler/backend/riscv                                  17s   1GB
Apr 22 15:35:45 Starting compiler/backend/ag32
Apr 22 15:36:54 Finished compiler/backend/ag32                                 1m08s   1GB
Apr 22 15:36:54 Starting compiler/parsing/proofs
Apr 22 15:42:25 Finished compiler/parsing/proofs                               5m31s   1GB
Apr 22 15:42:25 Starting compiler/inference/proofs
Apr 22 15:45:04 Finished compiler/inference/proofs                             2m38s   1GB
Apr 22 15:45:05 Starting compiler/backend/semantics
Apr 22 15:51:55 Finished compiler/backend/semantics                            6m50s   1GB
Apr 22 15:51:55 Starting compiler/backend/reg_alloc/proofs
Apr 22 15:55:10 Finished compiler/backend/reg_alloc/proofs                     3m14s 797MB
Apr 22 15:55:10 Starting compiler/backend/proofs
Apr 22 16:32:09 Finished compiler/backend/proofs                              36m58s   3GB
Apr 22 16:32:09 Starting compiler/encoders/x64/proofs
Apr 22 16:42:05 Finished compiler/encoders/x64/proofs                          9m54s   4GB
Apr 22 16:42:05 Starting compiler/encoders/arm6/proofs
Apr 22 16:55:11 Finished compiler/encoders/arm6/proofs                        13m05s   6GB
Apr 22 16:55:11 Starting compiler/encoders/arm8/proofs
Apr 22 17:00:51 Finished compiler/encoders/arm8/proofs                         5m39s   1GB
Apr 22 17:00:51 Starting compiler/encoders/mips/proofs
Apr 22 17:10:38 Finished compiler/encoders/mips/proofs                         9m47s   2GB
Apr 22 17:10:38 Starting compiler/encoders/riscv/proofs
Apr 22 17:18:54 Finished compiler/encoders/riscv/proofs                        8m15s   1GB
Apr 22 17:18:55 Starting compiler/encoders/ag32/proofs
Apr 22 17:21:22 Finished compiler/encoders/ag32/proofs                         2m27s 699MB
Apr 22 17:21:22 Starting compiler/backend/x64/proofs
Apr 22 17:21:42 Finished compiler/backend/x64/proofs                             19s   1GB
Apr 22 17:21:42 Starting compiler/backend/arm6/proofs
Apr 22 17:22:04 Finished compiler/backend/arm6/proofs                            21s   1GB
Apr 22 17:22:04 Starting compiler/backend/arm8/proofs
Apr 22 17:22:23 Finished compiler/backend/arm8/proofs                            18s 770MB
Apr 22 17:22:23 Starting compiler/backend/mips/proofs
Apr 22 17:22:43 Finished compiler/backend/mips/proofs                            20s   1GB
Apr 22 17:22:44 Starting compiler/backend/riscv/proofs
Apr 22 17:23:04 Finished compiler/backend/riscv/proofs                           20s   1GB
Apr 22 17:23:04 Starting compiler/backend/ag32/proofs
Apr 22 17:31:52 Finished compiler/backend/ag32/proofs                          8m48s   2GB
Apr 22 17:31:53 Starting compiler/proofs
Apr 22 17:33:26 Finished compiler/proofs                                       1m33s   3GB
Apr 22 17:33:27 Starting candle/set-theory
Apr 22 17:33:54 Finished candle/set-theory                                       26s 927MB
Apr 22 17:33:54 Starting candle/syntax-lib
Apr 22 17:34:05 Finished candle/syntax-lib                                       10s 631MB
Apr 22 17:34:05 Starting candle/standard/syntax
Apr 22 17:35:50 Finished candle/standard/syntax                                1m44s   1GB
Apr 22 17:35:50 Starting candle/standard/semantics
Apr 22 17:37:27 Finished candle/standard/semantics                             1m37s   1GB
Apr 22 17:37:28 Starting candle/standard/monadic
Apr 22 17:39:00 Finished candle/standard/monadic                               1m32s   1GB
Apr 22 17:39:00 Starting candle/standard/ml_kernel
Apr 22 17:42:46 Finished candle/standard/ml_kernel                             3m45s   2GB
Apr 22 17:42:47 Starting candle/standard/opentheory
Apr 22 17:51:04 Finished candle/standard/opentheory                            8m17s   4GB
Apr 22 17:51:04 Starting candle/standard/opentheory/compilation
Apr 22 18:20:04 Finished candle/standard/opentheory/compilation               28m59s  16GB
Apr 22 18:20:04 Starting candle/standard/opentheory/compilation/proofs
Apr 22 18:21:01 Finished candle/standard/opentheory/compilation/proofs           56s   2GB
Apr 22 18:21:01 Starting characteristic/examples
Apr 22 18:22:23 Finished characteristic/examples                               1m22s   2GB
Apr 22 18:22:23 Starting tutorial/solutions
Apr 22 18:35:32 Finished tutorial/solutions                                   13m08s   6GB
Apr 22 18:35:33 Starting translator/monadic/examples
Apr 22 18:38:23 Finished translator/monadic/examples                           2m50s   2GB
Apr 22 18:38:23 Starting examples
Apr 22 18:46:40 Finished examples                                              8m16s   4GB
Apr 22 18:46:40 Starting examples/compilation/x64
Apr 22 20:39:24 Finished examples/compilation/x64                           1h52m43s  13GB
Apr 22 20:39:24 Starting examples/compilation/x64/proofs
Apr 22 20:40:51 Finished examples/compilation/x64/proofs                       1m25s   2GB
Apr 22 20:40:51 Starting examples/compilation/ag32
Apr 22 21:09:18 Finished examples/compilation/ag32                            28m27s   6GB
Apr 22 21:09:18 Starting examples/compilation/ag32/proofs
Apr 22 21:10:22 Finished examples/compilation/ag32/proofs                      1m01s   3GB
Apr 22 21:10:22 Starting translator/okasaki-examples
Apr 22 21:14:22 Finished translator/okasaki-examples                           4m00s   1GB
Apr 22 21:14:22 Starting translator/other-examples
Apr 22 21:17:58 Finished translator/other-examples                             3m35s   1GB
Apr 22 21:17:58 Starting compiler/parsing/tests
Apr 22 21:18:24 Finished compiler/parsing/tests                                  25s 609MB
Apr 22 21:18:24 Starting compiler/inference/tests
Apr 22 21:22:26 Finished compiler/inference/tests                              4m00s   2GB
Apr 22 21:22:26 Starting compiler/bootstrap/translation
Apr 22 23:48:02 Finished compiler/bootstrap/translation                     2h25m35s  36GB
Apr 22 23:48:02 Starting unverified/sexpr-bootstrap/x64/64
Apr 22 23:55:36 Finished unverified/sexpr-bootstrap/x64/64                     7m33s   3GB
Apr 22 23:55:36 Starting unverified/sexpr-bootstrap/x64/32
Apr 23 00:00:04 Finished unverified/sexpr-bootstrap/x64/32                     4m27s   4GB
Apr 23 00:00:04 Starting compiler/benchmarks
Apr 23 00:00:11 Finished compiler/benchmarks                                      6s  23MB
Apr 23 00:00:12 Starting compiler/bootstrap/compilation/x64/64
Apr 23 10:12:51 Finished compiler/bootstrap/compilation/x64/64             10h12m39s  64GB
Apr 23 10:12:51 Starting compiler/bootstrap/compilation/x64/64/proofs
Apr 23 10:17:12 Finished compiler/bootstrap/compilation/x64/64/proofs          4m20s   6GB
Apr 23 10:17:12 Starting compiler/bootstrap/compilation/x64/32
Apr 23 19:23:33 Finished compiler/bootstrap/compilation/x64/32              9h06m20s  64GB
Apr 23 19:23:33 Starting compiler/bootstrap/compilation/x64/32/proofs
Apr 23 19:26:41 Finished compiler/bootstrap/compilation/x64/32/proofs          3m08s   5GB
Apr 23 19:26:41 Starting compiler/bootstrap/compilation/ag32/32
Apr 24 04:56:00 Finished compiler/bootstrap/compilation/ag32/32             9h29m18s  64GB
Apr 24 04:56:00 Starting compiler/bootstrap/compilation/ag32/32/proofs
Apr 24 05:20:19 Finished compiler/bootstrap/compilation/ag32/32/proofs        24m18s  14GB
Apr 24 05:20:19 SUCCESS