Job 1719

CakeML:37e4c964919a222c307a9139e03035620e15eba1
  Reduce reimplementation of mlint in examples [Jan 17 00:19:33]
#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 17 08:47:58 Claimed job
Jan 17 08:48:01 Reusing HOL
Jan 17 08:48:13 Starting developers
Jan 17 08:48:17 Finished developers                                               4s 121MB
Jan 17 08:48:17 Starting developers/bin
Jan 17 08:48:22 Finished developers/bin                                           4s 674MB
Jan 17 08:48:22 Starting semantics/ffi
Jan 17 08:48:30 Finished semantics/ffi                                            8s 212MB
Jan 17 08:48:30 Starting semantics
Jan 17 08:49:54 Finished semantics                                             1m23s   1GB
Jan 17 08:49:54 Starting semantics/proofs
Jan 17 08:53:22 Finished semantics/proofs                                      3m28s   1GB
Jan 17 08:53:22 Starting semantics/alt_semantics
Jan 17 08:53:33 Finished semantics/alt_semantics                                 10s 375MB
Jan 17 08:53:33 Starting semantics/alt_semantics/proofs
Jan 17 08:55:59 Finished semantics/alt_semantics/proofs                        2m25s 912MB
Jan 17 08:55:59 Starting basis/pure
Jan 17 08:56:52 Finished basis/pure                                              52s 693MB
Jan 17 08:56:52 Starting translator
Jan 17 08:59:41 Finished translator                                            2m49s   1GB
Jan 17 08:59:42 Starting compiler/parsing
Jan 17 09:00:53 Finished compiler/parsing                                      1m11s   1GB
Jan 17 09:00:53 Starting characteristic
Jan 17 09:06:37 Finished characteristic                                        5m43s   1GB
Jan 17 09:06:37 Starting translator/monadic
Jan 17 09:08:20 Finished translator/monadic                                    1m42s   1GB
Jan 17 09:08:20 Starting basis
Jan 17 09:55:13 Finished basis                                                46m51s  14GB
Jan 17 09:55:13 Starting compiler/inference
Jan 17 09:56:19 Finished compiler/inference                                    1m06s   1GB
Jan 17 09:56:19 Starting compiler/backend/reg_alloc
Jan 17 09:57:24 Finished compiler/backend/reg_alloc                            1m04s   1GB
Jan 17 09:57:24 Starting compiler/backend/gc
Jan 17 10:00:38 Finished compiler/backend/gc                                   3m14s   1GB
Jan 17 10:00:38 Starting compiler/backend
Jan 17 10:05:11 Finished compiler/backend                                      4m32s   2GB
Jan 17 10:05:11 Starting compiler/encoders/asm
Jan 17 10:05:34 Finished compiler/encoders/asm                                   23s 549MB
Jan 17 10:05:34 Starting compiler/encoders/x64
Jan 17 10:05:59 Finished compiler/encoders/x64                                   24s 979MB
Jan 17 10:05:59 Starting compiler/encoders/arm7
Jan 17 10:06:50 Finished compiler/encoders/arm7                                  50s 662MB
Jan 17 10:06:51 Starting compiler/encoders/arm8
Jan 17 10:07:05 Finished compiler/encoders/arm8                                  14s 664MB
Jan 17 10:07:05 Starting compiler/encoders/mips
Jan 17 10:07:22 Finished compiler/encoders/mips                                  16s   1GB
Jan 17 10:07:22 Starting compiler/encoders/riscv
Jan 17 10:07:37 Finished compiler/encoders/riscv                                 15s 729MB
Jan 17 10:07:37 Starting compiler/encoders/ag32
Jan 17 10:07:55 Finished compiler/encoders/ag32                                  17s 631MB
Jan 17 10:07:55 Starting compiler/backend/x64
Jan 17 10:08:14 Finished compiler/backend/x64                                    18s   1GB
Jan 17 10:08:14 Starting compiler/backend/arm7
Jan 17 10:08:35 Finished compiler/backend/arm7                                   21s   1GB
Jan 17 10:08:35 Starting compiler/backend/arm8
Jan 17 10:08:54 Finished compiler/backend/arm8                                   18s   1GB
Jan 17 10:08:54 Starting compiler/backend/mips
Jan 17 10:09:15 Finished compiler/backend/mips                                   20s   1GB
Jan 17 10:09:15 Starting compiler/backend/riscv
Jan 17 10:09:35 Finished compiler/backend/riscv                                  19s   1GB
Jan 17 10:09:35 Starting compiler/backend/ag32
Jan 17 10:10:43 Finished compiler/backend/ag32                                 1m08s   1GB
Jan 17 10:10:43 Starting compiler/parsing/proofs
Jan 17 10:14:23 Finished compiler/parsing/proofs                               3m39s   1GB
Jan 17 10:14:23 Starting compiler/inference/proofs
Jan 17 10:16:46 Finished compiler/inference/proofs                             2m22s   1GB
Jan 17 10:16:46 Starting compiler/backend/semantics
Jan 17 10:45:21 Finished compiler/backend/semantics                           28m34s   2GB
Jan 17 10:45:21 Starting compiler/backend/reg_alloc/proofs
Jan 17 10:48:50 Finished compiler/backend/reg_alloc/proofs                     3m28s 753MB
Jan 17 10:48:50 Starting compiler/backend/proofs
Jan 17 11:39:21 Finished compiler/backend/proofs                              50m28s  11GB
Jan 17 11:39:22 Starting compiler/backend/serialiser
Jan 17 11:40:33 Finished compiler/backend/serialiser                           1m11s   1GB
Jan 17 11:40:33 Starting compiler/encoders/x64/proofs
Jan 17 11:50:04 Finished compiler/encoders/x64/proofs                          9m30s   4GB
Jan 17 11:50:05 Starting compiler/encoders/arm7/proofs
Jan 17 12:03:20 Finished compiler/encoders/arm7/proofs                        13m15s   3GB
Jan 17 12:03:20 Starting compiler/encoders/arm8/proofs
Jan 17 12:10:07 Finished compiler/encoders/arm8/proofs                         6m46s   1GB
Jan 17 12:10:07 Starting compiler/encoders/mips/proofs
Jan 17 12:19:56 Finished compiler/encoders/mips/proofs                         9m49s   3GB
Jan 17 12:19:57 Starting compiler/encoders/riscv/proofs
Jan 17 12:28:50 Finished compiler/encoders/riscv/proofs                        8m53s   1GB
Jan 17 12:28:50 Starting compiler/encoders/ag32/proofs
Jan 17 12:31:22 Finished compiler/encoders/ag32/proofs                         2m32s 696MB
Jan 17 12:31:22 Starting compiler/backend/x64/proofs
Jan 17 12:31:45 Finished compiler/backend/x64/proofs                             22s   1GB
Jan 17 12:31:45 Starting compiler/backend/arm7/proofs
Jan 17 12:32:09 Finished compiler/backend/arm7/proofs                            23s   1GB
Jan 17 12:32:09 Starting compiler/backend/arm8/proofs
Jan 17 12:32:33 Finished compiler/backend/arm8/proofs                            24s   1GB
Jan 17 12:32:34 Starting compiler/backend/mips/proofs
Jan 17 12:32:56 Finished compiler/backend/mips/proofs                            22s   1GB
Jan 17 12:32:57 Starting compiler/backend/riscv/proofs
Jan 17 12:33:19 Finished compiler/backend/riscv/proofs                           22s   1GB
Jan 17 12:33:19 Starting compiler/backend/ag32/proofs
Jan 17 12:45:46 Finished compiler/backend/ag32/proofs                         12m25s   2GB
Jan 17 12:45:46 Starting compiler/proofs
Jan 17 12:47:29 Finished compiler/proofs                                       1m42s   3GB
Jan 17 12:47:29 Starting candle/set-theory
Jan 17 12:47:57 Finished candle/set-theory                                       28s 761MB
Jan 17 12:47:57 Starting candle/syntax-lib
Jan 17 12:48:09 Finished candle/syntax-lib                                       11s 498MB
Jan 17 12:48:09 Starting candle/standard/syntax
Jan 17 12:49:55 Finished candle/standard/syntax                                1m46s 958MB
Jan 17 12:49:55 Starting candle/standard/semantics
Jan 17 12:51:38 Finished candle/standard/semantics                             1m42s   1GB
Jan 17 12:51:38 Starting candle/standard/monadic
Jan 17 12:53:13 Finished candle/standard/monadic                               1m34s   1GB
Jan 17 12:53:13 Starting candle/standard/ml_kernel
Jan 17 12:59:52 Finished candle/standard/ml_kernel                             6m39s   4GB
Jan 17 12:59:53 Starting candle/overloading/syntax
Jan 17 13:02:53 Finished candle/overloading/syntax                             3m00s   1GB
Jan 17 13:02:53 Starting candle/overloading/semantics
Jan 17 13:14:35 Finished candle/overloading/semantics                         11m41s   2GB
Jan 17 13:14:35 Starting candle/prover
Jan 17 13:22:01 Finished candle/prover                                         7m26s   3GB
Jan 17 13:22:01 Starting pancake
Jan 17 13:23:58 Finished pancake                                               1m56s   2GB
Jan 17 13:23:58 Starting pancake/ffi
Jan 17 13:23:58 Finished pancake/ffi                                              0s   7MB
Jan 17 13:23:58 Starting pancake/semantics
Jan 17 13:26:14 Finished pancake/semantics                                     2m16s   1GB
Jan 17 13:26:14 Starting pancake/proofs
Jan 17 13:38:01 Finished pancake/proofs                                       11m46s   7GB
Jan 17 13:38:01 Starting characteristic/examples
Jan 17 13:39:25 Finished characteristic/examples                               1m23s   3GB
Jan 17 13:39:25 Starting tutorial/solutions
Jan 17 13:55:35 Finished tutorial/solutions                                   16m08s  10GB
Jan 17 13:55:35 Starting translator/monadic/examples
Jan 17 13:58:49 Finished translator/monadic/examples                           3m14s   2GB
Jan 17 13:58:49 Starting examples
Jan 17 14:08:08 Finished examples                                              9m18s   5GB
Jan 17 14:08:08 Starting examples/compilation/x64
Jan 17 16:38:06 Finished examples/compilation/x64                           2h29m55s  19GB
Jan 17 16:38:06 Starting examples/compilation/x64/proofs
Jan 17 16:40:10 Finished examples/compilation/x64/proofs                       2m03s   3GB
Jan 17 16:40:10 Starting examples/compilation/ag32
Jan 17 17:15:16 Finished examples/compilation/ag32                            35m05s   8GB
Jan 17 17:15:16 Starting examples/compilation/ag32/proofs
Jan 17 17:16:04 Finished examples/compilation/ag32/proofs                        47s   2GB
Jan 17 17:16:04 Starting examples/cost
Jan 17 18:10:49 Finished examples/cost                                        54m43s   7GB
Jan 17 18:10:50 Starting examples/lpr_checker
Jan 17 18:11:39 Finished examples/lpr_checker                                    49s 747MB
Jan 17 18:11:39 Starting examples/lpr_checker/array
Jan 17 18:26:24 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                                                                   (73s)     OK
lpr_composeProgTheory                                                           (162s)     OK
Starting work on lpr_arrayProgTheory
lpr_arrayProgTheory                                                             (711s)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-1719/examples/lpr_checker/array/lpr_arrayProgScript.sml : Fail "Static Errors"
 error in load /home/cug/hk324/cml-regression/cakeml-1719/examples/lpr_checker/array/lpr_arrayProgScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"