Job 1193

CakeML:df30bf50b46fc366b9af4840506b199138767565
  Retire 'top' as a variable name [Feb 20 14:30:35]
#724 (constrain_op_case)
Merging into:210f5c2ce0804027acbac59d87eab48cdeed1625
  Merge pull request #727 from IlmariReissumies/ad-hoc-overloading [Feb 21 09:48:53]
HOL:9d20add95c75b8c69157845df5d5e74f24633371
  Merge remote-tracking branch 'origin/interaction-guide-update' into d [Feb 19 09:30:56]
Machine:stove 4.15.0-55-generic x86_64 GNU/Linux

Feb 21 11:11:59 Claimed job
Feb 21 11:12:01 Reusing HOL
Feb 21 11:12:46 Starting developers
Feb 21 11:12:50 Finished developers                                               4s 128MB
Feb 21 11:12:50 Starting developers/bin
Feb 21 11:12:57 Finished developers/bin                                           6s   1GB
Feb 21 11:12:57 Starting semantics/ffi
Feb 21 11:13:07 Finished semantics/ffi                                            9s 249MB
Feb 21 11:13:07 Starting semantics
Feb 21 11:14:24 Finished semantics                                             1m16s   1GB
Feb 21 11:14:24 Starting semantics/proofs
Feb 21 11:17:34 Finished semantics/proofs                                      3m09s 988MB
Feb 21 11:17:34 Starting semantics/alt_semantics
Feb 21 11:17:42 Finished semantics/alt_semantics                                  7s 333MB
Feb 21 11:17:42 Starting semantics/alt_semantics/proofs
Feb 21 11:19:44 Finished semantics/alt_semantics/proofs                        2m01s 838MB
Feb 21 11:19:44 Starting basis/pure
Feb 21 11:20:32 Finished basis/pure                                              47s 662MB
Feb 21 11:20:32 Starting translator
Feb 21 11:22:59 Finished translator                                            2m26s   1GB
Feb 21 11:22:59 Starting compiler/parsing
Feb 21 11:24:02 Finished compiler/parsing                                      1m03s   2GB
Feb 21 11:24:02 Starting characteristic
Feb 21 11:29:46 Finished characteristic                                        5m44s   2GB
Feb 21 11:29:46 Starting translator/monadic
Feb 21 11:31:18 Finished translator/monadic                                    1m31s   1GB
Feb 21 11:31:18 Starting basis
Feb 21 12:01:00 Finished basis                                                29m40s  16GB
Feb 21 12:01:00 Starting compiler/inference
Feb 21 12:01:58 Finished compiler/inference                                      58s   1GB
Feb 21 12:01:58 Starting compiler/backend/reg_alloc
Feb 21 12:02:59 Finished compiler/backend/reg_alloc                            1m00s   1GB
Feb 21 12:02:59 Starting compiler/backend/gc
Feb 21 12:06:10 Finished compiler/backend/gc                                   3m10s   2GB
Feb 21 12:06:10 Starting compiler/backend
Feb 21 12:10:18 Finished compiler/backend                                      4m08s   3GB
Feb 21 12:10:18 Starting compiler/encoders/asm
Feb 21 12:10:39 Finished compiler/encoders/asm                                   20s 880MB
Feb 21 12:10:39 Starting compiler/encoders/x64
Feb 21 12:11:33 Finished compiler/encoders/x64                                   53s 970MB
Feb 21 12:11:33 Starting compiler/encoders/arm7
Feb 21 12:13:10 Finished compiler/encoders/arm7                                1m36s   1GB
Feb 21 12:13:10 Starting compiler/encoders/arm8
Feb 21 12:13:42 Finished compiler/encoders/arm8                                  31s 823MB
Feb 21 12:13:42 Starting compiler/encoders/mips
Feb 21 12:14:45 Finished compiler/encoders/mips                                1m03s 895MB
Feb 21 12:14:45 Starting compiler/encoders/riscv
Feb 21 12:16:03 Finished compiler/encoders/riscv                               1m17s   1GB
Feb 21 12:16:03 Starting compiler/encoders/ag32
Feb 21 12:16:21 Finished compiler/encoders/ag32                                  17s 666MB
Feb 21 12:16:21 Starting compiler/backend/x64
Feb 21 12:16:39 Finished compiler/backend/x64                                    18s   1GB
Feb 21 12:16:39 Starting compiler/backend/arm7
Feb 21 12:16:58 Finished compiler/backend/arm7                                   19s   1GB
Feb 21 12:16:58 Starting compiler/backend/arm8
Feb 21 12:17:16 Finished compiler/backend/arm8                                   17s   1GB
Feb 21 12:17:16 Starting compiler/backend/mips
Feb 21 12:17:34 Finished compiler/backend/mips                                   18s   1GB
Feb 21 12:17:35 Starting compiler/backend/riscv
Feb 21 12:17:54 Finished compiler/backend/riscv                                  19s   1GB
Feb 21 12:17:54 Starting compiler/backend/ag32
Feb 21 12:19:00 Finished compiler/backend/ag32                                 1m06s 961MB
Feb 21 12:19:00 Starting compiler/parsing/proofs
Feb 21 12:24:33 Finished compiler/parsing/proofs                               5m32s   1GB
Feb 21 12:24:33 Starting compiler/inference/proofs
Feb 21 12:26:57 Finished compiler/inference/proofs                             2m23s   1GB
Feb 21 12:26:57 Starting compiler/backend/semantics
Feb 21 12:52:52 Finished compiler/backend/semantics                           25m54s   2GB
Feb 21 12:52:52 Starting compiler/backend/reg_alloc/proofs
Feb 21 12:56:09 Finished compiler/backend/reg_alloc/proofs                     3m16s 860MB
Feb 21 12:56:09 Starting compiler/backend/proofs
Feb 21 13:39:22 FAILED: compiler/backend/proofs
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)/compiler/backend/reachability[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
Scanning [1m$(CAKEMLDIR)/compiler/backend/gc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reachability/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/semantics[0m
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:   10s  user:    9s     OK
Starting work on data_spaceProofTheory
data_simpProofTheory                            real:   14s  user:   13s     OK
Starting work on bvl_constProofTheory
data_spaceProofTheory                           real:   24s  user:   23s     OK
Starting work on bvi_letProofTheory
bvi_letProofTheory                              real:   18s  user:   17s     OK
Starting work on clos_annotateProofTheory
data_liveProofTheory                            real:   60s  user:   59s     OK
Starting work on bvi_to_dataProofTheory
bvl_constProofTheory                            real:   46s  user:   45s     OK
Starting work on bvl_handleProofTheory
clos_annotateProofTheory                        real:   24s  user:   23s     OK
Starting work on clos_callProofTheory
bvl_handleProofTheory                           real:   18s  user:   17s     OK
Starting work on bvl_inlineProofTheory
bvl_inlineProofTheory                           real:   29s  user:   28s     OK
Starting work on clos_fvsProofTheory
clos_fvsProofTheory                             real:   15s  user:   14s     OK
Starting work on clos_knownPropsTheory
clos_knownPropsTheory                           real:   10s  user:    9s     OK
Starting work on clos_letopProofTheory
clos_letopProofTheory                           real:   17s  user:   16s     OK
Starting work on clos_ticksProofTheory
bvi_tailrecProofTheory                          real:  156s  user:  154s     OK
Starting work on bvl_to_bviProofTheory
clos_ticksProofTheory                           real:   22s  user:   21s     OK
Starting work on clos_knownProofTheory
bvi_to_dataProofTheory                          real:  124s  user:  121s     OK
Starting work on clos_mtiProofTheory
clos_mtiProofTheory                             real:   32s  user:   31s     OK
Starting work on clos_numberProofTheory
clos_callProofTheory                            real:  159s  user:  156s     OK
Starting work on bvl_jumpProofTheory
clos_numberProofTheory                          real:   23s  user:   22s     OK
Starting work on word_simpProofTheory
bvl_jumpProofTheory                             real:   10s  user:    9s     OK
Starting work on word_bignumProofTheory
word_simpProofTheory                            real:   50s  user:   49s     OK
Starting work on word_gcFunctionsTheory
clos_knownProofTheory                           real:  118s  user:  116s     OK
Starting work on clos_to_bvlProofTheory
word_gcFunctionsTheory                          real:   25s  user:   24s     OK
Starting work on data_to_word_memoryProofTheory
bvl_to_bviProofTheory                           real:  179s  user:  176s     OK
Starting work on word_allocProofTheory
word_bignumProofTheory                          real:  191s  user:  189s     OK
Starting work on word_instProofTheory
word_instProofTheory                            real:   46s  user:   45s     OK
Starting work on word_removeProofTheory
clos_to_bvlProofTheory                          real:  193s  user:  189s     OK
Starting work on word_depthProofTheory
word_removeProofTheory                          real:   28s  user:   27s     OK
Starting work on flat_patternProofTheory
word_depthProofTheory                           real:   62s  user:   60s     OK
Starting work on flat_to_closProofTheory
flat_patternProofTheory                         real:   44s  user:   43s     OK
Starting work on lab_filterProofTheory
flat_to_closProofTheory                         real:   55s  user:   53s     OK
Starting work on stack_removeProofTheory
lab_filterProofTheory                           real:   54s  user:   52s     OK
Starting work on flat_elimProofTheory
flat_elimProofTheory                            real:   60s  user:   59s     OK
Starting work on source_to_flatProofTheory
source_to_flatProofTheory                       real:   97s  user:   95s     OK
Starting work on stack_allocProofTheory
stack_removeProofTheory                         real:  236s  user:  233s     OK
Starting work on lab_to_targetProofTheory
word_allocProofTheory                           real:  555s  user:  550s     OK
Starting work on word_to_wordProofTheory
data_to_word_memoryProofTheory                  real:  598s  user:  593s     OK
Starting work on stack_namesProofTheory
stack_namesProofTheory                          real:   29s  user:   28s     OK
Starting work on stack_rawcallProofTheory
word_to_wordProofTheory                         real:   61s  user:   59s     OK
Starting work on data_to_word_gcProofTheory
stack_rawcallProofTheory                        real:   64s  user:   62s     OK
Starting work on word_to_stackProofTheory
lab_to_targetProofTheory                        real:  207s  user:  204s     OK
Starting work on word_elimProofTheory
stack_allocProofTheory                          real:  376s  user:  371s     OK
word_elimProofTheory                            real:  117s  user:  115s     OK
data_to_word_gcProofTheory                      real:  214s  user:  211s     OK
Starting work on data_to_word_bignumProofTheory
data_to_word_bignumProofTheory                  real:  232s  user:  230s     OK
Starting work on data_to_word_assignProofTheory
word_to_stackProofTheory                        real: 1487s  user: 1471s     OK
Starting work on stack_to_labProofTheory
stack_to_labProofTheory                         real:   92s  user:   90sFAIL<1>
 Saved definition __ "halt_view_def"
 Saved induction ___ "halt_view_ind"
 Saved theorem _____ "next_lab_non_zero"
 Saved theorem _____ "stack_to_lab_lab_pres"
 Saved theorem _____ "stack_to_lab_lab_pres_T"
 Saved theorem _____ "flatten_T_F"
 Saved theorem _____ "prog_to_section_labels_ok"
 error in quse /home/cur/sao/cakeml/regression/cakeml-1193/compiler/backend/proofs/stack_to_labProofScript.sml : HOL_ERR {message = "No consistent parse", origin_function = "typed_parse_in_context", origin_structure = "Parse"}
 error in load /home/cur/sao/cakeml/regression/cakeml-1193/compiler/backend/proofs/stack_to_labProofScript : 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"}
data_to_word_assignProofTheory                                          M-KILLED