Job 1524

CakeML:fddd5c18d0255133e7cc5e6da1aeefaef9e73472
  record type fixes for basis/ [May 15 13:49:34]
HOL:1354090035c466ccae632435bb016c0bebf281d7
  Move large_numberTheory to examples/probability [May 13 23:47:06]
Machine:oven3 4.19.67.1.amd64-smp

May 16 10:59:19 Claimed job
May 16 10:59:31 Building HOL
May 16 11:31:50 Starting developers
May 16 11:31:57 Finished developers                                               7s 108MB
May 16 11:31:57 Starting developers/bin
May 16 11:32:11 Finished developers/bin                                          13s   1GB
May 16 11:32:11 Starting semantics/ffi
May 16 11:32:36 Finished semantics/ffi                                           24s 270MB
May 16 11:32:37 Starting semantics
May 16 11:35:55 Finished semantics                                             3m17s   1GB
May 16 11:35:55 Starting semantics/proofs
May 16 11:43:52 Finished semantics/proofs                                      7m56s   1GB
May 16 11:43:52 Starting semantics/alt_semantics
May 16 11:44:13 Finished semantics/alt_semantics                                 20s 369MB
May 16 11:44:13 Starting semantics/alt_semantics/proofs
May 16 11:49:05 Finished semantics/alt_semantics/proofs                        4m51s 800MB
May 16 11:49:05 Starting basis/pure
May 16 11:55:07 Finished basis/pure                                            6m01s 822MB
May 16 11:55:07 Starting translator
May 16 12:01:51 Finished translator                                            6m44s   1GB
May 16 12:01:52 Starting compiler/parsing
May 16 12:04:36 Finished compiler/parsing                                      2m44s   3GB
May 16 12:04:37 Starting characteristic
May 16 12:16:38 Finished characteristic                                       12m01s   1GB
May 16 12:16:38 Starting translator/monadic
May 16 12:20:07 Finished translator/monadic                                    3m29s   1GB
May 16 12:20:08 Starting basis
May 16 13:55:43 Finished basis                                              1h35m35s  16GB
May 16 13:55:44 Starting compiler/inference
May 16 13:58:25 Finished compiler/inference                                    2m41s   1GB
May 16 13:58:25 Starting compiler/backend/reg_alloc
May 16 14:00:32 Finished compiler/backend/reg_alloc                            2m06s   1GB
May 16 14:00:32 Starting compiler/backend/gc
May 16 14:02:17 FAILED: compiler/backend/gc
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[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)/examples/fun-op-sem/lprefix_lub[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)/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)/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
Starting work on multiwordTheory
Starting work on asmTheory
Starting work on backend_commonTheory
Starting work on README.md
README.md                                                                                                                                                    real:    0s  user:    0s     OK
Starting work on gc_sharedTheory
asmTheory                                                                                                                                                    real:   15s  user:   13s     OK
backend_commonTheory                                                                                                                                         real:   20s  user:   19s     OK
Starting work on closLangTheory
Starting work on stackLangTheory
gc_sharedTheory                                                                                                                                              real:   28s  user:   26s     OK
Starting work on copying_gcTheory
stackLangTheory                                                                                                                                              real:   26s  user:   25s     OK
Starting work on wordLangTheory
closLangTheory                                                                                                                                               real:   29s  user:   28s     OK
Starting work on dataLangTheory
multiwordTheory                                                                                                                                              real:   52s  user:   49s     OK
Starting work on mc_multiwordTheory
copying_gcTheory                                                                                                                                             real:   26s  user:   24s     OK
Starting work on gen_gcTheory
dataLangTheory                                                                                                                                               real:   23s  user:   21s     OK
wordLangTheory                                                                                                                                               real:   33s  user:   31s     OK
Starting work on word_depthTheory
Starting work on word_allocTheory
gen_gcTheory                                                                                                                                                 real:   46s  user:   44sFAIL<1>
 error in load /root/regression/cakeml-1524/compiler/backend/gc/gen_gcScript : HOL_ERR {message = "No parse of quotation leads to success", origin_function = "Q_TAC", origin_structure = "Tactical"}
 Proof of 
 
 conf state h t.
   gc_inv conf state heap0 roots0  (state.r2 = [])  (state.r4 = h::t) 
   (state.r3 = []) 
   gc_inv conf (state with <|r2 := h::t; r4 := []|>) heap0 roots0
 
 failed.
 Uncaught exception: HOL_ERR {message = "No parse of quotation leads to success", origin_function = "Q_TAC", origin_structure = "Tactical"}
mc_multiwordTheory                                                                                                                                                                   M-KILLED
word_depthTheory                                                                                                                                                                     M-KILLED
word_allocTheory                                                                                                                                                                     M-KILLED