Job 977

CakeML:8e393beb8cb1fbeb5c2cfc264bd1e8189d236b0e
  Fix a typo in a comment "tyoe" [Jul 31 11:35:58]
HOL:8179c0d99ce8ead96edb7a913d49962b77102bf7
  Further tweaks to nlist material, getting TM example to build again [Aug 01 07:55:11]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Aug 02 13:14:20 Claimed job
Aug 02 13:15:00 Building HOL
Aug 02 13:22:51 Starting developers
Aug 02 13:22:52 Finished developers                                               0s  21MB
Aug 02 13:22:52 Starting developers/bin
Aug 02 13:24:25 Finished developers/bin                                        1m32s 238MB
Aug 02 13:24:25 Starting semantics/ffi
Aug 02 13:24:59 Finished semantics/ffi                                           33s 342MB
Aug 02 13:24:59 Starting semantics
Aug 02 13:26:29 Finished semantics                                             1m29s 850MB
Aug 02 13:26:29 Starting semantics/proofs
Aug 02 13:29:30 Finished semantics/proofs                                      3m00s   1GB
Aug 02 13:29:31 Starting semantics/alt_semantics
Aug 02 13:29:37 Finished semantics/alt_semantics                                  5s 307MB
Aug 02 13:29:38 Starting semantics/alt_semantics/proofs
Aug 02 13:31:26 Finished semantics/alt_semantics/proofs                        1m47s 864MB
Aug 02 13:31:26 Starting basis/pure
Aug 02 13:34:57 Finished basis/pure                                            3m30s 693MB
Aug 02 13:34:57 Starting translator
Aug 02 13:36:40 Finished translator                                            1m42s   1GB
Aug 02 13:36:40 Starting compiler/parsing
Aug 02 13:37:37 Finished compiler/parsing                                        56s   1GB
Aug 02 13:37:37 Starting characteristic
Aug 02 13:42:47 Finished characteristic                                        5m09s   1GB
Aug 02 13:42:48 Starting translator/monadic
Aug 02 13:44:11 Finished translator/monadic                                    1m23s   1GB
Aug 02 13:44:12 Starting basis
Aug 02 14:00:50 Finished basis                                                16m37s   2GB
Aug 02 14:00:50 Starting compiler/inference
Aug 02 14:02:40 Finished compiler/inference                                    1m49s   1GB
Aug 02 14:02:41 Starting compiler/backend/reg_alloc
Aug 02 14:03:39 Finished compiler/backend/reg_alloc                              58s   1GB
Aug 02 14:03:39 Starting compiler/backend/gc
Aug 02 14:12:44 Finished compiler/backend/gc                                   9m04s   1GB
Aug 02 14:12:45 Starting compiler/backend
Aug 02 14:12:46 Finished compiler/backend                                         0s  43MB
Aug 02 14:12:46 Starting compiler/encoders/asm
Aug 02 14:12:47 Finished compiler/encoders/asm                                    0s  37MB
Aug 02 14:12:47 Starting compiler/encoders/x64
Aug 02 14:13:44 Finished compiler/encoders/x64                                   56s 681MB
Aug 02 14:13:44 Starting compiler/encoders/arm7
Aug 02 14:15:20 Finished compiler/encoders/arm7                                1m35s   1GB
Aug 02 14:15:20 Starting compiler/encoders/arm8
Aug 02 14:15:49 Finished compiler/encoders/arm8                                  28s 866MB
Aug 02 14:15:50 Starting compiler/encoders/mips
Aug 02 14:16:54 Finished compiler/encoders/mips                                1m03s 827MB
Aug 02 14:16:54 Starting compiler/encoders/riscv
Aug 02 14:18:11 Finished compiler/encoders/riscv                               1m16s 792MB
Aug 02 14:18:11 Starting compiler/encoders/ag32
Aug 02 14:18:26 Finished compiler/encoders/ag32                                  14s 761MB
Aug 02 14:18:27 Starting compiler/backend/x64
Aug 02 14:18:43 Finished compiler/backend/x64                                    15s   1GB
Aug 02 14:18:43 Starting compiler/backend/arm7
Aug 02 14:19:01 Finished compiler/backend/arm7                                   17s   1GB
Aug 02 14:19:01 Starting compiler/backend/arm8
Aug 02 14:19:19 Finished compiler/backend/arm8                                   16s   1GB
Aug 02 14:19:19 Starting compiler/backend/mips
Aug 02 14:19:35 Finished compiler/backend/mips                                   16s   1GB
Aug 02 14:19:36 Starting compiler/backend/riscv
Aug 02 14:19:53 Finished compiler/backend/riscv                                  16s   1GB
Aug 02 14:19:53 Starting compiler/backend/ag32
Aug 02 14:21:01 Finished compiler/backend/ag32                                 1m06s   1GB
Aug 02 14:21:01 Starting compiler/parsing/proofs
Aug 02 14:26:36 Finished compiler/parsing/proofs                               5m34s 814MB
Aug 02 14:26:36 Starting compiler/inference/proofs
Aug 02 14:29:16 Finished compiler/inference/proofs                             2m39s 938MB
Aug 02 14:29:17 Starting compiler/backend/semantics
Aug 02 14:36:17 Finished compiler/backend/semantics                            6m59s   2GB
Aug 02 14:36:17 Starting compiler/backend/reg_alloc/proofs
Aug 02 14:39:27 Finished compiler/backend/reg_alloc/proofs                     3m09s 752MB
Aug 02 14:39:27 Starting compiler/backend/proofs
Aug 02 14:55:06 FAILED: compiler/backend/proofs
]0;Holmake: .]0;Holmake: ~/regression/HOL-8179c0d99ce8ead96edb7a913d49962b77102bf7/examples/machine-code/multiword]0;Holmake: ~/regression/HOL-8179c0d99ce8ead96edb7a913d49962b77102bf7/examples/machine-code/multiword[1mWorking in $(HOLDIR)/examples/machine-code/multiword[0m
]0;Holmake: .]0;Holmake: ..]0;Holmake: ~/regression/cakeml-977/basis/pure]0;Holmake: ~/regression/HOL-8179c0d99ce8ead96edb7a913d49962b77102bf7/examples/balanced_bst]0;Holmake: ~/regression/HOL-8179c0d99ce8ead96edb7a913d49962b77102bf7/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: ~/regression/cakeml-977/basis/pure]0;Holmake: ~/regression/HOL-8179c0d99ce8ead96edb7a913d49962b77102bf7/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-8179c0d99ce8ead96edb7a913d49962b77102bf7/examples/formal-languages]0;Holmake: ~/regression/HOL-8179c0d99ce8ead96edb7a913d49962b77102bf7/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-8179c0d99ce8ead96edb7a913d49962b77102bf7/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-8179c0d99ce8ead96edb7a913d49962b77102bf7/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-8179c0d99ce8ead96edb7a913d49962b77102bf7/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-8179c0d99ce8ead96edb7a913d49962b77102bf7/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-8179c0d99ce8ead96edb7a913d49962b77102bf7/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ~/regression/cakeml-977/basis/pure]0;Holmake: ~/regression/cakeml-977/misc]0;Holmake: ~/regression/HOL-8179c0d99ce8ead96edb7a913d49962b77102bf7/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-8179c0d99ce8ead96edb7a913d49962b77102bf7/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-977/misc]0;Holmake: ~/regression/cakeml-977/developers]0;Holmake: ~/regression/cakeml-977/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-977/misc]0;Holmake: ~/regression/cakeml-977/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-977/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-977/misc]0;Holmake: ~/regression/cakeml-977/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression/cakeml-977/basis/pure]0;Holmake: ~/regression/cakeml-977/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ..]0;Holmake: ../reg_alloc]0;Holmake: ~/regression/cakeml-977/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-977/semantics]0;Holmake: ~/regression/cakeml-977/semantics/ffi]0;Holmake: ~/regression/cakeml-977/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-977/semantics]0;Holmake: ~/regression/cakeml-977/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/regression/cakeml-977/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-977/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ../reg_alloc]0;Holmake: ~/regression/cakeml-977/unverified/reg_alloc]0;Holmake: ~/regression/cakeml-977/unverified/reg_alloc[1mWorking in $(CAKEMLDIR)/unverified/reg_alloc[0m
]0;Holmake: ../reg_alloc]0;Holmake: ../reg_alloc[1mWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc[0m
]0;Holmake: ..]0;Holmake: ../../encoders/asm]0;Holmake: ~/regression/HOL-8179c0d99ce8ead96edb7a913d49962b77102bf7/examples/l3-machine-code/common]0;Holmake: ~/regression/HOL-8179c0d99ce8ead96edb7a913d49962b77102bf7/examples/l3-machine-code/common[1mWorking in $(HOLDIR)/examples/l3-machine-code/common[0m
]0;Holmake: ../../encoders/asm]0;Holmake: ../../encoders/asm[1mWorking in $(CAKEMLDIR)/compiler/encoders/asm[0m
]0;Holmake: ..]0;Holmake: ~/regression/cakeml-977/semantics/proofs]0;Holmake: ~/regression/cakeml-977/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ..]0;Holmake: ..[1mWorking in $(CAKEMLDIR)/compiler/backend[0m
]0;Holmake: .]0;Holmake: ../gc]0;Holmake: ../gc[1mWorking in $(CAKEMLDIR)/compiler/backend/gc[0m
]0;Holmake: .]0;Holmake: ../reg_alloc/proofs]0;Holmake: ~/regression/cakeml-977/translator/monadic]0;Holmake: ~/regression/cakeml-977/characteristic]0;Holmake: ~/regression/cakeml-977/compiler/parsing]0;Holmake: ~/regression/cakeml-977/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ~/regression/cakeml-977/characteristic]0;Holmake: ~/regression/cakeml-977/translator]0;Holmake: ~/regression/cakeml-977/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ~/regression/cakeml-977/characteristic]0;Holmake: ~/regression/cakeml-977/characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ~/regression/cakeml-977/translator/monadic]0;Holmake: ~/regression/cakeml-977/translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ../reg_alloc/proofs]0;Holmake: ../reg_alloc/proofs[1mWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
]0;Holmake: .]0;Holmake: ../semantics]0;Holmake: ../semantics[1mWorking in $(CAKEMLDIR)/compiler/backend/semantics[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/compiler/backend/proofs[0m
Starting work on bvi_tailrecProofTheory
Starting work on data_liveProofTheory
Starting work on data_simpProofTheory
Starting work on data_spaceProofTheory
data_simpProofTheory                                                                                       OK
Starting work on bvl_constProofTheory
data_spaceProofTheory                                                                                      OK
Starting work on bvl_jumpProofTheory
bvl_jumpProofTheory                                                                                        OK
Starting work on bvi_letProofTheory
data_liveProofTheory                                                                                       OK
Starting work on bvi_to_dataProofTheory
bvi_letProofTheory                                                                                         OK
Starting work on clos_annotateProofTheory
bvl_constProofTheory                                                                                       OK
Starting work on bvl_handleProofTheory
clos_annotateProofTheory                                                                                   OK
Starting work on clos_callProofTheory
bvl_handleProofTheory                                                                                      OK
Starting work on bvl_inlineProofTheory
bvl_inlineProofTheory                                                                                      OK
Starting work on clos_fvsProofTheory
clos_fvsProofTheory                                                                                        OK
Starting work on clos_knownPropsTheory
clos_knownPropsTheory                                                                                      OK
Starting work on clos_letopProofTheory
bvi_to_dataProofTheory                                                                                     OK
Starting work on clos_ticksProofTheory
clos_letopProofTheory                                                                                      OK
Starting work on clos_labelsProofTheory
clos_ticksProofTheory                                                                                      OK
Starting work on clos_knownProofTheory
bvi_tailrecProofTheory                                                                                     OK
Starting work on bvl_to_bviProofTheory
clos_labelsProofTheory                                                                                     OK
Starting work on clos_mtiProofTheory
clos_mtiProofTheory                                                                                        OK
Starting work on clos_numberProofTheory
clos_numberProofTheory                                                                                     OK
Starting work on word_simpProofTheory
clos_knownProofTheory                                                                                      OK
Starting work on word_bignumProofTheory
word_simpProofTheory                                                                                       OK
Starting work on word_gcFunctionsTheory
clos_callProofTheory                                                                                       OK
Starting work on clos_to_bvlProofTheory
word_gcFunctionsTheory                                                                                     OK
Starting work on data_to_word_memoryProofTheory
bvl_to_bviProofTheory                                                                                      OK
Starting work on word_allocProofTheory
word_bignumProofTheory                                                                                     OK
Starting work on word_instProofTheory
clos_to_bvlProofTheory                                                                                     OK
Starting work on word_removeProofTheory
word_instProofTheory                                                                                       OK
Starting work on flat_elimProofTheory
word_removeProofTheory                                                                                     OK
Starting work on flat_exh_matchProofTheory
flat_elimProofTheory                                                                                       OK
Starting work on flat_reorder_matchProofTheory
flat_exh_matchProofTheory                                                                                  OK
Starting work on flat_to_patProofTheory
flat_reorder_matchProofTheory                                                                              OK
Starting work on flat_uncheck_ctorsProofTheory
flat_uncheck_ctorsProofTheory                                                                              OK
Starting work on lab_filterProofTheory
flat_to_patProofTheory                                                                                     OK
Starting work on stack_removeProofTheory
lab_filterProofTheory                                                                                      OK
Starting work on pat_to_closProofTheory
pat_to_closProofTheory                                                                                     OK
Starting work on source_to_flatProofTheory
data_to_word_memoryProofTheory                                                                             OK
Starting work on stack_allocProofTheory
source_to_flatProofTheory                                                                                  OK
Starting work on stack_namesProofTheory
word_allocProofTheory                                                                                      OK
Starting work on word_to_wordProofTheory
stack_namesProofTheory                                                                                     OK
Starting work on word_to_stackProofTheory
word_to_wordProofTheory                                                                                    OK
Starting work on data_to_word_gcProofTheory
stack_removeProofTheory                                                                                    OK
Starting work on lab_to_targetProofTheory
lab_to_targetProofTheory                                                                          FAILED! <1>
      mem_store_byte_def,
      labSemTheory.assert_def,
      mem_store_byte_aux_def,
      mem_store_def,
      labSemTheory.addr_def,
      ...
      ]
 error in quse /home/myreen/regression/cakeml-977/compiler/backend/proofs/lab_to_targetProofScript.sml : Fail "Static Errors"
 error in load lab_to_targetProofScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"
stack_allocProofTheory                                                                               M-KILLED
word_to_stackProofTheory                                                                             M-KILLED
data_to_word_gcProofTheory                                                                           M-KILLED