Job 1582

CakeML:02b7596a1e78ffe81747453856daa593313bbc8b
  Prove equivalence of big-/small-step semantics for declarations [Sep 16 19:32:11]
#834 (master)
Merging into:1cfcd59d4f8168f639ea94c4020ba0249898078a
  Merge pull request #833 from CakeML/parse-err [Sep 14 09:26:31]
HOL:9b9646dfe8c21bf1f359f11f3eedf37c281ac01b
  Holmake: "link-to-sigobj" now can/should be done in Holmakefiles [Sep 16 07:28:06]
Machine:oven3 4.19.67.1.amd64-smp

Sep 17 08:11:58 Claimed job
Sep 17 08:12:09 Building HOL
Sep 17 08:37:19 Starting developers
Sep 17 08:37:27 Finished developers                                               8s 104MB
Sep 17 08:37:27 Starting developers/bin
Sep 17 08:37:40 Finished developers/bin                                          12s   1GB
Sep 17 08:37:40 Starting semantics/ffi
Sep 17 08:38:06 Finished semantics/ffi                                           25s 280MB
Sep 17 08:38:06 Starting semantics
Sep 17 08:41:17 Finished semantics                                             3m10s   1GB
Sep 17 08:41:17 Starting semantics/proofs
Sep 17 08:49:33 Finished semantics/proofs                                      8m16s   1GB
Sep 17 08:49:34 Starting semantics/alt_semantics
Sep 17 08:49:57 Finished semantics/alt_semantics                                 23s 398MB
Sep 17 08:49:58 Starting semantics/alt_semantics/proofs
Sep 17 08:55:21 Finished semantics/alt_semantics/proofs                        5m23s   1GB
Sep 17 08:55:21 Starting basis/pure
Sep 17 09:01:27 Finished basis/pure                                            6m05s 887MB
Sep 17 09:01:27 Starting translator
Sep 17 09:08:16 Finished translator                                            6m48s   1GB
Sep 17 09:08:16 Starting compiler/parsing
Sep 17 09:10:59 Finished compiler/parsing                                      2m42s   2GB
Sep 17 09:10:59 Starting characteristic
Sep 17 09:23:07 Finished characteristic                                       12m07s   2GB
Sep 17 09:23:08 Starting translator/monadic
Sep 17 09:26:39 Finished translator/monadic                                    3m31s   1GB
Sep 17 09:26:40 Starting basis
Sep 17 11:02:54 Finished basis                                              1h36m14s   9GB
Sep 17 11:02:55 Starting compiler/inference
Sep 17 11:05:41 Finished compiler/inference                                    2m45s   1GB
Sep 17 11:05:41 Starting compiler/backend/reg_alloc
Sep 17 11:07:45 Finished compiler/backend/reg_alloc                            2m04s   1GB
Sep 17 11:07:46 Starting compiler/backend/gc
Sep 17 11:14:54 Finished compiler/backend/gc                                   7m07s   2GB
Sep 17 11:14:54 Starting compiler/backend
Sep 17 11:24:17 Finished compiler/backend                                      9m23s   4GB
Sep 17 11:24:18 Starting compiler/encoders/asm
Sep 17 11:25:09 Finished compiler/encoders/asm                                   51s 721MB
Sep 17 11:25:10 Starting compiler/encoders/x64
Sep 17 11:27:29 Finished compiler/encoders/x64                                 2m18s 804MB
Sep 17 11:27:29 Starting compiler/encoders/arm7
Sep 17 11:32:03 Finished compiler/encoders/arm7                                4m34s   1GB
Sep 17 11:32:04 Starting compiler/encoders/arm8
Sep 17 11:33:27 Finished compiler/encoders/arm8                                1m23s 740MB
Sep 17 11:33:28 Starting compiler/encoders/mips
Sep 17 11:36:42 Finished compiler/encoders/mips                                3m13s 868MB
Sep 17 11:36:42 Starting compiler/encoders/riscv
Sep 17 11:40:33 Finished compiler/encoders/riscv                               3m51s 794MB
Sep 17 11:40:34 Starting compiler/encoders/ag32
Sep 17 11:41:16 Finished compiler/encoders/ag32                                  42s 932MB
Sep 17 11:41:17 Starting compiler/backend/x64
Sep 17 11:42:01 Finished compiler/backend/x64                                    44s   1GB
Sep 17 11:42:01 Starting compiler/backend/arm7
Sep 17 11:42:51 Finished compiler/backend/arm7                                   49s   1GB
Sep 17 11:42:51 Starting compiler/backend/arm8
Sep 17 11:43:35 Finished compiler/backend/arm8                                   43s   1GB
Sep 17 11:43:35 Starting compiler/backend/mips
Sep 17 11:44:19 Finished compiler/backend/mips                                   42s   1GB
Sep 17 11:44:19 Starting compiler/backend/riscv
Sep 17 11:45:02 Finished compiler/backend/riscv                                  42s   1GB
Sep 17 11:45:02 Starting compiler/backend/ag32
Sep 17 11:47:34 Finished compiler/backend/ag32                                 2m31s   1GB
Sep 17 11:47:34 Starting compiler/parsing/proofs
Sep 17 12:01:56 Finished compiler/parsing/proofs                              14m22s   1GB
Sep 17 12:01:57 Starting compiler/inference/proofs
Sep 17 12:07:20 Finished compiler/inference/proofs                             5m22s   1GB
Sep 17 12:07:20 Starting compiler/backend/semantics
Sep 17 13:08:47 Finished compiler/backend/semantics                         1h01m26s   2GB
Sep 17 13:08:48 Starting compiler/backend/reg_alloc/proofs
Sep 17 13:16:29 Finished compiler/backend/reg_alloc/proofs                     7m40s   1GB
Sep 17 13:16:29 Starting compiler/backend/proofs
Sep 17 14:58:32 Finished compiler/backend/proofs                            1h42m02s  16GB
Sep 17 14:58:32 Starting compiler/encoders/x64/proofs
Sep 17 15:20:13 Finished compiler/encoders/x64/proofs                         21m40s   4GB
Sep 17 15:20:13 Starting compiler/encoders/arm7/proofs
Sep 17 15:49:35 Finished compiler/encoders/arm7/proofs                        29m22s   4GB
Sep 17 15:49:36 Starting compiler/encoders/arm8/proofs
Sep 17 16:05:26 Finished compiler/encoders/arm8/proofs                        15m49s   1GB
Sep 17 16:05:26 Starting compiler/encoders/mips/proofs
Sep 17 16:27:59 Finished compiler/encoders/mips/proofs                        22m32s   2GB
Sep 17 16:27:59 Starting compiler/encoders/riscv/proofs
Sep 17 16:48:22 Finished compiler/encoders/riscv/proofs                       20m22s   1GB
Sep 17 16:48:23 Starting compiler/encoders/ag32/proofs
Sep 17 16:54:09 Finished compiler/encoders/ag32/proofs                         5m45s 831MB
Sep 17 16:54:09 Starting compiler/backend/x64/proofs
Sep 17 16:54:58 Finished compiler/backend/x64/proofs                             49s   1GB
Sep 17 16:54:58 Starting compiler/backend/arm7/proofs
Sep 17 16:55:51 Finished compiler/backend/arm7/proofs                            52s   1GB
Sep 17 16:55:52 Starting compiler/backend/arm8/proofs
Sep 17 16:56:40 Finished compiler/backend/arm8/proofs                            48s   1GB
Sep 17 16:56:40 Starting compiler/backend/mips/proofs
Sep 17 16:57:30 Finished compiler/backend/mips/proofs                            49s   1GB
Sep 17 16:57:31 Starting compiler/backend/riscv/proofs
Sep 17 16:58:20 Finished compiler/backend/riscv/proofs                           48s   1GB
Sep 17 16:58:20 Starting compiler/backend/ag32/proofs
Sep 17 17:25:47 Finished compiler/backend/ag32/proofs                         27m27s   3GB
Sep 17 17:25:48 Starting compiler/proofs
Sep 17 17:30:12 Finished compiler/proofs                                       4m23s   3GB
Sep 17 17:30:12 Starting candle/set-theory
Sep 17 17:31:12 Finished candle/set-theory                                       59s 801MB
Sep 17 17:31:12 Starting candle/syntax-lib
Sep 17 17:31:35 Finished candle/syntax-lib                                       22s 537MB
Sep 17 17:31:35 Starting candle/standard/syntax
Sep 17 17:35:32 Finished candle/standard/syntax                                3m56s 913MB
Sep 17 17:35:32 Starting candle/standard/semantics
Sep 17 17:39:22 Finished candle/standard/semantics                             3m50s   1GB
Sep 17 17:39:23 Starting candle/standard/monadic
Sep 17 17:43:08 Finished candle/standard/monadic                               3m44s   1GB
Sep 17 17:43:08 Starting candle/standard/ml_kernel
Sep 17 17:55:00 Finished candle/standard/ml_kernel                            11m51s   5GB
Sep 17 17:55:00 Starting candle/overloading/syntax
Sep 17 18:01:46 Finished candle/overloading/syntax                             6m45s   1GB
Sep 17 18:01:46 Starting candle/overloading/semantics
Sep 17 18:28:23 Finished candle/overloading/semantics                         26m34s   3GB
Sep 17 18:28:23 Starting pancake
Sep 17 18:30:04 Finished pancake                                               1m41s 816MB
Sep 17 18:30:05 Starting pancake/ffi
Sep 17 18:30:05 Finished pancake/ffi                                              0s   9MB
Sep 17 18:30:06 Starting pancake/semantics
Sep 17 18:34:54 Finished pancake/semantics                                     4m48s   1GB
Sep 17 18:34:55 Starting pancake/proofs
Sep 17 19:01:14 Finished pancake/proofs                                       26m19s   6GB
Sep 17 19:01:15 Starting characteristic/examples
Sep 17 19:04:05 Finished characteristic/examples                               2m49s   2GB
Sep 17 19:04:05 Starting tutorial/solutions
Sep 17 19:37:42 Finished tutorial/solutions                                   33m36s   8GB
Sep 17 19:37:42 Starting translator/monadic/examples
Sep 17 19:43:41 Finished translator/monadic/examples                           5m58s   3GB
Sep 17 19:43:41 Starting examples
Sep 17 20:00:34 Finished examples                                             16m51s   3GB
Sep 17 20:00:34 Starting examples/compilation/x64
Sep 18 01:22:02 Finished examples/compilation/x64                           5h21m27s  14GB
Sep 18 01:22:02 Starting examples/compilation/x64/proofs
Sep 18 01:25:54 Finished examples/compilation/x64/proofs                       3m51s   3GB
Sep 18 01:25:54 Starting examples/compilation/ag32
Sep 18 02:41:19 Finished examples/compilation/ag32                          1h15m22s   8GB
Sep 18 02:41:19 Starting examples/compilation/ag32/proofs
Sep 18 02:43:11 Finished examples/compilation/ag32/proofs                      1m52s   3GB
Sep 18 02:43:12 Starting examples/cost
Sep 18 04:40:54 Finished examples/cost                                      1h57m41s   8GB
Sep 18 04:40:54 Starting examples/lpr_checker
Sep 18 04:49:10 Finished examples/lpr_checker                                  8m15s   2GB
Sep 18 04:49:11 Starting examples/lpr_checker/compilation
Sep 18 05:25:34 Finished examples/lpr_checker/compilation                     36m23s  10GB
Sep 18 05:25:35 Starting examples/lpr_checker/compilation/proofs
Sep 18 05:27:00 Finished examples/lpr_checker/compilation/proofs               1m25s   3GB
Sep 18 05:27:01 Starting examples/lpr_checker/array
Sep 18 05:59:15 Finished examples/lpr_checker/array                           32m13s   4GB
Sep 18 05:59:15 Starting examples/lpr_checker/array/compilation
Sep 18 06:43:04 Finished examples/lpr_checker/array/compilation               43m48s  12GB
Sep 18 06:43:04 Starting examples/lpr_checker/array/compilation/proofs
Sep 18 06:44:52 Finished examples/lpr_checker/array/compilation/proofs         1m48s   4GB
Sep 18 06:44:53 Starting examples/opentheory
Sep 18 07:06:21 Finished examples/opentheory                                  21m27s   4GB
Sep 18 07:06:21 Starting examples/opentheory
Sep 18 07:06:24 Finished examples/opentheory                                      2s  33MB
Sep 18 07:06:24 Starting examples/opentheory/compilation
Sep 18 08:13:57 Finished examples/opentheory/compilation                    1h07m32s  17GB
Sep 18 08:13:57 Starting examples/opentheory/compilation/proofs
Sep 18 08:15:29 Finished examples/opentheory/compilation/proofs                1m31s   3GB
Sep 18 08:15:29 Starting examples/opentheory/compilation/ag32
Sep 18 09:28:25 Finished examples/opentheory/compilation/ag32               1h12m55s  18GB
Sep 18 09:28:26 Starting examples/opentheory/compilation/ag32/proofs
Sep 18 09:31:55 Finished examples/opentheory/compilation/ag32/proofs           3m28s   6GB
Sep 18 09:31:55 Starting examples/sat_encodings
Sep 18 09:35:50 Finished examples/sat_encodings                                3m54s 917MB
Sep 18 09:35:50 Starting examples/sat_encodings/case_studies
Sep 18 09:39:09 Finished examples/sat_encodings/case_studies                   3m18s 799MB
Sep 18 09:39:09 Starting examples/sat_encodings/translation
Sep 18 09:51:11 Finished examples/sat_encodings/translation                   12m02s   3GB
Sep 18 09:51:12 Starting examples/sat_encodings/translation/compilation
Sep 18 11:09:27 Finished examples/sat_encodings/translation/compilation     1h18m15s  11GB
Sep 18 11:09:28 Starting translator/okasaki-examples
Sep 18 11:18:35 Finished translator/okasaki-examples                           9m07s   1GB
Sep 18 11:18:36 Starting translator/other-examples
Sep 18 11:22:33 Finished translator/other-examples                             3m57s   1GB
Sep 18 11:22:34 Starting compiler/parsing/tests
Sep 18 11:23:40 Finished compiler/parsing/tests                                1m06s 586MB
Sep 18 11:23:40 Starting compiler/inference/tests
Sep 18 11:39:23 Finished compiler/inference/tests                             15m42s   3GB
Sep 18 11:39:23 Starting compiler/bootstrap/translation
Sep 18 17:02:46 Finished compiler/bootstrap/translation                     5h23m23s  23GB
Sep 18 17:02:47 Starting unverified/sexpr-bootstrap/x64/64
Sep 18 17:26:47 Finished unverified/sexpr-bootstrap/x64/64                    23m59s   8GB
Sep 18 17:26:47 Starting unverified/sexpr-bootstrap/x64/32
Sep 18 17:47:26 Finished unverified/sexpr-bootstrap/x64/32                    20m38s   8GB
Sep 18 17:47:26 Starting compiler/benchmarks
Sep 18 17:47:31 Finished compiler/benchmarks                                      4s  33MB
Sep 18 17:47:31 Starting compiler/bootstrap/compilation/x64/64
Sep 19 23:44:00 Finished compiler/bootstrap/compilation/x64/64             29h56m27s 109GB
Sep 19 23:44:00 Starting compiler/bootstrap/compilation/x64/64/proofs
Sep 19 23:48:47 Finished compiler/bootstrap/compilation/x64/64/proofs          4m46s  16GB
Sep 19 23:48:47 Starting compiler/bootstrap/compilation/x64/32
Sep 21 00:16:22 Finished compiler/bootstrap/compilation/x64/32             24h27m33s 112GB
Sep 21 00:16:22 Starting compiler/bootstrap/compilation/x64/32/proofs
Sep 21 00:20:43 Finished compiler/bootstrap/compilation/x64/32/proofs          4m20s  14GB
Sep 21 00:20:43 Starting compiler/bootstrap/compilation/ag32/32
Sep 22 00:49:38 Finished compiler/bootstrap/compilation/ag32/32            24h28m53s 102GB
Sep 22 00:49:38 Starting compiler/bootstrap/compilation/ag32/32/proofs
Sep 22 01:09:34 Finished compiler/bootstrap/compilation/ag32/32/proofs        19m55s  38GB
Sep 22 01:09:35 SUCCESS