Job 1721

CakeML:c2b9d4e069d153a2a7af5c38beec8e8f33fa7587
  Better fix to previous [Jan 18 00:04:41]
#856 (printing)
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 18 01:46:40 Claimed job
Jan 18 01:46:43 Reusing HOL
Jan 18 01:46:56 Starting developers
Jan 18 01:47:00 Finished developers                                               4s 151MB
Jan 18 01:47:00 Starting developers/bin
Jan 18 01:47:04 Finished developers/bin                                           4s 675MB
Jan 18 01:47:04 Starting semantics/ffi
Jan 18 01:47:13 Finished semantics/ffi                                            8s 232MB
Jan 18 01:47:13 Starting semantics
Jan 18 01:48:35 Finished semantics                                             1m21s   1GB
Jan 18 01:48:35 Starting semantics/proofs
Jan 18 01:52:06 Finished semantics/proofs                                      3m30s   1GB
Jan 18 01:52:06 Starting semantics/alt_semantics
Jan 18 01:52:17 Finished semantics/alt_semantics                                 10s 353MB
Jan 18 01:52:17 Starting semantics/alt_semantics/proofs
Jan 18 01:54:40 Finished semantics/alt_semantics/proofs                        2m23s   1GB
Jan 18 01:54:40 Starting basis/pure
Jan 18 01:55:33 Finished basis/pure                                              53s 699MB
Jan 18 01:55:33 Starting translator
Jan 18 01:58:20 Finished translator                                            2m46s   2GB
Jan 18 01:58:20 Starting compiler/parsing
Jan 18 01:59:32 Finished compiler/parsing                                      1m11s   1GB
Jan 18 01:59:32 Starting characteristic
Jan 18 02:05:10 Finished characteristic                                        5m38s   2GB
Jan 18 02:05:11 Starting translator/monadic
Jan 18 02:06:53 Finished translator/monadic                                    1m42s   1GB
Jan 18 02:06:54 Starting basis
Jan 18 02:53:13 Finished basis                                                46m17s  17GB
Jan 18 02:53:13 Starting compiler/inference
Jan 18 02:54:19 Finished compiler/inference                                    1m06s   1GB
Jan 18 02:54:20 Starting compiler/backend/reg_alloc
Jan 18 02:55:25 Finished compiler/backend/reg_alloc                            1m05s   1GB
Jan 18 02:55:25 Starting compiler/backend/gc
Jan 18 02:58:38 Finished compiler/backend/gc                                   3m12s   2GB
Jan 18 02:58:38 Starting compiler/backend
Jan 18 03:03:07 Finished compiler/backend                                      4m28s   3GB
Jan 18 03:03:07 Starting compiler/encoders/asm
Jan 18 03:03:30 Finished compiler/encoders/asm                                   22s 570MB
Jan 18 03:03:30 Starting compiler/encoders/x64
Jan 18 03:03:55 Finished compiler/encoders/x64                                   24s 979MB
Jan 18 03:03:55 Starting compiler/encoders/arm7
Jan 18 03:04:45 Finished compiler/encoders/arm7                                  49s   1GB
Jan 18 03:04:45 Starting compiler/encoders/arm8
Jan 18 03:04:59 Finished compiler/encoders/arm8                                  14s 662MB
Jan 18 03:05:00 Starting compiler/encoders/mips
Jan 18 03:05:17 Finished compiler/encoders/mips                                  16s   1GB
Jan 18 03:05:17 Starting compiler/encoders/riscv
Jan 18 03:05:32 Finished compiler/encoders/riscv                                 15s   1GB
Jan 18 03:05:32 Starting compiler/encoders/ag32
Jan 18 03:05:50 Finished compiler/encoders/ag32                                  17s 788MB
Jan 18 03:05:50 Starting compiler/backend/x64
Jan 18 03:06:10 Finished compiler/backend/x64                                    19s   1GB
Jan 18 03:06:10 Starting compiler/backend/arm7
Jan 18 03:06:29 Finished compiler/backend/arm7                                   18s   1GB
Jan 18 03:06:29 Starting compiler/backend/arm8
Jan 18 03:06:48 Finished compiler/backend/arm8                                   19s   1GB
Jan 18 03:06:49 Starting compiler/backend/mips
Jan 18 03:07:08 Finished compiler/backend/mips                                   19s   1GB
Jan 18 03:07:08 Starting compiler/backend/riscv
Jan 18 03:07:28 Finished compiler/backend/riscv                                  19s   1GB
Jan 18 03:07:28 Starting compiler/backend/ag32
Jan 18 03:08:37 Finished compiler/backend/ag32                                 1m08s   1GB
Jan 18 03:08:37 Starting compiler/parsing/proofs
Jan 18 03:12:20 Finished compiler/parsing/proofs                               3m42s   1GB
Jan 18 03:12:20 Starting compiler/inference/proofs
Jan 18 03:14:44 Finished compiler/inference/proofs                             2m24s   1GB
Jan 18 03:14:44 Starting compiler/backend/semantics
Jan 18 03:43:37 Finished compiler/backend/semantics                           28m52s   1GB
Jan 18 03:43:37 Starting compiler/backend/reg_alloc/proofs
Jan 18 03:47:01 Finished compiler/backend/reg_alloc/proofs                     3m23s 839MB
Jan 18 03:47:01 Starting compiler/backend/proofs
Jan 18 04:38:09 Finished compiler/backend/proofs                              51m03s  22GB
Jan 18 04:38:09 Starting compiler/backend/serialiser
Jan 18 04:39:21 Finished compiler/backend/serialiser                           1m11s   1GB
Jan 18 04:39:21 Starting compiler/encoders/x64/proofs
Jan 18 04:48:58 Finished compiler/encoders/x64/proofs                          9m37s   4GB
Jan 18 04:48:58 Starting compiler/encoders/arm7/proofs
Jan 18 05:02:17 Finished compiler/encoders/arm7/proofs                        13m19s   3GB
Jan 18 05:02:18 Starting compiler/encoders/arm8/proofs
Jan 18 05:08:59 Finished compiler/encoders/arm8/proofs                         6m40s   1GB
Jan 18 05:08:59 Starting compiler/encoders/mips/proofs
Jan 18 05:18:45 Finished compiler/encoders/mips/proofs                         9m45s   2GB
Jan 18 05:18:45 Starting compiler/encoders/riscv/proofs
Jan 18 05:27:36 Finished compiler/encoders/riscv/proofs                        8m51s   1GB
Jan 18 05:27:36 Starting compiler/encoders/ag32/proofs
Jan 18 05:30:10 Finished compiler/encoders/ag32/proofs                         2m33s 713MB
Jan 18 05:30:10 Starting compiler/backend/x64/proofs
Jan 18 05:30:33 Finished compiler/backend/x64/proofs                             22s   1GB
Jan 18 05:30:33 Starting compiler/backend/arm7/proofs
Jan 18 05:30:57 Finished compiler/backend/arm7/proofs                            23s   1GB
Jan 18 05:30:58 Starting compiler/backend/arm8/proofs
Jan 18 05:31:19 Finished compiler/backend/arm8/proofs                            21s   1GB
Jan 18 05:31:20 Starting compiler/backend/mips/proofs
Jan 18 05:31:43 Finished compiler/backend/mips/proofs                            23s   1GB
Jan 18 05:31:44 Starting compiler/backend/riscv/proofs
Jan 18 05:32:07 Finished compiler/backend/riscv/proofs                           23s   1GB
Jan 18 05:32:07 Starting compiler/backend/ag32/proofs
Jan 18 05:44:47 Finished compiler/backend/ag32/proofs                         12m36s   2GB
Jan 18 05:44:47 Starting compiler/proofs
Jan 18 05:46:29 Finished compiler/proofs                                       1m42s   3GB
Jan 18 05:46:29 Starting candle/set-theory
Jan 18 05:46:58 Finished candle/set-theory                                       28s 834MB
Jan 18 05:46:58 Starting candle/syntax-lib
Jan 18 05:47:09 Finished candle/syntax-lib                                       10s 681MB
Jan 18 05:47:09 Starting candle/standard/syntax
Jan 18 05:48:56 Finished candle/standard/syntax                                1m47s   1GB
Jan 18 05:48:56 Starting candle/standard/semantics
Jan 18 05:50:38 Finished candle/standard/semantics                             1m41s   1GB
Jan 18 05:50:38 Starting candle/standard/monadic
Jan 18 05:52:10 Finished candle/standard/monadic                               1m32s   1GB
Jan 18 05:52:10 Starting candle/standard/ml_kernel
Jan 18 05:58:57 Finished candle/standard/ml_kernel                             6m47s   3GB
Jan 18 05:58:58 Starting candle/overloading/syntax
Jan 18 06:01:55 Finished candle/overloading/syntax                             2m57s   1GB
Jan 18 06:01:55 Starting candle/overloading/semantics
Jan 18 06:13:19 Finished candle/overloading/semantics                         11m23s   3GB
Jan 18 06:13:19 Starting candle/prover
Jan 18 06:20:47 Finished candle/prover                                         7m28s   3GB
Jan 18 06:20:47 Starting pancake
Jan 18 06:22:43 Finished pancake                                               1m55s   2GB
Jan 18 06:22:43 Starting pancake/ffi
Jan 18 06:22:43 Finished pancake/ffi                                              0s   6MB
Jan 18 06:22:43 Starting pancake/semantics
Jan 18 06:24:58 Finished pancake/semantics                                     2m14s   1GB
Jan 18 06:24:58 Starting pancake/proofs
Jan 18 06:36:38 Finished pancake/proofs                                       11m40s   5GB
Jan 18 06:36:38 Starting characteristic/examples
Jan 18 06:38:03 Finished characteristic/examples                               1m24s   2GB
Jan 18 06:38:03 Starting tutorial/solutions
Jan 18 06:53:55 Finished tutorial/solutions                                   15m51s  11GB
Jan 18 06:53:55 Starting translator/monadic/examples
Jan 18 06:57:07 Finished translator/monadic/examples                           3m11s   2GB
Jan 18 06:57:07 Starting examples
Jan 18 07:06:19 Finished examples                                              9m11s   6GB
Jan 18 07:06:19 Starting examples/compilation/x64
Jan 18 09:36:02 Finished examples/compilation/x64                           2h29m42s  20GB
Jan 18 09:36:03 Starting examples/compilation/x64/proofs
Jan 18 09:37:49 Finished examples/compilation/x64/proofs                       1m46s   3GB
Jan 18 09:37:49 Starting examples/compilation/ag32
Jan 18 10:13:17 Finished examples/compilation/ag32                            35m28s   9GB
Jan 18 10:13:17 Starting examples/compilation/ag32/proofs
Jan 18 10:14:07 Finished examples/compilation/ag32/proofs                        49s   4GB
Jan 18 10:14:07 Starting examples/cost
Jan 18 11:09:05 Finished examples/cost                                        54m55s   7GB
Jan 18 11:09:05 Starting examples/lpr_checker
Jan 18 11:09:53 Finished examples/lpr_checker                                    47s 992MB
Jan 18 11:09:53 Starting examples/lpr_checker/array
Jan 18 11:24:51 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)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[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                                                                   (70s)     OK
lpr_composeProgTheory                                                           (162s)     OK
Starting work on lpr_arrayProgTheory
lpr_arrayProgTheory                                                             (723s)FAIL<1>
   (
      [
         QUOTE
         " (*#loc 2884 4*)\226\136\128x y z. simple_tochars_side x y z = T"
         ],
      ... \\ ... \\ ... ...
      ) |> update_precondition
 error in quse /home/cug/hk324/cml-regression/cakeml-1721/examples/lpr_checker/array/lpr_arrayProgScript.sml : Fail "Static Errors"
 error in load /home/cug/hk324/cml-regression/cakeml-1721/examples/lpr_checker/array/lpr_arrayProgScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"