CakeML Regression Test

Job 2767

CakeML:9d8f9055a279b0866110174117f655f55f6c861a
  Remove redundant theorem in misc. Fixes #1124 [Jan 25 17:39:38]
#1125 (1124-remove-misctheoryalist_insert_pull_insert)
Merging into:7a0bcc6c0345d8f4081aa961bbab662d063864f0
  Merge pull request #1119 from CakeML/ordinarymath-patch-1 [Jan 23 05:26:11]
HOL:5c113170525b75be2ec405b1079ec20d2008f2c4
  Remove some more adjoin_to* (from pairScript.sml) [Jan 20 23:55:48]
Machine:pavlova

Jan 25 18:42:22 Claimed job
Jan 25 18:42:29 Reusing HOL
Jan 25 18:42:40 Starting developers
Jan 25 18:42:44 Finished developers                                               3s 213MB
Jan 25 18:42:45 Starting developers/bin
Jan 25 18:42:52 Finished developers/bin                                           5s 746MB
Jan 25 18:42:52 Starting misc
Jan 25 18:43:36 Finished misc                                                    42s   2GB
Jan 25 18:43:37 Starting compiler/proofs
Jan 25 20:21:36 Finished compiler/proofs                                    1h37m58s  28GB
Jan 25 20:21:37 Starting compiler/bootstrap/translation
Jan 26 02:08:29 Finished compiler/bootstrap/translation                     5h46m50s  80GB
Jan 26 02:08:30 Starting semantics/ffi
Jan 26 02:08:40 Finished semantics/ffi                                            9s 573MB
Jan 26 02:08:41 Starting semantics
Jan 26 02:08:42 Finished semantics                                                0s  52MB
Jan 26 02:08:43 Starting semantics/proofs
Jan 26 02:09:07 Finished semantics/proofs                                        22s 748MB
Jan 26 02:09:08 Starting semantics/alt_semantics
Jan 26 02:09:29 Finished semantics/alt_semantics                                 20s 880MB
Jan 26 02:09:30 Starting semantics/alt_semantics/proofs
Jan 26 02:19:51 Finished semantics/alt_semantics/proofs                       10m20s   2GB
Jan 26 02:19:52 Starting basis/pure
Jan 26 02:19:54 Finished basis/pure                                               0s  59MB
Jan 26 02:19:55 Starting translator
Jan 26 02:21:26 Finished translator                                            1m29s   3GB
Jan 26 02:21:26 Starting compiler/parsing
Jan 26 02:21:28 Finished compiler/parsing                                         0s  61MB
Jan 26 02:21:29 Starting characteristic
Jan 26 02:21:31 Finished characteristic                                           0s  88MB
Jan 26 02:21:31 Starting translator/monadic
Jan 26 02:21:33 Finished translator/monadic                                       0s  88MB
Jan 26 02:21:34 Starting translator/monadic/monad_base
Jan 26 02:21:35 Finished translator/monadic/monad_base                            0s  52MB
Jan 26 02:21:36 Starting basis
Jan 26 02:24:03 Finished basis                                                 2m26s   4GB
Jan 26 02:24:04 Starting compiler
Jan 26 02:24:07 Finished compiler                                                 1s 200MB
Jan 26 02:24:08 Starting compiler/inference
Jan 26 02:24:10 Finished compiler/inference                                       0s  84MB
Jan 26 02:24:10 Starting compiler/backend/reg_alloc
Jan 26 02:24:12 Finished compiler/backend/reg_alloc                               0s  53MB
Jan 26 02:24:13 Starting compiler/backend/gc
Jan 26 02:24:15 Finished compiler/backend/gc                                      1s 130MB
Jan 26 02:24:16 Starting compiler/backend
Jan 26 02:24:21 Finished compiler/backend                                         4s 259MB
Jan 26 02:24:22 Starting compiler/encoders/asm
Jan 26 02:24:23 Finished compiler/encoders/asm                                    0s  85MB
Jan 26 02:24:24 Starting compiler/encoders/x64
Jan 26 02:24:26 Finished compiler/encoders/x64                                    0s  88MB
Jan 26 02:24:27 Starting compiler/encoders/arm7
Jan 26 02:24:28 Finished compiler/encoders/arm7                                   0s  92MB
Jan 26 02:24:29 Starting compiler/encoders/arm8
Jan 26 02:24:31 Finished compiler/encoders/arm8                                   0s  84MB
Jan 26 02:24:32 Starting compiler/encoders/arm8_asl
Jan 26 02:25:28 Finished compiler/encoders/arm8_asl                              55s  18GB
Jan 26 02:25:29 Starting compiler/encoders/mips
Jan 26 02:25:31 Finished compiler/encoders/mips                                   0s  88MB
Jan 26 02:25:32 Starting compiler/encoders/riscv
Jan 26 02:25:34 Finished compiler/encoders/riscv                                  0s  88MB
Jan 26 02:25:35 Starting compiler/encoders/ag32
Jan 26 02:25:36 Finished compiler/encoders/ag32                                   0s  84MB
Jan 26 02:25:37 Starting compiler/encoders/tests
Jan 26 02:25:39 Finished compiler/encoders/tests                                  1s 111MB
Jan 26 02:25:40 Starting compiler/encoders/monadic_enc
Jan 26 02:25:42 Finished compiler/encoders/monadic_enc                            1s 125MB
Jan 26 02:25:43 Starting compiler/backend/x64
Jan 26 02:25:45 Finished compiler/backend/x64                                     1s 125MB
Jan 26 02:25:46 Starting compiler/backend/arm7
Jan 26 02:25:48 Finished compiler/backend/arm7                                    1s 134MB
Jan 26 02:25:49 Starting compiler/backend/arm8
Jan 26 02:25:51 Finished compiler/backend/arm8                                    1s 135MB
Jan 26 02:25:52 Starting compiler/backend/mips
Jan 26 02:25:54 Finished compiler/backend/mips                                    1s 135MB
Jan 26 02:25:55 Starting compiler/backend/riscv
Jan 26 02:25:57 Finished compiler/backend/riscv                                   1s 125MB
Jan 26 02:25:58 Starting compiler/backend/ag32
Jan 26 02:27:04 Finished compiler/backend/ag32                                 1m05s   3GB
Jan 26 02:27:05 Starting compiler/backend/pattern_matching
Jan 26 02:27:06 Finished compiler/backend/pattern_matching                        0s  51MB
Jan 26 02:27:07 Starting compiler/parsing/ocaml
Jan 26 02:28:49 Finished compiler/parsing/ocaml                                1m40s   1GB
Jan 26 02:28:50 Starting compiler/printing
Jan 26 02:28:51 Finished compiler/printing                                        0s  90MB
Jan 26 02:28:52 Starting compiler/parsing/proofs
Jan 26 02:28:54 Finished compiler/parsing/proofs                                  0s  65MB
Jan 26 02:28:54 Starting compiler/inference/proofs
Jan 26 02:28:56 Finished compiler/inference/proofs                                0s  89MB
Jan 26 02:28:57 Starting compiler/backend/semantics
Jan 26 02:32:04 Finished compiler/backend/semantics                            3m06s   2GB
Jan 26 02:32:05 Starting compiler/backend/reg_alloc/proofs
Jan 26 02:32:07 Finished compiler/backend/reg_alloc/proofs                        0s  88MB
Jan 26 02:32:08 Starting compiler/backend/proofs
Jan 26 02:32:55 Finished compiler/backend/proofs                                 46s   2GB
Jan 26 02:32:56 Starting compiler/backend/serialiser
Jan 26 02:32:58 Finished compiler/backend/serialiser                              1s 137MB
Jan 26 02:32:59 Starting compiler/encoders/x64/proofs
Jan 26 02:43:17 Finished compiler/encoders/x64/proofs                         10m17s   5GB
Jan 26 02:43:18 Starting compiler/encoders/arm7/proofs
Jan 26 02:56:38 Finished compiler/encoders/arm7/proofs                        13m19s  10GB
Jan 26 02:56:39 Starting compiler/encoders/arm8/proofs
Jan 26 03:03:46 Finished compiler/encoders/arm8/proofs                         7m06s   4GB
Jan 26 03:03:47 Starting compiler/encoders/arm8_asl/proofs
Jan 26 03:19:27 Finished compiler/encoders/arm8_asl/proofs                    15m38s   4GB
Jan 26 03:19:28 Starting compiler/encoders/mips/proofs
Jan 26 03:29:36 Finished compiler/encoders/mips/proofs                        10m07s   9GB
Jan 26 03:29:37 Starting compiler/encoders/riscv/proofs
Jan 26 03:38:04 Finished compiler/encoders/riscv/proofs                        8m25s   3GB
Jan 26 03:38:04 Starting compiler/encoders/ag32/proofs
Jan 26 03:40:58 Finished compiler/encoders/ag32/proofs                         2m52s   1GB
Jan 26 03:40:58 Starting compiler/backend/x64/proofs
Jan 26 03:41:32 Finished compiler/backend/x64/proofs                             32s   2GB
Jan 26 03:41:33 Starting compiler/backend/arm7/proofs
Jan 26 03:42:04 Finished compiler/backend/arm7/proofs                            30s   2GB
Jan 26 03:42:05 Starting compiler/backend/arm8/proofs
Jan 26 03:42:35 Finished compiler/backend/arm8/proofs                            29s   2GB
Jan 26 03:42:36 Starting compiler/backend/arm8_asl
Jan 26 03:42:57 Finished compiler/backend/arm8_asl                               20s   2GB
Jan 26 03:42:58 Starting compiler/backend/mips/proofs
Jan 26 03:43:28 Finished compiler/backend/mips/proofs                            29s   2GB
Jan 26 03:43:29 Starting compiler/backend/riscv/proofs
Jan 26 03:44:04 Finished compiler/backend/riscv/proofs                           33s   2GB
Jan 26 03:44:05 Starting compiler/backend/ag32/proofs
Jan 26 03:57:52 Finished compiler/backend/ag32/proofs                         13m46s   4GB
Jan 26 03:57:53 Starting compiler/backend/cv_compute
Jan 26 03:59:04 Finished compiler/backend/cv_compute                           1m10s   2GB
Jan 26 03:59:05 Starting cv_translator
Jan 26 04:20:23 Finished cv_translator                                        21m16s   9GB
Jan 26 04:20:24 Starting candle
Jan 26 04:20:25 Finished candle                                                   0s  12MB
Jan 26 04:20:26 Starting candle/set-theory
Jan 26 04:21:01 Finished candle/set-theory                                       34s   1GB
Jan 26 04:21:02 Starting candle/syntax-lib
Jan 26 04:21:03 Finished candle/syntax-lib                                        0s  60MB
Jan 26 04:21:04 Starting candle/standard
Jan 26 04:21:05 Finished candle/standard                                          0s  12MB
Jan 26 04:21:06 Starting candle/standard/syntax
Jan 26 04:21:19 Finished candle/standard/syntax                                  11s 779MB
Jan 26 04:21:19 Starting candle/standard/semantics
Jan 26 04:23:21 Finished candle/standard/semantics                             2m00s   1GB
Jan 26 04:23:22 Starting candle/standard/monadic
Jan 26 04:23:24 Finished candle/standard/monadic                                  0s  89MB
Jan 26 04:23:25 Starting candle/standard/ml_kernel
Jan 26 04:25:08 Finished candle/standard/ml_kernel                             1m42s   4GB
Jan 26 04:25:09 Starting candle/standard/ml_kernel/lisp
Jan 26 04:25:10 Finished candle/standard/ml_kernel/lisp                           0s  45MB
Jan 26 04:25:11 Starting candle/overloading
Jan 26 04:25:12 Finished candle/overloading                                       0s  11MB
Jan 26 04:25:13 Starting candle/overloading/syntax
Jan 26 04:28:22 Finished candle/overloading/syntax                             3m07s   2GB
Jan 26 04:28:23 Starting candle/overloading/semantics
Jan 26 04:39:29 Finished candle/overloading/semantics                         11m05s   4GB
Jan 26 04:39:30 Starting candle/overloading/monadic
Jan 26 04:41:47 Finished candle/overloading/monadic                            2m16s   2GB
Jan 26 04:41:48 Starting candle/overloading/ml_kernel
Jan 26 04:49:01 Finished candle/overloading/ml_kernel                          7m11s   5GB
Jan 26 04:49:02 Starting candle/overloading/ml_checker
Jan 26 04:51:10 Finished candle/overloading/ml_checker                         2m07s   6GB
Jan 26 04:51:11 Starting candle/prover
Jan 26 05:00:54 Finished candle/prover                                         9m42s   5GB
Jan 26 05:00:55 Starting candle/prover/compute
Jan 26 05:00:57 Finished candle/prover/compute                                    1s 114MB
Jan 26 05:00:58 Starting pancake
Jan 26 05:01:20 Finished pancake                                                 20s 836MB
Jan 26 05:01:21 Starting pancake/semantics
Jan 26 05:03:31 Finished pancake/semantics                                     2m09s   1GB
Jan 26 05:03:32 Starting pancake/parser
Jan 26 05:03:55 Finished pancake/parser                                          22s 455MB
Jan 26 05:03:56 Starting pancake/proofs
Jan 26 05:20:06 Finished pancake/proofs                                       16m08s   7GB
Jan 26 05:20:07 Starting pancake/ta_progs
Jan 26 05:20:08 Finished pancake/ta_progs                                         0s  11MB
Jan 26 05:20:08 Starting compiler/dafny
Jan 26 05:22:47 Finished compiler/dafny                                        2m36s   8GB
Jan 26 05:22:47 Starting compiler/dafny/translation
Jan 26 05:40:47 Finished compiler/dafny/translation                           17m58s  17GB
Jan 26 05:40:48 Starting compiler/dafny/compilation
Jan 26 05:43:16 Finished compiler/dafny/compilation                            2m27s   7GB
Jan 26 05:43:16 Starting compiler/dafny/semantics
Jan 26 05:43:53 Finished compiler/dafny/semantics                                36s   1GB
Jan 26 05:43:54 Starting characteristic/examples
Jan 26 05:45:20 Finished characteristic/examples                               1m25s   4GB
Jan 26 05:45:21 Starting tutorial/solutions
Jan 26 05:47:41 Finished tutorial/solutions                                    2m19s   3GB
Jan 26 05:47:42 Starting translator/monadic/examples
Jan 26 05:50:34 Finished translator/monadic/examples                           2m51s   3GB
Jan 26 05:50:35 Starting examples
Jan 26 05:56:32 Finished examples                                              5m55s   4GB
Jan 26 05:56:32 Starting examples/compilation
Jan 26 05:56:33 Finished examples/compilation                                     0s  11MB
Jan 26 05:56:34 Starting examples/compilation/x64
Jan 26 06:03:08 Finished examples/compilation/x64                              6m33s   4GB
Jan 26 06:03:09 Starting examples/compilation/x64/proofs
Jan 26 06:05:35 Finished examples/compilation/x64/proofs                       2m25s   4GB
Jan 26 06:05:36 Starting examples/compilation/ag32
Jan 26 06:07:25 Finished examples/compilation/ag32                             1m47s   2GB
Jan 26 06:07:25 Starting examples/compilation/ag32/proofs
Jan 26 06:08:28 Finished examples/compilation/ag32/proofs                      1m01s   5GB
Jan 26 06:08:29 Starting examples/lpr_checker
Jan 26 06:08:59 Finished examples/lpr_checker                                    29s   1GB
Jan 26 06:08:59 Starting examples/lpr_checker/array
Jan 26 06:35:17 Finished examples/lpr_checker/array                           26m16s  28GB
Jan 26 06:35:18 Starting examples/lpr_checker/array/compilation
Jan 26 06:43:26 Finished examples/lpr_checker/array/compilation                8m07s  36GB
Jan 26 06:43:27 Starting examples/lpr_checker/array/compilation/proofs
Jan 26 06:44:37 Finished examples/lpr_checker/array/compilation/proofs         1m08s   6GB
Jan 26 06:44:38 Starting examples/lpr_checker/array/compilation/proofsARM8
Jan 26 06:45:46 Finished examples/lpr_checker/array/compilation/proofsARM8     1m07s   6GB
Jan 26 06:45:47 Starting .
Jan 26 06:45:50 Finished .                                                        2s 280MB
Jan 26 06:45:51 Starting examples/xlrup_checker
Jan 26 06:46:25 Finished examples/xlrup_checker                                  32s   1GB
Jan 26 06:46:26 Starting examples/xlrup_checker/array
Jan 26 06:59:28 Finished examples/xlrup_checker/array                         13m00s   8GB
Jan 26 06:59:29 Starting examples/xlrup_checker/array/compilation
Jan 26 07:00:27 Finished examples/xlrup_checker/array/compilation                57s   4GB
Jan 26 07:00:28 Starting examples/xlrup_checker/array/compilation/proofs
Jan 26 07:01:27 Finished examples/xlrup_checker/array/compilation/proofs         58s   5GB
Jan 26 07:01:28 Starting examples/pseudo_bool
Jan 26 07:02:59 Finished examples/pseudo_bool                                  1m30s   2GB
Jan 26 07:03:00 Starting examples/pseudo_bool/cnf_encoding
Jan 26 07:03:28 Finished examples/pseudo_bool/cnf_encoding                       27s   1GB
Jan 26 07:03:29 Starting examples/pseudo_bool/graph_encoding
Jan 26 07:04:14 Finished examples/pseudo_bool/graph_encoding                     43s   1GB
Jan 26 07:04:15 Starting examples/pseudo_bool/array
Jan 26 08:12:24 Finished examples/pseudo_bool/array                         1h08m07s  28GB
Jan 26 08:12:25 Starting examples/pseudo_bool/array/compilation
Jan 26 08:21:04 Finished examples/pseudo_bool/array/compilation                8m38s  15GB
Jan 26 08:21:05 Starting examples/pseudo_bool/array/compilation/proofs
Jan 26 08:23:38 Finished examples/pseudo_bool/array/compilation/proofs         2m32s   6GB
Jan 26 08:23:39 Starting examples/pseudo_bool/array/compilation/proofsARM8
Jan 26 08:24:51 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m11s   6GB
Jan 26 08:24:52 Starting examples/opentheory
Jan 26 08:33:22 Finished examples/opentheory                                   8m29s   4GB
Jan 26 08:33:23 Starting examples/opentheory/compilation
Jan 26 08:34:50 Finished examples/opentheory/compilation                       1m26s   5GB
Jan 26 08:34:51 Starting examples/opentheory/compilation/proofs
Jan 26 08:35:53 Finished examples/opentheory/compilation/proofs                1m01s   4GB
Jan 26 08:35:54 Starting examples/opentheory/compilation/ag32
Jan 26 08:37:25 Finished examples/opentheory/compilation/ag32                  1m30s   6GB
Jan 26 08:37:26 Starting examples/opentheory/compilation/ag32/proofs
Jan 26 08:39:04 Finished examples/opentheory/compilation/ag32/proofs           1m36s   8GB
Jan 26 08:39:05 Starting examples/sat_encodings
Jan 26 08:40:04 Finished examples/sat_encodings                                  58s 869MB
Jan 26 08:40:05 Starting examples/sat_encodings/demo
Jan 26 08:40:06 Finished examples/sat_encodings/demo                              0s  12MB
Jan 26 08:40:07 Starting examples/sat_encodings/case_studies
Jan 26 08:41:54 Finished examples/sat_encodings/case_studies                   1m45s   1GB
Jan 26 08:41:55 Starting examples/sat_encodings/translation
Jan 26 08:45:33 Finished examples/sat_encodings/translation                    3m37s   2GB
Jan 26 08:45:34 Starting examples/sat_encodings/translation/compilation
Jan 26 08:47:22 Finished examples/sat_encodings/translation/compilation        1m46s   4GB
Jan 26 08:47:23 Starting examples/deflate
Jan 26 08:47:50 Finished examples/deflate                                        26s 653MB
Jan 26 08:47:51 Starting examples/deflate/translation
Jan 26 08:48:57 Finished examples/deflate/translation                          1m04s   4GB
Jan 26 08:48:58 Starting examples/deflate/translation/compilation
Jan 26 08:49:44 Finished examples/deflate/translation/compilation                45s   3GB
Jan 26 08:49:45 Starting examples/vipr
Jan 26 08:53:14 Finished examples/vipr                                         3m27s   4GB
Jan 26 08:53:15 Starting examples/vipr/compilation
Jan 26 08:54:08 Finished examples/vipr/compilation                               52s   4GB
Jan 26 08:54:09 Starting translator/okasaki-examples
Jan 26 08:58:16 Finished translator/okasaki-examples                           4m05s   3GB
Jan 26 08:58:17 Starting translator/other-examples
Jan 26 08:59:07 Finished translator/other-examples                               49s   3GB
Jan 26 08:59:08 Starting translator/other-examples/auxiliary
Jan 26 08:59:09 Finished translator/other-examples/auxiliary                      0s  11MB
Jan 26 08:59:10 Starting compiler/parsing/tests
Jan 26 08:59:45 Finished compiler/parsing/tests                                  34s   1GB
Jan 26 08:59:46 Starting compiler/inference/tests
Jan 26 09:00:21 Finished compiler/inference/tests                                33s   2GB
Jan 26 09:00:22 Starting compiler/printing/test
Jan 26 09:01:32 Finished compiler/printing/test                                1m09s   4GB
Jan 26 09:01:33 Starting icing/flover
Jan 26 09:36:06 Finished icing/flover                                         34m31s   1GB
Jan 26 09:36:07 Starting icing/flover/Infra
Jan 26 09:36:08 Finished icing/flover/Infra                                       0s  11MB
Jan 26 09:36:08 Starting icing/flover/semantics
Jan 26 09:36:09 Finished icing/flover/semantics                                   0s  12MB
Jan 26 09:36:10 Starting icing/
Jan 26 10:03:22 Finished icing/                                               27m10s   7GB
Jan 26 10:03:23 Starting icing/examples
Jan 26 10:04:58 Finished icing/examples                                        1m34s   7GB
Jan 26 10:04:59 Starting compiler/repl
Jan 26 10:12:57 Finished compiler/repl                                         7m57s   7GB
Jan 26 10:12:58 Starting unverified/sexpr-bootstrap/x64/64
Jan 26 10:16:57 Finished unverified/sexpr-bootstrap/x64/64                     3m57s  18GB
Jan 26 10:16:58 Starting unverified/sexpr-bootstrap/x64/32
Jan 26 10:20:23 Finished unverified/sexpr-bootstrap/x64/32                     3m24s  15GB
Jan 26 10:20:24 Starting compiler/benchmarks
Jan 26 10:21:10 Finished compiler/benchmarks                                     44s 712MB
Jan 26 10:21:11 Starting compiler/benchmarks/cakeml_benchmarks/cakeml
Jan 26 10:21:14 Finished compiler/benchmarks/cakeml_benchmarks/cakeml             2s 255MB
Jan 26 10:21:15 Starting compiler/benchmarks/mlton_benchmarks/cakeml
Jan 26 10:21:18 Finished compiler/benchmarks/mlton_benchmarks/cakeml              2s 257MB
Jan 26 10:21:19 Starting compiler/bootstrap/compilation/x64/64
Jan 26 10:43:01 Finished compiler/bootstrap/compilation/x64/64                21m41s  57GB
Jan 26 10:43:02 Starting compiler/bootstrap/compilation/x64/64/proofs
Jan 26 11:07:24 Finished compiler/bootstrap/compilation/x64/64/proofs         24m21s  54GB
Jan 26 11:07:25 Starting compiler/bootstrap/compilation/x64/32
Jan 26 11:31:51 Finished compiler/bootstrap/compilation/x64/32                24m25s  62GB
Jan 26 11:31:52 Starting compiler/bootstrap/compilation/x64/32/proofs
Jan 26 11:36:00 Finished compiler/bootstrap/compilation/x64/32/proofs          4m07s  24GB
Jan 26 11:36:01 Starting compiler/bootstrap/compilation/arm8/64
Jan 26 12:12:20 Finished compiler/bootstrap/compilation/arm8/64               36m17s  78GB
Jan 26 12:12:21 Starting compiler/bootstrap/compilation/arm8/64/proofs
Jan 26 12:17:36 Finished compiler/bootstrap/compilation/arm8/64/proofs         5m14s  28GB
Jan 26 12:17:37 Starting compiler/bootstrap/compilation/ag32/32
Jan 26 12:42:54 Finished compiler/bootstrap/compilation/ag32/32               25m16s  65GB
Jan 26 12:42:55 Starting compiler/bootstrap/compilation/ag32/32/proofs
Jan 26 12:47:44 Finished compiler/bootstrap/compilation/ag32/32/proofs         4m48s  30GB
Jan 26 12:47:45 SUCCESS