Job 1385

CakeML:1ba207029b09017b30a15c49363aa7c222c1d983
  Fix build failure caused by HOL change to ThyDataSexp API [Nov 06 00:51:29]
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 00:57:53 Claimed job
Nov 06 00:58:07 Building HOL
Nov 06 01:13:22 Starting developers
Nov 06 01:13:27 Finished developers                                               4s  99MB
Nov 06 01:13:27 Starting developers/bin
Nov 06 01:13:34 Finished developers/bin                                           6s   1GB
Nov 06 01:13:34 Starting semantics/ffi
Nov 06 01:13:45 Finished semantics/ffi                                           11s 236MB
Nov 06 01:13:45 Starting semantics
Nov 06 01:15:22 Finished semantics                                             1m36s   1GB
Nov 06 01:15:22 Starting semantics/proofs
Nov 06 01:18:55 Finished semantics/proofs                                      3m32s 940MB
Nov 06 01:18:55 Starting semantics/alt_semantics
Nov 06 01:19:04 Finished semantics/alt_semantics                                  9s 325MB
Nov 06 01:19:05 Starting semantics/alt_semantics/proofs
Nov 06 01:21:22 Finished semantics/alt_semantics/proofs                        2m16s 687MB
Nov 06 01:21:22 Starting basis/pure
Nov 06 01:24:22 Finished basis/pure                                            2m59s 714MB
Nov 06 01:24:22 Starting translator
Nov 06 01:27:07 Finished translator                                            2m45s   1GB
Nov 06 01:27:08 Starting compiler/parsing
Nov 06 01:28:22 Finished compiler/parsing                                      1m14s   2GB
Nov 06 01:28:22 Starting characteristic
Nov 06 01:34:38 Finished characteristic                                        6m16s   1GB
Nov 06 01:34:39 Starting translator/monadic
Nov 06 01:36:19 Finished translator/monadic                                    1m39s   1GB
Nov 06 01:36:19 Starting basis
Nov 06 02:13:11 Finished basis                                                36m36s  11GB
Nov 06 02:13:12 Starting compiler/inference
Nov 06 02:14:24 Finished compiler/inference                                    1m12s   1GB
Nov 06 02:14:24 Starting compiler/backend/reg_alloc
Nov 06 02:15:31 Finished compiler/backend/reg_alloc                            1m06s   1GB
Nov 06 02:15:31 Starting compiler/backend/gc
Nov 06 02:19:17 Finished compiler/backend/gc                                   3m43s   2GB
Nov 06 02:19:17 Starting compiler/backend
Nov 06 02:24:04 Finished compiler/backend                                      4m47s   3GB
Nov 06 02:24:05 Starting compiler/encoders/asm
Nov 06 02:24:28 Finished compiler/encoders/asm                                   23s 686MB
Nov 06 02:24:28 Starting compiler/encoders/x64
Nov 06 02:25:33 Finished compiler/encoders/x64                                 1m04s   1GB
Nov 06 02:25:33 Starting compiler/encoders/arm7
Nov 06 02:27:44 Finished compiler/encoders/arm7                                2m10s   1GB
Nov 06 02:27:44 Starting compiler/encoders/arm8
Nov 06 02:28:24 Finished compiler/encoders/arm8                                  39s 920MB
Nov 06 02:28:24 Starting compiler/encoders/mips
Nov 06 02:30:00 Finished compiler/encoders/mips                                1m35s   1GB
Nov 06 02:30:00 Starting compiler/encoders/riscv
Nov 06 02:31:52 Finished compiler/encoders/riscv                               1m51s 872MB
Nov 06 02:31:52 Starting compiler/encoders/ag32
Nov 06 02:32:11 Finished compiler/encoders/ag32                                  18s 602MB
Nov 06 02:32:11 Starting compiler/backend/x64
Nov 06 02:32:30 Finished compiler/backend/x64                                    18s   1GB
Nov 06 02:32:30 Starting compiler/backend/arm7
Nov 06 02:32:51 Finished compiler/backend/arm7                                   21s   1GB
Nov 06 02:32:52 Starting compiler/backend/arm8
Nov 06 02:33:11 Finished compiler/backend/arm8                                   19s   1GB
Nov 06 02:33:11 Starting compiler/backend/mips
Nov 06 02:33:31 Finished compiler/backend/mips                                   19s   1GB
Nov 06 02:33:31 Starting compiler/backend/riscv
Nov 06 02:33:52 Finished compiler/backend/riscv                                  20s   1GB
Nov 06 02:33:53 Starting compiler/backend/ag32
Nov 06 02:35:06 Finished compiler/backend/ag32                                 1m13s   1GB
Nov 06 02:35:06 Starting compiler/parsing/proofs
Nov 06 02:40:55 Finished compiler/parsing/proofs                               5m49s   1GB
Nov 06 02:40:56 Starting compiler/inference/proofs
Nov 06 02:43:32 Finished compiler/inference/proofs                             2m36s   1GB
Nov 06 02:43:32 Starting compiler/backend/semantics
Nov 06 03:14:42 Finished compiler/backend/semantics                           31m09s   1GB
Nov 06 03:14:42 Starting compiler/backend/reg_alloc/proofs
Nov 06 03:18:24 Finished compiler/backend/reg_alloc/proofs                     3m41s 767MB
Nov 06 03:18:24 Starting compiler/backend/proofs
Nov 06 03:27:07 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:   27s  user:   26s     OK
Starting work on bvi_letProofTheory
bvi_letProofTheory                              real:   20s  user:   19s     OK
Starting work on clos_annotateProofTheory
bvl_constProofTheory                            real:   56s  user:   55s     OK
Starting work on bvl_handleProofTheory
data_liveProofTheory                            real:   78s  user:   76s     OK
Starting work on bvi_to_dataProofTheory
clos_annotateProofTheory                        real:   30s  user:   29s     OK
Starting work on clos_callProofTheory
bvl_handleProofTheory                           real:   20s  user:   19s     OK
Starting work on bvl_inlineProofTheory
bvl_inlineProofTheory                           real:   34s  user:   32s     OK
Starting work on clos_fvsProofTheory
clos_fvsProofTheory                             real:   17s  user:   16s     OK
Starting work on clos_knownPropsTheory
clos_knownPropsTheory                           real:   11s  user:   10s     OK
Starting work on clos_letopProofTheory
clos_letopProofTheory                           real:   20s  user:   19s     OK
Starting work on clos_ticksProofTheory
bvi_tailrecProofTheory                          real:  198s  user:  195s     OK
Starting work on bvl_to_bviProofTheory
clos_ticksProofTheory                           real:   28s  user:   26s     OK
Starting work on clos_knownProofTheory
bvi_to_dataProofTheory                          real:  141s  user:  138s     OK
Starting work on clos_mtiProofTheory
clos_mtiProofTheory                             real:   37s  user:   36s     OK
Starting work on clos_numberProofTheory
clos_callProofTheory                            real:  185s  user:  181s     OK
Starting work on bvl_jumpProofTheory
clos_numberProofTheory                          real:   27s  user:   26s     OK
Starting work on word_simpProofTheory
bvl_jumpProofTheory                             real:   10s  user:    9s     OK
Starting work on word_bignumProofTheory
word_simpProofTheory                            real:   56s  user:   55s     OK
Starting work on word_gcFunctionsTheory
clos_knownProofTheory                           real:  136s  user:  133s     OK
Starting work on clos_to_bvlProofTheory
word_gcFunctionsTheory                          real:   31s  user:   30s     OK
Starting work on data_to_word_memoryProofTheory
bvl_to_bviProofTheory                           real:  207s  user:  202s     OK
Starting work on word_allocProofTheory
word_bignumProofTheory                          real:  211s  user:  207s     OK
Starting work on word_instProofTheory
word_instProofTheory                            real:   20s  user:   19sFAIL<1>
 <<HOL message: mk_functional: 
   pattern completion has added 4 clauses to the original specification.>>
 Saved definition __ "pull_ops_simp_def"
 <<HOL message: mk_functional: 
   pattern completion has added 5 clauses to the original specification.>>
 Saved definition __ "binary_branch_exp_def"
 Saved induction ___ "binary_branch_exp_ind"
 error in quse /home/cake/oven/regression/cakeml-1385/compiler/backend/proofs/word_instProofScript.sml : HOL_ERR {message = "on line 382, characters 76-81:\nIncorrect number of arguments to abbreviated operator result (expects 2)", origin_function = "parse_type", origin_structure = "Parse"}
 error in load /home/cake/oven/regression/cakeml-1385/compiler/backend/proofs/word_instProofScript : HOL_ERR {message = "on line 382, characters 76-81:\nIncorrect number of arguments to abbreviated operator result (expects 2)", origin_function = "parse_type", origin_structure = "Parse"}
 Uncaught exception: HOL_ERR {message = "on line 382, characters 76-81:\nIncorrect number of arguments to abbreviated operator result (expects 2)", origin_function = "parse_type", origin_structure = "Parse"}
clos_to_bvlProofTheory                                                  M-KILLED
data_to_word_memoryProofTheory                                          M-KILLED
word_allocProofTheory                                                   M-KILLED