Job 1595

CakeML:82e40ae78a115fa5a1954355cd4852d325a44c4f
  make monadic trans skip over bad EvalM theorems [Sep 30 00:28:34]
#839 (lpr_transform)
Merging into:93a43c51f337a845a8696f031d3fc712c62dd2da
  Merge pull request #835 from CakeML/enc-dec [Sep 29 09:23:45]
HOL:424885cd3abe129d536c979db549b5efe69b23fa
  Fix Unicode violation in topologyScript.sml [Sep 20 06:39:34]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Sep 30 06:21:01 Claimed job
Sep 30 06:21:08 Reusing HOL
Sep 30 06:21:49 Starting developers
Sep 30 06:21:53 Finished developers                                               4s 145MB
Sep 30 06:21:54 Starting developers/bin
Sep 30 06:22:00 Finished developers/bin                                           6s   1GB
Sep 30 06:22:00 Starting semantics/ffi
Sep 30 06:22:12 Finished semantics/ffi                                           11s 262MB
Sep 30 06:22:12 Starting semantics
Sep 30 06:23:35 Finished semantics                                             1m22s   1GB
Sep 30 06:23:35 Starting semantics/proofs
Sep 30 06:27:12 Finished semantics/proofs                                      3m36s   1GB
Sep 30 06:27:12 Starting semantics/alt_semantics
Sep 30 06:27:24 Finished semantics/alt_semantics                                 11s 366MB
Sep 30 06:27:24 Starting semantics/alt_semantics/proofs
Sep 30 06:29:50 Finished semantics/alt_semantics/proofs                        2m26s 797MB
Sep 30 06:29:51 Starting basis/pure
Sep 30 06:30:43 Finished basis/pure                                              52s 879MB
Sep 30 06:30:43 Starting translator
Sep 30 06:33:59 Finished translator                                            3m15s   1GB
Sep 30 06:33:59 Starting compiler/parsing
Sep 30 06:35:11 Finished compiler/parsing                                      1m11s   2GB
Sep 30 06:35:11 Starting characteristic
Sep 30 06:40:49 Finished characteristic                                        5m38s   2GB
Sep 30 06:40:49 Starting translator/monadic
Sep 30 06:42:30 Finished translator/monadic                                    1m40s   1GB
Sep 30 06:42:30 Starting basis
Sep 30 07:27:15 Finished basis                                                44m43s  25GB
Sep 30 07:27:15 Starting compiler/inference
Sep 30 07:28:23 Finished compiler/inference                                    1m07s   1GB
Sep 30 07:28:23 Starting compiler/backend/reg_alloc
Sep 30 07:29:32 Finished compiler/backend/reg_alloc                            1m08s   1GB
Sep 30 07:29:32 Starting compiler/backend/gc
Sep 30 07:32:53 Finished compiler/backend/gc                                   3m20s   2GB
Sep 30 07:32:53 Starting compiler/backend
Sep 30 07:37:55 Finished compiler/backend                                      5m01s   3GB
Sep 30 07:37:55 Starting compiler/encoders/asm
Sep 30 07:38:19 Finished compiler/encoders/asm                                   23s 691MB
Sep 30 07:38:19 Starting compiler/encoders/x64
Sep 30 07:38:45 Finished compiler/encoders/x64                                   25s   1GB
Sep 30 07:38:45 Starting compiler/encoders/arm7
Sep 30 07:39:37 Finished compiler/encoders/arm7                                  51s 798MB
Sep 30 07:39:37 Starting compiler/encoders/arm8
Sep 30 07:39:50 Finished compiler/encoders/arm8                                  13s 977MB
Sep 30 07:39:50 Starting compiler/encoders/mips
Sep 30 07:40:09 Finished compiler/encoders/mips                                  18s   1GB
Sep 30 07:40:09 Starting compiler/encoders/riscv
Sep 30 07:40:26 Finished compiler/encoders/riscv                                 16s 851MB
Sep 30 07:40:26 Starting compiler/encoders/ag32
Sep 30 07:40:44 Finished compiler/encoders/ag32                                  18s 669MB
Sep 30 07:40:44 Starting compiler/backend/x64
Sep 30 07:41:03 Finished compiler/backend/x64                                    18s   1GB
Sep 30 07:41:03 Starting compiler/backend/arm7
Sep 30 07:41:24 Finished compiler/backend/arm7                                   20s   1GB
Sep 30 07:41:24 Starting compiler/backend/arm8
Sep 30 07:41:44 Finished compiler/backend/arm8                                   20s   1GB
Sep 30 07:41:44 Starting compiler/backend/mips
Sep 30 07:42:05 Finished compiler/backend/mips                                   19s   1GB
Sep 30 07:42:05 Starting compiler/backend/riscv
Sep 30 07:42:25 Finished compiler/backend/riscv                                  20s   1GB
Sep 30 07:42:25 Starting compiler/backend/ag32
Sep 30 07:43:35 Finished compiler/backend/ag32                                 1m09s   1GB
Sep 30 07:43:35 Starting compiler/parsing/proofs
Sep 30 07:50:27 Finished compiler/parsing/proofs                               6m52s   1GB
Sep 30 07:50:28 Starting compiler/inference/proofs
Sep 30 07:52:56 Finished compiler/inference/proofs                             2m28s   1GB
Sep 30 07:52:56 Starting compiler/backend/semantics
Sep 30 08:21:32 Finished compiler/backend/semantics                           28m35s   3GB
Sep 30 08:21:32 Starting compiler/backend/reg_alloc/proofs
Sep 30 08:24:57 Finished compiler/backend/reg_alloc/proofs                     3m24s   1GB
Sep 30 08:24:57 Starting compiler/backend/proofs
Sep 30 09:15:54 Finished compiler/backend/proofs                              50m56s  17GB
Sep 30 09:15:54 Starting compiler/backend/serialiser
Sep 30 09:17:03 Finished compiler/backend/serialiser                           1m08s   1GB
Sep 30 09:17:04 Starting compiler/encoders/x64/proofs
Sep 30 09:26:34 Finished compiler/encoders/x64/proofs                          9m30s   4GB
Sep 30 09:26:34 Starting compiler/encoders/arm7/proofs
Sep 30 09:39:39 Finished compiler/encoders/arm7/proofs                        13m04s   7GB
Sep 30 09:39:39 Starting compiler/encoders/arm8/proofs
Sep 30 09:46:27 Finished compiler/encoders/arm8/proofs                         6m48s   1GB
Sep 30 09:46:27 Starting compiler/encoders/mips/proofs
Sep 30 09:56:23 Finished compiler/encoders/mips/proofs                         9m55s   2GB
Sep 30 09:56:23 Starting compiler/encoders/riscv/proofs
Sep 30 10:05:21 Finished compiler/encoders/riscv/proofs                        8m58s   1GB
Sep 30 10:05:21 Starting compiler/encoders/ag32/proofs
Sep 30 10:07:56 Finished compiler/encoders/ag32/proofs                         2m34s   1GB
Sep 30 10:07:56 Starting compiler/backend/x64/proofs
Sep 30 10:08:18 Finished compiler/backend/x64/proofs                             21s   1GB
Sep 30 10:08:18 Starting compiler/backend/arm7/proofs
Sep 30 10:08:42 Finished compiler/backend/arm7/proofs                            23s   1GB
Sep 30 10:08:42 Starting compiler/backend/arm8/proofs
Sep 30 10:09:05 Finished compiler/backend/arm8/proofs                            23s   1GB
Sep 30 10:09:05 Starting compiler/backend/mips/proofs
Sep 30 10:09:28 Finished compiler/backend/mips/proofs                            22s   1GB
Sep 30 10:09:28 Starting compiler/backend/riscv/proofs
Sep 30 10:09:51 Finished compiler/backend/riscv/proofs                           22s   1GB
Sep 30 10:09:51 Starting compiler/backend/ag32/proofs
Sep 30 10:22:48 Finished compiler/backend/ag32/proofs                         12m56s   2GB
Sep 30 10:22:48 Starting compiler/proofs
Sep 30 10:24:34 Finished compiler/proofs                                       1m45s   3GB
Sep 30 10:24:34 Starting candle/set-theory
Sep 30 10:25:04 Finished candle/set-theory                                       29s 771MB
Sep 30 10:25:04 Starting candle/syntax-lib
Sep 30 10:25:16 Finished candle/syntax-lib                                       11s 505MB
Sep 30 10:25:16 Starting candle/standard/syntax
Sep 30 10:27:09 Finished candle/standard/syntax                                1m52s   1GB
Sep 30 10:27:09 Starting candle/standard/semantics
Sep 30 10:28:54 Finished candle/standard/semantics                             1m44s   1GB
Sep 30 10:28:54 Starting candle/standard/monadic
Sep 30 10:30:36 Finished candle/standard/monadic                               1m42s   1GB
Sep 30 10:30:36 Starting candle/standard/ml_kernel
Sep 30 10:36:05 Finished candle/standard/ml_kernel                             5m28s   4GB
Sep 30 10:36:05 Starting candle/overloading/syntax
Sep 30 10:39:12 Finished candle/overloading/syntax                             3m06s   1GB
Sep 30 10:39:12 Starting candle/overloading/semantics
Sep 30 10:51:11 Finished candle/overloading/semantics                         11m59s   5GB
Sep 30 10:51:11 Starting pancake
Sep 30 10:53:05 Finished pancake                                               1m54s   2GB
Sep 30 10:53:06 Starting pancake/ffi
Sep 30 10:53:06 Finished pancake/ffi                                              0s   8MB
Sep 30 10:53:06 Starting pancake/semantics
Sep 30 10:55:23 Finished pancake/semantics                                     2m17s   1GB
Sep 30 10:55:23 Starting pancake/proofs
Sep 30 11:07:57 Finished pancake/proofs                                       12m33s   5GB
Sep 30 11:07:57 Starting characteristic/examples
Sep 30 11:09:31 Finished characteristic/examples                               1m33s   3GB
Sep 30 11:09:31 Starting tutorial/solutions
Sep 30 11:25:48 Finished tutorial/solutions                                   16m16s   9GB
Sep 30 11:25:48 Starting translator/monadic/examples
Sep 30 11:29:04 Finished translator/monadic/examples                           3m16s   3GB
Sep 30 11:29:04 Starting examples
Sep 30 11:37:58 Finished examples                                              8m53s   3GB
Sep 30 11:37:58 Starting examples/compilation/x64
Sep 30 14:08:49 Finished examples/compilation/x64                           2h30m49s  16GB
Sep 30 14:08:49 Starting examples/compilation/x64/proofs
Sep 30 14:10:40 Finished examples/compilation/x64/proofs                       1m51s   3GB
Sep 30 14:10:40 Starting examples/compilation/ag32
Sep 30 14:45:20 Finished examples/compilation/ag32                            34m39s   8GB
Sep 30 14:45:20 Starting examples/compilation/ag32/proofs
Sep 30 14:46:08 Finished examples/compilation/ag32/proofs                        47s   3GB
Sep 30 14:46:08 Starting examples/cost
Sep 30 15:40:26 Finished examples/cost                                        54m15s   7GB
Sep 30 15:40:26 Starting examples/lpr_checker
Sep 30 15:41:03 FAILED: examples/lpr_checker
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/src/bag[0m
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/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[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/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/lem_lib_stub[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
Starting work on README.md
Starting work on satSemTheory
README.md                                                                                                                                                                       (0s)     OK
satSemTheory                                                                                                                                                                   (10s)     OK
Starting work on lprTheory
lprTheory                                                                                                                                                                      (14s)     OK
Starting work on lpr_parsingTheory
Starting work on ramseyTheory
ramseyTheory                                                                                                                                                                    (8s)FAIL<1>
 Saved theorem _____ "ALOOKUP_transpose"
 /home/cug/hk324/cml-regression/cakeml-1595/examples/lpr_checker/ramseyScript.sml:387: error: Value or constructor (clique_edges_nonzero) has not been declared
 Found near
   Q.store_thm
   (
      "ramsey_lpr_wf",
      [QUOTE " (*#loc 381 23*)\n  EVERY wf_clause (ramsey_lpr k n)"],
      ... >> ... >> ... ...
      )
 Uncaught exception: Fail "Static Errors"
lpr_parsingTheory                                                                                                                                                               (9s)MKILLED