Job 1387

CakeML:8e16563a1134805bbfb06b3befecc00f5fd2b239
  Fix parsing problems in stack_rawcallProof due to ancestry changes [Nov 07 03:52:31]
HOL:0c45436d2e80652f7fd2c0c6c22230f194a0d238
  Fix Unicode violation in previous [Nov 06 07:17:15]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Nov 07 04:00:23 Claimed job
Nov 07 04:00:30 Building HOL
Nov 07 04:15:49 Starting developers
Nov 07 04:15:54 Finished developers                                               4s 101MB
Nov 07 04:15:54 Starting developers/bin
Nov 07 04:16:01 Finished developers/bin                                           6s   1GB
Nov 07 04:16:01 Starting semantics/ffi
Nov 07 04:16:12 Finished semantics/ffi                                           11s 236MB
Nov 07 04:16:13 Starting semantics
Nov 07 04:17:48 Finished semantics                                             1m34s   1GB
Nov 07 04:17:48 Starting semantics/proofs
Nov 07 04:21:22 Finished semantics/proofs                                      3m34s 901MB
Nov 07 04:21:22 Starting semantics/alt_semantics
Nov 07 04:21:32 Finished semantics/alt_semantics                                  9s 325MB
Nov 07 04:21:32 Starting semantics/alt_semantics/proofs
Nov 07 04:23:47 Finished semantics/alt_semantics/proofs                        2m14s   1GB
Nov 07 04:23:47 Starting basis/pure
Nov 07 04:26:46 Finished basis/pure                                            2m58s   1GB
Nov 07 04:26:47 Starting translator
Nov 07 04:29:31 Finished translator                                            2m44s   1GB
Nov 07 04:29:31 Starting compiler/parsing
Nov 07 04:30:46 Finished compiler/parsing                                      1m14s   3GB
Nov 07 04:30:46 Starting characteristic
Nov 07 04:36:58 Finished characteristic                                        6m12s   1GB
Nov 07 04:36:59 Starting translator/monadic
Nov 07 04:38:39 Finished translator/monadic                                    1m40s   1GB
Nov 07 04:38:39 Starting basis
Nov 07 05:15:11 Finished basis                                                36m31s  14GB
Nov 07 05:15:11 Starting compiler/inference
Nov 07 05:16:25 Finished compiler/inference                                    1m13s   1GB
Nov 07 05:16:25 Starting compiler/backend/reg_alloc
Nov 07 05:17:32 Finished compiler/backend/reg_alloc                            1m06s   1GB
Nov 07 05:17:32 Starting compiler/backend/gc
Nov 07 05:21:17 Finished compiler/backend/gc                                   3m44s   2GB
Nov 07 05:21:17 Starting compiler/backend
Nov 07 05:26:08 Finished compiler/backend                                      4m49s   2GB
Nov 07 05:26:08 Starting compiler/encoders/asm
Nov 07 05:26:31 Finished compiler/encoders/asm                                   23s 874MB
Nov 07 05:26:31 Starting compiler/encoders/x64
Nov 07 05:27:37 Finished compiler/encoders/x64                                 1m05s 747MB
Nov 07 05:27:37 Starting compiler/encoders/arm7
Nov 07 05:29:48 Finished compiler/encoders/arm7                                2m10s   1GB
Nov 07 05:29:48 Starting compiler/encoders/arm8
Nov 07 05:30:28 Finished compiler/encoders/arm8                                  39s 937MB
Nov 07 05:30:29 Starting compiler/encoders/mips
Nov 07 05:32:06 Finished compiler/encoders/mips                                1m36s   1GB
Nov 07 05:32:06 Starting compiler/encoders/riscv
Nov 07 05:33:56 Finished compiler/encoders/riscv                               1m50s   1GB
Nov 07 05:33:56 Starting compiler/encoders/ag32
Nov 07 05:34:15 Finished compiler/encoders/ag32                                  18s 635MB
Nov 07 05:34:15 Starting compiler/backend/x64
Nov 07 05:34:33 Finished compiler/backend/x64                                    18s 932MB
Nov 07 05:34:33 Starting compiler/backend/arm7
Nov 07 05:34:55 Finished compiler/backend/arm7                                   21s   1GB
Nov 07 05:34:55 Starting compiler/backend/arm8
Nov 07 05:35:15 Finished compiler/backend/arm8                                   19s   1GB
Nov 07 05:35:15 Starting compiler/backend/mips
Nov 07 05:35:35 Finished compiler/backend/mips                                   19s   1GB
Nov 07 05:35:35 Starting compiler/backend/riscv
Nov 07 05:35:56 Finished compiler/backend/riscv                                  20s   1GB
Nov 07 05:35:56 Starting compiler/backend/ag32
Nov 07 05:37:10 Finished compiler/backend/ag32                                 1m13s   1GB
Nov 07 05:37:10 Starting compiler/parsing/proofs
Nov 07 05:42:58 Finished compiler/parsing/proofs                               5m47s 912MB
Nov 07 05:42:58 Starting compiler/inference/proofs
Nov 07 05:45:34 Finished compiler/inference/proofs                             2m36s   1GB
Nov 07 05:45:34 Starting compiler/backend/semantics
Nov 07 06:16:56 Finished compiler/backend/semantics                           31m21s   2GB
Nov 07 06:16:56 Starting compiler/backend/reg_alloc/proofs
Nov 07 06:20:44 Finished compiler/backend/reg_alloc/proofs                     3m47s 848MB
Nov 07 06:20:44 Starting compiler/backend/proofs
Nov 07 06:45:11 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:    1s     OK
Starting work on data_simpProofTheory
reachable_sptProofTheory                        real:   12s  user:   11s     OK
Starting work on data_spaceProofTheory
data_simpProofTheory                            real:   14s  user:   13s     OK
Starting work on bvl_constProofTheory
data_spaceProofTheory                           real:   28s  user:   27s     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:   77s  user:   75s     OK
Starting work on bvi_to_dataProofTheory
clos_annotateProofTheory                        real:   28s  user:   27s     OK
Starting work on clos_callProofTheory
bvl_handleProofTheory                           real:   21s  user:   20s     OK
Starting work on bvl_inlineProofTheory
bvl_inlineProofTheory                           real:   34s  user:   33s     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:   19s  user:   18s     OK
Starting work on clos_ticksProofTheory
bvi_tailrecProofTheory                          real:  198s  user:  195s     OK
Starting work on bvl_to_bviProofTheory
clos_ticksProofTheory                           real:   26s  user:   25s     OK
Starting work on clos_knownProofTheory
bvi_to_dataProofTheory                          real:  144s  user:  140s     OK
Starting work on clos_mtiProofTheory
clos_mtiProofTheory                             real:   38s  user:   36s     OK
Starting work on clos_numberProofTheory
clos_callProofTheory                            real:  184s  user:  181s     OK
Starting work on bvl_jumpProofTheory
bvl_jumpProofTheory                             real:   10s  user:    9s     OK
Starting work on word_simpProofTheory
clos_numberProofTheory                          real:   26s  user:   25s     OK
Starting work on word_bignumProofTheory
clos_knownProofTheory                           real:  135s  user:  133s     OK
Starting work on clos_to_bvlProofTheory
word_simpProofTheory                            real:   56s  user:   54s     OK
Starting work on word_gcFunctionsTheory
word_gcFunctionsTheory                          real:   31s  user:   29s     OK
Starting work on data_to_word_memoryProofTheory
bvl_to_bviProofTheory                           real:  201s  user:  197s     OK
Starting work on word_allocProofTheory
word_bignumProofTheory                          real:  212s  user:  209s     OK
Starting work on word_instProofTheory
word_instProofTheory                            real:   52s  user:   51s     OK
Starting work on word_removeProofTheory
clos_to_bvlProofTheory                          real:  219s  user:  214s     OK
Starting work on word_depthProofTheory
word_removeProofTheory                          real:   31s  user:   30s     OK
Starting work on flat_patternProofTheory
flat_patternProofTheory                         real:   51s  user:   49s     OK
Starting work on flat_to_closProofTheory
word_depthProofTheory                           real:   73s  user:   72s     OK
Starting work on lab_filterProofTheory
flat_to_closProofTheory                         real:   60s  user:   58s     OK
Starting work on stack_removeProofTheory
lab_filterProofTheory                           real:   62s  user:   60s     OK
Starting work on flat_elimProofTheory
stack_removeProofTheory                         real:  278s  user:  274s     OK
Starting work on lab_to_targetProofTheory
word_allocProofTheory                           real:  662s  user:  654s     OK
Starting work on word_to_wordProofTheory
word_to_wordProofTheory                         real:   69s  user:   68s     OK
Starting work on stack_allocProofTheory
data_to_word_memoryProofTheory                  real:  770s  user:  761s     OK
Starting work on data_to_word_gcProofTheory
lab_to_targetProofTheory                        real:  247s  user:  244s     OK
Starting work on stack_namesProofTheory
stack_namesProofTheory                          real:   35s  user:   33s     OK
Starting work on stack_rawcallProofTheory
stack_rawcallProofTheory                        real:   74s  user:   72s     OK
Starting work on word_to_stackProofTheory
data_to_word_gcProofTheory                      real:  262s  user:  258s     OK
Starting work on data_to_word_bignumProofTheory
word_to_stackProofTheory                        real:  133s  user:  130sFAIL<1>
 Saved theorem _____ "state_rel_set_var"
 Saved theorem _____ "state_rel_set_var2"
 Saved theorem _____ "wMoveSingle_thm"
 Saved theorem _____ "IS_SOME_get_vars_set_var"
 Saved theorem _____ "IS_SOME_get_vars_EVERY"
 Saved theorem _____ "evaluate_wMoveAux_seqsem"
 Saved theorem _____ "evaluate_SeqStackFree"
 error in quse /home/cake/oven/regression/cakeml-1387/compiler/backend/proofs/word_to_stackProofScript.sml : HOL_ERR {message = "No consistent parse", origin_function = "typed_parse_in_context", origin_structure = "Parse"}
 error in load /home/cake/oven/regression/cakeml-1387/compiler/backend/proofs/word_to_stackProofScript : HOL_ERR {message = "No consistent parse", origin_function = "typed_parse_in_context", origin_structure = "Parse"}
 Uncaught exception: HOL_ERR {message = "No consistent parse", origin_function = "typed_parse_in_context", origin_structure = "Parse"}
flat_elimProofTheory                                                    M-KILLED
stack_allocProofTheory                                                  M-KILLED
data_to_word_bignumProofTheory                                          M-KILLED