Job 2269

CakeML:ac25fc69c400ec7b945ab386e058acaa81da1097
  Fix for ffiname [Jan 13 18:01:20]
#976 (ffiname)
Merging into:45534e558612704f938386fc12b79bc991c3afa3
  Update for new year [Jan 01 02:20:21]
HOL:fbdc8f631085370c871c50b58817d2e5b679eb88
  Reverted [REC]; re-worked REC_VAR_NO_TRANS (and I_NO_TRANS) by method [Jan 11 22:08:58]
Machine:stove 5.15.0-86-generic x86_64 GNU/Linux

Jan 13 20:49:18 Claimed job
Jan 13 20:49:26 Building HOL
Jan 13 21:03:10 Starting developers
Jan 13 21:03:16 Finished developers                                               5s 180MB
Jan 13 21:03:16 Starting developers/bin
Jan 13 21:03:22 Finished developers/bin                                           6s   1GB
Jan 13 21:03:22 Starting compiler/proofs
Jan 13 22:57:29 Finished compiler/proofs                                    1h54m06s  20GB
Jan 13 22:57:29 Starting compiler/bootstrap/translation
Jan 14 07:12:48 Finished compiler/bootstrap/translation                     8h15m18s  38GB
Jan 14 07:12:48 Starting semantics/ffi
Jan 14 07:12:54 Finished semantics/ffi                                            5s 212MB
Jan 14 07:12:54 Starting semantics
Jan 14 07:12:56 Finished semantics                                                1s  24MB
Jan 14 07:12:56 Starting semantics/proofs
Jan 14 07:13:27 Finished semantics/proofs                                        31s 769MB
Jan 14 07:13:28 Starting semantics/alt_semantics
Jan 14 07:13:59 Finished semantics/alt_semantics                                 31s 873MB
Jan 14 07:13:59 Starting semantics/alt_semantics/proofs
Jan 14 07:26:03 Finished semantics/alt_semantics/proofs                       12m03s   1GB
Jan 14 07:26:03 Starting basis/pure
Jan 14 07:26:04 Finished basis/pure                                               1s  17MB
Jan 14 07:26:04 Starting translator
Jan 14 07:27:54 Finished translator                                            1m49s   1GB
Jan 14 07:27:54 Starting compiler/parsing
Jan 14 07:27:55 Finished compiler/parsing                                         1s  22MB
Jan 14 07:27:55 Starting characteristic
Jan 14 07:27:57 Finished characteristic                                           1s  26MB
Jan 14 07:27:58 Starting translator/monadic
Jan 14 07:27:59 Finished translator/monadic                                       1s  25MB
Jan 14 07:28:00 Starting basis
Jan 14 07:31:45 Finished basis                                                 3m45s   3GB
Jan 14 07:31:45 Starting compiler/inference
Jan 14 07:31:47 Finished compiler/inference                                       1s  18MB
Jan 14 07:31:47 Starting compiler/backend/reg_alloc
Jan 14 07:31:49 Finished compiler/backend/reg_alloc                               1s  20MB
Jan 14 07:31:49 Starting compiler/backend/gc
Jan 14 07:31:51 Finished compiler/backend/gc                                      2s  26MB
Jan 14 07:31:51 Starting compiler/backend
Jan 14 07:32:04 Finished compiler/backend                                        12s 702MB
Jan 14 07:32:04 Starting compiler/encoders/asm
Jan 14 07:32:05 Finished compiler/encoders/asm                                    1s  18MB
Jan 14 07:32:05 Starting compiler/encoders/x64
Jan 14 07:32:07 Finished compiler/encoders/x64                                    1s  23MB
Jan 14 07:32:07 Starting compiler/encoders/arm7
Jan 14 07:32:09 Finished compiler/encoders/arm7                                   1s  23MB
Jan 14 07:32:09 Starting compiler/encoders/arm8
Jan 14 07:32:11 Finished compiler/encoders/arm8                                   1s  21MB
Jan 14 07:32:11 Starting compiler/encoders/arm8_asl
Jan 14 09:58:33 Finished compiler/encoders/arm8_asl                         2h26m21s  45GB
Jan 14 09:58:33 Starting compiler/encoders/mips
Jan 14 09:58:35 Finished compiler/encoders/mips                                   1s  22MB
Jan 14 09:58:35 Starting compiler/encoders/riscv
Jan 14 09:58:36 Finished compiler/encoders/riscv                                  1s  23MB
Jan 14 09:58:37 Starting compiler/encoders/ag32
Jan 14 09:58:38 Finished compiler/encoders/ag32                                   1s  21MB
Jan 14 09:58:38 Starting compiler/backend/x64
Jan 14 09:58:41 Finished compiler/backend/x64                                     2s  27MB
Jan 14 09:58:41 Starting compiler/backend/arm7
Jan 14 09:58:43 Finished compiler/backend/arm7                                    2s  24MB
Jan 14 09:58:43 Starting compiler/backend/arm8
Jan 14 09:58:45 Finished compiler/backend/arm8                                    2s  30MB
Jan 14 09:58:45 Starting compiler/backend/mips
Jan 14 09:58:48 Finished compiler/backend/mips                                    2s  23MB
Jan 14 09:58:48 Starting compiler/backend/riscv
Jan 14 09:58:50 Finished compiler/backend/riscv                                   2s  25MB
Jan 14 09:58:50 Starting compiler/backend/ag32
Jan 14 10:00:16 Finished compiler/backend/ag32                                 1m26s   1GB
Jan 14 10:00:16 Starting compiler/parsing/proofs
Jan 14 10:00:18 Finished compiler/parsing/proofs                                  1s  18MB
Jan 14 10:00:18 Starting compiler/inference/proofs
Jan 14 10:00:20 Finished compiler/inference/proofs                                1s  22MB
Jan 14 10:00:20 Starting compiler/backend/semantics
Jan 14 10:01:34 Finished compiler/backend/semantics                            1m14s   1GB
Jan 14 10:01:34 Starting compiler/backend/reg_alloc/proofs
Jan 14 10:01:36 Finished compiler/backend/reg_alloc/proofs                        1s  23MB
Jan 14 10:01:36 Starting compiler/backend/proofs
Jan 14 10:02:34 Finished compiler/backend/proofs                                 57s   2GB
Jan 14 10:02:34 Starting compiler/backend/serialiser
Jan 14 10:02:37 Finished compiler/backend/serialiser                              2s  40MB
Jan 14 10:02:37 Starting compiler/encoders/x64/proofs
Jan 14 10:12:29 Finished compiler/encoders/x64/proofs                          9m51s   5GB
Jan 14 10:12:29 Starting compiler/encoders/arm7/proofs
Jan 14 10:26:25 Finished compiler/encoders/arm7/proofs                        13m55s   4GB
Jan 14 10:26:25 Starting compiler/encoders/arm8/proofs
Jan 14 10:33:30 Finished compiler/encoders/arm8/proofs                         7m04s   1GB
Jan 14 10:33:30 Starting compiler/encoders/arm8_asl/proofs
Jan 14 11:26:01 Finished compiler/encoders/arm8_asl/proofs                    52m30s   8GB
Jan 14 11:26:01 Starting compiler/encoders/mips/proofs
Jan 14 11:36:45 Finished compiler/encoders/mips/proofs                        10m43s   2GB
Jan 14 11:36:45 Starting compiler/encoders/riscv/proofs
Jan 14 11:45:42 Finished compiler/encoders/riscv/proofs                        8m57s   1GB
Jan 14 11:45:42 Starting compiler/encoders/ag32/proofs
Jan 14 11:48:12 Finished compiler/encoders/ag32/proofs                         2m29s   1GB
Jan 14 11:48:12 Starting compiler/backend/x64/proofs
Jan 14 11:48:43 Finished compiler/backend/x64/proofs                             30s   1GB
Jan 14 11:48:43 Starting compiler/backend/arm7/proofs
Jan 14 11:49:17 Finished compiler/backend/arm7/proofs                            33s   2GB
Jan 14 11:49:17 Starting compiler/backend/arm8/proofs
Jan 14 11:49:50 Finished compiler/backend/arm8/proofs                            32s   2GB
Jan 14 11:49:50 Starting compiler/backend/arm8_asl
Jan 14 11:50:13 Finished compiler/backend/arm8_asl                               23s   1GB
Jan 14 11:50:14 Starting compiler/backend/mips/proofs
Jan 14 11:50:48 Finished compiler/backend/mips/proofs                            34s   2GB
Jan 14 11:50:48 Starting compiler/backend/riscv/proofs
Jan 14 11:51:23 Finished compiler/backend/riscv/proofs                           35s   2GB
Jan 14 11:51:23 Starting compiler/backend/ag32/proofs
Jan 14 12:05:03 Finished compiler/backend/ag32/proofs                         13m39s   2GB
Jan 14 12:05:03 Starting candle/set-theory
Jan 14 12:05:42 Finished candle/set-theory                                       39s   1GB
Jan 14 12:05:42 Starting candle/syntax-lib
Jan 14 12:05:44 Finished candle/syntax-lib                                        1s  20MB
Jan 14 12:05:44 Starting candle/standard/syntax
Jan 14 12:05:56 Finished candle/standard/syntax                                  11s 697MB
Jan 14 12:05:56 Starting candle/standard/semantics
Jan 14 12:07:56 Finished candle/standard/semantics                             1m59s   1GB
Jan 14 12:07:56 Starting candle/standard/monadic
Jan 14 12:07:58 Finished candle/standard/monadic                                  1s  21MB
Jan 14 12:07:58 Starting candle/standard/ml_kernel
Jan 14 12:09:40 Finished candle/standard/ml_kernel                             1m42s   3GB
Jan 14 12:09:40 Starting candle/overloading/syntax
Jan 14 12:13:03 Finished candle/overloading/syntax                             3m22s   1GB
Jan 14 12:13:03 Starting candle/overloading/semantics
Jan 14 12:25:34 Finished candle/overloading/semantics                         12m30s   2GB
Jan 14 12:25:34 Starting candle/overloading/monadic
Jan 14 12:28:21 Finished candle/overloading/monadic                            2m47s   2GB
Jan 14 12:28:21 Starting candle/overloading/ml_kernel
Jan 14 12:36:18 Finished candle/overloading/ml_kernel                          7m56s   3GB
Jan 14 12:36:18 Starting candle/overloading/ml_checker
Jan 14 12:38:55 Finished candle/overloading/ml_checker                         2m37s   3GB
Jan 14 12:38:55 Starting candle/prover
Jan 14 12:49:00 Finished candle/prover                                        10m04s   3GB
Jan 14 12:49:01 Starting pancake
Jan 14 12:49:44 Finished pancake                                                 43s 886MB
Jan 14 12:49:44 Starting pancake/ffi
Jan 14 12:49:45 Finished pancake/ffi                                              0s  13MB
Jan 14 12:49:45 Starting pancake/semantics
Jan 14 12:52:11 Finished pancake/semantics                                     2m25s   1GB
Jan 14 12:52:11 Starting pancake/parser
Jan 14 12:52:34 Finished pancake/parser                                          22s 905MB
Jan 14 12:52:34 Starting pancake/proofs
Jan 14 13:25:54 Finished pancake/proofs                                       33m20s   7GB
Jan 14 13:25:55 Starting characteristic/examples
Jan 14 13:27:40 Finished characteristic/examples                               1m45s   2GB
Jan 14 13:27:40 Starting tutorial/solutions
Jan 14 13:43:06 Finished tutorial/solutions                                   15m25s   8GB
Jan 14 13:43:06 Starting translator/monadic/examples
Jan 14 13:47:13 Finished translator/monadic/examples                           4m06s   3GB
Jan 14 13:47:13 Starting examples
Jan 14 14:03:42 Finished examples                                             16m29s   4GB
Jan 14 14:03:42 Starting examples/compilation/x64
Jan 14 16:03:50 Finished examples/compilation/x64                           2h00m07s  19GB
Jan 14 16:03:50 Starting examples/compilation/x64/proofs
Jan 14 16:06:26 Finished examples/compilation/x64/proofs                       2m35s   4GB
Jan 14 16:06:26 Starting examples/compilation/ag32
Jan 14 16:36:51 Finished examples/compilation/ag32                            30m24s   9GB
Jan 14 16:36:51 Starting examples/compilation/ag32/proofs
Jan 14 16:37:54 Finished examples/compilation/ag32/proofs                      1m03s   5GB
Jan 14 16:37:54 Starting examples/compilation/to_word
Jan 14 16:41:21 Finished examples/compilation/to_word                          3m26s   4GB
Jan 14 16:41:21 Starting examples/lpr_checker
Jan 14 16:42:27 Finished examples/lpr_checker                                  1m05s   1GB
Jan 14 16:42:27 Starting examples/lpr_checker/array
Jan 14 17:13:46 Finished examples/lpr_checker/array                           31m19s   5GB
Jan 14 17:13:46 Starting examples/lpr_checker/array/compilation
Jan 14 18:05:20 Finished examples/lpr_checker/array/compilation               51m33s  20GB
Jan 14 18:05:20 Starting examples/lpr_checker/array/compilation/proofs
Jan 14 18:07:27 Finished examples/lpr_checker/array/compilation/proofs         2m07s   3GB
Jan 14 18:07:27 Starting examples/lpr_checker/array/compilation/proofsARM8
Jan 14 18:14:08 Finished examples/lpr_checker/array/compilation/proofsARM8     6m40s  11GB
Jan 14 18:14:08 Starting examples/pseudo_bool
Jan 14 18:15:56 Finished examples/pseudo_bool                                  1m47s   1GB
Jan 14 18:15:56 Starting examples/pseudo_bool/cnf_encoding
Jan 14 18:16:22 Finished examples/pseudo_bool/cnf_encoding                       25s 744MB
Jan 14 18:16:22 Starting examples/pseudo_bool/graph_encoding
Jan 14 18:17:04 Finished examples/pseudo_bool/graph_encoding                     42s 795MB
Jan 14 18:17:04 Starting examples/pseudo_bool/array
Jan 14 19:10:35 Finished examples/pseudo_bool/array                           53m30s   5GB
Jan 14 19:10:35 Starting examples/pseudo_bool/array/compilation
Jan 14 22:06:53 Finished examples/pseudo_bool/array/compilation             2h56m17s  34GB
Jan 14 22:06:53 Starting examples/pseudo_bool/array/compilation/proofs
Jan 14 22:09:46 Finished examples/pseudo_bool/array/compilation/proofs         2m53s   6GB
Jan 14 22:09:46 Starting examples/opentheory
Jan 14 22:20:44 Finished examples/opentheory                                  10m57s   4GB
Jan 14 22:20:44 Starting examples/opentheory
Jan 14 22:20:46 Finished examples/opentheory                                      1s  28MB
Jan 14 22:20:46 Starting examples/opentheory/compilation
Jan 14 22:58:45 Finished examples/opentheory/compilation                      37m58s  35GB
Jan 14 22:58:45 Starting examples/opentheory/compilation/proofs
Jan 14 22:59:46 Finished examples/opentheory/compilation/proofs                1m01s   4GB
Jan 14 22:59:46 Starting examples/opentheory/compilation/ag32
Jan 14 23:32:21 Finished examples/opentheory/compilation/ag32                 32m34s  29GB
Jan 14 23:32:21 Starting examples/opentheory/compilation/ag32/proofs
Jan 14 23:34:34 Finished examples/opentheory/compilation/ag32/proofs           2m12s   8GB
Jan 14 23:34:34 Starting examples/sat_encodings
Jan 14 23:36:39 Finished examples/sat_encodings                                2m05s 935MB
Jan 14 23:36:39 Starting examples/sat_encodings/case_studies
Jan 14 23:38:27 Finished examples/sat_encodings/case_studies                   1m47s   1GB
Jan 14 23:38:28 Starting examples/sat_encodings/translation
Jan 14 23:44:38 Finished examples/sat_encodings/translation                    6m10s   3GB
Jan 14 23:44:38 Starting examples/sat_encodings/translation/compilation
Jan 15 00:31:21 Finished examples/sat_encodings/translation/compilation       46m42s  20GB
Jan 15 00:31:21 Starting examples/deflate
Jan 15 00:32:21 Finished examples/deflate                                      1m00s 822MB
Jan 15 00:32:21 Starting examples/deflate/translation
Jan 15 00:34:12 Finished examples/deflate/translation                          1m50s   4GB
Jan 15 00:34:12 Starting examples/deflate/translation/compilation
Jan 15 00:54:14 Finished examples/deflate/translation/compilation             20m02s  15GB
Jan 15 00:54:14 Starting examples/vipr
Jan 15 00:58:21 Finished examples/vipr                                         4m06s   4GB
Jan 15 00:58:21 Starting examples/vipr/compilation
Jan 15 01:19:20 Finished examples/vipr/compilation                            20m58s  17GB
Jan 15 01:19:20 Starting translator/okasaki-examples
Jan 15 01:24:35 Finished translator/okasaki-examples                           5m14s   2GB
Jan 15 01:24:35 Starting translator/other-examples
Jan 15 01:27:17 Finished translator/other-examples                             2m42s   1GB
Jan 15 01:27:18 Starting compiler/parsing/tests
Jan 15 01:27:50 Finished compiler/parsing/tests                                  32s 813MB
Jan 15 01:27:50 Starting compiler/inference/tests
Jan 15 01:36:23 Finished compiler/inference/tests                              8m33s   4GB
Jan 15 01:36:23 Starting compiler/printing/test
Jan 15 01:40:18 Finished compiler/printing/test                                3m54s   3GB
Jan 15 01:40:18 Starting icing/flover
Jan 15 02:23:46 Finished icing/flover                                         43m27s   2GB
Jan 15 02:23:46 Starting icing/
Jan 15 03:17:20 Finished icing/                                               53m33s   8GB
Jan 15 03:17:20 Starting icing/examples
Jan 15 03:18:56 Finished icing/examples                                        1m35s   3GB
Jan 15 03:18:56 Starting compiler/repl
Jan 15 03:27:57 Finished compiler/repl                                         9m00s   5GB
Jan 15 03:27:57 Starting unverified/sexpr-bootstrap/x64/64
Jan 15 03:41:31 Finished unverified/sexpr-bootstrap/x64/64                    13m33s  16GB
Jan 15 03:41:31 Starting unverified/sexpr-bootstrap/x64/32
Jan 15 03:52:38 Finished unverified/sexpr-bootstrap/x64/32                    11m06s  13GB
Jan 15 03:52:38 Starting compiler/benchmarks
Jan 15 04:08:18 Finished compiler/benchmarks                                  15m39s   2GB
Jan 15 04:08:18 Starting compiler/bootstrap/compilation/x64/64
Jan 15 16:04:41 Finished compiler/bootstrap/compilation/x64/64             11h56m22s  64GB
Jan 15 16:04:41 Starting compiler/bootstrap/compilation/x64/64/proofs
Jan 15 16:25:37 Finished compiler/bootstrap/compilation/x64/64/proofs         20m55s  24GB
Jan 15 16:25:37 Starting compiler/bootstrap/compilation/x64/32
Jan 15 23:43:07 Finished compiler/bootstrap/compilation/x64/32              7h17m29s  64GB
Jan 15 23:43:07 Starting compiler/bootstrap/compilation/x64/32/proofs
Jan 15 23:46:20 Finished compiler/bootstrap/compilation/x64/32/proofs          3m13s  21GB
Jan 15 23:46:20 Starting compiler/bootstrap/compilation/ag32/32
Jan 16 07:14:22 Finished compiler/bootstrap/compilation/ag32/32             7h28m01s  64GB
Jan 16 07:14:22 Starting compiler/bootstrap/compilation/ag32/32/proofs
Jan 16 07:21:44 Finished compiler/bootstrap/compilation/ag32/32/proofs         7m21s  41GB
Jan 16 07:21:44 SUCCESS