Job 1810

CakeML:a94b08d68372d18b3de5703f212a08aa713df665
  Merge pull request #861 from mktnk3/pan-to-mc_updated [Feb 28 10:36:05]
HOL:056df98e1f9596a4b6565e74abc49207247cc49b
  More tweaks to DefnBase, and more test cases [Feb 28 00:06:07]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux
Artefacts:cake-x64-32.tar.gz
cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz

Mar 01 02:40:04 Claimed job
Mar 01 02:40:07 Building HOL
Mar 01 02:49:45 Starting developers
Mar 01 02:49:49 Finished developers                                               4s 132MB
Mar 01 02:49:49 Starting developers/bin
Mar 01 02:49:53 Finished developers/bin                                           4s 675MB
Mar 01 02:49:53 Starting semantics/ffi
Mar 01 02:50:03 Finished semantics/ffi                                            9s 262MB
Mar 01 02:50:03 Starting semantics
Mar 01 02:52:17 Finished semantics                                             2m13s   1GB
Mar 01 02:52:17 Starting semantics/proofs
Mar 01 02:55:58 Finished semantics/proofs                                      3m40s   1GB
Mar 01 02:55:58 Starting semantics/alt_semantics
Mar 01 02:56:14 Finished semantics/alt_semantics                                 16s 503MB
Mar 01 02:56:14 Starting semantics/alt_semantics/proofs
Mar 01 02:58:43 Finished semantics/alt_semantics/proofs                        2m28s 886MB
Mar 01 02:58:43 Starting basis/pure
Mar 01 03:01:32 Finished basis/pure                                            2m48s 887MB
Mar 01 03:01:32 Starting translator
Mar 01 03:04:35 Finished translator                                            3m02s   1GB
Mar 01 03:04:35 Starting compiler/parsing
Mar 01 03:05:51 Finished compiler/parsing                                      1m16s   2GB
Mar 01 03:05:51 Starting characteristic
Mar 01 03:12:14 Finished characteristic                                        6m22s   2GB
Mar 01 03:12:14 Starting translator/monadic
Mar 01 03:14:09 Finished translator/monadic                                    1m54s   1GB
Mar 01 03:14:09 Starting basis
Mar 01 04:00:57 Finished basis                                                46m46s  22GB
Mar 01 04:00:57 Starting compiler/inference
Mar 01 04:02:24 Finished compiler/inference                                    1m27s   1GB
Mar 01 04:02:25 Starting compiler/backend/reg_alloc
Mar 01 04:04:09 Finished compiler/backend/reg_alloc                            1m44s   1GB
Mar 01 04:04:09 Starting compiler/backend/gc
Mar 01 04:08:31 Finished compiler/backend/gc                                   4m21s   2GB
Mar 01 04:08:31 Starting compiler/backend
Mar 01 04:13:59 Finished compiler/backend                                      5m28s   2GB
Mar 01 04:13:59 Starting compiler/encoders/asm
Mar 01 04:14:29 Finished compiler/encoders/asm                                   29s 694MB
Mar 01 04:14:29 Starting compiler/encoders/x64
Mar 01 04:15:37 Finished compiler/encoders/x64                                 1m07s   1GB
Mar 01 04:15:37 Starting compiler/encoders/arm7
Mar 01 04:17:41 Finished compiler/encoders/arm7                                2m04s   1GB
Mar 01 04:17:42 Starting compiler/encoders/arm8
Mar 01 04:18:24 Finished compiler/encoders/arm8                                  42s   1GB
Mar 01 04:18:24 Starting compiler/encoders/arm8_asl
Mar 01 06:26:57 Finished compiler/encoders/arm8_asl                         2h08m29s  39GB
Mar 01 06:26:57 Starting compiler/encoders/mips
Mar 01 06:28:28 Finished compiler/encoders/mips                                1m31s   1GB
Mar 01 06:28:28 Starting compiler/encoders/riscv
Mar 01 06:30:16 Finished compiler/encoders/riscv                               1m47s   1GB
Mar 01 06:30:16 Starting compiler/encoders/ag32
Mar 01 06:30:38 Finished compiler/encoders/ag32                                  21s 689MB
Mar 01 06:30:38 Starting compiler/backend/x64
Mar 01 06:31:00 Finished compiler/backend/x64                                    21s   1GB
Mar 01 06:31:00 Starting compiler/backend/arm7
Mar 01 06:31:24 Finished compiler/backend/arm7                                   23s   1GB
Mar 01 06:31:24 Starting compiler/backend/arm8
Mar 01 06:31:47 Finished compiler/backend/arm8                                   22s   1GB
Mar 01 06:31:47 Starting compiler/backend/mips
Mar 01 06:32:10 Finished compiler/backend/mips                                   22s   1GB
Mar 01 06:32:10 Starting compiler/backend/riscv
Mar 01 06:32:32 Finished compiler/backend/riscv                                  22s   1GB
Mar 01 06:32:33 Starting compiler/backend/ag32
Mar 01 06:33:56 Finished compiler/backend/ag32                                 1m23s   1GB
Mar 01 06:33:56 Starting compiler/parsing/proofs
Mar 01 06:37:40 Finished compiler/parsing/proofs                               3m43s   1GB
Mar 01 06:37:40 Starting compiler/inference/proofs
Mar 01 06:40:12 Finished compiler/inference/proofs                             2m32s   1GB
Mar 01 06:40:13 Starting compiler/backend/semantics
Mar 01 07:07:57 Finished compiler/backend/semantics                           27m43s   2GB
Mar 01 07:07:57 Starting compiler/backend/reg_alloc/proofs
Mar 01 07:11:27 Finished compiler/backend/reg_alloc/proofs                     3m30s   1GB
Mar 01 07:11:27 Starting compiler/backend/proofs
Mar 01 08:02:58 Finished compiler/backend/proofs                              51m29s  21GB
Mar 01 08:02:58 Starting compiler/backend/serialiser
Mar 01 08:04:36 Finished compiler/backend/serialiser                           1m37s   2GB
Mar 01 08:04:36 Starting compiler/encoders/x64/proofs
Mar 01 08:14:13 Finished compiler/encoders/x64/proofs                          9m37s   3GB
Mar 01 08:14:13 Starting compiler/encoders/arm7/proofs
Mar 01 08:27:15 Finished compiler/encoders/arm7/proofs                        13m01s   4GB
Mar 01 08:27:15 Starting compiler/encoders/arm8/proofs
Mar 01 08:34:09 Finished compiler/encoders/arm8/proofs                         6m53s   1GB
Mar 01 08:34:09 Starting compiler/encoders/arm8_asl/proofs
Mar 01 09:24:00 Finished compiler/encoders/arm8_asl/proofs                    49m50s   7GB
Mar 01 09:24:00 Starting compiler/encoders/mips/proofs
Mar 01 09:33:55 Finished compiler/encoders/mips/proofs                         9m54s   3GB
Mar 01 09:33:55 Starting compiler/encoders/riscv/proofs
Mar 01 09:42:55 Finished compiler/encoders/riscv/proofs                        9m00s   1GB
Mar 01 09:42:55 Starting compiler/encoders/ag32/proofs
Mar 01 09:45:29 Finished compiler/encoders/ag32/proofs                         2m33s 680MB
Mar 01 09:45:29 Starting compiler/backend/x64/proofs
Mar 01 09:45:57 Finished compiler/backend/x64/proofs                             27s   1GB
Mar 01 09:45:57 Starting compiler/backend/arm7/proofs
Mar 01 09:46:25 Finished compiler/backend/arm7/proofs                            27s   1GB
Mar 01 09:46:25 Starting compiler/backend/arm8/proofs
Mar 01 09:46:53 Finished compiler/backend/arm8/proofs                            27s   1GB
Mar 01 09:46:53 Starting compiler/backend/arm8_asl
Mar 01 09:47:17 Finished compiler/backend/arm8_asl                               23s   1GB
Mar 01 09:47:17 Starting compiler/backend/mips/proofs
Mar 01 09:47:45 Finished compiler/backend/mips/proofs                            28s   2GB
Mar 01 09:47:45 Starting compiler/backend/riscv/proofs
Mar 01 09:48:13 Finished compiler/backend/riscv/proofs                           27s   1GB
Mar 01 09:48:13 Starting compiler/backend/ag32/proofs
Mar 01 10:00:59 Finished compiler/backend/ag32/proofs                         12m46s   3GB
Mar 01 10:00:59 Starting compiler/proofs
Mar 01 10:03:27 Finished compiler/proofs                                       2m27s   3GB
Mar 01 10:03:27 Starting candle/set-theory
Mar 01 10:04:01 Finished candle/set-theory                                       33s   1GB
Mar 01 10:04:01 Starting candle/syntax-lib
Mar 01 10:04:14 Finished candle/syntax-lib                                       13s 672MB
Mar 01 10:04:14 Starting candle/standard/syntax
Mar 01 10:06:16 Finished candle/standard/syntax                                2m01s   1GB
Mar 01 10:06:16 Starting candle/standard/semantics
Mar 01 10:08:04 Finished candle/standard/semantics                             1m48s   1GB
Mar 01 10:08:05 Starting candle/standard/monadic
Mar 01 10:09:57 Finished candle/standard/monadic                               1m52s   1GB
Mar 01 10:09:57 Starting candle/standard/ml_kernel
Mar 01 10:16:09 Finished candle/standard/ml_kernel                             6m12s   4GB
Mar 01 10:16:09 Starting candle/overloading/syntax
Mar 01 10:19:20 Finished candle/overloading/syntax                             3m10s   1GB
Mar 01 10:19:20 Starting candle/overloading/semantics
Mar 01 10:30:59 Finished candle/overloading/semantics                         11m37s   3GB
Mar 01 10:30:59 Starting candle/overloading/monadic
Mar 01 10:33:34 Finished candle/overloading/monadic                            2m34s   1GB
Mar 01 10:33:34 Starting candle/overloading/ml_kernel
Mar 01 10:40:48 Finished candle/overloading/ml_kernel                          7m14s   3GB
Mar 01 10:40:49 Starting candle/overloading/ml_checker
Mar 01 10:43:16 Finished candle/overloading/ml_checker                         2m27s   3GB
Mar 01 10:43:16 Starting candle/prover
Mar 01 10:50:45 Finished candle/prover                                         7m28s   2GB
Mar 01 10:50:45 Starting pancake
Mar 01 10:54:24 Finished pancake                                               3m39s   4GB
Mar 01 10:54:24 Starting pancake/ffi
Mar 01 10:54:24 Finished pancake/ffi                                              0s  35MB
Mar 01 10:54:24 Starting pancake/semantics
Mar 01 10:56:52 Finished pancake/semantics                                     2m28s   1GB
Mar 01 10:56:52 Starting pancake/proofs
Mar 01 11:08:50 Finished pancake/proofs                                       11m57s   5GB
Mar 01 11:08:50 Starting characteristic/examples
Mar 01 11:10:13 Finished characteristic/examples                               1m22s   2GB
Mar 01 11:10:13 Starting tutorial/solutions
Mar 01 11:26:24 Finished tutorial/solutions                                   16m11s  10GB
Mar 01 11:26:25 Starting translator/monadic/examples
Mar 01 11:30:15 Finished translator/monadic/examples                           3m50s   2GB
Mar 01 11:30:15 Starting examples
Mar 01 11:39:42 Finished examples                                              9m26s   4GB
Mar 01 11:39:42 Starting examples/compilation/x64
Mar 01 14:08:31 Finished examples/compilation/x64                           2h28m47s  17GB
Mar 01 14:08:32 Starting examples/compilation/x64/proofs
Mar 01 14:11:11 Finished examples/compilation/x64/proofs                       2m39s   3GB
Mar 01 14:11:12 Starting examples/compilation/ag32
Mar 01 14:46:04 Finished examples/compilation/ag32                            34m52s   8GB
Mar 01 14:46:04 Starting examples/compilation/ag32/proofs
Mar 01 14:46:59 Finished examples/compilation/ag32/proofs                        54s   3GB
Mar 01 14:46:59 Starting examples/cost
Mar 01 15:42:02 Finished examples/cost                                        55m01s   7GB
Mar 01 15:42:02 Starting examples/lpr_checker
Mar 01 15:43:06 Finished examples/lpr_checker                                  1m03s   1GB
Mar 01 15:43:06 Starting examples/lpr_checker/array
Mar 01 16:11:00 Finished examples/lpr_checker/array                           27m53s  11GB
Mar 01 16:11:00 Starting examples/lpr_checker/array/compilation
Mar 01 17:37:16 Finished examples/lpr_checker/array/compilation             1h26m11s  30GB
Mar 01 17:37:16 Starting examples/lpr_checker/array/compilation/proofs
Mar 01 17:39:01 Finished examples/lpr_checker/array/compilation/proofs         1m44s   6GB
Mar 01 17:39:01 Starting examples/opentheory
Mar 01 17:48:57 Finished examples/opentheory                                   9m56s   5GB
Mar 01 17:48:57 Starting examples/opentheory
Mar 01 17:48:58 Finished examples/opentheory                                      1s 130MB
Mar 01 17:48:58 Starting examples/opentheory/compilation
Mar 01 18:27:51 Finished examples/opentheory/compilation                      38m52s  31GB
Mar 01 18:27:51 Starting examples/opentheory/compilation/proofs
Mar 01 18:29:16 Finished examples/opentheory/compilation/proofs                1m25s   2GB
Mar 01 18:29:16 Starting examples/opentheory/compilation/ag32
Mar 01 19:07:18 Finished examples/opentheory/compilation/ag32                 38m00s  30GB
Mar 01 19:07:18 Starting examples/opentheory/compilation/ag32/proofs
Mar 01 19:09:04 Finished examples/opentheory/compilation/ag32/proofs           1m46s   6GB
Mar 01 19:09:04 Starting examples/sat_encodings
Mar 01 19:11:06 Finished examples/sat_encodings                                2m01s 727MB
Mar 01 19:11:06 Starting examples/sat_encodings/case_studies
Mar 01 19:12:49 Finished examples/sat_encodings/case_studies                   1m43s 965MB
Mar 01 19:12:50 Starting examples/sat_encodings/translation
Mar 01 19:18:33 Finished examples/sat_encodings/translation                    5m43s   5GB
Mar 01 19:18:33 Starting examples/sat_encodings/translation/compilation
Mar 01 20:07:45 Finished examples/sat_encodings/translation/compilation       49m11s  18GB
Mar 01 20:07:45 Starting translator/okasaki-examples
Mar 01 20:12:40 Finished translator/okasaki-examples                           4m54s   1GB
Mar 01 20:12:40 Starting translator/other-examples
Mar 01 20:14:38 Finished translator/other-examples                             1m57s   1GB
Mar 01 20:14:38 Starting compiler/parsing/tests
Mar 01 20:15:08 Finished compiler/parsing/tests                                  29s 596MB
Mar 01 20:15:08 Starting compiler/inference/tests
Mar 01 20:23:15 Finished compiler/inference/tests                              8m06s   3GB
Mar 01 20:23:15 Starting compiler/bootstrap/translation
Mar 01 22:56:41 Finished compiler/bootstrap/translation                     2h33m24s  30GB
Mar 01 22:56:41 Starting unverified/sexpr-bootstrap/x64/64
Mar 01 23:06:53 Finished unverified/sexpr-bootstrap/x64/64                    10m10s   9GB
Mar 01 23:06:53 Starting unverified/sexpr-bootstrap/x64/32
Mar 01 23:15:43 Finished unverified/sexpr-bootstrap/x64/32                     8m49s   8GB
Mar 01 23:15:43 Starting compiler/benchmarks
Mar 01 23:16:40 Finished compiler/benchmarks                                     56s 673MB
Mar 01 23:16:40 Starting compiler/bootstrap/compilation/x64/64
Mar 02 12:00:42 Finished compiler/bootstrap/compilation/x64/64             12h44m01s  64GB
Mar 02 12:00:42 Starting compiler/bootstrap/compilation/x64/64/proofs
Mar 02 12:03:36 Finished compiler/bootstrap/compilation/x64/64/proofs          2m53s  23GB
Mar 02 12:03:37 Starting compiler/bootstrap/compilation/x64/32
Mar 02 23:46:05 Finished compiler/bootstrap/compilation/x64/32             11h42m27s  64GB
Mar 02 23:46:06 Starting compiler/bootstrap/compilation/x64/32/proofs
Mar 02 23:48:37 Finished compiler/bootstrap/compilation/x64/32/proofs          2m31s  18GB
Mar 02 23:48:38 Starting compiler/bootstrap/compilation/ag32/32
Mar 03 10:54:59 Finished compiler/bootstrap/compilation/ag32/32            11h06m19s  64GB
Mar 03 10:54:59 Starting compiler/bootstrap/compilation/ag32/32/proofs
Mar 03 11:20:36 Finished compiler/bootstrap/compilation/ag32/32/proofs        25m37s  27GB
Mar 03 11:20:37 SUCCESS