Job 1386

CakeML:fed254846684a58d2774a88a33801834cc7865cd
  Fix parse error in word_instProof caused by set_grammar_ancestry change [Nov 06 02:12:05]
HOL:7306534b8eacfd26bbae4448d0ba21dc7dcaaf8b
  Again allow ancestral data to consume deltas all at once on theory-load [Nov 04 11:09:37]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Nov 06 03:30:02 Claimed job
Nov 06 03:30:04 Reusing HOL
Nov 06 03:30:51 Starting developers
Nov 06 03:30:56 Finished developers                                               4s 105MB
Nov 06 03:30:56 Starting developers/bin
Nov 06 03:31:03 Finished developers/bin                                           6s   1GB
Nov 06 03:31:03 Starting semantics/ffi
Nov 06 03:31:14 Finished semantics/ffi                                           11s 224MB
Nov 06 03:31:14 Starting semantics
Nov 06 03:32:40 Finished semantics                                             1m25s 906MB
Nov 06 03:32:40 Starting semantics/proofs
Nov 06 03:36:16 Finished semantics/proofs                                      3m35s   1GB
Nov 06 03:36:16 Starting semantics/alt_semantics
Nov 06 03:36:25 Finished semantics/alt_semantics                                  9s 289MB
Nov 06 03:36:25 Starting semantics/alt_semantics/proofs
Nov 06 03:38:41 Finished semantics/alt_semantics/proofs                        2m15s 849MB
Nov 06 03:38:41 Starting basis/pure
Nov 06 03:39:33 Finished basis/pure                                              51s 728MB
Nov 06 03:39:33 Starting translator
Nov 06 03:42:22 Finished translator                                            2m49s   1GB
Nov 06 03:42:22 Starting compiler/parsing
Nov 06 03:43:35 Finished compiler/parsing                                      1m12s   2GB
Nov 06 03:43:36 Starting characteristic
Nov 06 03:49:49 Finished characteristic                                        6m13s   2GB
Nov 06 03:49:49 Starting translator/monadic
Nov 06 03:51:30 Finished translator/monadic                                    1m40s   1GB
Nov 06 03:51:31 Starting basis
Nov 06 04:28:15 Finished basis                                                36m44s  11GB
Nov 06 04:28:16 Starting compiler/inference
Nov 06 04:29:22 Finished compiler/inference                                    1m05s   1GB
Nov 06 04:29:22 Starting compiler/backend/reg_alloc
Nov 06 04:30:29 Finished compiler/backend/reg_alloc                            1m06s   1GB
Nov 06 04:30:29 Starting compiler/backend/gc
Nov 06 04:34:02 Finished compiler/backend/gc                                   3m32s   2GB
Nov 06 04:34:02 Starting compiler/backend
Nov 06 04:38:50 Finished compiler/backend                                      4m47s   3GB
Nov 06 04:38:50 Starting compiler/encoders/asm
Nov 06 04:39:13 Finished compiler/encoders/asm                                   23s 900MB
Nov 06 04:39:14 Starting compiler/encoders/x64
Nov 06 04:39:40 Finished compiler/encoders/x64                                   25s 977MB
Nov 06 04:39:40 Starting compiler/encoders/arm7
Nov 06 04:40:32 Finished compiler/encoders/arm7                                  51s 729MB
Nov 06 04:40:32 Starting compiler/encoders/arm8
Nov 06 04:40:45 Finished compiler/encoders/arm8                                  13s 936MB
Nov 06 04:40:46 Starting compiler/encoders/mips
Nov 06 04:41:05 Finished compiler/encoders/mips                                  18s 944MB
Nov 06 04:41:05 Starting compiler/encoders/riscv
Nov 06 04:41:20 Finished compiler/encoders/riscv                                 15s 716MB
Nov 06 04:41:20 Starting compiler/encoders/ag32
Nov 06 04:41:39 Finished compiler/encoders/ag32                                  18s 879MB
Nov 06 04:41:39 Starting compiler/backend/x64
Nov 06 04:41:58 Finished compiler/backend/x64                                    19s   1GB
Nov 06 04:41:58 Starting compiler/backend/arm7
Nov 06 04:42:20 Finished compiler/backend/arm7                                   21s   1GB
Nov 06 04:42:20 Starting compiler/backend/arm8
Nov 06 04:42:39 Finished compiler/backend/arm8                                   18s   1GB
Nov 06 04:42:39 Starting compiler/backend/mips
Nov 06 04:42:58 Finished compiler/backend/mips                                   19s   1GB
Nov 06 04:42:58 Starting compiler/backend/riscv
Nov 06 04:43:19 Finished compiler/backend/riscv                                  20s   1GB
Nov 06 04:43:19 Starting compiler/backend/ag32
Nov 06 04:44:30 Finished compiler/backend/ag32                                 1m11s   1GB
Nov 06 04:44:31 Starting compiler/parsing/proofs
Nov 06 04:50:24 Finished compiler/parsing/proofs                               5m53s   1GB
Nov 06 04:50:24 Starting compiler/inference/proofs
Nov 06 04:54:03 Finished compiler/inference/proofs                             2m34s 903MB
Nov 06 04:54:03 Starting compiler/backend/semantics
Nov 06 05:25:28 Finished compiler/backend/semantics                           31m25s   2GB
Nov 06 05:25:28 Starting compiler/backend/reg_alloc/proofs
Nov 06 05:29:11 Finished compiler/backend/reg_alloc/proofs                     3m42s 978MB
Nov 06 05:29:12 Starting compiler/backend/proofs
Nov 06 05:50:25 FAILED: compiler/backend/proofs
Scanning $(HOLDIR)/examples/machine-code/multiword
Scanning $(HOLDIR)/examples/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc/lem_lib_stub
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/compiler/backend/reachability
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
Scanning $(HOLDIR)/examples/l3-machine-code/common
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/backend/gc
Scanning $(CAKEMLDIR)/compiler/backend/reachability/proofs
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/compiler/backend/semantics
Starting work on reachable_sptProofTheory
Starting work on README.md
Starting work on bvi_tailrecProofTheory
Starting work on data_liveProofTheory
README.md                                       real:    1s  user:    0s     OK
Starting work on data_simpProofTheory
reachable_sptProofTheory                        real:   12s  user:   11s     OK
Starting work on data_spaceProofTheory
data_simpProofTheory                            real:   15s  user:   14s     OK
Starting work on bvl_constProofTheory
data_spaceProofTheory                           real:   28s  user:   26s     OK
Starting work on bvi_letProofTheory
bvi_letProofTheory                              real:   20s  user:   19s     OK
Starting work on clos_annotateProofTheory
bvl_constProofTheory                            real:   55s  user:   54s     OK
Starting work on bvl_handleProofTheory
data_liveProofTheory                            real:   78s  user:   76s     OK
Starting work on bvi_to_dataProofTheory
clos_annotateProofTheory                        real:   28s  user:   26s     OK
Starting work on clos_callProofTheory
bvl_handleProofTheory                           real:   21s  user:   20s     OK
Starting work on bvl_inlineProofTheory
bvl_inlineProofTheory                           real:   35s  user:   34s     OK
Starting work on clos_fvsProofTheory
clos_fvsProofTheory                             real:   18s  user:   17s     OK
Starting work on clos_knownPropsTheory
clos_knownPropsTheory                           real:   11s  user:   10s     OK
Starting work on clos_letopProofTheory
clos_letopProofTheory                           real:   19s  user:   18s     OK
Starting work on clos_ticksProofTheory
bvi_tailrecProofTheory                          real:  195s  user:  192s     OK
Starting work on bvl_to_bviProofTheory
clos_ticksProofTheory                           real:   26s  user:   25s     OK
Starting work on clos_knownProofTheory
bvi_to_dataProofTheory                          real:  141s  user:  138s     OK
Starting work on clos_mtiProofTheory
clos_mtiProofTheory                             real:   37s  user:   35s     OK
Starting work on clos_numberProofTheory
clos_callProofTheory                            real:  187s  user:  183s     OK
Starting work on bvl_jumpProofTheory
clos_numberProofTheory                          real:   26s  user:   25s     OK
Starting work on word_simpProofTheory
bvl_jumpProofTheory                             real:   10s  user:    9s     OK
Starting work on word_bignumProofTheory
word_simpProofTheory                            real:   55s  user:   54s     OK
Starting work on word_gcFunctionsTheory
clos_knownProofTheory                           real:  136s  user:  134s     OK
Starting work on clos_to_bvlProofTheory
word_gcFunctionsTheory                          real:   30s  user:   29s     OK
Starting work on data_to_word_memoryProofTheory
bvl_to_bviProofTheory                           real:  205s  user:  201s     OK
Starting work on word_allocProofTheory
word_bignumProofTheory                          real:  211s  user:  207s     OK
Starting work on word_instProofTheory
word_instProofTheory                            real:   53s  user:   51s     OK
Starting work on word_removeProofTheory
clos_to_bvlProofTheory                          real:  220s  user:  215s     OK
Starting work on word_depthProofTheory
word_removeProofTheory                          real:   32s  user:   30s     OK
Starting work on flat_patternProofTheory
flat_patternProofTheory                         real:   50s  user:   49s     OK
Starting work on flat_to_closProofTheory
word_depthProofTheory                           real:   72s  user:   71s     OK
Starting work on lab_filterProofTheory
flat_to_closProofTheory                         real:   60s  user:   58s     OK
Starting work on stack_removeProofTheory
lab_filterProofTheory                           real:   60s  user:   59s     OK
Starting work on flat_elimProofTheory
stack_removeProofTheory                         real:  272s  user:  269s     OK
Starting work on lab_to_targetProofTheory
word_allocProofTheory                           real:  639s  user:  632s     OK
Starting work on word_to_wordProofTheory
word_to_wordProofTheory                         real:   70s  user:   68s     OK
Starting work on stack_allocProofTheory
data_to_word_memoryProofTheory                  real:  759s  user:  751s     OK
Starting work on data_to_word_gcProofTheory
lab_to_targetProofTheory                        real:  250s  user:  245s     OK
Starting work on stack_namesProofTheory
stack_namesProofTheory                          real:   35s  user:   33s     OK
Starting work on stack_rawcallProofTheory
stack_rawcallProofTheory                        real:   16s  user:   14sFAIL<1>
 comp_seq p1 p2 i default  default 
 k dest. p1 = StackFree k  p2 = Call NONE (INL dest) NONE
 
 failed.
 First unsolved sub-goal is
 
 k dest. p1 = StackFree k  p2 = Call NONE (INL dest) NONE
 
 Failed to prove theorem comp_seq_neq_IMP.
 Uncaught exception: HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
flat_elimProofTheory                                                    M-KILLED
stack_allocProofTheory                                                  M-KILLED
data_to_word_gcProofTheory                                              M-KILLED