Job 1981

CakeML:f2df689d09c81d4d1e2bb92ea7ece382501321ba
  Tidy up word_cse test and add to build-sequence [Sep 13 21:06:06]
#908 (common-sub-exp-elim)
Merging into:d3c647d33b4e11f592a6f21f6ac90e4bef15977d
  Fix some broken proofs [Sep 14 07:41:37]
HOL:6d032bf33d3633d210f8817c9e769ae66be444aa
  Fix sttVariants given ancestry change in stt example [Sep 09 06:53:04]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Sep 14 16:46:51 Claimed job
Sep 14 16:46:53 Reusing HOL
Sep 14 16:47:06 Starting developers
Sep 14 16:47:11 Finished developers                                               4s 106MB
Sep 14 16:47:11 Starting developers/bin
Sep 14 16:47:17 Finished developers/bin                                           6s   1GB
Sep 14 16:47:17 Starting semantics/ffi
Sep 14 16:47:25 Finished semantics/ffi                                            8s 223MB
Sep 14 16:47:26 Starting semantics
Sep 14 16:49:48 Finished semantics                                             2m22s   1GB
Sep 14 16:49:48 Starting semantics/proofs
Sep 14 16:58:08 Finished semantics/proofs                                      8m19s   1GB
Sep 14 16:58:08 Starting semantics/alt_semantics
Sep 14 16:58:34 Finished semantics/alt_semantics                                 25s 558MB
Sep 14 16:58:34 Starting semantics/alt_semantics/proofs
Sep 14 17:13:53 Finished semantics/alt_semantics/proofs                       15m19s   1GB
Sep 14 17:13:54 Starting basis/pure
Sep 14 17:14:57 Finished basis/pure                                            1m03s 917MB
Sep 14 17:14:57 Starting translator
Sep 14 17:22:16 Finished translator                                            7m19s   2GB
Sep 14 17:22:16 Starting compiler/parsing
Sep 14 17:23:43 Finished compiler/parsing                                      1m26s   4GB
Sep 14 17:23:43 Starting characteristic
Sep 14 17:30:43 Finished characteristic                                        6m59s   2GB
Sep 14 17:30:43 Starting translator/monadic
Sep 14 17:32:40 Finished translator/monadic                                    1m56s   1GB
Sep 14 17:32:40 Starting basis
Sep 14 18:24:07 Finished basis                                                51m25s  20GB
Sep 14 18:24:07 Starting compiler/inference
Sep 14 18:25:37 Finished compiler/inference                                    1m30s   1GB
Sep 14 18:25:37 Starting compiler/backend/reg_alloc
Sep 14 18:27:21 Finished compiler/backend/reg_alloc                            1m44s   1GB
Sep 14 18:27:21 Starting compiler/backend/gc
Sep 14 18:31:40 Finished compiler/backend/gc                                   4m18s   2GB
Sep 14 18:31:40 Starting compiler/backend
Sep 14 18:37:15 Finished compiler/backend                                      5m35s   2GB
Sep 14 18:37:15 Starting compiler/encoders/asm
Sep 14 18:37:45 Finished compiler/encoders/asm                                   29s 915MB
Sep 14 18:37:45 Starting compiler/encoders/x64
Sep 14 18:38:14 Finished compiler/encoders/x64                                   28s 920MB
Sep 14 18:38:14 Starting compiler/encoders/arm7
Sep 14 18:39:07 Finished compiler/encoders/arm7                                  53s 852MB
Sep 14 18:39:07 Starting compiler/encoders/arm8
Sep 14 18:39:24 Finished compiler/encoders/arm8                                  16s 945MB
Sep 14 18:39:24 Starting compiler/encoders/arm8_asl
Sep 14 18:41:57 Finished compiler/encoders/arm8_asl                            2m32s   1GB
Sep 14 18:41:57 Starting compiler/encoders/mips
Sep 14 18:43:28 Finished compiler/encoders/mips                                1m30s   1GB
Sep 14 18:43:28 Starting compiler/encoders/riscv
Sep 14 18:45:15 Finished compiler/encoders/riscv                               1m46s   1GB
Sep 14 18:45:15 Starting compiler/encoders/ag32
Sep 14 18:45:35 Finished compiler/encoders/ag32                                  20s 861MB
Sep 14 18:45:35 Starting compiler/backend/x64
Sep 14 18:45:56 Finished compiler/backend/x64                                    20s   1GB
Sep 14 18:45:56 Starting compiler/backend/arm7
Sep 14 18:46:19 Finished compiler/backend/arm7                                   22s   1GB
Sep 14 18:46:19 Starting compiler/backend/arm8
Sep 14 18:46:40 Finished compiler/backend/arm8                                   20s   1GB
Sep 14 18:46:40 Starting compiler/backend/mips
Sep 14 18:47:01 Finished compiler/backend/mips                                   21s   1GB
Sep 14 18:47:01 Starting compiler/backend/riscv
Sep 14 18:47:22 Finished compiler/backend/riscv                                  21s   1GB
Sep 14 18:47:22 Starting compiler/backend/ag32
Sep 14 18:48:49 Finished compiler/backend/ag32                                 1m26s   1GB
Sep 14 18:48:49 Starting compiler/parsing/proofs
Sep 14 18:52:52 Finished compiler/parsing/proofs                               4m02s   1GB
Sep 14 18:52:52 Starting compiler/inference/proofs
Sep 14 18:55:39 Finished compiler/inference/proofs                             2m47s   1GB
Sep 14 18:55:39 Starting compiler/backend/semantics
Sep 14 18:58:52 FAILED: compiler/backend/semantics
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/machine-code/hoare-triple[0m
Scanning [1m$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[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$(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)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(HOLDIR)/src/hol88[0m
Scanning [1m$(HOLDIR)/src/real[0m
Scanning [1m$(HOLDIR)/src/floating-point[0m
Scanning [1m$(HOLDIR)/src/monad/more_monads[0m
Scanning [1m$(HOLDIR)/src/update[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Scanning [1m$(CAKEMLDIR)/semantics/alt_semantics[0m
Scanning [1m$(CAKEMLDIR)/semantics/alt_semantics/proofs[0m
Scanned 41 directories
Starting work on README.md
Starting work on backendPropsTheory
Starting work on closSemTheory
Starting work on flatSemTheory
README.md                                                                       (0s)     OK
Starting work on wordSemTheory
backendPropsTheory                                                             (12s)     OK
closSemTheory                                                                  (27s)     OK
Starting work on bvlSemTheory
Starting work on closPropsTheory
flatSemTheory                                                                  (31s)     OK
Starting work on dataSemTheory
bvlSemTheory                                                                   (22s)     OK
Starting work on bviSemTheory
wordSemTheory                                                                  (58s)     OK
Starting work on flatPropsTheory
bviSemTheory                                                                   (25s)     OK
Starting work on targetSemTheory
targetSemTheory                                                                (16s)     OK
Starting work on labSemTheory
flatPropsTheory                                                                (58s)     OK
Starting work on targetPropsTheory
labSemTheory                                                                   (28s)     OK
Starting work on labPropsTheory
targetPropsTheory                                                              (14s)     OK
Starting work on stackSemTheory
dataSemTheory                                                                 (126s)     OK
Starting work on dataPropsTheory
stackSemTheory                                                                 (38s)     OK
Starting work on data_monadTheory
data_monadTheory                                                               (14s)FAIL<1>
 Exception raised at TotalDefn.xDefine:
 at Defn.Hol_defn:
 between line 150, character 2 and line 161, character 67:
 at Defn.parse_quote:
 at Preterm.type-analysis:
 on line 152, characters 31-34:
 Couldn't infer type for overloaded name move
 error in quse /home/cug/hk324/cml-regression/cakeml-1981/compiler/backend/semantics/data_monadScript.sml : HOL_ERR {message = "at Defn.Hol_defn:\nbetween line 150, character 2 and line 161, character 67:\nat Defn.parse_quote:\nat Preterm.type-analysis:\non line 152, characters 31-34:\nCouldn't infer type for overloaded name move", origin_function = "xDefine", origin_structure = "TotalDefn"}
 error in load /home/cug/hk324/cml-regression/cakeml-1981/compiler/backend/semantics/data_monadScript : HOL_ERR {message = "at Defn.Hol_defn:\nbetween line 150, character 2 and line 161, character 67:\nat Defn.parse_quote:\nat Preterm.type-analysis:\non line 152, characters 31-34:\nCouldn't infer type for overloaded name move", origin_function = "xDefine", origin_structure = "TotalDefn"}
 Uncaught exception: HOL_ERR {message = "at Defn.Hol_defn:\nbetween line 150, character 2 and line 161, character 67:\nat Defn.parse_quote:\nat Preterm.type-analysis:\non line 152, characters 31-34:\nCouldn't infer type for overloaded name move", origin_function = "xDefine", origin_structure = "TotalDefn"}
closPropsTheory                                                               (159s)MKILLED
labPropsTheory                                                                 (64s)MKILLED
dataPropsTheory                                                                (28s)MKILLED