Job 1638

CakeML:6b7cb175197ce7d47ce8a1110417b7371d41e8c9
  More general version of the previous [Nov 15 10:14:13]
#845 (eval-type-rep)
Merging into:6b1184f731754a44e6368258d6c1b1cc729aa0f5
  Merge pull request #843 from CakeML/newline-fix [Nov 13 19:24:32]
HOL:7e1cdab63fa78a67a3fabc28a9f2a909e65b6921
  Make RPROD (and PAIR_REL and ###) more polymorphic [Nov 12 10:36:34]
Machine:oven3 4.19.67.1.amd64-smp

Nov 15 15:51:20 Claimed job
Nov 15 15:51:33 Reusing HOL
Nov 15 15:52:24 Starting developers
Nov 15 15:52:32 Finished developers                                               8s 136MB
Nov 15 15:52:32 Starting developers/bin
Nov 15 15:52:45 Finished developers/bin                                          12s   1GB
Nov 15 15:52:45 Starting semantics/ffi
Nov 15 15:53:11 Finished semantics/ffi                                           25s 270MB
Nov 15 15:53:11 Starting semantics
Nov 15 15:56:06 Finished semantics                                             2m54s   1GB
Nov 15 15:56:06 Starting semantics/proofs
Nov 15 16:04:43 Finished semantics/proofs                                      8m37s   1GB
Nov 15 16:04:44 Starting semantics/alt_semantics
Nov 15 16:05:11 Finished semantics/alt_semantics                                 26s 407MB
Nov 15 16:05:11 Starting semantics/alt_semantics/proofs
Nov 15 16:10:29 Finished semantics/alt_semantics/proofs                        5m17s   1GB
Nov 15 16:10:29 Starting basis/pure
Nov 15 16:12:16 Finished basis/pure                                            1m46s 634MB
Nov 15 16:12:16 Starting translator
Nov 15 16:18:16 Finished translator                                            5m59s   1GB
Nov 15 16:18:16 Starting compiler/parsing
Nov 15 16:20:55 Finished compiler/parsing                                      2m39s   3GB
Nov 15 16:20:56 Starting characteristic
Nov 15 16:33:13 Finished characteristic                                       12m16s   2GB
Nov 15 16:33:13 Starting translator/monadic
Nov 15 16:36:42 Finished translator/monadic                                    3m28s   1GB
Nov 15 16:36:42 Starting basis
Nov 15 18:16:27 Finished basis                                              1h39m45s  23GB
Nov 15 18:16:28 Starting compiler/inference
Nov 15 18:18:53 Finished compiler/inference                                    2m25s   1GB
Nov 15 18:18:54 Starting compiler/backend/reg_alloc
Nov 15 18:21:03 Finished compiler/backend/reg_alloc                            2m09s   1GB
Nov 15 18:21:04 Starting compiler/backend/gc
Nov 15 18:27:49 Finished compiler/backend/gc                                   6m45s   2GB
Nov 15 18:27:50 Starting compiler/backend
Nov 15 18:37:36 Finished compiler/backend                                      9m46s   3GB
Nov 15 18:37:36 Starting compiler/encoders/asm
Nov 15 18:38:26 Finished compiler/encoders/asm                                   49s 917MB
Nov 15 18:38:26 Starting compiler/encoders/x64
Nov 15 18:39:23 Finished compiler/encoders/x64                                   56s   1GB
Nov 15 18:39:23 Starting compiler/encoders/arm7
Nov 15 18:41:51 Finished compiler/encoders/arm7                                2m27s 937MB
Nov 15 18:41:51 Starting compiler/encoders/arm8
Nov 15 18:42:21 Finished compiler/encoders/arm8                                  29s 652MB
Nov 15 18:42:21 Starting compiler/encoders/mips
Nov 15 18:42:58 Finished compiler/encoders/mips                                  36s   1GB
Nov 15 18:42:58 Starting compiler/encoders/riscv
Nov 15 18:43:33 Finished compiler/encoders/riscv                                 34s   1GB
Nov 15 18:43:34 Starting compiler/encoders/ag32
Nov 15 18:44:14 Finished compiler/encoders/ag32                                  39s 624MB
Nov 15 18:44:14 Starting compiler/backend/x64
Nov 15 18:44:56 Finished compiler/backend/x64                                    41s   1GB
Nov 15 18:44:57 Starting compiler/backend/arm7
Nov 15 18:45:43 Finished compiler/backend/arm7                                   46s   1GB
Nov 15 18:45:44 Starting compiler/backend/arm8
Nov 15 18:46:25 Finished compiler/backend/arm8                                   41s   1GB
Nov 15 18:46:25 Starting compiler/backend/mips
Nov 15 18:47:10 Finished compiler/backend/mips                                   44s   1GB
Nov 15 18:47:10 Starting compiler/backend/riscv
Nov 15 18:47:52 Finished compiler/backend/riscv                                  41s   1GB
Nov 15 18:47:53 Starting compiler/backend/ag32
Nov 15 18:50:21 Finished compiler/backend/ag32                                 2m28s   1GB
Nov 15 18:50:22 Starting compiler/parsing/proofs
Nov 15 19:04:53 Finished compiler/parsing/proofs                              14m31s 926MB
Nov 15 19:04:54 Starting compiler/inference/proofs
Nov 15 19:10:27 Finished compiler/inference/proofs                             5m33s   1GB
Nov 15 19:10:28 Starting compiler/backend/semantics
Nov 15 20:12:58 Finished compiler/backend/semantics                         1h02m29s   3GB
Nov 15 20:12:58 Starting compiler/backend/reg_alloc/proofs
Nov 15 20:20:50 Finished compiler/backend/reg_alloc/proofs                     7m51s 885MB
Nov 15 20:20:50 Starting compiler/backend/proofs
Nov 15 22:02:17 Finished compiler/backend/proofs                            1h41m25s  16GB
Nov 15 22:02:17 Starting compiler/backend/serialiser
Nov 15 22:04:40 Finished compiler/backend/serialiser                           2m22s   1GB
Nov 15 22:04:40 Starting compiler/encoders/x64/proofs
Nov 15 22:26:20 Finished compiler/encoders/x64/proofs                         21m39s   4GB
Nov 15 22:26:20 Starting compiler/encoders/arm7/proofs
Nov 15 22:56:14 Finished compiler/encoders/arm7/proofs                        29m53s   2GB
Nov 15 22:56:14 Starting compiler/encoders/arm8/proofs
Nov 15 23:11:37 Finished compiler/encoders/arm8/proofs                        15m22s   1GB
Nov 15 23:11:38 Starting compiler/encoders/mips/proofs
Nov 15 23:34:10 Finished compiler/encoders/mips/proofs                        22m31s   3GB
Nov 15 23:34:10 Starting compiler/encoders/riscv/proofs
Nov 15 23:54:30 Finished compiler/encoders/riscv/proofs                       20m19s   1GB
Nov 15 23:54:30 Starting compiler/encoders/ag32/proofs
Nov 16 00:00:19 Finished compiler/encoders/ag32/proofs                         5m48s 836MB
Nov 16 00:00:19 Starting compiler/backend/x64/proofs
Nov 16 00:01:09 Finished compiler/backend/x64/proofs                             50s   1GB
Nov 16 00:01:10 Starting compiler/backend/arm7/proofs
Nov 16 00:01:58 Finished compiler/backend/arm7/proofs                            48s   1GB
Nov 16 00:01:59 Starting compiler/backend/arm8/proofs
Nov 16 00:02:49 Finished compiler/backend/arm8/proofs                            49s   1GB
Nov 16 00:02:49 Starting compiler/backend/mips/proofs
Nov 16 00:03:40 Finished compiler/backend/mips/proofs                            51s   1GB
Nov 16 00:03:40 Starting compiler/backend/riscv/proofs
Nov 16 00:04:31 Finished compiler/backend/riscv/proofs                           50s   1GB
Nov 16 00:04:31 Starting compiler/backend/ag32/proofs
Nov 16 00:32:07 Finished compiler/backend/ag32/proofs                         27m34s   3GB
Nov 16 00:32:07 Starting compiler/proofs
Nov 16 00:35:53 Finished compiler/proofs                                       3m45s   3GB
Nov 16 00:35:53 Starting candle/set-theory
Nov 16 00:36:53 Finished candle/set-theory                                     1m00s 732MB
Nov 16 00:36:54 Starting candle/syntax-lib
Nov 16 00:37:17 Finished candle/syntax-lib                                       23s 613MB
Nov 16 00:37:17 Starting candle/standard/syntax
Nov 16 00:41:15 Finished candle/standard/syntax                                3m56s   1GB
Nov 16 00:41:15 Starting candle/standard/semantics
Nov 16 00:45:07 Finished candle/standard/semantics                             3m51s   1GB
Nov 16 00:45:07 Starting candle/standard/monadic
Nov 16 00:48:54 Finished candle/standard/monadic                               3m45s   1GB
Nov 16 00:48:54 Starting candle/standard/ml_kernel
Nov 16 01:01:19 Finished candle/standard/ml_kernel                            12m24s   4GB
Nov 16 01:01:19 Starting candle/overloading/syntax
Nov 16 01:08:12 Finished candle/overloading/syntax                             6m52s   1GB
Nov 16 01:08:12 Starting candle/overloading/semantics
Nov 16 01:34:40 Finished candle/overloading/semantics                         26m27s   3GB
Nov 16 01:34:40 Starting pancake
Nov 16 01:38:26 Finished pancake                                               3m45s   2GB
Nov 16 01:38:26 Starting pancake/ffi
Nov 16 01:38:27 Finished pancake/ffi                                              0s   7MB
Nov 16 01:38:27 Starting pancake/semantics
Nov 16 01:43:19 Finished pancake/semantics                                     4m51s   1GB
Nov 16 01:43:19 Starting pancake/proofs
Nov 16 02:10:35 Finished pancake/proofs                                       27m15s   6GB
Nov 16 02:10:35 Starting characteristic/examples
Nov 16 02:14:04 Finished characteristic/examples                               3m29s   2GB
Nov 16 02:14:05 Starting tutorial/solutions
Nov 16 02:48:52 Finished tutorial/solutions                                   34m45s  10GB
Nov 16 02:48:52 Starting translator/monadic/examples
Nov 16 02:54:46 Finished translator/monadic/examples                           5m53s   2GB
Nov 16 02:54:46 Starting examples
Nov 16 03:11:55 Finished examples                                             17m08s   3GB
Nov 16 03:11:55 Starting examples/compilation/x64
Nov 16 08:38:19 Finished examples/compilation/x64                           5h26m22s  20GB
Nov 16 08:38:19 Starting examples/compilation/x64/proofs
Nov 16 08:41:54 Finished examples/compilation/x64/proofs                       3m34s   3GB
Nov 16 08:41:54 Starting examples/compilation/ag32
Nov 16 09:58:37 Finished examples/compilation/ag32                          1h16m42s   8GB
Nov 16 09:58:37 Starting examples/compilation/ag32/proofs
Nov 16 10:00:15 Finished examples/compilation/ag32/proofs                      1m37s   4GB
Nov 16 10:00:15 Starting examples/cost
Nov 16 11:54:19 Finished examples/cost                                      1h54m03s   8GB
Nov 16 11:54:20 Starting examples/lpr_checker
Nov 16 11:56:03 Finished examples/lpr_checker                                  1m42s   1GB
Nov 16 11:56:03 Starting examples/lpr_checker/array
Nov 16 12:58:53 Finished examples/lpr_checker/array                         1h02m49s   5GB
Nov 16 12:58:53 Starting examples/lpr_checker/array/compilation
Nov 16 16:08:45 Finished examples/lpr_checker/array/compilation             3h09m51s  41GB
Nov 16 16:08:45 Starting examples/lpr_checker/array/compilation/proofs
Nov 16 16:11:19 Finished examples/lpr_checker/array/compilation/proofs         2m33s   6GB
Nov 16 16:11:19 Starting examples/opentheory
Nov 16 16:32:08 Finished examples/opentheory                                  20m48s   3GB
Nov 16 16:32:08 Starting examples/opentheory
Nov 16 16:32:11 Finished examples/opentheory                                      2s  33MB
Nov 16 16:32:11 Starting examples/opentheory/compilation
Nov 16 17:50:13 Finished examples/opentheory/compilation                    1h18m00s  30GB
Nov 16 17:50:13 Starting examples/opentheory/compilation/proofs
Nov 16 17:51:43 Finished examples/opentheory/compilation/proofs                1m29s   4GB
Nov 16 17:51:43 Starting examples/opentheory/compilation/ag32
Nov 16 19:20:35 Finished examples/opentheory/compilation/ag32               1h28m51s  40GB
Nov 16 19:20:35 Starting examples/opentheory/compilation/ag32/proofs
Nov 16 19:24:02 Finished examples/opentheory/compilation/ag32/proofs           3m27s   6GB
Nov 16 19:24:02 Starting examples/sat_encodings
Nov 16 19:27:58 Finished examples/sat_encodings                                3m55s 958MB
Nov 16 19:27:58 Starting examples/sat_encodings/case_studies
Nov 16 19:31:19 Finished examples/sat_encodings/case_studies                   3m20s 760MB
Nov 16 19:31:19 Starting examples/sat_encodings/translation
Nov 16 19:42:52 Finished examples/sat_encodings/translation                   11m32s   3GB
Nov 16 19:42:52 Starting examples/sat_encodings/translation/compilation
Nov 16 21:09:10 Finished examples/sat_encodings/translation/compilation     1h26m17s  25GB
Nov 16 21:09:10 Starting translator/okasaki-examples
Nov 16 21:18:25 Finished translator/okasaki-examples                           9m14s   1GB
Nov 16 21:18:26 Starting translator/other-examples
Nov 16 21:21:51 Finished translator/other-examples                             3m25s   1GB
Nov 16 21:21:51 Starting compiler/parsing/tests
Nov 16 21:22:56 Finished compiler/parsing/tests                                1m04s 586MB
Nov 16 21:22:57 Starting compiler/inference/tests
Nov 16 21:38:59 Finished compiler/inference/tests                             16m02s   3GB
Nov 16 21:38:59 Starting compiler/bootstrap/translation
Nov 17 03:11:50 Finished compiler/bootstrap/translation                     5h32m50s  30GB
Nov 17 03:11:50 Starting unverified/sexpr-bootstrap/x64/64
Nov 17 03:36:04 Finished unverified/sexpr-bootstrap/x64/64                    24m13s   9GB
Nov 17 03:36:04 Starting unverified/sexpr-bootstrap/x64/32
Nov 17 03:57:00 Finished unverified/sexpr-bootstrap/x64/32                    20m55s   8GB
Nov 17 03:57:00 Starting compiler/benchmarks
Nov 17 03:57:05 Finished compiler/benchmarks                                      4s  33MB
Nov 17 03:57:05 Starting compiler/bootstrap/compilation/x64/64
Nov 18 09:03:57 Finished compiler/bootstrap/compilation/x64/64             29h06m50s 110GB
Nov 18 09:03:57 Starting compiler/bootstrap/compilation/x64/64/proofs
Nov 18 09:08:34 Finished compiler/bootstrap/compilation/x64/64/proofs          4m36s  19GB
Nov 18 09:08:34 Starting compiler/bootstrap/compilation/x64/32
Nov 19 07:55:34 Finished compiler/bootstrap/compilation/x64/32             22h46m57s  79GB
Nov 19 07:55:34 Starting compiler/bootstrap/compilation/x64/32/proofs
Nov 19 07:59:50 Finished compiler/bootstrap/compilation/x64/32/proofs          4m15s  18GB
Nov 19 07:59:51 Starting compiler/bootstrap/compilation/ag32/32
Nov 20 09:49:23 Finished compiler/bootstrap/compilation/ag32/32            25h49m30s 111GB
Nov 20 09:49:24 Starting compiler/bootstrap/compilation/ag32/32/proofs
Nov 20 10:10:39 Finished compiler/bootstrap/compilation/ag32/32/proofs        21m14s  33GB
Nov 20 10:10:39 SUCCESS