Job 1718

CakeML:2efbde0cb484b93f7b764dc9571295487a6b5a70
  fix typestamp [Jan 16 20:47:13]
#857 (eval-bitmaps)
Merging into:fd3e72e7afc931fb4f4945cae710715da37ea03c
  Merge pull request #852 from CakeML/tidy-up [Jan 05 17:40:32]
HOL:af01322db66662cdba8bcd13dd1e0fa76d818bfa
  Proper names for theorems. [Jan 14 05:47:46]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Jan 16 23:18:29 Claimed job
Jan 16 23:18:32 Reusing HOL
Jan 16 23:18:44 Starting developers
Jan 16 23:18:48 Finished developers                                               4s 155MB
Jan 16 23:18:48 Starting developers/bin
Jan 16 23:18:52 Finished developers/bin                                           4s 675MB
Jan 16 23:18:52 Starting semantics/ffi
Jan 16 23:19:01 Finished semantics/ffi                                            8s 232MB
Jan 16 23:19:01 Starting semantics
Jan 16 23:20:22 Finished semantics                                             1m21s   1GB
Jan 16 23:20:22 Starting semantics/proofs
Jan 16 23:23:51 Finished semantics/proofs                                      3m29s   1GB
Jan 16 23:23:51 Starting semantics/alt_semantics
Jan 16 23:24:02 Finished semantics/alt_semantics                                 10s 414MB
Jan 16 23:24:02 Starting semantics/alt_semantics/proofs
Jan 16 23:26:26 Finished semantics/alt_semantics/proofs                        2m24s 802MB
Jan 16 23:26:26 Starting basis/pure
Jan 16 23:27:16 Finished basis/pure                                              49s 683MB
Jan 16 23:27:16 Starting translator
Jan 16 23:30:01 Finished translator                                            2m44s   1GB
Jan 16 23:30:01 Starting compiler/parsing
Jan 16 23:31:14 Finished compiler/parsing                                      1m13s   3GB
Jan 16 23:31:15 Starting characteristic
Jan 16 23:36:55 Finished characteristic                                        5m40s   2GB
Jan 16 23:36:56 Starting translator/monadic
Jan 16 23:38:35 Finished translator/monadic                                    1m39s   1GB
Jan 16 23:38:35 Starting basis
Jan 17 00:22:42 Finished basis                                                44m06s  21GB
Jan 17 00:22:43 Starting compiler/inference
Jan 17 00:23:49 Finished compiler/inference                                    1m06s   1GB
Jan 17 00:23:49 Starting compiler/backend/reg_alloc
Jan 17 00:24:55 Finished compiler/backend/reg_alloc                            1m06s   1GB
Jan 17 00:24:55 Starting compiler/backend/gc
Jan 17 00:28:09 Finished compiler/backend/gc                                   3m13s   2GB
Jan 17 00:28:09 Starting compiler/backend
Jan 17 00:32:43 Finished compiler/backend                                      4m34s   2GB
Jan 17 00:32:43 Starting compiler/encoders/asm
Jan 17 00:33:05 Finished compiler/encoders/asm                                   21s 685MB
Jan 17 00:33:05 Starting compiler/encoders/x64
Jan 17 00:33:31 Finished compiler/encoders/x64                                   25s   1GB
Jan 17 00:33:31 Starting compiler/encoders/arm7
Jan 17 00:34:22 Finished compiler/encoders/arm7                                  51s   1GB
Jan 17 00:34:22 Starting compiler/encoders/arm8
Jan 17 00:34:36 Finished compiler/encoders/arm8                                  13s 819MB
Jan 17 00:34:36 Starting compiler/encoders/mips
Jan 17 00:34:53 Finished compiler/encoders/mips                                  17s   1GB
Jan 17 00:34:54 Starting compiler/encoders/riscv
Jan 17 00:35:09 Finished compiler/encoders/riscv                                 14s 742MB
Jan 17 00:35:09 Starting compiler/encoders/ag32
Jan 17 00:35:26 Finished compiler/encoders/ag32                                  17s 663MB
Jan 17 00:35:26 Starting compiler/backend/x64
Jan 17 00:35:46 Finished compiler/backend/x64                                    19s   1GB
Jan 17 00:35:46 Starting compiler/backend/arm7
Jan 17 00:36:06 Finished compiler/backend/arm7                                   19s   1GB
Jan 17 00:36:06 Starting compiler/backend/arm8
Jan 17 00:36:25 Finished compiler/backend/arm8                                   19s   1GB
Jan 17 00:36:26 Starting compiler/backend/mips
Jan 17 00:36:45 Finished compiler/backend/mips                                   19s   1GB
Jan 17 00:36:45 Starting compiler/backend/riscv
Jan 17 00:37:05 Finished compiler/backend/riscv                                  19s   1GB
Jan 17 00:37:05 Starting compiler/backend/ag32
Jan 17 00:38:12 Finished compiler/backend/ag32                                 1m06s   1GB
Jan 17 00:38:12 Starting compiler/parsing/proofs
Jan 17 00:41:52 Finished compiler/parsing/proofs                               3m39s   1GB
Jan 17 00:41:52 Starting compiler/inference/proofs
Jan 17 00:44:13 Finished compiler/inference/proofs                             2m21s   1GB
Jan 17 00:44:13 Starting compiler/backend/semantics
Jan 17 01:12:10 Finished compiler/backend/semantics                           27m57s   2GB
Jan 17 01:12:11 Starting compiler/backend/reg_alloc/proofs
Jan 17 01:15:38 Finished compiler/backend/reg_alloc/proofs                     3m27s 805MB
Jan 17 01:15:38 Starting compiler/backend/proofs
Jan 17 02:04:01 Finished compiler/backend/proofs                              48m22s  17GB
Jan 17 02:04:02 Starting compiler/backend/serialiser
Jan 17 02:05:15 Finished compiler/backend/serialiser                           1m13s   1GB
Jan 17 02:05:15 Starting compiler/encoders/x64/proofs
Jan 17 02:14:47 Finished compiler/encoders/x64/proofs                          9m31s   4GB
Jan 17 02:14:47 Starting compiler/encoders/arm7/proofs
Jan 17 02:28:06 Finished compiler/encoders/arm7/proofs                        13m18s   3GB
Jan 17 02:28:06 Starting compiler/encoders/arm8/proofs
Jan 17 02:34:45 Finished compiler/encoders/arm8/proofs                         6m39s   1GB
Jan 17 02:34:45 Starting compiler/encoders/mips/proofs
Jan 17 02:44:34 Finished compiler/encoders/mips/proofs                         9m48s   2GB
Jan 17 02:44:34 Starting compiler/encoders/riscv/proofs
Jan 17 02:53:25 Finished compiler/encoders/riscv/proofs                        8m51s   1GB
Jan 17 02:53:25 Starting compiler/encoders/ag32/proofs
Jan 17 02:55:59 Finished compiler/encoders/ag32/proofs                         2m34s 731MB
Jan 17 02:55:59 Starting compiler/backend/x64/proofs
Jan 17 02:56:22 Finished compiler/backend/x64/proofs                             22s   1GB
Jan 17 02:56:22 Starting compiler/backend/arm7/proofs
Jan 17 02:56:46 Finished compiler/backend/arm7/proofs                            23s   1GB
Jan 17 02:56:47 Starting compiler/backend/arm8/proofs
Jan 17 02:57:10 Finished compiler/backend/arm8/proofs                            23s   1GB
Jan 17 02:57:10 Starting compiler/backend/mips/proofs
Jan 17 02:57:33 Finished compiler/backend/mips/proofs                            23s   1GB
Jan 17 02:57:34 Starting compiler/backend/riscv/proofs
Jan 17 02:57:57 Finished compiler/backend/riscv/proofs                           23s   1GB
Jan 17 02:57:57 Starting compiler/backend/ag32/proofs
Jan 17 03:10:41 Finished compiler/backend/ag32/proofs                         12m41s   2GB
Jan 17 03:10:42 Starting compiler/proofs
Jan 17 03:12:40 Finished compiler/proofs                                       1m58s   3GB
Jan 17 03:12:40 Starting candle/set-theory
Jan 17 03:13:09 Finished candle/set-theory                                       28s 723MB
Jan 17 03:13:09 Starting candle/syntax-lib
Jan 17 03:13:20 Finished candle/syntax-lib                                       10s 688MB
Jan 17 03:13:20 Starting candle/standard/syntax
Jan 17 03:15:06 Finished candle/standard/syntax                                1m46s 883MB
Jan 17 03:15:07 Starting candle/standard/semantics
Jan 17 03:16:49 Finished candle/standard/semantics                             1m41s   1GB
Jan 17 03:16:49 Starting candle/standard/monadic
Jan 17 03:18:23 Finished candle/standard/monadic                               1m33s   1GB
Jan 17 03:18:23 Starting candle/standard/ml_kernel
Jan 17 03:24:50 Finished candle/standard/ml_kernel                             6m27s   2GB
Jan 17 03:24:51 Starting candle/overloading/syntax
Jan 17 03:27:53 Finished candle/overloading/syntax                             3m02s   1GB
Jan 17 03:27:53 Starting candle/overloading/semantics
Jan 17 03:39:18 Finished candle/overloading/semantics                         11m25s   2GB
Jan 17 03:39:19 Starting candle/prover
Jan 17 03:46:12 Finished candle/prover                                         6m53s   2GB
Jan 17 03:46:12 Starting pancake
Jan 17 03:48:08 Finished pancake                                               1m55s   2GB
Jan 17 03:48:08 Starting pancake/ffi
Jan 17 03:48:08 Finished pancake/ffi                                              0s   6MB
Jan 17 03:48:08 Starting pancake/semantics
Jan 17 03:50:23 Finished pancake/semantics                                     2m14s 988MB
Jan 17 03:50:24 Starting pancake/proofs
Jan 17 04:02:00 Finished pancake/proofs                                       11m36s   6GB
Jan 17 04:02:00 Starting characteristic/examples
Jan 17 04:03:19 Finished characteristic/examples                               1m18s   2GB
Jan 17 04:03:19 Starting tutorial/solutions
Jan 17 04:19:08 Finished tutorial/solutions                                   15m47s   9GB
Jan 17 04:19:08 Starting translator/monadic/examples
Jan 17 04:22:16 Finished translator/monadic/examples                           3m08s   2GB
Jan 17 04:22:16 Starting examples
Jan 17 04:31:02 Finished examples                                              8m45s   3GB
Jan 17 04:31:02 Starting examples/compilation/x64
Jan 17 07:00:04 Finished examples/compilation/x64                           2h28m58s  17GB
Jan 17 07:00:04 Starting examples/compilation/x64/proofs
Jan 17 07:02:01 Finished examples/compilation/x64/proofs                       1m56s   3GB
Jan 17 07:02:01 Starting examples/compilation/ag32
Jan 17 07:35:37 Finished examples/compilation/ag32                            33m35s   9GB
Jan 17 07:35:37 Starting examples/compilation/ag32/proofs
Jan 17 07:36:24 Finished examples/compilation/ag32/proofs                        47s   2GB
Jan 17 07:36:24 Starting examples/cost
Jan 17 08:31:09 Finished examples/cost                                        54m43s   8GB
Jan 17 08:31:09 Starting examples/lpr_checker
Jan 17 08:31:57 Finished examples/lpr_checker                                    47s 971MB
Jan 17 08:31:57 Starting examples/lpr_checker/array
Jan 17 08:47:57 FAILED: examples/lpr_checker/array
Scanning [1m$(HOLDIR)/src/sort[0m
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/quotient/src[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/algorithms[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/src/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/basis[0m
Scanning [1m$(HOLDIR)/examples/bootstrap[0m
Scanning [1m$(CAKEMLDIR)/examples[0m
Scanning [1m$(CAKEMLDIR)/examples/lpr_checker[0m
Starting work on README.md
Starting work on lpr_composeProgTheory
Starting work on lpr_listTheory
README.md                                                                         (0s)     OK
lpr_listTheory                                                                   (66s)     OK
lpr_composeProgTheory                                                           (154s)     OK
Starting work on lpr_arrayProgTheory
lpr_arrayProgTheory                                                             (717s)     OK
Starting work on lpr_arrayFullProgTheory
Starting work on lpr_arrayRamseyProgTheory
lpr_arrayFullProgTheory                                                          (75s)FAIL<1>
              ... ... v4  ... ... v5)))
 
 failed.
 Failed to prove theorem run_proof_arr_spec.
 
 Exception raised at cfLetAutoLib.xlet_auto:
 Not a cf_let expression (THEN1 on line 132) (THEN1 on line 135) (THEN1 on line 130) (THEN1 on line 155) (THEN1 on line 168)
 error in quse /home/cug/hk324/cml-regression/cakeml-1718/examples/lpr_checker/array/lpr_arrayFullProgScript.sml : HOL_ERR {message = "Not a cf_let expression (THEN1 on line 132) (THEN1 on line 135) (THEN1 on line 130) (THEN1 on line 155) (THEN1 on line 168)", origin_function = "xlet_auto", origin_structure = "cfLetAutoLib"}
 error in load /home/cug/hk324/cml-regression/cakeml-1718/examples/lpr_checker/array/lpr_arrayFullProgScript : HOL_ERR {message = "Not a cf_let expression (THEN1 on line 132) (THEN1 on line 135) (THEN1 on line 130) (THEN1 on line 155) (THEN1 on line 168)", origin_function = "xlet_auto", origin_structure = "cfLetAutoLib"}
 Uncaught exception: HOL_ERR {message = "Not a cf_let expression (THEN1 on line 132) (THEN1 on line 135) (THEN1 on line 130) (THEN1 on line 155) (THEN1 on line 168)", origin_function = "xlet_auto", origin_structure = "cfLetAutoLib"}
lpr_arrayRamseyProgTheory                                                        (76s)MKILLED