Job 984

CakeML:980410c6c89921c2e8950a5127bd9f32791f50bf
  Fix more def_compte issues [Aug 05 04:31:17]
HOL:469c71a6019be577cd36d669ee28493a9905026f
  Port HOL Light proof of compactness for prop. logic [Aug 05 04:18:13]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Aug 08 07:13:58 Claimed job
Aug 08 07:14:06 Building HOL
Aug 08 07:23:32 Starting developers
Aug 08 07:23:34 Finished developers                                               2s  20MB
Aug 08 07:23:35 Starting developers/bin
Aug 08 07:23:41 Finished developers/bin                                           6s 960MB
Aug 08 07:23:42 Starting semantics/ffi
Aug 08 07:24:20 Finished semantics/ffi                                           38s 506MB
Aug 08 07:24:20 Starting semantics
Aug 08 07:25:55 Finished semantics                                             1m34s   1GB
Aug 08 07:25:55 Starting semantics/proofs
Aug 08 07:28:52 Finished semantics/proofs                                      2m57s   1GB
Aug 08 07:28:53 Starting semantics/alt_semantics
Aug 08 07:29:01 Finished semantics/alt_semantics                                  8s 258MB
Aug 08 07:29:01 Starting semantics/alt_semantics/proofs
Aug 08 07:30:51 Finished semantics/alt_semantics/proofs                        1m49s 750MB
Aug 08 07:30:51 Starting basis/pure
Aug 08 07:34:29 Finished basis/pure                                            3m37s 633MB
Aug 08 07:34:29 Starting translator
Aug 08 07:36:15 Finished translator                                            1m46s   1GB
Aug 08 07:36:16 Starting compiler/parsing
Aug 08 07:37:14 Finished compiler/parsing                                        57s   2GB
Aug 08 07:37:14 Starting characteristic
Aug 08 07:42:34 Finished characteristic                                        5m19s   1GB
Aug 08 07:42:34 Starting translator/monadic
Aug 08 07:44:04 Finished translator/monadic                                    1m29s   1GB
Aug 08 07:44:04 Starting basis
Aug 08 08:02:16 Finished basis                                                18m11s   2GB
Aug 08 08:02:16 Starting compiler/inference
Aug 08 08:04:14 Finished compiler/inference                                    1m58s   1GB
Aug 08 08:04:14 Starting compiler/backend/reg_alloc
Aug 08 08:05:14 Finished compiler/backend/reg_alloc                              59s   1GB
Aug 08 08:05:14 Starting compiler/backend/gc
Aug 08 08:14:32 Finished compiler/backend/gc                                   9m17s   2GB
Aug 08 08:14:32 Starting compiler/backend
Aug 08 08:14:35 Finished compiler/backend                                         2s  24MB
Aug 08 08:14:35 Starting compiler/encoders/asm
Aug 08 08:14:36 Finished compiler/encoders/asm                                    1s  15MB
Aug 08 08:14:36 Starting compiler/encoders/x64
Aug 08 08:15:37 Finished compiler/encoders/x64                                 1m00s 595MB
Aug 08 08:15:37 Starting compiler/encoders/arm7
Aug 08 08:17:18 Finished compiler/encoders/arm7                                1m41s   1GB
Aug 08 08:17:19 Starting compiler/encoders/arm8
Aug 08 08:17:51 Finished compiler/encoders/arm8                                  32s 572MB
Aug 08 08:17:52 Starting compiler/encoders/mips
Aug 08 08:18:59 Finished compiler/encoders/mips                                1m07s   1GB
Aug 08 08:18:59 Starting compiler/encoders/riscv
Aug 08 08:20:19 Finished compiler/encoders/riscv                               1m19s 770MB
Aug 08 08:20:19 Starting compiler/encoders/ag32
Aug 08 08:20:36 Finished compiler/encoders/ag32                                  16s 622MB
Aug 08 08:20:36 Starting compiler/backend/x64
Aug 08 08:20:55 Finished compiler/backend/x64                                    18s   1GB
Aug 08 08:20:56 Starting compiler/backend/arm7
Aug 08 08:21:15 Finished compiler/backend/arm7                                   18s   1GB
Aug 08 08:21:15 Starting compiler/backend/arm8
Aug 08 08:21:34 Finished compiler/backend/arm8                                   18s   1GB
Aug 08 08:21:34 Starting compiler/backend/mips
Aug 08 08:21:54 Finished compiler/backend/mips                                   19s   1GB
Aug 08 08:21:54 Starting compiler/backend/riscv
Aug 08 08:22:13 Finished compiler/backend/riscv                                  19s   1GB
Aug 08 08:22:13 Starting compiler/backend/ag32
Aug 08 08:23:23 Finished compiler/backend/ag32                                 1m09s 926MB
Aug 08 08:23:23 Starting compiler/parsing/proofs
Aug 08 08:28:55 Finished compiler/parsing/proofs                               5m31s 936MB
Aug 08 08:28:55 Starting compiler/inference/proofs
Aug 08 08:31:40 Finished compiler/inference/proofs                             2m45s   1GB
Aug 08 08:31:40 Starting compiler/backend/semantics
Aug 08 08:38:51 Finished compiler/backend/semantics                            7m09s   2GB
Aug 08 08:38:51 Starting compiler/backend/reg_alloc/proofs
Aug 08 08:42:09 Finished compiler/backend/reg_alloc/proofs                     3m18s 663MB
Aug 08 08:42:09 Starting compiler/backend/proofs
Aug 08 09:20:47 Finished compiler/backend/proofs                              38m37s   5GB
Aug 08 09:20:47 Starting compiler/encoders/x64/proofs
Aug 08 09:30:53 Finished compiler/encoders/x64/proofs                         10m05s   5GB
Aug 08 09:30:53 Starting compiler/encoders/arm7/proofs
Aug 08 09:44:12 Finished compiler/encoders/arm7/proofs                        13m19s   3GB
Aug 08 09:44:12 Starting compiler/encoders/arm8/proofs
Aug 08 09:50:51 Finished compiler/encoders/arm8/proofs                         6m38s   1GB
Aug 08 09:50:52 Starting compiler/encoders/mips/proofs
Aug 08 10:00:45 Finished compiler/encoders/mips/proofs                         9m53s   2GB
Aug 08 10:00:45 Starting compiler/encoders/riscv/proofs
Aug 08 10:08:56 Finished compiler/encoders/riscv/proofs                        8m10s   1GB
Aug 08 10:08:56 Starting compiler/encoders/ag32/proofs
Aug 08 10:11:25 Finished compiler/encoders/ag32/proofs                         2m28s 630MB
Aug 08 10:11:25 Starting compiler/backend/x64/proofs
Aug 08 10:11:45 Finished compiler/backend/x64/proofs                             19s   1GB
Aug 08 10:11:45 Starting compiler/backend/arm7/proofs
Aug 08 10:12:05 Finished compiler/backend/arm7/proofs                            19s 864MB
Aug 08 10:12:05 Starting compiler/backend/arm8/proofs
Aug 08 10:12:25 Finished compiler/backend/arm8/proofs                            19s   1GB
Aug 08 10:12:25 Starting compiler/backend/mips/proofs
Aug 08 10:12:46 Finished compiler/backend/mips/proofs                            20s   1GB
Aug 08 10:12:46 Starting compiler/backend/riscv/proofs
Aug 08 10:13:06 Finished compiler/backend/riscv/proofs                           20s   1GB
Aug 08 10:13:06 Starting compiler/backend/ag32/proofs
Aug 08 10:21:49 Finished compiler/backend/ag32/proofs                          8m43s   2GB
Aug 08 10:21:50 Starting compiler/proofs
Aug 08 10:23:09 Finished compiler/proofs                                       1m19s   3GB
Aug 08 10:23:10 Starting candle/set-theory
Aug 08 10:23:36 Finished candle/set-theory                                       26s 668MB
Aug 08 10:23:36 Starting candle/syntax-lib
Aug 08 10:23:47 Finished candle/syntax-lib                                       10s 668MB
Aug 08 10:23:47 Starting candle/standard/syntax
Aug 08 10:25:31 Finished candle/standard/syntax                                1m43s   1GB
Aug 08 10:25:31 Starting candle/standard/semantics
Aug 08 10:27:09 Finished candle/standard/semantics                             1m37s   1GB
Aug 08 10:27:09 Starting candle/standard/monadic
Aug 08 10:28:44 Finished candle/standard/monadic                               1m34s   1GB
Aug 08 10:28:44 Starting candle/standard/ml_kernel
Aug 08 10:32:30 Finished candle/standard/ml_kernel                             3m46s   3GB
Aug 08 10:32:30 Starting candle/standard/opentheory
Aug 08 10:41:00 Finished candle/standard/opentheory                            8m29s   4GB
Aug 08 10:41:00 Starting candle/standard/opentheory/compilation
Aug 08 11:11:16 Finished candle/standard/opentheory/compilation               30m15s  12GB
Aug 08 11:11:16 Starting candle/standard/opentheory/compilation/proofs
Aug 08 11:12:03 Finished candle/standard/opentheory/compilation/proofs           46s   2GB
Aug 08 11:12:03 Starting characteristic/examples
Aug 08 11:13:28 Finished characteristic/examples                               1m24s   2GB
Aug 08 11:13:28 Starting tutorial/solutions
Aug 08 11:26:43 Finished tutorial/solutions                                   13m14s   6GB
Aug 08 11:26:43 Starting translator/monadic/examples
Aug 08 11:29:38 Finished translator/monadic/examples                           2m54s   1GB
Aug 08 11:29:38 Starting examples
Aug 08 11:38:25 Finished examples                                              8m46s   4GB
Aug 08 11:38:25 Starting examples/compilation/x64
Aug 08 13:42:06 Finished examples/compilation/x64                           2h03m41s  13GB
Aug 08 13:42:06 Starting examples/compilation/x64/proofs
Aug 08 13:43:37 Finished examples/compilation/x64/proofs                       1m30s   2GB
Aug 08 13:43:37 Starting examples/compilation/ag32
Aug 08 14:12:18 Finished examples/compilation/ag32                            28m39s   5GB
Aug 08 14:12:18 Starting examples/compilation/ag32/proofs
Aug 08 14:13:10 Finished examples/compilation/ag32/proofs                        51s   2GB
Aug 08 14:13:10 Starting translator/okasaki-examples
Aug 08 14:17:14 Finished translator/okasaki-examples                           4m03s   1GB
Aug 08 14:17:14 Starting translator/other-examples
Aug 08 14:20:49 Finished translator/other-examples                             3m34s   1GB
Aug 08 14:20:49 Starting compiler/parsing/tests
Aug 08 14:21:14 Finished compiler/parsing/tests                                  25s 590MB
Aug 08 14:21:15 Starting compiler/inference/tests
Aug 08 14:25:28 Finished compiler/inference/tests                              4m12s   4GB
Aug 08 14:25:28 Starting compiler/bootstrap/translation
Aug 08 16:52:47 Finished compiler/bootstrap/translation                     2h27m18s  40GB
Aug 08 16:52:47 Starting unverified/sexpr-bootstrap/x64/64
Aug 08 17:05:06 Finished unverified/sexpr-bootstrap/x64/64                    12m17s   3GB
Aug 08 17:05:06 Starting unverified/sexpr-bootstrap/x64/32
Aug 08 17:13:48 Finished unverified/sexpr-bootstrap/x64/32                     8m40s   5GB
Aug 08 17:13:48 Starting compiler/benchmarks
Aug 08 17:13:56 Finished compiler/benchmarks                                      7s  24MB
Aug 08 17:13:57 Starting compiler/bootstrap/compilation/x64/64
Aug 09 05:25:03 Finished compiler/bootstrap/compilation/x64/64             12h11m05s  64GB
Aug 09 05:25:03 Starting compiler/bootstrap/compilation/x64/64/proofs
Aug 09 05:29:18 Finished compiler/bootstrap/compilation/x64/64/proofs          4m14s   5GB
Aug 09 05:29:18 Starting compiler/bootstrap/compilation/x64/32
Aug 09 17:12:06 Finished compiler/bootstrap/compilation/x64/32             11h42m46s  64GB
Aug 09 17:12:06 Starting compiler/bootstrap/compilation/x64/32/proofs
Aug 09 17:14:40 Finished compiler/bootstrap/compilation/x64/32/proofs          2m34s  10GB
Aug 09 17:14:41 Starting compiler/bootstrap/compilation/ag32/32
Aug 10 05:38:31 Finished compiler/bootstrap/compilation/ag32/32            12h23m50s  64GB
Aug 10 05:38:31 Starting compiler/bootstrap/compilation/ag32/32/proofs
Aug 10 06:02:31 Finished compiler/bootstrap/compilation/ag32/32/proofs        23m59s  17GB
Aug 10 06:02:31 SUCCESS